A constant folding monad, the additional state stores auxiliary declarations required to build the new constant.
Instances For
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.
Instances For
- getLit : Lean.FVarId → Lean.Compiler.LCNF.CompilerM (Option α)
Attempt to turn the provided
Exprinto a value of typeαif it is whatever concept of a literalαhas. Note that this function does assume that the providedExprdoes indeed have typeα. Turn a value of type
αinto a series of auxiliaryLetDecls + a finalExprputting them all together into a literal of typeα, where again the idea of what a literal is depends onα.
A typeclass for detecting and producing literals of arbitrary types inside of LCNF.
Instances
A wrapper around LCNF.mkAuxLetDecl that will automatically store the
LetDecl in the state of FolderM.
Instances For
A wrapper around mkAuxLetDecl that also calls mkLit.
Instances For
Instances For
Instances For
Instances For
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
Instances For
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
Instances For
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
Instances For
Turn a unary function such as Nat.succ into a constant folder.
Instances For
Turn a binary function such as Nat.add into a constant folder.
Instances For
Instances For
Provide a folder for an operation with a left neutral element.
Instances For
Provide a folder for an operation with a right neutral element.
Instances For
Provide a folder for an operation with a left annihilator.
Instances For
Provide a folder for an operation with a right annihilator.
Instances For
Instances For
Instances For
Instances For
Pick the first folder out of folders that succeeds.
Instances For
Provide a folder for an operation that has the same left and right neutral element.
Instances For
Provide a folder for an operation that has the same left and right annihilator.
Instances For
Literal folders for higher order datastructures.
Instances For
Instances For
Apply all known folders to decl.
Instances For
Instances For
Instances For
Instances For
Apply a list of default folders to decl