Pantograph.lean

@@ -1,7 +1,8 @@
+import Pantograph.Delate
+import Pantograph.Elab
 import Pantograph.Environment
 import Pantograph.Frontend
 import Pantograph.Goal
 import Pantograph.Library
 import Pantograph.Protocol
-import Pantograph.Delate
 import Pantograph.Version

Pantograph/Delate.lean

@@ -2,7 +2,7 @@
 This file handles "Delation": The conversion of Kernel view into Search view.
 -/
 import Lean
-import Pantograph.Expr
+import Std.Data.HashMap
 import Pantograph.Goal
 import Pantograph.Protocol
 
@@ -11,6 +11,163 @@ open Lean
 -- Symbol processing functions --
 
 namespace Pantograph
+
+structure ProjectionApplication where
+  projector: Name
+  numParams: Nat
+  inner: Expr
+
+@[export pantograph_expr_proj_to_app]
+def exprProjToApp (env: Environment) (e: Expr): ProjectionApplication :=
+  let (typeName, idx, inner) := match e with
+    | .proj typeName idx inner => (typeName, idx, inner)
+    | _ => panic! "Argument must be proj"
+  let ctor := getStructureCtor env typeName
+  let fieldName := getStructureFields env typeName |>.get! idx
+  let projector := getProjFnForField? env typeName fieldName |>.get!
+  {
+    projector,
+    numParams := ctor.numParams,
+    inner,
+  }
+
+def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
+
+/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
+@[export pantograph_unfold_aux_lemmas]
+def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
+  Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
+
+/--
+Force the instantiation of delayed metavariables even if they cannot be fully
+instantiated. This is used during resumption to provide diagnostic data about
+the current goal.
+
+Since Lean 4 does not have an `Expr` constructor corresponding to delayed
+metavariables, any delayed metavariables must be recursively handled by this
+function to ensure that nested delayed metavariables can be properly processed.
+The caveat is this recursive call will lead to infinite recursion if a loop
+between metavariable assignment exists.
+
+This function ensures any metavariable in the result is either
+1. Delayed assigned with its pending mvar not assigned in any form
+2. Not assigned (delay or not)
+ -/
+partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do
+  --let padding := String.join $ List.replicate level "│ "
+  --IO.println s!"{padding}Starting {toString eOrig}"
+  let mut result ← Meta.transform (← instantiateMVars eOrig)
+    (pre := fun e => e.withApp fun f args => do
+      let .mvar mvarId := f | return .continue
+      --IO.println s!"{padding}├V {e}"
+      let mvarDecl ← mvarId.getDecl
+
+      -- This is critical to maintaining the interdependency of metavariables.
+      -- Without setting `.syntheticOpaque`, Lean's metavariable elimination
+      -- system will not make the necessary delayed assigned mvars in case of
+      -- nested mvars.
+      mvarId.setKind .syntheticOpaque
+
+      mvarId.withContext do
+        let lctx ← MonadLCtx.getLCtx
+        if mvarDecl.lctx.any (λ decl => !lctx.contains decl.fvarId) then
+          let violations := mvarDecl.lctx.decls.foldl (λ acc decl? => match decl? with
+            | .some decl => if lctx.contains decl.fvarId then acc else acc ++ [decl.fvarId.name]
+            | .none => acc) []
+          panic! s!"In the context of {mvarId.name}, there are local context variable violations: {violations}"
+
+        if let .some assign ← getExprMVarAssignment? mvarId then
+          --IO.println s!"{padding}├A ?{mvarId.name}"
+          assert! !(← mvarId.isDelayedAssigned)
+          return .visit (mkAppN assign args)
+        else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
+          --let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList
+          --IO.println s!"{padding}├MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"
+
+          if args.size < fvars.size then
+            throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}"
+          --if !args.isEmpty then
+            --IO.println s!"{padding}├── Arguments Begin"
+          let args ← args.mapM self
+          --if !args.isEmpty then
+            --IO.println s!"{padding}├── Arguments End"
+          if !(← mvarIdPending.isAssignedOrDelayedAssigned) then
+            --IO.println s!"{padding}├T1"
+            let result := mkAppN f args
+            return .done result
+
+          let pending ← mvarIdPending.withContext do
+            let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1)
+            --IO.println s!"{padding}├Pre: {inner}"
+            pure <| (← inner.abstractM fvars).instantiateRev args
+
+          -- Tail arguments
+          let result := mkAppRange pending fvars.size args.size args
+          --IO.println s!"{padding}├MD {result}"
+          return .done result
+        else
+          assert! !(← mvarId.isAssigned)
+          assert! !(← mvarId.isDelayedAssigned)
+          --if !args.isEmpty then
+          --  IO.println s!"{padding}├── Arguments Begin"
+          let args ← args.mapM self
+          --if !args.isEmpty then
+          --  IO.println s!"{padding}├── Arguments End"
+
+          --IO.println s!"{padding}├M ?{mvarId.name}"
+          return .done (mkAppN f args))
+  --IO.println s!"{padding}└Result {result}"
+  return result
+  where
+  self e := instantiateDelayedMVars e --(level := level + 1)
+
+/--
+Convert an expression to an equiavlent form with
+1. No nested delayed assigned mvars
+2. No aux lemmas
+3. No assigned mvars
+ -/
+@[export pantograph_instantiate_all_m]
+def instantiateAll (e: Expr): MetaM Expr := do
+  let e ← instantiateDelayedMVars e
+  let e ← unfoldAuxLemmas e
+  return e
+
+structure DelayedMVarInvocation where
+  mvarIdPending: MVarId
+  args: Array (FVarId × (Option Expr))
+  -- Extra arguments applied to the result of this substitution
+  tail: Array Expr
+
+-- The pending mvar of any delayed assigned mvar must not be assigned in any way.
+@[export pantograph_to_delayed_mvar_invocation_m]
+def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do
+  let .mvar mvarId := e.getAppFn | return .none
+  let .some decl ← getDelayedMVarAssignment? mvarId | return .none
+  let mvarIdPending := decl.mvarIdPending
+  let mvarDecl ← mvarIdPending.getDecl
+  -- Print the function application e. See Lean's `withOverApp`
+  let args := e.getAppArgs
+
+  assert! args.size ≥ decl.fvars.size
+  assert! !(← mvarIdPending.isAssigned)
+  assert! !(← mvarIdPending.isDelayedAssigned)
+  let fvarArgMap: Std.HashMap FVarId Expr := Std.HashMap.ofList $ (decl.fvars.map (·.fvarId!) |>.zip args).toList
+  let subst ← mvarDecl.lctx.foldlM (init := []) λ acc localDecl => do
+    let fvarId := localDecl.fvarId
+    let a := fvarArgMap[fvarId]?
+    return acc ++ [(fvarId, a)]
+
+  assert! decl.fvars.all (λ fvar => mvarDecl.lctx.findFVar? fvar |>.isSome)
+
+  return .some {
+    mvarIdPending,
+    args := subst.toArray,
+    tail := args.toList.drop decl.fvars.size |>.toArray,
+  }
+
+-- Condensed representation
+
 namespace Condensed
 
 -- Mirrors Lean's LocalDecl
@@ -32,12 +189,6 @@ structure Goal where
 @[export pantograph_goal_is_lhs]
 def isLHS (g: Goal) : Bool := isLHSGoal? g.target |>.isSome
 
--- Functions for creating contexts and states
-@[export pantograph_elab_context]
-def elabContext: Elab.Term.Context := {
-    errToSorry := false
-  }
-
 end Condensed
 
 -- Get the list of visible (by default) free variables from a goal
@@ -97,38 +248,6 @@ protected def GoalState.toCondensed (state: GoalState):
       | .none => throwError s!"Metavariable does not exist in context {goal.name}"
   metaM.run' (s := state.savedState.term.meta.meta)
 
---- Input Functions ---
-
-/-- Read syntax object from string -/
-def parseTerm (env: Environment) (s: String): Except String Syntax :=
-  Parser.runParserCategory
-    (env := env)
-    (catName := `term)
-    (input := s)
-    (fileName := "<stdin>")
-
-def parseTermM [Monad m] [MonadEnv m] (s: String): m (Except String Syntax) := do
-  return Parser.runParserCategory
-    (env := ← MonadEnv.getEnv)
-    (catName := `term)
-    (input := s)
-    (fileName := "<stdin>")
-
-/-- Parse a syntax object. May generate additional metavariables! -/
-def elabType (syn: Syntax): Elab.TermElabM (Except String Expr) := do
-  try
-    let expr ← Elab.Term.elabType syn
-    return .ok expr
-  catch ex => return .error (← ex.toMessageData.toString)
-def elabTerm (syn: Syntax) (expectedType? : Option Expr := .none): Elab.TermElabM (Except String Expr) := do
-  try
-    let expr ← Elab.Term.elabTerm (stx := syn) expectedType?
-    return .ok expr
-  catch ex => return .error (← ex.toMessageData.toString)
-
-
---- Output Functions ---
-
 def typeExprToBound (expr: Expr): MetaM Protocol.BoundExpression := do
   Meta.forallTelescope expr fun arr body => do
     let binders ← arr.mapM fun fvar => do

Pantograph/Elab.lean

@@ -0,0 +1,40 @@
+import Lean
+open Lean
+
+namespace Pantograph
+
+-- Functions for creating contexts and states
+@[export pantograph_default_elab_context]
+def defaultElabContext: Elab.Term.Context := {
+    errToSorry := false
+  }
+
+/-- Read syntax object from string -/
+def parseTerm (env: Environment) (s: String): Except String Syntax :=
+  Parser.runParserCategory
+    (env := env)
+    (catName := `term)
+    (input := s)
+    (fileName := "<stdin>")
+
+def parseTermM [Monad m] [MonadEnv m] (s: String): m (Except String Syntax) := do
+  return Parser.runParserCategory
+    (env := ← MonadEnv.getEnv)
+    (catName := `term)
+    (input := s)
+    (fileName := "<stdin>")
+
+/-- Parse a syntax object. May generate additional metavariables! -/
+def elabType (syn: Syntax): Elab.TermElabM (Except String Expr) := do
+  try
+    let expr ← Elab.Term.elabType syn
+    return .ok expr
+  catch ex => return .error (← ex.toMessageData.toString)
+def elabTerm (syn: Syntax) (expectedType? : Option Expr := .none): Elab.TermElabM (Except String Expr) := do
+  try
+    let expr ← Elab.Term.elabTerm (stx := syn) expectedType?
+    return .ok expr
+  catch ex => return .error (← ex.toMessageData.toString)
+
+
+end Pantograph

Pantograph/Environment.lean

@@ -1,5 +1,6 @@
-import Pantograph.Protocol
 import Pantograph.Delate
+import Pantograph.Elab
+import Pantograph.Protocol
 import Lean
 
 open Lean

Pantograph/Expr.lean

@@ -1,162 +0,0 @@
-import Lean
-import Std.Data.HashMap
-
-open Lean
-
-namespace Pantograph
-
-structure ProjectionApplication where
-  projector: Name
-  numParams: Nat
-  inner: Expr
-
-@[export pantograph_expr_proj_to_app]
-def exprProjToApp (env: Environment) (e: Expr): ProjectionApplication :=
-  let (typeName, idx, inner) := match e with
-    | .proj typeName idx inner => (typeName, idx, inner)
-    | _ => panic! "Argument must be proj"
-  let ctor := getStructureCtor env typeName
-  let fieldName := getStructureFields env typeName |>.get! idx
-  let projector := getProjFnForField? env typeName fieldName |>.get!
-  {
-    projector,
-    numParams := ctor.numParams,
-    inner,
-  }
-
-def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
-
-/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
-@[export pantograph_unfold_aux_lemmas]
-def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
-  Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
-
-/--
-Force the instantiation of delayed metavariables even if they cannot be fully
-instantiated. This is used during resumption to provide diagnostic data about
-the current goal.
-
-Since Lean 4 does not have an `Expr` constructor corresponding to delayed
-metavariables, any delayed metavariables must be recursively handled by this
-function to ensure that nested delayed metavariables can be properly processed.
-The caveat is this recursive call will lead to infinite recursion if a loop
-between metavariable assignment exists.
-
-This function ensures any metavariable in the result is either
-1. Delayed assigned with its pending mvar not assigned in any form
-2. Not assigned (delay or not)
- -/
-partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do
-  --let padding := String.join $ List.replicate level "│ "
-  --IO.println s!"{padding}Starting {toString eOrig}"
-  let mut result ← Meta.transform (← instantiateMVars eOrig)
-    (pre := fun e => e.withApp fun f args => do
-      let .mvar mvarId := f | return .continue
-      --IO.println s!"{padding}├V {e}"
-      let mvarDecl ← mvarId.getDecl
-
-      -- This is critical to maintaining the interdependency of metavariables.
-      -- Without setting `.syntheticOpaque`, Lean's metavariable elimination
-      -- system will not make the necessary delayed assigned mvars in case of
-      -- nested mvars.
-      mvarId.setKind .syntheticOpaque
-
-      mvarId.withContext do
-        let lctx ← MonadLCtx.getLCtx
-        if mvarDecl.lctx.any (λ decl => !lctx.contains decl.fvarId) then
-          let violations := mvarDecl.lctx.decls.foldl (λ acc decl? => match decl? with
-            | .some decl => if lctx.contains decl.fvarId then acc else acc ++ [decl.fvarId.name]
-            | .none => acc) []
-          panic! s!"In the context of {mvarId.name}, there are local context variable violations: {violations}"
-
-        if let .some assign ← getExprMVarAssignment? mvarId then
-          --IO.println s!"{padding}├A ?{mvarId.name}"
-          assert! !(← mvarId.isDelayedAssigned)
-          return .visit (mkAppN assign args)
-        else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
-          --let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList
-          --IO.println s!"{padding}├MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"
-
-          if args.size < fvars.size then
-            throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}"
-          --if !args.isEmpty then
-            --IO.println s!"{padding}├── Arguments Begin"
-          let args ← args.mapM self
-          --if !args.isEmpty then
-            --IO.println s!"{padding}├── Arguments End"
-          if !(← mvarIdPending.isAssignedOrDelayedAssigned) then
-            --IO.println s!"{padding}├T1"
-            let result := mkAppN f args
-            return .done result
-
-          let pending ← mvarIdPending.withContext do
-            let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1)
-            --IO.println s!"{padding}├Pre: {inner}"
-            pure <| (← inner.abstractM fvars).instantiateRev args
-
-          -- Tail arguments
-          let result := mkAppRange pending fvars.size args.size args
-          --IO.println s!"{padding}├MD {result}"
-          return .done result
-        else
-          assert! !(← mvarId.isAssigned)
-          assert! !(← mvarId.isDelayedAssigned)
-          --if !args.isEmpty then
-          --  IO.println s!"{padding}├── Arguments Begin"
-          let args ← args.mapM self
-          --if !args.isEmpty then
-          --  IO.println s!"{padding}├── Arguments End"
-
-          --IO.println s!"{padding}├M ?{mvarId.name}"
-          return .done (mkAppN f args))
-  --IO.println s!"{padding}└Result {result}"
-  return result
-  where
-  self e := instantiateDelayedMVars e --(level := level + 1)
-
-/--
-Convert an expression to an equiavlent form with
-1. No nested delayed assigned mvars
-2. No aux lemmas
-3. No assigned mvars
- -/
-@[export pantograph_instantiate_all_m]
-def instantiateAll (e: Expr): MetaM Expr := do
-  let e ← instantiateDelayedMVars e
-  let e ← unfoldAuxLemmas e
-  return e
-
-structure DelayedMVarInvocation where
-  mvarIdPending: MVarId
-  args: Array (FVarId × (Option Expr))
-  -- Extra arguments applied to the result of this substitution
-  tail: Array Expr
-
--- The pending mvar of any delayed assigned mvar must not be assigned in any way.
-@[export pantograph_to_delayed_mvar_invocation_m]
-def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do
-  let .mvar mvarId := e.getAppFn | return .none
-  let .some decl ← getDelayedMVarAssignment? mvarId | return .none
-  let mvarIdPending := decl.mvarIdPending
-  let mvarDecl ← mvarIdPending.getDecl
-  -- Print the function application e. See Lean's `withOverApp`
-  let args := e.getAppArgs
-
-  assert! args.size ≥ decl.fvars.size
-  assert! !(← mvarIdPending.isAssigned)
-  assert! !(← mvarIdPending.isDelayedAssigned)
-  let fvarArgMap: Std.HashMap FVarId Expr := Std.HashMap.ofList $ (decl.fvars.map (·.fvarId!) |>.zip args).toList
-  let subst ← mvarDecl.lctx.foldlM (init := []) λ acc localDecl => do
-    let fvarId := localDecl.fvarId
-    let a := fvarArgMap[fvarId]?
-    return acc ++ [(fvarId, a)]
-
-  assert! decl.fvars.all (λ fvar => mvarDecl.lctx.findFVar? fvar |>.isSome)
-
-  return .some {
-    mvarIdPending,
-    args := subst.toArray,
-    tail := args.toList.drop decl.fvars.size |>.toArray,
-  }
-
-end Pantograph

Pantograph/Library.lean

@@ -41,7 +41,7 @@ namespace Pantograph
 def runMetaM { α } (metaM: MetaM α): CoreM α :=
   metaM.run'
 def runTermElabM { α } (termElabM: Elab.TermElabM α): CoreM α :=
-  termElabM.run' (ctx := Condensed.elabContext) |>.run'
+  termElabM.run' (ctx := defaultElabContext) |>.run'
 
 def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
 

Repl.lean

@@ -22,7 +22,7 @@ abbrev CR α := Except Protocol.InteractionError α
 def runMetaInMainM { α } (metaM: Lean.MetaM α): MainM α :=
   metaM.run'
 def runTermElabInMainM { α } (termElabM: Lean.Elab.TermElabM α) : MainM α :=
-  termElabM.run' (ctx := Condensed.elabContext) |>.run'
+  termElabM.run' (ctx := defaultElabContext) |>.run'
 
 def execute (command: Protocol.Command): MainM Lean.Json := do
   let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=

Test/Common.lean

@@ -89,9 +89,9 @@ def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq) (options: Array
 def runMetaMSeq (env: Environment) (metaM: MetaM LSpec.TestSeq): IO LSpec.TestSeq :=
   runCoreMSeq env metaM.run'
 def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α :=
-  termElabM.run' (ctx := Condensed.elabContext)
+  termElabM.run' (ctx := defaultElabContext)
 def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq): IO LSpec.TestSeq :=
-  runMetaMSeq env $ termElabM.run' (ctx := Condensed.elabContext)
+  runMetaMSeq env $ termElabM.run' (ctx := defaultElabContext)
 
 def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e
 

Test/Delate.lean

@@ -64,7 +64,7 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
         | .ok expr => pure expr
         | .error e => return elabFailure e
       return LSpec.check source ((← serializeExpressionSexp expr) = target)
-    let metaM := (Elab.Term.withLevelNames levels termElabM).run' (ctx := Condensed.elabContext)
+    let metaM := (Elab.Term.withLevelNames levels termElabM).run' (ctx := defaultElabContext)
     return LSpec.TestSeq.append suites (← runMetaMSeq env metaM))
     LSpec.TestSeq.done
 
@@ -85,7 +85,7 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
     let testCaseName := target.take 10
     let test := LSpec.check   testCaseName ((← serializeExpressionSexp expr) = target)
     return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
-  runMetaMSeq env $ termElabM.run' (ctx := Condensed.elabContext)
+  runMetaMSeq env $ termElabM.run' (ctx := defaultElabContext)
 
 -- Instance parsing
 def test_instance (env: Environment): IO LSpec.TestSeq :=

Test/Metavar.lean

@@ -66,7 +66,7 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
   let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
 
   let coreContext: Lean.Core.Context ← createCoreContext #[]
-  let metaM := termElabM.run' (ctx := Condensed.elabContext)
+  let metaM := termElabM.run' (ctx := defaultElabContext)
   let coreM := metaM.run'
   match ← (coreM.run' coreContext { env := env }).toBaseIO with
   | .error exception =>

Test/Proofs.lean

@@ -74,7 +74,7 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
   let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
 
   let coreContext: Lean.Core.Context ← createCoreContext #[]
-  let metaM := termElabM.run' (ctx := Condensed.elabContext)
+  let metaM := termElabM.run' (ctx := defaultElabContext)
   let coreM := metaM.run'
   match ← (coreM.run' coreContext { env := env }).toBaseIO with
   | .error exception =>