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

  Mapping from existing universe parameter names to the new ones.

• paramNames : Array Lean.Name

  Parameters that have been normalized.

@[reducible, inline]

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

Monad for the universe level normalizer

Equations

• Lean.Compiler.LCNF.NormLevelParam.M = StateM Lean.Compiler.LCNF.NormLevelParam.State

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.

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.

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

• Lean.Compiler.LCNF.normLevelParams e = match StateT.run (Lean.Compiler.LCNF.NormLevelParam.normExpr e) { nextIdx := 1, map := ∅, paramNames := #[] } with | (e, s) => (e, s.paramNames.toList)

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 : Lean.Expr) : Lean.CollectLevelParams.Visitor

Equations

• Lean.Compiler.LCNF.CollectLevelParams.visitType type = Lean.CollectLevelParams.visitExpr type

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

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.

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

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

Equations

• Lean.Compiler.LCNF.CollectLevelParams.visitParam p = Lean.Compiler.LCNF.CollectLevelParams.visitType p.type

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

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

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

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

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.