Documentation

Lean.Compiler.LCNF.Level

Universe level utilities for the code generator #

Universe level parameter normalizer #

The specializer creates "keys" for a function specialization. The key is an expression containing the function being specialized and the argument values used for the specialization. The key does not contain free variables, and function parameter names are irrelevant due to alpha equivalence. The universe level normalizer ensures the universe parameter names are irrelevant when comparing keys.

source
structure Lean.Compiler.LCNF.NormLevelParam.State :
Type

  • Counter for generating new (normalized) universe parameter names.

    nextIdx : Nat

  • Mapping from existing universe parameter names to the new ones.

    map : Lean.HashMap Lean.Name Lean.Level

  • Parameters that have been normalized.

    paramNames : Array Lean.Name

State for the universe level normalizer monad.

Instances For
    source
    @[inline]
    abbrev Lean.Compiler.LCNF.NormLevelParam.M (α : Type) :
    Type

    Monad for the universe leve normalizer

    Equations
    source
    partial def Lean.Compiler.LCNF.NormLevelParam.normLevel (u : Lean.Level) :
    Lean.Compiler.LCNF.NormLevelParam.M Lean.Level

    Normalize universe level parameter names in the given universe level.

    source
    partial def Lean.Compiler.LCNF.NormLevelParam.normExpr (e : Lean.Expr) :
    Lean.Compiler.LCNF.NormLevelParam.M Lean.Expr

    Normalize universe level parameter names in the given expression.

    source
    def Lean.Compiler.LCNF.normLevelParams (e : Lean.Expr) :
    Lean.Expr × List Lean.Name

    Normalize universe level parameter names in the given expression. The function also returns the list of universe level parameter names that have been normalized.

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

    Universe level collector #

    This module extends support for Code. See Lean.Util.CollectLevelParams.lean

    In the code specializer, we create new auxiliary declarations and the universe level parameter collector is used to setup the new auxiliary declarations.

    See Decl.setLevelParams.

    source
    @[inline]
    abbrev Lean.Compiler.LCNF.CollectLevelParams.visitType (type : Lean.Expr) :
    Lean.CollectLevelParams.Visitor
    Equations
    source
    def Lean.Compiler.LCNF.CollectLevelParams.visitArg (arg : Lean.Compiler.LCNF.Arg) :
    Lean.CollectLevelParams.Visitor
    Equations
    • One or more equations did not get rendered due to their size.
    source
    def Lean.Compiler.LCNF.CollectLevelParams.visitArgs (args : Array Lean.Compiler.LCNF.Arg) :
    Lean.CollectLevelParams.Visitor
    Equations
    source
    def Lean.Compiler.LCNF.CollectLevelParams.visitLetValue (e : Lean.Compiler.LCNF.LetValue) :
    Lean.CollectLevelParams.Visitor
    Equations
    • One or more equations did not get rendered due to their size.
    source
    def Lean.Compiler.LCNF.CollectLevelParams.visitParam (p : Lean.Compiler.LCNF.Param) :
    Lean.CollectLevelParams.Visitor
    Equations
    source
    def Lean.Compiler.LCNF.CollectLevelParams.visitParams (ps : Array Lean.Compiler.LCNF.Param) :
    Lean.CollectLevelParams.Visitor
    Equations
    source
    partial def Lean.Compiler.LCNF.CollectLevelParams.visitAlt (alt : Lean.Compiler.LCNF.Alt) :
    Lean.CollectLevelParams.Visitor
    source
    partial def Lean.Compiler.LCNF.CollectLevelParams.visitAlts (alts : Array Lean.Compiler.LCNF.Alt) :
    Lean.CollectLevelParams.Visitor
    source
    partial def Lean.Compiler.LCNF.CollectLevelParams.visitCode :
    Lean.Compiler.LCNF.Code → Lean.CollectLevelParams.Visitor
    source
    def Lean.Compiler.LCNF.Decl.setLevelParams (decl : Lean.Compiler.LCNF.Decl) :
    Lean.Compiler.LCNF.Decl

    Collect universe level parameters collecting in the type, parameters, and value, and then set decl.levelParams with the resulting value.

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