HepLean 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

State for the universe level normalizer monad.

  • nextIdx : Nat

    Counter for generating new (normalized) universe parameter names.

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

    Mapping from existing universe parameter names to the new ones.

  • paramNames : Array Lake.Name

    Parameters that have been normalized.

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

    Monad for the universe level normalizer

    Equations
    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.

      Equations
      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
        @[reducible, inline]
        abbrev Lean.Compiler.LCNF.CollectLevelParams.visitType (type : Lean.Expr) :
        Lean.CollectLevelParams.Visitor
        Equations
        Instances For
          source
          def Lean.Compiler.LCNF.CollectLevelParams.visitArg (arg : Lean.Compiler.LCNF.Arg) :
          Lean.CollectLevelParams.Visitor
          Equations
          Instances For
            source
            def Lean.Compiler.LCNF.CollectLevelParams.visitArgs (args : Array Lean.Compiler.LCNF.Arg) :
            Lean.CollectLevelParams.Visitor
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Lean.Compiler.LCNF.CollectLevelParams.visitLetValue (e : Lean.Compiler.LCNF.LetValue) :
              Lean.CollectLevelParams.Visitor
              Equations
              Instances For
                source
                def Lean.Compiler.LCNF.CollectLevelParams.visitParam (p : Lean.Compiler.LCNF.Param) :
                Lean.CollectLevelParams.Visitor
                Equations
                Instances For
                  source
                  def Lean.Compiler.LCNF.CollectLevelParams.visitParams (ps : Array Lean.Compiler.LCNF.Param) :
                  Lean.CollectLevelParams.Visitor
                  Equations
                  • One or more equations did not get rendered due to their size.
                  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.

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