Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
I
Iris
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 116
    • Issues 116
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 22
    • Merge Requests 22
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Iris
  • Iris
  • Merge Requests
  • !257

Merged
Opened May 30, 2019 by Robbert@robbertkrebbersMaintainer

Turn the arguments of functors into COFEs + write some docs

  • Overview 37
  • Commits 4
  • 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
Assignee
Assign to
Reviewer
Request review from
None
Milestone
None
Assign milestone
Time tracking
Reference: iris/iris!257
Source branch: robbert/functor_cofe

Revert this merge request

This will create a new commit in order to revert the existing changes.

Switch branch
Cancel
A new branch will be created in your fork and a new merge request will be started.

Cherry-pick this merge request

Switch branch
Cancel
A new branch will be created in your fork and a new merge request will be started.