From 4a272286d67014dfbff5ad9acaa6a703f700df20 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 4 Feb 2016 10:41:56 +0100
Subject: [PATCH] Rename modures -> algebra and iris -> program_logic.

---
 _CoqProject                             | 58 ++++++++++++-------------
 {modures => algebra}/agree.v            |  2 +-
 {modures => algebra}/auth.v             |  2 +-
 {modures => algebra}/base.v             |  0
 {modures => algebra}/cmra.v             |  2 +-
 {modures => algebra}/cmra_big_op.v      |  2 +-
 {modures => algebra}/cmra_tactics.v     |  4 +-
 {modures => algebra}/cofe.v             |  2 +-
 {modures => algebra}/cofe_solver.v      |  2 +-
 {modures => algebra}/dra.v              |  2 +-
 {modures => algebra}/excl.v             |  2 +-
 {modures => algebra}/fin_maps.v         |  2 +-
 {modures => algebra}/option.v           |  2 +-
 {modures => algebra}/sts.v              |  4 +-
 heap_lang/heap_lang.v                   |  2 +-
 heap_lang/lifting.v                     |  4 +-
 heap_lang/tests.v                       |  2 +-
 modures/logic.v => logic/upred.v        |  2 +-
 {iris => program_logic}/adequacy.v      |  4 +-
 {iris => program_logic}/functor.v       |  2 +-
 {iris => program_logic}/hoare.v         |  2 +-
 {iris => program_logic}/hoare_lifting.v |  2 +-
 {iris => program_logic}/language.v      |  2 +-
 {iris => program_logic}/lifting.v       |  4 +-
 {iris => program_logic}/model.v         |  4 +-
 {iris => program_logic}/namespace.v     |  2 +-
 {iris => program_logic}/ownership.v     |  2 +-
 {iris => program_logic}/pviewshifts.v   |  4 +-
 {iris => program_logic}/resources.v     |  4 +-
 {iris => program_logic}/tests.v         |  2 +-
 {iris => program_logic}/viewshifts.v    |  2 +-
 {iris => program_logic}/weakestpre.v    |  4 +-
 {iris => program_logic}/wsat.v          |  4 +-
 33 files changed, 70 insertions(+), 70 deletions(-)
 rename {modures => algebra}/agree.v (99%)
 rename {modures => algebra}/auth.v (99%)
 rename {modures => algebra}/base.v (100%)
 rename {modures => algebra}/cmra.v (99%)
 rename {modures => algebra}/cmra_big_op.v (99%)
 rename {modures => algebra}/cmra_tactics.v (97%)
 rename {modures => algebra}/cofe.v (99%)
 rename {modures => algebra}/cofe_solver.v (99%)
 rename {modures => algebra}/dra.v (99%)
 rename {modures => algebra}/excl.v (99%)
 rename {modures => algebra}/fin_maps.v (99%)
 rename {modures => algebra}/option.v (99%)
 rename {modures => algebra}/sts.v (99%)
 rename modures/logic.v => logic/upred.v (99%)
 rename {iris => program_logic}/adequacy.v (98%)
 rename {iris => program_logic}/functor.v (97%)
 rename {iris => program_logic}/hoare.v (98%)
 rename {iris => program_logic}/hoare_lifting.v (99%)
 rename {iris => program_logic}/language.v (98%)
 rename {iris => program_logic}/lifting.v (98%)
 rename {iris => program_logic}/model.v (96%)
 rename {iris => program_logic}/namespace.v (96%)
 rename {iris => program_logic}/ownership.v (98%)
 rename {iris => program_logic}/pviewshifts.v (98%)
 rename {iris => program_logic}/resources.v (98%)
 rename {iris => program_logic}/tests.v (87%)
 rename {iris => program_logic}/viewshifts.v (98%)
 rename {iris => program_logic}/weakestpre.v (99%)
 rename {iris => program_logic}/wsat.v (98%)

diff --git a/_CoqProject b/_CoqProject
index 2ccb23daf..1757f9d37 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -34,35 +34,35 @@ prelude/sets.v
 prelude/decidable.v
 prelude/list.v
 prelude/error.v
-modures/option.v
-modures/cmra.v
-modures/cmra_big_op.v
-modures/cmra_tactics.v
-modures/sts.v
-modures/auth.v
-modures/fin_maps.v
-modures/logic.v
-modures/cofe.v
-modures/base.v
-modures/dra.v
-modures/cofe_solver.v
-modures/agree.v
-modures/excl.v
-iris/model.v
-iris/adequacy.v
-iris/hoare_lifting.v
-iris/lifting.v
-iris/namespace.v
-iris/viewshifts.v
-iris/wsat.v
-iris/ownership.v
-iris/weakestpre.v
-iris/pviewshifts.v
-iris/resources.v
-iris/hoare.v
-iris/language.v
-iris/functor.v
-iris/tests.v
+algebra/option.v
+algebra/cmra.v
+algebra/cmra_big_op.v
+algebra/cmra_tactics.v
+algebra/sts.v
+algebra/auth.v
+algebra/fin_maps.v
+logic/upred.v
+algebra/cofe.v
+algebra/base.v
+algebra/dra.v
+algebra/cofe_solver.v
+algebra/agree.v
+algebra/excl.v
+program_logic/model.v
+program_logic/adequacy.v
+program_logic/hoare_lifting.v
+program_logic/lifting.v
+program_logic/namespace.v
+program_logic/viewshifts.v
+program_logic/wsat.v
+program_logic/ownership.v
+program_logic/weakestpre.v
+program_logic/pviewshifts.v
+program_logic/resources.v
+program_logic/hoare.v
+program_logic/language.v
+program_logic/functor.v
+program_logic/tests.v
 heap_lang/heap_lang.v
 heap_lang/heap_lang_tactics.v
 heap_lang/lifting.v
diff --git a/modures/agree.v b/algebra/agree.v
similarity index 99%
rename from modures/agree.v
rename to algebra/agree.v
index bceadd518..65464cdd1 100644
--- a/modures/agree.v
+++ b/algebra/agree.v
@@ -1,4 +1,4 @@
-Require Export modures.cmra.
+Require Export algebra.cmra.
 Local Hint Extern 10 (_ ≤ _) => omega.
 
 Record agree (A : Type) : Type := Agree {
diff --git a/modures/auth.v b/algebra/auth.v
similarity index 99%
rename from modures/auth.v
rename to algebra/auth.v
index c99b37013..32e76cd48 100644
--- a/modures/auth.v
+++ b/algebra/auth.v
@@ -1,4 +1,4 @@
-Require Export modures.excl.
+Require Export algebra.excl.
 Local Arguments validN _ _ _ !_ /.
 
 Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
diff --git a/modures/base.v b/algebra/base.v
similarity index 100%
rename from modures/base.v
rename to algebra/base.v
diff --git a/modures/cmra.v b/algebra/cmra.v
similarity index 99%
rename from modures/cmra.v
rename to algebra/cmra.v
index 326f8b490..8e1bbdff9 100644
--- a/modures/cmra.v
+++ b/algebra/cmra.v
@@ -1,4 +1,4 @@
-Require Export modures.cofe.
+Require Export algebra.cofe.
 
 Class Unit (A : Type) := unit : A → A.
 Instance: Params (@unit) 2.
diff --git a/modures/cmra_big_op.v b/algebra/cmra_big_op.v
similarity index 99%
rename from modures/cmra_big_op.v
rename to algebra/cmra_big_op.v
index c96118a09..a11ce17f6 100644
--- a/modures/cmra_big_op.v
+++ b/algebra/cmra_big_op.v
@@ -1,4 +1,4 @@
-Require Export modures.cmra.
+Require Export algebra.cmra.
 Require Import prelude.fin_maps.
 
 Fixpoint big_op {A : cmraT} `{Empty A} (xs : list A) : A :=
diff --git a/modures/cmra_tactics.v b/algebra/cmra_tactics.v
similarity index 97%
rename from modures/cmra_tactics.v
rename to algebra/cmra_tactics.v
index c2cce946a..27b6efb85 100644
--- a/modures/cmra_tactics.v
+++ b/algebra/cmra_tactics.v
@@ -1,5 +1,5 @@
-Require Export modures.cmra.
-Require Import modures.cmra_big_op.
+Require Export algebra.cmra.
+Require Import algebra.cmra_big_op.
 
 (** * Simple solver for validity and inclusion by reflection *)
 Module ra_reflection. Section ra_reflection.
diff --git a/modures/cofe.v b/algebra/cofe.v
similarity index 99%
rename from modures/cofe.v
rename to algebra/cofe.v
index bab5b05d0..2b48fcc6a 100644
--- a/modures/cofe.v
+++ b/algebra/cofe.v
@@ -1,4 +1,4 @@
-Require Export modures.base.
+Require Export algebra.base.
 
 (** Unbundeled version *)
 Class Dist A := dist : nat → relation A.
diff --git a/modures/cofe_solver.v b/algebra/cofe_solver.v
similarity index 99%
rename from modures/cofe_solver.v
rename to algebra/cofe_solver.v
index 977a6fdc5..b0c1543a4 100644
--- a/modures/cofe_solver.v
+++ b/algebra/cofe_solver.v
@@ -1,4 +1,4 @@
-Require Export modures.cofe.
+Require Export algebra.cofe.
 
 Record solution (F : cofeT → cofeT → cofeT) := Solution {
   solution_car :> cofeT;
diff --git a/modures/dra.v b/algebra/dra.v
similarity index 99%
rename from modures/dra.v
rename to algebra/dra.v
index 933deff4a..0e61179da 100644
--- a/modures/dra.v
+++ b/algebra/dra.v
@@ -1,4 +1,4 @@
-Require Export modures.cmra.
+Require Export algebra.cmra.
 
 (** From disjoint pcm *)
 Record validity {A} (P : A → Prop) : Type := Validity {
diff --git a/modures/excl.v b/algebra/excl.v
similarity index 99%
rename from modures/excl.v
rename to algebra/excl.v
index a86ccd72e..a0be19baf 100644
--- a/modures/excl.v
+++ b/algebra/excl.v
@@ -1,4 +1,4 @@
-Require Export modures.cmra.
+Require Export algebra.cmra.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 
diff --git a/modures/fin_maps.v b/algebra/fin_maps.v
similarity index 99%
rename from modures/fin_maps.v
rename to algebra/fin_maps.v
index 58eb39cd1..d9062626f 100644
--- a/modures/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -1,4 +1,4 @@
-Require Export modures.cmra prelude.gmap modures.option.
+Require Export algebra.cmra prelude.gmap algebra.option.
 
 Section cofe.
 Context `{Countable K} {A : cofeT}.
diff --git a/modures/option.v b/algebra/option.v
similarity index 99%
rename from modures/option.v
rename to algebra/option.v
index a553fa1b0..071ecafb2 100644
--- a/modures/option.v
+++ b/algebra/option.v
@@ -1,4 +1,4 @@
-Require Export modures.cmra.
+Require Export algebra.cmra.
 
 (* COFE *)
 Section cofe.
diff --git a/modures/sts.v b/algebra/sts.v
similarity index 99%
rename from modures/sts.v
rename to algebra/sts.v
index 90ad94ba3..4e699e1d3 100644
--- a/modures/sts.v
+++ b/algebra/sts.v
@@ -1,5 +1,5 @@
-Require Export modures.cmra.
-Require Import prelude.sets modures.dra.
+Require Export algebra.cmra.
+Require Import prelude.sets algebra.dra.
 Local Arguments valid _ _ !_ /.
 Local Arguments op _ _ !_ !_ /.
 Local Arguments unit _ _ !_ /.
diff --git a/heap_lang/heap_lang.v b/heap_lang/heap_lang.v
index 5482c8e01..1511b05a5 100644
--- a/heap_lang/heap_lang.v
+++ b/heap_lang/heap_lang.v
@@ -1,5 +1,5 @@
 Require Export Autosubst.Autosubst.
-Require Export iris.language.
+Require Export program_logic.language.
 Require Import prelude.gmap.
 
 Module heap_lang.
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index e89728dac..62df239ee 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -1,5 +1,5 @@
-Require Import prelude.gmap iris.lifting.
-Require Export iris.weakestpre heap_lang.heap_lang_tactics.
+Require Import prelude.gmap program_logic.lifting.
+Require Export program_logic.weakestpre heap_lang.heap_lang_tactics.
 Import uPred.
 Import heap_lang.
 Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index d5297a534..4ca0d01e2 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -1,5 +1,5 @@
 (** This file is essentially a bunch of testcases. *)
-Require Import modures.logic.
+Require Import logic.upred.
 Require Import heap_lang.lifting heap_lang.sugar.
 Import heap_lang.
 Import uPred.
diff --git a/modures/logic.v b/logic/upred.v
similarity index 99%
rename from modures/logic.v
rename to logic/upred.v
index a50c0dbc3..01f467cb0 100644
--- a/modures/logic.v
+++ b/logic/upred.v
@@ -1,4 +1,4 @@
-Require Export modures.cmra.
+Require Export algebra.cmra.
 Local Hint Extern 1 (_ ≼ _) => etransitivity; [eassumption|].
 Local Hint Extern 1 (_ ≼ _) => etransitivity; [|eassumption].
 Local Hint Extern 10 (_ ≤ _) => omega.
diff --git a/iris/adequacy.v b/program_logic/adequacy.v
similarity index 98%
rename from iris/adequacy.v
rename to program_logic/adequacy.v
index 27d5ab13d..1efb3abcd 100644
--- a/iris/adequacy.v
+++ b/program_logic/adequacy.v
@@ -1,5 +1,5 @@
-Require Export iris.hoare.
-Require Import iris.wsat.
+Require Export program_logic.hoare.
+Require Import program_logic.wsat.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 100 (@eq coPset _ _) => eassumption || solve_elem_of.
 Local Hint Extern 10 (✓{_} _) =>
diff --git a/iris/functor.v b/program_logic/functor.v
similarity index 97%
rename from iris/functor.v
rename to program_logic/functor.v
index 49c7a0dfe..cecfd67b2 100644
--- a/iris/functor.v
+++ b/program_logic/functor.v
@@ -1,4 +1,4 @@
-Require Export modures.cmra.
+Require Export algebra.cmra.
 
 Structure iFunctor := IFunctor {
   ifunctor_car :> cofeT → cmraT;
diff --git a/iris/hoare.v b/program_logic/hoare.v
similarity index 98%
rename from iris/hoare.v
rename to program_logic/hoare.v
index 100998cc2..f34281bf7 100644
--- a/iris/hoare.v
+++ b/program_logic/hoare.v
@@ -1,4 +1,4 @@
-Require Export iris.weakestpre iris.viewshifts.
+Require Export program_logic.weakestpre program_logic.viewshifts.
 
 Definition ht {Λ Σ} (E : coPset) (P : iProp Λ Σ)
     (e : expr Λ) (Q : val Λ → iProp Λ Σ) : iProp Λ Σ :=
diff --git a/iris/hoare_lifting.v b/program_logic/hoare_lifting.v
similarity index 99%
rename from iris/hoare_lifting.v
rename to program_logic/hoare_lifting.v
index 172ce73bc..7ff9d1d7f 100644
--- a/iris/hoare_lifting.v
+++ b/program_logic/hoare_lifting.v
@@ -1,4 +1,4 @@
-Require Export iris.hoare iris.lifting.
+Require Export program_logic.hoare program_logic.lifting.
 
 Local Notation "{{ P } } ef ?@ E {{ Q } }" :=
   (default True%I ef (λ e, ht E P e Q))
diff --git a/iris/language.v b/program_logic/language.v
similarity index 98%
rename from iris/language.v
rename to program_logic/language.v
index 1a4bc01b2..783ac2a73 100644
--- a/iris/language.v
+++ b/program_logic/language.v
@@ -1,4 +1,4 @@
-Require Export modures.cofe.
+Require Export algebra.cofe.
 
 Structure language := Language {
   expr : Type;
diff --git a/iris/lifting.v b/program_logic/lifting.v
similarity index 98%
rename from iris/lifting.v
rename to program_logic/lifting.v
index 94093941b..c028b22ce 100644
--- a/iris/lifting.v
+++ b/program_logic/lifting.v
@@ -1,5 +1,5 @@
-Require Export iris.weakestpre.
-Require Import iris.wsat.
+Require Export program_logic.weakestpre.
+Require Import program_logic.wsat.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
 Local Hint Extern 10 (✓{_} _) =>
diff --git a/iris/model.v b/program_logic/model.v
similarity index 96%
rename from iris/model.v
rename to program_logic/model.v
index 6fde393bb..40be67805 100644
--- a/iris/model.v
+++ b/program_logic/model.v
@@ -1,5 +1,5 @@
-Require Export modures.logic iris.resources.
-Require Import modures.cofe_solver.
+Require Export logic.upred program_logic.resources.
+Require Import algebra.cofe_solver.
 
 Module iProp.
 Definition F (Λ : language) (Σ : iFunctor) (A B : cofeT) : cofeT :=
diff --git a/iris/namespace.v b/program_logic/namespace.v
similarity index 96%
rename from iris/namespace.v
rename to program_logic/namespace.v
index 7db388927..11c3a001c 100644
--- a/iris/namespace.v
+++ b/program_logic/namespace.v
@@ -1,4 +1,4 @@
-Require Export modures.base prelude.countable prelude.co_pset.
+Require Export algebra.base prelude.countable prelude.co_pset.
 
 Definition namespace := list positive.
 Definition nnil : namespace := nil.
diff --git a/iris/ownership.v b/program_logic/ownership.v
similarity index 98%
rename from iris/ownership.v
rename to program_logic/ownership.v
index fc168f419..0fbbeb8ff 100644
--- a/iris/ownership.v
+++ b/program_logic/ownership.v
@@ -1,4 +1,4 @@
-Require Export iris.model.
+Require Export program_logic.model.
 
 Definition inv {Λ Σ} (i : positive) (P : iProp Λ Σ) : iProp Λ Σ :=
   uPred_own (Res {[ i ↦ to_agree (Later (iProp_unfold P)) ]} ∅ ∅).
diff --git a/iris/pviewshifts.v b/program_logic/pviewshifts.v
similarity index 98%
rename from iris/pviewshifts.v
rename to program_logic/pviewshifts.v
index 4ff9bf80f..1ce9fc629 100644
--- a/iris/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -1,5 +1,5 @@
-Require Export iris.ownership prelude.co_pset.
-Require Import iris.wsat.
+Require Export program_logic.ownership prelude.co_pset.
+Require Import program_logic.wsat.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
 Local Hint Extern 100 (_ ∉ _) => solve_elem_of.
diff --git a/iris/resources.v b/program_logic/resources.v
similarity index 98%
rename from iris/resources.v
rename to program_logic/resources.v
index d2692b7da..5692e645d 100644
--- a/iris/resources.v
+++ b/program_logic/resources.v
@@ -1,5 +1,5 @@
-Require Export modures.fin_maps modures.agree modures.excl.
-Require Export iris.language iris.functor.
+Require Export algebra.fin_maps algebra.agree algebra.excl.
+Require Export program_logic.language program_logic.functor.
 
 Record res (Λ : language) (Σ : iFunctor) (A : cofeT) := Res {
   wld : mapRA positive (agreeRA A);
diff --git a/iris/tests.v b/program_logic/tests.v
similarity index 87%
rename from iris/tests.v
rename to program_logic/tests.v
index 6c03babaa..b499de9fa 100644
--- a/iris/tests.v
+++ b/program_logic/tests.v
@@ -1,5 +1,5 @@
 (** This file tests a bunch of things. *)
-Require Import iris.model.
+Require Import program_logic.model.
 
 Module ModelTest. (* Make sure we got the notations right. *)
   Definition iResTest {Λ : language} {Σ : iFunctor}
diff --git a/iris/viewshifts.v b/program_logic/viewshifts.v
similarity index 98%
rename from iris/viewshifts.v
rename to program_logic/viewshifts.v
index 55a54e1c1..c44d8a415 100644
--- a/iris/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -1,4 +1,4 @@
-Require Export iris.pviewshifts.
+Require Export program_logic.pviewshifts.
 
 Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
   (□ (P → pvs E1 E2 Q))%I.
diff --git a/iris/weakestpre.v b/program_logic/weakestpre.v
similarity index 99%
rename from iris/weakestpre.v
rename to program_logic/weakestpre.v
index 2f4d50aec..5d3a383f9 100644
--- a/iris/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -1,5 +1,5 @@
-Require Export iris.pviewshifts.
-Require Import iris.wsat.
+Require Export program_logic.pviewshifts.
+Require Import program_logic.wsat.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 100 (@eq coPset _ _) => eassumption || solve_elem_of.
 Local Hint Extern 100 (_ ∉ _) => solve_elem_of.
diff --git a/iris/wsat.v b/program_logic/wsat.v
similarity index 98%
rename from iris/wsat.v
rename to program_logic/wsat.v
index 996842ca5..6df7ef4be 100644
--- a/iris/wsat.v
+++ b/program_logic/wsat.v
@@ -1,5 +1,5 @@
-Require Export iris.model prelude.co_pset.
-Require Export modures.cmra_big_op modures.cmra_tactics.
+Require Export program_logic.model prelude.co_pset.
+Require Export algebra.cmra_big_op algebra.cmra_tactics.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 10 (✓{_} _) => solve_validN.
 Local Hint Extern 1 (✓{_} (gst _)) => apply gst_validN.
-- 
GitLab