Documentation

Lean.Compiler.IR.Borrow

Equations
Instances For

    We perform borrow inference in a block of mutually recursive functions. Join points are viewed as local functions, and are identified using their local id + the name of the surrounding function. We keep a mapping from function and joint points to parameters (Array Param). Recall that Param contains the field borrow.

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

      Mark parameters that take a reference as borrow

      Equations
      Instances For

        We do perform borrow inference for constants marked as export. Reason: we current write wrappers in C++ for using exported functions. These wrappers use smart pointers such as object_ref. When writing a new wrapper we need to know whether an argument is a borrow inference or not. We can revise this decision when we implement code for generating the wrappers automatically.

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

            Apply the inferred borrow annotations stored at ParamMap to a block of mutually recursive functions.

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

                        Updates map[k] using the current set of owned variables.

                        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

                            For each ps[i], if ps[i] is owned, then mark xs[i] as owned.

                            Equations
                            Instances For

                              For each xs[i], if xs[i] is owned, then mark ps[i] as owned. We use this action to preserve tail calls. That is, if we have a tail call f xs, if the i-th parameter is borrowed, but xs[i] is owned we would have to insert a dec xs[i] after f xs and consequently "break" the tail call.

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

                                Mark xs[i] as owned if it is one of the parameters ps. We use this action to mark function parameters that are being "packed" inside constructors. This is a heuristic, and is not related with the effectiveness of the reset/reuse optimization. It is useful for code such as

                                def f (x y : obj) :=
                                let z := ctor_1 x y;
                                ret z
                                
                                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

                                          Keep executing x until it reaches a fixpoint

                                          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