A constant folding monad, the additional state stores auxiliary declarations required to build the new constant.
Equations
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.
Equations
Instances For
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
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α.
Instances
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
A wrapper around mkAuxLetDecl that also calls mkLit.
Instances For
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
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
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.
Equations
- One or more equations did not get rendered due to their size.
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
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
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
Equations
- One or more equations did not get rendered due to their size.
Instances For
All arithmetic folders.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Apply all known folders to decl.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Instances For
Apply a list of default folders to decl