Left-hand side let (#7078)

* Left-hand side let (using)

Based on initial implementation by @ak3n

* Only inherit user-written let bindings in with clauses (i.e. not
@-patterns)

* Don't lose outer let bindings (when in a where clause)

CHANGELOG.md

@@ -22,6 +22,28 @@ Language
 
 Changes to type checker and other components defining the Agda language.
 
+* Left-hand side let: `using x ← e`
+
+  This new construct can be using in left-hand sides together with `with` and
+  `rewrite` to give names to subexpressions. It is the left-hand side
+  counterpart of a `let`-binding and supports the same limited form of pattern
+  matching on eta-expandable record values.
+
+  It can be quite useful when you have a function doing a series of nested
+  `with`s that share some expressions. Something like
+
+  ```agda
+  fun : A → B
+  fun x using z ← e with foo z
+  ... | p with bar z
+  ...   | q = r
+  ```
+
+  Here the expression `e` doesn't have to be repeated in the two `with`-expressions.
+
+  As in a `with`, multiple bindings can be separated by a `|`, and variables to
+  the left are in scope in bindings to the right.
+
 Reflection
 ----------
 

doc/user-manual/language/with-abstraction.lagda.rst

@@ -483,7 +483,7 @@ of the vector argument using ``suc-+`` first.
     suc-+ (suc m) n rewrite suc-+ m n = refl
 
     infixr 1 _×_
-    _×_ : ∀ {a b} (A : Set a) (B : Set b) → Set ?
+    _×_ : ∀ {a b} (A : Set a) (B : Set b) → Set _
     A × B = Σ A (λ _ → B)
 
     splitAt : ∀ m {n} → Vec A (m + n) → Vec A m × Vec A n
@@ -501,6 +501,59 @@ You can alternate arbitrarily many ``rewrite`` and pattern-matching
 ``with`` clauses and still perform a ``with`` abstraction afterwards
 if necessary.
 
+.. _with-using:
+
+..
+  ::
+  module with-using {a} {A : Set a} where
+    open import Agda.Builtin.Nat
+    open import Agda.Builtin.Sigma
+    open import Agda.Builtin.Equality
+    open import Agda.Builtin.Unit
+
+    open with-invert {A = A} hiding (splitAt)
+
+Left-hand side let-bindings
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+An alternative to an irrefutable ``with``, when you just need to bind
+a variable or do simple unpacking of record values, is to use a
+``using``-binding. This is the left-hand side counterpart of a
+:ref:`let-binding <let-expressions>` and supports the same limited
+form of pattern matching.
+
+For instance, the irrefutable ``with`` used in ``splitAt`` in the
+section above can be changed to ``using``:
+
+::
+
+    splitAt : ∀ m {n} → Vec A (m + n) → Vec A m × Vec A n
+    splitAt zero    xs       = ([] , xs)
+    splitAt (suc m) (x ∷ xs) using (ys , zs) ← splitAt m xs = (x ∷ ys , zs)
+
+Variables bound with ``using`` are in scope in following ``with``
+clauses, allowing you to reuse bindings across multiple nested ``with`` s:
+
+::
+
+    contrived : ∀ m {n} → Vec A (m + n) → (Vec A m → Bool) → (Vec A n → Bool) → Bool
+    contrived m xs p q using (ys , zs) ← splitAt m xs
+                       with p ys
+    ... | true = true
+    ... | false with q zs
+    ...   | true  = false
+    ...   | false = true
+
+For convenience, multiple bindings can be separated by ``|``, and this
+has the same meaning as repeating the ``using`` keyword: bindings to
+the left are in scope to the right.
+
+Contrary to ``with`` and ``rewrite``, ``using`` does not perform any
+abstraction over the bound terms, but simply introduces a local
+binding. This can make it much cheaper to use than an irrefutable
+``with`` in situations where the goal type and context are big and
+expensive to normalise, and the abstraction isn't required.
+
 ..
   ::
   module with-rewrite where

src/full/Agda/Interaction/Highlighting/FromAbstract.hs

@@ -327,6 +327,7 @@ instance (HasRange n, Hilite p, Hilite e) => Hilite (RewriteEqn' x n p e) where
   hilite = \case
     Rewrite es    -> hilite $ fmap snd es
     Invert _x pes -> hilite pes
+    LeftLet pes   -> hilite pes
 
 instance Hilite a => Hilite (A.Clause' a) where
   hilite (A.Clause lhs strippedPats rhs wh _catchall) =

src/full/Agda/Syntax/Abstract/UsedNames.hs

@@ -133,6 +133,7 @@ instance BoundAndUsed e => BoundAndUsed (LHSCore' e) where
 instance (BoundAndUsed x, BoundAndUsed p, BoundAndUsed e) => BoundAndUsed (RewriteEqn' q x p e) where
   boundAndUsed (Rewrite es)  = boundAndUsed $ snd <$> es
   boundAndUsed (Invert _ bs) = parBoundAndUsed (namedThing <$> bs) <> boundAndUsed (nameOf <$> bs)
+  boundAndUsed (LeftLet bs)  = boundAndUsed bs
 
 instance BoundAndUsed LetBinding where
   boundAndUsed = \ case   -- Note: binder last since it's not recursive

src/full/Agda/Syntax/Abstract/Views.hs

@@ -385,6 +385,7 @@ instance (ExprLike qn, ExprLike nm, ExprLike p, ExprLike e) => ExprLike (Rewrite
   recurseExpr f = \case
     Rewrite es    -> Rewrite <$> recurseExpr f es
     Invert qn pes -> Invert <$> recurseExpr f qn <*> recurseExpr f pes
+    LeftLet pes   -> LeftLet <$> recurseExpr f pes
 
 instance ExprLike WhereDeclarations where
   recurseExpr f (WhereDecls a b c) = WhereDecls a b <$> recurseExpr f c

src/full/Agda/Syntax/Common.hs

@@ -2969,16 +2969,19 @@ instance NFData CoverageCheck
 data RewriteEqn' qn nm p e
   = Rewrite (List1 (qn, e))             -- ^ @rewrite e@
   | Invert qn (List1 (Named nm (p, e))) -- ^ @with p <- e in eq@
+  | LeftLet (List1 (p, e))              -- ^ @using p <- e@
   deriving (Eq, Show, Functor, Foldable, Traversable)
 
 instance (NFData qn, NFData nm, NFData p, NFData e) => NFData (RewriteEqn' qn nm p e) where
   rnf = \case
     Rewrite es    -> rnf es
     Invert qn pes -> rnf (qn, pes)
+    LeftLet pes   -> rnf pes
 
 instance (Pretty nm, Pretty p, Pretty e) => Pretty (RewriteEqn' qn nm p e) where
   pretty = \case
     Rewrite es   -> prefixedThings (text "rewrite") $ List1.toList (pretty . snd <$> es)
+    LeftLet pes  -> prefixedThings (text "using") [pretty p <+> "<-" <+> pretty e | (p, e) <- List1.toList pes]
     Invert _ pes -> prefixedThings (text "invert") $ List1.toList (namedWith <$> pes) where
 
       namedWith (Named nm (p, e)) =
@@ -2991,11 +2994,13 @@ instance (HasRange qn, HasRange nm, HasRange p, HasRange e) => HasRange (Rewrite
   getRange = \case
     Rewrite es    -> getRange es
     Invert qn pes -> getRange (qn, pes)
+    LeftLet pes   -> getRange pes
 
 instance (KillRange qn, KillRange nm, KillRange e, KillRange p) => KillRange (RewriteEqn' qn nm p e) where
   killRange = \case
     Rewrite es    -> killRangeN Rewrite es
     Invert qn pes -> killRangeN Invert qn pes
+    LeftLet pes   -> killRangeN LeftLet pes
 
 -----------------------------------------------------------------------------
 -- * Information on expanded ellipsis (@...@)

src/full/Agda/Syntax/Concrete/Generic.hs

@@ -197,7 +197,8 @@ instance ExprLike LHS where
 instance (ExprLike qn, ExprLike e) => ExprLike (RewriteEqn' qn nm p e) where
   mapExpr f = \case
     Rewrite es    -> Rewrite (mapExpr f es)
-    Invert qn pes -> Invert qn (fmap (fmap $ fmap $ mapExpr f) pes)
+    Invert qn pes -> Invert qn $ (fmap . fmap . fmap . mapExpr) f pes
+    LeftLet pes   -> LeftLet $ (fmap . fmap . mapExpr) f pes
   foldExpr     = __IMPOSSIBLE__
   traverseExpr = __IMPOSSIBLE__
 

src/full/Agda/Syntax/Parser/Parser.y

@@ -1093,19 +1093,11 @@ CommaImportNames1
 LHS :: { [RewriteEqn] -> [WithExpr] -> LHS }
 LHS : Expr1 {% exprToLHS $1 }
 
-WithClause :: { [Either RewriteEqn (List1 (Named Name Expr))] }
-WithClause
-  : 'with' WithExprs WithClause
-    {% fmap (++ $3) (buildWithStmt $2)  }
-  | 'rewrite' UnnamedWithExprs WithClause
-    { Left (Rewrite $ fmap ((),) $2) : $3 }
-  | {- empty -} { [] }
-
 -- Parsing either an expression @e@ or a @(rewrite | with p <-) e1 | ... | en@.
 HoleContent :: { HoleContent }
 HoleContent
   : Expr                   {  HoleContentExpr    $1 }
-  | WithClause
+  | WHS
     {% fmap HoleContentRewrite $ forM $1 $ \case
          Left r  -> pure r
          Right{} -> parseError "Cannot declare a 'with' abstraction from inside a hole."
@@ -1200,8 +1192,11 @@ FunClause
 WHS :: { [Either RewriteEqn (List1 (Named Name Expr))] }
 WHS
   : {- empty -}                           { [] }
-  | 'with'    WithExprs        WithClause {% fmap (++ $3) (buildWithStmt $2) }
-  | 'rewrite' UnnamedWithExprs WithClause { Left (Rewrite $ fmap ((),) $2) : $3 }
+  | 'with'    WithExprs        WHS {% fmap (++ $3) (buildWithStmt $2) }
+  | 'rewrite' UnnamedWithExprs WHS { Left (Rewrite $ fmap ((),) $2) : $3 }
+  | 'using'   UnnamedWithExprs WHS {% do
+      eqn <- buildUsingStmt $2
+      pure $ Left eqn : $3 }
 
 RHS :: { RHSOrTypeSigs }
 RHS
@@ -2233,6 +2228,13 @@ buildWithStmt nes = do
   let rws = groupByEither ws
   pure $ map (first (Invert ())) rws
 
+buildUsingStmt :: List1 Expr -> Parser RewriteEqn
+buildUsingStmt es = do
+  mpatexprs <- mapM exprToAssignment es
+  case mapM (fmap $ \(pat, _, expr) -> (pat, expr)) mpatexprs of
+    Nothing -> parseError' (rStart' $ getRange es) "Expected assignments"
+    Just assignments -> pure $ LeftLet assignments
+
 buildSingleWithStmt ::
   Named Name Expr ->
   Parser (Either (Named Name (Pattern, Expr)) (Named Name Expr))

src/full/Agda/Syntax/Translation/AbstractToConcrete.hs

@@ -1136,6 +1136,7 @@ instance (ToConcrete p, ToConcrete a) => ToConcrete (RewriteEqn' qn A.BindName p
       pe <- toConcrete pe
       n  <- toConcrete n
       pure $ Named n pe
+    LeftLet pes -> LeftLet <$> mapM toConcrete pes
 
 instance ToConcrete (Maybe A.BindName) where
   type ConOfAbs (Maybe A.BindName) = Maybe C.Name

src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs

@@ -2745,6 +2745,7 @@ instance ToAbstract (RewriteEqn' () A.BindName A.Pattern A.Expr) where
     Invert _ pes -> do
       qn <- withFunctionName "-invert"
       pure $ Invert qn pes
+    LeftLet pes -> pure $ LeftLet pes
 
 instance ToAbstract C.RewriteEqn where
   type AbsOfCon C.RewriteEqn = RewriteEqn' () A.BindName A.Pattern A.Expr
@@ -2761,19 +2762,28 @@ instance ToAbstract C.RewriteEqn where
       -- constraints of the form @p ≡ e@.
       nps <- forM nps $ \ (n, p) -> do
         -- first the pattern
+        p <- toAbsPat p
+        -- and then the name
+        n <- toAbstract $ fmap (NewName WithBound . C.mkBoundName_) n
+        pure (n, p)
+      -- we finally reassemble the telescope
+      pure $ List1.zipWith (\ (n,p) e -> Named n (p, e)) nps es
+    LeftLet pes -> fmap LeftLet $ forM pes $ \ (p, e) -> do
+      -- first check the expression: the pattern may shadow
+      -- some of the variables mentioned in it!
+      e <- toAbstract e
+      p <- toAbsPat p
+      pure (p, e)
+    where
+      toAbsPat p = do
         -- Expand puns if optHiddenArgumentPuns is True.
         puns <- optHiddenArgumentPuns <$> pragmaOptions
         p <- return $ if puns then expandPuns p else p
         p <- parsePattern p
         p <- toAbstract p
         checkPatternLinearity p (typeError . RepeatedVariablesInPattern)
         bindVarsToBind
-        p <- toAbstract p
-        -- and then the name
-        n <- toAbstract $ fmap (NewName WithBound . C.mkBoundName_) n
-        pure (n, p)
-      -- we finally reassemble the telescope
-      pure $ List1.zipWith (\ (n,p) e -> Named n (p, e)) nps es
+        toAbstract p
 
 instance ToAbstract AbstractRHS where
   type AbsOfCon AbstractRHS = A.RHS

src/full/Agda/TypeChecking/Rules/Def.hs

@@ -13,6 +13,8 @@ import Data.IntSet (IntSet)
 import qualified Data.IntSet as IntSet
 import qualified Data.List as List
 import Data.Maybe
+import Data.Map (Map)
+import qualified Data.Map as Map
 import Data.Semigroup (Semigroup((<>)))
 
 import Agda.Interaction.Options
@@ -251,10 +253,13 @@ checkFunDefS :: Type             -- ^ the type we expect the function to have
              -> Maybe QName      -- ^ is it a with function (if so, what's the name of the parent function)
              -> A.DefInfo        -- ^ range info
              -> QName            -- ^ the name of the function
-             -> Maybe Substitution -- ^ substitution (from with abstraction) that needs to be applied to module parameters
+             -> Maybe (Substitution, Map Name LetBinding)
+                                 -- ^ substitution (from with abstraction) that needs to be applied
+                                 --   to module parameters, and let-bindings inherited from parent
+                                 --   clause
              -> [A.Clause]       -- ^ the clauses to check
              -> TCM ()
-checkFunDefS t ai extlam with i name withSub cs = do
+checkFunDefS t ai extlam with i name withSubAndLets cs = do
 
     traceCall (CheckFunDefCall (getRange i) name cs True) $ do
         reportSDoc "tc.def.fun" 10 $
@@ -281,9 +286,9 @@ checkFunDefS t ai extlam with i name withSub cs = do
         -- Check the clauses
         cs <- traceCall NoHighlighting $ do -- To avoid flicker.
           forM (zip cs [0..]) $ \ (c, clauseNo) -> do
-            atClause name clauseNo t withSub c $ do
+            atClause name clauseNo t (fst <$> withSubAndLets) c $ do
               (c,b) <- applyModalityToContextFunBody ai $ do
-                checkClause t withSub c
+                checkClause t withSubAndLets c
               -- Andreas, 2013-11-23 do not solve size constraints here yet
               -- in case we are checking the body of an extended lambda.
               -- 2014-04-24: The size solver requires each clause to be
@@ -554,6 +559,7 @@ data WithFunctionProblem
     , wfPermFinal  :: Permutation                       -- ^ Final permutation (including permutation for the parent clause).
     , wfClauses    :: List1 A.Clause                    -- ^ The given clauses for the with function
     , wfCallSubst :: Substitution                       -- ^ Subtsitution to generate call for the parent.
+    , wfLetBindings :: Map Name LetBinding              -- ^ The let-bindings in scope of the parent (in the parent context)
     }
 
 checkSystemCoverage
@@ -694,13 +700,22 @@ checkClauseLHS t withSub c@(A.Clause lhs@(A.SpineLHS i x aps) strippedPats rhs0
 
 checkClause
   :: Type          -- ^ Type of function defined by this clause.
-  -> Maybe Substitution  -- ^ Module parameter substitution arising from with-abstraction.
+  -> Maybe (Substitution, Map Name LetBinding)  -- ^ Module parameter substitution arising from with-abstraction, and inherited let-bindings.
   -> A.SpineClause -- ^ Clause.
-  -> TCM (Clause,ClausesPostChecks)  -- ^ Type-checked clause
+  -> TCM (Clause, ClausesPostChecks)  -- ^ Type-checked clause
 
-checkClause t withSub c@(A.Clause lhs@(A.SpineLHS i x aps) strippedPats rhs0 wh catchall) = do
+checkClause t withSubAndLets c@(A.Clause lhs@(A.SpineLHS i x aps) strippedPats rhs0 wh catchall) = do
+  let withSub       = fst <$> withSubAndLets
   cxtNames <- reverse . map (fst . unDom) <$> getContext
   checkClauseLHS t withSub c $ \ lhsResult@(LHSResult npars delta ps absurdPat trhs patSubst asb psplit ixsplit) -> do
+
+    let installInheritedLets k
+          | Just (withSub, lets) <- withSubAndLets = do
+            lets' <- traverse makeOpen $ applySubst (patSubst `composeS` withSub) lets
+            locallyTC eLetBindings (lets' <>) k
+          | otherwise = k
+
+    installInheritedLets $ do
         -- Note that we might now be in irrelevant context,
         -- in case checkLeftHandSide walked over an irrelevant projection pattern.
 
@@ -910,9 +925,16 @@ checkRHS i x aps t lhsResult@(LHSResult _ delta ps absurdPat trhs _ _asb _ _) rh
       rewriteEqnRHS qname eq $
         List1.ifNull qes {-then-} rs {-else-} $ \ qes -> Rewrite qes : rs
     Invert qname pes -> invertEqnRHS qname (List1.toList pes) rs
+    LeftLet pes -> usingEqnRHS (List1.toList pes) rs
 
     where
 
+    -- @using@ clauses
+    usingEqnRHS :: [(A.Pattern, A.Expr)] -> [A.RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
+    usingEqnRHS pes rs = do
+      let letBindings = for (List1.toList pes) $ \(p, e) -> A.LetPatBind (LetRange $ getRange e) p e
+      checkLetBindings letBindings $ rewriteEqnsRHS rs strippedPats rhs wh
+
     -- @invert@ clauses
     invertEqnRHS :: QName -> [Named A.BindName (A.Pattern,A.Expr)] -> [A.RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
     invertEqnRHS qname pes rs = do
@@ -1115,13 +1137,16 @@ checkWithRHS x aux t (LHSResult npars delta ps _absurdPat trhs _ _asb _ _) vtys0
           , "            delta2" <+> do escapeContext impossible (size delta) $ addContext delta1 $ prettyTCM delta2
           ]
 
-        return (v, WithFunction x aux t delta delta1 delta2 vtys t' ps npars perm' perm finalPerm cs argsS)
+        -- Only inherit user-written let bindings from parent clauses. Others, like @-patterns,
+        -- should not be carried over.
+        lets <- Map.filter ((== UserWritten) . letOrigin) <$> (traverse getOpen =<< viewTC eLetBindings)
+
+        return (v, WithFunction x aux t delta delta1 delta2 vtys t' ps npars perm' perm finalPerm cs argsS lets)
 
 -- | Invoked in empty context.
 checkWithFunction :: [Name] -> WithFunctionProblem -> TCM (Maybe Term)
 checkWithFunction _ NoWithFunction = return Nothing
-checkWithFunction cxtNames (WithFunction f aux t delta delta1 delta2 vtys b qs npars perm' perm finalPerm cs argsS) = do
-
+checkWithFunction cxtNames (WithFunction f aux t delta delta1 delta2 vtys b qs npars perm' perm finalPerm cs argsS lets) = do
   let -- Δ₁ ws Δ₂ ⊢ withSub : Δ′    (where Δ′ is the context of the parent lhs)
       withSub :: Substitution
       withSub = let as = map (snd . unArg) vtys in
@@ -1225,7 +1250,7 @@ checkWithFunction cxtNames (WithFunction f aux t delta delta1 delta2 vtys b qs n
   -- Check the with function
   let info = Info.mkDefInfo (nameConcrete $ qnameName aux) noFixity' PublicAccess abstr (getRange cs)
   ai <- defArgInfo <$> getConstInfo f
-  checkFunDefS withFunType ai Nothing (Just f) info aux (Just withSub) $ List1.toList cs
+  checkFunDefS withFunType ai Nothing (Just f) info aux (Just (withSub, lets)) $ List1.toList cs
   return $ Just $ call_in_parent
 
 -- | Type check a where clause.