Denotation of open cfgs in presence of function calls

[YaZko]

This PR describes the ongoing work to denote open control flow graphs, such as in the asm language used in the tutorial, in presence of functional calls and return statements. The motivation for this PR comes from Vellvm.

Currently, we only extend asm with return statements, a Bret case in the Branch data-type, so that we do not have to bother with call-stacks. We quickly describe why this extension is already problematic.

A natural denotation for Bret r is to return the value stored in the register r. However, this impacts the type of the denotation of a block: from itree E label, we now may return a value, i.e. we now work with an itree E (label + value).

This simple modification however completely jeopardize the denotation of open programs: by relying on a loop operator over the ktree category, we rely on the uniformity of the entry and return types. Intuitively, the issue is that returning acts as an exception, so that the loop combinator do not know what to do when fed such a value.

The natural answer is naturally "since it acts as an effect, it should be an event"! However, this cannot work either. Indeed, if the event is simply parametized by the register and returning a value, then our type has not changes. To avoid carrying a value, it would have to be parameterized by the continuation, i.e. the continuation at call-site, which would require some higher-order trickery that itrees do not support.

We therefore are exploring a more blasphemous path: stranding away from the beautiful land of the freer monad and denote (before interpretation!) our programs directly into eitherT value (itree E). By doing so, the exception behavior is internalize by the eitherT monad transformers, and we recover the right type for our loop combinator.

As far as denotation is concerned, it is fairly straightforward: it only requires a slight generalization of the finite type manipulated, as well as of course lifting the Kleisli structure via the EitherT transformer (see Basics/MonadEither.v).

Things get a bit more troublesome from there. We now need a new interpreter, and as far as I can see it cannot be simply expressed in terms of the current interp. The file InterEither therefore define two such, where the hesitation comes from whether the handlers themselves should live in the either monad.

This path will likely lead to the duplication of all the code related to interpreters. Alternatively, we could try defining a type class of "Interpretable" monads in order to factor things out.

If anyone sees a simpler way to tackle this issue, suggestions are welcome :)

[gmalecha]

I didn't follow your explanation above as to why changing the semantics of basic blocks to itree Call (label + val) doesn't work. Naively, this would result in something akin to:

denote_block : block -> itree Call (label + val)
denote_function : function -> itree Call val
denote_program : closed_program -> itree Call val

denote_function uses loop to tie a knot, and denote_program uses something like mrec (now defined using loop?).