fix: Change the main interaction monad to MetaM

This commit is contained in:
Leni Aniva 2023-12-08 16:17:16 -08:00
parent d7fcc502f9
commit 2fe4fa9bc4
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 options := options
} }
try try
let termElabM := loop.run context |>.run' {} let metaM := loop.run context |>.run' {}
let metaM := termElabM.run' (ctx := {
declName? := some "_pantograph",
errToSorry := false
})
let coreM := metaM.run' let coreM := metaM.run'
IO.println "ready." IO.println "ready."
discard <| coreM.toIO coreContext { env := env } discard <| coreM.toIO coreContext { env := env }

View File

@ -16,11 +16,17 @@ structure State where
goalStates: Lean.HashMap Nat GoalState := Lean.HashMap.empty goalStates: Lean.HashMap Nat GoalState := Lean.HashMap.empty
/-- Main state monad for executing commands -/ /-- 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 -- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables
-- certain monadic features in `MainM` -- certain monadic features in `MainM`
abbrev CR α := Except Protocol.InteractionError α 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 def execute (command: Protocol.Command): MainM Lean.Json := do
let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json := let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
match Lean.fromJson? command.payload with 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 match syntax_from_str env args.expr with
| .error str => return .error $ errorI "parsing" str | .error str => return .error $ errorI "parsing" str
| .ok syn => do | .ok syn => do
match (← syntax_to_expr syn) with match ← runTermElabM <| syntax_to_expr syn with
| .error str => return .error $ errorI "elab" str | .error str => return .error $ errorI "elab" str
| .ok expr => do | .ok expr => do
try try
@ -133,7 +139,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
(match syntax_from_str env expr with (match syntax_from_str env expr with
| .error str => return .error <| errorI "parsing" str | .error str => return .error <| errorI "parsing" str
| .ok syn => do | .ok syn => do
(match (← syntax_to_expr syn) with (match ← runTermElabM <| syntax_to_expr syn with
| .error str => return .error <| errorI "elab" str | .error str => return .error <| errorI "elab" str
| .ok expr => return .ok expr)) | .ok expr => return .ok expr))
| .none, .some copyFrom => | .none, .some copyFrom =>
@ -145,7 +151,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
match expr? with match expr? with
| .error error => return .error error | .error error => return .error error
| .ok expr => | .ok expr =>
let goalState ← GoalState.create expr let goalState ← runTermElabM <| GoalState.create expr
let stateId := state.nextId let stateId := state.nextId
set { state with set { state with
goalStates := state.goalStates.insert stateId goalState, goalStates := state.goalStates.insert stateId goalState,
@ -159,9 +165,9 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
| .some goalState => do | .some goalState => do
let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with
| .some tactic, .none => do | .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 | .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") | _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr} must be supplied")
match nextGoalState? with match nextGoalState? with
| .error error => return .error error | .error error => return .error error

View File

@ -10,8 +10,7 @@ open Lean
def test_symbol_visibility (env: Environment): IO LSpec.TestSeq := do def test_symbol_visibility (env: Environment): IO LSpec.TestSeq := do
let entries: List (Name × Bool) := [ let entries: List (Name × Bool) := [
("Nat.add_comm".toName, false), ("Nat.add_comm".toName, false),
("Lean.Name".toName, true), ("Lean.Name".toName, true)
("_private.Init.0.Lean.Name".toName, true)
] ]
let suite := entries.foldl (λ suites (symbol, target) => let suite := entries.foldl (λ suites (symbol, target) =>
let constant := env.constants.find! symbol 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 LSpec.TestSeq.append suites test) LSpec.TestSeq.done
return suite return suite
def suite: IO LSpec.TestSeq := do def suite: IO LSpec.TestSeq := do
let env: Environment ← importModules let env: Environment ← importModules
(imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false })) (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 let result ← step
return suite ++ result) LSpec.TestSeq.done return suite ++ result) LSpec.TestSeq.done
try try
let termElabM := commands.run context |>.run' {} let metaM := commands.run context |>.run' {}
let metaM := termElabM.run' (ctx := {
declName? := some "_pantograph",
errToSorry := false
})
let coreM := metaM.run' let coreM := metaM.run'
return Prod.fst $ (← coreM.toIO coreContext { env := env }) return Prod.fst $ (← coreM.toIO coreContext { env := env })
catch ex => catch ex =>