@[inline, reducible]

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.

Equations

• Lean.Compiler.LCNF.Simp.ConstantFold.FolderM = StateRefT' IO.RealWorld (Array Lean.Compiler.LCNF.CodeDecl) Lean.Compiler.LCNF.CompilerM

@[inline, reducible]

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.

Equations

• Lean.Compiler.LCNF.Simp.ConstantFold.Folder = (Array Lean.Compiler.LCNF.Arg → Lean.Compiler.LCNF.Simp.ConstantFold.FolderM (Option Lean.Compiler.LCNF.LetValue))

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

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

• getLit : Lean.FVarId → Lean.Compiler.LCNF.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 : α → Lean.Compiler.LCNF.Simp.ConstantFold.FolderM Lean.Compiler.LCNF.LetValue

  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 : Lean.Compiler.LCNF.LetValue) (prefixName : optParam Lake.Name `_x) : Lean.Compiler.LCNF.Simp.ConstantFold.FolderM Lean.FVarId

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

Equations

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

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

A wrapper around mkAuxLetDecl that also calls mkLit.

Equations

• Lean.Compiler.LCNF.Simp.ConstantFold.mkAuxLit x prefixName = do let lit ← Lean.Compiler.LCNF.Simp.ConstantFold.mkLit x Lean.Compiler.LCNF.Simp.ConstantFold.mkAuxLetDecl lit prefixName

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

Equations

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

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

Equations

• Lean.Compiler.LCNF.Simp.ConstantFold.mkNatLit n = pure (Lean.Compiler.LCNF.LetValue.value (Lean.Compiler.LCNF.LitValue.natVal n))

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

Equations

• Lean.Compiler.LCNF.Simp.ConstantFold.instLiteralNat = { getLit := Lean.Compiler.LCNF.Simp.ConstantFold.getNatLit, mkLit := Lean.Compiler.LCNF.Simp.ConstantFold.mkNatLit }

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

Equations

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

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

Equations

• Lean.Compiler.LCNF.Simp.ConstantFold.mkStringLit n = pure (Lean.Compiler.LCNF.LetValue.value (Lean.Compiler.LCNF.LitValue.strVal n))

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

Equations

• Lean.Compiler.LCNF.Simp.ConstantFold.instLiteralString = { getLit := Lean.Compiler.LCNF.Simp.ConstantFold.getStringLit, mkLit := Lean.Compiler.LCNF.Simp.ConstantFold.mkStringLit }

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

Equations

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

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

Equations

• Lean.Compiler.LCNF.Simp.ConstantFold.mkBoolLit b = let ctor := if b = true then `Bool.true else `Bool.false; pure (Lean.Compiler.LCNF.LetValue.const ctor [] #[])

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

Equations

• Lean.Compiler.LCNF.Simp.ConstantFold.instLiteralBool = { getLit := Lean.Compiler.LCNF.Simp.ConstantFold.getBoolLit, mkLit := Lean.Compiler.LCNF.Simp.ConstantFold.mkBoolLit }

def Lean.Compiler.LCNF.Simp.ConstantFold.mkNatWrapperInstance {α : Type} [Inhabited α] (ofNat : Nat → α) (ofNatName : Lake.Name) (toNat : α → Nat) : Lean.Compiler.LCNF.Simp.ConstantFold.Literal α

Equations

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

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

Equations

• Lean.Compiler.LCNF.Simp.ConstantFold.instLiteralUInt8 = Lean.Compiler.LCNF.Simp.ConstantFold.mkNatWrapperInstance UInt8.ofNat `UInt8.ofNat UInt8.toNat

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

Equations

• Lean.Compiler.LCNF.Simp.ConstantFold.instLiteralUInt16 = Lean.Compiler.LCNF.Simp.ConstantFold.mkNatWrapperInstance UInt16.ofNat `UInt16.ofNat UInt16.toNat

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

Equations

• Lean.Compiler.LCNF.Simp.ConstantFold.instLiteralUInt32 = Lean.Compiler.LCNF.Simp.ConstantFold.mkNatWrapperInstance UInt32.ofNat `UInt32.ofNat UInt32.toNat

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

Equations

• Lean.Compiler.LCNF.Simp.ConstantFold.instLiteralUInt64 = Lean.Compiler.LCNF.Simp.ConstantFold.mkNatWrapperInstance UInt64.ofNat `UInt64.ofNat UInt64.toNat

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

Equations

• Lean.Compiler.LCNF.Simp.ConstantFold.instLiteralChar = Lean.Compiler.LCNF.Simp.ConstantFold.mkNatWrapperInstance Char.ofNat `Char.ofNat Char.toNat

def Lean.Compiler.LCNF.Simp.ConstantFold.getPseudoListLiteral (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.CompilerM (Option (List Lean.FVarId × Lean.Expr × Lean.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

Equations

• Lean.Compiler.LCNF.Simp.ConstantFold.getPseudoListLiteral fvarId = Lean.Compiler.LCNF.Simp.ConstantFold.getPseudoListLiteral.go fvarId []

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

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

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

Equations

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

def Lean.Compiler.LCNF.Simp.ConstantFold.foldArrayLiteral : Lean.Compiler.LCNF.Simp.ConstantFold.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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

Equations

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

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.leftNeutral {α : Type} [Lean.Compiler.LCNF.Simp.ConstantFold.Literal α] [BEq α] (neutral : α) : Lean.Compiler.LCNF.Simp.ConstantFold.Folder

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

Equations

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

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.rightNeutral {α : Type} [Lean.Compiler.LCNF.Simp.ConstantFold.Literal α] [BEq α] (neutral : α) : Lean.Compiler.LCNF.Simp.ConstantFold.Folder

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

Equations

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

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.leftAnnihilator {α : Type} [Lean.Compiler.LCNF.Simp.ConstantFold.Literal α] [BEq α] (annihilator : α) (zero : α) : Lean.Compiler.LCNF.Simp.ConstantFold.Folder

Provide a folder for an operation with a left annihilator.

Equations

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

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.rightAnnihilator {α : Type} [Lean.Compiler.LCNF.Simp.ConstantFold.Literal α] [BEq α] (annihilator : α) (zero : α) : Lean.Compiler.LCNF.Simp.ConstantFold.Folder

Provide a folder for an operation with a right annihilator.

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Pick the first folder out of folders that succeeds.

Equations

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

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.leftRightNeutral {α : Type} [Lean.Compiler.LCNF.Simp.ConstantFold.Literal α] [BEq α] (neutral : α) : Lean.Compiler.LCNF.Simp.ConstantFold.Folder

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

Equations

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

def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.leftRightAnnihilator {α : Type} [Lean.Compiler.LCNF.Simp.ConstantFold.Literal α] [BEq α] (annihilator : α) (zero : α) : Lean.Compiler.LCNF.Simp.ConstantFold.Folder

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

Equations

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

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

Literal folders for higher order datastructures.

Equations

• Lean.Compiler.LCNF.Simp.ConstantFold.higherOrderLiteralFolders = [(`List.toArray, Lean.Compiler.LCNF.Simp.ConstantFold.foldArrayLiteral)]

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

Equations

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

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

All arithmetic folders.

Equations

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

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

Equations

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

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

All string folders.

Equations

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

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

Apply all known folders to decl.

Equations

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

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

Equations

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

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

• declName : Lake.Name
• folderDeclName : Lake.Name

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

• declName : Lake.Name
• folderDeclName : Lake.Name
• folder : Lean.Compiler.LCNF.Simp.ConstantFold.Folder

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

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

Equations

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

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

Equations

• Lean.Compiler.LCNF.Simp.ConstantFold.getFolders = do let __do_lift ← Lean.getEnv pure (Lean.PersistentEnvExtension.getState Lean.Compiler.LCNF.Simp.ConstantFold.folderExt __do_lift).snd

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

Apply a list of default folders to decl

Equations

• Lean.Compiler.LCNF.Simp.ConstantFold.foldConstants decl = do let __do_lift ← liftM Lean.Compiler.LCNF.Simp.ConstantFold.getFolders Lean.Compiler.LCNF.Simp.ConstantFold.applyFolders decl __do_lift