Initial refactor

_CoqProject

 -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

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.
 

theories/typing/side.v → theories/encodings/side.v

 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.

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 Σ := {

theories/typing/stype.v → 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 :=

theories/examples/branching_examples.v

 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.
 

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.
 

theories/examples/examples.v

 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.

theories/examples/list_sort.v

 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.

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.