feat: Change the main interaction monad #40

Merged
aniva merged 4 commits from core/loop into dev 2023-12-14 05:46:40 -08:00
3 changed files with 14 additions and 8 deletions
Showing only changes of commit 1fb189a38f - Show all commits

View File

@ -134,24 +134,23 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
let state ← get let state ← get
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
let expr?: Except _ Lean.Expr ← (match args.expr, args.copyFrom with let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with
| .some expr, .none => | .some expr, .none =>
(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 ← 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 => return .ok expr)) | .ok expr => return .ok (← GoalState.create expr)))
| .none, .some copyFrom => | .none, .some copyFrom =>
(match env.find? <| copyFrom.toName with (match env.find? <| copyFrom.toName with
| .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}" | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
| .some cInfo => return .ok cInfo.type) | .some cInfo => return .ok (← GoalState.create cInfo.type))
| _, _ => | _, _ =>
return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied") return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied")
match expr? with match expr? with
| .error error => return .error error | .error error => return .error error
| .ok expr => | .ok goalState =>
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,
@ -225,6 +224,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
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 => do
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 {
root?, root?,

View File

@ -51,6 +51,10 @@ protected def GoalState.env (state: GoalState): Environment :=
state.savedState.term.meta.core.env state.savedState.term.meta.core.env
private def GoalState.mvars (state: GoalState): SSet MVarId := private def GoalState.mvars (state: GoalState): SSet MVarId :=
state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
private def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit :=
state.savedState.term.restore
def GoalState.restoreMetaM (state: GoalState): MetaM Unit :=
state.savedState.term.meta.restore
/-- Inner function for executing tactic on goal state -/ /-- Inner function for executing tactic on goal state -/
def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) : def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) :
@ -84,6 +88,7 @@ inductive TacticResult where
/-- Execute tactic on given state -/ /-- Execute tactic on given state -/
protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String): protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String):
M TacticResult := do M TacticResult := do
state.restoreElabM
let goal ← match state.savedState.tactic.goals.get? goalId with let goal ← match state.savedState.tactic.goals.get? goalId with
| .some goal => pure $ goal | .some goal => pure $ goal
| .none => return .indexError goalId | .none => return .indexError goalId
@ -118,6 +123,7 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String
} }
protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String): M TacticResult := do protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String): M TacticResult := do
state.restoreElabM
let goal ← match state.savedState.tactic.goals.get? goalId with let goal ← match state.savedState.tactic.goals.get? goalId with
| .some goal => pure goal | .some goal => pure goal
| .none => return .indexError goalId | .none => return .indexError goalId

View File

@ -242,8 +242,8 @@ def serialize_goal (options: Protocol.Options) (goal: MVarId) (mvarDecl: Metavar
of_name (n: Name) := name_to_ast n (sanitize := false) of_name (n: Name) := name_to_ast n (sanitize := false)
protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalState := .none) (options: Protocol.Options := {}): MetaM (Array Protocol.Goal):= do protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalState := .none) (options: Protocol.Options := {}): MetaM (Array Protocol.Goal):= do
state.restoreMetaM
let goals := state.goals.toArray let goals := state.goals.toArray
state.savedState.term.meta.restore
let parentDecl? := parent.bind (λ parentState => let parentDecl? := parent.bind (λ parentState =>
let parentGoal := parentState.goals.get! state.parentGoalId let parentGoal := parentState.goals.get! state.parentGoalId
parentState.mctx.findDecl? parentGoal) parentState.mctx.findDecl? parentGoal)
@ -256,8 +256,8 @@ protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalSt
/-- Print the metavariables in a readable format -/ /-- Print the metavariables in a readable format -/
protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM Unit := do protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM Unit := do
goalState.restoreMetaM
let savedState := goalState.savedState let savedState := goalState.savedState
savedState.term.meta.restore
let goals := savedState.tactic.goals let goals := savedState.tactic.goals
let mctx ← getMCtx let mctx ← getMCtx
let root := goalState.root let root := goalState.root