feat(lib): Export goal.print function

This commit is contained in:
Leni Aniva 2024-03-14 16:34:01 -07:00
parent 4eec930dd4
commit 3debcc021a
2 changed files with 10 additions and 7 deletions

View File

@ -179,12 +179,6 @@ 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 => runMetaM <| do | .some goalState => runMetaM <| do
goalState.restoreMetaM return .ok (← goalPrint goalState state.options)
let root? ← goalState.rootExpr?.mapM (λ expr => serialize_expression state.options expr)
let parent? ← goalState.parentExpr?.mapM (λ expr => serialize_expression state.options expr)
return .ok {
root?,
parent?,
}
end Pantograph end Pantograph

View File

@ -165,6 +165,15 @@ def goalResume (target: GoalState) (goals: Array String): Except String GoalStat
def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM (Array Protocol.Goal) := def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM (Array Protocol.Goal) :=
runMetaM <| state.serializeGoals (parent := .none) options runMetaM <| state.serializeGoals (parent := .none) options
@[export pantograph_goal_print_m]
def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Protocol.GoalPrintResult := do
let metaM := do
state.restoreMetaM
return {
root? := ← state.rootExpr?.mapM (λ expr => serialize_expression options expr),
parent? := ← state.parentExpr?.mapM (λ expr => serialize_expression options expr),
}
runMetaM metaM
end Pantograph end Pantograph