From 787c9e606d30ef78ee2b0786db3d87e8576df242 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 24 Jan 2025 19:22:58 -0800
Subject: [PATCH] chore: Cleanup REPL loop

---
 Main.lean             | 24 ++++++++++++------------
 Repl.lean             |  1 -
 Test/Integration.lean |  4 +---
 3 files changed, 13 insertions(+), 16 deletions(-)

diff --git a/Main.lean b/Main.lean
index b20724d..c4d30c6 100644
--- a/Main.lean
+++ b/Main.lean
@@ -10,22 +10,25 @@ open Pantograph.Protocol
 
 /-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
 def parseCommand (s: String): Except String Command := do
-  let s := s.trim
-  match s.get? 0 with
-  | .some '{' => -- Parse in Json mode
+  match s.trim.get? 0 with
+  | .some '{' =>
+    -- Parse in Json mode
     Lean.fromJson? (← Lean.Json.parse s)
-  | .some _ => -- Parse in line mode
+  | .some _ =>
+    -- Parse in line mode
     let offset := s.posOf ' ' |> s.offsetOfPos
     if offset = s.length then
       return { cmd := s.take offset, payload := Lean.Json.null }
     else
       let payload ← s.drop offset |> Lean.Json.parse
       return { cmd := s.take offset, payload := payload }
-  | .none => throw "Command is empty"
+  | .none =>
+    throw "Command is empty"
 
 partial def loop : MainM Unit := do repeat do
   let state ← get
   let command ← (← IO.getStdin).getLine
+  -- Halt the program if empty line is given
   if command.trim.length = 0 then break
   match parseCommand command with
   | .error error =>
@@ -47,20 +50,17 @@ partial def loop : MainM Unit := do repeat do
 
 unsafe def main (args: List String): IO Unit := do
   -- NOTE: A more sophisticated scheme of command line argument handling is needed.
-  -- Separate imports and options
   if args == ["--version"] then do
     IO.println s!"{Pantograph.version}"
     return
 
   Pantograph.initSearch ""
 
-  let coreContext ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none)
-    |>.toArray |> Pantograph.createCoreContext
-  let imports:= args.filter (λ s => ¬ (s.startsWith "--"))
+  -- Separate imports and options
+  let (options, imports) := args.partition (·.startsWith "--")
+  let coreContext ← options.map (·.drop 2) |>.toArray |> Pantograph.createCoreContext
   let coreState ← Pantograph.createCoreState imports.toArray
-  let context: Context := {
-    imports
-  }
+  let context: Context := {}
   try
     let coreM := loop.run context |>.run' {}
     IO.println "ready."
diff --git a/Repl.lean b/Repl.lean
index 083edd1..ddf3201 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -4,7 +4,6 @@ import Pantograph
 namespace Pantograph.Repl
 
 structure Context where
-  imports: List String
 
 /-- Stores state of the REPL -/
 structure State where
diff --git a/Test/Integration.lean b/Test/Integration.lean
index 7864515..9815954 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -235,9 +235,7 @@ def test_frontend_process_sorry : Test :=
 
 def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do
   -- Setup the environment for execution
-  let context: Context := {
-    imports := ["Init"]
-  }
+  let context: Context := {}
   let commands: MainM LSpec.TestSeq :=
     steps.foldlM (λ suite step => do
       let result ← step