Repl.lean

@@ -5,10 +5,10 @@ namespace Pantograph.Repl
 
 open Lean
 
-set_option trace.Pantograph.Frontend.MetaTranslate true
-
 structure Context where
   coreContext : Core.Context
+  -- If true, the environment will change after running `CoreM`
+  inheritEnv : Bool := false
 
 /-- Stores state of the REPL -/
 structure State where
@@ -30,6 +30,9 @@ instance : MonadEnv MainM where
   getEnv := return (← get).env
   modifyEnv f := modify fun s => { s with env := f s.env  }
 
+def withInheritEnv [Monad m] [MonadWithReaderOf Context m] [MonadLift MainM m] { α } (z : m α) : m α := do
+  withTheReader Context ({ · with inheritEnv := true }) z
+
 def newGoalState (goalState : GoalState) : MainM Nat := do
   let state ← get
   let stateId := state.nextId
@@ -62,7 +65,7 @@ def runCoreM { α } (coreM : CoreM α) : EMainM α := do
       Except.ok <$> coreM
     catch ex =>
       let desc ← ex.toMessageData.toString
-      return Except.error $ ({ error := "exception", desc } : Protocol.InteractionError)
+      return Except.error ({ error := "exception", desc } : Protocol.InteractionError)
     finally
       for {msg, ..} in (← getTraceState).traces do
         IO.eprintln (← msg.format.toIO)
@@ -73,14 +76,13 @@ def runCoreM { α } (coreM : CoreM α) : EMainM α := do
     | Except.error (Exception.error _ msg)   => Protocol.throw $ { error := "core", desc := ← msg.toString }
     | Except.error (Exception.internal id _) => Protocol.throw $ { error := "internal", desc := (← id.getName).toString }
     | Except.ok a                            => pure a
-  if result matches .ok _ then
-    modifyEnv λ _ => state'.env
+  if (← read).inheritEnv && result matches .ok _ then
+    setEnv state'.env
   liftExcept result
 
 def runCoreM' { α } (coreM : Protocol.FallibleT CoreM α) : EMainM α := do
   liftExcept $ ← runCoreM coreM.run
 
-
 def liftMetaM { α } (metaM : MetaM α): EMainM α :=
   runCoreM metaM.run'
 def liftTermElabM { α } (termElabM : Elab.TermElabM α) (levelNames : List Name := [])
@@ -98,7 +100,7 @@ def liftTermElabM { α } (termElabM: Elab.TermElabM α) (levelNames : List Name
 section Frontend
 
 structure CompilationUnit where
-  -- Should be the penultimate environment, but this is ok
+  -- Environment immediately before the unit
   env : Environment
   boundary : Nat × Nat
   invocations : List Protocol.InvokedTactic
@@ -106,7 +108,7 @@ structure CompilationUnit where
   messages : Array String
   newConstants : List Name
 
-def frontend_process_inner (args: Protocol.FrontendProcess): EMainM Protocol.FrontendProcessResult := do
+def frontend_process (args: Protocol.FrontendProcess): EMainM Protocol.FrontendProcessResult := do
   let options := (← getMainState).options
   let (fileName, file) ← match args.fileName?, args.file? with
     | .some fileName, .none => do
@@ -242,7 +244,7 @@ def execute (command: Protocol.Command): MainM Json := do
   env_inspect (args: Protocol.EnvInspect): EMainM Protocol.EnvInspectResult := do
     let state ← getMainState
     runCoreM' $ Environment.inspect args state.options
-  env_add (args: Protocol.EnvAdd): EMainM Protocol.EnvAddResult := do
+  env_add (args: Protocol.EnvAdd): EMainM Protocol.EnvAddResult := withInheritEnv do
     runCoreM' $ Environment.addDecl args.name (args.levels?.getD #[]) args.type? args.value args.isTheorem
   env_save (args: Protocol.EnvSaveLoad): EMainM Protocol.EnvSaveLoadResult := do
     let env ← MonadEnv.getEnv
@@ -402,7 +404,5 @@ def execute (command: Protocol.Command): MainM Json := do
     let (goalState, _) ← goalStateUnpickle args.path (← MonadEnv.getEnv)
     let id ← newGoalState goalState
     return { id }
-  frontend_process (args: Protocol.FrontendProcess): EMainM Protocol.FrontendProcessResult := do
-    frontend_process_inner args
 
 end Pantograph.Repl

Test/Tactic/Prograde.lean

@@ -131,10 +131,6 @@ def test_define_root_expr : TestT Elab.TermElabM Unit := do
   let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr"
   addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p x =>\n  let binder := x.fst;\n  binder 5")
 
---set_option pp.all true
---#check @PSigma (α := Prop) (β := λ (p: Prop) => p)
---def test_define_root_expr : TestT Elab.TermElabM Unit := do
-
 def test_have_proof : TestT Elab.TermElabM Unit := do
   let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
   let state0 ← GoalState.create rootExpr