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

fix(goal): Allow parent expr to be fragments

This commit is contained in:
Leni Aniva 2025-06-30 15:00:30 -07:00
parent 8857b88d9a
commit dd7c6c36c8
Signed by: aniva
GPG Key ID: D5F96287843E8DFB
3 changed files with 18 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
Pantograph/Goal.lean
View File

@ -64,7 +64,11 @@ structure GoalState where
-- The root goal which is the search target -- The root goal which is the search target
root: MVarId root: MVarId
-- Parent goals assigned to produce this state /--
Parent goals which became assigned or fragmented to produce this state.
Note that due to the existence of tactic fragments, parent goals do not
necessarily have an expression assignment.
-/
parentMVars : List MVarId := [] parentMVars : List MVarId := []
-- Any goal associated with a fragment has a partial tactic which has not -- Any goal associated with a fragment has a partial tactic which has not
@ -202,8 +206,11 @@ protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvarId: MVarI
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
return expr return expr
@[export pantograph_goal_state_parent_exprs] @[export pantograph_goal_state_parent_exprs]
protected def GoalState.parentExprs (state : GoalState) : List Expr := protected def GoalState.parentExprs (state : GoalState) : List (Except Fragment Expr) :=
state.parentMVars.map λ goal => state.getMVarEAssignment goal |>.get! state.parentMVars.map λ goal => match state.getMVarEAssignment goal with
| .some e => .ok e
-- A parent goal which is not assigned must have a fragment
| .none => .error state.fragments[goal]!
@[always_inline] @[always_inline]
protected def GoalState.hasUniqueParent (state : GoalState) : Bool := protected def GoalState.hasUniqueParent (state : GoalState) : Bool :=
state.parentMVars.length == 1 state.parentMVars.length == 1

9
Repl.lean
View File

@ -147,10 +147,15 @@ def goal_tactic (args: Protocol.GoalTactic): EMainM Protocol.GoalTacticResult :=
match nextGoalState? with match nextGoalState? with
| .error error => Protocol.throw error | .error error => Protocol.throw error
| .ok (.success nextGoalState messages) => do | .ok (.success nextGoalState messages) => do
let env ← getEnv
let nextStateId ← newGoalState nextGoalState let nextStateId ← newGoalState nextGoalState
let parentExprs := nextGoalState.parentExprs let parentExprs := nextGoalState.parentExprs
let hasSorry := parentExprs.any (·.hasSorry) let hasSorry := parentExprs.any λ
let hasUnsafe := parentExprs.any ((← getEnv).hasUnsafe ·) | .ok e => e.hasSorry
| .error _ => false
let hasUnsafe := parentExprs.any λ
| .ok e => env.hasUnsafe e
| .error _ => false
let goals ← runCoreM $ nextGoalState.serializeGoals (options := state.options) |>.run' let goals ← runCoreM $ nextGoalState.serializeGoals (options := state.options) |>.run'
return { return {
nextStateId? := .some nextStateId, nextStateId? := .some nextStateId,

2
Test/Serial.lean
View File

@ -84,7 +84,7 @@ def test_pickling_env_extensions : TestM Unit := do
let goal := state.goals[0]! let goal := state.goals[0]!
let type ← goal.withContext do let type ← goal.withContext do
let .ok type ← elabTerm (← `(term|(2: Nat) ≤ 3)) (.some $ .sort 0) | unreachable! let .ok type ← elabTerm (← `(term|(2: Nat) ≤ 3)) (.some $ .sort 0) | unreachable!
pure type instantiateMVars type
let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type) | unreachable! let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type) | unreachable!
let parentExpr := state1.parentExpr! let parentExpr := state1.parentExpr!
checkTrue "src has aux lemma" $ parentExpr.getUsedConstants.any (·.isAuxLemma) checkTrue "src has aux lemma" $ parentExpr.getUsedConstants.any (·.isAuxLemma)