A constant folding monad, the additional state stores auxiliary declarations required to build the new constant.
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.
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α.getLit : Lean.FVarId → Lean.Compiler.LCNF.CompilerM (Option α)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.
Equations
- One or more equations did not get rendered due to their size.
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
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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 [] #[])
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
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.
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.
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.
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.
Equations
- One or more equations did not get rendered due to their size.
Provide a folder for an operation with a left neutral element.
Equations
- One or more equations did not get rendered due to their size.
Provide a folder for an operation with a right neutral element.
Equations
- One or more equations did not get rendered due to their size.
Provide a folder for an operation with a left annihilator.
Equations
- One or more equations did not get rendered due to their size.
Provide a folder for an operation with a right annihilator.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Pick the first folder out of folders that succeeds.
Equations
- One or more equations did not get rendered due to their size.
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.
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.
Literal folders for higher order datastructures.
Equations
Equations
- One or more equations did not get rendered due to their size.
All arithmetic folders.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
All string folders.
Equations
- One or more equations did not get rendered due to their size.
Apply all known folders to decl.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
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
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