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
  • nextIdx : Nat

    Counter for generating new (normalized) universe parameter names.

  • map : Lean.HashMap Lake.Name Lean.Level

    Mapping from existing universe parameter names to the new ones.

  • paramNames : Array Lake.Name

    Parameters that have been normalized.

State for the universe level normalizer monad.

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

    Monad for the universe leve normalizer

    Instances For
      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 Lake.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.

      Instances For

        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, reducible]
        abbrev Lean.Compiler.LCNF.CollectLevelParams.visitType (type : Lean.Expr) :
        Lean.CollectLevelParams.Visitor
        Instances For
          source
          def Lean.Compiler.LCNF.CollectLevelParams.visitArg (arg : Lean.Compiler.LCNF.Arg) :
          Lean.CollectLevelParams.Visitor
          Instances For
            source
            def Lean.Compiler.LCNF.CollectLevelParams.visitArgs (args : Array Lean.Compiler.LCNF.Arg) :
            Lean.CollectLevelParams.Visitor
            Instances For
              source
              def Lean.Compiler.LCNF.CollectLevelParams.visitLetValue (e : Lean.Compiler.LCNF.LetValue) :
              Lean.CollectLevelParams.Visitor
              Instances For
                source
                def Lean.Compiler.LCNF.CollectLevelParams.visitParam (p : Lean.Compiler.LCNF.Param) :
                Lean.CollectLevelParams.Visitor
                Instances For
                  source
                  def Lean.Compiler.LCNF.CollectLevelParams.visitParams (ps : Array Lean.Compiler.LCNF.Param) :
                  Lean.CollectLevelParams.Visitor
                  Instances For
                    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.

                    Instances For