From 9894ad7c7e2a8e7fde305e1a542f708fd1481c5e Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 26 Nov 2024 12:16:14 -0800
Subject: [PATCH 01/15] refactor: InfoTree functions

---
 Pantograph/Frontend.lean          |  2 +-
 Pantograph/Frontend/Elab.lean     | 82 ++-----------------------------
 Pantograph/Frontend/InfoTree.lean | 81 ++++++++++++++++++++++++++++++
 3 files changed, 85 insertions(+), 80 deletions(-)
 create mode 100644 Pantograph/Frontend/InfoTree.lean

diff --git a/Pantograph/Frontend.lean b/Pantograph/Frontend.lean
index fd91823..9a41567 100644
--- a/Pantograph/Frontend.lean
+++ b/Pantograph/Frontend.lean
@@ -1,4 +1,4 @@
-/- Adapted from lean-training-data by semorrison -/
 import Pantograph.Frontend.Basic
 import Pantograph.Frontend.Elab
+import Pantograph.Frontend.InfoTree
 import Pantograph.Frontend.MetaTranslate
diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index ceecfae..b3173a7 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -7,77 +7,10 @@ import Pantograph.Frontend.Basic
 import Pantograph.Frontend.MetaTranslate
 import Pantograph.Goal
 import Pantograph.Protocol
+import Pantograph.Frontend.InfoTree
 
 open Lean
 
-namespace Lean.Elab.Info
-/-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/
-protected def stx? : Info → Option Syntax
-  | .ofTacticInfo         info => info.stx
-  | .ofTermInfo           info => info.stx
-  | .ofCommandInfo        info => info.stx
-  | .ofMacroExpansionInfo info => info.stx
-  | .ofOptionInfo         info => info.stx
-  | .ofFieldInfo          info => info.stx
-  | .ofCompletionInfo     info => info.stx
-  | .ofUserWidgetInfo     info => info.stx
-  | .ofCustomInfo         info => info.stx
-  | .ofFVarAliasInfo      _    => none
-  | .ofFieldRedeclInfo    info => info.stx
-  | .ofOmissionInfo       info => info.stx
-/-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/
-protected def isOriginal (i : Info) : Bool :=
-  match i.stx? with
-  | none => true   -- Somewhat unclear what to do with `FVarAliasInfo`, so be conservative.
-  | some stx => match stx.getHeadInfo with
-    | .original .. => true
-    | _ => false
-end Lean.Elab.Info
-
-namespace Lean.Elab.TacticInfo
-
-/-- Find the name for the outermost `Syntax` in this `TacticInfo`. -/
-def name? (t : TacticInfo) : Option Name :=
-  match t.stx with
-  | Syntax.node _ n _ => some n
-  | _ => none
-/-- Decide whether a tactic is "substantive",
-or is merely a tactic combinator (e.g. `by`, `;`, multiline tactics, parenthesized tactics). -/
-def isSubstantive (t : TacticInfo) : Bool :=
-  match t.name? with
-  | none => false
-  | some `null => false
-  | some ``cdot => false
-  | some ``cdotTk => false
-  | some ``Lean.Parser.Term.byTactic => false
-  | some ``Lean.Parser.Tactic.tacticSeq => false
-  | some ``Lean.Parser.Tactic.tacticSeq1Indented => false
-  | some ``Lean.Parser.Tactic.«tactic_<;>_» => false
-  | some ``Lean.Parser.Tactic.paren => false
-  | _ => true
-
-end Lean.Elab.TacticInfo
-
-namespace Lean.Elab.InfoTree
-
-/--
-Keep `.node` nodes and `.hole` nodes satisfying predicates.
-
-Returns a `List InfoTree`, although in most situations this will be a singleton.
--/
-partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) :
-    InfoTree → List InfoTree
-  | .context ctx tree => tree.filter p m |>.map (.context ctx)
-  | .node info children =>
-    if p info then
-      [.node info (children.toList.map (filter p m)).join.toPArray']
-    else
-      (children.toList.map (filter p m)).join
-  | .hole mvar => if m mvar then [.hole mvar] else []
-
-end Lean.Elab.InfoTree
-
-
 namespace Pantograph.Frontend
 
 -- Info tree filtering functions
@@ -131,19 +64,10 @@ protected def usedConstants (t: TacticInvocation) : NameSet :=
 
 end TacticInvocation
 
-/-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
-partial def findAllInfo (t : Elab.InfoTree) (context?: Option Elab.ContextInfo) (pred : Elab.Info → Bool) :
-    List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree) :=
-  match t with
-  | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) pred
-  | .node i children  =>
-      (if pred i then [(i, context?, children)] else []) ++ children.toList.bind (fun t => findAllInfo t context? pred)
-  | _ => []
-
 /-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics,
 each equipped with its relevant `ContextInfo`, and any children info trees. -/
 private def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation :=
-  let infos := findAllInfo t none fun i => match i with
+  let infos := t.findAllInfo none fun i => match i with
     | .ofTacticInfo _ => true
     | _ => false
   infos.filterMap fun p => match p with
@@ -178,7 +102,7 @@ structure InfoWithContext where
   context?: Option Elab.ContextInfo := .none
 
 private def collectSorrysInTree (t : Elab.InfoTree) : List InfoWithContext :=
-  let infos := findAllInfo t none fun i => match i with
+  let infos := t.findAllInfo none fun i => match i with
     | .ofTermInfo { expectedType?, expr, stx, .. } =>
       expr.isSorry ∧ expectedType?.isSome ∧ stx.isOfKind `Lean.Parser.Term.sorry
     | .ofTacticInfo { stx, goalsBefore, .. } =>
diff --git a/Pantograph/Frontend/InfoTree.lean b/Pantograph/Frontend/InfoTree.lean
new file mode 100644
index 0000000..4e60710
--- /dev/null
+++ b/Pantograph/Frontend/InfoTree.lean
@@ -0,0 +1,81 @@
+/- Adapted from lean-training-data by semorrison -/
+import Lean.Elab.InfoTree
+import Lean.Parser.Term
+
+open Lean
+
+namespace Lean.Elab.Info
+/-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/
+protected def stx? : Info → Option Syntax
+  | .ofTacticInfo         info => info.stx
+  | .ofTermInfo           info => info.stx
+  | .ofCommandInfo        info => info.stx
+  | .ofMacroExpansionInfo info => info.stx
+  | .ofOptionInfo         info => info.stx
+  | .ofFieldInfo          info => info.stx
+  | .ofCompletionInfo     info => info.stx
+  | .ofUserWidgetInfo     info => info.stx
+  | .ofCustomInfo         info => info.stx
+  | .ofFVarAliasInfo      _    => none
+  | .ofFieldRedeclInfo    info => info.stx
+  | .ofOmissionInfo       info => info.stx
+/-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/
+protected def isOriginal (i : Info) : Bool :=
+  match i.stx? with
+  | none => true   -- Somewhat unclear what to do with `FVarAliasInfo`, so be conservative.
+  | some stx => match stx.getHeadInfo with
+    | .original .. => true
+    | _ => false
+end Lean.Elab.Info
+
+namespace Lean.Elab.TacticInfo
+
+/-- Find the name for the outermost `Syntax` in this `TacticInfo`. -/
+def name? (t : TacticInfo) : Option Name :=
+  match t.stx with
+  | Syntax.node _ n _ => some n
+  | _ => none
+/-- Decide whether a tactic is "substantive",
+or is merely a tactic combinator (e.g. `by`, `;`, multiline tactics, parenthesized tactics). -/
+def isSubstantive (t : TacticInfo) : Bool :=
+  match t.name? with
+  | none => false
+  | some `null => false
+  | some ``cdot => false
+  | some ``cdotTk => false
+  | some ``Lean.Parser.Term.byTactic => false
+  | some ``Lean.Parser.Tactic.tacticSeq => false
+  | some ``Lean.Parser.Tactic.tacticSeq1Indented => false
+  | some ``Lean.Parser.Tactic.«tactic_<;>_» => false
+  | some ``Lean.Parser.Tactic.paren => false
+  | _ => true
+
+end Lean.Elab.TacticInfo
+
+namespace Lean.Elab.InfoTree
+
+/--
+Keep `.node` nodes and `.hole` nodes satisfying predicates.
+
+Returns a `List InfoTree`, although in most situations this will be a singleton.
+-/
+partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) :
+    InfoTree → List InfoTree
+  | .context ctx tree => tree.filter p m |>.map (.context ctx)
+  | .node info children =>
+    if p info then
+      [.node info (children.toList.map (filter p m)).join.toPArray']
+    else
+      (children.toList.map (filter p m)).join
+  | .hole mvar => if m mvar then [.hole mvar] else []
+
+/-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
+partial def findAllInfo (t : InfoTree) (context?: Option Elab.ContextInfo) (pred : Elab.Info → Bool) :
+    List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree) :=
+  match t with
+  | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) pred
+  | .node i children  =>
+      (if pred i then [(i, context?, children)] else []) ++ children.toList.bind (fun t => findAllInfo t context? pred)
+  | _ => []
+
+end Lean.Elab.InfoTree

From 9ede3cf7175db43e1e660f64e58eaac4251eed8b Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 8 Dec 2024 15:38:03 -0800
Subject: [PATCH 02/15] feat: InfoTree printing

---
 Pantograph/Frontend/InfoTree.lean | 73 ++++++++++++++++++++++++-------
 1 file changed, 58 insertions(+), 15 deletions(-)

diff --git a/Pantograph/Frontend/InfoTree.lean b/Pantograph/Frontend/InfoTree.lean
index 4e60710..aa99db2 100644
--- a/Pantograph/Frontend/InfoTree.lean
+++ b/Pantograph/Frontend/InfoTree.lean
@@ -1,12 +1,19 @@
-/- Adapted from lean-training-data by semorrison -/
+/- Adapted from lean-training-data -/
 import Lean.Elab.InfoTree
 import Lean.Parser.Term
+import Lean.PrettyPrinter
 
 open Lean
 
-namespace Lean.Elab.Info
+namespace Lean.Elab
+
+private def elaboratorToString : Name → String
+  | .anonymous => ""
+  | n => s!"[{n}]"
+private def indent (s : String) : String := "\n".intercalate $ s.splitOn "\n" |>.map ("\t" ++ .)
+
 /-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/
-protected def stx? : Info → Option Syntax
+protected def Info.stx? : Info → Option Syntax
   | .ofTacticInfo         info => info.stx
   | .ofTermInfo           info => info.stx
   | .ofCommandInfo        info => info.stx
@@ -20,24 +27,35 @@ protected def stx? : Info → Option Syntax
   | .ofFieldRedeclInfo    info => info.stx
   | .ofOmissionInfo       info => info.stx
 /-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/
-protected def isOriginal (i : Info) : Bool :=
+protected def Info.isOriginal (i : Info) : Bool :=
   match i.stx? with
   | none => true   -- Somewhat unclear what to do with `FVarAliasInfo`, so be conservative.
   | some stx => match stx.getHeadInfo with
     | .original .. => true
     | _ => false
-end Lean.Elab.Info
 
-namespace Lean.Elab.TacticInfo
+def ContextInfo.ppExpr (ctx : ContextInfo) (lctx : LocalContext) (e : Expr) : IO Format :=
+  ctx.runMetaM lctx (do Meta.ppExpr (← instantiateMVars e))
+
+def CommandInfo.toString (info : CommandInfo) (ctx : ContextInfo) : IO String := do
+  let stx := (← ctx.ppSyntax {} info.stx).pretty
+  return s!"{stx}\n{elaboratorToString info.elaborator}"
+
+def TermInfo.toString (info : TermInfo) (ctx : ContextInfo) : IO String := do
+  let stx := (← ctx.ppSyntax info.lctx info.stx).pretty
+  let expectedType ← info.expectedType?.mapM fun ty => do
+    pure s!": {(← ctx.ppExpr info.lctx ty).pretty}"
+  let expr := (← ctx.ppExpr info.lctx info.expr).pretty
+  return s!"{stx}\n{elaboratorToString info.elaborator}{expr}{expectedType}"
 
 /-- Find the name for the outermost `Syntax` in this `TacticInfo`. -/
-def name? (t : TacticInfo) : Option Name :=
+def TacticInfo.name? (t : TacticInfo) : Option Name :=
   match t.stx with
   | Syntax.node _ n _ => some n
   | _ => none
 /-- Decide whether a tactic is "substantive",
 or is merely a tactic combinator (e.g. `by`, `;`, multiline tactics, parenthesized tactics). -/
-def isSubstantive (t : TacticInfo) : Bool :=
+def TacticInfo.isSubstantive (t : TacticInfo) : Bool :=
   match t.name? with
   | none => false
   | some `null => false
@@ -49,17 +67,22 @@ def isSubstantive (t : TacticInfo) : Bool :=
   | some ``Lean.Parser.Tactic.«tactic_<;>_» => false
   | some ``Lean.Parser.Tactic.paren => false
   | _ => true
-
-end Lean.Elab.TacticInfo
-
-namespace Lean.Elab.InfoTree
+def TacticInfo.pp (info : TacticInfo) (ctx : ContextInfo) : IO Format :=
+  ctx.runMetaM {} try
+    Lean.PrettyPrinter.ppTactic ⟨info.stx⟩
+  catch _ =>
+    pure "<failed to pretty print>"
+def TacticInfo.toString (i : TacticInfo) (ctx : ContextInfo) : IO String := do
+  let name := i.name?
+  let stx := Format.pretty (← i.pp ctx)
+  return s!"{stx}\n{name} {stx}"
 
 /--
 Keep `.node` nodes and `.hole` nodes satisfying predicates.
 
 Returns a `List InfoTree`, although in most situations this will be a singleton.
 -/
-partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) :
+partial def InfoTree.filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) :
     InfoTree → List InfoTree
   | .context ctx tree => tree.filter p m |>.map (.context ctx)
   | .node info children =>
@@ -70,7 +93,7 @@ partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) :
   | .hole mvar => if m mvar then [.hole mvar] else []
 
 /-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
-partial def findAllInfo (t : InfoTree) (context?: Option Elab.ContextInfo) (pred : Elab.Info → Bool) :
+partial def InfoTree.findAllInfo (t : InfoTree) (context?: Option Elab.ContextInfo) (pred : Elab.Info → Bool) :
     List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree) :=
   match t with
   | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) pred
@@ -78,4 +101,24 @@ partial def findAllInfo (t : InfoTree) (context?: Option Elab.ContextInfo) (pred
       (if pred i then [(i, context?, children)] else []) ++ children.toList.bind (fun t => findAllInfo t context? pred)
   | _ => []
 
-end Lean.Elab.InfoTree
+@[export pantograph_infotree_to_string_m]
+partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo) : IO String := do
+  match t with
+  | .context ctx t => t.toString (ctx.mergeIntoOuter? ctx?)
+  | .node info children =>
+    if let some ctx := ctx? then
+      let node : Option String ← match info with
+      | .ofTermInfo    info => some <$> (do pure <| s!"[term] {(← info.toString ctx)}")
+      | .ofCommandInfo info => some <$> (do pure <| s!"[command] {(← info.toString ctx)}")
+      | .ofTacticInfo  info => some <$> (do pure <| s!"[tactic] {(← info.toString ctx)}")
+      | _                   => pure none
+      let children := "\n".intercalate (← children.toList.mapM λ t' => do pure $ indent $ ← t'.toString ctx)
+      return s!"{node}\n{children}"
+    else throw <| IO.userError "No `ContextInfo` available."
+  | .hole mvarId =>
+    if let some ctx := ctx? then
+      let payload := (← ctx.runMetaM {} (do Meta.ppGoal mvarId)).pretty
+      return s!"[hole] {payload}"
+    else throw <| IO.userError "No `ContextInfo` available."
+
+end Lean.Elab

From b950dc9b1a278aabfb7fb2a19be60d7b1e636494 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 8 Dec 2024 22:51:55 -0800
Subject: [PATCH 03/15] fix: Verbose printing of infotree

---
 Pantograph/Frontend/InfoTree.lean | 32 +++++++++++++++++++------------
 1 file changed, 20 insertions(+), 12 deletions(-)

diff --git a/Pantograph/Frontend/InfoTree.lean b/Pantograph/Frontend/InfoTree.lean
index aa99db2..3b57a54 100644
--- a/Pantograph/Frontend/InfoTree.lean
+++ b/Pantograph/Frontend/InfoTree.lean
@@ -9,7 +9,7 @@ namespace Lean.Elab
 
 private def elaboratorToString : Name → String
   | .anonymous => ""
-  | n => s!"[{n}]"
+  | n => s!"⟨{n}⟩ "
 private def indent (s : String) : String := "\n".intercalate $ s.splitOn "\n" |>.map ("\t" ++ .)
 
 /-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/
@@ -39,14 +39,14 @@ def ContextInfo.ppExpr (ctx : ContextInfo) (lctx : LocalContext) (e : Expr) : IO
 
 def CommandInfo.toString (info : CommandInfo) (ctx : ContextInfo) : IO String := do
   let stx := (← ctx.ppSyntax {} info.stx).pretty
-  return s!"{stx}\n{elaboratorToString info.elaborator}"
+  return s!"{elaboratorToString info.elaborator}\n{stx}"
 
 def TermInfo.toString (info : TermInfo) (ctx : ContextInfo) : IO String := do
   let stx := (← ctx.ppSyntax info.lctx info.stx).pretty
-  let expectedType ← info.expectedType?.mapM fun ty => do
-    pure s!": {(← ctx.ppExpr info.lctx ty).pretty}"
+  let expectedType := (← info.expectedType?.mapM fun ty => do
+    pure s!": {(← ctx.ppExpr info.lctx ty).pretty}").getD ""
   let expr := (← ctx.ppExpr info.lctx info.expr).pretty
-  return s!"{stx}\n{elaboratorToString info.elaborator}{expr}{expectedType}"
+  return s!"{elaboratorToString info.elaborator}{expr}{expectedType}\n{stx}"
 
 /-- Find the name for the outermost `Syntax` in this `TacticInfo`. -/
 def TacticInfo.name? (t : TacticInfo) : Option Name :=
@@ -75,7 +75,7 @@ def TacticInfo.pp (info : TacticInfo) (ctx : ContextInfo) : IO Format :=
 def TacticInfo.toString (i : TacticInfo) (ctx : ContextInfo) : IO String := do
   let name := i.name?
   let stx := Format.pretty (← i.pp ctx)
-  return s!"{stx}\n{name} {stx}"
+  return s!"{name}\n{stx}"
 
 /--
 Keep `.node` nodes and `.hole` nodes satisfying predicates.
@@ -102,16 +102,24 @@ partial def InfoTree.findAllInfo (t : InfoTree) (context?: Option Elab.ContextIn
   | _ => []
 
 @[export pantograph_infotree_to_string_m]
-partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo) : IO String := do
+partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo := .none) : IO String := do
   match t with
   | .context ctx t => t.toString (ctx.mergeIntoOuter? ctx?)
   | .node info children =>
     if let some ctx := ctx? then
-      let node : Option String ← match info with
-      | .ofTermInfo    info => some <$> (do pure <| s!"[term] {(← info.toString ctx)}")
-      | .ofCommandInfo info => some <$> (do pure <| s!"[command] {(← info.toString ctx)}")
-      | .ofTacticInfo  info => some <$> (do pure <| s!"[tactic] {(← info.toString ctx)}")
-      | _                   => pure none
+      let node : String ← match info with
+      | .ofTermInfo    info => pure s!"[term] {(← info.toString ctx)}"
+      | .ofCommandInfo info => pure s!"[command] {(← info.toString ctx)}"
+      | .ofTacticInfo  info => pure s!"[tactic] {(← info.toString ctx)}"
+      | .ofMacroExpansionInfo _ => pure "[macro_exp]"
+      | .ofOptionInfo _ => pure "[option]"
+      | .ofFieldInfo _ => pure "[field]"
+      | .ofCompletionInfo _ => pure "[completion]"
+      | .ofUserWidgetInfo _ => pure "[user_widget]"
+      | .ofCustomInfo _ => pure "[custom]"
+      | .ofFVarAliasInfo _ => pure "[fvar]"
+      | .ofFieldRedeclInfo _ => pure "[field_redecl]"
+      | .ofOmissionInfo _ => pure "[omission]"
       let children := "\n".intercalate (← children.toList.mapM λ t' => do pure $ indent $ ← t'.toString ctx)
       return s!"{node}\n{children}"
     else throw <| IO.userError "No `ContextInfo` available."

From ea813e5bc5d0116d09d9e8f43c3213fa33b2ae4d Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 8 Dec 2024 23:21:36 -0800
Subject: [PATCH 04/15] feat: Monadic info collection

---
 Pantograph/Frontend/Elab.lean     | 26 ++++++++++++++++----------
 Pantograph/Frontend/InfoTree.lean | 29 +++++++++++++++++++++++++----
 Repl.lean                         |  4 ++--
 Test/Frontend.lean                | 12 +++++++++++-
 4 files changed, 54 insertions(+), 17 deletions(-)

diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index b3173a7..6bc67f3 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -67,7 +67,7 @@ end TacticInvocation
 /-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics,
 each equipped with its relevant `ContextInfo`, and any children info trees. -/
 private def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation :=
-  let infos := t.findAllInfo none fun i => match i with
+  let infos := t.findAllInfo none false fun i => match i with
     | .ofTacticInfo _ => true
     | _ => false
   infos.filterMap fun p => match p with
@@ -101,21 +101,27 @@ structure InfoWithContext where
   info: Elab.Info
   context?: Option Elab.ContextInfo := .none
 
-private def collectSorrysInTree (t : Elab.InfoTree) : List InfoWithContext :=
-  let infos := t.findAllInfo none fun i => match i with
-    | .ofTermInfo { expectedType?, expr, stx, .. } =>
-      expr.isSorry ∧ expectedType?.isSome ∧ stx.isOfKind `Lean.Parser.Term.sorry
+private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext) := do
+  let infos ← t.findAllInfoM none true fun i ctx? => match i with
+    | .ofTermInfo { expectedType?, expr, stx, lctx, .. } => do
+      let .some expectedType := expectedType? | return false
+      let .some ctx := ctx? | return false
+      if expr.isSorry ∧ stx.isOfKind `Lean.Parser.Term.sorry then
+        return true
+      ctx.runMetaM lctx do
+        let type ← Meta.inferType expr
+        Bool.not <$> Meta.isDefEq type expectedType
     | .ofTacticInfo { stx, goalsBefore, .. } =>
       -- The `sorry` term is distinct from the `sorry` tactic
       let isSorry := stx.isOfKind `Lean.Parser.Tactic.tacticSorry
-      isSorry ∧ !goalsBefore.isEmpty
-    | _ => false
-  infos.map fun (info, context?, _) => { info, context? }
+      return isSorry ∧ !goalsBefore.isEmpty
+    | _ => return false
+  return infos.map fun (info, context?, _) => { info, context? }
 
 -- NOTE: Plural deliberately not spelled "sorries"
 @[export pantograph_frontend_collect_sorrys_m]
-def collectSorrys (step: CompilationStep) : List InfoWithContext :=
-  step.trees.bind collectSorrysInTree
+def collectSorrys (step: CompilationStep) : IO (List InfoWithContext) := do
+  return (← step.trees.mapM collectSorrysInTree).join
 
 
 
diff --git a/Pantograph/Frontend/InfoTree.lean b/Pantograph/Frontend/InfoTree.lean
index 3b57a54..c72dbe6 100644
--- a/Pantograph/Frontend/InfoTree.lean
+++ b/Pantograph/Frontend/InfoTree.lean
@@ -93,14 +93,35 @@ partial def InfoTree.filter (p : Info → Bool) (m : MVarId → Bool := fun _ =>
   | .hole mvar => if m mvar then [.hole mvar] else []
 
 /-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
-partial def InfoTree.findAllInfo (t : InfoTree) (context?: Option Elab.ContextInfo) (pred : Elab.Info → Bool) :
-    List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree) :=
+partial def InfoTree.findAllInfo
+    (t : InfoTree)
+    (context?: Option Elab.ContextInfo)
+    (haltOnMatch : Bool := false)
+    (pred : Elab.Info → Bool)
+    : List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree) :=
   match t with
-  | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) pred
+  | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) haltOnMatch pred
   | .node i children  =>
-      (if pred i then [(i, context?, children)] else []) ++ children.toList.bind (fun t => findAllInfo t context? pred)
+    let head := if pred i then [(i, context?, children)] else []
+    let tail := if haltOnMatch then [] else children.toList.bind (fun t => findAllInfo t context? haltOnMatch pred)
+    head ++ tail
   | _ => []
 
+/-- Monadic analogue of `findAllInfo` -/
+partial def InfoTree.findAllInfoM [Monad m]
+    (t : InfoTree)
+    (context?: Option Elab.ContextInfo)
+    (haltOnMatch : Bool)
+    (pred : Elab.Info → Option Elab.ContextInfo → m Bool)
+    : m (List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree)) := do
+  match t with
+  | .context inner t => t.findAllInfoM (inner.mergeIntoOuter? context?) haltOnMatch pred
+  | .node i children  =>
+    let head := if ← pred i context? then [(i, context?, children)] else []
+    let tail := if haltOnMatch then pure [] else children.toList.mapM (fun t => t.findAllInfoM context? haltOnMatch pred)
+    return head ++ (← tail).join
+  | _ => return []
+
 @[export pantograph_infotree_to_string_m]
 partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo := .none) : IO String := do
   match t with
diff --git a/Repl.lean b/Repl.lean
index 3f8a3c6..f1c8f42 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -257,10 +257,10 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
             pure $ .some invocations
           else
             pure .none
-        let sorrys := if args.sorrys then
+        let sorrys ← if args.sorrys then
             Frontend.collectSorrys step
           else
-            []
+            pure []
         let messages ← step.messageStrings
         return (step.before, boundary, invocations?, sorrys, messages)
       let li ← frontendM.run context |>.run' state
diff --git a/Test/Frontend.lean b/Test/Frontend.lean
index 015cfa8..a03b283 100644
--- a/Test/Frontend.lean
+++ b/Test/Frontend.lean
@@ -10,7 +10,9 @@ def collectSorrysFromSource (source: String) : MetaM (List GoalState) := do
   let filename := "<anonymous>"
   let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {}
   let m := Frontend.mapCompilationSteps λ step => do
-    return (step.before, Frontend.collectSorrys step)
+    for tree in step.trees do
+      IO.println s!"{← tree.toString}"
+    return (step.before, ← Frontend.collectSorrys step)
   let li ← m.run context |>.run' state
   let goalStates ← li.filterMapM λ (env, sorrys) => withEnv env do
     if sorrys.isEmpty then
@@ -177,6 +179,13 @@ example (n: Nat) : mystery n + 1 = n + 2 := sorry
     }
   ])
 
+def test_capture_type_mismatch : TestT MetaM Unit := do
+  let input := "
+def mystery : Nat := true
+  "
+  let goalStates ← (collectSorrysFromSource input).run' {}
+  let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
+
 
 def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
@@ -185,6 +194,7 @@ def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
     ("sorry_in_induction", test_sorry_in_induction),
     ("sorry_in_coupled", test_sorry_in_coupled),
     ("environment_capture", test_environment_capture),
+    ("capture_type_mismatch", test_capture_type_mismatch),
   ]
   tests.map (fun (name, test) => (name, runMetaMSeq env $ runTest test))
 

From 17ab2eafd8868652d83072f074696413825ebab5 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Dec 2024 00:03:53 -0800
Subject: [PATCH 05/15] fix: Halt on match guard

---
 Pantograph/Frontend/Elab.lean     | 2 --
 Pantograph/Frontend/InfoTree.lean | 4 ++--
 Test/Frontend.lean                | 2 --
 3 files changed, 2 insertions(+), 6 deletions(-)

diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index 6bc67f3..d5af8b5 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -123,8 +123,6 @@ private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext)
 def collectSorrys (step: CompilationStep) : IO (List InfoWithContext) := do
   return (← step.trees.mapM collectSorrysInTree).join
 
-
-
 /--
 Since we cannot directly merge `MetavarContext`s, we have to get creative. This
 function duplicates frozen mvars in term and tactic info nodes, and add them to
diff --git a/Pantograph/Frontend/InfoTree.lean b/Pantograph/Frontend/InfoTree.lean
index c72dbe6..50b0965 100644
--- a/Pantograph/Frontend/InfoTree.lean
+++ b/Pantograph/Frontend/InfoTree.lean
@@ -103,7 +103,7 @@ partial def InfoTree.findAllInfo
   | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) haltOnMatch pred
   | .node i children  =>
     let head := if pred i then [(i, context?, children)] else []
-    let tail := if haltOnMatch then [] else children.toList.bind (fun t => findAllInfo t context? haltOnMatch pred)
+    let tail := if haltOnMatch ∧ !head.isEmpty then [] else children.toList.bind (fun t => findAllInfo t context? haltOnMatch pred)
     head ++ tail
   | _ => []
 
@@ -118,7 +118,7 @@ partial def InfoTree.findAllInfoM [Monad m]
   | .context inner t => t.findAllInfoM (inner.mergeIntoOuter? context?) haltOnMatch pred
   | .node i children  =>
     let head := if ← pred i context? then [(i, context?, children)] else []
-    let tail := if haltOnMatch then pure [] else children.toList.mapM (fun t => t.findAllInfoM context? haltOnMatch pred)
+    let tail := if haltOnMatch ∧ !head.isEmpty then pure [] else children.toList.mapM (fun t => t.findAllInfoM context? haltOnMatch pred)
     return head ++ (← tail).join
   | _ => return []
 
diff --git a/Test/Frontend.lean b/Test/Frontend.lean
index a03b283..3b765fd 100644
--- a/Test/Frontend.lean
+++ b/Test/Frontend.lean
@@ -10,8 +10,6 @@ def collectSorrysFromSource (source: String) : MetaM (List GoalState) := do
   let filename := "<anonymous>"
   let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {}
   let m := Frontend.mapCompilationSteps λ step => do
-    for tree in step.trees do
-      IO.println s!"{← tree.toString}"
     return (step.before, ← Frontend.collectSorrys step)
   let li ← m.run context |>.run' state
   let goalStates ← li.filterMapM λ (env, sorrys) => withEnv env do

From 2d068ecd5072386fd4043931b96e64fd47760aab Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Dec 2024 00:06:20 -0800
Subject: [PATCH 06/15] fix: Use guarded `isDefEq`

---
 Pantograph/Frontend/Elab.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index d5af8b5..c4704fc 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -110,7 +110,7 @@ private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext)
         return true
       ctx.runMetaM lctx do
         let type ← Meta.inferType expr
-        Bool.not <$> Meta.isDefEq type expectedType
+        Bool.not <$> Meta.isExprDefEqGuarded type expectedType
     | .ofTacticInfo { stx, goalsBefore, .. } =>
       -- The `sorry` term is distinct from the `sorry` tactic
       let isSorry := stx.isOfKind `Lean.Parser.Tactic.tacticSorry

From 5ef2b5c11840890471db123ecce3f26642e38478 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Dec 2024 19:40:00 -0800
Subject: [PATCH 07/15] feat: Collect newly defined constants

---
 Pantograph/Frontend/Elab.lean | 15 ++++++++++++++-
 Test/Frontend.lean            | 27 +++++++++++++++++++++++++++
 2 files changed, 41 insertions(+), 1 deletion(-)

diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index c4704fc..4ace608 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -2,6 +2,7 @@
 import Lean.Elab.Import
 import Lean.Elab.Command
 import Lean.Elab.InfoTree
+import Lean.DeclarationRange
 
 import Pantograph.Frontend.Basic
 import Pantograph.Frontend.MetaTranslate
@@ -128,7 +129,7 @@ Since we cannot directly merge `MetavarContext`s, we have to get creative. This
 function duplicates frozen mvars in term and tactic info nodes, and add them to
 the current `MetavarContext`.
 -/
-@[export pantograph_frontend_sorrys_to_goal_state]
+@[export pantograph_frontend_sorrys_to_goal_state_m]
 def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM GoalState := do
   assert! !sorrys.isEmpty
   let goalsM := sorrys.mapM λ i => do
@@ -147,5 +148,17 @@ def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM GoalState := do
   GoalState.createFromMVars goals root
 
 
+@[export pantograph_frontend_collect_new_defined_constants_m]
+def collectNewDefinedConstants (step : CompilationStep) : IO (List Name) := do
+  step.after.constants.map₂.foldlM (λ acc name _ => do
+    if step.before.contains name then
+      return acc
+    let coreM : CoreM Bool := Option.isSome <$> findDeclarationRanges? name
+    let hasRange ← coreM.run' { fileName := step.fileName, fileMap := step.fileMap } { env := step.after } |>.toBaseIO
+    match hasRange with
+    | .ok true => return name :: acc
+    | .ok false => return acc
+    | .error e => throw $ IO.userError (← e.toMessageData.toString)
+    ) []
 
 end Pantograph.Frontend
diff --git a/Test/Frontend.lean b/Test/Frontend.lean
index 3b765fd..68aaf94 100644
--- a/Test/Frontend.lean
+++ b/Test/Frontend.lean
@@ -184,6 +184,31 @@ def mystery : Nat := true
   let goalStates ← (collectSorrysFromSource input).run' {}
   let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
 
+def collectNewConstants (source: String) : MetaM (List (List Name)) := do
+  let filename := "<anonymous>"
+  let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {}
+  let m := Frontend.mapCompilationSteps λ step => do
+    Frontend.collectNewDefinedConstants step
+  m.run context |>.run' state
+
+def test_collect_one_constant : TestT MetaM Unit := do
+  let input := "
+def mystery : Nat := 123
+  "
+  let names ← collectNewConstants input
+  checkEq "constants" names [[`mystery]]
+def test_collect_one_theorem : TestT MetaM Unit := do
+  let input := "
+theorem mystery [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get i) < sizeOf as := by
+  match as, i with
+  | a::as, ⟨0, _⟩  => simp_arith [get]
+  | a::as, ⟨i+1, h⟩ =>
+    have ih := sizeOf_get as ⟨i, Nat.le_of_succ_le_succ h⟩
+    apply Nat.lt_trans ih
+    simp_arith
+  "
+  let names ← collectNewConstants input
+  checkEq "constants" names [[`mystery]]
 
 def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
@@ -193,6 +218,8 @@ def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
     ("sorry_in_coupled", test_sorry_in_coupled),
     ("environment_capture", test_environment_capture),
     ("capture_type_mismatch", test_capture_type_mismatch),
+    ("collect_one_constant", test_collect_one_constant),
+    ("collect_one_theorem", test_collect_one_theorem),
   ]
   tests.map (fun (name, test) => (name, runMetaMSeq env $ runTest test))
 

From 0b4ded10493585aeba2e9b345ddc9ed81d4a02ad Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Dec 2024 20:15:53 -0800
Subject: [PATCH 08/15] fix: Collect sorrys and type mismatches

---
 Pantograph/Frontend/Elab.lean     | 21 +++++++++++++--------
 Pantograph/Frontend/InfoTree.lean | 12 ++++++------
 Test/Frontend.lean                | 11 ++++++++++-
 3 files changed, 29 insertions(+), 15 deletions(-)

diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index 4ace608..2eff084 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -103,20 +103,25 @@ structure InfoWithContext where
   context?: Option Elab.ContextInfo := .none
 
 private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext) := do
-  let infos ← t.findAllInfoM none true fun i ctx? => match i with
+  let infos ← t.findAllInfoM none fun i ctx? => match i with
     | .ofTermInfo { expectedType?, expr, stx, lctx, .. } => do
-      let .some expectedType := expectedType? | return false
-      let .some ctx := ctx? | return false
+      let .some expectedType := expectedType? | return (false, true)
+      let .some ctx := ctx? | return (false, true)
       if expr.isSorry ∧ stx.isOfKind `Lean.Parser.Term.sorry then
-        return true
-      ctx.runMetaM lctx do
+        return (true, false)
+      let typeMatch ← ctx.runMetaM lctx do
         let type ← Meta.inferType expr
-        Bool.not <$> Meta.isExprDefEqGuarded type expectedType
+        Meta.isExprDefEqGuarded type expectedType
+      return match typeMatch, expr.hasSorry with
+      | false, true => (true, false) -- Types mismatch but has sorry -> collect, halt
+      | false, false => (true, false) -- Types mistmatch but no sorry -> collect, halt
+      | true, true => (false, true) -- Types match but has sorry -> continue
+      | true, false => (false, false) -- Types match but no sorries -> halt
     | .ofTacticInfo { stx, goalsBefore, .. } =>
       -- The `sorry` term is distinct from the `sorry` tactic
       let isSorry := stx.isOfKind `Lean.Parser.Tactic.tacticSorry
-      return isSorry ∧ !goalsBefore.isEmpty
-    | _ => return false
+      return (isSorry ∧ !goalsBefore.isEmpty, ¬ isSorry)
+    | _ => return (false, true)
   return infos.map fun (info, context?, _) => { info, context? }
 
 -- NOTE: Plural deliberately not spelled "sorries"
diff --git a/Pantograph/Frontend/InfoTree.lean b/Pantograph/Frontend/InfoTree.lean
index 50b0965..cfef621 100644
--- a/Pantograph/Frontend/InfoTree.lean
+++ b/Pantograph/Frontend/InfoTree.lean
@@ -107,18 +107,18 @@ partial def InfoTree.findAllInfo
     head ++ tail
   | _ => []
 
-/-- Monadic analogue of `findAllInfo` -/
+/-- Monadic analogue of `findAllInfo`, but predicate controls whether to recurse. -/
 partial def InfoTree.findAllInfoM [Monad m]
     (t : InfoTree)
     (context?: Option Elab.ContextInfo)
-    (haltOnMatch : Bool)
-    (pred : Elab.Info → Option Elab.ContextInfo → m Bool)
+    (pred : Elab.Info → Option Elab.ContextInfo → m (Bool × Bool))
     : m (List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree)) := do
   match t with
-  | .context inner t => t.findAllInfoM (inner.mergeIntoOuter? context?) haltOnMatch pred
+  | .context inner t => t.findAllInfoM (inner.mergeIntoOuter? context?) pred
   | .node i children  =>
-    let head := if ← pred i context? then [(i, context?, children)] else []
-    let tail := if haltOnMatch ∧ !head.isEmpty then pure [] else children.toList.mapM (fun t => t.findAllInfoM context? haltOnMatch pred)
+    let (flagCollect, flagRecurse) ← pred i context?
+    let head := if flagCollect then [(i, context?, children)] else []
+    let tail := if ¬ flagRecurse then pure [] else children.toList.mapM (fun t => t.findAllInfoM context? pred)
     return head ++ (← tail).join
   | _ => return []
 
diff --git a/Test/Frontend.lean b/Test/Frontend.lean
index 68aaf94..2259029 100644
--- a/Test/Frontend.lean
+++ b/Test/Frontend.lean
@@ -179,10 +179,19 @@ example (n: Nat) : mystery n + 1 = n + 2 := sorry
 
 def test_capture_type_mismatch : TestT MetaM Unit := do
   let input := "
-def mystery : Nat := true
+def mystery (k: Nat) : Nat := true
   "
   let goalStates ← (collectSorrysFromSource input).run' {}
   let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
+  checkEq "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize)) #[
+    {
+      target := { pp? := "Nat" },
+      vars := #[{
+         userName := "k",
+         type? := .some { pp? := "Nat" },
+      }],
+    }
+  ]
 
 def collectNewConstants (source: String) : MetaM (List (List Name)) := do
   let filename := "<anonymous>"

From dd00d803d1fe500f46710bb32bfcc9eeeb2d8062 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Dec 2024 20:38:27 -0800
Subject: [PATCH 09/15] feat: Collect sorry/elab failure boundaries

---
 Pantograph/Frontend/Basic.lean |  7 +++++++
 Pantograph/Frontend/Elab.lean  | 19 ++++++++++++++-----
 Pantograph/Protocol.lean       |  2 ++
 Repl.lean                      | 13 +++++++------
 Test/Frontend.lean             |  4 ++--
 5 files changed, 32 insertions(+), 13 deletions(-)

diff --git a/Pantograph/Frontend/Basic.lean b/Pantograph/Frontend/Basic.lean
index 1074a94..87decd4 100644
--- a/Pantograph/Frontend/Basic.lean
+++ b/Pantograph/Frontend/Basic.lean
@@ -30,6 +30,13 @@ end Lean.PersistentArray
 
 namespace Pantograph.Frontend
 
+@[export pantograph_frontend_stx_byte_range]
+def stxByteRange (stx : Syntax) : String.Pos × String.Pos :=
+  let pos := stx.getPos?.getD 0
+  let endPos := stx.getTailPos?.getD 0
+  (pos, endPos)
+
+
 abbrev FrontendM := Elab.Frontend.FrontendM
 
 structure CompilationStep where
diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index 2eff084..a33fbef 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -129,28 +129,37 @@ private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext)
 def collectSorrys (step: CompilationStep) : IO (List InfoWithContext) := do
   return (← step.trees.mapM collectSorrysInTree).join
 
+structure AnnotatedGoalState where
+  state : GoalState
+  srcBoundaries : List (String.Pos × String.Pos)
+
 /--
 Since we cannot directly merge `MetavarContext`s, we have to get creative. This
 function duplicates frozen mvars in term and tactic info nodes, and add them to
 the current `MetavarContext`.
 -/
 @[export pantograph_frontend_sorrys_to_goal_state_m]
-def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM GoalState := do
+def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM AnnotatedGoalState := do
   assert! !sorrys.isEmpty
   let goalsM := sorrys.mapM λ i => do
     match i.info with
     | .ofTermInfo termInfo  => do
       let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context?
-      return [mvarId]
+      return [(mvarId, stxByteRange termInfo.stx)]
     | .ofTacticInfo tacticInfo => do
-      MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
+      let mvarIds ← MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
+      let range := stxByteRange tacticInfo.stx
+      return mvarIds.map (·, range)
     | _ => panic! "Invalid info"
-  let goals := List.join (← goalsM.run {} |>.run' {})
+  let annotatedGoals := List.join (← goalsM.run {} |>.run' {})
+  let goals := annotatedGoals.map Prod.fst
+  let srcBoundaries := annotatedGoals.map Prod.snd
   let root := match goals with
     | [] => panic! "No MVars generated"
     | [g] => g
     | _ => { name := .anonymous }
-  GoalState.createFromMVars goals root
+  let state ← GoalState.createFromMVars goals root
+  return { state, srcBoundaries }
 
 
 @[export pantograph_frontend_collect_new_defined_constants_m]
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 0cb6cac..5cb24e8 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -329,6 +329,8 @@ structure CompilationUnit where
   invocations?: Option (List InvokedTactic) := .none
   goalStateId?: Option Nat := .none
   goals: Array Goal := #[]
+  -- Code segments which generated the goals
+  goalSrcBoundaries: Array (Nat × Nat) := #[]
   messages: Array String := #[]
   deriving Lean.ToJson
 structure FrontendProcessResult where
diff --git a/Repl.lean b/Repl.lean
index f1c8f42..201a841 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -265,18 +265,19 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
         return (step.before, boundary, invocations?, sorrys, messages)
       let li ← frontendM.run context |>.run' state
       let units ← li.mapM λ (env, boundary, invocations?, sorrys, messages) => Lean.withEnv env do
-        let (goalStateId?, goals) ← if sorrys.isEmpty then do
-            pure (.none, #[])
+        let (goalStateId?, goals, goalSrcBoundaries) ← if sorrys.isEmpty then do
+            pure (.none, #[], #[])
           else do
-            let goalState ← runMetaInMainM $ Frontend.sorrysToGoalState sorrys
-            let stateId ← newGoalState goalState
-            let goals ← goalSerialize goalState options
-            pure (.some stateId, goals)
+            let { state, srcBoundaries } ← runMetaInMainM $ Frontend.sorrysToGoalState sorrys
+            let stateId ← newGoalState state
+            let goals ← goalSerialize state options
+            pure (.some stateId, goals, srcBoundaries.toArray.map (λ (b, e) => (b.byteIdx, e.byteIdx)))
         return {
           boundary,
           invocations?,
           goalStateId?,
           goals,
+          goalSrcBoundaries,
           messages,
         }
       return .ok { units }
diff --git a/Test/Frontend.lean b/Test/Frontend.lean
index 2259029..a3b73ae 100644
--- a/Test/Frontend.lean
+++ b/Test/Frontend.lean
@@ -15,8 +15,8 @@ def collectSorrysFromSource (source: String) : MetaM (List GoalState) := do
   let goalStates ← li.filterMapM λ (env, sorrys) => withEnv env do
     if sorrys.isEmpty then
       return .none
-    let goalState ← Frontend.sorrysToGoalState sorrys
-    return .some goalState
+    let { state, .. } ← Frontend.sorrysToGoalState sorrys
+    return .some state
   return goalStates
 
 def test_multiple_sorrys_in_proof : TestT MetaM Unit := do

From 9a69c48cb23f313e5986e87a8867eaf3d9b6528e Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Dec 2024 20:42:05 -0800
Subject: [PATCH 10/15] fix: Integration test failure

---
 Test/Integration.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Test/Integration.lean b/Test/Integration.lean
index 9fb86b7..171bc91 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -222,6 +222,7 @@ def test_frontend_process_sorry : Test :=
          boundary := (solved.utf8ByteSize, solved.utf8ByteSize + withSorry.utf8ByteSize),
          goalStateId? := .some 0,
          goals := #[goal1],
+         goalSrcBoundaries := #[(57, 62)],
          messages := #["<anonymous>:2:0: warning: declaration uses 'sorry'\n"],
        }],
     }: Protocol.FrontendProcessResult),

From eb0374dfb3cd73df86bfcfe5a0ed1f5d03d37cce Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Dec 2024 20:57:25 -0800
Subject: [PATCH 11/15] feat: Collect new constants in repl

---
 Pantograph/Protocol.lean |  3 +++
 Repl.lean                | 13 +++++++++++--
 Test/Integration.lean    |  2 ++
 3 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 5cb24e8..d80c761 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -312,6 +312,8 @@ structure FrontendProcess where
   invocations: Bool := false
   -- If set to true, collect `sorry`s
   sorrys: Bool := false
+  -- If set to true, extract new constants
+  newConstants: Bool := false
   deriving Lean.FromJson
 structure InvokedTactic where
   goalBefore: String
@@ -332,6 +334,7 @@ structure CompilationUnit where
   -- Code segments which generated the goals
   goalSrcBoundaries: Array (Nat × Nat) := #[]
   messages: Array String := #[]
+  newConstants: Option (Array String) := .none
   deriving Lean.ToJson
 structure FrontendProcessResult where
   units: List CompilationUnit
diff --git a/Repl.lean b/Repl.lean
index 201a841..710b132 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -262,9 +262,17 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
           else
             pure []
         let messages ← step.messageStrings
-        return (step.before, boundary, invocations?, sorrys, messages)
+        let newConstants ← if args.newConstants then
+            Frontend.collectNewDefinedConstants step
+          else
+            pure []
+        return (step.before, boundary, invocations?, sorrys, messages, newConstants)
       let li ← frontendM.run context |>.run' state
-      let units ← li.mapM λ (env, boundary, invocations?, sorrys, messages) => Lean.withEnv env do
+      let units ← li.mapM λ (env, boundary, invocations?, sorrys, messages, newConstants) => Lean.withEnv env do
+        let newConstants := if args.newConstants then
+            .some $ newConstants.toArray.map λ name => name.toString
+          else
+            .none
         let (goalStateId?, goals, goalSrcBoundaries) ← if sorrys.isEmpty then do
             pure (.none, #[], #[])
           else do
@@ -279,6 +287,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
           goals,
           goalSrcBoundaries,
           messages,
+          newConstants,
         }
       return .ok { units }
     catch e =>
diff --git a/Test/Integration.lean b/Test/Integration.lean
index 171bc91..8d53168 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -174,6 +174,7 @@ def test_frontend_process : Test :=
         ("file", .str file),
         ("invocations", .bool true),
         ("sorrys", .bool false),
+        ("newConstants", .bool false),
       ]
      ({
        units := [{
@@ -214,6 +215,7 @@ def test_frontend_process_sorry : Test :=
         ("file", .str file),
         ("invocations", .bool false),
         ("sorrys", .bool true),
+        ("newConstants", .bool false),
       ]
      ({
        units := [{

From 1527743900b2af65514be9cf6a3d9f18b818874a Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Dec 2024 21:00:33 -0800
Subject: [PATCH 12/15] refactor: Optionalize CompilationUnit

---
 Pantograph/Protocol.lean | 10 ++++++----
 Repl.lean                | 17 +++++++++--------
 Test/Integration.lean    |  4 ++--
 3 files changed, 17 insertions(+), 14 deletions(-)

diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index d80c761..f232d9e 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -327,14 +327,16 @@ structure InvokedTactic where
 structure CompilationUnit where
   -- String boundaries of compilation units
   boundary: (Nat × Nat)
+  messages: Array String := #[]
   -- Tactic invocations
   invocations?: Option (List InvokedTactic) := .none
   goalStateId?: Option Nat := .none
-  goals: Array Goal := #[]
+  goals?: Option (Array Goal) := .none
   -- Code segments which generated the goals
-  goalSrcBoundaries: Array (Nat × Nat) := #[]
-  messages: Array String := #[]
-  newConstants: Option (Array String) := .none
+  goalSrcBoundaries?: Option (Array (Nat × Nat)) := .none
+
+  -- New constants defined in compilation unit
+  newConstants?: Option (Array String) := .none
   deriving Lean.ToJson
 structure FrontendProcessResult where
   units: List CompilationUnit
diff --git a/Repl.lean b/Repl.lean
index 710b132..283bcf3 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -269,25 +269,26 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
         return (step.before, boundary, invocations?, sorrys, messages, newConstants)
       let li ← frontendM.run context |>.run' state
       let units ← li.mapM λ (env, boundary, invocations?, sorrys, messages, newConstants) => Lean.withEnv env do
-        let newConstants := if args.newConstants then
+        let newConstants? := if args.newConstants then
             .some $ newConstants.toArray.map λ name => name.toString
           else
             .none
-        let (goalStateId?, goals, goalSrcBoundaries) ← if sorrys.isEmpty then do
-            pure (.none, #[], #[])
+        let (goalStateId?, goals?, goalSrcBoundaries?) ← if sorrys.isEmpty then do
+            pure (.none, .none, .none)
           else do
             let { state, srcBoundaries } ← runMetaInMainM $ Frontend.sorrysToGoalState sorrys
             let stateId ← newGoalState state
             let goals ← goalSerialize state options
-            pure (.some stateId, goals, srcBoundaries.toArray.map (λ (b, e) => (b.byteIdx, e.byteIdx)))
+            let srcBoundaries := srcBoundaries.toArray.map (λ (b, e) => (b.byteIdx, e.byteIdx))
+            pure (.some stateId, .some goals, .some srcBoundaries)
         return {
           boundary,
+          messages,
           invocations?,
           goalStateId?,
-          goals,
-          goalSrcBoundaries,
-          messages,
-          newConstants,
+          goals?,
+          goalSrcBoundaries?,
+          newConstants?,
         }
       return .ok { units }
     catch e =>
diff --git a/Test/Integration.lean b/Test/Integration.lean
index 8d53168..3e9bed2 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -223,8 +223,8 @@ def test_frontend_process_sorry : Test :=
        }, {
          boundary := (solved.utf8ByteSize, solved.utf8ByteSize + withSorry.utf8ByteSize),
          goalStateId? := .some 0,
-         goals := #[goal1],
-         goalSrcBoundaries := #[(57, 62)],
+         goals? := .some #[goal1],
+         goalSrcBoundaries? := .some #[(57, 62)],
          messages := #["<anonymous>:2:0: warning: declaration uses 'sorry'\n"],
        }],
     }: Protocol.FrontendProcessResult),

From 37a5884be40790a946e0b8e26879ed3bbf509077 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Dec 2024 21:39:33 -0800
Subject: [PATCH 13/15] fix: Use `ppSyntax` instead of `ppTactic`

---
 Pantograph/Frontend/Elab.lean | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index a33fbef..d9480f0 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -87,9 +87,11 @@ def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protoc
   tactics.mapM λ invocation => do
     let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty
     let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty
-    let tactic ← invocation.ctx.runMetaM {} do
-      let t ← PrettyPrinter.ppTactic ⟨invocation.info.stx⟩
-      return t.pretty
+    let tactic ← invocation.ctx.runMetaM {} <| Meta.withMCtx invocation.info.mctxBefore do
+      return (← invocation.ctx.ppSyntax {} invocation.info.stx).pretty
+      -- FIXME: Why does this not work? There are problems with `term.pseudo.antiquot`
+      --PrettyPrinter.ppTactic ⟨invocation.info.stx⟩
+      --return t.pretty
     let usedConstants := invocation.usedConstants.toArray.map λ n => n.toString
     return {
       goalBefore,

From 681c3fb78d2055e4d8dbe1fcd2ef5c66d28b6469 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 10 Dec 2024 12:21:56 -0800
Subject: [PATCH 14/15] fix: Disallow indeterminant type `sorry`

---
 Pantograph/Frontend/Elab.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index d9480f0..3da5fca 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -1,4 +1,3 @@
-/- Adapted from https://github.com/semorrison/lean-training-data -/
 import Lean.Elab.Import
 import Lean.Elab.Command
 import Lean.Elab.InfoTree
@@ -16,6 +15,7 @@ namespace Pantograph.Frontend
 
 -- Info tree filtering functions
 
+/- Adapted from lean-training-data -/
 structure TacticInvocation where
   info : Elab.TacticInfo
   ctx : Elab.ContextInfo
@@ -107,10 +107,12 @@ structure InfoWithContext where
 private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext) := do
   let infos ← t.findAllInfoM none fun i ctx? => match i with
     | .ofTermInfo { expectedType?, expr, stx, lctx, .. } => do
-      let .some expectedType := expectedType? | return (false, true)
       let .some ctx := ctx? | return (false, true)
       if expr.isSorry ∧ stx.isOfKind `Lean.Parser.Term.sorry then
+        if expectedType?.isNone then
+          throw $ .userError "Sorry of indeterminant type is not allowed"
         return (true, false)
+      let .some expectedType := expectedType? | return (false, true)
       let typeMatch ← ctx.runMetaM lctx do
         let type ← Meta.inferType expr
         Meta.isExprDefEqGuarded type expectedType

From 95503c45e4ac6217889cd21d63672d58768835f1 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 10 Dec 2024 21:45:57 -0800
Subject: [PATCH 15/15] doc: frontend.process newConstants

---
 doc/repl.md | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/doc/repl.md b/doc/repl.md
index 464c7cc..d332986 100644
--- a/doc/repl.md
+++ b/doc/repl.md
@@ -44,9 +44,11 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
   state. The user is responsible to ensure the sender/receiver instances share
   the same environment.
 * `frontend.process { ["fileName": <fileName>,] ["file": <str>], invocations:
-  <bool>, sorrys: <bool> }`: Executes the Lean frontend on a file, collecting
-  either the tactic invocations (`"invocations": true`) or the sorrys into goal
-  states (`"sorrys": true`)
+  <bool>, sorrys: <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`.
 
 ## Errors