Documentation

Propagate arguments of application inwards; except for Lam where the argument becomes let-bound. appProp tries to propagate as many arguments as possible, down as many levels as possible; and should be called in a top-down traversal.

The idea is that this reduces the number of traversals, which hopefully leads to shorter compile times.

Note [AppProp no shadowing]

Case 1.

Imagine:

(case x of
   D a b -> h a) (f x y)

rewriting this to:

let b = f x y
in  case x of
      D a b -> h a b

is very bad because b in h a b is now bound by the pattern instead of the newly introduced let-binding

instead we must deshadow w.r.t. the new variable and rewrite to:

let b = f x y
in  case x of
      D a b1 -> h a b

Case 2.

Imagine

(x -> e) u

where u has a free variable named x, rewriting this to:

let x = u
in  e

would be very bad, because the let-binding suddenly captures the free variable in u. To prevent this from happening we over-approximate and check whether x is in the current InScopeSet, and deshadow if that's the case, i.e. we then rewrite to:

let x1 = u
in  e [x:=x1]

Case 3.

The same for:

(let x = w in e) u

where u again has a free variable x, rewriting this to:

let x = w in (e u)

would be bad because the let-binding now captures the free variable in u.

To prevent this from happening, we unconditionally deshadow the function part of the application w.r.t. the free variables in the argument part of the application. It is okay to over-approximate in this case and deshadow w.r.t the current InScopeSet.

Specialize functions on arguments which are constant, except when they are clock, reset generators.

Specialize an application on its argument

Specialize functions on their non-representable argument

Specialize functions on their type

Specialize functions on arguments which are zero-width. These arguments can have only one possible value, and specializing on this value may create additional opportunities for transformations to fire.

As we can't remove zero-width arguements (as transformations cannot change the type of a term), we instead substitute all occurances of a lambda-bound variable with a zero-width type with the only value of that type.