From 03de6315b569f8adf62540554cccdae18009ce3a Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date: Tue, 11 Jun 2019 19:15:40 +0200
Subject: [PATCH] Initial refactor

---
 _CoqProject                                        | 7 ++++---
 theories/{encodings => base_logic}/auth_excl.v     | 0
 theories/encodings/channel.v                       | 5 +++--
 theories/{typing => encodings}/side.v              | 2 +-
 theories/encodings/stype.v                         | 4 ++--
 theories/{typing/stype.v => encodings/stype_def.v} | 4 +---
 theories/examples/branching_examples.v             | 1 -
 theories/examples/branching_proofs.v               | 1 -
 theories/examples/examples.v                       | 3 +--
 theories/examples/list_sort.v                      | 1 -
 theories/examples/proofs.v                         | 1 -
 11 files changed, 12 insertions(+), 17 deletions(-)
 rename theories/{encodings => base_logic}/auth_excl.v (100%)
 rename theories/{typing => encodings}/side.v (86%)
 rename theories/{typing/stype.v => encodings/stype_def.v} (99%)

diff --git a/_CoqProject b/_CoqProject
index e859773..15c320d 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,10 +1,11 @@
 -Q theories osiris
 -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
-theories/typing/side.v
-theories/typing/stype.v
+theories/base_logic/auth_excl.v
+theories/encodings/involutive.v
+theories/encodings/side.v
+theories/encodings/stype_def.v
 theories/encodings/encodable.v
 theories/encodings/list.v
-theories/encodings/auth_excl.v
 theories/encodings/channel.v
 theories/encodings/stype.v
 theories/encodings/stype_enc.v
diff --git a/theories/encodings/auth_excl.v b/theories/base_logic/auth_excl.v
similarity index 100%
rename from theories/encodings/auth_excl.v
rename to theories/base_logic/auth_excl.v
diff --git a/theories/encodings/channel.v b/theories/encodings/channel.v
index fa0ed8a..c9feffb 100644
--- a/theories/encodings/channel.v
+++ b/theories/encodings/channel.v
@@ -5,8 +5,9 @@ From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import excl auth list.
 From iris.base_logic.lib Require Import auth.
 From iris.heap_lang.lib Require Import spin_lock.
-From osiris.typing Require Export side.
-From osiris.encodings Require Import list auth_excl.
+From osiris.base_logic Require Import auth_excl.
+From osiris.encodings Require Export side.
+From osiris.encodings Require Import list.
 Set Default Proof Using "Type".
 Import uPred.
 
diff --git a/theories/typing/side.v b/theories/encodings/side.v
similarity index 86%
rename from theories/typing/side.v
rename to theories/encodings/side.v
index 1c418d8..f58a57b 100644
--- a/theories/typing/side.v
+++ b/theories/encodings/side.v
@@ -1,5 +1,5 @@
 From iris.heap_lang Require Import proofmode notation.
-From osiris.typing Require Export involutive.
+From osiris.encodings Require Export involutive.
 
 Inductive side := Left | Right.
 Instance side_inhabited : Inhabited side := populate Left.
diff --git a/theories/encodings/stype.v b/theories/encodings/stype.v
index dc38fdd..6cdfac0 100644
--- a/theories/encodings/stype.v
+++ b/theories/encodings/stype.v
@@ -5,8 +5,8 @@ From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
 From iris.algebra Require Import list auth excl.
 From iris.base_logic Require Import invariants.
-From osiris.typing Require Export stype.
-From osiris.encodings Require Import auth_excl.
+From osiris.base_logic Require Import auth_excl.
+From osiris.encodings Require Export stype_def.
 From osiris.encodings Require Export channel.
 
 Class logrelG A Σ := {
diff --git a/theories/typing/stype.v b/theories/encodings/stype_def.v
similarity index 99%
rename from theories/typing/stype.v
rename to theories/encodings/stype_def.v
index da45f64..3a82661 100644
--- a/theories/typing/stype.v
+++ b/theories/encodings/stype_def.v
@@ -4,11 +4,9 @@ From stdpp Require Export list.
 From iris.base_logic Require Import base_logic.
 From iris.algebra Require Import updates local_updates.
 From iris.heap_lang Require Import proofmode notation.
+From osiris.encodings Require Import involutive.
 Set Default Proof Using "Type".
 
-Class Involutive {A} (R : relation A) (f : A → A) :=
-  involutive x : R (f (f x)) x.
-
 Inductive action := Send | Receive.
 Instance action_inhabited : Inhabited action := populate Send.
 Definition dual_action (a : action) : action :=
diff --git a/theories/examples/branching_examples.v b/theories/examples/branching_examples.v
index bd75583..8b74313 100644
--- a/theories/examples/branching_examples.v
+++ b/theories/examples/branching_examples.v
@@ -1,7 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
-From osiris.typing Require Import side stype.
 From osiris.encodings Require Import channel branching.
 From iris.base_logic Require Import invariants.
 
diff --git a/theories/examples/branching_proofs.v b/theories/examples/branching_proofs.v
index a7cadc1..5226ad6 100644
--- a/theories/examples/branching_proofs.v
+++ b/theories/examples/branching_proofs.v
@@ -2,7 +2,6 @@ From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
 From iris.base_logic Require Import invariants.
-From osiris.typing Require Import side stype.
 From osiris.encodings Require Import branching.
 From osiris.examples Require Import branching_examples.
 
diff --git a/theories/examples/examples.v b/theories/examples/examples.v
index f5db63f..b40881b 100644
--- a/theories/examples/examples.v
+++ b/theories/examples/examples.v
@@ -1,8 +1,7 @@
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
-From osiris.typing Require Import side stype.
-From osiris.encodings Require Import channel stype.
+From osiris.encodings Require Import stype.
 From iris.base_logic Require Import invariants.
 
 Section Examples.
diff --git a/theories/examples/list_sort.v b/theories/examples/list_sort.v
index 9d2c764..c235b9a 100644
--- a/theories/examples/list_sort.v
+++ b/theories/examples/list_sort.v
@@ -1,7 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
-From osiris.typing Require Import side stype.
 From osiris.encodings Require Import list channel stype_enc.
 From iris.base_logic Require Import invariants.
 From stdpp Require Import sorting.
diff --git a/theories/examples/proofs.v b/theories/examples/proofs.v
index 262c675..8254e53 100644
--- a/theories/examples/proofs.v
+++ b/theories/examples/proofs.v
@@ -2,7 +2,6 @@ From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
 From iris.base_logic Require Import invariants.
-From osiris.typing Require Import side stype.
 From osiris.encodings Require Import stype.
 From osiris.examples Require Import examples.
 
-- 
GitLab