make repl more extensible

REPL/Actions.lean

@@ -0,0 +1,4 @@
+import REPL.Actions.Basic
+import REPL.Actions.Tactic
+import REPL.Actions.Command
+import REPL.Actions.File

REPL/Actions/Basic.lean

@@ -0,0 +1,109 @@
+import REPL.Basic
+import REPL.Frontend
+import REPL.Util.Path
+import REPL.Lean.ContextInfo
+import REPL.Lean.Environment
+import REPL.Lean.InfoTree
+import REPL.Lean.InfoTree.ToJson
+import REPL.Snapshots
+
+open Lean Elab InfoTree
+
+namespace REPL.Actions
+
+/-- Line and column information for error messages and sorries. -/
+structure Pos where
+  line : Nat
+  column : Nat
+deriving ToJson, FromJson
+
+/-- Severity of a message. -/
+inductive Severity
+  | trace | info | warning | error
+deriving ToJson, FromJson
+
+/-- A Lean message. -/
+structure Message where
+  pos : Pos
+  endPos : Option Pos
+  severity : Severity
+  data : String
+deriving ToJson, FromJson
+
+/-- Construct the JSON representation of a Lean message. -/
+def Message.of (m : Lean.Message) : IO Message := do pure <|
+  { pos := ⟨m.pos.line, m.pos.column⟩,
+    endPos := m.endPos.map fun p => ⟨p.line, p.column⟩,
+    severity := match m.severity with
+    | .information => .info
+    | .warning => .warning
+    | .error => .error,
+    data := (← m.data.toString).trim }
+
+/-- A Lean `sorry`. -/
+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 FromJson
+
+instance : ToJson Sorry where
+  toJson r := Json.mkObj <| .flatten [
+    [("goal", r.goal)],
+    [("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 :=
+  { pos := ⟨pos.line, pos.column⟩,
+    endPos := ⟨endPos.line, endPos.column⟩,
+    goal,
+    proofState }
+
+def Json.nonemptyList [ToJson α] (k : String) : List α → List (String × Json)
+  | [] => []
+  | l  => [⟨k, toJson l⟩]
+
+/-- Json wrapper for an error. -/
+structure Error where
+  message : String
+deriving ToJson, FromJson
+
+abbrev ResultT (m : Type → Type) (α : Type) := ExceptT Error m α
+
+def collectFVarsAux : Expr → NameSet
+  | .fvar fvarId => NameSet.empty.insert fvarId.name
+  | .app fm arg => (collectFVarsAux fm).union $ collectFVarsAux arg
+  | .lam _ binderType body _ => (collectFVarsAux binderType).union $ collectFVarsAux body
+  | .forallE _ binderType body _ => (collectFVarsAux binderType).union $ collectFVarsAux body
+  | .letE _ type value body _ => ((collectFVarsAux type).union $ collectFVarsAux value).union $ collectFVarsAux body
+  | .mdata _ expr => collectFVarsAux expr
+  | .proj _ _ struct => collectFVarsAux struct
+  | _ => NameSet.empty
+
+/-- Collect all fvars in the expression, and return their names. -/
+def collectFVars (e : Expr) : MetaM (Array Expr) := do
+  let names := collectFVarsAux e
+  let mut fvars := #[]
+  for ldecl in ← getLCtx do
+    if ldecl.isImplementationDetail then
+      continue
+    if names.contains ldecl.fvarId.name then
+      fvars := fvars.push $ .fvar ldecl.fvarId
+  return fvars
+
+def abstractAllLambdaFVars (e : Expr) : MetaM Expr := do
+  let mut e' := e
+  while e'.hasFVar do
+    let fvars ← collectFVars e'
+    if fvars.isEmpty then
+      break
+    e' ← Meta.mkLambdaFVars fvars e'
+  return e'

REPL/Actions/Command.lean

@@ -0,0 +1,130 @@
+import REPL.Basic
+import REPL.Actions.Basic
+import REPL.Actions.Tactic
+import REPL.Frontend
+
+open Lean Elab InfoTree
+
+namespace REPL.Actions
+
+structure CommandOptions where
+  allTactics : Option Bool := none
+  rootGoals : Option Bool := none
+  /--
+  Should be "full", "tactics", "original", or "substantive".
+  Anything else is ignored.
+  -/
+  infotree : Option String
+
+/-- Run Lean commands.
+If `env = none`, starts a new session (in which you can use `import`).
+If `env = some n`, builds on the existing environment `n`.
+-/
+@[repl_request]
+structure Command extends CommandOptions where
+  env : Option Nat
+  cmd : String
+deriving ToJson, FromJson
+
+/--
+A response to a Lean command.
+`env` can be used in later calls, to build on the stored environment.
+-/
+structure CommandResponse where
+  env : Nat
+  messages : List Message := []
+  sorries : List Sorry := []
+  tactics : List Tactic := []
+  infotree : Option Json := none
+deriving FromJson
+
+instance : ToJson CommandResponse where
+  toJson r := Json.mkObj <| .flatten [
+    [("env", r.env)],
+    Json.nonemptyList "messages" r.messages,
+    Json.nonemptyList "sorries" r.sorries,
+    Json.nonemptyList "tactics" r.tactics,
+    match r.infotree with | some j => [("infotree", j)] | none => []
+  ]
+
+@[repl_request]
+structure PickleEnvironment where
+  env : Nat
+  pickleTo : System.FilePath
+deriving ToJson, FromJson
+
+@[repl_request]
+structure UnpickleEnvironment where
+  unpickleEnvFrom : System.FilePath
+deriving ToJson, FromJson
+
+variable [Monad m] [MonadREPL m] [MonadLiftT IO m]
+
+/-- Record an `CommandSnapshot` into the REPL state, returning its index for future use. -/
+@[specialize]
+def recordCommandSnapshot (state : CommandSnapshot) : m Nat := do
+  modifyGetCmdSnaps fun s => (s.size, s.push state)
+
+/--
+Run a command, returning the id of the new environment, and any messages and sorries.
+-/
+@[repl_request_handler Command]
+def runCommand (s : Command) : ResultT M CommandResponse := do
+  let cmdSnapshot? ← s.env.mapM fun i => do
+    let some env := (← get).cmdStates[i]? | throw ⟨"Unknown environment."⟩
+    return env
+  let initialCmdState? := cmdSnapshot?.map fun c => c.cmdState
+  let (initialCmdState, cmdState, messages, trees) ← do
+    try
+      IO.processInput s.cmd initialCmdState?
+    catch ex : IO.Error =>
+      throw ⟨ex.toString⟩
+  let messages ← messages.mapM fun m => Message.of m
+  -- For debugging purposes, sometimes we print out the trees here:
+  -- trees.forM fun t => do IO.println (← t.format)
+  let sorries ← sorries trees initialCmdState.env none
+  let sorries ← match s.rootGoals with
+    | some true => pure (sorries ++ (← collectRootGoalsAsSorries trees initialCmdState.env))
+    | _ => pure sorries
+  let tactics ← match s.allTactics with
+    | some true => tactics trees initialCmdState.env
+    | _ => pure []
+  let cmdSnapshot :=
+    { cmdState
+      cmdContext := (cmdSnapshot?.map fun c => c.cmdContext).getD
+        { fileName := "",
+          fileMap := default,
+          snap? := none,
+          cancelTk? := none } }
+  let env ← recordCommandSnapshot cmdSnapshot
+  let jsonTrees := match s.infotree with
+    | some "full" => trees
+    | some "tactics" => trees.flatMap InfoTree.retainTacticInfo
+    | some "original" => trees.flatMap InfoTree.retainTacticInfo |>.flatMap InfoTree.retainOriginal
+    | some "substantive" => trees.flatMap InfoTree.retainTacticInfo |>.flatMap InfoTree.retainSubstantive
+    | _ => []
+  let infotree ←
+    if jsonTrees.isEmpty then
+      pure none
+    else
+      pure <| some <| Json.arr (← jsonTrees.toArray.mapM fun t => t.toJson none)
+  return show CommandResponse from
+    { env,
+      messages,
+      sorries,
+      tactics
+      infotree }
+
+/-- Pickle a `CommandSnapshot`, generating a JSON response. -/
+@[specialize, repl_request_handler PickleEnvironment]
+def pickleCommandSnapshot (n : PickleEnvironment) : ResultT m CommandResponse := do
+  let some env := (← getCmdSnaps)[n.env]? | throw ⟨"Unknown environment."⟩
+  discard <| env.pickle n.pickleTo
+  return { env := n.env }
+
+/-- Unpickle a `CommandSnapshot`, generating a JSON response. -/
+@[repl_request_handler UnpickleEnvironment]
+def unpickleCommandSnapshot (n : UnpickleEnvironment) : M CommandResponse := do
+  let (env, _) ← CommandSnapshot.unpickle n.unpickleEnvFrom
+  let env ← recordCommandSnapshot env
+  return { env }

REPL/Actions/File.lean

@@ -0,0 +1,22 @@
+import REPL.Basic
+import REPL.Actions.Basic
+import REPL.Actions.Command
+
+open Lean Elab InfoTree
+
+namespace REPL.Actions
+
+/-- Process a Lean file in a fresh environment if `env` is not provided. -/
+@[repl_request]
+structure File extends CommandOptions where
+  env : Option Nat
+  path : System.FilePath
+deriving ToJson, FromJson
+
+@[repl_request_handler File]
+def processFile (s : File) : ResultT M CommandResponse := do
+  try
+    let cmd ← IO.FS.readFile s.path
+    runCommand { s with env := s.env, cmd }
+  catch e : IO.Error =>
+    throw ⟨e.toString⟩