Resolution of prophecy variables can be attached to atomic expressions
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
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
v of the top level
Resolve will be automatically evaluated through contextual closure.