Documentation

Lean.Compiler.IR.Borrow

@[inline, reducible]
Instances For
    @[inline, reducible]
    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.

      @[inline, reducible]
      Instances For

        Mark parameters that take a reference as borrow

        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.

          Instances For

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

            Instances For
              @[inline, reducible]
              abbrev Lean.IR.Borrow.M (α : Type) :
              Instances For

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

                Instances For

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

                  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.

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

                        Keep executing x until it reaches a fixpoint