diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 7f135f5..fba5a4f 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -113,11 +113,14 @@ protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState } /-- Immediately bring all parent goals back into scope. Used in automatic mode -/ -@[export pantograph_goal_state_immediate_resume_parent] +@[export pantograph_goal_state_immediate_resume] protected def GoalState.immediateResume (state: GoalState) (parent: GoalState): GoalState := -- Prune parents solved goals let mctx := state.mctx - let parentGoals := parent.goals.filter $ λ goal => mctx.eAssignment.contains goal + let parentGoals := parent.goals.filter λ goal => + let isDuplicate := state.goals.contains goal + let isSolved := mctx.eAssignment.contains goal || mctx.dAssignment.contains goal + (¬ isDuplicate) && (¬ isSolved) { state with savedState := { @@ -127,25 +130,25 @@ protected def GoalState.immediateResume (state: GoalState) (parent: GoalState): } /-- -Brings into scope a list of goals +Brings into scope a list of goals. User must ensure `goals` is distinct. -/ @[export pantograph_goal_state_resume] -protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState := +protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState := do if ¬ (goals.all (λ goal => state.mvars.contains goal)) then let invalid_goals := goals.filter (λ goal => ¬ state.mvars.contains goal) |>.map (·.name.toString) .error s!"Goals {invalid_goals} are not in scope" - else - -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic. - let unassigned := goals.filter (λ goal => - let mctx := state.mctx - ¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal)) - .ok { - state with - savedState := { - term := state.savedState.term, - tactic := { goals := unassigned }, - }, - } + -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic. + let unassigned := goals.filter λ goal => + let isSolved := state.mctx.eAssignment.contains goal || state.mctx.dAssignment.contains goal + let isDuplicate := state.goals.contains goal + (¬ isDuplicate) && (¬ isSolved) + return { + state with + savedState := { + term := state.savedState.term, + tactic := { goals := unassigned }, + }, + } /-- Brings into scope all goals from `branch` -/ diff --git a/Repl.lean b/Repl.lean index a735c88..15a651d 100644 --- a/Repl.lean +++ b/Repl.lean @@ -321,9 +321,7 @@ def execute (command: Protocol.Command): MainM Json := do | .ok (.success nextGoalState) => do let nextGoalState ← match state.options.automaticMode, args.conv? with | true, .none => do - let .ok result := nextGoalState.resume (nextGoalState.goals ++ goalState.goals) | - Protocol.throw $ errorIO "Resuming known goals" - pure result + pure $ nextGoalState.immediateResume goalState | true, .some true => pure nextGoalState | true, .some false => do let .some (_, _, dormantGoals) := goalState.convMVar? |