From 3bb8e757873c4aa522ef9afb3a3b8f5048861b84 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 2 May 2025 11:26:17 -0400 Subject: [PATCH 1/3] chore: Code cleanup --- Repl.lean | 4 +--- Test/Tactic/Prograde.lean | 4 ---- 2 files changed, 1 insertion(+), 7 deletions(-) diff --git a/Repl.lean b/Repl.lean index ce6a9df..6a03cbe 100644 --- a/Repl.lean +++ b/Repl.lean @@ -5,8 +5,6 @@ namespace Pantograph.Repl open Lean -set_option trace.Pantograph.Frontend.MetaTranslate true - structure Context where coreContext : Core.Context @@ -30,7 +28,7 @@ instance : MonadEnv MainM where getEnv := return (← get).env modifyEnv f := modify fun s => { s with env := f s.env } -def newGoalState (goalState: GoalState) : MainM Nat := do +def newGoalState (goalState : GoalState) : MainM Nat := do let state ← get let stateId := state.nextId set { state with diff --git a/Test/Tactic/Prograde.lean b/Test/Tactic/Prograde.lean index 6a806ce..aace238 100644 --- a/Test/Tactic/Prograde.lean +++ b/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 -- 2.44.1 From 4bb44dd56a8072d69db6f9be82bdde54ca807f0e Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 2 May 2025 11:33:11 -0400 Subject: [PATCH 2/3] chore: Syntax cleanup in repl --- Repl.lean | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/Repl.lean b/Repl.lean index 6a03cbe..4c9ddf2 100644 --- a/Repl.lean +++ b/Repl.lean @@ -39,7 +39,7 @@ def newGoalState (goalState : GoalState) : MainM Nat := do def runCoreM { α } (coreM : CoreM α) : EMainM α := do let scope := (← get).scope - let options :=(← get).options + let options := (← get).options let cancelTk? ← match options.timeout with | 0 => pure .none | _ => .some <$> IO.CancelToken.new @@ -60,7 +60,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) @@ -72,16 +72,15 @@ def runCoreM { α } (coreM : CoreM α) : EMainM α := do | 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 + 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 := []) +def liftTermElabM { α } (termElabM : Elab.TermElabM α) (levelNames : List Name := []) : EMainM α := do let scope := (← get).scope let context := { @@ -96,7 +95,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 @@ -104,7 +103,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 @@ -400,7 +399,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 -- 2.44.1 From eb41c179d1ce92249924ed84fb9a895594693704 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 2 May 2025 11:40:32 -0400 Subject: [PATCH 3/3] feat(repl): Conditional environment inheritance --- Repl.lean | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/Repl.lean b/Repl.lean index 4c9ddf2..c37da05 100644 --- a/Repl.lean +++ b/Repl.lean @@ -7,6 +7,8 @@ open Lean 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 @@ -28,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 @@ -71,7 +76,7 @@ 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 + if (← read).inheritEnv && result matches .ok _ then setEnv state'.env liftExcept result @@ -239,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 -- 2.44.1