Commit acdea9ec authored by Ralf Jung's avatar Ralf Jung

Move global functor to base_logic

parent 634fdbb6
...@@ -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