fix: Change the main interaction monad to MetaM

This commit is contained in:
Leni Aniva 2023-12-08 16:17:16 -08:00
parent de2688ccfa
commit c76751861a
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
4 changed files with 15 additions and 20 deletions

View File

@ -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 }

View File

@ -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

View File

@ -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 }))

View File

@ -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 =>