Pantograph/Delate.lean

@@ -37,7 +37,7 @@ def analyzeProjection (env: Environment) (e: Expr): Projection :=
 def anonymousLevel : Level := .mvar ⟨.anonymous⟩
 
 @[export pantograph_expr_proj_to_app]
-def exprProjToApp (env : Environment) (e : Expr) : Expr :=
+def exprProjToApp (env: Environment) (e: Expr): Expr :=
   let anon : Expr := .mvar ⟨.anonymous⟩
   match analyzeProjection env e with
   | .field projector numParams =>
@@ -66,18 +66,9 @@ def exprProjToApp (env : Environment) (e : Expr) : Expr :=
 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_m]
+@[export pantograph_unfold_aux_lemmas]
-def unfoldAuxLemmas : Expr → CoreM Expr :=
+def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
-  (Meta.deltaExpand · Lean.Name.isAuxLemma)
+  Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
-/-- Unfold all matcher applications -/
-@[export pantograph_unfold_matchers_m]
-def unfoldMatchers (expr : Expr) : CoreM Expr :=
-  Core.transform expr λ e => do
-    let .some mapp ← Meta.matchMatcherApp? e | return .continue e
-    let .some matcherInfo := (← getEnv).find? mapp.matcherName | panic! "Matcher must exist"
-    let f ← Meta.instantiateValueLevelParams matcherInfo mapp.matcherLevels.toList
-    let mdata := KVMap.empty.insert `matcher (DataValue.ofName mapp.matcherName)
-    return .visit $ .mdata mdata (f.betaRev e.getAppRevArgs (useZeta := true))
 
 /--
 Force the instantiation of delayed metavariables even if they cannot be fully
@@ -94,92 +85,91 @@ 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 (expr : Expr) : MetaM Expr :=
+partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do
-  withTraceNode `Pantograph.Delate (λ _ex => return m!":= {← Meta.ppExpr expr}") do
+  --let padding := String.join $ List.replicate level "│ "
-  let mut result ← Meta.transform (← instantiateMVars expr)
+  --IO.println s!"{padding}Starting {toString eOrig}"
-    λ e => e.withApp fun f args => do
+  let mut result ← Meta.transform (← instantiateMVars eOrig)
-    let .mvar mvarId := f | return .continue
+    (pre := fun e => e.withApp fun f args => do
-    trace[Pantograph.Delate] "V {e}"
+      let .mvar mvarId := f | return .continue
-    let mvarDecl ← mvarId.getDecl
+      --IO.println s!"{padding}├V {e}"
+      let mvarDecl ← mvarId.getDecl
 
-    -- This is critical to maintaining the interdependency of metavariables.
+      -- This is critical to maintaining the interdependency of metavariables.
-    -- Without setting `.syntheticOpaque`, Lean's metavariable elimination
+      -- Without setting `.syntheticOpaque`, Lean's metavariable elimination
-    -- system will not make the necessary delayed assigned mvars in case of
+      -- system will not make the necessary delayed assigned mvars in case of
-    -- nested mvars.
+      -- nested mvars.
-    mvarId.setKind .syntheticOpaque
+      mvarId.setKind .syntheticOpaque
 
-    mvarId.withContext do
+      mvarId.withContext do
-      let lctx ← MonadLCtx.getLCtx
+        let lctx ← MonadLCtx.getLCtx
-      if mvarDecl.lctx.any (λ decl => !lctx.contains decl.fvarId) then
+        if mvarDecl.lctx.any (λ decl => !lctx.contains decl.fvarId) then
-        let violations := mvarDecl.lctx.decls.foldl (λ acc decl? => match decl? with
+          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]
+            | .some decl => if lctx.contains decl.fvarId then acc else acc ++ [decl.fvarId.name]
-          | .none => acc) []
+            | .none => acc) []
-        panic! s!"In the context of {mvarId.name}, there are local context variable violations: {violations}"
+          panic! s!"In the context of {mvarId.name}, there are local context variable violations: {violations}"
 
-      if let .some assign ← getExprMVarAssignment? mvarId then
+        if let .some assign ← getExprMVarAssignment? mvarId then
-        trace[Pantograph.Delate] "A ?{mvarId.name}"
+          --IO.println s!"{padding}├A ?{mvarId.name}"
-        assert! !(← mvarId.isDelayedAssigned)
+          assert! !(← mvarId.isDelayedAssigned)
-        return .visit (mkAppN assign args)
+          return .visit (mkAppN assign args)
-      else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
+        else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
-        if ← isTracingEnabledFor `Pantograph.Delate then
+          --let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList
-          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}]"
-          trace[Pantograph.Delate]"MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"
 
-        if args.size < fvars.size then
+          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 expr}"
+            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
+          --if !args.isEmpty then
-          trace[Pantograph.Delate] "─ Arguments Begin"
+            --IO.println s!"{padding}├── Arguments Begin"
-        let args ← args.mapM self
+          let args ← args.mapM self
-        if !args.isEmpty then
+          --if !args.isEmpty then
-          trace[Pantograph.Delate] "─ Arguments End"
+            --IO.println s!"{padding}├── Arguments End"
-        if !(← mvarIdPending.isAssignedOrDelayedAssigned) then
+          if !(← mvarIdPending.isAssignedOrDelayedAssigned) then
-          trace[Pantograph.Delate] "T1"
+            --IO.println s!"{padding}├T1"
-          let result := mkAppN f args
+            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"
 
-        let pending ← mvarIdPending.withContext do
+          --IO.println s!"{padding}├M ?{mvarId.name}"
-          let inner ← instantiateDelayedMVars (.mvar mvarIdPending)
+          return .done (mkAppN f args))
-          trace[Pantograph.Delate] "Pre: {inner}"
+  --IO.println s!"{padding}└Result {result}"
-          pure <| (← inner.abstractM fvars).instantiateRev args
-
-        -- Tail arguments
-        let result := mkAppRange pending fvars.size args.size args
-        trace[Pantograph.Delate] "MD {result}"
-        return .done result
-      else
-        assert! !(← mvarId.isAssigned)
-        assert! !(← mvarId.isDelayedAssigned)
-        if !args.isEmpty then
-          trace[Pantograph.Delate] "─ Arguments Begin"
-        let args ← args.mapM self
-        if !args.isEmpty then
-          trace[Pantograph.Delate] "─ Arguments End"
-
-        trace[Pantograph.Delate] "M ?{mvarId.name}"
-        return .done (mkAppN f args)
-  trace[Pantoraph.Delate] "Result {result}"
   return result
   where
-  self e := instantiateDelayedMVars e
+  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 or matchers
+2. No aux lemmas
 3. No assigned mvars
  -/
 @[export pantograph_instantiate_all_m]
-def instantiateAll (e : Expr) : MetaM Expr := do
+def instantiateAll (e: Expr): MetaM Expr := do
   let e ← instantiateDelayedMVars e
   let e ← unfoldAuxLemmas e
-  let e ← unfoldMatchers e
   return e
 
 structure DelayedMVarInvocation where
-  mvarIdPending : MVarId
+  mvarIdPending: MVarId
-  args : Array (FVarId × (Option Expr))
+  args: Array (FVarId × (Option Expr))
   -- Extra arguments applied to the result of this substitution
-  tail : Array Expr
+  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]
@@ -604,7 +594,4 @@ protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState :
       | other => s!"[{other}]"
     parentHasMVar (mvarId: MVarId): Bool := parent?.map (λ state => state.mctx.decls.contains mvarId) |>.getD true
 
-initialize
-  registerTraceClass `Pantograph.Delate
-
 end Pantograph

Pantograph/Frontend/MetaTranslate.lean

@@ -62,7 +62,7 @@ private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do
   let sourceMCtx ← getSourceMCtx
   -- We want to create as few mvars as possible
   let (srcExpr, _) := instantiateMVarsCore (mctx := sourceMCtx) srcExpr
-  trace[Pantograph.Frontend.MetaTranslate] "Transform src: {srcExpr}"
+  --IO.println s!"Transform src: {srcExpr}"
   let result ← Core.transform srcExpr λ e => do
     let state ← get
     match e with
@@ -100,10 +100,10 @@ partial def translateLocalDecl (srcLocalDecl: LocalDecl) : MetaTranslateM LocalD
   addTranslatedFVar srcLocalDecl.fvarId fvarId
   match srcLocalDecl with
   | .cdecl index _ userName type bi kind => do
-    trace[Pantograph.Frontend.MetaTranslate] "[CD] {userName} {toString type}"
+    --IO.println s!"[CD] {userName} {toString type}"
     return .cdecl index fvarId userName (← translateExpr type) bi kind
   | .ldecl index _ userName type value nonDep kind => do
-    trace[Pantograph.Frontend.MetaTranslate] "[LD] {toString type} := {toString value}"
+    --IO.println s!"[LD] {toString type} := {toString value}"
     return .ldecl index fvarId userName (← translateExpr type) (← translateExpr value) nonDep kind
 
 partial def translateLCtx : MetaTranslateM LocalContext := do
@@ -162,7 +162,4 @@ end MetaTranslate
 
 export MetaTranslate (MetaTranslateM)
 
-initialize
-  registerTraceClass `Pantograph.Frontend.MetaTranslate
-
 end Pantograph.Frontend

Pantograph/Protocol.lean

@@ -346,9 +346,10 @@ structure FrontendProcess where
   -- One of these two must be supplied: Either supply the file name or the content.
   fileName?: Option String := .none
   file?: Option String := .none
-  -- Whether to read the header
+  -- If set to true, read the header (otherwise discards the header)
   readHeader : Bool := false
-  -- Alter the REPL environment after the compilation units.
+  -- If set to true, Pantograph's environment will be altered to whatever is
+  -- after the compilation units.
   inheritEnv : Bool := false
   -- collect tactic invocations
   invocations: Bool := false

Test/Common.lean

@@ -108,7 +108,7 @@ def strToTermSyntax (s: String): CoreM Syntax := do
     (input := s)
     (fileName := ← getFileName) | panic! s!"Failed to parse {s}"
   return stx
-def parseSentence (s : String) (expectedType? : Option Expr := .none) : Elab.TermElabM Expr := do
+def parseSentence (s: String): Elab.TermElabM Expr := do
   let stx ← match Parser.runParserCategory
     (env := ← MonadEnv.getEnv)
     (catName := `term)
@@ -116,7 +116,7 @@ def parseSentence (s : String) (expectedType? : Option Expr := .none) : Elab.Ter
     (fileName := ← getFileName) with
     | .ok syn => pure syn
     | .error error => throwError "Failed to parse: {error}"
-  Elab.Term.elabTerm (stx := stx) expectedType?
+  Elab.Term.elabTerm (stx := stx) .none
 
 def runTacticOnMVar (tacticM: Elab.Tactic.TacticM Unit) (goal: MVarId): Elab.TermElabM (List MVarId) := do
     let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }

Test/Delate.lean

@@ -3,10 +3,11 @@ import Pantograph.Delate
 import Test.Common
 import Lean
 
-open Lean Pantograph
+open Lean
-
 namespace Pantograph.Test.Delate
 
+open Pantograph
+
 deriving instance Repr, DecidableEq for Protocol.BoundExpression
 
 def test_serializeName: LSpec.TestSeq :=
@@ -112,13 +113,6 @@ def test_projection_exists (env: Environment) : IO LSpec.TestSeq:= runTest do
   checkEq "numParams" numParams 2
   checkEq "numFields" numFields 2
 
-def test_matcher : TestT Elab.TermElabM Unit := do
-  let t ← parseSentence "Nat → Nat"
-  let e ← parseSentence "fun (n : Nat) => match n with | 0 => 0 | k => k" (.some t)
-  let .some _ ← Meta.matchMatcherApp? e.bindingBody! | fail "Must be a matcher app"
-  let e' ← instantiateAll e
-  checkTrue "ok" <| ← Meta.isTypeCorrect e'
-
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [
     ("serializeName", do pure test_serializeName),
@@ -129,7 +123,6 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
     ("Instance", test_instance env),
     ("Projection Prod", test_projection_prod env),
     ("Projection Exists", test_projection_exists env),
-    ("Matcher", runTestTermElabM env test_matcher),
   ]
 
 end Pantograph.Test.Delate

doc/repl.md

@@ -46,15 +46,14 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
   Save/Load a goal state to/from a file. The environment is not carried with the
   state. The user is responsible to ensure the sender/receiver instances share
   the same environment.
-* `frontend.process { ["fileName": <fileName>,] ["file": <str>], readHeader: <bool>, inheritEnv: <bool>, invocations:
+* `frontend.process { ["fileName": <fileName>,] ["file": <str>], invocations:
   <bool>, sorrys: <bool>, typeErrorsAsGoals: <bool>, newConstants: <bool> }`:
   Executes the Lean frontend on a file, collecting the tactic invocations
   (`"invocations": true`), the sorrys and type errors into goal states
   (`"sorrys": true`), and new constants (`"newConstants": true`). In the case of
   `sorrys`, this command additionally outputs the position of each captured
-  `sorry`. Conditionally inherit the environment from executing the file.
+  `sorry`. Warning: Behaviour is unstable in case of multiple `sorry`s. Use the
-  Warning: Behaviour is unstable in case of multiple `sorry`s. Use the draft
+  draft tactic if possible.
-  tactic if possible.
 
 ## Errors