Pantograph/Frontend/Basic.lean

@@ -42,14 +42,6 @@ structure CompilationStep where
   msgs : List Message
   trees : List Elab.InfoTree
 
-namespace CompilationStep
-
-@[export pantograph_frontend_compilation_step_message_strings_m]
-def messageStrings (step: CompilationStep) : IO (Array String) := do
-  List.toArray <$> step.msgs.mapM (·.toString)
-
-end CompilationStep
-
 
 /--
 Process one command, returning a `CompilationStep` and

Pantograph/Protocol.lean

@@ -298,18 +298,11 @@ structure InvokedTactic where
   goalAfter: String
   tactic: String
   deriving Lean.ToJson
-
-structure CompilationUnit where
-  -- String boundaries of compilation units
-  boundary: (Nat × Nat)
-  -- Tactic invocations
-  invocations?: Option (List InvokedTactic) := .none
-  goalStateId?: Option Nat := .none
-  goals: Array Goal := #[]
-  messages: Array String := #[]
-  deriving Lean.ToJson
 structure FrontendProcessResult where
-  units: List CompilationUnit
+  -- String boundaries of compilation units
+  units: List (Nat × Nat)
+  invocations?: Option (List InvokedTactic) := .none
+  goalStates?: Option (List (Nat × Array Goal)) := .none
   deriving Lean.ToJson
 
 abbrev CR α := Except InteractionError α

Repl.lean

@@ -216,36 +216,35 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
           let env ← Lean.MonadEnv.getEnv
           pure <| .some env
       let (context, state) ← do Frontend.createContextStateFromFile file fileName env? {}
-      let frontendM := Frontend.mapCompilationSteps λ step => do
+      let m := Frontend.mapCompilationSteps λ step => do
-        let boundary := (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
+        let unitBoundary := (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
-        let invocations?: Option (List Protocol.InvokedTactic) ← if args.invocations then
+        let tacticInvocations ← if args.invocations then
-            let invocations ← Frontend.collectTacticsFromCompilationStep step
+            Frontend.collectTacticsFromCompilationStep step
-            pure $ .some invocations
           else
-            pure .none
+            pure []
         let sorrys := if args.sorrys then
             Frontend.collectSorrys step
           else
             []
-        let messages ← step.messageStrings
+        return (unitBoundary, tacticInvocations, sorrys)
-        return (boundary, invocations?, sorrys, messages)
+      let li ← m.run context |>.run' state
-      let li ← frontendM.run context |>.run' state
+      let units := li.map λ (unit, _, _) => unit
-      let units ← li.mapM λ (boundary, invocations?, sorrys, messages) => do
+      let invocations? := if args.invocations then
-        let (goalStateId?, goals) ← if sorrys.isEmpty then do
+          .some $ li.bind λ (_, invocations, _) => invocations
-            pure (.none, #[])
+        else
-          else do
+          .none
+      let goalStates? ← if args.sorrys then do
+          let stateIds ← li.filterMapM λ (_, _, sorrys) => do
+            if sorrys.isEmpty then
+              return .none
             let goalState ← runMetaInMainM $ Frontend.sorrysToGoalState sorrys
             let stateId ← newGoalState goalState
             let goals ← goalSerialize goalState options
-            pure (.some stateId, goals)
+            return .some (stateId, goals)
-        return {
+          pure $ .some stateIds
-          boundary,
+        else
-          invocations?,
+          pure .none
-          goalStateId?,
+      return .ok { units, invocations?, goalStates? }
-          goals,
-          messages,
-        }
-      return .ok { units }
     catch e =>
       return .error $ errorI "frontend" (← e.toMessageData.toString)
 

Test/Integration.lean

@@ -176,8 +176,7 @@ def test_frontend_process : Test :=
         ("sorrys", .bool false),
       ]
      ({
-       units := [{
+       units := [(0, file.utf8ByteSize)],
-         boundary := (0, file.utf8ByteSize),
        invocations? := .some [
          {
            goalBefore := "⊢ ∀ (p : Prop), p → p",
@@ -190,7 +189,6 @@ def test_frontend_process : Test :=
            tactic := "exact h",
          },
        ]
-       }],
     }: Protocol.FrontendProcessResult),
   ]
 
@@ -214,14 +212,13 @@ def test_frontend_process_sorry : Test :=
         ("sorrys", .bool true),
       ]
      ({
-       units := [{
+       units := [
-         boundary := (0, solved.utf8ByteSize),
+         (0, solved.utf8ByteSize),
-       }, {
+         (solved.utf8ByteSize, solved.utf8ByteSize + withSorry.utf8ByteSize),
-         boundary := (solved.utf8ByteSize, solved.utf8ByteSize + withSorry.utf8ByteSize),
+       ],
-         goalStateId? := .some 0,
+       goalStates? := [
-         goals := #[goal1],
+         (0, #[goal1]),
-         messages := #["<anonymous>:2:0: warning: declaration uses 'sorry'\n"],
+       ]
-       }],
     }: Protocol.FrontendProcessResult),
   ]