Documentation

Lean.Compiler.IR.LiveVars

Remark: in the paper "Counting Immutable Beans" the concepts of free and live variables coincide because the paper does not consider join points. For example, consider the function body B

let x := ctor_0;
jmp block_1 x

in a context where we have the join point block_1 defined as

block_1 (x : obj) : obj :=
let z := ctor_0 x y;
ret z

The variable y is live in the function body B since it occurs in block_1 which is "invoked" by B.

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

We use State Context instead of ReaderT Context Id because we remove non local joint points from Context whenever we visit them instead of maintaining a set of visited non local join points.

Remark: we don't need to track local join points because we assume there is no variable or join point shadowing in our IR.

Equations
    Instances For
      @[reducible, inline]
      Equations
        Instances For
          @[reducible, inline]
          Equations
            Instances For
              @[reducible, inline]
              abbrev Lean.IR.IsLive.visitArg (w : Index) (a : Arg) :
              Equations
                Instances For
                  @[reducible, inline]
                  Equations
                    Instances For
                      @[reducible, inline]
                      Equations
                        Instances For

                          Return true if x is live in the function body b in the context ctx.

                          Remark: the context only needs to contain all (free) join point declarations.

                          Recall that we say that a join point j is free in b if b contains FnBody.jmp j ys and j is not local.

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