cps & contification

[Stephen Weeks]

> (f,g) in TailCall corresponds to something like:
...
> I.e., the caller is f and the callee is g, with no notion that g is
> really being called in L_1? or even deeper lexical nesting?

Right.  No notion of lexical nesting.

> Second question, relating to the safety constraints below, is it possible
> for a local function to be unused?  If so, then although g is
> called in L_1, it may not be the case that g is really called by f.

Local functions are never unused.  

> (f,g,j) in NonTailCall corresponds to something like:
> 
> fun f (...)
>   = let
>       fun L_1 (...)
>         = ...
>       fun L_2 (...)
>         = L_1(g(...))
>     in
>       ...
>     end
> 
> Again, no notion that g is really being called in L_2, although it is
> returning to the continuation L_1?

Right.  This would be (f, g, L_1).

>  How about the possibility that L_2 is
> never called; in which case does g really ever return to L_1?

Can't happen.

> > An analysis A is safe for program p = (fm, T, N) if 
> > 	*   A(fm) = fm
> 
> Does        A(fm) = Unknown
> make more sense? 

Yes.

> > 	**  For all nontail calls (f, g, j) in N, either
> > 		A(f) = Uncalled
> > 		or A(g) in {Uncalled, Unknown, j}
> > 	*** For all tail calls (f, g) in T, either 
> > 		A(f) = Uncalled
> > 		or A(g) in {Unknown, f, A(f)}
> 
> Assuming an exclusive or, if A(f) <> Uncalled, why can A(g) = Uncalled in
> non-tail calls but not in tail calls.

That is a mistake.  The nontail condition should read

 		A(f) = Uncalled
 		or A(g) in {Unknown, j}

BTW, the or is not an exclusive or.  It is the usual mathematical or.

> > 3. If A(f) in Jump and there is a path of tail calls from f to g
> >    then A(g) in {Unknown, A(f)} U Fun
> > 	Proof: by induction on the length of the path.
> 
> Does this fact depend on A(f) in Jump, or just A(f) <> Uncalled?  

Just the latter.  Good point.

> > 2. For all functions that are marked Unknown, we need to run a second analysis
> > 	that determines if they can be contified within another function.  To 
> > 	me this feels like doing some kind of scc or dominator calculation on
> > 	the graph of tail calls, but I don't quite see it yet.
> 
> I agree that there is a graph feel to this problem, but I don't see it yet
> either.

I've almost got a dominator approach worked out.  I should be able to send mail
with it later today.