Merge pull request 'feat(frontend): Alternative methods of initializing environment' (#173) from frontend/env-init into dev

Reviewed-on: #173

Pantograph/Frontend/Basic.lean

@@ -40,6 +40,7 @@ def stxByteRange (stx : Syntax) : String.Pos × String.Pos :=
 abbrev FrontendM := Elab.Frontend.FrontendM
 
 structure CompilationStep where
+  scope : Elab.Command.Scope
   fileName : String
   fileMap : FileMap
   src : Substring
@@ -74,7 +75,7 @@ def processOneCommand: FrontendM (CompilationStep × Bool) := do
   let msgs := s'.messages.toList.drop s.messages.toList.length
   let trees := s'.infoState.trees.drop s.infoState.trees.size
   let ⟨_, fileName, fileMap⟩  := (← read).inputCtx
-  return ({ fileName, fileMap, src, stx, before, after, msgs, trees }, done)
+  return ({ scope := s.scopes.head!, fileName, fileMap, src, stx, before, after, msgs, trees }, done)
 
 partial def mapCompilationSteps { α } (f: CompilationStep → IO α) : FrontendM (List α) := do
   let (cmd, done) ← processOneCommand

Pantograph/Protocol.lean

@@ -346,6 +346,11 @@ structure FrontendProcess where
   -- One of these two must be supplied: Either supply the file name or the content.
   fileName?: Option String := .none
   file?: Option String := .none
+  -- If set to true, read the header (otherwise discards the header)
+  readHeader : Bool := false
+  -- If set to true, Pantograph's environment will be altered to whatever is
+  -- after the compilation units.
+  inheritEnv : Bool := false
   -- collect tactic invocations
   invocations: Bool := false
   -- collect `sorry`s

Repl.lean

@@ -53,11 +53,10 @@ def frontend_process_inner (args: Protocol.FrontendProcess): MainM (CR Protocol.
     | .none, .some file =>
       pure ("<anonymous>", file)
     | _, _ => return .error <| errorI "arguments" "Exactly one of {fileName, file} must be supplied"
-  let env?: Option Environment ← if args.fileName?.isSome then
+  let env?: Option Environment ← if args.readHeader then
       pure .none
     else do
-      let env ← getEnv
+      .some <$> getEnv
-      pure <| .some env
   let (context, state) ← do Frontend.createContextStateFromFile file fileName env? {}
   let frontendM: Elab.Frontend.FrontendM (List CompilationUnit) :=
     Frontend.mapCompilationSteps λ step => do
@@ -83,7 +82,9 @@ def frontend_process_inner (args: Protocol.FrontendProcess): MainM (CR Protocol.
       messages,
       newConstants
     }
-  let li ← frontendM.run context |>.run' state
+  let (li, state') ← frontendM.run context |>.run state
+  if args.inheritEnv then
+    setEnv state'.commandState.env
   let units ← li.mapM λ step => withEnv step.env do
     let newConstants? := if args.newConstants then
         .some $ step.newConstants.toArray.map λ name => name.toString
@@ -141,7 +142,7 @@ def execute (command: Protocol.Command): MainM Json := do
     | "goal.print"    => run goal_print
     | "goal.save"     => run goal_save
     | "goal.load"     => run goal_load
-    | "frontend.process"  => run frontend_process
+    | "frontend.process" => run frontend_process
     | cmd =>
       let error: Protocol.InteractionError :=
         errorCommand s!"Unknown command {cmd}"

Test/Frontend.lean

@@ -1,11 +1,28 @@
-import LSpec
 import Pantograph
 import Repl
 import Test.Common
 
+import LSpec
+
 open Lean Pantograph
 namespace Pantograph.Test.Frontend
 
+def runFrontend { α } (source: String) (f : Frontend.CompilationStep → IO α) : MetaM (List α) := do
+  let filename := "<anonymous>"
+  let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {}
+  let m := Frontend.mapCompilationSteps f
+  m.run context |>.run' state
+
+def test_open : TestT MetaM Unit := do
+  let sketch := "
+open Nat
+example : ∀ (n : Nat), n + 1 = Nat.succ n := by
+  intro
+  apply add_one
+  "
+  let errors ← runFrontend sketch λ step => step.msgs.mapM (·.toString)
+  checkEq "errors" errors [[], []]
+
 def collectSorrysFromSource (source: String) (options : Frontend.GoalCollectionOptions := {})
     : MetaM (List GoalState) := do
   let filename := "<anonymous>"
@@ -233,6 +250,7 @@ theorem mystery [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get
 
 def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
+    ("open", test_open),
     ("multiple_sorrys_in_proof", test_multiple_sorrys_in_proof),
     ("sorry_in_middle", test_sorry_in_middle),
     ("sorry_in_induction", test_sorry_in_induction),

Test/Integration.lean

@@ -173,6 +173,8 @@ def test_frontend_process : Test :=
       [
         ("file",              .str file),
         ("invocations",       .bool true),
+        ("readHeader",        .bool false),
+        ("inheritEnv",        .bool false),
         ("sorrys",            .bool false),
         ("typeErrorsAsGoals", .bool false),
         ("newConstants",      .bool false),
@@ -214,6 +216,8 @@ def test_frontend_process_sorry : Test :=
     step "frontend.process"
       [
         ("file", .str file),
+        ("readHeader",        .bool false),
+        ("inheritEnv",        .bool false),
         ("invocations", .bool false),
         ("sorrys", .bool true),
         ("typeErrorsAsGoals", .bool false),