Merge pull request 'chore: Code cleanup' (#164) from chore/cleanup into dev

Reviewed-on: #164

Main.lean

@@ -10,23 +10,26 @@ 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.trim.get? 0 with
-  match s.get? 0 with
+  | .some '{' =>
-  | .some '{' => -- Parse in Json mode
+    -- 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
+partial def loop : MainM Unit := do repeat do
   let state ← get
   let command ← (← IO.getStdin).getLine
-  if command.trim.length = 0 then return ()
+  -- Halt the program if empty line is given
+  if command.trim.length = 0 then break
   match parseCommand command with
   | .error error =>
     let error  := Lean.toJson ({ error := "command", desc := error }: InteractionError)
@@ -43,25 +46,21 @@ partial def loop : MainM Unit := do
       let message ← e.toMessageData.toString
       let error  := Lean.toJson ({ error := "main", desc := message }: InteractionError)
       IO.println error.compress
-  loop
 
 
 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)
+  -- Separate imports and options
-    |>.toArray |> Pantograph.createCoreContext
+  let (options, imports) := args.partition (·.startsWith "--")
-  let imports:= args.filter (λ s => ¬ (s.startsWith "--"))
+  let coreContext ← options.map (·.drop 2) |>.toArray |> Pantograph.createCoreContext
   let coreState ← Pantograph.createCoreState imports.toArray
-  let context: Context := {
+  let context: Context := {}
-    imports
-  }
   try
     let coreM := loop.run context |>.run' {}
     IO.println "ready."

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
@@ -13,7 +12,9 @@ structure State where
   goalStates: Std.HashMap Nat GoalState := Std.HashMap.empty
 
 /-- Main state monad for executing commands -/
-abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
+abbrev MainM := ReaderT Context $ StateRefT State Lean.CoreM
+/-- Fallible subroutine return type -/
+abbrev CR α := Except Protocol.InteractionError α
 
 def newGoalState (goalState: GoalState) : MainM Nat := do
   let state ← get
@@ -25,10 +26,6 @@ def newGoalState (goalState: GoalState) : MainM Nat := do
   return stateId
 
 
--- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables
--- certain monadic features in `MainM`
-abbrev CR α := Except Protocol.InteractionError α
-
 def runMetaInMainM { α } (metaM: Lean.MetaM α): MainM α :=
   metaM.run'
 def runTermElabInMainM { α } (termElabM: Lean.Elab.TermElabM α) : MainM α :=

Test/Environment.lean

@@ -110,7 +110,7 @@ def test_symbol_location : TestT IO Unit := do
     checkTrue "file" result.sourceUri?.isNone
     checkEq "pos" (result.sourceStart?.map (·.column)) <| .some 0
     checkEq "pos" (result.sourceEnd?.map (·.column)) <| .some 88
-    let .ok { imports, constNames, extraConstNames } ← Environment.moduleRead ⟨"Init.Data.Nat.Basic"⟩ | fail "Module read failed"
+    let .ok { imports, constNames, .. } ← Environment.moduleRead ⟨"Init.Data.Nat.Basic"⟩ | fail "Module read failed"
     checkEq "imports" imports #["Init.SimpLemmas", "Init.Data.NeZero"]
     checkTrue "constNames" $ constNames.contains "Nat.succ_add"
 

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 := {
+  let context: Context := {}
-    imports := ["Init"]
-  }
   let commands: MainM LSpec.TestSeq :=
     steps.foldlM (λ suite step => do
       let result ← step

Test/Proofs.lean

@@ -750,8 +750,6 @@ def test_tactic_failure_synthesize_placeholder : TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
 
-  let iex : InternalExceptionId := { idx := 4 }
-  IO.println s!"{← iex.getName}"
   let tactic := "simpa [h] using And.imp_left h _"
   --let state2 ← match ← state1.tacticOn 0 tactic with
   --  | .success state => pure state