Documentation

Lean.Compiler.LCNF.Simp.ConstantFold

@[reducible, inline]

A constant folding monad, the additional state stores auxiliary declarations required to build the new constant.

Equations
@[reducible, inline]

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

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

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

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