chore: move to new frontend

src/Lean/Meta/Closure.lean

@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -94,8 +95,7 @@ BTW, this module also provides the `zeta : Bool` flag. When set to true, it
 expands all let-variables occurring in the target expression.
 -/
 
-namespace Lean
-namespace Meta
+namespace Lean.Meta
 namespace Closure
 
 structure ToProcessElement :=
@@ -123,52 +123,55 @@ structure State :=
 
 abbrev ClosureM := ReaderT Context $ StateRefT State MetaM
 
-@[inline] def visitLevel (f : Level → ClosureM Level) (u : Level) : ClosureM Level :=
-if !u.hasMVar && !u.hasParam then pure u
-else do
-  s ← get;
+@[inline] def visitLevel (f : Level → ClosureM Level) (u : Level) : ClosureM Level := do
+if !u.hasMVar && !u.hasParam then
+  pure u
+else
+  let s ← get
   match s.visitedLevel.find? u with
   | some v => pure v
   | none   => do
-    v ← f u;
-    modify $ fun s => { s with visitedLevel := s.visitedLevel.insert u v };
+    let v ← f u
+    modify fun s => { s with visitedLevel := s.visitedLevel.insert u v }
     pure v
 
-@[inline] def visitExpr (f : Expr → ClosureM Expr) (e : Expr) : ClosureM Expr :=
-if !e.hasLevelParam && !e.hasFVar && !e.hasMVar then pure e
-else do
-  s ← get;
+@[inline] def visitExpr (f : Expr → ClosureM Expr) (e : Expr) : ClosureM Expr := do
+if !e.hasLevelParam && !e.hasFVar && !e.hasMVar then
+  pure e
+else
+  let s ← get
   match s.visitedExpr.find? e with
   | some r => pure r
-  | none   => do
-    r ← f e;
-    modify $ fun s => { s with visitedExpr := s.visitedExpr.insert e r };
+  | none   =>
+    let r ← f e
+    modify fun s => { s with visitedExpr := s.visitedExpr.insert e r }
     pure r
 
 def mkNewLevelParam (u : Level) : ClosureM Level := do
-s ← get;
-let p := (`u).appendIndexAfter s.nextLevelIdx;
-modify $ fun s => { s with levelParams := s.levelParams.push p, nextLevelIdx := s.nextLevelIdx + 1, levelArgs := s.levelArgs.push u };
+let s ← get
+let p := (`u).appendIndexAfter s.nextLevelIdx
+modify fun s => { s with levelParams := s.levelParams.push p, nextLevelIdx := s.nextLevelIdx + 1, levelArgs := s.levelArgs.push u }
 pure $ mkLevelParam p
 
 partial def collectLevelAux : Level → ClosureM Level
-| u@(Level.succ v _)      => do v ← visitLevel collectLevelAux v; pure $ u.updateSucc! v
-| u@(Level.max v w _)     => do v ← visitLevel collectLevelAux v; w ← visitLevel collectLevelAux w; pure $ u.updateMax! v w
-| u@(Level.imax v w _)    => do v ← visitLevel collectLevelAux v; w ← visitLevel collectLevelAux w; pure $ u.updateIMax! v w
+| u@(Level.succ v _)      => do return u.updateSucc! (← visitLevel collectLevelAux v)
+| u@(Level.max v w _)     => do return u.updateMax! (← visitLevel collectLevelAux v) (← visitLevel collectLevelAux w)
+| u@(Level.imax v w _)    => do return u.updateIMax! (← visitLevel collectLevelAux v) (← visitLevel collectLevelAux w)
 | u@(Level.mvar mvarId _) => mkNewLevelParam u
 | u@(Level.param _ _)     => mkNewLevelParam u
 | u@(Level.zero _)        => pure u
 
 def collectLevel (u : Level) : ClosureM Level := do
--- u ← instantiateLevelMVars u;
+-- u ← instantiateLevelMVars u
 visitLevel collectLevelAux u
 
 def preprocess (e : Expr) : ClosureM Expr := do
-e ← instantiateMVars e;
-ctx ← read;
+let e ← instantiateMVars e
+let ctx ← read
 -- If we are not zeta-expanding let-decls, then we use `check` to find
 -- which let-decls are dependent. We say a let-decl is dependent if its lambda abstraction is type incorrect.
-when (!ctx.zeta) $ liftM $ check e;
+if !ctx.zeta then
+  check e
 pure e
 
 /--
@@ -176,134 +179,128 @@ pure e
   The correctness of the procedure does not rely on unique user names.
   Recall that the pretty printer takes care of unintended collisions. -/
 def mkNextUserName : ClosureM Name := do
-s ← get;
-let n := (`_x).appendIndexAfter s.nextExprIdx;
-modify $ fun s => { s with nextExprIdx := s.nextExprIdx + 1 };
+let s ← get
+let n := (`_x).appendIndexAfter s.nextExprIdx
+modify fun s => { s with nextExprIdx := s.nextExprIdx + 1 }
 pure n
 
 def pushToProcess (elem : ToProcessElement) : ClosureM Unit :=
 modify fun s => { s with toProcess := s.toProcess.push elem }
 
-partial def collectExprAux : Expr → ClosureM Expr
-| e =>
-  let collect (e : Expr) := visitExpr collectExprAux e;
-  match e with
-  | Expr.proj _ _ s _    => do s ← collect s; pure (e.updateProj! s)
-  | Expr.forallE _ d b _ => do d ← collect d; b ← collect b; pure (e.updateForallE! d b)
-  | Expr.lam _ d b _     => do d ← collect d; b ← collect b; pure (e.updateLambdaE! d b)
-  | Expr.letE _ t v b _  => do t ← collect t; v ← collect v; b ← collect b; pure (e.updateLet! t v b)
-  | Expr.app f a _       => do f ← collect f; a ← collect a; pure (e.updateApp! f a)
-  | Expr.mdata _ b _     => do b ← collect b; pure (e.updateMData! b)
-  | Expr.sort u _        => do u ← collectLevel u; pure (e.updateSort! u)
-  | Expr.const c us _    => do us ← us.mapM collectLevel; pure (e.updateConst! us)
-  | Expr.mvar mvarId _   => do
-    mvarDecl ← getMVarDecl mvarId;
-    type ← preprocess mvarDecl.type;
-    type ← collect type;
-    newFVarId ← mkFreshFVarId;
-    userName ← mkNextUserName;
-    modify fun s => { s with
-      newLocalDeclsForMVars := s.newLocalDeclsForMVars.push $ LocalDecl.cdecl (arbitrary _) newFVarId userName type BinderInfo.default,
-      exprMVarArgs          := s.exprMVarArgs.push e
-    };
-    pure $ mkFVar newFVarId
-  | Expr.fvar fvarId _ => do
-    ctx ← read;
-    decl ← getLocalDecl fvarId;
-    match ctx.zeta, decl.value? with
-    | true, some value => do value ← preprocess value; collect value
-    | _,    _          => do
-      newFVarId ← mkFreshFVarId;
-      pushToProcess ⟨fvarId, newFVarId⟩;
-      pure $ mkFVar newFVarId
-  | e => pure e
+partial def collectExprAux (e : Expr) : ClosureM Expr := do
+let collect (e : Expr) := visitExpr collectExprAux e
+match e with
+| Expr.proj _ _ s _    => return e.updateProj! (← collect s)
+| Expr.forallE _ d b _ => return e.updateForallE! (← collect d) (← collect b)
+| Expr.lam _ d b _     => return e.updateLambdaE! (← collect d) (← collect b)
+| Expr.letE _ t v b _  => return e.updateLet! (← collect t) (← collect v) (← collect b)
+| Expr.app f a _       => return e.updateApp! (← collect f) (← collect a)
+| Expr.mdata _ b _     => return e.updateMData! (← collect b)
+| Expr.sort u _        => return e.updateSort! (← collectLevel u)
+| Expr.const c us _    => return e.updateConst! (← us.mapM collectLevel)
+| Expr.mvar mvarId _   =>
+  let mvarDecl ← getMVarDecl mvarId
+  let type ← preprocess mvarDecl.type
+  let type ← collect type
+  let newFVarId ← mkFreshFVarId
+  let userName ← mkNextUserName
+  modify fun s => { s with
+    newLocalDeclsForMVars := s.newLocalDeclsForMVars.push $ LocalDecl.cdecl (arbitrary _) newFVarId userName type BinderInfo.default,
+    exprMVarArgs          := s.exprMVarArgs.push e
+  }
+  return mkFVar newFVarId
+| Expr.fvar fvarId _ =>
+  match (← read).zeta, (← getLocalDecl fvarId).value? with
+  | true, some value => collect (← preprocess value)
+  | _,    _          =>
+    let newFVarId ← mkFreshFVarId
+    pushToProcess ⟨fvarId, newFVarId⟩
+    return mkFVar newFVarId
+| e => pure e
 
 def collectExpr (e : Expr) : ClosureM Expr := do
-e ← preprocess e;
+let e ← preprocess e
 visitExpr collectExprAux e
 
-partial def pickNextToProcessAux (lctx : LocalContext)
-    : Nat → Array ToProcessElement → ToProcessElement → ToProcessElement × Array ToProcessElement
-| i, toProcess, elem =>
-  if h : i < toProcess.size then
-    let elem' := toProcess.get ⟨i, h⟩;
-    if (lctx.get! elem.fvarId).index < (lctx.get! elem'.fvarId).index then
-      pickNextToProcessAux (i+1) (toProcess.set ⟨i, h⟩ elem) elem'
-    else
-      pickNextToProcessAux (i+1) toProcess elem
+partial def pickNextToProcessAux (lctx : LocalContext) (i : Nat) (toProcess : Array ToProcessElement) (elem : ToProcessElement)
+    : ToProcessElement × Array ToProcessElement :=
+if h : i < toProcess.size then
+  let elem' := toProcess.get ⟨i, h⟩
+  if (lctx.get! elem.fvarId).index < (lctx.get! elem'.fvarId).index then
+    pickNextToProcessAux lctx (i+1) (toProcess.set ⟨i, h⟩ elem) elem'
   else
-    (elem, toProcess)
+    pickNextToProcessAux lctx (i+1) toProcess elem
+else
+  (elem, toProcess)
 
 def pickNextToProcess? : ClosureM (Option ToProcessElement) := do
-lctx ← getLCtx;
-s ← get;
+let lctx ← getLCtx
+let s ← get
 if s.toProcess.isEmpty then pure none
 else
   modifyGet fun s =>
-    let elem      := s.toProcess.back;
-    let toProcess := s.toProcess.pop;
-    let (elem, toProcess) := pickNextToProcessAux lctx 0 toProcess elem;
+    let elem      := s.toProcess.back
+    let toProcess := s.toProcess.pop
+    let (elem, toProcess) := pickNextToProcessAux lctx 0 toProcess elem
     (some elem, { s with toProcess := toProcess })
 
 def pushFVarArg (e : Expr) : ClosureM Unit :=
 modify fun s => { s with exprFVarArgs := s.exprFVarArgs.push e }
 
 def pushLocalDecl (newFVarId : FVarId) (userName : Name) (type : Expr) (bi := BinderInfo.default) : ClosureM Unit := do
-type ← collectExpr type;
+let type ← collectExpr type
 modify fun s => { s with newLocalDecls := s.newLocalDecls.push $ LocalDecl.cdecl (arbitrary _) newFVarId userName type bi }
 
-partial def process : Unit → ClosureM Unit
-| _ => do
-  elem? ← pickNextToProcess?;
-  match elem? with
-  | none => pure ()
-  | some ⟨fvarId, newFVarId⟩ => do
-    localDecl ← getLocalDecl fvarId;
-    match localDecl with
-    | LocalDecl.cdecl _ _ userName type bi => do
-      pushLocalDecl newFVarId userName type bi;
-      pushFVarArg (mkFVar fvarId);
-      process ()
-    | LocalDecl.ldecl _ _ userName type val _ => do
-      zetaFVarIds ← getZetaFVarIds;
-      if !zetaFVarIds.contains fvarId then do
-        /- Non-dependent let-decl
+partial def process : ClosureM Unit := do
+match (← pickNextToProcess?) with
+| none => pure ()
+| some ⟨fvarId, newFVarId⟩ =>
+  let localDecl ← getLocalDecl fvarId
+  match localDecl with
+  | LocalDecl.cdecl _ _ userName type bi =>
+    pushLocalDecl newFVarId userName type bi
+    pushFVarArg (mkFVar fvarId)
+    process
+  | LocalDecl.ldecl _ _ userName type val _ =>
+    let zetaFVarIds ← getZetaFVarIds
+    if !zetaFVarIds.contains fvarId then
+      /- Non-dependent let-decl
 
-           Recall that if `fvarId` is in `zetaFVarIds`, then we zeta-expanded it
-           during type checking (see `check` at `collectExpr`).
+          Recall that if `fvarId` is in `zetaFVarIds`, then we zeta-expanded it
+          during type checking (see `check` at `collectExpr`).
 
-           Our type checker may zeta-expand declarations that are not needed, but this
-           check is conservative, and seems to work well in practice. -/
-        pushLocalDecl newFVarId userName type;
-        pushFVarArg (mkFVar fvarId);
-        process ()
-      else do
-        /- Dependent let-decl -/
-        type ← collectExpr type;
-        val  ← collectExpr val;
-        modify fun s => { s with newLetDecls := s.newLetDecls.push $ LocalDecl.ldecl (arbitrary _) newFVarId userName type val false };
-        /- We don't want to interleave let and lambda declarations in our closure. So, we expand any occurrences of newFVarId
-           at `newLocalDecls` -/
-        modify fun s => { s with newLocalDecls := s.newLocalDecls.map (replaceFVarIdAtLocalDecl newFVarId val) };
-        process ()
+          Our type checker may zeta-expand declarations that are not needed, but this
+          check is conservative, and seems to work well in practice. -/
+      pushLocalDecl newFVarId userName type
+      pushFVarArg (mkFVar fvarId)
+      process
+    else
+      /- Dependent let-decl -/
+      let type ← collectExpr type
+      let val  ← collectExpr val
+      modify fun s => { s with newLetDecls := s.newLetDecls.push $ LocalDecl.ldecl (arbitrary _) newFVarId userName type val false }
+      /- We don't want to interleave let and lambda declarations in our closure. So, we expand any occurrences of newFVarId
+         at `newLocalDecls` -/
+      modify fun s => { s with newLocalDecls := s.newLocalDecls.map (replaceFVarIdAtLocalDecl newFVarId val) }
+      process
 
 @[inline] def mkBinding (isLambda : Bool) (decls : Array LocalDecl) (b : Expr) : Expr :=
-let xs := decls.map LocalDecl.toExpr;
-let b  := b.abstract xs;
+let xs := decls.map LocalDecl.toExpr
+let b  := b.abstract xs
 decls.size.foldRev
   (fun i b =>
-    let decl := decls.get! i;
+    let decl := decls[i]
     match decl with
     | LocalDecl.cdecl _ _ n ty bi  =>
-      let ty := ty.abstractRange i xs;
+      let ty := ty.abstractRange i xs
       if isLambda then
         Lean.mkLambda n bi ty b
       else
         Lean.mkForall n bi ty b
     | LocalDecl.ldecl _ _ n ty val nonDep =>
       if b.hasLooseBVar 0 then
-        let ty  := ty.abstractRange i xs;
-        let val := val.abstractRange i xs;
+        let ty  := ty.abstractRange i xs
+        let val := val.abstractRange i xs
         mkLet n ty val b nonDep
       else
         b.lowerLooseBVars 1 1)
@@ -323,19 +320,19 @@ structure MkValueTypeClosureResult :=
 (exprArgs    : Array Expr)
 
 def mkValueTypeClosureAux (type : Expr) (value : Expr) : ClosureM (Expr × Expr) := do
-resetZetaFVarIds;
+resetZetaFVarIds
 withTrackingZeta do
-  type  ← collectExpr type;
-  value ← collectExpr value;
-  process ();
+  let type  ← collectExpr type
+  let value ← collectExpr value
+  process
   pure (type, value)
 
 def mkValueTypeClosure (type : Expr) (value : Expr) (zeta : Bool) : MetaM MkValueTypeClosureResult := do
-((type, value), s) ← ((mkValueTypeClosureAux type value).run { zeta := zeta }).run {};
-let newLocalDecls := s.newLocalDecls.reverse ++ s.newLocalDeclsForMVars;
-let newLetDecls   := s.newLetDecls.reverse;
-let type  := mkForall newLocalDecls (mkForall newLetDecls type);
-let value := mkLambda newLocalDecls (mkLambda newLetDecls value);
+let ((type, value), s) ← ((mkValueTypeClosureAux type value).run { zeta := zeta }).run {}
+let newLocalDecls := s.newLocalDecls.reverse ++ s.newLocalDeclsForMVars
+let newLetDecls   := s.newLetDecls.reverse
+let type  := mkForall newLocalDecls (mkForall newLetDecls type)
+let value := mkLambda newLocalDecls (mkLambda newLetDecls value)
 pure {
   type        := type,
   value       := value,
@@ -349,8 +346,8 @@ end Closure
 variables {m : Type → Type} [MonadLiftT MetaM m]
 
 private def mkAuxDefinitionImp (name : Name) (type : Expr) (value : Expr) (zeta : Bool) : MetaM Expr := do
-result ← Closure.mkValueTypeClosure type value zeta;
-env ← getEnv;
+let result ← Closure.mkValueTypeClosure type value zeta
+let env ← getEnv
 let decl := Declaration.defnDecl {
   name     := name,
   lparams  := result.levelParams.toList,
@@ -358,9 +355,9 @@ let decl := Declaration.defnDecl {
   value    := result.value,
   hints    := ReducibilityHints.regular (getMaxHeight env result.value + 1),
   isUnsafe := env.hasUnsafe result.type || env.hasUnsafe result.value
-};
-trace! `Meta.debug (name ++ " : " ++ result.type ++ " := " ++ result.value);
-addAndCompile decl;
+}
+trace[Meta.debug]! "{name} : {result.type} := {result.value}"
+addAndCompile decl
 pure $ mkAppN (mkConst name result.levelArgs.toList) result.exprArgs
 
 /--
@@ -370,14 +367,13 @@ pure $ mkAppN (mkConst name result.levelArgs.toList) result.exprArgs
   returned where `u_i`s are universe parameters and metavariables `type` and `value` depend on,
   and `t_j`s are free and meta variables `type` and `value` depend on. -/
 def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zeta := false) : m Expr := liftMetaM do
-trace! `Meta.debug (name ++ " : " ++ type ++ " := " ++ value);
+trace[Meta.debug]! "{name} : {type} := {value}"
 mkAuxDefinitionImp name type value zeta
 
 /-- Similar to `mkAuxDefinition`, but infers the type of `value`. -/
 def mkAuxDefinitionFor (name : Name) (value : Expr) : m Expr := liftMetaM do
-type ← inferType value;
-let type := type.headBeta;
+let type ← inferType value
+let type := type.headBeta
 mkAuxDefinition name type value
 
-end Meta
-end Lean
+end Lean.Meta