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
    Instances For
      @[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
        Instances For

          A typeclass for detecting and producing literals of arbitrary types inside of LCNF.

          • getLit : FVarIdCompilerM (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 LetDecls + a final Expr putting 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
              Instances For
                def Lean.Compiler.LCNF.Simp.ConstantFold.mkAuxLit {α : Type} [Literal α] (x : α) (prefixName : Name := `_x) :

                A wrapper around mkAuxLetDecl that also calls mkLit.

                Equations
                  Instances For
                    def Lean.Compiler.LCNF.Simp.ConstantFold.mkNatWrapperInstance {α : Type} [Inhabited α] (ofNat : Natα) (ofNatName : Name) (toNat : αNat) :
                    Equations
                      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
                            
                            Equations
                              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
                                
                                Equations
                                  Instances For
                                    def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.mkUnary {α β : Type} [Literal α] [Literal β] (folder : αβ) :

                                    Turn a unary function such as Nat.succ into a constant folder.

                                    Equations
                                      Instances For
                                        def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.mkBinary {α β γ : Type} [Literal α] [Literal β] [Literal γ] (folder : αβγ) :

                                        Turn a binary function such as Nat.add into a constant folder.

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

                                                Provide a folder for an operation with a left neutral element.

                                                Equations
                                                  Instances For

                                                    Provide a folder for an operation with a right neutral element.

                                                    Equations
                                                      Instances For

                                                        Provide a folder for an operation with a left annihilator.

                                                        Equations
                                                          Instances For

                                                            Provide a folder for an operation with a right annihilator.

                                                            Equations
                                                              Instances For
                                                                def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.divShift {α : Type} [Literal α] [BEq α] (shiftRight : Name) (pow2 log2 : αα) :
                                                                Equations
                                                                  Instances For
                                                                    def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.mulRhsShift {α : Type} [Literal α] [BEq α] (shiftLeft : Name) (pow2 log2 : αα) :
                                                                    Equations
                                                                      Instances For
                                                                        def Lean.Compiler.LCNF.Simp.ConstantFold.Folder.mulLhsShift {α : Type} [Literal α] [BEq α] (shiftLeft : Name) (pow2 log2 : αα) :
                                                                        Equations
                                                                          Instances For

                                                                            Pick the first folder out of folders that succeeds.

                                                                            Equations
                                                                              Instances For

                                                                                Provide a folder for an operation that has the same left and right neutral element.

                                                                                Equations
                                                                                  Instances For

                                                                                    Provide a folder for an operation that has the same left and right annihilator.

                                                                                    Equations
                                                                                      Instances For

                                                                                        Literal folders for higher order datastructures.

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

                                                                                                Folder for ofNat operations on fixed-sized integer types.

                                                                                                Equations
                                                                                                  Instances For

                                                                                                    All arithmetic folders.

                                                                                                    Equations
                                                                                                      Instances For

                                                                                                        All string folders.

                                                                                                        Equations
                                                                                                          Instances For

                                                                                                            Apply all known folders to decl.

                                                                                                            Equations
                                                                                                              Instances For
                                                                                                                Instances For
                                                                                                                  Equations
                                                                                                                    Instances For

                                                                                                                      Apply a list of default folders to decl

                                                                                                                      Equations
                                                                                                                        Instances For