From 3e0564c7ea3924c1e2a5cbe35e31aa347d08c207 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Mon, 19 Dec 2016 21:37:44 +0100
Subject: [PATCH] fn, int, bool are Send and Sync

---
 theories/typing/bool.v     | 3 +++
 theories/typing/function.v | 3 +++
 theories/typing/int.v      | 3 +++
 theories/typing/type.v     | 7 +++++++
 4 files changed, 16 insertions(+)

diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 7e49a86b..24d39789 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -9,6 +9,9 @@ Section bool.
     {| st_own tid vl := (∃ z:bool, ⌜vl = [ #z ]⌝)%I |}.
   Next Obligation. iIntros (tid vl) "H". iDestruct "H" as (z) "%". by subst. Qed.
 
+  Global Instance bool_send : Send bool.
+  Proof. iIntros (tid1 tid2 vl). done. Qed.
+
   Lemma typed_bool (b : Datatypes.bool) E L :
     typed_instruction_ty E L [] #b bool.
   Proof.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index fa673091..7d8e766c 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -18,6 +18,9 @@ Section fn.
     iIntros (A n E tys ty tid vl) "H". iDestruct "H" as (f) "[% _]". by subst.
   Qed.
 
+  Global Instance fn_send {A n} E tys ty : Send (@fn A n E tys ty).
+  Proof. iIntros (tid1 tid2 vl). done. Qed.
+
   Lemma fn_subtype_ty A n E0 L0 E tys1 tys2 ty1 ty2 :
     (∀ x, Forall2 (subtype (E0 ++ E x) L0) (tys2 x : vec _ _) (tys1 x : vec _ _)) →
     (∀ x, subtype (E0 ++ E x) L0 (ty1 x) (ty2 x)) →
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 88e86c93..8a376c8d 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -9,6 +9,9 @@ Section int.
     {| st_own tid vl := (∃ z:Z, ⌜vl = [ #z ]⌝)%I |}.
   Next Obligation. iIntros (tid vl) "H". iDestruct "H" as (z) "%". by subst. Qed.
 
+  Global Instance int_send : Send int.
+  Proof. iIntros (tid1 tid2 vl). done. Qed.
+
   Lemma typed_int (z : Z) E L :
     typed_instruction_ty E L [] #z int.
   Proof.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 34bccb46..f100c005 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -178,6 +178,13 @@ Section type.
       iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op // Qp_div_2.
       iDestruct "Hmt" as "[>% Hmt]". subst. by iApply "Hclose".
   Qed.
+
+  Global Instance ty_of_st_sync st :
+    Send (ty_of_st st) → Sync (ty_of_st st).
+  Proof.
+    iIntros (Hsend κ tid1 tid2 l) "H". iDestruct "H" as (vl) "[Hm Hown]".
+    iExists vl. iFrame "Hm". iNext. by iApply Hsend.
+  Qed.
 End type.
 
 Coercion ty_of_st : simple_type >-> type.
-- 
GitLab