This module contains logic for detecting simple ground expressions that can be extracted into statically initializable variables. To do this it attempts to compile declarations into a simple language of expressions, SimpleGroundExpr. If this attempt succeeds it stores the result in an environment extension, accessible through getSimpleGroundExpr. Later on the code emission step can reference this environment extension to generate static initializers for the respective declaration.

inductive Lean.Compiler.LCNF.SimpleGroundArg : Type

An argument to a SimpleGroundExpr. They get compiled to lean_object* in various ways.

• tagged (val : Nat) : SimpleGroundArg

  A simple tagged literal.

• reference (n : Name) : SimpleGroundArg

  A reference to another declaration that was marked as a simple ground expression. This gets compiled to a reference to the mangled version of the name.

• rawReference (s : String) : SimpleGroundArg

  A reference directly to a raw C name. This gets compiled to a reference to the name directly.

def Lean.Compiler.LCNF.instInhabitedSimpleGroundArg.default : SimpleGroundArg

Equations

• Lean.Compiler.LCNF.instInhabitedSimpleGroundArg.default = Lean.Compiler.LCNF.SimpleGroundArg.tagged default

@[implicit_reducible]

instance Lean.Compiler.LCNF.instInhabitedSimpleGroundArg : Inhabited SimpleGroundArg

Equations

• Lean.Compiler.LCNF.instInhabitedSimpleGroundArg = { default := Lean.Compiler.LCNF.instInhabitedSimpleGroundArg.default }

inductive Lean.Compiler.LCNF.SimpleGroundExpr : Type

A simple ground expression that can be turned into a static initializer.

• ctor (cidx : Nat) (objArgs : Array SimpleGroundArg) (usizeArgs : Array UInt64) (scalarArgs : Array UInt8) : SimpleGroundExpr

  Represents a lean_ctor_object. Crucially the scalarArgs array must have a size that is a multiple of 8.

• string (data : String) : SimpleGroundExpr

  A string literal, represented by a lean_string_object.

• pap (func : Name) (args : Array SimpleGroundArg) : SimpleGroundExpr

  A partial application, represented by a lean_closure_object.

• nameMkStr (args : Array (Name × UInt64)) : SimpleGroundExpr

  An application of Lean.Name.mkStrX. This expression is represented separately to ensure that long name literals get extracted into statically initializable constants. The arguments contain both the name of the string literal it references as well as the hash of the name up to that point. This is done to make emitting the literal as simple as possible.

• reference (n : Name) : SimpleGroundExpr

  A reference to another declaration that was marked as a simple ground expression. This gets compiled to a reference to the mangled version of the name.

• array (elems : Array SimpleGroundArg) : SimpleGroundExpr

  An array of lean_object* elements, represented by a lean_array_object.

• byteArray (data : Array UInt8) : SimpleGroundExpr

  A byte array (scalar array with elem_size=1), represented by a lean_sarray_object.

def Lean.Compiler.LCNF.instInhabitedSimpleGroundExpr.default : SimpleGroundExpr

Equations

• Lean.Compiler.LCNF.instInhabitedSimpleGroundExpr.default = Lean.Compiler.LCNF.SimpleGroundExpr.ctor default default default default

@[implicit_reducible]

instance Lean.Compiler.LCNF.instInhabitedSimpleGroundExpr : Inhabited SimpleGroundExpr

Equations

• Lean.Compiler.LCNF.instInhabitedSimpleGroundExpr = { default := Lean.Compiler.LCNF.instInhabitedSimpleGroundExpr.default }

structure Lean.Compiler.LCNF.SimpleGroundExtState : Type

• constNames : PHashMap Name SimpleGroundExpr
• revNames : List Name

@[implicit_reducible]

instance Lean.Compiler.LCNF.instInhabitedSimpleGroundExtState : Inhabited SimpleGroundExtState

Equations

• Lean.Compiler.LCNF.instInhabitedSimpleGroundExtState = { default := Lean.Compiler.LCNF.instInhabitedSimpleGroundExtState.default }

def Lean.Compiler.LCNF.instInhabitedSimpleGroundExtState.default : SimpleGroundExtState

Equations

• Lean.Compiler.LCNF.instInhabitedSimpleGroundExtState.default = { constNames := default, revNames := default }

def Lean.Compiler.LCNF.addSimpleGroundDecl (env : Environment) (declName : Name) (expr : SimpleGroundExpr) : Environment

Record declName as mapping to the simple ground expr expr.

Equations

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

def Lean.Compiler.LCNF.getSimpleGroundExpr (env : Environment) (declName : Name) : Option SimpleGroundExpr

Attempt to fetch a SimpleGroundExpr associated with declName if it exists.

Equations

• Lean.Compiler.LCNF.getSimpleGroundExpr env declName = Lean.PersistentHashMap.find? (Lean.Compiler.LCNF.simpleGroundDeclExt✝.getState env).constNames declName

def Lean.Compiler.LCNF.getSimpleGroundExprWithResolvedRefs (env : Environment) (declName : Name) : Option SimpleGroundExpr

Like getSimpleGroundExpr but recursively traverses reference exprs to get to actual ground values.

Equations

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

def Lean.Compiler.LCNF.isSimpleGroundDecl (env : Environment) (declName : Name) : Bool

Check if declName is recorded as being a SimpleGroundExpr.

Equations

• Lean.Compiler.LCNF.isSimpleGroundDecl env declName = Lean.PersistentHashMap.contains (Lean.Compiler.LCNF.simpleGroundDeclExt✝.getState env).constNames declName

def Lean.Compiler.LCNF.uint64ToByteArrayLE (n : UInt64) : Array UInt8

Equations

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

def Lean.Compiler.LCNF.detectSimpleGround : Pass

Equations

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