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.

      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
          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
                Equations
                • One or more equations did not get rendered due to their size.
                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
                    • One or more equations did not get rendered due to their size.
                    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
                      • One or more equations did not get rendered due to their size.
                      Instances For

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

                          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.
                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.
                            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.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  Provide a folder for an operation with a left annihilator.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    Provide a folder for an operation with a right annihilator.

                                    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
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For

                                            Pick the first folder out of folders that succeeds.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For

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

                                                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.
                                                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
                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For

                                                        All string 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
                                                            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