aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 12 Pull Requests 1 Packages Projects Releases Wiki Activity

chore: Use `StateRefT` in `Repl.lean`

This commit is contained in:
Leni Aniva 2025-01-24 20:19:07 -08:00
parent 6a7830cb71
commit 970c16a0a4
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
1 changed files with 3 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
Repl.lean
View File

@ -12,7 +12,9 @@ structure State where
goalStates: Std.HashMap Nat GoalState := Std.HashMap.empty goalStates: Std.HashMap Nat GoalState := Std.HashMap.empty
/-- Main state monad for executing commands -/ /-- Main state monad for executing commands -/
abbrev MainM := ReaderT Context (StateT State Lean.CoreM) abbrev MainM := ReaderT Context $ StateRefT State Lean.CoreM
/-- Fallible subroutine return type -/
abbrev CR α := Except Protocol.InteractionError α
def newGoalState (goalState: GoalState) : MainM Nat := do def newGoalState (goalState: GoalState) : MainM Nat := do
let state ← get let state ← get
@ -24,10 +26,6 @@ def newGoalState (goalState: GoalState) : MainM Nat := do
return stateId return stateId
-- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables
-- certain monadic features in `MainM`
abbrev CR α := Except Protocol.InteractionError α
def runMetaInMainM { α } (metaM: Lean.MetaM α): MainM α := def runMetaInMainM { α } (metaM: Lean.MetaM α): MainM α :=
metaM.run' metaM.run'
def runTermElabInMainM { α } (termElabM: Lean.Elab.TermElabM α) : MainM α := def runTermElabInMainM { α } (termElabM: Lean.Elab.TermElabM α) : MainM α :=