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.IR.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.IR.instInhabitedSimpleGroundArg.default : SimpleGroundArg

Equations

• Lean.IR.instInhabitedSimpleGroundArg.default = Lean.IR.SimpleGroundArg.tagged default

@[instance_reducible]

instance Lean.IR.instInhabitedSimpleGroundArg : Inhabited SimpleGroundArg

Equations

• Lean.IR.instInhabitedSimpleGroundArg = { default := Lean.IR.instInhabitedSimpleGroundArg.default }

inductive Lean.IR.SimpleGroundExpr : Type

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

• ctor (cidx : Nat) (objArgs : Array SimpleGroundArg) (usizeArgs : Array USize) (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 : FunId) (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.

def Lean.IR.instInhabitedSimpleGroundExpr.default : SimpleGroundExpr

Equations

• Lean.IR.instInhabitedSimpleGroundExpr.default = Lean.IR.SimpleGroundExpr.ctor default default default default

@[instance_reducible]

instance Lean.IR.instInhabitedSimpleGroundExpr : Inhabited SimpleGroundExpr

Equations

• Lean.IR.instInhabitedSimpleGroundExpr = { default := Lean.IR.instInhabitedSimpleGroundExpr.default }

structure Lean.IR.SimpleGroundExtState : Type

• constNames : PHashMap Name SimpleGroundExpr
• revNames : List Name

def Lean.IR.instInhabitedSimpleGroundExtState.default : SimpleGroundExtState

Equations

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

@[instance_reducible]

instance Lean.IR.instInhabitedSimpleGroundExtState : Inhabited SimpleGroundExtState

Equations

• Lean.IR.instInhabitedSimpleGroundExtState = { default := Lean.IR.instInhabitedSimpleGroundExtState.default }

def Lean.IR.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.IR.getSimpleGroundExpr (env : Environment) (declName : Name) : Option SimpleGroundExpr

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

Equations

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

def Lean.IR.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.IR.isSimpleGroundDecl (env : Environment) (declName : Name) : Bool

Check if declName is recorded as being a SimpleGroundExpr.

Equations

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

def Lean.IR.uint64ToByteArrayLE (n : UInt64) : Array UInt8

Equations

• Lean.IR.uint64ToByteArrayLE n = #[n.toUInt8, (n >>> 8).toUInt8, (n >>> 16).toUInt8, (n >>> 24).toUInt8, (n >>> 32).toUInt8, (n >>> 40).toUInt8, (n >>> 48).toUInt8, (n >>> 56).toUInt8]

def Lean.IR.Decl.detectSimpleGround (d : Decl) : CompilerM Unit

Detect whether d can be compiled to a SimpleGroundExpr. If it can record the associated SimpleGroundExpr into the environment for later processing by code emission.

Equations

• One or more equations did not get rendered due to their size.
• d.detectSimpleGround = pure ()