From c76751861aac4b4161d16d378a37222c425a3e8e Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 8 Dec 2023 16:17:16 -0800 Subject: [PATCH] fix: Change the main interaction monad to MetaM --- Main.lean | 6 +----- Pantograph.lean | 18 ++++++++++++------ Test/Catalog.lean | 5 +---- Test/Integration.lean | 6 +----- 4 files changed, 15 insertions(+), 20 deletions(-) diff --git a/Main.lean b/Main.lean index 59a7e95..e833649 100644 --- a/Main.lean +++ b/Main.lean @@ -102,11 +102,7 @@ unsafe def main (args: List String): IO Unit := do options := options } try - let termElabM := loop.run context |>.run' {} - let metaM := termElabM.run' (ctx := { - declName? := some "_pantograph", - errToSorry := false - }) + let metaM := loop.run context |>.run' {} let coreM := metaM.run' IO.println "ready." discard <| coreM.toIO coreContext { env := env } diff --git a/Pantograph.lean b/Pantograph.lean index a66db35..ab6a7b1 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -16,11 +16,17 @@ structure State where goalStates: Lean.HashMap Nat GoalState := Lean.HashMap.empty /-- Main state monad for executing commands -/ -abbrev MainM := ReaderT Context (StateT State Lean.Elab.TermElabM) +abbrev MainM := ReaderT Context (StateT State Lean.MetaM) -- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables -- certain monadic features in `MainM` abbrev CR α := Except Protocol.InteractionError α +def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α := + termElabM.run' (ctx := { + declName? := .none, + errToSorry := false, + }) + def execute (command: Protocol.Command): MainM Lean.Json := do let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json := match Lean.fromJson? command.payload with @@ -97,7 +103,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do match syntax_from_str env args.expr with | .error str => return .error $ errorI "parsing" str | .ok syn => do - match (← syntax_to_expr syn) with + match ← runTermElabM <| syntax_to_expr syn with | .error str => return .error $ errorI "elab" str | .ok expr => do try @@ -133,7 +139,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do (match syntax_from_str env expr with | .error str => return .error <| errorI "parsing" str | .ok syn => do - (match (← syntax_to_expr syn) with + (match ← runTermElabM <| syntax_to_expr syn with | .error str => return .error <| errorI "elab" str | .ok expr => return .ok expr)) | .none, .some copyFrom => @@ -145,7 +151,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do match expr? with | .error error => return .error error | .ok expr => - let goalState ← GoalState.create expr + let goalState ← runTermElabM <| GoalState.create expr let stateId := state.nextId set { state with goalStates := state.goalStates.insert stateId goalState, @@ -159,9 +165,9 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | .some goalState => do let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with | .some tactic, .none => do - pure ( Except.ok (← GoalState.execute goalState args.goalId tactic)) + pure ( Except.ok (← runTermElabM <| GoalState.execute goalState args.goalId tactic)) | .none, .some expr => do - pure ( Except.ok (← GoalState.tryAssign goalState args.goalId expr)) + pure ( Except.ok (← runTermElabM <| GoalState.tryAssign goalState args.goalId expr)) | _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr} must be supplied") match nextGoalState? with | .error error => return .error error diff --git a/Test/Catalog.lean b/Test/Catalog.lean index e082369..44c2bf7 100644 --- a/Test/Catalog.lean +++ b/Test/Catalog.lean @@ -10,8 +10,7 @@ open Lean def test_symbol_visibility (env: Environment): IO LSpec.TestSeq := do let entries: List (Name × Bool) := [ ("Nat.add_comm".toName, false), - ("Lean.Name".toName, true), - ("_private.Init.0.Lean.Name".toName, true) + ("Lean.Name".toName, true) ] let suite := entries.foldl (λ suites (symbol, target) => let constant := env.constants.find! symbol @@ -19,8 +18,6 @@ def test_symbol_visibility (env: Environment): IO LSpec.TestSeq := do LSpec.TestSeq.append suites test) LSpec.TestSeq.done return suite - - def suite: IO LSpec.TestSeq := do let env: Environment ← importModules (imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false })) diff --git a/Test/Integration.lean b/Test/Integration.lean index 65c2da6..50ee740 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -33,11 +33,7 @@ def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := d let result ← step return suite ++ result) LSpec.TestSeq.done try - let termElabM := commands.run context |>.run' {} - let metaM := termElabM.run' (ctx := { - declName? := some "_pantograph", - errToSorry := false - }) + let metaM := commands.run context |>.run' {} let coreM := metaM.run' return Prod.fst $ (← coreM.toIO coreContext { env := env }) catch ex =>