GitLab

This MR alters the mechanism for resolving prophecy variables in heaplang. The prophecy variable resolution operation can now be attached to any atomic expression e thanks to the Resolve e p v expression, where p is an expression evaluating to a prophecy variable, and v is the value to resolve the prophecy to. Furthermore, the observation made during the corresponding evaluation step contains not only the value for the resolved operation, but also the value obtained after evaluating e. This means that when evaluating something like Resolve (CAS #l #v1 #v2) #p #v, the list of observations is extended with a pair (w, v), where w is the result of the CAS.

Note that there are some limitations: Resolve (CAS e1 e2 e3) p v will not evaluate in the case where either of e1, e2 or e3 is not a value (and similarly for other atomic operations). However, this can be circumvented using let-normalization for the arguments of the wrapped (atomic) expression. There is a similar limitation when nesting Resolve constructors, and only the p and v of the top level Resolve will be automatically evaluated through contextual closure.

Any feedback @jung and @amintimany?