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 169
    • Issues 169
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 24
    • Merge requests 24
  • 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
  • !257

Turn the arguments of functors into COFEs + write some docs

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Robbert Krebbers requested to merge robbert/functor_cofe into master May 30, 2019
  • Overview 37
  • Commits 4
  • Pipelines 0
  • Changes 17

His MR changes cFunctor, rFunctor and urFunctor to be functors from COFEs to OFEs, cameras, respectively unital cameras. Before they were functors that took mere OFEs. This is fully backwards compatibly, since in the end of the day, we always instantiate the functor with iPreProp which is a COFE.

Motivation

This change is useful if one wants to construct recursive ghost state, e.g. in work with @jihgfee we basically want to have ghost state that contains streams of iProp, to model session types in a semantic way. For that, we instantiate Iris with something akin to the functor:

F(X) := μ Y. ▶ X ∗ ▶ Y

(Where X will be the recursive occurrence for iProp).

In order to constructor the inner fixpoint, μ Y. ▶ X ∗ ▶ Y, we use the COFE solver. However, for that to work, we need that X to be a COFE, which we do not get with the current functor infrastructure. This MR fixes that.

Documentation

Apart from this change, I tried to write some documentation, explaining the (updated) functor infrastructure.

Edited May 30, 2019 by Robbert Krebbers
Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: robbert/functor_cofe