opaque Lean.Meta.Sym.sym.debug : Lean.Option Bool

Sym Extensions

Extensible state mechanism for SymM, allowing modules to register persistent state that lives across simp invocations within a sym => block. Follows the same pattern as Grind.SolverExtension in Lean/Meta/Tactic/Grind/Types.lean.

opaque Lean.Meta.Sym.SymExtensionStateSpec : (α : Type) × Inhabited α

Opaque extension state type used to store type-erased extension values.

def Lean.Meta.Sym.SymExtensionState : Type

@[instance_reducible]

instance Lean.Meta.Sym.instInhabitedSymExtensionState : Inhabited SymExtensionState

structure Lean.Meta.Sym.SymExtension (σ : Type) : Type

A registered extension for SymM. Each extension gets a unique index into the extensions array in Sym.State. Can only be created via registerSymExtension.

• id : Nat
• mkInitial : IO σ

@[instance_reducible]

instance Lean.Meta.Sym.instInhabitedSymExtension {a✝ : Type} : Inhabited (SymExtension a✝)

def Lean.Meta.Sym.registerSymExtension {σ : Type} (mkInitial : IO σ) : IO (SymExtension σ)

Registers a new SymM state extension. Extensions can only be registered during initialization. Returns a handle for typed access to the extension's state.

def Lean.Meta.Sym.SymExtensions.mkInitialStates : IO (Array SymExtensionState)

Returns initial state for all registered extensions.

structure Lean.Meta.Sym.ProofInstArgInfo : Type

Information about a single argument position in a function's type signature.

This is used during pattern matching and structural definitional equality tests to identify arguments that can be skipped or handled specially (e.g., instance arguments can be synthesized, proof arguments can be inferred).

• isProof : Bool

  true if this argument is a proof (its type is a Prop).

• isInstance : Bool

  true if this argument is a type class instance.

@[instance_reducible]

instance Lean.Meta.Sym.instInhabitedProofInstArgInfo : Inhabited ProofInstArgInfo

structure Lean.Meta.Sym.ProofInstInfo : Type

Information about a function symbol. It stores which argument positions are proofs or instances, enabling optimizations during pattern matching and structural definitional equality tests such as skipping proof arguments or deferring instance synthesis.

• argsInfo : Array ProofInstArgInfo

  Information about each argument position.

@[instance_reducible]

instance Lean.Meta.Sym.instInhabitedProofInstInfo : Inhabited ProofInstInfo

inductive Lean.Meta.Sym.CongrInfo : Type

Information on how to build congruence proofs for function applications. This enables efficient rewriting of subterms without repeatedly inferring types or instances.

• none : CongrInfo

  None of the arguments of the function can be rewritten.

• fixedPrefix (prefixSize suffixSize : Nat) : CongrInfo

  For functions with a fixed prefix of implicit/instance arguments followed by explicit non-dependent arguments that can be rewritten independently.

  • prefixSize: Number of leading arguments (types, instances) that are determined by the suffix arguments and should not be rewritten directly.
  • suffixSize: Number of trailing arguments that can be rewritten using simple congruence.

  Examples (showing prefixSize, suffixSize):

  • HAdd.hAdd {α β γ} [HAdd α β γ] (a : α) (b : β): (4, 2) — rewrite a and b
  • And (p q : Prop): (0, 2) — rewrite both propositions
  • Eq {α} (a b : α): (1, 2) — rewrite a and b, type α is fixed
  • Neg.neg {α} [Neg α] (a : α): (2, 1) — rewrite just a
• interlaced (rewritable : Array Bool) : CongrInfo

  For functions with interlaced rewritable and non-rewritable arguments. Each element indicates whether the corresponding argument position can be rewritten.

  Example: For HEq {α : Sort u} (a : α) {β : Sort u} (b : β), the mask would be #[false, true, false, true] — we can rewrite a and b, but not α or β.

• congrTheorem (thm : CongrTheorem) : CongrInfo

  For functions that have proofs and Decidable arguments. For this kind of function we generate a custom theorem. Example: Array.eraseIdx {α : Type u} (xs : Array α) (i : Nat) (h : i < xs.size) : Array α. The proof argument h depends on xs and i. To be able to rewrite xs and i, we use the auto-generated theorem.

  Array.eraseIdx.congr_simp {α : Type u} (xs xs' : Array α) (e_xs : xs = xs')
      (i i' : Nat) (e_i : i = i') (h : i < xs.size) : xs.eraseIdx i h = xs'.eraseIdx i' ⋯
  

structure Lean.Meta.Sym.SharedExprs : Type

Pre-shared expressions for commonly used terms.

• trueExpr : Expr
• falseExpr : Expr
• natZExpr : Expr
• btrueExpr : Expr
• bfalseExpr : Expr
• ordEqExpr : Expr
• intExpr : Expr

structure Lean.Meta.Sym.Config : Type

Configuration options for the symbolic computation framework.

• verbose : Bool

  When true, issues are collected during proof search and reported on failure.

• enforceUnfoldReducible : Bool

  When true, shareCommon maintains the SymM invariant that reducible constants have been eagerly unfolded: if a new term contains one, shareCommon unfolds it before adding the term to the table of maximally shared terms.

• enforceFoldProjs : Bool

  When true, shareCommon maintains the SymM invariant that kernel projections have been folded into projection function applications: if a new term contains one, shareCommon folds it before adding the term to the table of maximally shared terms. cbv disables this check because it processes kernel projections natively.

@[instance_reducible]

instance Lean.Meta.Sym.instInhabitedConfig : Inhabited Config

structure Lean.Meta.Sym.Context : Type

Readonly context for the symbolic computation framework.

• sharedExprs : SharedExprs
• config : Config

structure Lean.Meta.Sym.Canon.State : Type

• cache : Std.HashMap Expr Expr

  Cache for value-level canonicalization (no type reductions applied).

• cacheInType : Std.HashMap Expr Expr

  Cache for type-level canonicalization (reductions applied).

structure Lean.Meta.Sym.State : Type

Mutable state for the symbolic computation framework.

• share : AlphaShareCommon.State

  ShareCommon (aka Hash-consing) state.

• maxFVar : PHashMap ExprPtr (Option FVarId)

  Maps expressions to their maximal free variable (by declaration index).

  • maxFVar[e] = some fvarId means fvarId is the free variable with the largest declaration index occurring in e.
  • maxFVar[e] = none means e contains no free variables (but may contain metavariables).

  Recall that if e contains a metavariable ?m, then we assume e may contain any free variable in the local context associated with ?m.

  This mapping enables O(1) local context compatibility checks during metavariable assignment. Instead of traversing local contexts with isSubPrefixOf, we check if the maximal free variable in the assigned value is in scope of the metavariable's local context.

  Note: We considered using a mapping PHashMap ExprPtr FVarId. However, there is a corner case that is not supported by this representation. e contains a metavariable (with an empty local context), and no free variables.

• proofInstInfo : PHashMap Name (Option ProofInstInfo)
• inferType : PHashMap ExprPtr Expr

  Cache for inferType results, keyed by pointer equality. SymM uses a fixed configuration, so we can use a simpler key than MetaM. Remark: type inference is a bottleneck on Meta.Tactic.Simp simplifier.

• getLevel : PHashMap ExprPtr Level

  Cache for getLevel results, keyed by pointer equality.

• congrInfo : PHashMap ExprPtr CongrInfo
• defEqI : PHashMap (ExprPtr × ExprPtr) Bool

  Cache for isDefEqI results

• extensions : Array SymExtensionState

  State for registered SymExtensions, indexed by extension id.

• issues : List MessageData

  Issues found during symbolic computation. Accumulated across operations within a sym => block and reported when a tactic fails.

• canon : Canon.State
• instanceOverrides : PHashMap Expr Expr

  Instances registered by satellite modules for types they create themselves (e.g., grind linarith's envelope type IntModule.OfNatModule.Q). Sym.synthInstance? consults this table (keyed by the instance type, structural equality) before running typeclass resolution. This both skips searches whose results are known in advance, and ensures the registered term is used as the canonical representative.

  We currently use this table to reduce the overhead of type class resolution in grind.

• debug : Bool

@[reducible, inline]

abbrev Lean.Meta.Sym.SymM (α : Type) : Type

def Lean.Meta.Sym.unfoldReducibleStep (e : Expr) : MetaM TransformStep

Auxiliary function for implementing unfoldReducible and unfoldReducibleSimproc. Performs a single step.

def Lean.Meta.Sym.isUnfoldReducibleTarget (e : Expr) : CoreM Bool

def Lean.Meta.Sym.unfoldReducible (e : Expr) : MetaM Expr

Unfolds all reducible declarations occurring in e. This is meant as a preprocessing step. It does not guarantee maximally shared terms

def Lean.Meta.Sym.foldProjs (e : Expr) : MetaM Expr

Converts nested Expr.projs into projection applications if possible. The structural simplifier and pattern matcher do not handle kernel projection terms; this preprocessing step folds them into projection function applications.

def Lean.Meta.Sym.SymM.run {α : Type} (x : SymM α) : MetaM α

def Lean.Meta.Sym.getSharedExprs : SymM SharedExprs

Returns maximally shared commonly used terms

def Lean.Meta.Sym.getTrueExpr : SymM Expr

Returns the internalized True constant.

def Lean.Meta.Sym.isTrueExpr (e : Expr) : SymM Bool

Returns true if e is the internalized True expression.

def Lean.Meta.Sym.getFalseExpr : SymM Expr

Returns the internalized False constant.

def Lean.Meta.Sym.isFalseExpr (e : Expr) : SymM Bool

Returns true if e is the internalized False expression.

def Lean.Meta.Sym.getBoolTrueExpr : SymM Expr

Returns the internalized Bool.true.

def Lean.Meta.Sym.isBoolTrueExpr (e : Expr) : SymM Bool

Returns true if e is the internalized Bool.true expression.

def Lean.Meta.Sym.getBoolFalseExpr : SymM Expr

Returns the internalized Bool.false.

def Lean.Meta.Sym.isBoolFalseExpr (e : Expr) : SymM Bool

Returns true if e is the internalized Bool.false expression.

def Lean.Meta.Sym.getNatZeroExpr : SymM Expr

Returns the internalized 0 : Nat numeral.

def Lean.Meta.Sym.getOrderingEqExpr : SymM Expr

Returns the internalized Ordering.eq.

def Lean.Meta.Sym.getIntExpr : SymM Expr

Returns the internalized Int.

def Lean.Meta.Sym.runShareCommonM {α : Type} (k : AlphaShareCommonM α) (ctx : AlphaShareCommon.Context) : SymM (Except AlphaShareCommon.Cache α)

Runs an AlphaShareCommonM action over the SymM hash-consing state. On a check violation, returns the cache accumulated before the failure as .error; the terms hash-consed before the failure are kept in the state, since they individually satisfy the invariants.

def Lean.Meta.Sym.withoutFoldProjsCheck {m : Type → Type u_1} {α : Type} [MonadWithReaderOf Context m] (x : m α) : m α

Runs x with the shareCommon kernel-projection check disabled. Use this to wrap code that temporarily violates the SymM folded-projections invariant, e.g., a head reducer that exposes kernel projections in intermediate terms and restores the invariant in its final result.

def Lean.Meta.Sym.withoutShareCommonChecks {m : Type → Type u_1} {α : Type} [MonadWithReaderOf Context m] (x : m α) : m α

def Lean.Meta.Sym.shareCommonWithoutChecks (e : Expr) (cache : AlphaShareCommon.Cache := ∅) : SymM Expr

Applies hash-consing to e. Recall that all expressions in a grind goal have been hash-consed. We perform this step before we internalize expressions.

This function does not try to unfoldReducible and foldProjs like shareCommon. cache may contain the results accumulated by a run of shareCommon that was interrupted by a check violation; see repairAndShare.

def Lean.Meta.Sym.shareCommon (e : Expr) : SymM Expr

Applies hash-consing to e. Recall that all expressions in a grind goal have been hash-consed. We perform this step before we internalize expressions.

Depending on the current configuration, this function also maintains the SymM invariants that reducible constants have been unfolded and kernel projections folded. The checks are node-local and are only performed on terms that have not been hash-consed before, so already-shared subterms cost nothing. When a violation is found, the term is repaired using unfoldReducible/foldProjs and re-processed.

def Lean.Meta.Sym.shareCommonInc (e : Expr) : SymM Expr

Incremental variant of shareCommon for expressions constructed from already-shared subterms.

Use this when an expression e was produced by a Lean API (e.g., inferType, mkApp4) that does not preserve maximal sharing, but the inputs to that API were already maximally shared.

Unlike shareCommon, this function does not use a local Std.HashMap ExprPtr Expr to track visited nodes. This is more efficient when the number of new (unshared) nodes is small, which is the common case when wrapping API calls that build a few constructor nodes around shared inputs.

Example:

-- `a` and `b` are already maximally shared
let result := mkApp2 f a b  -- result is not maximally shared
let result ← shareCommonInc result -- efficiently restore sharing

@[reducible, inline]

abbrev Lean.Meta.Sym.share (e : Expr) : SymM Expr

Incremental variant of shareCommon for expressions constructed from already-shared subterms.

Use this when an expression e was produced by a Lean API (e.g., inferType, mkApp4) that does not preserve maximal sharing, but the inputs to that API were already maximally shared.

Unlike shareCommon, this function does not use a local Std.HashMap ExprPtr Expr to track visited nodes. This is more efficient when the number of new (unshared) nodes is small, which is the common case when wrapping API calls that build a few constructor nodes around shared inputs.

Example:

-- `a` and `b` are already maximally shared
let result := mkApp2 f a b  -- result is not maximally shared
let result ← shareCommonInc result -- efficiently restore sharing

@[inline]

def Lean.Meta.Sym.isDebugEnabled : SymM Bool

Returns true if sym.debug is set

def Lean.Meta.Sym.getConfig : SymM Config

def Lean.Meta.Sym.reportIssue (msg : MessageData) : SymM Unit

Adds an issue message to the issue tracker.

@[inline]

def Lean.Meta.Sym.reportIssueIfVerbose (msg : MessageData) : SymM Unit

Reports an issue if verbose mode is enabled. Does nothing if verbose is false.

def Lean.Meta.Sym.doElemReportIssue!__ : ParserDescr

Reports an issue if verbose mode is enabled.

@[inline]

def Lean.Meta.Sym.reportDbgIssue (msg : MessageData) : SymM Unit

Reports an issue if both verbose and sym.debug are enabled. Does nothing otherwise.

def Lean.Meta.Sym.expandReportDbgIssueMacro (s : Syntax) : MacroM DoElem

def Lean.Meta.Sym.doElemReportDbgIssue!__ : ParserDescr

Similar to reportIssue!, but only reports issue if sym.debug is set to true.

def Lean.Meta.Sym.getIssues : SymM (List MessageData)

Returns all accumulated issues without clearing them.

def Lean.Meta.Sym.withNewIssueContext {α : Type} (x : SymM α) : SymM α

Runs x with a fresh issue context. Issues reported during x are prepended to the issues that existed before the call.

def Lean.Meta.Sym.isDefEqI (s t : Expr) : SymM Bool

Similar to Meta.isDefEqI, but the result is cache using pointer equality.

@[instance_reducible]

instance Lean.Meta.Sym.instInhabitedSymM {α : Type} : Inhabited (SymM α)

SymExtension accessors

@[implemented_by _private.Lean.Meta.Sym.SymM.0.Lean.Meta.Sym.SymExtension.getStateCoreImpl]

opaque Lean.Meta.Sym.SymExtension.getStateCore {σ : Type} (ext : SymExtension σ) (extensions : Array SymExtensionState) : IO σ

def Lean.Meta.Sym.SymExtension.getState {σ : Type} (ext : SymExtension σ) : SymM σ

@[implemented_by _private.Lean.Meta.Sym.SymM.0.Lean.Meta.Sym.SymExtension.modifyStateImpl]

opaque Lean.Meta.Sym.SymExtension.modifyState {σ : Type} (ext : SymExtension σ) (f : σ → σ) : SymM Unit