Merge pull request #10 from leanprover-community/snapshots

feat: tactic mode

README.md

@@ -1,8 +1,15 @@
 # A read-eval-print-loop for Lean 4
 
-Run using `./run`.
+Run using `lake exe repl`.
 Communicates via JSON on stdin and stdout.
 Commands should be separated by blank lines.
+
+The REPL works both in "command" mode and "tactic" mode.
+
+## Command mode
+
+In command mode, you send complete commands (e.g. declarations) to the REPL.
+
 Commands may be of the form
 
 ```json
@@ -23,13 +30,22 @@ You can only use `import` commands when you do not specify the `env` field.
 
 You can backtrack simply by using earlier values for `env`.
 
-The results are of the form
+The response includes:
+* A numeric label for the `Environment` after your command,
+  which you can use as the starting point for subsequent commands.
+* Any messages generated while processing your command.
+* A list of the `sorry`s in your command, including
+  * their expected type, and
+  * a numeric label for the proof state at the `sorry`, which you can then use in tactic mode.
+
+Example output:
 
 ```json
 {"sorries":
  [{"pos": {"line": 1, "column": 18},
    "endPos": {"line": 1, "column": 23},
-   "goal": "⊢ Nat"}],
+   "goal": "⊢ Nat",
+   "proofState": 0}],
  "messages":
  [{"severity": "error",
    "pos": {"line": 1, "column": 23},
@@ -39,7 +55,43 @@ The results are of the form
  "env": 6}
 ```
 
-showing any messages generated, or sorries with their goal states.
+showing any messages generated, and sorries with their goal states.
+
+## Tactic mode (experimental)
+
+The only way to enter tactic mode at present is to first issue a command containing a `sorry`,
+and then using the `proofState` index returned for each `sorry`.
+
+Example usage:
+```json
+{"cmd" : "def f : Nat := by sorry"}
+
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 18},
+   "goal": "⊢ Nat",
+   "endPos": {"line": 1, "column": 23}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 5},
+   "data": "declaration uses 'sorry'"}],
+ "env": 0}
+
+{"tactic": "apply Int.natAbs", "proofState": 0}
+
+{"proofState": 1, "goals": ["⊢ Int"]}
+
+{"tactic": "exact -37", "proofState": 1}
+
+{"proofState": 2, "goals": []}
+```
+
+At present there is nothing you can do with a completed proof state:
+we would like to extend this so that you can replace the original `sorry` with your tactic script,
+and obtain the resulting `Environment`
+
+## Future work
 
-Information is generated for tactic mode sorries,
-but currently not for term mode sorries.
+* Replay tactic scripts from tactic mode back into the original `sorry`.
+* Serialization and deserialization of environments and proof states

REPL/InfoTree.lean

@@ -6,9 +6,7 @@ Authors: Scott Morrison
 import Lean
 
 /-!
-# Code to move (eventually) to core.
-
-Mostly additional functions to deal with `InfoTree`.
+Additional functions to deal with `InfoTree`.
 -/
 
 open Lean Elab Meta

REPL/JSON.lean

@@ -6,8 +6,6 @@ Authors: Scott Morrison
 import Lean.Data.Json
 import Lean.Message
 import Lean.Elab.InfoTree.Main
-import REPL.Lean.ContextInfo
-import REPL.InfoTree
 
 open Lean Elab InfoTree
 
@@ -17,11 +15,19 @@ namespace REPL
 If `env = none`, starts a new session (in which you can use `import`).
 If `env = some n`, builds on the existing environment `n`.
 -/
-structure Run where
+structure Command where
   env : Option Nat
   cmd : String
 deriving ToJson, FromJson
 
+/--
+Run a tactic in a proof state.
+-/
+structure ProofStep where
+  proofState : Nat
+  tactic : String
+deriving ToJson, FromJson
+
 /-- Line and column information for error messages and sorries. -/
 structure Pos where
   line : Nat
@@ -56,28 +62,39 @@ structure Sorry where
   pos : Pos
   endPos : Pos
   goal : String
+  /--
+  The index of the proof state at the sorry.
+  You can use the `ProofStep` instruction to run a tactic at this state.
+  -/
+  proofState : Option Nat
 deriving ToJson, FromJson
 
 /-- Construct the JSON representation of a Lean sorry. -/
-def Sorry.of (ctx : ContextInfo) (g : SorryType) (pos endPos : Lean.Position) :
-    IO Sorry := do pure <|
+def Sorry.of (goal : String) (pos endPos : Lean.Position) (proofState : Option Nat) : Sorry :=
   { pos := ⟨pos.line, pos.column⟩,
     endPos := ⟨endPos.line, endPos.column⟩,
-    goal := ← match g with
-    | SorryType.tactic g => do pure s!"{(← ctx.ppGoals [g])}".trim
-    | SorryType.term _ none => unreachable!
-    | SorryType.term lctx (some t) => do pure s!"⊢ {← ctx.ppExpr lctx t}" }
+    goal,
+    proofState }
 
 /--
 A response to a Lean command.
 `env` can be used in later calls, to build on the stored environment.
 -/
-structure Response where
+structure CommandResponse where
   env : Nat
   messages : List Message
   sorries : List Sorry
 deriving ToJson, FromJson
 
+/--
+A response to a Lean tactic.
+`proofState` can be used in later calls, to run further tactics.
+-/
+structure ProofStepResponse where
+  proofState : Nat
+  goals : List String
+deriving ToJson, FromJson
+
 /-- Json wrapper for an error. -/
 structure Error where
   message : String

REPL/Main.lean

@@ -8,6 +8,8 @@ import REPL.Frontend
 import REPL.InfoTree
 import REPL.Util.Path
 import REPL.Util.TermUnsafe
+import REPL.Lean.ContextInfo
+import REPL.InfoTree
 
 /-!
 # A REPL for Lean.
@@ -55,30 +57,165 @@ open Lean Elab
 
 namespace REPL
 
+/--
+Bundled structure for the `State` and `Context` objects
+for the `CoreM`, `MetaM`, `TermElabM`, and `TacticM` monads.
+-/
+structure ProofState where
+  coreState     : Core.State
+  coreContext   : Core.Context
+  metaState     : Meta.State
+  metaContext   : Meta.Context
+  termState     : Term.State
+  termContext   : Term.Context
+  tacticState   : Tactic.State
+  tacticContext : Tactic.Context
+namespace ProofState
+
+open Lean Elab Tactic
+
+/-- Run a `CoreM` monadic function in the current `ProofState`, updating the `Core.State`. -/
+def runCoreM (p : ProofState) (t : CoreM α) : IO (α × ProofState) := do
+  let (a, coreState) ← (Lean.Core.CoreM.toIO · p.coreContext p.coreState) do t
+  return (a, { p with coreState })
+
+/-- Run a `MetaM` monadic function in the current `ProofState`, updating the `Meta.State`. -/
+def runMetaM (p : ProofState) (t : MetaM α) : IO (α × ProofState) := do
+  let ((a, metaState), p') ← p.runCoreM (Lean.Meta.MetaM.run (ctx := p.metaContext) (s := p.metaState) do t)
+  return (a, { p' with metaState })
+
+/-- Run a `TermElabM` monadic function in the current `ProofState`, updating the `Term.State`. -/
+def runTermElabM (p : ProofState) (t : TermElabM α) : IO (α × ProofState) := do
+  let ((a, termState), p') ← p.runMetaM (Lean.Elab.Term.TermElabM.run (s := p.termState) do t)
+  return (a, { p' with termState })
+
+/-- Run a `TacticM` monadic function in the current `ProofState`, updating the `Tactic.State`. -/
+def runTacticM (p : ProofState) (t : TacticM α) : IO (α × ProofState) := do
+  let ((a, tacticState), p') ← p.runTermElabM (t p.tacticContext |>.run p.tacticState)
+  return (a, { p' with tacticState })
+
+/--
+Run a `TacticM` monadic function in the current `ProofState`, updating the `Tactic.State`,
+and discarding the return value.
+-/
+def runTacticM' (p : ProofState) (t : TacticM α) : IO ProofState :=
+  Prod.snd <$> p.runTacticM t
+
+/--
+Evaluate a `Syntax` into a `TacticM` tactic, and run it in the current `ProofState`.
+-/
+def runSyntax (p : ProofState) (t : Syntax) : IO ProofState :=
+  Prod.snd <$> p.runTacticM (evalTactic t)
+
+/--
+Parse a string into a `Syntax`, evaluate it as a `TacticM` tactic,
+and run it in the current `ProofState`.
+-/
+def runString (p : ProofState) (t : String) : IO ProofState :=
+  match Parser.runParserCategory p.coreState.env `tactic t with
+  | .error e => throw (IO.userError e)
+  | .ok stx => p.runSyntax stx
+
+/-- Pretty print the current goals in the `ProofState`. -/
+def ppGoals (p : ProofState) : IO (List Format) :=
+  Prod.fst <$> p.runTacticM do (← getGoals).mapM (Meta.ppGoal ·)
+
+end ProofState
+
 /-- The monadic state for the Lean REPL. -/
 structure State where
-  environments : Array Environment
-  lines : Array Nat
+  /--
+  Environment snapshots after complete declarations.
+  The user can run a declaration in a given environment using `{"cmd": "def f := 37", "env": 17}`.
+  -/
+  environments : Array Environment := #[]
+  /--
+  Proof states after individual tactics.
+  The user can run a tactic in a given proof state using `{"tactic": "exact 42", "proofState": 5}`.
+  Declarations with containing `sorry` record a proof state at each sorry,
+  and report the numerical index for the recorded state at each sorry.
+  -/
+  proofStates : Array ProofState := #[]
+
+/--
+The Lean REPL monad.
 
-/-- The Lean REPL monad. -/
+We only use this with `m := IO`, but it is set up as a monad transformer for flexibility.
+-/
 abbrev M (m : Type → Type) := StateT State m
 
 variable [Monad m] [MonadLiftT IO m]
 
-/-- Get the next available id for a new environment. -/
-def nextId : M m Nat := do pure (← get).environments.size
+/-- Record an `Environment` into the REPL state, returning its index for future use. -/
+def recordEnvironment (env : Environment) : M m Nat := do
+  let id := (← get).environments.size
+  modify fun s => { s with environments := s.environments.push env }
+  return id
+
+/-- Record a `ProofState` into the REPL state, returning its index for future use. -/
+def recordProofState (proofState : ProofState) : M m Nat := do
+  let id := (← get).proofStates.size
+  modify fun s => { s with proofStates := s.proofStates.push proofState }
+  return id
+
+/--
+Construct a `ProofState` from a `ContextInfo` and optional `LocalContext`, and a list of goals.
 
-/-- Run a command, returning the id of the new environment, and any messages and sorries. -/
-def run (s : Run) : M m Response := do
-  let env? := s.env.bind ((← get).environments[·]?)
+For convenience, we also allow a list of `Expr`s, and these are appended to the goals
+as fresh metavariables with the given types.
+-/
+def createProofState (ctx : ContextInfo) (lctx? : Option LocalContext)
+    (goals : List MVarId) (types : List Expr := []) : IO ProofState := do
+  ctx.runMetaM (lctx?.getD {}) do
+    let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t))
+    pure <|
+    { coreState := ← getThe Core.State
+      coreContext := ← readThe Core.Context
+      metaState := ← getThe Meta.State
+      metaContext := ← readThe Meta.Context
+      termState := {}
+      termContext := {}
+      tacticState := { goals }
+      tacticContext := { elaborator := .anonymous } }
+
+/--
+Run a command, returning the id of the new environment, and any messages and sorries.
+-/
+def runCommand (s : Command) : M m (CommandResponse ⊕ Error) := do
+  let (env?, notFound) ← do match s.env with
+  | none => pure (none, false)
+  | some i => do match (← get).environments[i]? with
+    | some env => pure (some env, false)
+    | none => pure (none, true)
+  if notFound then
+    return .inr ⟨"Unknown environment."⟩
   let (env, messages, trees) ← IO.processInput s.cmd env? {} ""
   let messages ← messages.mapM fun m => Message.of m
   let sorries ← trees.bind InfoTree.sorries |>.mapM
-    fun ⟨ctx, g, pos, endPos⟩ => Sorry.of ctx g pos endPos
-  let lines := s.cmd.splitOn "\n" |>.length
-  let id ← nextId
-  modify fun s => { environments := s.environments.push env, lines := s.lines.push lines }
-  pure ⟨id, messages, sorries⟩
+    fun ⟨ctx, g, pos, endPos⟩ => do
+      let (goal, proofState) ← match g with
+      | .tactic g => do
+         pure (s!"{(← ctx.ppGoals [g])}".trim, some (← createProofState ctx none [g]))
+      | .term lctx (some t) => do
+         pure (s!"⊢ {← ctx.ppExpr lctx t}", some (← createProofState ctx lctx [] [t]))
+      | .term _ none => unreachable!
+      let proofStateId ← proofState.mapM recordProofState
+      return Sorry.of goal pos endPos proofStateId
+  let id ← recordEnvironment env
+  return .inl ⟨id, messages, sorries⟩
+
+/--
+Run a single tactic, returning the id of the new proof statement, and the new goals.
+-/
+-- TODO return messages?
+-- TODO detect sorries?
+def runProofStep (s : ProofStep) : M m (ProofStepResponse ⊕ Error) := do
+  match (← get).proofStates[s.proofState]? with
+  | none => return .inr ⟨"Unknown proof state."⟩
+  | some proofState =>
+    let proofState' ← proofState.runString s.tactic
+    let id ← recordProofState proofState'
+    return .inl { proofState := id, goals := (← proofState'.ppGoals).map fun s => s!"{s}" }
 
 end REPL
 
@@ -91,9 +228,14 @@ partial def getLines : IO String := do
   | "\n" => pure "\n"
   | line => pure <| line ++ (← getLines)
 
+instance [ToJson α] [ToJson β] : ToJson (α ⊕ β) where
+  toJson x := match x with
+  | .inl a => toJson a
+  | .inr b => toJson b
+
 /-- Read-eval-print loop for Lean. -/
 partial def repl : IO Unit :=
-  StateT.run' loop ⟨#[], #[]⟩
+  StateT.run' loop {}
 where loop : M IO Unit := do
   let query ← getLines
   if query = "" then
@@ -102,11 +244,13 @@ where loop : M IO Unit := do
   match json with
   | .error e => IO.println <| toString <| toJson (⟨e⟩ : Error)
   | .ok j => match fromJson? j with
-    | .error e => IO.println <| toString <| toJson (⟨e⟩ : Error)
-    | .ok (r : Run) => IO.println <| toString <| toJson (← run r)
+    | .ok (r : REPL.ProofStep) => IO.println <| toString <| toJson (← runProofStep r)
+    | .error _ => match fromJson? j with
+      | .ok (r : REPL.Command) => IO.println <| toString <| toJson (← runCommand r)
+      | .error e => IO.println <| toString <| toJson (⟨e⟩ : Error)
   loop
 
-/-- Main executable function, run as `lake env lean --run Mathlib/Util/REPL.lean`. -/
+/-- Main executable function, run as `lake exe repl`. -/
 def main (_ : List String) : IO Unit := do
   searchPathRef.set compile_time_search_path%
   repl