From ebde7c9eed50d4cc29b235150cf5e4841f6dbc85 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 13 Jan 2025 10:20:36 -0800 Subject: [PATCH] feat: Prohibit coupling in drafting --- Pantograph/Frontend/Elab.lean | 5 +++++ Pantograph/Tactic/Assign.lean | 4 +++- 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean index 3da5fca..4ccb609 100644 --- a/Pantograph/Frontend/Elab.lean +++ b/Pantograph/Frontend/Elab.lean @@ -149,9 +149,14 @@ def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM AnnotatedGoalState match i.info with | .ofTermInfo termInfo => do let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context? + if (← mvarId.getType).hasSorry then + throwError s!"Coupling is not allowed in drafting" return [(mvarId, stxByteRange termInfo.stx)] | .ofTacticInfo tacticInfo => do let mvarIds ← MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context? + for mvarId in mvarIds do + if (← mvarId.getType).hasSorry then + throwError s!"Coupling is not allowed in drafting" let range := stxByteRange tacticInfo.stx return mvarIds.map (·, range) | _ => panic! "Invalid info" diff --git a/Pantograph/Tactic/Assign.lean b/Pantograph/Tactic/Assign.lean index d1dbf0c..c87dd46 100644 --- a/Pantograph/Tactic/Assign.lean +++ b/Pantograph/Tactic/Assign.lean @@ -30,7 +30,9 @@ def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do def sorryToHole (src : Expr) : StateRefT (List MVarId) MetaM Expr := do Meta.transform src λ | .app (.app (.const ``sorryAx ..) type) .. => do - -- FIXME: Handle cases of coupled goals + let type ← instantiateMVars type + if type.hasSorry then + throwError s!"Coupling is not allowed in draft tactic: {← Meta.ppExpr type}" let mvar ← Meta.mkFreshExprSyntheticOpaqueMVar type modify (mvar.mvarId! :: .) pure $ .done mvar