From b9413b6f490c98f56807b9734e2ef3891042b9e1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 28 Oct 2016 11:07:09 +0200
Subject: [PATCH] Move program_logic stuff that does not depend on the language
 to base_logic/lib.

---
 _CoqProject                                   | 22 +++++++++----------
 {program_logic => base_logic/lib}/auth.v      |  2 +-
 {program_logic => base_logic/lib}/boxes.v     |  2 +-
 .../lib}/cancelable_invariants.v              |  2 +-
 .../lib}/counter_examples.v                   |  0
 .../lib}/fancy_updates.v                      |  2 +-
 .../lib}/invariants.v                         |  5 ++---
 .../lib}/namespaces.v                         |  0
 {program_logic => base_logic/lib}/sts.v       |  2 +-
 .../lib}/thread_local.v                       |  2 +-
 .../lib}/viewshifts.v                         |  2 +-
 {program_logic => base_logic/lib}/wsat.v      |  0
 heap_lang/adequacy.v                          |  2 +-
 heap_lang/heap.v                              |  4 ++--
 heap_lang/lib/barrier/proof.v                 |  3 +--
 heap_lang/lifting.v                           |  2 +-
 program_logic/adequacy.v                      |  2 +-
 program_logic/ectx_lifting.v                  |  1 -
 program_logic/hoare.v                         |  3 ++-
 program_logic/lifting.v                       |  1 -
 program_logic/weakestpre.v                    |  3 ++-
 tests/heap_lang.v                             |  1 -
 tests/proofmode.v                             |  2 +-
 23 files changed, 31 insertions(+), 34 deletions(-)
 rename {program_logic => base_logic/lib}/auth.v (99%)
 rename {program_logic => base_logic/lib}/boxes.v (99%)
 rename {program_logic => base_logic/lib}/cancelable_invariants.v (97%)
 rename {program_logic => base_logic/lib}/counter_examples.v (100%)
 rename {program_logic => base_logic/lib}/fancy_updates.v (99%)
 rename {program_logic => base_logic/lib}/invariants.v (95%)
 rename {program_logic => base_logic/lib}/namespaces.v (100%)
 rename {program_logic => base_logic/lib}/sts.v (99%)
 rename {program_logic => base_logic/lib}/thread_local.v (98%)
 rename {program_logic => base_logic/lib}/viewshifts.v (98%)
 rename {program_logic => base_logic/lib}/wsat.v (100%)

diff --git a/_CoqProject b/_CoqProject
index 3947fdf58..4ff403e8e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -70,25 +70,25 @@ base_logic/double_negation.v
 base_logic/lib/iprop.v
 base_logic/lib/own.v
 base_logic/lib/saved_prop.v
+base_logic/lib/namespaces.v
+base_logic/lib/wsat.v
+base_logic/lib/invariants.v
+base_logic/lib/fancy_updates.v
+base_logic/lib/viewshifts.v
+base_logic/lib/auth.v
+base_logic/lib/sts.v
+base_logic/lib/boxes.v
+base_logic/lib/thread_local.v
+base_logic/lib/cancelable_invariants.v
+base_logic/lib/counter_examples.v
 program_logic/adequacy.v
 program_logic/lifting.v
-program_logic/invariants.v
-program_logic/wsat.v
 program_logic/weakestpre.v
-program_logic/fancy_updates.v
 program_logic/hoare.v
-program_logic/viewshifts.v
 program_logic/language.v
 program_logic/ectx_language.v
 program_logic/ectxi_language.v
 program_logic/ectx_lifting.v
-program_logic/auth.v
-program_logic/sts.v
-program_logic/namespaces.v
-program_logic/boxes.v
-program_logic/counter_examples.v
-program_logic/thread_local.v
-program_logic/cancelable_invariants.v
 heap_lang/lang.v
 heap_lang/tactics.v
 heap_lang/wp_tactics.v
diff --git a/program_logic/auth.v b/base_logic/lib/auth.v
similarity index 99%
rename from program_logic/auth.v
rename to base_logic/lib/auth.v
index 8696055ae..fd0ab02fa 100644
--- a/program_logic/auth.v
+++ b/base_logic/lib/auth.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export invariants.
+From iris.base_logic.lib Require Export invariants.
 From iris.algebra Require Export auth.
 From iris.algebra Require Import gmap.
 From iris.base_logic Require Import big_op.
diff --git a/program_logic/boxes.v b/base_logic/lib/boxes.v
similarity index 99%
rename from program_logic/boxes.v
rename to base_logic/lib/boxes.v
index e7524868f..a55d1c8a9 100644
--- a/program_logic/boxes.v
+++ b/base_logic/lib/boxes.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export invariants.
+From iris.base_logic.lib Require Export invariants.
 From iris.algebra Require Import auth gmap agree.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
diff --git a/program_logic/cancelable_invariants.v b/base_logic/lib/cancelable_invariants.v
similarity index 97%
rename from program_logic/cancelable_invariants.v
rename to base_logic/lib/cancelable_invariants.v
index 59b68d314..1cbdefa77 100644
--- a/program_logic/cancelable_invariants.v
+++ b/base_logic/lib/cancelable_invariants.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export invariants.
+From iris.base_logic.lib Require Export invariants.
 From iris.algebra Require Export frac.
 From iris.proofmode Require Import tactics.
 Import uPred.
diff --git a/program_logic/counter_examples.v b/base_logic/lib/counter_examples.v
similarity index 100%
rename from program_logic/counter_examples.v
rename to base_logic/lib/counter_examples.v
diff --git a/program_logic/fancy_updates.v b/base_logic/lib/fancy_updates.v
similarity index 99%
rename from program_logic/fancy_updates.v
rename to base_logic/lib/fancy_updates.v
index b3423cd74..18af313b1 100644
--- a/program_logic/fancy_updates.v
+++ b/base_logic/lib/fancy_updates.v
@@ -1,6 +1,6 @@
 From iris.base_logic.lib Require Export own.
 From iris.prelude Require Export coPset.
-From iris.program_logic Require Import wsat.
+From iris.base_logic.lib Require Import wsat.
 From iris.algebra Require Import gmap.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics classes.
diff --git a/program_logic/invariants.v b/base_logic/lib/invariants.v
similarity index 95%
rename from program_logic/invariants.v
rename to base_logic/lib/invariants.v
index e43a561f9..727a8b659 100644
--- a/program_logic/invariants.v
+++ b/base_logic/lib/invariants.v
@@ -1,6 +1,5 @@
-From iris.program_logic Require Export fancy_updates.
-From iris.program_logic Require Export namespaces.
-From iris.program_logic Require Import wsat.
+From iris.base_logic.lib Require Export fancy_updates namespaces.
+From iris.base_logic.lib Require Import wsat.
 From iris.algebra Require Import gmap.
 From iris.proofmode Require Import tactics coq_tactics intro_patterns.
 Import uPred.
diff --git a/program_logic/namespaces.v b/base_logic/lib/namespaces.v
similarity index 100%
rename from program_logic/namespaces.v
rename to base_logic/lib/namespaces.v
diff --git a/program_logic/sts.v b/base_logic/lib/sts.v
similarity index 99%
rename from program_logic/sts.v
rename to base_logic/lib/sts.v
index b605e567c..47c79df7e 100644
--- a/program_logic/sts.v
+++ b/base_logic/lib/sts.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export invariants.
+From iris.base_logic.lib Require Export invariants.
 From iris.algebra Require Export sts.
 From iris.proofmode Require Import tactics.
 Import uPred.
diff --git a/program_logic/thread_local.v b/base_logic/lib/thread_local.v
similarity index 98%
rename from program_logic/thread_local.v
rename to base_logic/lib/thread_local.v
index 6b4adae59..be3dca174 100644
--- a/program_logic/thread_local.v
+++ b/base_logic/lib/thread_local.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export invariants.
+From iris.base_logic.lib Require Export invariants.
 From iris.algebra Require Export gmap gset coPset.
 From iris.proofmode Require Import tactics.
 Import uPred.
diff --git a/program_logic/viewshifts.v b/base_logic/lib/viewshifts.v
similarity index 98%
rename from program_logic/viewshifts.v
rename to base_logic/lib/viewshifts.v
index d7eef16ad..be4a00ef4 100644
--- a/program_logic/viewshifts.v
+++ b/base_logic/lib/viewshifts.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export invariants.
+From iris.base_logic.lib Require Export invariants.
 From iris.proofmode Require Import tactics.
 
 Definition vs `{invG Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
diff --git a/program_logic/wsat.v b/base_logic/lib/wsat.v
similarity index 100%
rename from program_logic/wsat.v
rename to base_logic/lib/wsat.v
diff --git a/heap_lang/adequacy.v b/heap_lang/adequacy.v
index 6addeac52..01aecda22 100644
--- a/heap_lang/adequacy.v
+++ b/heap_lang/adequacy.v
@@ -1,7 +1,7 @@
 From iris.program_logic Require Export weakestpre adequacy.
 From iris.heap_lang Require Export heap.
 From iris.algebra Require Import auth.
-From iris.program_logic Require Import wsat auth.
+From iris.base_logic.lib Require Import wsat auth.
 From iris.heap_lang Require Import proofmode notation.
 From iris.proofmode Require Import tactics.
 
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 03576859a..388bcf99c 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -1,7 +1,7 @@
 From iris.heap_lang Require Export lifting.
 From iris.algebra Require Import auth gmap frac dec_agree.
-From iris.program_logic Require Export invariants.
-From iris.program_logic Require Import wsat auth.
+From iris.base_logic.lib Require Export invariants.
+From iris.base_logic.lib Require Import wsat auth.
 From iris.proofmode Require Import tactics.
 Import uPred.
 (* TODO: The entire construction could be generalized to arbitrary languages that have
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 59057fc9a..9436c07e1 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -2,8 +2,7 @@ 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 lib.saved_prop.
-From iris.program_logic Require Import sts.
+From iris.base_logic Require Import big_op lib.saved_prop lib.sts.
 From iris.heap_lang Require Import proofmode.
 From iris.heap_lang.lib.barrier Require Import protocol.
 
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index a2d7729d8..2d2e5be87 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Export weakestpre.
-From iris.program_logic Require Import wsat ectx_lifting. (* for ownP *)
+From iris.program_logic Require Import ectx_lifting.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics.
 From iris.proofmode Require Import tactics.
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index c922ee24f..4fa371934 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -1,7 +1,7 @@
 From iris.program_logic Require Export weakestpre.
 From iris.algebra Require Import gmap auth agree gset coPset.
 From iris.base_logic Require Import big_op soundness.
-From iris.program_logic Require Import wsat.
+From iris.base_logic.lib Require Import wsat.
 From iris.proofmode Require Import tactics.
 Import uPred.
 
diff --git a/program_logic/ectx_lifting.v b/program_logic/ectx_lifting.v
index 9ec7f6878..99df308b6 100644
--- a/program_logic/ectx_lifting.v
+++ b/program_logic/ectx_lifting.v
@@ -1,6 +1,5 @@
 (** Some derived lemmas for ectx-based languages *)
 From iris.program_logic Require Export ectx_language weakestpre lifting.
-From iris.program_logic Require Import wsat.
 From iris.proofmode Require Import tactics.
 
 Section wp.
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 302504187..4ce26dd3a 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -1,4 +1,5 @@
-From iris.program_logic Require Export weakestpre viewshifts.
+From iris.program_logic Require Export weakestpre.
+From iris.base_logic.lib Require Export viewshifts.
 From iris.proofmode Require Import tactics.
 
 Definition ht `{irisG Λ Σ} (E : coPset) (P : iProp Σ)
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index adad69e31..8b05a8290 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -1,5 +1,4 @@
 From iris.program_logic Require Export weakestpre.
-From iris.program_logic Require Import wsat.
 From iris.base_logic Require Export big_op.
 From iris.proofmode Require Import tactics.
 
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 7ff2089ac..6b98efa4d 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -1,4 +1,5 @@
-From iris.program_logic Require Export fancy_updates language.
+From iris.base_logic.lib Require Export fancy_updates.
+From iris.program_logic Require Export language.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics classes.
 From iris.algebra Require Import auth.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index d18943ad0..5f05dd6f3 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -2,7 +2,6 @@
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import adequacy.
-From iris.program_logic Require Import wsat.
 From iris.heap_lang Require Import proofmode notation.
 
 Section LiftingTests.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 21811f906..fa970acf3 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From iris.program_logic Require Import invariants.
+From iris.base_logic.lib Require Import invariants.
 
 Lemma demo_0 {M : ucmraT} (P Q : uPred M) :
   □ (P ∨ Q) ⊢ (∀ x, x = 0 ∨ x = 1) → (Q ∨ P).
-- 
GitLab