From 447596447e6f290f4ec7d3b2fa63c39035493871 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date: Thu, 2 May 2019 10:29:51 +0200
Subject: [PATCH] Refactored encodable and minor clean up

---
 _CoqProject                    |  1 +
 theories/encodings/encodable.v | 66 +++++++++++++++++++++++++++++++++
 theories/encodings/stype.v     |  1 -
 theories/encodings/stype_enc.v | 67 +---------------------------------
 theories/examples/proofs_enc.v |  2 +-
 theories/typing/stype.v        |  8 ++--
 6 files changed, 73 insertions(+), 72 deletions(-)
 create mode 100644 theories/encodings/encodable.v

diff --git a/_CoqProject b/_CoqProject
index 5b3e256..7a5a098 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -3,6 +3,7 @@
 theories/typing/involutive.v
 theories/typing/side.v
 theories/typing/stype.v
+theories/encodings/encodable.v
 theories/encodings/list.v
 theories/encodings/auth_excl.v
 theories/encodings/channel.v
diff --git a/theories/encodings/encodable.v b/theories/encodings/encodable.v
new file mode 100644
index 0000000..2f80f68
--- /dev/null
+++ b/theories/encodings/encodable.v
@@ -0,0 +1,66 @@
+From iris.heap_lang Require Import proofmode notation.
+
+Class Encodable A := encode : A -> val.
+Instance val_encodable : Encodable val := id.
+Instance int_encodable : Encodable Z := λ n, #n.
+Instance bool_encodable : Encodable bool := λ b, #b.
+Instance unit_encodable : Encodable unit := λ _, #().
+Instance loc_encodable : Encodable loc := λ l, #l.
+
+Class Decodable A := decode : val -> option A.
+Instance val_decodable : Decodable val := id $ Some.
+Instance int_decodable : Decodable Z :=
+  λ v, match v with
+       | LitV (LitInt z) => Some z
+       | _ => None
+       end.
+Instance bool_decodable : Decodable bool :=
+  λ v, match v with
+       | LitV (LitBool b) => Some b
+       | _ => None
+       end.
+Instance loc_decodable : Decodable loc :=
+  λ v, match v with
+       | LitV (LitLoc l) => Some l
+       | _ => None
+       end.
+
+Class EncDec (A : Type) {EA : Encodable A} {DA : Decodable A} :=
+{
+  encdec : ∀ v, decode (encode v) = Some v;
+  decenc : ∀ (v : val) (w : A) , decode v = Some w -> encode w = v
+}.
+
+Ltac solve_encdec := intros v; by unfold decode, encode.
+Ltac solve_decenc :=
+  intros v w H;
+  destruct v as [l | | | | ]; try by inversion H;
+  destruct l; try by inversion H.
+
+Ltac solve_encdec_decenc :=
+  split; [solve_encdec | solve_decenc].
+
+Instance val_encdec : EncDec val.
+Proof.
+  split.
+  - intros v. unfold decode, encode. eauto.
+  - intros v w H. by destruct v; inversion H.
+Qed.
+Instance int_encdec : EncDec Z.
+Proof. solve_encdec_decenc. Qed.
+Instance bool_encdec : EncDec bool.
+Proof. solve_encdec_decenc. Qed.
+Instance loc_encdec : EncDec loc.
+Proof. solve_encdec_decenc. Qed.
+
+Lemma enc_dec {A : Type} `{ED : EncDec A}
+      v (w : A) : encode w = v <-> decode v = Some w.
+Proof.
+  split.
+  - intros.
+    rewrite -encdec.
+    rewrite -H.
+    reflexivity.
+  - intros.
+    apply decenc. eauto.
+Qed.
diff --git a/theories/encodings/stype.v b/theories/encodings/stype.v
index 0129edf..dd4528e 100644
--- a/theories/encodings/stype.v
+++ b/theories/encodings/stype.v
@@ -273,7 +273,6 @@ Section stype_specs.
           iApply (st_eval_send with "HP").
             by iRewrite -"Heq".
       }
-
       iModIntro. iFrame. rewrite /is_st. auto.
   Qed.
 
diff --git a/theories/encodings/stype_enc.v b/theories/encodings/stype_enc.v
index 4edc469..3768474 100644
--- a/theories/encodings/stype_enc.v
+++ b/theories/encodings/stype_enc.v
@@ -3,72 +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.
-
-Class Encodable A := encode : A -> val.
-Instance val_encodable : Encodable val := id.
-Instance int_encodable : Encodable Z := λ n, #n.
-Instance bool_encodable : Encodable bool := λ b, #b.
-Instance unit_encodable : Encodable unit := λ _, #().
-Instance loc_encodable : Encodable loc := λ l, #l.
-
-Class Decodable A := decode : val -> option A.
-Instance val_decodable : Decodable val := id $ Some.
-Instance int_decodable : Decodable Z :=
-  λ v, match v with
-       | LitV (LitInt z) => Some z
-       | _ => None
-       end.
-Instance bool_decodable : Decodable bool :=
-  λ v, match v with
-       | LitV (LitBool b) => Some b
-       | _ => None
-       end.
-Instance loc_decodable : Decodable loc :=
-  λ v, match v with
-       | LitV (LitLoc l) => Some l
-       | _ => None
-       end.
-
-Class EncDec (A : Type) {EA : Encodable A} {DA : Decodable A} :=
-{
-  encdec : ∀ v, decode (encode v) = Some v;
-  decenc : ∀ (v : val) (w : A) , decode v = Some w -> encode w = v
-}.
-
-Ltac solve_encdec := intros v; by unfold decode, encode.
-Ltac solve_decenc :=
-  intros v w H;
-  destruct v as [l | | | | ]; try by inversion H;
-  destruct l; try by inversion H.
-
-Ltac solve_encdec_decenc :=
-  split; [solve_encdec | solve_decenc].
-
-Instance val_encdec : EncDec val.
-Proof.
-  split.
-  - intros v. unfold decode, encode. eauto.
-  - intros v w H. by destruct v; inversion H.
-Qed.
-Instance int_encdec : EncDec Z.
-Proof. solve_encdec_decenc. Qed.
-Instance bool_encdec : EncDec bool.
-Proof. solve_encdec_decenc. Qed.
-Instance loc_encdec : EncDec loc.
-Proof. solve_encdec_decenc. Qed.
-
-Lemma enc_dec {A : Type} `{ED : EncDec A}
-      v (w : A) : encode w = v <-> decode v = Some w.
-Proof.
-  split.
-  - intros.
-    rewrite -encdec.
-    rewrite -H.
-    reflexivity.
-  - intros.
-    apply decenc. eauto.
-Qed.
+From osiris.encodings Require Export encodable stype.
 
 Section DualStypeEnc.
   Context `{EncDec V} `{PROP: bi} .
diff --git a/theories/examples/proofs_enc.v b/theories/examples/proofs_enc.v
index 5dd0ba4..521d2f2 100644
--- a/theories/examples/proofs_enc.v
+++ b/theories/examples/proofs_enc.v
@@ -57,8 +57,8 @@ Section ExampleProofsEnc.
   Lemma heaplet_proof :
     {{{ True }}} heaplet_example {{{ v l, RET v; ⌜v = #5⌝ ∗ l ↦ v }}}.
   Proof.
-    iIntros (Φ H) "HΦ".
     rewrite /heaplet_example.
+    iIntros (Φ H) "HΦ".
     wp_apply (new_chan_st_spec N (<!> v @ (v ↦ #5), TEnd))=> //;
     iIntros (c γ) "[Hstl Hstr]"=> /=.
     wp_apply (wp_fork with "[Hstl]").
diff --git a/theories/typing/stype.v b/theories/typing/stype.v
index 84f31e4..ce4de20 100644
--- a/theories/typing/stype.v
+++ b/theories/typing/stype.v
@@ -39,13 +39,13 @@ Notation "<!> x @ P , st" :=
 Notation "<?> x @ P , st" :=
   (TSR Receive (λ x, P%I) (λ x, st%stype))
   (at level 200, x pattern, st at level 200) : stype_scope.
-Notation "<!> x , st" := (<!> x @ True, (st x))%stype
+Notation "<!> x , st" := (<!> x @ True, st%stype)%stype
   (at level 200, x pattern, st at level 200) : stype_scope.
-Notation "<?> x , st" := (<?> x @ True, (st x))%stype
+Notation "<?> x , st" := (<?> x @ True, st%stype)%stype
   (at level 200, x pattern, st at level 200) : stype_scope.
-Notation "<!> @ P , st" := (<!> dummy__ @ P dummy__, st dummy__)%stype
+Notation "<!> @ P , st" := (<!> x @ P x, st x)%stype
   (at level 200, st at level 200) : stype_scope.
-Notation "<?> @ P , st" := (<?> dummy__ @ P dummy__, st dummy__)%stype
+Notation "<?> @ P , st" := (<?> x @ P x, st x)%stype
   (at level 200, st at level 200) : stype_scope.
 
 Section stype_ofe.
-- 
GitLab