Documentation

Lean.Compiler.LCNF.ToLCNF

Return true if e is a lcProof application. Recall that we use lcProof to erase all nested proofs.

Equations
Instances For
    @[reducible, inline]

    State for BindCasesM monad Mapping from _alt.<idx> variables to new join points

    Equations
    Instances For

      This method returns code that at each exit point of cases, it jumps to jpDecl. It is similar to Code.bind, but we add special support for inlineMatcher. The inlineMatcher function inlines the auxiliary _match_<idx> declarations. To make sure there is no code duplication, inlineMatcher creates auxiliary declarations _alt.<idx>. We can say the _alt.<idx> declarations are pre join points. For each auxiliary declaration used at an exit point of cases, this method creates an new auxiliary join point that invokes _alt.<idx>, and then jumps to jpDecl. The goal is to make sure the auxiliary join point is the only occurrence of _alt.<idx>, then simp will inline it. That is, our goal is to try to promote the pre join points _alt.<idx> into a proper join point.

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

                Add LCNF element to the current sequence

                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

                      Create Code that executes the current seq and then returns result

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

                                  Create a new local declaration using a Lean regular type.

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

                                            Eta-expand with n lambdas.

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

                                              Eta reduce implicits. We use this function to eliminate introduced by the implicit lambda feature, where it generates terms such as fun {α} => ReaderT.pure

                                              Put the given expression in LCNF.

                                              • Nested proofs are replaced with lcProof-applications.
                                              • Eta-expand applications of declarations that satisfy shouldEtaExpand.
                                              • Put computationally relevant expressions in A-normal form.
                                              Equations
                                              Instances For

                                                Giving f a constant .const declName us, convert args into args', and return .const declName us args'

                                                If args.size == arity, then just return app. Otherwise return

                                                let k := app
                                                k args[arity:]
                                                

                                                Visit a matcher/casesOn alternative.