Merge branch 'repl++' of github.com:leanprover-community/repl into re…

…pl++

README.md

@@ -115,7 +115,7 @@ results in output
  [{"tactic": "exact rfl",
    "proofState": 0,
    "pos": {"line": 5, "column": 29},
-   "goals": "⊢ f + g = 39",
+   "goalsBefore": "⊢ f + g = 39",
    "endPos": {"line": 5, "column": 38}}],
  "env": 0}
  ```
@@ -143,11 +143,11 @@ Example usage:
 
 {"tactic": "apply Int.natAbs", "proofState": 0}
 
-{"proofState": 1, "goals": ["x : Unit\n⊢ Int"]}
+{"proofState": 1, "goalsBefore": ["x : Unit\n⊢ Int"]}
 
 {"tactic": "exact -37", "proofState": 1}
 
-{"proofState": 2, "goals": []}
+{"proofState": 2, "goalsBefore": []}
 ```
 
 You can use `sorry` in tactic mode.

REPL/JSON/REPL.lean

@@ -21,9 +21,9 @@ open JSON
 -/
 
 def TacticResult.toJson (t : TacticResult) : M m JSON.Tactic := do
-  let goals := "\n".intercalate (← t.proofState.ppGoals)
-  let proofStateId ← recordProofSnapshot t.proofState
-  return Tactic.of goals t.src t.pos t.endPos proofStateId
+  let goals := "\n".intercalate (← t.before.ppGoals)
+  let proofStateId ← recordProofSnapshot t.before
+  return Tactic.of goals none t.src t.pos t.endPos proofStateId
 
 def SorryResult.toJson (s : SorryResult) : M m JSON.Sorry := do
   return { ← TacticResult.toJson s.toTacticResult with }
@@ -50,7 +50,7 @@ def ProofStepResponse.toJson (r : ProofStepResponse) : M m JSON.ProofStepRespons
   let id ← recordProofSnapshot r.proofState
   return {
     proofState := id
-    goals := (← r.proofState.ppGoals)
+    goalsAfter := (← r.proofState.ppGoals)
     messages
     sorries
     traces := r.traces }

REPL/JSON/Types.lean

@@ -87,7 +87,8 @@ def Message.of (m : Lean.Message) : IO Message := do pure <|
 structure Tactic where
   pos : Pos
   endPos : Pos
-  goals : String
+  goalsBefore : String
+  goalsAfter? : Option String
   tactic : String
   /--
   The index of the proof state at the sorry.
@@ -97,10 +98,12 @@ structure Tactic where
 deriving ToJson
 
 /-- Construct the JSON representation of a Lean tactic. -/
-def Tactic.of (goals tactic : String) (pos endPos : Lean.Position) (proofState : Option Nat) : Tactic :=
+def Tactic.of (goalsBefore : String) (goalsAfter? : Option String) (tactic : String)
+    (pos endPos : Lean.Position) (proofState : Option Nat) : Tactic :=
   { pos := ⟨pos.line, pos.column⟩,
     endPos := ⟨endPos.line, endPos.column⟩,
-    goals,
+    goalsBefore,
+    goalsAfter?,
     tactic,
     proofState }
 
@@ -110,15 +113,20 @@ structure Sorry extends Tactic where
 
 instance : ToJson Sorry where
   toJson r := Json.mkObj <| .join [
-    [("goals", r.goals)],
+    [("goalsBefore", r.goalsBefore)],
+    match r.goalsAfter? with | .none => [] | .some a => [("goalsAfter", a)],
     [("proofState", toJson r.proofState)],
     if r.pos.line ≠ 0 then [("pos", toJson r.pos)] else [],
     if r.endPos.line ≠ 0 then [("endPos", toJson r.endPos)] else [],
   ]
 
 /-- Construct the JSON representation of a Lean sorry. -/
 def Sorry.of (goal : String) (pos endPos : Lean.Position) (proofState : Option Nat) : Sorry :=
-  { Tactic.of goal "sorry" pos endPos proofState with }
+  { Tactic.of goal none "sorry" pos endPos proofState with }
+
+structure Proof where
+
+deriving ToJson
 
 structure SourceResponse where
   src : String
@@ -134,6 +142,7 @@ structure CommandResponse where
   messages : List Message := []
   sorries : List Sorry := []
   tactics : List Tactic := []
+  proofs : List Proof := []
   infotree : Option Json := none
 
 def Json.nonemptyList [ToJson α] (k : String) : List α → List (String × Json)
@@ -160,7 +169,7 @@ A response to a Lean tactic.
 -/
 structure ProofStepResponse where
   proofState : Nat
-  goals : List String
+  goalsAfter : List String
   messages : List Message := []
   sorries : List Sorry := []
   traces : List String
@@ -169,7 +178,7 @@ deriving ToJson
 instance : ToJson ProofStepResponse where
   toJson r := Json.mkObj <| .join [
     [("proofState", r.proofState)],
-    [("goals", toJson r.goals)],
+    [("goalsAfter", toJson r.goalsAfter)],
     Json.nonemptyList "messages" r.messages,
     Json.nonemptyList "sorries" r.sorries,
     Json.nonemptyList "traces" r.traces

REPL/Main.lean

@@ -235,7 +235,8 @@ def recordProofSnapshot (proofState : ProofSnapshot) : M m Nat := do
   return id
 
 structure TacticResult where
-  proofState : ProofSnapshot
+  before : ProofSnapshot
+  after? : Option ProofSnapshot := none
   src : String
   stx : Syntax
   pos : Position
@@ -249,7 +250,10 @@ def tactics (trees : List InfoTree) : m (List TacticResult) :=
   trees.bind InfoTree.tactics |>.mapM
     fun ⟨ctx, stx, goals, pos, endPos⟩ => do
       let src := Format.pretty (← ppTactic ctx stx)
-      return { proofState := (← ProofSnapshot.create ctx none none goals), pos, endPos, src, stx }
+      return {
+        after? := none,
+        before := (← ProofSnapshot.create ctx none none goals),
+        pos, endPos, src, stx }
 where ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format :=
   ctx.runMetaM {} try
     Lean.PrettyPrinter.ppTactic ⟨stx⟩
@@ -261,9 +265,9 @@ def sorries (trees : List InfoTree) (env? : Option Environment) : m (List SorryR
     fun ⟨ctx, g, pos, endPos⟩ => do
       match g with
       | .tactic g => do
-        pure <| some { proofState := (← ProofSnapshot.create ctx none env? [g]), pos, endPos }
+        pure <| some { before := (← ProofSnapshot.create ctx none env? [g]), pos, endPos }
       | .term lctx (some t) => do
-        pure <| some { proofState := (← ProofSnapshot.create ctx lctx env? [] [t]), pos, endPos }
+        pure <| some { before := (← ProofSnapshot.create ctx lctx env? [] [t]), pos, endPos }
       | .term _ none =>
         pure none
 

REPL/Proof.lean

@@ -4,77 +4,92 @@ open Lean Elab Lean.Parser.Tactic
 
 namespace Proof
 
+/-- The metavariable context and goals observed at some point in a proof. -/
 structure State where
   mctx : MetavarContext
-  goals : Array MVarId
+  goals : List MVarId
 
+/-- The goals both before and after a proof step. -/
 structure Goals where
   before : State
   after : State
 
-structure Data where
+/-- The syntax of a proof step, and if already observed, the goals before and after. -/
+structure Step where
   stx : Syntax
   goals? : Option Goals := none
 
+def Step.ofTacticInfo (i : TacticInfo) : Step where
+  stx := i.stx
+  goals? := some <|
+  { before := { mctx := i.mctxBefore, goals := i.goalsBefore },
+    after := { mctx := i.mctxAfter, goals := i.goalsAfter} }
+
 end Proof
 
 open Proof
 
+/--
+An inductive type representing a structured proof script.
+
+The constructors do not exhaustively represent possible structuring tactics:
+as a fallback some blocks will be represented by `atom`.
+-/
 inductive Proof where
-  | atom : Data → Proof
-  | tacticSeq : Data → Array Proof → Proof
-  | cdot : Data → Proof → Proof
+  | atom : Step → Proof
+  | tacticSeq : Step → Array Proof → Proof
+  | cdot : Step → Proof → Proof
 namespace Proof
 
 instance : Inhabited Proof := ⟨.atom { stx := .missing }⟩
 
-def data : Proof → Data
+def step : Proof → Step
   | atom d => d
   | tacticSeq d _ => d
   | cdot d _ => d
 
--- We're probably not going to use this: reading the `InfoTree` immediately is easier than
--- doing one pass on the Syntax and then trying to merge in the `InfoTree` data.
-partial def ofSyntax (stx : Syntax) : Proof :=
-  match stx with
-  | Syntax.node _ ``tacticSeq #[Syntax.node _ ``tacticSeq1Indented ps] =>
-    .tacticSeq { stx } (ps.map ofSyntax)
-  | Syntax.node _ _ _  => atom { stx }
-  | _ => unreachable!
+-- -- We're probably not going to use this: reading the `InfoTree` immediately is easier than
+-- -- doing one pass on the Syntax and then trying to merge in the `InfoTree` data.
+-- partial def ofSyntax (stx : Syntax) : Proof :=
+--   match stx with
+--   | Syntax.node _ ``tacticSeq #[Syntax.node _ ``tacticSeq1Indented ps] =>
+--     .tacticSeq { stx } (ps.map ofSyntax)
+--   | Syntax.node _ _ _  => atom { stx }
+--   | _ => unreachable!
 
-def ofString (s : String) : CoreM Proof := do
-  match Parser.runParserCategory (← getEnv) `tactic s with
-  | .ok stx => pure (ofSyntax stx)
-  | .error _ => throwError "failed to parse tactic string"
+-- def ofString (s : String) : CoreM Proof := do
+--   match Parser.runParserCategory (← getEnv) `tactic s with
+--   | .ok stx => pure (ofSyntax stx)
+--   | .error _ => throwError "failed to parse tactic string"
 
 partial def ofInfoTree (tree : InfoTree) : Option Proof :=
   match tree with
-  | .node (.ofTacticInfo { stx .. }) children =>
-    match stx with
+  | .node (.ofTacticInfo info) children =>
+    let step := .ofTacticInfo info
+    match info.stx with
     | Syntax.node _ ``Lean.Parser.Term.byTactic _
     | Syntax.node _ ``Lean.Parser.Tactic.tacticSeq _
     | Syntax.atom _ "by" =>
       match children.toList with
       | [t] => ofInfoTree t
       | _ => none -- malformed: should have exactly one child
     | Syntax.node _ ``Lean.Parser.Tactic.tacticSeq1Indented _ =>
-      -- TODO extract goal information
-      .some (.tacticSeq { stx } (children.toList.filterMap ofInfoTree).toArray)
+      .some (.tacticSeq step (children.toList.filterMap ofInfoTree).toArray)
     | Syntax.node _ ``_root_.cdot _ =>
       match children.toList with
       | [_, c] =>
         match ofInfoTree c with
-        | some p => .some (.cdot { stx } p)
+        | some p => .some (.cdot step p)
         | none => none
       | _ => none
-    | _ => .some (.atom { stx })
+    | _ => .some (.atom step)
   | _ => none
 
-partial def ppRaw (p : Proof) : String :=
-  match p with
-  | atom d => ".raw: " ++ toString d.stx
-  | tacticSeq _ ps => ".tacticSeq\n" ++ (ps.map ppRaw).foldl (· ++ "\n  " ++ ·) "  "
-  | cdot _ p => ".cdot\n" ++ ppRaw p
+-- partial def ppRaw (p : Proof) : String :=
+--   match p with
+--   | atom d => ".raw: " ++ toString d.stx
+--   | tacticSeq _ ps => ".tacticSeq\n" ++ (ps.map ppRaw).foldl (· ++ "\n  " ++ ·) "  "
+--   | cdot _ p => ".cdot\n" ++ ppRaw p
 
 partial def pp (p : Proof) : String :=
   match p with

test/Mathlib/test/20240209.expected.out

@@ -16,5 +16,5 @@
    "pos": {"line": 0, "column": 0},
    "endPos": {"line": 0, "column": 0},
    "data": "unsolved goals\n⊢ False"}],
- "goals": []}
+ "goalsBefore": []}
 

test/Mathlib/test/exact.expected.out

@@ -18,7 +18,7 @@
    "pos": {"line": 0, "column": 0},
    "endPos": {"line": 0, "column": 0},
    "data": "Try this: exact Nat.zero_lt_one"}],
- "goals": []}
+ "goalsBefore": []}
 
 {"sorries":
  [{"proofState": 2,

test/Mathlib/test/induction.expected.out

@@ -18,12 +18,12 @@
   "case succ\nn✝ : ℕ\nn_ih✝ : n✝ = n✝\n⊢ Nat.succ n✝ = Nat.succ n✝"]}
 
 {"proofState": 2,
- "goals": ["case succ\nn✝ : ℕ\nn_ih✝ : n✝ = n✝\n⊢ Nat.succ n✝ = Nat.succ n✝"]}
+ "goalsBefore": ["case succ\nn✝ : ℕ\nn_ih✝ : n✝ = n✝\n⊢ Nat.succ n✝ = Nat.succ n✝"]}
 
 {"sorries":
  [{"proofState": 3, "goal": "case zero\n⊢ Nat.zero = Nat.zero"},
   {"proofState": 4,
    "goal": "case succ\nx : ℕ\nn_ih✝ : x = x\n⊢ Nat.succ x = Nat.succ x"}],
  "proofState": 5,
- "goals": []}
+ "goalsBefore": []}
 

test/Mathlib/test/pickle.expected.out

@@ -12,5 +12,5 @@
    "data": "declaration uses 'sorry'"}],
  "env": 1}
 
-{"proofState": 1, "goals": ["x : ℕ\nh : 2 * (2 * (2 * (2 * x))) = 48\n⊢ x = 3"]}
+{"proofState": 1, "goalsBefore": ["x : ℕ\nh : 2 * (2 * (2 * (2 * x))) = 48\n⊢ x = 3"]}
 

test/Mathlib/test/pickle_2.expected.out

@@ -1,4 +1,4 @@
-{"proofState": 0, "goals": ["x : ℕ\nh : 2 * (2 * (2 * (2 * x))) = 48\n⊢ x = 3"]}
+{"proofState": 0, "goalsBefore": ["x : ℕ\nh : 2 * (2 * (2 * (2 * x))) = 48\n⊢ x = 3"]}
 
-{"proofState": 1, "goals": ["x : ℕ\nh : 2 * (2 * (2 * (2 * x))) = 48\n⊢ x = 3"]}
+{"proofState": 1, "goalsBefore": ["x : ℕ\nh : 2 * (2 * (2 * (2 * x))) = 48\n⊢ x = 3"]}
 

test/all_tactics.expected.out

@@ -3,12 +3,12 @@
    [{"tactic": "have t := 37",
      "proofState": 0,
      "pos": {"line": 1, "column": 18},
-     "goals": "⊢ Nat",
+     "goalsBefore": "⊢ Nat",
      "endPos": {"line": 1, "column": 30}},
     {"tactic": "exact t",
      "proofState": 1,
      "pos": {"line": 1, "column": 32},
-     "goals": "t : Nat\n⊢ Nat",
+     "goalsBefore": "t : Nat\n⊢ Nat",
      "endPos": {"line": 1, "column": 39}}],
    "source": "def f : Nat := by have t := 37; exact t",
    "env": 0}]}

test/by_cases.expected.out

@@ -3,7 +3,7 @@
    "sorries":
    [{"proofState": 0,
      "pos": {"line": 1, "column": 36},
-     "goals": "x : Int\n⊢ x = x",
+     "goalsBefore": "x : Int\n⊢ x = x",
      "endPos": {"line": 1, "column": 41}}],
    "messages":
    [{"severity": "warning",
@@ -13,15 +13,15 @@
    "env": 0}]}
 
 {"proofState": 1,
- "goals":
+ "goalsAfter":
  ["case pos\nx : Int\nh : x < 0\n⊢ x = x",
   "case neg\nx : Int\nh : ¬x < 0\n⊢ x = x"]}
 
-{"proofState": 2, "goals": ["case neg\nx : Int\nh : ¬x < 0\n⊢ x = x"]}
+{"proofState": 2, "goalsAfter": ["case neg\nx : Int\nh : ¬x < 0\n⊢ x = x"]}
 
 {"sorries":
- [{"proofState": 3, "goals": "case pos\nx : Int\nh : x < 0\n⊢ x = x"},
-  {"proofState": 4, "goals": "case neg\nx : Int\nh : ¬x < 0\n⊢ x = x"}],
+ [{"proofState": 3, "goalsBefore": "case pos\nx : Int\nh : x < 0\n⊢ x = x"},
+  {"proofState": 4, "goalsBefore": "case neg\nx : Int\nh : ¬x < 0\n⊢ x = x"}],
  "proofState": 5,
- "goals": []}
+ "goalsAfter": []}
 

test/calc.expected.out

@@ -3,28 +3,28 @@
    [{"tactic": "calc\n  3 = 4 := by sorry\n  4 = 5 := by sorry",
      "proofState": 2,
      "pos": {"line": 1, "column": 22},
-     "goals": "⊢ 3 = 5",
+     "goalsBefore": "⊢ 3 = 5",
      "endPos": {"line": 3, "column": 19}},
     {"tactic": "sorry",
      "proofState": 3,
      "pos": {"line": 2, "column": 14},
-     "goals": "⊢ 3 = 4",
+     "goalsBefore": "⊢ 3 = 4",
      "endPos": {"line": 2, "column": 19}},
     {"tactic": "sorry",
      "proofState": 4,
      "pos": {"line": 3, "column": 14},
-     "goals": "⊢ 4 = 5",
+     "goalsBefore": "⊢ 4 = 5",
      "endPos": {"line": 3, "column": 19}}],
    "source":
    "example : 3 = 5 := by\n  calc\n    3 = 4 := by sorry\n    4 = 5 := by sorry",
    "sorries":
    [{"proofState": 0,
      "pos": {"line": 2, "column": 14},
-     "goals": "⊢ 3 = 4",
+     "goalsBefore": "⊢ 3 = 4",
      "endPos": {"line": 2, "column": 19}},
     {"proofState": 1,
      "pos": {"line": 3, "column": 14},
-     "goals": "⊢ 4 = 5",
+     "goalsBefore": "⊢ 4 = 5",
      "endPos": {"line": 3, "column": 19}}],
    "messages":
    [{"severity": "warning",