source
@[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.

Equations

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

Instances For

source
@[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`.

Equations

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

Instances For

source
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

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

Instances

source
def Lean.Compiler.LCNF.Simp.ConstantFold.mkAuxLetDecl (e : LetValue) (prefixName : Name := `_x) :
FolderM 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.

Instances For

source
def Lean.Compiler.LCNF.Simp.ConstantFold.mkAuxLit {α : Type} [Literal α] (x : α) (prefixName : Name := `_x) :
FolderM 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

Instances For

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

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

Instances For

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

- Lean.Compiler.LCNF.Simp.ConstantFold.mkNatLit n = pure (Lean.Compiler.LCNF.LetValue.lit (Lean.Compiler.LCNF.LitValue.nat n))

Instances For

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

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

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

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

Instances For

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

- Lean.Compiler.LCNF.Simp.ConstantFold.mkStringLit n = pure (Lean.Compiler.LCNF.LetValue.lit (Lean.Compiler.LCNF.LitValue.str n))

Instances For

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

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

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

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

Instances For

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

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

Instances For

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

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

source
def Lean.Compiler.LCNF.Simp.ConstantFold.mkNatWrapperInstance {α : Type} (ofNat : Nat → α) (ofNatName : Name) (toNat : α → Nat) :
Literal α
Equations

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

Instances For

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

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

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

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

Instances For

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

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

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

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

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

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

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

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

source
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

Equations

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

Instances For

source
def Lean.Compiler.LCNF.Simp.ConstantFold.mkPseudoArrayLiteral (elements : Array FVarId) (typ : Expr) (typLevel : Level) :
FolderM 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.

Instances For

source
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

Equations

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

Instances For

source
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.

Equations

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

Instances For

source
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.

Equations

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

Instances For

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

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

Instances For

source
def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.leftNeutral {α : Type} [Literal α] [BEq α] (neutral : α) :
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.

Instances For

source
def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.rightNeutral {α : Type} [Literal α] [BEq α] (neutral : α) :
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.

Instances For

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

Provide a folder for an operation with a left annihilator.

Equations

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

Instances For

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

Provide a folder for an operation with a right annihilator.

Equations

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

Pick the first folder out of `folders` that succeeds.

Equations

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

Instances For

source
def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.leftRightNeutral {α : Type} [Literal α] [BEq α] (neutral : α) :
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.

Instances For

source
def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.leftRightAnnihilator {α : Type} [Literal α] [BEq α] (annihilator zero : α) :
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.

Instances For

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

Literal folders for higher order datastructures.

Equations

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

Instances For

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

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

Instances For

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

- Lean.Compiler.LCNF.Simp.ConstantFold.natPowThreshold = 256

Instances For

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

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

Instances For

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

Folder for ofNat operations on fixed-sized integer types.

Equations

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

Instances For

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

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

Instances For

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

All arithmetic folders.

Equations

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

Instances For

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

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

Instances For

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

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

Instances For

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

All string folders.

Equations

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

Instances For

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

Apply all known folders to `decl`.

Equations

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

Instances For

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

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

Instances For

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

- declName : Name
- folderDeclName : Name

Instances For

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

- declName : Name
- folderDeclName : Name
- folder : Folder

Instances For

source
opaque Lean.Compiler.LCNF.Simp.ConstantFold.folderExt :
PersistentEnvExtension FolderOleanEntry FolderEntry (List FolderEntry × SMap Name Folder)
source
def Lean.Compiler.LCNF.Simp.ConstantFold.registerFolder (declName folderDeclName : Name) :
CoreM Unit
Equations

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

Instances For

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

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

Instances For

source
def Lean.Compiler.LCNF.Simp.ConstantFold.foldConstants (decl : LetDecl) :
CompilerM (Option (Array 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

Instances For