doc-next-gen

Mathlib.Tactic.Variable

Module docstring

{"# The variable? command

This defines a command like variable that automatically adds all missing typeclass arguments. For example, variable? [Module R M] is the same as variable [Semiring R] [AddCommMonoid M] [Module R M], though if any of these three instance arguments can be inferred from previous variables then they will be omitted.

An inherent limitation with this command is that variables are recorded in the scope as syntax. This means that variable? needs to pretty print the expressions we get from typeclass synthesis errors, and these might fail to round trip. "}

Mathlib.Command.Variable.variable?.checkRedundant opaque
: Lean.Option✝ Bool
Full source 
register_option variable?.checkRedundant : Bool :=
  { defValue := true
    group := "variable?"
    descr := "Warn if instance arguments can be inferred from preceding ones" }
Redundancy Check Option for `variable?` Command
Informal description
The option `variable?.checkRedundant` is a boolean flag that determines whether the `variable?` command should check for redundant typeclass arguments when automatically adding missing instances.
Mathlib.Command.Variable.bracketedBinderType definition
: Syntax → Option Term
Full source 
/-- Get the type out of a bracketed binder. -/
def bracketedBinderType : Syntax → Option Term
  | `(bracketedBinderF|($_* $[: $ty?]? $(_annot?)?)) => ty?
  | `(bracketedBinderF|{$_* $[: $ty?]?})             => ty?
  | `(bracketedBinderF|⦃$_* $[: $ty?]?⦄)             => ty?
  | `(bracketedBinderF|[$[$_ :]? $ty])               => some ty
  | _                                                => none
Extract type from bracketed binder
Informal description
The function extracts the type from a bracketed binder syntax in Lean. It handles various forms of bracketed binders including parentheses `()`, curly braces `{}`, double curly braces `⦃⦄`, and square brackets `[]`. For each form, it returns the type component if present, otherwise it returns `none`.
Mathlib.Command.Variable.variable? definition
: Lean.ParserDescr✝
Full source 
/-- The `variable?` command has the same syntax as `variable`, but it will auto-insert
missing instance arguments wherever they are needed.
It does not add variables that can already be deduced from others in the current context.
By default the command checks that variables aren't implied by earlier ones, but it does *not*
check that earlier variables aren't implied by later ones.
Unlike `variable`, the `variable?` command does not support changing variable binder types.

The `variable?` command will give a suggestion to replace itself with a command of the form
`variable? ...binders... => ...binders...`.  The binders after the `=>` are the completed
list of binders. When this `=>` clause is present, the command verifies that the expanded
binders match the post-`=>` binders.  The purpose of this is to help keep code that uses
`variable?` resilient against changes to the typeclass hierarchy, at least in the sense
that this additional information can be used to debug issues that might arise.
One can also replace `variable? ...binders... =>` with `variable`.

The core algorithm is to try elaborating binders one at a time, and whenever there is a
typeclass instance inference failure, it synthesizes binder syntax for it and adds it to
the list of binders and tries again, recursively. There are no guarantees that this
process gives the "correct" list of binders.

Structures tagged with the `variable_alias` attribute can serve as aliases for a collection
of typeclasses. For example, given
```lean
@[variable_alias]
structure VectorSpace (k V : Type*) [Field k] [AddCommGroup V] [Module k V]
```
then `variable? [VectorSpace k V]` is
equivalent to `variable {k V : Type*} [Field k] [AddCommGroup V] [Module k V]`, assuming
that there are no pre-existing instances on `k` and `V`.
Note that this is not a simple replacement: it only adds instances not inferable
from others in the current scope.

A word of warning: the core algorithm depends on pretty printing, so if terms that appear
in binders do not round trip, this algorithm can fail. That said, it has some support
for quantified binders such as `[∀ i, F i]`. -/
syntax (name := «variable?»)
  "variable?" (ppSpace bracketedBinder)* (" =>" (ppSpace bracketedBinder)*)? : command
Automatic typeclass variable insertion command (`variable?`)
Informal description
The `variable?` command is a variant of the `variable` command that automatically inserts missing typeclass arguments when needed. It does not add variables that can already be inferred from the current context. The command provides a suggestion to replace itself with a completed list of binders, which helps maintain code resilience against changes in the typeclass hierarchy. Structures tagged with the `variable_alias` attribute can serve as aliases for collections of typeclasses, allowing `variable?` to expand them into their constituent typeclass instances when needed.
Mathlib.Command.Variable.variableAliasAttr opaque
: TagAttribute
Full source 
/--
Attribute to record aliases for the `variable?` command. Aliases are structures that have no
fields, and additional typeclasses are recorded as *arguments* to the structure.

Example:
```
@[variable_alias]
structure VectorSpace (k V : Type*)
  [Field k] [AddCommGroup V] [Module k V]
```
Then `variable? [VectorSpace k V]` ensures that these three typeclasses are present in
the current scope. Notice that it's looking at the arguments to the `VectorSpace` type
constructor. You should not have any fields in `variable_alias` structures.

Notice that `VectorSpace` is not a class; the `variable?` command allows non-classes with the
`variable_alias` attribute to use instance binders.
-/
initialize variableAliasAttr : TagAttribute ←
  registerTagAttribute `variable_alias "Attribute to record aliases for the `variable?` command."
`variable_alias` Attribute for `variable?` Command
Informal description
The `variable_alias` attribute is used to record aliases for the `variable?` command, which allows for automatic inclusion of missing typeclass arguments. Structures marked with this attribute must have no fields, and additional typeclasses are recorded as arguments to the structure.
Mathlib.Command.Variable.pendingActionableSynthMVar definition
(binder : TSyntax `` bracketedBinder) : TermElabM (Option MVarId)
Full source 
/-- Find a synthetic typeclass metavariable with no expr metavariables in its type. -/
def pendingActionableSynthMVar (binder : TSyntax ``bracketedBinder) :
    TermElabM (Option MVarId) := do
  let pendingMVars := (← get).pendingMVars
  if pendingMVars.isEmpty then
    return none
  for mvarId in pendingMVars.reverse do
    let some decl ← Term.getSyntheticMVarDecl? mvarId | continue
    match decl.kind with
    | .typeClass _ =>
      let ty ← instantiateMVars (← mvarId.getType)
      if !ty.hasExprMVar then
        return mvarId
    | _ => pure ()
  throwErrorAt binder "Can not satisfy requirements for {binder} due to metavariables."
Pending actionable typeclass metavariable finder
Informal description
The function searches for a typeclass metavariable that has no metavariables in its type, among the pending metavariables in the current context. If found, it returns the metavariable identifier; otherwise, it returns `none`. If the search fails due to unresolved metavariables in the type, it raises an error indicating that the requirements for the given binder cannot be satisfied.
Mathlib.Command.Variable.getSubproblem definition
(binder : TSyntax `` bracketedBinder) (ty : Term) : TermElabM (Option (MessageData × TSyntax `` bracketedBinder))
Full source 
/-- Try elaborating `ty`. Returns `none` if it doesn't need any additional typeclasses,
or it returns a new binder that needs to come first. Does not add info unless it throws
an exception. -/
partial def getSubproblem
    (binder : TSyntax ``bracketedBinder) (ty : Term) :
    TermElabM (Option (MessageDataMessageData × TSyntax ``bracketedBinder)) := do
  let res : Term.TermElabResult (Option (MessageData × TSyntax ``bracketedBinder)) ←
    Term.observing do
    withTheReader Term.Context (fun ctx => {ctx with ignoreTCFailures := true}) do
    Term.withAutoBoundImplicit do
      _ ← Term.elabType ty
      Term.synthesizeSyntheticMVars (postpone := .yes) (ignoreStuckTC := true)
      let fvarIds := (← getLCtx).getFVarIds
      if let some mvarId ← pendingActionableSynthMVar binder then
        trace[«variable?»] "Actionable mvar:{mvarId}"
        -- TODO alter goal based on configuration, for example Semiring -> CommRing.
        -- 1. Find the new fvars that this instance problem depends on:
        let fvarIds' := (← mvarId.getDecl).lctx.getFVarIds.filter
                          (fun fvar => !(fvarIds.contains fvar))
        -- 2. Abstract the instance problem with respect to these fvars
        let goal ← mvarId.withContext do instantiateMVars <|
                    (← mkForallFVars (usedOnly := true) (fvarIds'.map .fvar) (← mvarId.getType))
        -- Note: pretty printing is not guaranteed to round-trip, but it's what we can do.
        let ty' ← PrettyPrinter.delab goal
        let binder' ← withRef binder `(bracketedBinderF| [$ty'])
        return some (← addMessageContext m!"{mvarId}", binder')
      else
        return none
  match res with
  | .ok v _ => return v
  | .error .. => Term.applyResult res
Typeclass subproblem finder for variable command
Informal description
The function attempts to elaborate a type `ty` and returns either `none` if no additional typeclasses are needed, or a pair consisting of an error message and a new binder that needs to be added first. It operates in a context where typeclass failures are ignored and automatically binds implicit variables. If there is a pending actionable typeclass metavariable (a typeclass goal that can be solved immediately), it processes this metavariable by: 1. Identifying new free variables that this instance depends on 2. Abstracting the instance problem with respect to these variables 3. Creating a new binder syntax for the abstracted problem 4. Returning the metavariable's context message and the new binder If no actionable metavariable is found, it returns `none`. The function is used internally by the `variable?` command to handle automatic insertion of missing typeclass arguments.
Mathlib.Command.Variable.completeBinders' definition
(maxSteps : Nat) (gas : Nat) (checkRedundant : Bool) (binders : TSyntaxArray `` bracketedBinder) (toOmit : Array Bool) (i : Nat) : TermElabM (TSyntaxArray `` bracketedBinder × Array Bool)
Full source 
/-- Tries elaborating binders, inserting new binders whenever typeclass inference fails.
`i` is the index of the next binder that needs to be checked.

The `toOmit` array keeps track of which binders should be removed at the end,
in particular the `variable_alias` binders and any redundant binders. -/
partial def completeBinders' (maxSteps : Nat) (gas : Nat)
    (checkRedundant : Bool)
    (binders : TSyntaxArray ``bracketedBinder)
    (toOmit : Array Bool) (i : Nat) :
    TermElabM (TSyntaxArrayTSyntaxArray ``bracketedBinder × Array Bool) := do
  if h : 0 < gas ∧ i < binders.size then
    let binder := binders[i]
    trace[«variable?»] "\
      Have {(← getLCtx).getFVarIds.size} fvars and {(← getLocalInstances).size} local instances. \
      Looking at{indentD binder}"
    let sub? ← getSubproblem binder (bracketedBinderType binder).get!
    if let some (goalMsg, binder') := sub? then
      trace[«variable?»] m!"new subproblem:{indentD binder'}"
      if binders.any (stop := i) (· == binder') then
        let binders' := binders.extract 0 i
        throwErrorAt binder "\
          Binder{indentD binder}\nwas not able to satisfy one of its dependencies using \
          the pre-existing binder{indentD binder'}\n\n\
          This might be due to differences in implicit arguments, which are not represented \
          in binders since they are generated by pretty printing unsatisfied dependencies.\n\n\
          Current variable command:{indentD (← `(command| variable $binders'*))}\n\n\
          Local context for the unsatisfied dependency:{goalMsg}"
      let binders := binders.insertIdx i binder'
      completeBinders' maxSteps (gas - 1) checkRedundant binders toOmit i
    else
      let lctx ← getLCtx
      let linst ← getLocalInstances
      withOptions (fun opts => Term.checkBinderAnnotations.set opts false) <| -- for variable_alias
      Term.withAutoBoundImplicit <|
      Term.elabBinders #[binder] fun bindersElab => do
        let types : Array Expr ← bindersElab.mapM (inferType ·)
        trace[«variable?»] m!"elaborated binder types array = {types}"
        Term.synthesizeSyntheticMVarsNoPostponing -- checkpoint for withAutoBoundImplicit
        Term.withoutAutoBoundImplicit do
        let (binders, toOmit) := ← do
          match binder with
          | `(bracketedBinderF|[$[$ident? :]? $ty]) =>
            -- Check if it's an alias
            let type ← instantiateMVars (← inferType bindersElab.back!)
            if ← isVariableAlias type then
              if ident?.isSome then
                throwErrorAt binder "`variable_alias` binders can't have an explicit name"
              -- Switch to implicit so that `elabBinders` succeeds.
              -- We keep it around so that it gets infotrees
              let binder' ← withRef binder `(bracketedBinderF|{_ : $ty})
              return (binders.set! i binder', toOmit.push true)
            -- Check that this wasn't already an instance
            let res ← try withLCtx lctx linst <| trySynthInstance type catch _ => pure .none
            if let .some _ := res then
              if checkRedundant then
                let mvar ← mkFreshExprMVarAt lctx linst type
                logWarningAt binder
                  m!"Instance argument can be inferred from earlier arguments.\n{mvar.mvarId!}"
              return (binders, toOmit.push true)
            else
              return (binders, toOmit.push false)
          | _ => return (binders, toOmit.push false)
        completeBinders' maxSteps gas checkRedundant binders toOmit (i + 1)
  else
    if h : gas = 0 ∧ i < binders.size then
      let binders' := binders.extract 0 i
      logErrorAt binders[i] m!"Maximum recursion depth for variables! reached. This might be a \
        bug, or you can try adjusting `set_option variable?.maxSteps {maxSteps}`\n\n\
        Current variable command:{indentD (← `(command| variable $binders'*))}"
    return (binders, toOmit)
where
  isVariableAlias (type : Expr) : MetaM Bool := do
    forallTelescope type fun _ type => do
      if let .const name _ := type.getAppFn then
        if variableAliasAttr.hasTag (← getEnv) name then
          return true
      return false
Binder completion helper for variable? command
Informal description
The function `completeBinders'` is an internal helper function used by the `variable?` command. It processes an array of binders (syntax elements representing variable declarations), attempting to elaborate them while automatically inserting any missing typeclass arguments. The function takes parameters including: - `maxSteps`: maximum recursion depth - `gas`: remaining steps counter - `checkRedundant`: flag to check for redundant binders - `binders`: array of binder syntax elements to process - `toOmit`: array tracking which binders should be omitted - `i`: current index in the binders array The function works recursively, handling each binder in sequence. For each binder, it: 1. Checks for subproblems (missing dependencies) 2. Handles special cases like `variable_alias` binders 3. Checks if the binder can be inferred from context 4. Updates the binders array and omission tracking array accordingly
Mathlib.Command.Variable.completeBinders definition
(maxSteps : Nat) (checkRedundant : Bool) (binders : TSyntaxArray `` bracketedBinder) : TermElabM (TSyntaxArray `` bracketedBinder × Array Bool)
Full source 
def completeBinders (maxSteps : Nat) (checkRedundant : Bool)
    (binders : TSyntaxArray ``bracketedBinder) :
    TermElabM (TSyntaxArrayTSyntaxArray ``bracketedBinder × Array Bool) :=
  completeBinders' maxSteps maxSteps checkRedundant binders #[] 0
Binder completion with automatic typeclass insertion
Informal description
The function `completeBinders` processes an array of syntax binders (variable declarations) by automatically inserting any missing typeclass arguments. It takes parameters: - `maxSteps`: maximum recursion depth - `checkRedundant`: flag to check for redundant binders - `binders`: array of binder syntax elements to process The function returns a pair consisting of: 1. The processed array of binders with missing typeclass arguments added 2. A boolean array indicating which binders were omitted (when they could be inferred from context) This is a wrapper function that initializes the recursive processing performed by `completeBinders'`.
Mathlib.Command.Variable.cleanBinders definition
(binders : TSyntaxArray `` bracketedBinder) : TSyntaxArray `` bracketedBinder
Full source 
/-- Strip off whitespace and comments. -/
def cleanBinders (binders : TSyntaxArray ``bracketedBinder) :
    TSyntaxArray ``bracketedBinder := Id.run do
  let mut binders' := #[]
  for binder in binders do
    binders' := binders'.push <| ⟨binder.raw.unsetTrailing⟩
  return binders'
Clean syntax binders
Informal description
The function removes trailing whitespace and comments from an array of syntax objects representing binders.
Mathlib.Command.Variable.elabVariables definition
: CommandElab
Full source 
@[command_elab «variable?», inherit_doc «variable?»]
def elabVariables : CommandElab := fun stx =>
  match stx with
  | `(variable? $binders* $[=> $expectedBinders?*]?) => do
    let checkRedundant := variable?.checkRedundant.get (← getOptions)
    process stx checkRedundant binders expectedBinders?
  | _ => throwUnsupportedSyntax
where
  extendScope (binders : TSyntaxArray ``bracketedBinder) : CommandElabM Unit := do
    for binder in binders do
      let varUIds ← (← getBracketedBinderIds binder) |>.mapM
        (withFreshMacroScope ∘ MonadQuotation.addMacroScope)
      modifyScope fun scope =>
        { scope with varDecls := scope.varDecls.push binder, varUIds := scope.varUIds ++ varUIds }
  process (stx : Syntax) (checkRedundant : Bool)
      (binders : TSyntaxArray ``bracketedBinder)
      (expectedBinders? : Option <| TSyntaxArray ``bracketedBinder) : CommandElabM Unit := do
    let binders := cleanBinders binders
    let maxSteps := variable?.maxSteps.get (← getOptions)
    trace[«variable?»] "variable?.maxSteps = {maxSteps}"
    for binder in binders do
      if (bracketedBinderType binder).isNone then
        throwErrorAt binder "variable? cannot update pre-existing variables"
    let (binders', suggest) ← runTermElabM fun _ => do
      let (binders, toOmit) ← completeBinders maxSteps checkRedundant binders
      /- Elaborate the binders again, which also adds the infotrees.
      This also makes sure the list works with auto-bound implicits at the front. -/
      Term.withAutoBoundImplicit <| Term.elabBinders binders fun _ => pure ()
      -- Filter out omitted binders
      let binders' : TSyntaxArray ``bracketedBinder :=
        (binders.zip toOmit).filterMap fun (b, toOmit) => if toOmit then none else some b
      if let some expectedBinders := expectedBinders? then
        trace[«variable?»] "checking expected binders"
        /- We re-elaborate the binders to create an expression that represents the entire resulting
        local context (auto-bound implicits mean we can't just the `binders` array). -/
        let elabAndPackageBinders (binders : TSyntaxArray ``bracketedBinder) :
            TermElabM AbstractMVarsResult :=
          withoutModifyingStateWithInfoAndMessages <| Term.withAutoBoundImplicit <|
            Term.elabBinders binders fun _ => do
              let e ← mkForallFVars (← getLCtx).getFVars (.sort .zero)
              let res ← abstractMVars e
              -- Throw in the level names from the current state since `Type*` produces new
              -- level names.
              return {res with paramNames := (← get).levelNames.toArray ++ res.paramNames}
        let ctx1 ← elabAndPackageBinders binders'
        let ctx2 ← elabAndPackageBinders expectedBinders
        trace[«variable?»] "new context: paramNames = {ctx1.paramNames}, {
          ""}numMVars = {ctx1.numMVars}\n{indentD ctx1.expr}"
        trace[«variable?»] "expected context: paramNames = {ctx2.paramNames}, {
          ""}numMVars = {ctx2.numMVars}\n{indentD ctx2.expr}"
        if ctx1.paramNames == ctx2.paramNames && ctx1.numMVars == ctx2.numMVars then
          if ← isDefEq ctx1.expr ctx2.expr then
            return (binders', false)
        logWarning "Calculated binders do not match the expected binders given after `=>`."
        return (binders', true)
      else
        return (binders', true)
    extendScope binders'
    let varComm ← `(command| variable? $binders* => $binders'*)
    trace[«variable?»] "derived{indentD varComm}"
    if suggest then
      liftTermElabM <| Lean.Meta.Tactic.TryThis.addSuggestion stx (origSpan? := stx) varComm
Automatic typeclass variable declaration command
Informal description
The command `variable?` automatically adds missing typeclass arguments when declaring variables. For example, `variable? [Module R M]` will implicitly add `[Semiring R] [AddCommMonoid M]` if they aren't already present, unless they can be inferred from context. The command processes syntax binders, completes them with necessary typeclass instances, and extends the current scope with these declarations.
Mathlib.Command.Variable.ignorevariable? definition
: Lean.Linter.IgnoreFunction
Full source 
/-- Hint for the unused variables linter. Copies the one for `variable`. -/
@[unused_variables_ignore_fn]
def ignorevariable? : Lean.Linter.IgnoreFunction := fun _ stack _ =>
  stack.matches [`null, none, `null, ``Mathlib.Command.Variable.variable?]
  || stack.matches [`null, none, `null, `null, ``Mathlib.Command.Variable.variable?]
Ignore function for unused variables in `variable?` command
Informal description
A function that serves as a hint for the unused variables linter, specifically designed to ignore variables declared using the `variable?` command. It checks the call stack to determine if the current context involves the `variable?` command, and if so, it signals the linter to ignore the unused variables in this context.