fix: NameGenerator bug (#32)

Author: kim-em

REPL/Lean/InfoTree.lean

@@ -189,7 +189,7 @@ def findSorryTermNodes (t : InfoTree) : List (TermInfo × ContextInfo) :=
 inductive SorryType
 | tactic : MVarId → SorryType
 | term : LocalContext → Option Expr → SorryType
-
+#check MVarId
 /--
 Finds all appearances of `sorry` in an `InfoTree`, reporting
 * the `ContextInfo` at that point,
@@ -199,7 +199,9 @@ Finds all appearances of `sorry` in an `InfoTree`, reporting
 -/
 def sorries (t : InfoTree) : List (ContextInfo × SorryType × Position × Position) :=
   (t.findSorryTacticNodes.map fun ⟨i, ctx⟩ =>
-    ({ ctx with mctx := i.mctxBefore }, .tactic i.goalsBefore.head!, stxRange ctx.fileMap i.stx)) ++
+    let g := i.goalsBefore.head!
+    let ngen := { ctx.ngen with namePrefix := g.name }
+    ({ ctx with mctx := i.mctxBefore, ngen := ngen }, .tactic g, stxRange ctx.fileMap i.stx)) ++
   (t.findSorryTermNodes.map fun ⟨i, ctx⟩ =>
     (ctx, .term i.lctx i.expectedType?, stxRange ctx.fileMap i.stx))
 

REPL/Main.lean

@@ -240,7 +240,7 @@ def runProofStep (s : ProofStep) : M IO (ProofStepResponse ⊕ Error) := do
       let proofState' ← proofState.runString s.tactic
       return .inl (← createProofStepReponse proofState' proofState)
     catch ex =>
-      return .inr ⟨ex.toString⟩
+      return .inr ⟨"Lean error:\n" ++ ex.toString⟩
 
 end REPL
 
@@ -272,7 +272,8 @@ inductive Input
 def parse (query : String) : IO Input := do
   let json := Json.parse query
   match json with
-  | .error e => throw <| IO.userError <| toString <| toJson (⟨e⟩ : Error)
+  | .error e => throw <| IO.userError <| toString <| toJson <|
+      (⟨"Could not parse JSON:\n" ++ e⟩ : Error)
   | .ok j => match fromJson? j with
     | .ok (r : REPL.ProofStep) => return .proofStep r
     | .error _ => match fromJson? j with
@@ -285,7 +286,8 @@ def parse (query : String) : IO Input := do
     | .ok (r : REPL.UnpickleProofState) => return .unpickleProofSnapshot r
     | .error _ => match fromJson? j with
     | .ok (r : REPL.Command) => return .command r
-    | .error e => throw <| IO.userError <| toString <| toJson (⟨e⟩ : Error)
+    | .error e => throw <| IO.userError <| toString <| toJson <|
+        (⟨"Could not parse as a valid JSON command:\n" ++ e⟩ : Error)
 
 /-- Read-eval-print loop for Lean. -/
 unsafe def repl : IO Unit :=
@@ -294,6 +296,7 @@ where loop : M IO Unit := do
   let query ← getLines
   if query = "" then
     return ()
+  if query.startsWith "#" || query.startsWith "--" then loop else
   IO.println <| toString <| ← match ← parse query with
   | .command r => return toJson (← runCommand r)
   | .proofStep r => return toJson (← runProofStep r)

REPL/Snapshots.lean

@@ -182,7 +182,6 @@ def runString (p : ProofSnapshot) (t : String) : IO ProofSnapshot :=
 /-- Pretty print the current goals in the `ProofSnapshot`. -/
 def ppGoals (p : ProofSnapshot) : IO (List Format) :=
   Prod.fst <$> p.runMetaM do p.tacticState.goals.mapM (Meta.ppGoal ·)
-
 /--
 Construct a `ProofSnapshot` from a `ContextInfo` and optional `LocalContext`, and a list of goals.
 
@@ -193,6 +192,7 @@ def create (ctx : ContextInfo) (lctx? : Option LocalContext)
     (goals : List MVarId) (types : List Expr := []) : IO ProofSnapshot := do
   ctx.runMetaM (lctx?.getD {}) do
     let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t))
+    goals.head!.withContext do
     pure <|
     { coreState := ← getThe Core.State
       coreContext := ← readThe Core.Context

test/name_generator.expected.out

@@ -0,0 +1,49 @@
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 2, "column": 45},
+   "goal": "x : Int\nh0 : x > 0\n⊢ False",
+   "endPos": {"line": 2, "column": 50}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 2, "column": 0},
+   "endPos": {"line": 2, "column": 7},
+   "data": "declaration uses 'sorry'"}],
+ "env": 0}
+
+{"sorries": [{"proofState": 1, "goal": "x : Int\nh0 : x > 0\n⊢ x > 0"}],
+ "proofState": 2,
+ "goals": ["x : Int\nh0 h : x > 0\n⊢ False"]}
+
+{"proofState": 3, "goals": []}
+
+{"proofState": 4, "goals": []}
+
+{"traces":
+ ["[Meta.Tactic.simp.rewrite] of_eq_true (eq_true h0):1000, x > 0 ==> True"],
+ "proofState": 5,
+ "goals": []}
+
+{"traces": ["[Meta.Tactic.simp.rewrite] h0:1000, x > 0 ==> True"],
+ "proofState": 6,
+ "goals": []}
+
+{"traces": ["[Meta.Tactic.simp.rewrite] h0:1000, x > 0 ==> True"],
+ "proofState": 7,
+ "goals": []}
+
+{"proofState": 8,
+ "messages":
+ [{"severity": "error",
+   "pos": {"line": 0, "column": 0},
+   "endPos": {"line": 0, "column": 0},
+   "data": "unsolved goals\nx : Int\nh0 : x > 0\n⊢ x > 0"}],
+ "goals": []}
+
+{"proofState": 9,
+ "messages":
+ [{"severity": "error",
+   "pos": {"line": 0, "column": 0},
+   "endPos": {"line": 0, "column": 0},
+   "data": "unsolved goals\nx : Int\nh0 : x > 0\n⊢ x > 0"}],
+ "goals": []}
+

test/name_generator.in

@@ -0,0 +1,18 @@
+{"cmd": "set_option trace.Meta.Tactic.simp true\nexample {x : Int} (h0 : x > 0) : False := by sorry"}
+
+{"tactic": "have h : x > 0 := by sorry", "proofState": 0}
+
+{"tactic": "exact h0", "proofState": 1}
+
+{"tactic": "assumption", "proofState": 1}
+
+{"tactic": "simp only [of_eq_true (eq_true h0)]", "proofState": 1}
+
+{"tactic": "{ simp [h0] }", "proofState": 1}
+
+{"tactic": "{ simp (config := {memoize := false}) [h0] }", "proofState": 1}
+
+{"tactic": "{ rw (config := {}) [(show x = x from rfl)] }", "proofState": 1}
+
+{"tactic": "{ rw [(show x = x from rfl)] }", "proofState": 1}
+

test/unknown_tactic.expected.out

@@ -10,5 +10,5 @@
    "data": "declaration uses 'sorry'"}],
  "env": 0}
 
-{"message": "<input>:1:1: unknown tactic"}
+{"message": "Lean error:\n<input>:1:1: unknown tactic"}