[MLton] What are the semantics for Word_addCheck?

[Ben Chambers]

Quoting Matthew Fluet <fluet@cs.cornell.edu>:

>
> > What are the semantics for Word_addCheck?
>
>               | Word_addCheck of WordSize.t * {signed: bool} (* codegen *)
>
> In the (S)XML intermediate language, it performs a twos compliment
> addition of two values of the appropriate WordSize, implicitly raising the
> Overflow exception.  The {signed: bool} component determines whether the
> addition is signed or unsigned for the purposes of overflow checking.
>
> In the later intermediate languages, the Word_addCheck primitive may only
> appear in an Arith transfer, where it explicitly names the success and
> overflow labels.
>
> > Also, what other primitives are we likely to come across in a simple
> program?
>
> If you are pulling in the Basis Library, you are likely to see most of
> them.  The notable exceptions are that you won't encounter:
>    MLton_deserialize
>    MLton_serialize
>    MLton_share
>    MLton_size
>    MLton_touch
>    Thread_*
>    Weak_*
>    World_save
>
> Also, assuming that you are performing the CPS transform on the SXML
> intermediate language but after the SXML simplification (which would
> probably be the best place to do so), then you also won't see:
>    Exn_*
>    TopLevel_*
>
> > Basically, we've finished a CPS transform, and we're now trying to
> interpret
> > them in order to ensure that the transform was correct (before we start
> running
> > things like Delta CFA and Gamma CFA on them).  Most of the interpreter is
> > written except for the Prim Ops, and we're trying to figure out what those
> do
> > and how they work.
>
> Could you explain a little more what you are doing?  You are writing an
> interpreter for the SXML intermediate language?  That seems like quite a
> bit of work.  Can't you just continue compiling the CPS transformed
> program?

We're writing a little interpreter to test the implementation of the CPS
language.  Also, the CFAs we're planning on writing proceed in a very similar
manner to the interpreter, so it'll actually be a useful starting point for
those.  We are not trying to write a fully feature interpreter for either CPS or
 SXML, merely something that can appropriately follow the control flow paths.

Thanks for the description of the Primitives, it'll be vastly useful as we run
across ones that we haven't implemented yet!

-- Ben Chambers