the extension to continuation based contification

[Matthew Fluet]

Is it possible to only introduce the "return to X" continuations if the
analysis hits top for the function X?  Once it is determined that some
top-level function (say F) has more than one continuation, there's no hope
for contifying it; so, rather than propagating that non-contification
through to functions whose continuations are F, establish a "return to F"
continuation for the analysis of the body of F, maybe allowing other
functions to be contified into F.  I think this corresponds to changing
the definition of Reppy's join to something like:

Gamma1 join Gamma2
= { F -> K' | F \in dom(Gamma1) U dom(Gamma2),
              K' = case(Gamma1(F),Gamma2(F))
                     of (bot,bot) => bot
                      | (bot,K) => K
                      | (K,bot) => K
                      | (K1,K2) => if K1 = K2 
                                    then K1
                                    else KF ("return to F continuation") } 

This certainly breaks the RCont domain, but I think that might be o.k.,
because we really only care about the domain of maps from function labels
to continuations.  But I'm not sure what that does to the fixed-point I
think is being taken over the set of mutually recursive top-level CPS
functions.

In any event, I'd be interested in looking at the implementation of the
continuation contification pass for MLton, at least to see if my quick
sketch of translating Reppy's analysis to the CPS IL is close.