Refactoring: encodings -> proto

_CoqProject

 -Q theories osiris
 -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
 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/channel.v
-theories/encodings/stype.v
-theories/encodings/stype_enc.v
-theories/encodings/branching.v
+theories/proto/encodable.v
+theories/proto/list.v
+theories/proto/channel.v
+theories/proto/involutive.v
+theories/proto/side.v
+theories/proto/stype_def.v
+theories/proto/stype.v
+theories/proto/stype_enc.v
+theories/proto/branching.v
 theories/examples/examples.v
 theories/examples/proofs.v
 theories/examples/proofs_enc.v

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.encodings Require Import channel branching.
 From iris.base_logic Require Import invariants.
+From osiris.proto Require Import channel branching.
 
 Section BranchingExamples.
   Context `{!heapG Σ} (N : namespace).

theories/examples/branching_proofs.v

@@ -2,7 +2,7 @@ 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.encodings Require Import branching.
+From osiris.proto Require Import branching.
 From osiris.examples Require Import branching_examples.
 
 Section BranchingExampleProofs.

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.encodings Require Import stype.
 From iris.base_logic Require Import invariants.
+From osiris.proto Require Import stype.
 
 Section Examples.
   Context `{!heapG Σ} (N : namespace).

theories/examples/list_sort.v

+From stdpp Require Import sorting.
+Require Import Coq.Lists.List.
+Require Import Omega.
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
-From osiris.encodings Require Import list channel stype_enc.
+From osiris.proto Require Import list channel stype_enc.
 From iris.base_logic Require Import invariants.
-From stdpp Require Import sorting.
-Require Import Coq.Lists.List.
-Require Import Omega.
 
 Section ListSortExample.
   Context `{!heapG Σ} `{logrelG val Σ} (N : namespace).

theories/examples/proofs.v

@@ -2,7 +2,7 @@ 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.encodings Require Import stype.
+From osiris.proto Require Import stype.
 From osiris.examples Require Import examples.
 
 Section ExampleProofs.

theories/examples/proofs_enc.v

@@ -3,7 +3,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import list auth excl.
 From iris.base_logic Require Import invariants.
-From osiris.encodings Require Import stype_enc.
+From osiris.proto Require Import stype_enc.
 From osiris.examples Require Import examples.
 
 Section ExampleProofsEnc.

theories/encodings/branching.v → theories/proto/branching.v

@@ -3,7 +3,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import list auth excl.
 From iris.base_logic Require Import invariants.
-From osiris.encodings Require Export stype_enc.
+From osiris.proto Require Export stype_enc.
 
 Section DualBranch.
   Context `{PROP : bi}.

theories/encodings/channel.v → theories/proto/channel.v

@@ -6,8 +6,8 @@ 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.base_logic Require Import auth_excl.
-From osiris.encodings Require Export side.
-From osiris.encodings Require Import list.
+From osiris.proto Require Export side.
+From osiris.proto Require Import list.
 Set Default Proof Using "Type".
 Import uPred.
 

theories/proto/involutive.v

+From iris.heap_lang Require Import proofmode notation.
+
+Class Involutive {A} (R : relation A) (f : A → A) :=
+  involutive x : R (f (f x)) x.

theories/encodings/side.v → theories/proto/side.v

 From iris.heap_lang Require Import proofmode notation.
-From osiris.encodings Require Export involutive.
+From osiris.proto Require Export involutive.
 
 Inductive side := Left | Right.
 Instance side_inhabited : Inhabited side := populate Left.

theories/encodings/stype.v → theories/proto/stype.v

@@ -6,8 +6,8 @@ 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.base_logic Require Import auth_excl.
-From osiris.encodings Require Export stype_def.
-From osiris.encodings Require Export channel.
+From osiris.proto Require Export stype_def.
+From osiris.proto Require Export channel.
 
 Class logrelG A Σ := {
   logrelG_channelG :> chanG Σ;

theories/encodings/stype_def.v → theories/proto/stype_def.v

@@ -4,7 +4,7 @@ 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.
+From osiris.proto Require Import involutive.
 Set Default Proof Using "Type".
 
 Inductive action := Send | Receive.

theories/encodings/stype_enc.v → theories/proto/stype_enc.v

@@ -3,7 +3,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import list auth excl.
 From iris.base_logic Require Import invariants.
-From osiris.encodings Require Export encodable stype.
+From osiris.proto Require Export encodable stype.
 
 Section DualStypeEnc.
   Context `{EncDec V} `{PROP: bi} .