|
| 1 | +/- |
| 2 | +Copyright (c) 2026 Lua Viana Reis. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Lua Viana Reis |
| 5 | +-/ |
| 6 | +module |
| 7 | + |
| 8 | +public meta import Mathlib.Tactic.Set |
| 9 | +public meta import Lean.Elab.BuiltinTerm |
| 10 | + |
| 11 | +/-! |
| 12 | +# The `setm` tactic |
| 13 | +
|
| 14 | +This module defines the `setm` tactic. |
| 15 | +-/ |
| 16 | + |
| 17 | +public meta section |
| 18 | + |
| 19 | +open Lean Elab Tactic Meta Term Syntax |
| 20 | + |
| 21 | +namespace Mathlib.Tactic.SetM |
| 22 | + |
| 23 | +/-- This parser is declared inside a hidden namespace and should never be used. Its |
| 24 | +purpose is to register the ``Hidden.setmSyntheticHole` syntaax node kind in |
| 25 | +the environment. -/ |
| 26 | +scoped syntax:max (name := Hidden.setmSyntheticHole) |
| 27 | + "?" (ident <|> "_") : term |
| 28 | + |
| 29 | +open Hidden in |
| 30 | +/-- We give a distinguished name to the named holes appearing in the `setm` match pattern, |
| 31 | +to avoid unifying them with other metavariables in the context which have the same name. The |
| 32 | +distinguished name is reused across all holes with the same name in the pattern. -/ |
| 33 | +meta partial def wrapSyntheticHoles : Syntax → StateT (NameMap Name) TacticM Syntax := |
| 34 | + fun stx => do |
| 35 | + if stx.isOfKind ``Lean.Parser.Term.syntheticHole && stx[1].isIdent then |
| 36 | + let name ← |
| 37 | + if let .some old := (← get).get? stx[1].getId then |
| 38 | + pure old |
| 39 | + else |
| 40 | + let unique ← mkFreshUserName stx[1].getId |
| 41 | + modify (.insert · stx[1].getId unique) |
| 42 | + pure unique |
| 43 | + return stx.setKind ``setmSyntheticHole |>.setArg 1 (mkIdent name) |
| 44 | + match stx with |
| 45 | + | .node info kind args => return .node info kind (← args.mapM wrapSyntheticHoles) |
| 46 | + | _ => return stx |
| 47 | + |
| 48 | +open Hidden in |
| 49 | +/-- Elaborate the named `setm` holes, creating metavariables for them. -/ |
| 50 | +@[term_elab Hidden.setmSyntheticHole] |
| 51 | +def elabSetmSyntheticHole : Term.TermElab := fun stx expectedType? => do |
| 52 | + unless stx.isOfKind ``setmSyntheticHole do |
| 53 | + throwUnsupportedSyntax |
| 54 | + if let .ident _ _ n _ := stx[1] then |
| 55 | + -- Reuse metavariables in the context who have the same name. |
| 56 | + -- nb: at this point, they already have the distinguished names, so this is safe. |
| 57 | + for (id, decl) in (← getMCtx).decls do |
| 58 | + if decl.userName == n then return .mvar id |
| 59 | + let mvar ← mkFreshExprMVar expectedType? (userName := n) |
| 60 | + registerMVarErrorHoleInfo mvar.mvarId! stx |
| 61 | + return mvar |
| 62 | + else elabHole stx expectedType? |
| 63 | + |
| 64 | +syntax (name := setMStx) "setm " term (Parser.Tactic.location)? : tactic |
| 65 | + |
| 66 | +-- This code was copied from the `change` tactic in core. I am not sure if in our context, |
| 67 | +-- all of it is necessary (could there be other synthetic opaque MVars that were not holes?). |
| 68 | +meta def elabSetM (e : Expr) (p : Syntax) : TacticM Expr := do |
| 69 | + let p ← runTermElab do |
| 70 | + let p ← Term.elabTermEnsuringType p (← inferType e) |
| 71 | + unless ← isDefEq p e do |
| 72 | + Term.synthesizeSyntheticMVars (postpone := .partial) |
| 73 | + discard <| isDefEq p e |
| 74 | + pure p |
| 75 | + withAssignableSyntheticOpaque do |
| 76 | + unless ← isDefEq p e do |
| 77 | + throwError MessageData.ofLazyM (es := #[p, e]) do |
| 78 | + let (p, tgt) ← addPPExplicitToExposeDiff p e |
| 79 | + return m!"setm: pattern{indentExpr p}\nis not defeq to goal{indentExpr tgt}" |
| 80 | + return ← instantiateMVars p |
| 81 | + |
| 82 | +@[tactic setMStx] |
| 83 | +meta def evalSetM : Tactic |
| 84 | + | `(tactic| setm $pat:term $[$loc:location]?) => withReducibleAndInstances do |
| 85 | + let (pat, names) ← StateT.run (wrapSyntheticHoles pat) .empty |
| 86 | + let locations := expandOptLocation (Lean.mkOptionalNode loc) |
| 87 | + -- First, unify the pattern with the target of each location. |
| 88 | + withLocation locations |
| 89 | + (atLocal := unify pat ∘ .some) |
| 90 | + (atTarget := unify pat .none) |
| 91 | + (failed := fun _ ↦ throwError "'setm' tactic failed") |
| 92 | + -- Now, make a mapping of hole names to the metavariables that appeared in the pattern. |
| 93 | + let mctx ← getMCtx |
| 94 | + let mvars : NameMap MVarId := mctx.decls.foldl (init := {}) fun acc id decl => |
| 95 | + if let Option.some n := Id.run <| do |
| 96 | + for (n, un) in names do |
| 97 | + if un == decl.userName then return .some n |
| 98 | + return .none |
| 99 | + then acc.insert n id |
| 100 | + else acc |
| 101 | + -- Finally, for each metavariable... |
| 102 | + for (n, m) in mvars do |
| 103 | + -- ... instantiate it and introduce a let into the context... |
| 104 | + let val ← instantiateMVars (.mvar m) |
| 105 | + let ty ← m.getType' |
| 106 | + let fvar ← liftMetaTacticAux fun goal ↦ do |
| 107 | + let (fvar, goal) ← (← goal.define n ty val).intro1P |
| 108 | + return (fvar, [goal]) |
| 109 | + -- ... and rewrite the introduced decl in each one of the locations. |
| 110 | + withLocation locations |
| 111 | + (atLocal := rewrite fvar val ∘ .some) |
| 112 | + (atTarget := rewrite fvar val .none) |
| 113 | + (failed := fun _ ↦ throwError "'setm' tactic failed") |
| 114 | + | _ => throwUnsupportedSyntax |
| 115 | + where |
| 116 | + unify (pat : Syntax) (lvar : Option FVarId) : TacticM Unit := do |
| 117 | + let e ← if let .some l := lvar |
| 118 | + then l.getType |
| 119 | + else getMainTarget |
| 120 | + let tgt ← elabSetM e pat |
| 121 | + liftMetaTactic fun goal => do |
| 122 | + return [← changeDecl goal tgt lvar] |
| 123 | + rewrite (fvar : FVarId) (val : Expr) (lvar : Option FVarId) : TacticM Unit := do |
| 124 | + liftMetaTactic fun goal ↦ do |
| 125 | + let tgt ← instantiateMVars (← lvar.elim goal.getType (·.getType)) |
| 126 | + let absTgt ← kabstract tgt val |
| 127 | + let goal ← if absTgt.hasLooseBVars |
| 128 | + then changeDecl goal (absTgt.instantiate1 (.fvar fvar)) lvar |
| 129 | + else pure goal |
| 130 | + return [goal] |
| 131 | + changeDecl (goal : MVarId) (tgt : Expr) (l? : Option FVarId := .none) : MetaM MVarId := |
| 132 | + match l? with |
| 133 | + | .some fvar => do |
| 134 | + let lctx := (← goal.getDecl).lctx.modifyLocalDecl fvar |
| 135 | + fun d ↦ d.setType tgt |
| 136 | + goal.modifyLCtx (fun _ ↦ lctx) |
| 137 | + return goal |
| 138 | + | .none => goal.replaceTargetDefEq tgt |
| 139 | + |
| 140 | +end Mathlib.Tactic.SetM |
0 commit comments