RSSA

[Stephen Weeks]

> O.k.  Here's a more serious concern.  Many of the primitives that are
> implemented via Ccalls (the impCCall predicate) need to work with the
> returned value; e.g., all the intInf operations are implemented as
> C-calls, but after returning from C, I need to update the frontier and
> extract the real result.  So, I think CReturn needs a Prim.t, so I know
> what to do; that gets messy, because it means that the implementation of a
> lot of primitives need be split into what to do at the CCall and what to
> do at the CReturn.

This is just a question of source code textual distance, right?  For
each prim I'd define two functions (e.g. coshBefore and coshAfter) and
put the definitions next to each other.  Then I don't think it's messy
or hard to maintain even if the calls are distant.