merge file_mode

Author: kim-em

README.md

@@ -92,6 +92,34 @@ However, if the first `def f` command returned `{"env" : 1}`, then we can use
 ```
 and then the second invocation of `expensive_tactic` will be fast again.
 
+## File mode
+
+There is a simple wrapper around command mode that allows reading in an entire file.
+
+If `test/file.lean` contains
+```lean
+def f : Nat := 37
+
+def g := 2
+
+theorem h : f + g = 39 := by exact rfl
+```
+
+then
+```
+echo '{"path": "test/file.lean", "allTactics": true}' | lake exe repl
+```
+results in output
+```json
+{"tactics":
+ [{"tactic": "exact rfl",
+   "proofState": 0,
+   "pos": {"line": 5, "column": 29},
+   "goals": "⊢ f + g = 39",
+   "endPos": {"line": 5, "column": 38}}],
+ "env": 0}
+ ```
+
 ## Tactic mode (experimental)
 
 To enter tactic mode issue a command containing a `sorry`,

REPL/JSON.lean

@@ -11,22 +11,29 @@ open Lean Elab InfoTree
 
 namespace REPL
 
+structure CommandOptions where
+  allTactics : 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`.
 -/
-structure Command where
+structure Command extends CommandOptions where
   env : Option Nat
   incr : Option Nat
   cmd : String
-  allTactics : Option Bool := none
-  /--
-  Should be "full", "tactics", "original", or "substantive".
-  Anything else is ignored.
-  -/
-  infotree : Option String
 deriving ToJson, FromJson
 
+/-- Process a Lean file in a fresh environment. -/
+structure File extends CommandOptions where
+  path : System.FilePath
+deriving FromJson
+
 /--
 Run a tactic in a proof state.
 -/

REPL/Main.lean

@@ -252,6 +252,13 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
       tactics
       infotree }
 
+def processFile (s : File) : M IO (CommandResponse ⊕ Error) := do
+  try
+    let cmd ← IO.FS.readFile s.path
+    runCommand { s with env := none, cmd }
+  catch e =>
+    pure <| .inr ⟨e.toString⟩
+
 /--
 Run a single tactic, returning the id of the new proof statement, and the new goals.
 -/
@@ -286,6 +293,7 @@ instance [ToJson α] [ToJson β] : ToJson (α ⊕ β) where
 /-- Commands accepted by the REPL. -/
 inductive Input
 | command : REPL.Command → Input
+| file : REPL.File → Input
 | proofStep : REPL.ProofStep → Input
 | pickleEnvironment : REPL.PickleEnvironment → Input
 | unpickleEnvironment : REPL.UnpickleEnvironment → Input
@@ -310,6 +318,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 _ => match fromJson? j with
+    | .ok (r : REPL.File) => return .file r
     | .error e => throw <| IO.userError <| toString <| toJson <|
         (⟨"Could not parse as a valid JSON command:\n" ++ e⟩ : Error)
 
@@ -323,6 +333,7 @@ where loop : M IO Unit := do
   if query.startsWith "#" || query.startsWith "--" then loop else
   IO.println <| toString <| ← match ← parse query with
   | .command r => return toJson (← runCommand r)
+  | .file r => return toJson (← processFile r)
   | .proofStep r => return toJson (← runProofStep r)
   | .pickleEnvironment r => return toJson (← pickleCommandSnapshot r)
   | .unpickleEnvironment r => return toJson (← unpickleCommandSnapshot r)

test/file.expected.out

@@ -0,0 +1,8 @@
+{"tactics":
+ [{"tactic": "exact rfl",
+   "proofState": 0,
+   "pos": {"line": 5, "column": 29},
+   "goals": "⊢ f + g = 39",
+   "endPos": {"line": 5, "column": 38}}],
+ "env": 0}
+

test/file.in

@@ -0,0 +1 @@
+{"path": "test/file.lean", "allTactics": true}

test/file.lean

@@ -0,0 +1,5 @@
+def f : Nat := 37
+
+def g := 2
+
+theorem h : f + g = 39 := by exact rfl