@[reducible, inline]

abbrev Lean.Compiler.LCNF.Simp.ConstantFold.FolderM (α : Type) : Type

A constant folding monad, the additional state stores auxiliary declarations required to build the new constant.

@[reducible, inline]

abbrev Lean.Compiler.LCNF.Simp.ConstantFold.Folder : Type

A constant folder for a specific function, takes all the arguments of a certain function and produces a new Expr + auxiliary declarations in the FolderM monad on success. If the folding fails it returns none.

class Lean.Compiler.LCNF.Simp.ConstantFold.Literal (α : Type) : Type

A typeclass for detecting and producing literals of arbitrary types inside of LCNF.

• getLit : FVarId → CompilerM (Option α)

  Attempt to turn the provided Expr into a value of type α if it is whatever concept of a literal α has. Note that this function does assume that the provided Expr does indeed have type α.

• mkLit : α → FolderM (LetValue Purity.pure)

  Turn a value of type α into a series of auxiliary LetDecls + a final Expr putting them all together into a literal of type α, where again the idea of what a literal is depends on α.

def Lean.Compiler.LCNF.Simp.ConstantFold.mkAuxLetDecl (e : LetValue Purity.pure) (prefixName : Name := `_x) : FolderM FVarId

A wrapper around LCNF.mkAuxLetDecl that will automatically store the LetDecl in the state of FolderM.

def Lean.Compiler.LCNF.Simp.ConstantFold.mkAuxLit {α : Type} [Literal α] (x : α) (prefixName : Name := `_x) : FolderM FVarId

A wrapper around mkAuxLetDecl that also calls mkLit.

def Lean.Compiler.LCNF.Simp.ConstantFold.getNatLit (fvarId : FVarId) : CompilerM (Option Nat)

def Lean.Compiler.LCNF.Simp.ConstantFold.mkNatLit (n : Nat) : FolderM (LetValue Purity.pure)

@[instance_reducible]

instance Lean.Compiler.LCNF.Simp.ConstantFold.instLiteralNat : Literal Nat

def Lean.Compiler.LCNF.Simp.ConstantFold.getStringLit (fvarId : FVarId) : CompilerM (Option String)

def Lean.Compiler.LCNF.Simp.ConstantFold.mkStringLit (n : String) : FolderM (LetValue Purity.pure)

@[instance_reducible]

instance Lean.Compiler.LCNF.Simp.ConstantFold.instLiteralString : Literal String

def Lean.Compiler.LCNF.Simp.ConstantFold.getBoolLit (fvarId : FVarId) : CompilerM (Option Bool)

def Lean.Compiler.LCNF.Simp.ConstantFold.mkBoolLit (b : Bool) : FolderM (LetValue Purity.pure)

@[instance_reducible]

instance Lean.Compiler.LCNF.Simp.ConstantFold.instLiteralBool : Literal Bool

def Lean.Compiler.LCNF.Simp.ConstantFold.getCharLit (fvarId : FVarId) : CompilerM (Option Char)

def Lean.Compiler.LCNF.Simp.ConstantFold.mkCharLit (c : Char) : FolderM (LetValue Purity.pure)

@[instance_reducible]

instance Lean.Compiler.LCNF.Simp.ConstantFold.instLiteralChar : Literal Char

@[instance_reducible]

def Lean.Compiler.LCNF.Simp.ConstantFold.mkUIntInstance {α : Type} (matchLit : LitValue → Option α) (litValueCtor : α → LitValue) : Literal α

@[instance_reducible]

instance Lean.Compiler.LCNF.Simp.ConstantFold.instLiteralUInt8 : Literal UInt8

@[instance_reducible]

instance Lean.Compiler.LCNF.Simp.ConstantFold.instLiteralUInt16 : Literal UInt16

@[instance_reducible]

instance Lean.Compiler.LCNF.Simp.ConstantFold.instLiteralUInt32 : Literal UInt32

@[instance_reducible]

instance Lean.Compiler.LCNF.Simp.ConstantFold.instLiteralUInt64 : Literal UInt64

def Lean.Compiler.LCNF.Simp.ConstantFold.getUSizeLit (fvarId : FVarId) : CompilerM (Option UInt64)

def Lean.Compiler.LCNF.Simp.ConstantFold.mkUSizeLit (x : UInt64) : CompilerM (LetValue Purity.pure)

def Lean.Compiler.LCNF.Simp.ConstantFold.getPseudoListLiteral (fvarId : FVarId) : CompilerM (Option (List FVarId × Expr × Level))

Turns an expression chain of the form

let _x.1 := @List.nil _
let _x.2 := @List.cons _ a _x.1
let _x.3 := @List.cons _ b _x.2
let _x.4 := @List.cons _ c _x.3
let _x.5 := @List.cons _ d _x.4
let _x.6 := @List.cons _ e _x.5

into: [a, b, c, d ,e] + The type contained in the list

def Lean.Compiler.LCNF.Simp.ConstantFold.mkPseudoArrayLiteral (elements : Array FVarId) (typ : Expr) (typLevel : Level) : FolderM (LetValue Purity.pure)

Turn an #[a, b, c] into:

let _x.12 := 3
let _x.8 := @Array.mkEmpty _ _x.12
let _x.22 := @Array.push _ _x.8 x
let _x.24 := @Array.push _ _x.22 y
let _x.26 := @Array.push _ _x.24 z
_x.26

def Lean.Compiler.LCNF.Simp.ConstantFold.foldArrayLiteral : Folder

Evaluate array literals at compile time, that is turn:

let _x.1 := @List.nil _
let _x.2 := @List.cons _ z _x.1
let _x.3 := @List.cons _ y _x.2
let _x.4 := @List.cons _ x _x.3
let _x.5 := @List.toArray _ _x.4

To its array form:

let _x.12 := 3
let _x.8 := @Array.mkEmpty _ _x.12
let _x.22 := @Array.push _ _x.8 x
let _x.24 := @Array.push _ _x.22 y
let _x.26 := @Array.push _ _x.24 z

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.mkUnary {α β : Type} [Literal α] [Literal β] (folder : α → β) : Folder

Turn a unary function such as Nat.succ into a constant folder.

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.mkBinary {α β γ : Type} [Literal α] [Literal β] [Literal γ] (folder : α → β → γ) : Folder

Turn a binary function such as Nat.add into a constant folder.

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.mkBinaryDecisionProcedure {α β : Type} [Literal α] [Literal β] {r : α → β → Prop} (folder : (a : α) → (b : β) → Decidable (r a b)) : Folder

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.mkBinaryUSizeDecisionProcedure {r64 : UInt64 → UInt64 → Prop} {r32 : UInt32 → UInt32 → Prop} (f64 : (a b : UInt64) → Decidable (r64 a b)) (f32 : (a b : UInt32) → Decidable (r32 a b)) : Folder

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.mkBinaryUSize (f64 : UInt64 → UInt64 → UInt64) (f32 : UInt32 → UInt32 → UInt32) : Folder

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.mkUnaryUSize (f64 : UInt64 → UInt64) (f32 : UInt32 → UInt32) : Folder

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.mkUnaryToUSize {α : Type} [Literal α] (f64 : α → UInt64) (f32 : α → UInt32) : Folder

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.mkUnaryOfUSize {β : Type} [Literal β] [BEq β] (f64 : UInt64 → β) (f32 : UInt32 → β) : Folder

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.leftNeutralUSize (n64 : UInt64) (n32 : UInt32) : Folder

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.rightNeutralUSize (n64 : UInt64) (n32 : UInt32) : Folder

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.leftAnnihilatorUSize (a64 : UInt64) (a32 : UInt32) (zero64 : UInt64) (zero32 : UInt32) : Folder

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.rightAnnihilatorUSize (a64 : UInt64) (a32 : UInt32) (zero64 : UInt64) (zero32 : UInt32) : Folder

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.leftNeutral {α : Type} [Literal α] [BEq α] (neutral : α) (op : α → α → α) (_h : ∀ (x : α), op neutral x = x := by simp) : Folder

Provide a folder for an operation with a left neutral element.

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.rightNeutral {α : Type} [Literal α] [BEq α] (neutral : α) (op : α → α → α) (_h : ∀ (x : α), op x neutral = x := by simp) : Folder

Provide a folder for an operation with a right neutral element.

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.leftAnnihilator {α γ : Type} {β : Sort u_1} [Literal α] [BEq α] [Literal γ] (annihilator : α) (zero : γ) (op : α → β → γ) (_h : ∀ (x : β), op annihilator x = zero := by simp) : Folder

Provide a folder for an operation with a left annihilator.

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.rightAnnihilator {β γ : Type} {α : Sort u_1} [Literal β] [BEq β] [Literal γ] (annihilator : β) (zero : γ) (op : α → β → γ) (_h : ∀ (x : α), op x annihilator = zero := by simp) : Folder

Provide a folder for an operation with a right annihilator. The result type may differ from the operand types, e.g. Nat.blt x 0 = false.

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.sameArg {γ : Type} {α : Sort u_1} [Literal γ] (zero : γ) (op : α → α → γ) (_h : ∀ (x : α), op x x = zero := by simp) : Folder

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.sameArgUSize (zero64 : UInt64) (zero32 : UInt32) : Folder

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.idempotent {α : Sort u_1} (op : α → α → α) (_h : ∀ (x : α), op x x = x := by simp) : Folder

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.divShift {α : Type} [Literal α] [BEq α] (shiftRight : Name) (pow2 log2 : α → α) : Folder

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.mulRhsShift {α : Type} [Literal α] [BEq α] (shiftLeft : Name) (pow2 log2 : α → α) : Folder

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.mulLhsShift {α : Type} [Literal α] [BEq α] (shiftLeft : Name) (pow2 log2 : α → α) : Folder

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.divShiftUSize : Folder

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.mulRhsShiftUSize : Folder

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.mulLhsShiftUSize : Folder

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.first (folders : Array Folder) : Folder

Pick the first folder out of folders that succeeds.

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.leftRightNeutral {α : Type} [Literal α] [BEq α] (neutral : α) (op : α → α → α) (_h1 : ∀ (x : α), op neutral x = x := by simp) (_h2 : ∀ (x : α), op x neutral = x := by simp) : Folder

Provide a folder for an operation that has the same left and right neutral element.

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.leftRightNeutralUSize (n64 : UInt64) (n32 : UInt32) : Folder

Provide a folder for a USize operation that has the same left and right neutral element.

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.leftRightAnnihilator {α : Type} [Literal α] [BEq α] (annihilator zero : α) (op : α → α → α) (_h1 : ∀ (x : α), op annihilator x = zero := by simp) (_h2 : ∀ (x : α), op x annihilator = zero := by simp) : Folder

Provide a folder for an operation that has the same left and right annihilator.

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.leftRightAnnihilatorUSize (annihilator64 : UInt64) (annihilator32 : UInt32) (zero64 : UInt64) (zero32 : UInt32) : Folder

Provide a folder for a USize operation that has the same left and right annihilator.

def Lean.Compiler.LCNF.Simp.ConstantFold.higherOrderLiteralFolders : List (Name × Folder)

Literal folders for higher order datastructures.

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.mulShift {α : Type} [Literal α] [BEq α] (shiftLeft : Name) (pow2 log2 : α → α) : Folder

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.mulShiftUSize : Folder

def Lean.Compiler.LCNF.Simp.ConstantFold.natPowThreshold : Nat

def Lean.Compiler.LCNF.Simp.ConstantFold.foldNatPow (args : Array (Arg Purity.pure)) : FolderM (Option (LetValue Purity.pure))

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.ofNat (f : Nat → LitValue) (args : Array (Arg Purity.pure)) : FolderM (Option (LetValue Purity.pure))

Folder for ofNat operations on fixed-sized integer types.

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.ofNatLT (f : Nat → LitValue) (args : Array (Arg Purity.pure)) : FolderM (Option (LetValue Purity.pure))

Folder for ofNatLT operations on fixed-sized integer types. The bound is a proof and carries no runtime content, so only the numeral matters.

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.charOfNat (args : Array (Arg Purity.pure)) : FolderM (Option (LetValue Purity.pure))

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.toNat (args : Array (Arg Purity.pure)) : FolderM (Option (LetValue Purity.pure))

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.getObjTagNat (args : Array (Arg Purity.pure)) : FolderM (Option (LetValue Purity.pure))

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.natCtorIdx (args : Array (Arg Purity.pure)) : FolderM (Option (LetValue Purity.pure))

def Lean.Compiler.LCNF.Simp.ConstantFold.arithmeticFolders : List (Name × Folder)

All arithmetic folders.

def Lean.Compiler.LCNF.Simp.ConstantFold.relationFolders : List (Name × Folder)

def Lean.Compiler.LCNF.Simp.ConstantFold.conversionFolders : List (Name × Folder)

def Lean.Compiler.LCNF.Simp.ConstantFold.stringFolders : List (Name × Folder)

All string folders.

def Lean.Compiler.LCNF.Simp.ConstantFold.hashFolders : List (Name × Folder)

def Lean.Compiler.LCNF.Simp.ConstantFold.foldTaskGet (args : Array (Arg Purity.pure)) : FolderM (Option (LetValue Purity.pure))

def Lean.Compiler.LCNF.Simp.ConstantFold.taskFolders : List (Name × Folder)

def Lean.Compiler.LCNF.Simp.ConstantFold.charFolders : List (Name × Folder)

def Lean.Compiler.LCNF.Simp.ConstantFold.applyFolders (decl : LetDecl Purity.pure) (folders : SMap Name Folder) : CompilerM (Option (Array (CodeDecl Purity.pure)))

Apply all known folders to decl.

def Lean.Compiler.LCNF.Simp.ConstantFold.builtinFolders : SMap Name Folder

structure Lean.Compiler.LCNF.Simp.ConstantFold.FolderOleanEntry : Type

• declName : Name
• folderDeclName : Name

structure Lean.Compiler.LCNF.Simp.ConstantFold.FolderEntry extends Lean.Compiler.LCNF.Simp.ConstantFold.FolderOleanEntry : Type

• declName : Name
• folderDeclName : Name
• folder : Folder

opaque Lean.Compiler.LCNF.Simp.ConstantFold.folderExt : PersistentEnvExtension FolderOleanEntry FolderEntry (List FolderEntry × SMap Name Folder)

def Lean.Compiler.LCNF.Simp.ConstantFold.registerFolder (declName folderDeclName : Name) : CoreM Unit

def Lean.Compiler.LCNF.Simp.ConstantFold.getFolders : CoreM (SMap Name Folder)

def Lean.Compiler.LCNF.Simp.ConstantFold.foldConstants (decl : LetDecl Purity.pure) : CompilerM (Option (Array (CodeDecl Purity.pure)))

Apply a list of default folders to decl