Commit e71c3257 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'move-global-func' into 'master'

Move global functor to base_logic

Sorry to bring this up again, I just think it's important to get this as right as we can, right now. ;)

This moves the global functor and dynamic composeable ownership to `base_logic`. The reasoning behind this is that if someone builds another program logic in our base logic, they will likely want to re-use this, so it makes more sense to have it in base_logic than in program_logic.

The rule for stuff to be in program_logic is: It depends on the Iris' notion of a language, or on world satisfaction (i.e., on our specific way to do invariants). Thus, `saved_prop` also moves to `base_logic` and becomes reusable by other program logics.
(If we want, we can talk about changing this to just "anything that depends on our notion of a language". Is it conceivable that our world satisfaction is reusable?)

When we talked about this previously, Robbert raised concerns about the name `iProp`. However, considering that we also have `iTactics` and use `I` for the `uPred_scope`, I feel like the letter "i" has already leaked way beyond `program_logic`, so this PR doesn't actually change anything. If you want, interpret `iProp` as "internal propositions", that even makes sense. ;)

Cc @robbertkrebbers @jjourdan

See merge request !18
parents 8c2608ed acdea9ec
Pipeline #2917 passed with stage
in 9 minutes and 26 seconds
...@@ -35,19 +35,23 @@ running: ...@@ -35,19 +35,23 @@ running:
* The folder [base_logic](base_logic) defines the Iris base logic and the * The folder [base_logic](base_logic) defines the Iris base logic and the
primitive connectives. It also contains derived constructions that are primitive connectives. It also contains derived constructions that are
entirely independent of the choice of resources. entirely independent of the choice of resources.
* The subfolder [lib](base_logic/lib) contains some generally useful
derived constructions. Most importantly, it defines composeable
dynamic resources and ownership of them; the other constructions depend
on this setup.
* The folder [program_logic](program_logic) specializes the base logic to build * The folder [program_logic](program_logic) specializes the base logic to build
Iris, the program logic. Most crucially, this includes world satisfaction Iris, the program logic. This includes weakest preconditions that are
and weakest preconditions. Furthermore, some language-independent derived defined for any language satisfying some generic axioms, and some derived
constructions (e.g., STSs) are defined in this folder. constructions that work for any such language.
* The folder [heap_lang](heap_lang) defines the ML-like concurrent heap language
* The subfolder [lib](heap_lang/lib) contains a few derived constructions
within this language, e.g., parallel composition.
Most notable here s [lib/barrier](heap_lang/lib/barrier), the implementation
and proof of a barrier as described in <http://doi.acm.org/10.1145/2818638>.
* The folder [proofmode](proofmode) contains the Iris proof mode, which extends * The folder [proofmode](proofmode) contains the Iris proof mode, which extends
Coq with contexts for persistent and spatial Iris assertions. It also contains Coq with contexts for persistent and spatial Iris assertions. It also contains
tactics for interactive proofs in Iris. Documentation can be found in tactics for interactive proofs in Iris. Documentation can be found in
[ProofMode.md](ProofMode.md). [ProofMode.md](ProofMode.md).
* The folder [heap_lang](heap_lang) defines the ML-like concurrent heap language
* The subfolder [lib](heap_lang/lib) contains a few derived constructions
within this language, e.g., parallel composition.
Most notable here is [lib/barrier](heap_lang/lib/barrier), the implementation
and proof of a barrier as described in <http://doi.acm.org/10.1145/2818638>.
* The folder [tests](tests) contains modules we use to test our infrastructure. * The folder [tests](tests) contains modules we use to test our infrastructure.
Users of the Iris Coq library should *not* depend on these modules; they may Users of the Iris Coq library should *not* depend on these modules; they may
change or disappear without any notice. change or disappear without any notice.
......
...@@ -67,7 +67,9 @@ base_logic/big_op.v ...@@ -67,7 +67,9 @@ base_logic/big_op.v
base_logic/hlist.v base_logic/hlist.v
base_logic/soundness.v base_logic/soundness.v
base_logic/double_negation.v base_logic/double_negation.v
program_logic/iprop.v base_logic/lib/iprop.v
base_logic/lib/own.v
base_logic/lib/saved_prop.v
program_logic/adequacy.v program_logic/adequacy.v
program_logic/lifting.v program_logic/lifting.v
program_logic/invariants.v program_logic/invariants.v
...@@ -80,8 +82,6 @@ program_logic/language.v ...@@ -80,8 +82,6 @@ program_logic/language.v
program_logic/ectx_language.v program_logic/ectx_language.v
program_logic/ectxi_language.v program_logic/ectxi_language.v
program_logic/ectx_lifting.v program_logic/ectx_lifting.v
program_logic/own.v
program_logic/saved_prop.v
program_logic/auth.v program_logic/auth.v
program_logic/sts.v program_logic/sts.v
program_logic/namespaces.v program_logic/namespaces.v
......
From iris.program_logic Require Export iprop.
From iris.algebra Require Import iprod gmap. From iris.algebra Require Import iprod gmap.
From iris.base_logic Require Import big_op. From iris.base_logic Require Import big_op.
From iris.base_logic Require Export iprop.
From iris.proofmode Require Import classes. From iris.proofmode Require Import classes.
Import uPred. Import uPred.
......
From iris.program_logic Require Export own. From iris.base_logic Require Export own.
From iris.algebra Require Import agree. From iris.algebra Require Import agree.
From iris.prelude Require Import gmap. From iris.prelude Require Import gmap.
Import uPred. Import uPred.
......
...@@ -2,8 +2,8 @@ From iris.program_logic Require Export weakestpre. ...@@ -2,8 +2,8 @@ From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.heap_lang.lib.barrier Require Export barrier. From iris.heap_lang.lib.barrier Require Export barrier.
From iris.prelude Require Import functions. From iris.prelude Require Import functions.
From iris.base_logic Require Import big_op. From iris.base_logic Require Import big_op lib.saved_prop.
From iris.program_logic Require Import saved_prop sts. From iris.program_logic Require Import sts.
From iris.heap_lang Require Import proofmode. From iris.heap_lang Require Import proofmode.
From iris.heap_lang.lib.barrier Require Import protocol. From iris.heap_lang.lib.barrier Require Import protocol.
......
From iris.algebra Require Export sts. From iris.algebra Require Export sts.
From iris.program_logic Require Import own. From iris.base_logic Require Import lib.own.
From iris.prelude Require Export gmap. From iris.prelude Require Export gmap.
(** The STS describing the main barrier protocol. Every state has an index-set (** The STS describing the main barrier protocol. Every state has an index-set
......
From iris.program_logic Require Export own language. From iris.base_logic Require Export lib.own.
From iris.program_logic Require Export language.
From iris.prelude Require Export coPset. From iris.prelude Require Export coPset.
From iris.algebra Require Import gmap auth agree gset coPset. From iris.algebra Require Import gmap auth agree gset coPset.
...@@ -27,4 +28,4 @@ Instance subG_irisΣ {Σ Λ} : subG (irisΣ Λ) Σ → irisPreG Λ Σ. ...@@ -27,4 +28,4 @@ Instance subG_irisΣ {Σ Λ} : subG (irisΣ Λ) Σ → irisPreG Λ Σ.
Proof. Proof.
intros [?%subG_inG [?%subG_inG intros [?%subG_inG [?%subG_inG
[?%subG_inG ?%subG_inG]%subG_inv]%subG_inv]%subG_inv; by constructor. [?%subG_inG ?%subG_inG]%subG_inv]%subG_inv]%subG_inv; by constructor.
Qed. Qed.
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment