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

feat: Expose parent and root expr functions

This commit is contained in:
Leni Aniva 2024-07-27 17:39:51 -07:00
parent 2682ce5b7b
commit bf941cd686
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
1 changed files with 4 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
Pantograph/Goal.lean
View File

@ -136,6 +136,7 @@ protected def GoalState.continue (target: GoalState) (branch: GoalState): Except
else else
target.resume (goals := branch.goals) target.resume (goals := branch.goals)
@[export pantograph_goal_state_root_expr]
protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do
let expr ← goalState.mctx.eAssignment.find? goalState.root let expr ← goalState.mctx.eAssignment.find? goalState.root
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
@ -146,12 +147,14 @@ protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do
else else
assert! goalState.goals.isEmpty assert! goalState.goals.isEmpty
return expr return expr
@[export pantograph_goal_state_parent_expr]
protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
let parent ← goalState.parentMVar? let parent ← goalState.parentMVar?
let expr := goalState.mctx.eAssignment.find! parent let expr := goalState.mctx.eAssignment.find! parent
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
return expr return expr
protected def GoalState.assignedExprOf? (goalState: GoalState) (mvar: MVarId): Option Expr := do @[export pantograph_goal_state_get_mvar_e_assignment]
protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvar: MVarId): Option Expr := do
let expr ← goalState.mctx.eAssignment.find? mvar let expr ← goalState.mctx.eAssignment.find? mvar
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
return expr return expr