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

refactor: Use library functions when possible

This commit is contained in:
Leni Aniva 2024-03-31 16:11:41 -07:00
parent 7988a25ce8
commit a1ed8f4b3d
2 changed files with 8 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Pantograph.lean
View File

@ -148,7 +148,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
| .some branchId, .none => do
match state.goalStates.find? branchId with
| .none => return .error $ errorIndex s!"Invalid state index {branchId}"
| .some branch => pure $ target.continue branch
| .some branch => pure $ goalContinue target branch
| .none, .some goals =>
pure $ goalResume target goals
| _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"

14
Pantograph/Library.lean
View File

@ -109,9 +109,9 @@ def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool):
Lean.CoreM (Protocol.CR Protocol.EnvAddResult) :=
Environment.addDecl { name, type, value, isTheorem }
def typeParse (typeParse: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
def parseElabType (type: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
let env ← Lean.MonadEnv.getEnv
let syn ← match parseTerm env typeParse with
let syn ← match parseTerm env type with
| .error str => return .error $ errorI "parsing" str
| .ok syn => pure syn
match ← elabType syn with
@ -119,13 +119,13 @@ def typeParse (typeParse: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) :
| .ok expr => return .ok expr
/-- This must be a TermElabM since the parsed expr contains extra information -/
def exprParse (exprStr: String) (expectedType?: Option String := .none): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
def parseElabExpr (expr: String) (expectedType?: Option String := .none): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
let env ← Lean.MonadEnv.getEnv
let expectedType? ← match ← expectedType?.mapM typeParse with
let expectedType? ← match ← expectedType?.mapM parseElabType with
| .none => pure $ .none
| .some (.ok t) => pure $ .some t
| .some (.error e) => return .error e
let syn ← match parseTerm env exprStr with
let syn ← match parseTerm env expr with
| .error str => return .error $ errorI "parsing" str
| .ok syn => pure syn
match ← elabTerm syn expectedType? with
@ -136,7 +136,7 @@ def exprParse (exprStr: String) (expectedType?: Option String := .none): Lean.El
def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&Protocol.Options):
Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do
let termElabM: Lean.Elab.TermElabM _ := do
let expr ← match ← exprParse expr expectedType? with
let expr ← match ← parseElabExpr expr expectedType? with
| .error e => return .error e
| .ok expr => pure expr
try
@ -152,7 +152,7 @@ def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&
@[export pantograph_goal_start_expr_m]
def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) :=
let termElabM: Lean.Elab.TermElabM _ := do
let expr ← match ← typeParse expr with
let expr ← match ← parseElabType expr with
| .error e => return .error e
| .ok expr => pure $ expr
return .ok $ ← GoalState.create expr