Documentation

Lean.Compiler.IR.Basic

Implements (extended) λPure and λRc proposed in the article "Counting Immutable Beans", Sebastian Ullrich and Leonardo de Moura.

The Lean to IR transformation produces λPure code, and this part is implemented in C++. The procedures described in the paper above are implemented in Lean.

@[reducible, inline]

Function identifier

Equations
Instances For
    @[reducible, inline]
    Equations
    Instances For
      structure Lean.IR.VarId :

      Variable identifier

      Instances For
        Equations

        Join point identifier

        Instances For
          @[reducible, inline]
          Equations
          Instances For
            Equations
            @[reducible, inline]
            Equations
            Instances For
              @[reducible, inline]
              Equations
              Instances For
                inductive Lean.IR.IRType :

                Low Level IR types. Most are self explanatory.

                • usize represents the C++ size_t Type. We have it here because it is 32-bit in 32-bit machines, and 64-bit in 64-bit machines, and we want the C++ backend for our Compiler to generate platform independent code.

                • irrelevant for Lean types, propositions and proofs.

                • object a pointer to a value in the heap.

                • tobject a pointer to a value in the heap or tagged pointer (i.e., the least significant bit is 1) storing a scalar value.

                • struct and union are used to return small values (e.g., Option, Prod, Except) on the stack.

                Remark: the RC operations for tobject are slightly more expensive because we first need to test whether the tobject is really a pointer or not.

                Remark: the Lean runtime assumes that sizeof(void*) == sizeof(sizeT). Lean cannot be compiled on old platforms where this is not True.

                Since values of type struct and union are only used to return values, We assume they must be used/consumed "linearly". We use the term "linear" here to mean "exactly once" in each execution. That is, given x : S, where S is a struct, then one of the following must hold in each (execution) branch. 1- x occurs only at a single ret x instruction. That is, it is being consumed by being returned. 2- x occurs only at a single ctor. That is, it is being "consumed" by being stored into another struct/union. 3- We extract (aka project) every single field of x exactly once. That is, we are consuming x by consuming each of one of its components. Minor refinement: we don't need to consume scalar fields or struct/union fields that do not contain object fields.

                Instances For
                  Equations
                  Instances For
                    Equations
                    Instances For
                      Equations
                      Instances For
                        inductive Lean.IR.Arg :

                        Arguments to applications, constructors, etc. We use irrelevant for Lean types, propositions and proofs that have been erased. Recall that for a Function f, we also generate f._rarg which does not take irrelevant arguments. However, f._rarg is only safe to be used in full applications.

                        Instances For
                          @[export lean_ir_mk_var_arg]
                          Equations
                          Instances For
                            inductive Lean.IR.LitVal :
                            Instances For
                              Equations
                              Instances For

                                Constructor information.

                                • name is the Name of the Constructor in Lean.
                                • cidx is the Constructor index (aka tag).
                                • size is the number of arguments of type object/tobject.
                                • usize is the number of arguments of type usize.
                                • ssize is the number of bytes used to store scalar values.

                                Recall that a Constructor object contains a header, then a sequence of pointers to other Lean objects, a sequence of USize (i.e., size_t) scalar values, and a sequence of other scalar values.

                                Instances For
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    Equations
                                    Instances For
                                      Equations
                                      • info.isScalar = !info.isRef
                                      Instances For
                                        inductive Lean.IR.Expr :
                                        Instances For
                                          @[export lean_ir_mk_ctor_expr]
                                          def Lean.IR.mkCtorExpr (n : Lake.Name) (cidx : Nat) (size : Nat) (usize : Nat) (ssize : Nat) (ys : Array Lean.IR.Arg) :
                                          Equations
                                          Instances For
                                            @[export lean_ir_mk_proj_expr]
                                            Equations
                                            Instances For
                                              @[export lean_ir_mk_uproj_expr]
                                              Equations
                                              Instances For
                                                @[export lean_ir_mk_sproj_expr]
                                                Equations
                                                Instances For
                                                  @[export lean_ir_mk_fapp_expr]
                                                  Equations
                                                  Instances For
                                                    @[export lean_ir_mk_papp_expr]
                                                    Equations
                                                    Instances For
                                                      @[export lean_ir_mk_app_expr]
                                                      Equations
                                                      Instances For
                                                        @[export lean_ir_mk_num_expr]
                                                        Equations
                                                        Instances For
                                                          @[export lean_ir_mk_str_expr]
                                                          Equations
                                                          Instances For
                                                            structure Lean.IR.Param :
                                                            Instances For
                                                              Equations
                                                              @[export lean_ir_mk_param]
                                                              Equations
                                                              Instances For
                                                                inductive Lean.IR.AltCore (FnBody : Type) :
                                                                Instances For
                                                                  inductive Lean.IR.FnBody :
                                                                  Instances For
                                                                    @[export lean_ir_mk_vdecl]
                                                                    Equations
                                                                    Instances For
                                                                      @[export lean_ir_mk_jdecl]
                                                                      Equations
                                                                      Instances For
                                                                        @[export lean_ir_mk_uset]
                                                                        Equations
                                                                        Instances For
                                                                          @[export lean_ir_mk_sset]
                                                                          Equations
                                                                          Instances For
                                                                            @[export lean_ir_mk_case]
                                                                            Equations
                                                                            Instances For
                                                                              @[export lean_ir_mk_ret]
                                                                              Equations
                                                                              Instances For
                                                                                @[export lean_ir_mk_jmp]
                                                                                Equations
                                                                                Instances For
                                                                                  @[export lean_ir_mk_unreachable]
                                                                                  Equations
                                                                                  Instances For
                                                                                    @[reducible, inline]
                                                                                    Equations
                                                                                    Instances For
                                                                                      @[reducible, match_pattern, inline]
                                                                                      Equations
                                                                                      Instances For
                                                                                        @[reducible, match_pattern, inline]
                                                                                        Equations
                                                                                        Instances For
                                                                                          Equations
                                                                                          Instances For
                                                                                            Equations
                                                                                            Instances For
                                                                                              Equations
                                                                                              Instances For
                                                                                                @[inline]
                                                                                                Equations
                                                                                                Instances For
                                                                                                  @[inline]

                                                                                                  If b is a non terminal, then return a pair (c, b') s.t. b == c <;> b', and c.body == FnBody.nil

                                                                                                  Equations
                                                                                                  • b.split = (b.resetBody, b.body)
                                                                                                  Instances For
                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        @[inline]
                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          @[inline]
                                                                                                          Equations
                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                          Instances For
                                                                                                            @[export lean_ir_mk_alt]
                                                                                                            def Lean.IR.mkAlt (n : Lake.Name) (cidx : Nat) (size : Nat) (usize : Nat) (ssize : Nat) (b : Lean.IR.FnBody) :
                                                                                                            Equations
                                                                                                            Instances For

                                                                                                              Extra information associated with a declaration.

                                                                                                              • sorryDep? : Option Lake.Name

                                                                                                                If some <blame>, then declaration depends on <blame> which uses a sorry axiom.

                                                                                                              Instances For
                                                                                                                Equations
                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            @[export lean_ir_mk_decl]
                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              @[export lean_ir_mk_extern_decl]
                                                                                                                              Equations
                                                                                                                              Instances For
                                                                                                                                @[export lean_ir_mk_dummy_extern_decl]
                                                                                                                                Equations
                                                                                                                                Instances For
                                                                                                                                  @[reducible, inline]

                                                                                                                                  Set of variable and join point names

                                                                                                                                  Equations
                                                                                                                                  Instances For
                                                                                                                                    Equations
                                                                                                                                    Instances For
                                                                                                                                      Equations
                                                                                                                                      Instances For
                                                                                                                                        Equations
                                                                                                                                        Instances For
                                                                                                                                          Equations
                                                                                                                                          Instances For
                                                                                                                                            Equations
                                                                                                                                            Instances For
                                                                                                                                              Equations
                                                                                                                                              Instances For
                                                                                                                                                Equations
                                                                                                                                                Instances For
                                                                                                                                                  Equations
                                                                                                                                                  Instances For
                                                                                                                                                    @[reducible, inline]
                                                                                                                                                    Equations
                                                                                                                                                    Instances For
                                                                                                                                                      class Lean.IR.AlphaEqv (α : Type) :
                                                                                                                                                      Instances
                                                                                                                                                        Equations
                                                                                                                                                        Instances For
                                                                                                                                                          Equations
                                                                                                                                                          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
                                                                                                                                                                    @[reducible, inline]
                                                                                                                                                                    Equations
                                                                                                                                                                    Instances For
                                                                                                                                                                      Equations
                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                      Instances For