Type-directed canonicalizer #

Canonicalizes expressions by normalizing types and instances. At the top level, it traverses applications, foralls, lambdas, and let-bindings, classifying each argument as a type, instance, implicit, or value using shouldCanon. Values are recursively visited but not normalized. Types and instances receive targeted reductions.

Reductions (applied only in type positions) #

Eta: fun x => f x → f
Projection: ⟨a, b⟩.1 → a (structure projections, not class projections)
Match/ite/cond: reduced when discriminant is a constructor or literal
Nat arithmetic: ground evaluation (2 + 1 → 3) and offset normalization (n.succ + 1 → n + 2)

Instance canonicalization #

Instances are re-synthesized via synthInstance. The instance type is first normalized using the type-level reductions above, so that OfNat (Fin (2+1)) 0 and OfNat (Fin 3) 0 produce the same canonical instance.

Two caches #

The canonicalizer maintains separate caches for type-level and value-level contexts. The same expression may canonicalize differently depending on whether it appears in a type position (where reductions are applied) or a value position (where it is only traversed). Caches are keyed by Expr (structural equality), not pointer equality, because the canonicalizer runs before shareCommon and enters binders using locally nameless representation.

Future work #

If needed we should add support for user-defined extensions.

source

def Lean.Meta.Sym.Canon.isSupport (pinfos : Array ParamInfo) (i : Nat) (arg : Expr) :

MetaM Bool

Returns true if shouldCannon pinfos i arg is not .visit. This is a helper function used to implement mbtc.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Lean.Meta.Sym.canon (e : Expr) :

SymM Expr

Canonicalize e by normalizing types, instances, and support arguments. Types receive targeted reductions (eta, projection, match/ite, Nat arithmetic). Instances are re-synthesized. Values are traversed but not reduced. Runs at reducible transparency.

Equations

Lean.Meta.Sym.canon e = do let __do_lift ← Lean.getOptions Lean.profileitM Lean.Exception "sym canon" __do_lift (Lean.Meta.withReducible (Lean.Meta.Sym.Canon.canon✝ e { }))

Instances For