|
| 1 | +/- |
| 2 | +Copyright (c) 2023 Kyle Miller. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Kyle Miller |
| 5 | +-/ |
| 6 | +import Lean |
| 7 | +import Std.Tactic.TryThis |
| 8 | + |
| 9 | +/-! |
| 10 | +# The `variable?` command |
| 11 | +
|
| 12 | +This defines a command like `variable` that automatically adds all missing typeclass |
| 13 | +arguments. For example, `variable? [Module R M]` is the same as |
| 14 | +`variable [Semiring R] [AddCommMonoid M] [Module R M]`, though if any of these three instance |
| 15 | +arguments can be inferred from previous variables then they will be omitted. |
| 16 | +
|
| 17 | +An inherent limitation with this command is that variables are recorded in the scope as |
| 18 | +*syntax*. This means that `variable?` needs to pretty print the expressions we get |
| 19 | +from typeclass synthesis errors, and these might fail to round trip. |
| 20 | +-/ |
| 21 | + |
| 22 | +namespace Mathlib.Command.Variable |
| 23 | +open Lean Elab Command Parser.Term Meta |
| 24 | + |
| 25 | +initialize registerTraceClass `variable? |
| 26 | + |
| 27 | +register_option variable?.maxSteps : Nat := |
| 28 | + { defValue := 15 |
| 29 | + group := "variable?" |
| 30 | + descr := |
| 31 | + "The maximum number of instance arguments `variable?` will try to insert before giving up" } |
| 32 | + |
| 33 | +register_option variable?.checkRedundant : Bool := |
| 34 | + { defValue := true |
| 35 | + group := "variable?" |
| 36 | + descr := "Warn if instance arguments can be inferred from preceding ones" } |
| 37 | + |
| 38 | +/-- Get the type out of a bracketed binder. -/ |
| 39 | +def bracketedBinderType : Syntax → Option Term |
| 40 | + | `(bracketedBinderF|($_* $[: $ty?]? $(_annot?)?)) => ty? |
| 41 | + | `(bracketedBinderF|{$_* $[: $ty?]?}) => ty? |
| 42 | + | `(bracketedBinderF|⦃$_* $[: $ty?]?⦄) => ty? |
| 43 | + | `(bracketedBinderF|[$[$_ :]? $ty]) => some ty |
| 44 | + | _ => none |
| 45 | + |
| 46 | +/-- The `variable?` command has the same syntax as `variable`, but it will auto-insert |
| 47 | +missing instance arguments wherever they are needed. |
| 48 | +It does not add variables that can already be deduced from others in the current context. |
| 49 | +By default the command checks that variables aren't implied by earlier ones, but it does *not* |
| 50 | +check that earlier variables aren't implied by later ones. |
| 51 | +Unlike `variable`, the `variable?` command does not support changing variable binder types. |
| 52 | +
|
| 53 | +The `variable?` command will give a suggestion to replace itself with a command of the form |
| 54 | +`variable? ...binders... => ...binders...`. The binders after the `=>` are the completed |
| 55 | +list of binders. When this `=>` clause is present, the command verifies that the expanded |
| 56 | +binders match the post-`=>` binders. The purpose of this is to help keep code that uses |
| 57 | +`variable?` resilient against changes to the typeclass hierarchy, at least in the sense |
| 58 | +that this additional information can be used to debug issues that might arise. |
| 59 | +One can also replace `variable? ...binders... =>` with `variable`. |
| 60 | +
|
| 61 | +The core algorithm is to try elaborating binders one at a time, and whenever there is a |
| 62 | +typeclass instance inference failure, it synthesizes binder syntax for it and adds it to |
| 63 | +the list of binders and tries again, recursively. There are no guarantees that this |
| 64 | +process gives the "correct" list of binders. |
| 65 | +
|
| 66 | +Structures tagged with the `variable_alias` attribute can serve as aliases for a collection |
| 67 | +of typeclasses. For example, given |
| 68 | +```lean |
| 69 | +@[variable_alias] |
| 70 | +structure VectorSpace (k V : Type _) [Field k] [AddCommGroup V] [Module k V] |
| 71 | +``` |
| 72 | +then `variable? [VectorSpace k V]` is |
| 73 | +equivalent to `variable {k V : Type _} [Field k] [AddCommGroup V] [Module k V]`, assuming |
| 74 | +that there are no pre-existing instances on `k` and `V`. |
| 75 | +Note that this is not a simple replacement: it only adds instances not inferrable |
| 76 | +from others in the current scope. |
| 77 | +
|
| 78 | +A word of warning: the core algorithm depends on pretty printing, so if terms that appear |
| 79 | +in binders do not round trip, this algorithm can fail. That said, it has some support |
| 80 | +for quantified binders such as `[∀ i, F i]`. -/ |
| 81 | +syntax (name := «variable?») |
| 82 | + "variable?" (ppSpace bracketedBinder)* (" =>" (ppSpace bracketedBinder)*)? : command |
| 83 | + |
| 84 | +/-- |
| 85 | +Attribute to record aliases for the `variable?` command. Aliases are structures that have no |
| 86 | +fields, and additional typeclasses are recorded as *arguments* to the structure. |
| 87 | +
|
| 88 | +Example: |
| 89 | +``` |
| 90 | +@[variable_alias] |
| 91 | +structure VectorSpace (k V : Type _) |
| 92 | + [Field k] [AddCommGroup V] [Module k V] |
| 93 | +``` |
| 94 | +Then `variable? [VectorSpace k V]` ensures that these three typeclasses are present in |
| 95 | +the current scope. Notice that it's looking at the arguments to the `VectorSpace` type |
| 96 | +constructor. You should not have any fields in `variable_alias` structures. |
| 97 | +
|
| 98 | +Notice that `VectorSpace` is not a class; the `variable?` command allows non-classes with the |
| 99 | +`variable_alias` attribute to use instance binders. |
| 100 | +-/ |
| 101 | +initialize variableAliasAttr : TagAttribute ← |
| 102 | + registerTagAttribute `variable_alias "Attribute to record aliases for the `variable?` command." |
| 103 | + |
| 104 | +/-- Find a synthetic typeclass metavariable with no expr metavariables in its type. -/ |
| 105 | +def pendingActionableSynthMVar (binder : TSyntax ``bracketedBinder) : |
| 106 | + TermElabM (Option MVarId) := do |
| 107 | + let pendingMVars := (← get).pendingMVars |
| 108 | + if pendingMVars.isEmpty then |
| 109 | + return none |
| 110 | + for mvarId in pendingMVars.reverse do |
| 111 | + let some decl ← Term.getSyntheticMVarDecl? mvarId | continue |
| 112 | + match decl.kind with |
| 113 | + | .typeClass => |
| 114 | + let ty ← instantiateMVars (← mvarId.getType) |
| 115 | + if !ty.hasExprMVar then |
| 116 | + return mvarId |
| 117 | + | _ => pure () |
| 118 | + throwErrorAt binder "Can not satisfy requirements for {binder} due to metavariables." |
| 119 | + |
| 120 | +/-- Try elaborating `ty`. Returns `none` if it doesn't need any additional typeclasses, |
| 121 | +or it returns a new binder that needs to come first. Does not add info unless it throws |
| 122 | +an exception. -/ |
| 123 | +partial def getSubproblem |
| 124 | + (binder : TSyntax ``bracketedBinder) (ty : Term) : |
| 125 | + TermElabM (Option (MessageData × TSyntax ``bracketedBinder)) := do |
| 126 | + let res : Term.TermElabResult (Option (MessageData × TSyntax ``bracketedBinder)) ← |
| 127 | + Term.observing do |
| 128 | + withTheReader Term.Context (fun ctx => {ctx with ignoreTCFailures := true}) do |
| 129 | + Term.withAutoBoundImplicit do |
| 130 | + _ ← Term.elabType ty |
| 131 | + Term.synthesizeSyntheticMVars (mayPostpone := true) (ignoreStuckTC := true) |
| 132 | + let fvarIds := (← getLCtx).getFVarIds |
| 133 | + if let some mvarId ← pendingActionableSynthMVar binder then |
| 134 | + trace[«variable?»] "Actionable mvar:{mvarId}" |
| 135 | + -- TODO alter goal based on configuration, for example Semiring -> CommRing. |
| 136 | + -- 1. Find the new fvars that this instance problem depends on: |
| 137 | + let fvarIds' := (← mvarId.getDecl).lctx.getFVarIds.filter |
| 138 | + (fun fvar => !(fvarIds.contains fvar)) |
| 139 | + -- 2. Abstract the instance problem with respect to these fvars |
| 140 | + let goal ← mvarId.withContext do instantiateMVars <| |
| 141 | + (← mkForallFVars (usedOnly := true) (fvarIds'.map .fvar) (← mvarId.getType)) |
| 142 | + -- Note: pretty printing is not guaranteed to round-trip, but it's what we can do. |
| 143 | + let ty' ← PrettyPrinter.delab goal |
| 144 | + let binder' ← withRef binder `(bracketedBinderF| [$ty']) |
| 145 | + return some (← addMessageContext m!"{mvarId}", binder') |
| 146 | + else |
| 147 | + return none |
| 148 | + match res with |
| 149 | + | .ok v _ => return v |
| 150 | + | .error .. => Term.applyResult res |
| 151 | + |
| 152 | +/-- Tries elaborating binders, inserting new binders whenever typeclass inference fails. |
| 153 | +`i` is the index of the next binder that needs to be checked. |
| 154 | +
|
| 155 | +The `toOmit` array keeps track of which binders should be removed at the end, |
| 156 | +in particular the `variable_alias` binders and any redundant binders. -/ |
| 157 | +partial def completeBinders' (maxSteps : Nat) (gas : Nat) |
| 158 | + (checkRedundant : Bool) |
| 159 | + (binders : TSyntaxArray ``bracketedBinder) |
| 160 | + (toOmit : Array Bool) (i : Nat) : |
| 161 | + TermElabM (TSyntaxArray ``bracketedBinder × Array Bool) := do |
| 162 | + if 0 < gas && i < binders.size then |
| 163 | + let binder := binders[i]! |
| 164 | + trace[«variable?»] |
| 165 | + "Have {(← getLCtx).getFVarIds.size} fvars and {(← getLocalInstances).size} local instances{ |
| 166 | + ""}. Looking at{indentD binder}" |
| 167 | + let sub? ← getSubproblem binder (bracketedBinderType binder).get! |
| 168 | + if let some (goalMsg, binder') := sub? then |
| 169 | + trace[«variable?»] m!"new subproblem:{indentD binder'}" |
| 170 | + if binders.any (stop := i) (· == binder') then |
| 171 | + let binders' := binders.extract 0 i |
| 172 | + throwErrorAt binder |
| 173 | + "Binder{indentD binder}\nwas not able to satisfy one of its dependencies using { |
| 174 | + ""}the pre-existing binder{indentD binder'}\n\n{ |
| 175 | + ""}This might be due to differences in implicit arguments, which are not represented { |
| 176 | + ""}in binders since they are generated by pretty printing unsatisfied dependencies.\n\n{ |
| 177 | + ""}Current variable command:{indentD (← `(command| variable $binders'*))}\n\n{ |
| 178 | + ""}Local context for the unsatisfied dependency:{goalMsg}" |
| 179 | + let binders := binders.insertAt! i binder' |
| 180 | + completeBinders' maxSteps (gas - 1) checkRedundant binders toOmit i |
| 181 | + else |
| 182 | + let lctx ← getLCtx |
| 183 | + let linst ← getLocalInstances |
| 184 | + withOptions (fun opts => Term.checkBinderAnnotations.set opts false) <| -- for variable_alias |
| 185 | + Term.withAutoBoundImplicit <| |
| 186 | + Term.elabBinders #[binder] fun bindersElab => do |
| 187 | + let types : Array Expr ← bindersElab.mapM (inferType ·) |
| 188 | + trace[«variable?»] m!"elaborated binder types array = {types}" |
| 189 | + Term.synthesizeSyntheticMVarsNoPostponing -- checkpoint for withAutoBoundImplicit |
| 190 | + Term.withoutAutoBoundImplicit do |
| 191 | + let (binders, toOmit) := ← do |
| 192 | + match binder with |
| 193 | + | `(bracketedBinderF|[$[$ident? :]? $ty]) => |
| 194 | + -- Check if it's an alias |
| 195 | + let type ← instantiateMVars (← inferType bindersElab.back) |
| 196 | + if ← isVariableAlias type then |
| 197 | + if ident?.isSome then |
| 198 | + throwErrorAt binder "`variable_alias` binders can't have an explicit name" |
| 199 | + -- Switch to implicit so that `elabBinders` succeeds. |
| 200 | + -- We keep it around so that it gets infotrees |
| 201 | + let binder' ← withRef binder `(bracketedBinderF|{_ : $ty}) |
| 202 | + return (binders.set! i binder', toOmit.push true) |
| 203 | + -- Check that this wasn't already an instance |
| 204 | + let res ← try withLCtx lctx linst <| trySynthInstance type catch _ => pure .none |
| 205 | + if let .some _ := res then |
| 206 | + if checkRedundant then |
| 207 | + let mvar ← mkFreshExprMVarAt lctx linst type |
| 208 | + logWarningAt binder |
| 209 | + m!"Instance argument can be inferred from earlier arguments.\n{mvar.mvarId!}" |
| 210 | + return (binders, toOmit.push true) |
| 211 | + else |
| 212 | + return (binders, toOmit.push false) |
| 213 | + | _ => return (binders, toOmit.push false) |
| 214 | + completeBinders' maxSteps gas checkRedundant binders toOmit (i + 1) |
| 215 | + else |
| 216 | + if gas == 0 && i < binders.size then |
| 217 | + let binders' := binders.extract 0 i |
| 218 | + logErrorAt binders[i]! m!"Maximum recursion depth for variables! reached. This might be a { |
| 219 | + ""}bug, or you can try adjusting `set_option variable?.maxSteps {maxSteps}`{ |
| 220 | + ""}\n\nCurrent variable command:{indentD (← `(command| variable $binders'*))}" |
| 221 | + return (binders, toOmit) |
| 222 | +where |
| 223 | + isVariableAlias (type : Expr) : MetaM Bool := do |
| 224 | + forallTelescope type fun _ type => do |
| 225 | + if let .const name _ := type.getAppFn then |
| 226 | + if variableAliasAttr.hasTag (← getEnv) name then |
| 227 | + return true |
| 228 | + return false |
| 229 | + |
| 230 | +def completeBinders (maxSteps : Nat) (checkRedundant : Bool) |
| 231 | + (binders : TSyntaxArray ``bracketedBinder) : |
| 232 | + TermElabM (TSyntaxArray ``bracketedBinder × Array Bool) := |
| 233 | + completeBinders' maxSteps maxSteps checkRedundant binders #[] 0 |
| 234 | + |
| 235 | +/-- Strip off whitespace and comments. -/ |
| 236 | +def cleanBinders (binders : TSyntaxArray ``bracketedBinder) : |
| 237 | + TSyntaxArray ``bracketedBinder := Id.run do |
| 238 | + let mut binders' := #[] |
| 239 | + for binder in binders do |
| 240 | + binders' := binders'.push <| ⟨binder.raw.unsetTrailing⟩ |
| 241 | + return binders' |
| 242 | + |
| 243 | +@[command_elab «variable?», inherit_doc «variable?»] |
| 244 | +def elabVariables : CommandElab := fun stx => |
| 245 | + match stx with |
| 246 | + | `(variable? $binders* $[=> $expectedBinders?*]?) => do |
| 247 | + let checkRedundant := variable?.checkRedundant.get (← getOptions) |
| 248 | + process stx checkRedundant binders expectedBinders? |
| 249 | + | _ => throwUnsupportedSyntax |
| 250 | +where |
| 251 | + extendScope (binders : TSyntaxArray ``bracketedBinder) : CommandElabM Unit := do |
| 252 | + for binder in binders do |
| 253 | + let varUIds ← getBracketedBinderIds binder |>.mapM |
| 254 | + (withFreshMacroScope ∘ MonadQuotation.addMacroScope) |
| 255 | + modifyScope fun scope => |
| 256 | + { scope with varDecls := scope.varDecls.push binder, varUIds := scope.varUIds ++ varUIds } |
| 257 | + process (stx : Syntax) (checkRedundant : Bool) |
| 258 | + (binders : TSyntaxArray ``bracketedBinder) |
| 259 | + (expectedBinders? : Option <| TSyntaxArray ``bracketedBinder) : CommandElabM Unit := do |
| 260 | + let binders := cleanBinders binders |
| 261 | + let maxSteps := variable?.maxSteps.get (← getOptions) |
| 262 | + trace[«variable?»] "variable?.maxSteps = {maxSteps}" |
| 263 | + for binder in binders do |
| 264 | + if (bracketedBinderType binder).isNone then |
| 265 | + throwErrorAt binder "variable? cannot update pre-existing variables" |
| 266 | + let (binders', suggest) ← runTermElabM fun _ => do |
| 267 | + let (binders, toOmit) ← completeBinders maxSteps checkRedundant binders |
| 268 | + /- Elaborate the binders again, which also adds the infotrees. |
| 269 | + This also makes sure the list works with auto-bound implicits at the front. -/ |
| 270 | + Term.withAutoBoundImplicit <| Term.elabBinders binders fun _ => pure () |
| 271 | + -- Filter out omitted binders |
| 272 | + let binders' : TSyntaxArray ``bracketedBinder := |
| 273 | + (binders.zip toOmit).filterMap fun (b, omit) => if omit then none else some b |
| 274 | + if let some expectedBinders := expectedBinders? then |
| 275 | + trace[«variable?»] "checking expected binders" |
| 276 | + /- We re-elaborate the biders to record expressions that represent the whole resulting |
| 277 | + local contexts (auto-bound implicits make it so we can't just use the argument to the |
| 278 | + function for `Term.elabBinders`). -/ |
| 279 | + let ctx1 ← Term.withAutoBoundImplicit <| Term.elabBinders binders' fun _ => do |
| 280 | + mkForallFVars (← getLCtx).getFVars (.sort .zero) |
| 281 | + let ctx2 ← Term.withAutoBoundImplicit <| Term.elabBinders expectedBinders fun _ => do |
| 282 | + mkForallFVars (← getLCtx).getFVars (.sort .zero) |
| 283 | + trace[«variable?»] "new context: {ctx1}" |
| 284 | + trace[«variable?»] "expected context: {ctx2}" |
| 285 | + if ← isDefEq ctx1 ctx2 then |
| 286 | + return (binders', false) |
| 287 | + else |
| 288 | + logWarning "Calculated binders do not match the expected binders given after `=>`." |
| 289 | + return (binders', true) |
| 290 | + else |
| 291 | + return (binders', true) |
| 292 | + extendScope binders' |
| 293 | + let varComm ← `(command| variable? $binders* => $binders'*) |
| 294 | + trace[«variable?»] "derived{indentD varComm}" |
| 295 | + if suggest then |
| 296 | + liftTermElabM <| Std.Tactic.TryThis.addSuggestion stx (origSpan? := stx) varComm |
| 297 | + |
| 298 | +/-- Hint for the unused variables linter. Copies the one for `variable`. -/ |
| 299 | +@[unused_variables_ignore_fn] |
| 300 | +def ignorevariable? : Lean.Linter.IgnoreFunction := fun _ stack _ => |
| 301 | + stack.matches [`null, none, `null, `Mathlib.Command.variable?] |
0 commit comments