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

      Create the temporary lcProof

      Equations
        Instances For

          Auxiliary inductive datatype for constructing LCNF Code objects. The toLCNF function maintains a sequence of elements that is eventually converted into Code.

          Instances For
            @[reducible, inline]

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

            Equations
              Instances For
                @[reducible, inline]

                Auxiliary monad for implementing bindCases

                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
                      Instances For
                        @[irreducible]
                        Equations
                          Instances For
                            • Local context containing the original Lean types (not LCNF ones).

                            • cache : PHashMap Expr Arg

                              Cache from Lean regular expression to LCNF argument.

                            • typeCache : Std.HashMap Expr Expr
                            • isTypeFormerTypeCache : Std.HashMap Expr Bool

                              isTypeFormerType cache

                            • LCNF sequence, we chain it to create a LCNF Code object.

                            • toAny : FVarIdSet

                              Fields that are type formers must be replaced with in the resulting code. Otherwise, we have data occurring in types. When converting a casesOn into LCNF, we add constructor fields that are types and type formers into this set. See visitCases.

                            Instances For
                              @[reducible, inline]
                              Equations
                                Instances For
                                  @[inline]
                                  Equations
                                    Instances For

                                      Add LCNF element to the current sequence

                                      Equations
                                        Instances For
                                          Equations
                                            Instances For
                                              Equations
                                                Instances For
                                                  def Lean.Compiler.LCNF.ToLCNF.letValueToArg (e : LetValue) (prefixName : Name := `_x) :
                                                  Equations
                                                    Instances For

                                                      Create Code that executes the current seq and then returns result

                                                      Equations
                                                        Instances For
                                                          Equations
                                                            Instances For
                                                              Equations
                                                                Instances For
                                                                  Equations
                                                                    Instances For
                                                                      Equations
                                                                        Instances For
                                                                          Equations
                                                                            Instances For
                                                                              def Lean.Compiler.LCNF.ToLCNF.mkParam (binderName : Name) (type : Expr) :

                                                                              Create a new local declaration using a Lean regular type.

                                                                              Equations
                                                                                Instances For
                                                                                  def Lean.Compiler.LCNF.ToLCNF.mkLetDecl (binderName : Name) (type value type' : Expr) (arg : Arg) :
                                                                                  Equations
                                                                                    Instances For
                                                                                      Equations
                                                                                        Instances For
                                                                                          Equations
                                                                                            Instances For
                                                                                              Equations
                                                                                                Instances For

                                                                                                  Eta-expand with n lambdas.

                                                                                                  Equations
                                                                                                    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'

                                                                                                          Eta expand if under applied, otherwise apply k

                                                                                                          partial def Lean.Compiler.LCNF.ToLCNF.toLCNF.mkOverApplication (app : Arg) (args : Array Expr) (arity : Nat) :

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

                                                                                                          let k := app
                                                                                                          k args[arity:]
                                                                                                          
                                                                                                          partial def Lean.Compiler.LCNF.ToLCNF.toLCNF.visitAlt (ctorName : Name) (numParams : Nat) (e : Expr) :

                                                                                                          Visit a matcher/casesOn alternative.