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

feat: Add support for the have, conv, and calc tactics #59

Merged
aniva merged 22 commits from goal/have-conv-calc into dev 2024-04-11 15:36:20 -07:00
Conversation 0 Commits 22 Files Changed 9 +5 -8
1 changed files with 5 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit dd94e29293 - Show all commits

13
Pantograph/Library.lean
View File

@ -136,8 +136,8 @@ def parseElabExpr (expr: String) (expectedType?: Option String := .none): Lean.E
@[export pantograph_expr_echo_m] @[export pantograph_expr_echo_m]
def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&Protocol.Options): def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&Protocol.Options):
Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) :=
let termElabM: Lean.Elab.TermElabM _ := do runTermElabM do
let expr ← match ← parseElabExpr expr expectedType? with let expr ← match ← parseElabExpr expr expectedType? with
| .error e => return .error e | .error e => return .error e
| .ok expr => pure expr | .ok expr => pure expr
@ -149,16 +149,14 @@ def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&
} }
catch exception => catch exception =>
return .error $ errorI "typing" (← exception.toMessageData.toString) return .error $ errorI "typing" (← exception.toMessageData.toString)
runTermElabM termElabM
@[export pantograph_goal_start_expr_m] @[export pantograph_goal_start_expr_m]
def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) := def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) :=
let termElabM: Lean.Elab.TermElabM _ := do runTermElabM do
let expr ← match ← parseElabType expr with let expr ← match ← parseElabType expr with
| .error e => return .error e | .error e => return .error e
| .ok expr => pure $ expr | .ok expr => pure $ expr
return .ok $ ← GoalState.create expr return .ok $ ← GoalState.create expr
runTermElabM termElabM
@[export pantograph_goal_tactic_m] @[export pantograph_goal_tactic_m]
def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult := def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult :=
@ -193,8 +191,8 @@ def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM (
runMetaM <| state.serializeGoals (parent := .none) options runMetaM <| state.serializeGoals (parent := .none) options
@[export pantograph_goal_print_m] @[export pantograph_goal_print_m]
def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Protocol.GoalPrintResult := do def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Protocol.GoalPrintResult :=
let metaM := do runMetaM do
state.restoreMetaM state.restoreMetaM
return { return {
root? := ← state.rootExpr?.mapM (λ expr => do root? := ← state.rootExpr?.mapM (λ expr => do
@ -202,7 +200,6 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto
parent? := ← state.parentExpr?.mapM (λ expr => do parent? := ← state.parentExpr?.mapM (λ expr => do
serialize_expression options (← unfoldAuxLemmas expr)), serialize_expression options (← unfoldAuxLemmas expr)),
} }
runMetaM metaM
end Pantograph end Pantograph