Documentation

Lean.Compiler.LCNF.JoinPoints

  • arity : Nat

    The arity of the candidate

  • The set of candidates that rely on this candidate to be a join point. For a more detailed explanation see the documentation of find

Info about a join point candidate (a fun declaration) during the find phase.

Instances For

    The state for the join point candidate finder.

    Instances For

      Find all fun declarations that qualify as a join point, that is:

      • are always fully applied
      • are always called in tail position

      Where a fun f is in tail position iff it is called as follows:

      let res := f arg
      res
      

      The majority (if not all) tail calls will be brought into this form by the simplifier pass.

      Furthermore a fun disqualifies as a join point if turning it into a join point would turn a call to it into an out of scope join point. This can happen if we have something like:

      def test (b : Bool) (x y : Nat) : Nat :=
        fun myjp x => Nat.add x (Nat.add x x)
        fun f y =>
          let x := Nat.add y y
          myjp x
        fun f y =>
          let x := Nat.mul y y
          myjp x
        cases b (f x) (g y)
      

      f and g can be detected as a join point right away, however myjp can only ever be detected as a join point after we have established this. This is because otherwise the calls to myjp in f and g would produce out of scope join point jumps.

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

        Replace all join point candidate fun declarations with jp ones and all calls to them with jmps.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          • currentJp? : Option Lean.FVarId

            The FVarId of the current join point if we are currently inside one.

          • candidates : Lean.FVarIdSet

            The list of valid candidates for extending the context. This will be all let and fun declarations as well as all jp parameters up until the last fun declaration in the tree.

          The context managed by ExtendM.

          Instances For

            The state managed by ExtendM.

            Instances For
              @[inline, reducible]

              The monad for the extendJoinPointContext pass.

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

                Replace a free variable if necessary, that is:

                • It is in the list of candidates
                • We are currently within a join point (if we are within a function there cannot be a need to replace them since we dont extend their context)
                • Said join point actually has a replacement parameter registered. otherwise just return fvar.
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  Add a new candidate to the current scope + to the list of candidates if we are currently within a join point. Then execute x.

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

                    Same as withNewCandidate but with multiple FVarIds.

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

                      Extend the context of the current join point (if we are within one) by fvar if necessary. This is necessary if:

                      • fvar is not in scope (that is, was declared outside of the current jp)
                      • we have not already extended the context by fvar
                      • the list of candidates contains fvar. This is because if we have something like:
                        let x := ..
                        fun f a =>
                          jp j b =>
                            let y := x
                            y
                        
                        There is no point in extending the context of j by x because we cannot lift a join point outside of a local function declaration.
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        Merge the extended context of two join points if necessary. That is if we have a structure such as:

                        jp j.1 ... =>
                          jp j.2 .. =>
                            ...
                          ...
                        

                        And we are just done visiting j.2 we want to extend the context of j.1 by all free variables that the context of j.2 was extended by as well because we need to drag these variables through at the call sites of j.2 in j.1.

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

                          We call this whenever we enter a new local function. It clears both the current join point and the list of candidates since we cant lift join points outside of functions as explained in mergeJpContextIfNecessary.

                          Equations
                          Instances For

                            We call this whenever we enter a new join point. It will set the current join point and extend the list of candidates by all of the parameters of the join point. This is so in the case of nested join points that refer to parameters of the current one we extend the context of the nested join points by said parameters.

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

                              We call this whenever we visit a new arm of a cases statement. It will back up the current scope (since we are doing a case split and want to continue with other arms afterwards) and add all of the parameters of the match arm to the list of candidates.

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

                                Use all of the above functions to find free variables declared outside of join points that said join points can be reasonaly extended by. Reasonable meaning that in case the current join point is nested within a function declaration we will not extend it by free variables declared before the function declaration because we cannot lift join points outside of function declarations.

                                All of this is done to eliminate dependencies of join points onto their position within the code so we can pull them out as far as possible, hopefully enabling new inlining possibilities in the next simplifier run.

                                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

                                    Context for ReduceAnalysisM.

                                    Instances For

                                      State for ReduceAnalysisM.

                                      Instances For
                                        @[inline, reducible]
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For

                                          Take a look at each join point and each of their call sites. If all call sites of a join point have one or more arguments in common, for example:

                                          jp _jp.1 a b c => ...
                                          ...
                                          cases foo
                                          | n1 => jmp _jp.1 d e f
                                          | n2 => jmp _jp.1 g e h
                                          

                                          We can get rid of the common argument in favour of inlining it directly into the join point (in this case the e). This reduces the amount of arguments we have to pass around drastically for example in ReaderT based monad stacks.

                                          Note 1: This transformation can in certain niche cases obtain better results. For example:

                                          jp foo a b => ..
                                          let x := ...
                                          cases discr
                                          | n1 => jmp foo x y
                                          | n2 => jmp foo x z
                                          

                                          Here we will not collapse the x since it is defined after the join point foo and thus not accessible for substitution yet. We could however reorder the code in such a way that this is possible, this is currently not done since we observe than in praxis most of the applications of this transformation can occur naturally without reordering.

                                          Note 2: This transformation is kind of the opposite of JoinPointContextExtender. However we still benefit from the extender because in the simp run after it we might be able to pull join point declarations further up in the hierarchy of nested functions/join points which in turn might enable additional optimizations. After we have performed all of these optimizations we can take away the (remaining) common arguments and end up with nicely floated and optimized code that has as little arguments as possible in the join points.

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

                                            Find all fun declarations in decl that qualify as join points then replace their definitions and call sites with jp/jmp.

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