From acdea9ecaa4ec52f8f93d1a4789dfc48f677dd35 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 27 Oct 2016 13:46:23 +0200
Subject: [PATCH] Move global functor to base_logic
---
README.md | 20 +++++++++++--------
_CoqProject | 6 +++---
{program_logic => base_logic/lib}/iprop.v | 0
{program_logic => base_logic/lib}/own.v | 2 +-
.../lib}/saved_prop.v | 2 +-
heap_lang/lib/barrier/proof.v | 4 ++--
heap_lang/lib/barrier/protocol.v | 2 +-
program_logic/iris.v | 5 +++--
8 files changed, 23 insertions(+), 18 deletions(-)
rename {program_logic => base_logic/lib}/iprop.v (100%)
rename {program_logic => base_logic/lib}/own.v (99%)
rename {program_logic => base_logic/lib}/saved_prop.v (97%)
diff --git a/README.md b/README.md
index ad3253864..c09bcdbdc 100644
--- a/README.md
+++ b/README.md
@@ -35,19 +35,23 @@ running:
* The folder [base_logic](base_logic) defines the Iris base logic and the
primitive connectives. It also contains derived constructions that are
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
- Iris, the program logic. Most crucially, this includes world satisfaction
- and weakest preconditions. Furthermore, some language-independent derived
- constructions (e.g., STSs) are defined in this folder.
-* 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>.
+ Iris, the program logic. This includes weakest preconditions that are
+ defined for any language satisfying some generic axioms, and some derived
+ constructions that work for any such language.
* The folder [proofmode](proofmode) contains the Iris proof mode, which extends
Coq with contexts for persistent and spatial Iris assertions. It also contains
tactics for interactive proofs in Iris. Documentation can be found in
[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.
Users of the Iris Coq library should *not* depend on these modules; they may
change or disappear without any notice.
diff --git a/_CoqProject b/_CoqProject
index 8d3655da7..863188830 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -67,7 +67,9 @@ base_logic/big_op.v
base_logic/hlist.v
base_logic/soundness.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/lifting.v
program_logic/invariants.v
@@ -80,8 +82,6 @@ program_logic/language.v
program_logic/ectx_language.v
program_logic/ectxi_language.v
program_logic/ectx_lifting.v
-program_logic/own.v
-program_logic/saved_prop.v
program_logic/auth.v
program_logic/sts.v
program_logic/namespaces.v
diff --git a/program_logic/iprop.v b/base_logic/lib/iprop.v
similarity index 100%
rename from program_logic/iprop.v
rename to base_logic/lib/iprop.v
diff --git a/program_logic/own.v b/base_logic/lib/own.v
similarity index 99%
rename from program_logic/own.v
rename to base_logic/lib/own.v
index f23b3eb14..1c2316258 100644
--- a/program_logic/own.v
+++ b/base_logic/lib/own.v
@@ -1,6 +1,6 @@
-From iris.program_logic Require Export iprop.
From iris.algebra Require Import iprod gmap.
From iris.base_logic Require Import big_op.
+From iris.base_logic Require Export iprop.
From iris.proofmode Require Import classes.
Import uPred.
diff --git a/program_logic/saved_prop.v b/base_logic/lib/saved_prop.v
similarity index 97%
rename from program_logic/saved_prop.v
rename to base_logic/lib/saved_prop.v
index 22cfc0014..0cac08c87 100644
--- a/program_logic/saved_prop.v
+++ b/base_logic/lib/saved_prop.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export own.
+From iris.base_logic Require Export own.
From iris.algebra Require Import agree.
From iris.prelude Require Import gmap.
Import uPred.
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 84f9abdbe..59057fc9a 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -2,8 +2,8 @@ From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang.lib.barrier Require Export barrier.
From iris.prelude Require Import functions.
-From iris.base_logic Require Import big_op.
-From iris.program_logic Require Import saved_prop sts.
+From iris.base_logic Require Import big_op lib.saved_prop.
+From iris.program_logic Require Import sts.
From iris.heap_lang Require Import proofmode.
From iris.heap_lang.lib.barrier Require Import protocol.
diff --git a/heap_lang/lib/barrier/protocol.v b/heap_lang/lib/barrier/protocol.v
index f59a64247..e347613a1 100644
--- a/heap_lang/lib/barrier/protocol.v
+++ b/heap_lang/lib/barrier/protocol.v
@@ -1,5 +1,5 @@
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.
(** The STS describing the main barrier protocol. Every state has an index-set
diff --git a/program_logic/iris.v b/program_logic/iris.v
index f0c91c294..7abeea65b 100644
--- a/program_logic/iris.v
+++ b/program_logic/iris.v
@@ -1,4 +1,5 @@
-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.algebra Require Import gmap auth agree gset coPset.
@@ -27,4 +28,4 @@ Instance subG_irisΣ {Σ Λ} : subG (irisΣ Λ) Σ → irisPreG Λ Σ.
Proof.
intros [?%subG_inG [?%subG_inG
[?%subG_inG ?%subG_inG]%subG_inv]%subG_inv]%subG_inv; by constructor.
-Qed.
\ No newline at end of file
+Qed.
--
GitLab