Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 170
    • Issues 170
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 23
    • Merge requests 23
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Merge requests
  • !244

Resolution of prophecy variables can be attached to atomic expressions

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Rodolphe Lepigre requested to merge lepigre/iris:atomic_resolve into master May 14, 2019
  • Overview 132
  • Commits 28
  • Pipelines 0
  • Changes 8

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?

Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: atomic_resolve