CWS paper

[Matthew Fluet]

I was looking at the revised contify analysis that I proposed, and I
realized that there isn't any need to make a distinction between function
labels and "return to f" labels.  It still all works out with the ordering

bot <=l l' <=l l   forall l' in Label

the join operation:

Gamma1 V Gamma2
 = {l |--> r | l in Label
               r = case (Gamma1(x), Gamma2(x))
                     of (bot, r') => r'
                      | (r', bot) => r'
                      | (r1, r2) => if r1 = r2
                                     then r1
                                     else l}

and the condition

If Gamma = Anal[program]  and Gamma(l) = r  and  r <> l, r <> bot,
 then the function with label l has exactly one continuation 
 and is contifiable.
Further, if Gamma(l) = bot, then the function with label l is never called.