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.

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 Name Level

  Mapping from existing universe parameter names to the new ones.

• paramNames : Array Name

  Parameters that have been normalized.

@[reducible, inline]

abbrev Lean.Compiler.LCNF.NormLevelParam.M (α : Type) : Type

Monad for the universe level normalizer

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

Normalize universe level parameter names in the given universe level.

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

Normalize universe level parameter names in the given expression.

def Lean.Compiler.LCNF.normLevelParams (e : Expr) : Expr × List 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.

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.

@[reducible, inline]

abbrev Lean.Compiler.LCNF.CollectLevelParams.visitType (type : Expr) : CollectLevelParams.Visitor

def Lean.Compiler.LCNF.CollectLevelParams.visitArg (arg : Arg) : CollectLevelParams.Visitor

def Lean.Compiler.LCNF.CollectLevelParams.visitArgs (args : Array Arg) : CollectLevelParams.Visitor

def Lean.Compiler.LCNF.CollectLevelParams.visitLetValue (e : LetValue) : CollectLevelParams.Visitor

def Lean.Compiler.LCNF.CollectLevelParams.visitParam (p : Param) : CollectLevelParams.Visitor

def Lean.Compiler.LCNF.CollectLevelParams.visitParams (ps : Array Param) : CollectLevelParams.Visitor

partial def Lean.Compiler.LCNF.CollectLevelParams.visitAlt (alt : Alt) : CollectLevelParams.Visitor

partial def Lean.Compiler.LCNF.CollectLevelParams.visitAlts (alts : Array Alt) : CollectLevelParams.Visitor

partial def Lean.Compiler.LCNF.CollectLevelParams.visitCode : Code → CollectLevelParams.Visitor

def Lean.Compiler.LCNF.CollectLevelParams.visitDeclValue : DeclValue → CollectLevelParams.Visitor

def Lean.Compiler.LCNF.Decl.setLevelParams (decl : Decl) : Decl

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