contification paper

[Matthew Fluet]

> > We may repeatedly
> > walk over a function body because it is successively contified in
> > other functions.
> 
> I don't understand this comment in 4.3.  Do you still believe it?  Is it worth
> mentioning?

It depends on how we define the transformation.  Here's the example I'm
thinking of:

fun fm () = ... K (f ()) ...
fun f () = ... g () ...
fun g () = ... h () ...
fun h () = ...

Now, a safe analysis is
A(fm) = Unknown
A(f) = K
A(g) = f
A(h) = Unknown
This doesn't correspond to any of our analyses, but it is safe.

I could see one transformation that just handled functions one at a time,
where we would go to:

fun fm () = ... K (f ()) ...
fun f () = let fun g () = ... h () ... ; ... g () ... 
fun h () = ...

and then to

fun fm () = let fun K () = ...
                fun f () = let fun g () = ... K (h ()) ... ; ... g () ... ;
            ...

And, in one sense, we walked over the body of g once when we contified it
in f and again when we contified f in fm.


But, I think Steve has a better transformation in mind.  If I have it
right, there is one top level transformer, on the program:

T[fm] = fm
T[let f(<x>) = e in P] = if A(f) = Unknown
                           then let f(<x>) = T'[e] in T[P]
                           else T[P]

which removes any function which isn't being kept at the top level, and
recursively walks over the ones that are.

Then T' is the recusive walk over the expression which appropriately
replaces nontail calls with tail calls, jumps to returns, and also inserts
the contified functions.  But I need to think a little more about the
right way to write T'.

Under this type of transformation, then the comment above doesn't apply.
And I think this is the better way to present it; we can probably also
drop that comment about the forest of two trees rooted at Uncalled and
Unknown.  That is more for the type of transformation I described above.