IntInf asserts

[Stephen Weeks]

> My thoughts were somthing like this: switching the type of
> the IntInf primitives basically requires some function of the form: 
> 
> val bytesNeeded: {prim: Prim.t, args: 'a vector} -> 'a option
...
> I think it would be better if LimitCheck statements were the only things
> that gave rise to limit checks; if bytesNeeded {prim, args} = SOME x, for
> some Assign {dst, prim, args, ...} statement, then the limit check
> insertion code needs to ensure that x bytes are available at the Assign
> statement.  (I think this fits in better with the limit check insertion
> formalization.)  This means that LimitCheck statement would have bytes as
> an Operand.t instead of int.

Looks good to me.  This cleans up the current world and makes
integration with they new approach to IntInf easy.

> How would this work in practice?  IntInf_* are easy, with the proposal to
> give them the type
>    val add = _prim "IntInf_add": int * int * Int.int -> int
> Then
> fun bytesNeeded {prim, args} =
>    case Prim.name prim of
>       IntInf_add => Vector.sub (args, 2)
>     | ...

Yep.

> Array_array is a little harder.  What I would propose is a quick rewrite
> after Representations have been establised.  

Sounds reasonable.

> Err... Need to run to colloquium, but there is a little more.  The major
> point of this is that it might give the pass that actually chooses the
> number of bytes for a limit check a little more freedom.  

Also good.

And I agree that it fits with in our forthcoming formalization, which
is on the todo after the exceptions paper, which is on the todo after
the shrinker, ...