safe for space ... and IntInf

[Stephen Weeks]

> I  was  thinking  about the flattener, and realized that if you don't require
> the flatten-ness of a procedure  result  to  be  the  same  as  that  of  any
> procedures it tail-calls to you won't be safe-for-space.  The problem is that
> unlike other coercions, where you only coerce up a finite lattice,  here  you
> can have loops.  I.e., if f tail-calls g and the result of f is flat and that
> of g is non-flat and g tail-calls f, then both of those tail-calls will  turn
> into non-tail-calls and you will use unbounded space.

You are correct.  Here is your example fleshed out.

fun isEven x = x mod 2 = 0
fun isOdd x = x mod 2 = 1
fun f(x: int): int * int = if isOdd x andalso x > 0 then g(x - 1) else (13, 15)
and g(x: int): int * int = if isEven x then f(x - 1) else (17, 19)
val _ = f 101

> Is this restriction currently in place (I.e., are we safe for space now)?

Yes.  Right now, the flattener never changes tail calls into non-tail
calls.   However, other Cps simplification passes, like useless.fun,
do turn tail calls into nontail calls.  I think useless is ok because
it has the one-way property (you can only coerce something that's
useful into something that's useless, but not vice versa).

Your mail also came at a fortunate time, as I was trying to track down 
a seg fault I was getting in the smith-normal-form regression test.
For stress testing, I turned off all the cps simplify passes (except
for poly equal) and ran the regressions.  smith-normal-form failed
with a seg fault when compiled normally, and failed with an assertion
failure in IntInf_do_neg when compiled -g.  The assertion failure was
right at the beginning, checking that the frontier is in the expected
place.
	assert(frontier == (pointer)&bp->limbs[bp->card - 1]);
I'd been tracking this bug for a couple hours when I received your
mail about the flattener.  Do you see the connection? :-)  As a
reminder, here is the code for bigNegate

	 fun bigNegate (arg: bigInt): bigInt =
		if Prim.isSmall arg
		      then let val argw = Prim.toWord arg
			   in if argw = badw
				 then negBad
				 else Prim.fromWord (Word.- (0w2, argw))
			   end
		      else Prim.~ (arg, allocate (1 + bigSize arg))

The problem is, when the flattener is turned off, there is an
allocation in between the call to allocate and the Prim.~ call.  The
argument tuple allocation screws everything up.  So, we are relying on 
the flattener for correctness of the IntInf implementation.  Any ideas 
on how to improve the implementation to remove this reliance, or at
least put an assert somewhere to avoid falling prey to this bug again?