feat: Use CoreM as the main interaction monad

This commit is contained in:
Leni Aniva 2023-12-12 18:39:02 -08:00
parent ac9f6f810c
commit 085b12c255
3 changed files with 14 additions and 14 deletions

View File

@ -102,8 +102,7 @@ unsafe def main (args: List String): IO Unit := do
options := options options := options
} }
try try
let metaM := loop.run context |>.run' {} let coreM := loop.run context |>.run' {}
let coreM := metaM.run'
IO.println "ready." IO.println "ready."
discard <| coreM.toIO coreContext { env := env } discard <| coreM.toIO coreContext { env := env }
catch ex => catch ex =>

View File

@ -16,16 +16,18 @@ 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.MetaM) abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
-- 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 α := def runMetaM { α } (metaM: Lean.MetaM α): Lean.CoreM α :=
metaM.run'
def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α :=
termElabM.run' (ctx := { termElabM.run' (ctx := {
declName? := .none, declName? := .none,
errToSorry := false, errToSorry := false,
}) }) |>.run'
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 :=
@ -89,8 +91,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
| .none, .defnInfo _ => info.value? | .none, .defnInfo _ => info.value?
| .none, _ => .none | .none, _ => .none
return .ok { return .ok {
type := ← serialize_expression state.options info.type, type := ← (serialize_expression state.options info.type).run',
value? := ← value?.mapM (λ v => serialize_expression state.options v), value? := ← value?.mapM (λ v => serialize_expression state.options v |>.run'),
publicName? := Lean.privateToUserName? name |>.map (·.toString), publicName? := Lean.privateToUserName? name |>.map (·.toString),
-- BUG: Warning: getUsedConstants here will not include projections. This is a known bug. -- BUG: Warning: getUsedConstants here will not include projections. This is a known bug.
typeDependency? := if args.dependency?.getD false then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n) else .none, typeDependency? := if args.dependency?.getD false then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n) else .none,
@ -102,8 +104,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
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 => runTermElabM do
match ← runTermElabM <| syntax_to_expr syn with match ← 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
@ -176,7 +178,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
goalStates := state.goalStates.insert state.nextId nextGoalState, goalStates := state.goalStates.insert state.nextId nextGoalState,
nextId := state.nextId + 1, nextId := state.nextId + 1,
} }
let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
return .ok { return .ok {
nextStateId? := .some nextStateId, nextStateId? := .some nextStateId,
goals? := .some goals, goals? := .some goals,
@ -209,7 +211,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
goalStates := state.goalStates.insert nextStateId nextGoalState, goalStates := state.goalStates.insert nextStateId nextGoalState,
nextId := state.nextId + 1 nextId := state.nextId + 1
} }
let goals ← nextGoalState.serializeGoals (parent := .none) (options := state.options) let goals ← nextGoalState.serializeGoals (parent := .none) (options := state.options) |>.run'
return .ok { return .ok {
nextStateId, nextStateId,
goals, goals,
@ -223,7 +225,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
let state ← get let state ← get
match state.goalStates.find? args.stateId with match state.goalStates.find? args.stateId with
| .none => return .error $ errorIndex s!"Invalid state index {args.stateId}" | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
| .some goalState => do | .some goalState => runMetaM <| do
goalState.restoreMetaM goalState.restoreMetaM
let root? ← goalState.rootExpr?.mapM (λ expr => serialize_expression state.options expr) let root? ← goalState.rootExpr?.mapM (λ expr => serialize_expression state.options expr)
return .ok { return .ok {

View File

@ -33,8 +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 metaM := commands.run context |>.run' {} let coreM := commands.run context |>.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 =>
return LSpec.check s!"Uncaught IO exception: {ex.toString}" false return LSpec.check s!"Uncaught IO exception: {ex.toString}" false