From 43751d3e4a2d3a6626002e0695faed6b060876a3 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Wed, 30 Jan 2019 16:16:15 +0100
Subject: [PATCH] unboxed types

---
 theories/typing/interp.v | 30 ++++++++++++++++++++++++++++++
 theories/typing/types.v  |  7 +++++++
 2 files changed, 37 insertions(+)

diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index bcc74bd..4268c85 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -1,6 +1,7 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Interpretations for System F_mu_ref types *)
 From iris.algebra Require Export list.
+From iris.proofmode Require Import tactics.
 From reloc.typing Require Export types.
 From reloc.logic Require Import model.
 From Autosubst Require Import Autosubst.
@@ -51,6 +52,35 @@ Section semtypes.
     apply I. by f_equiv.
   Defined.
 
+  Lemma unboxed_type_sound τ Δ v v' :
+    UnboxedType τ →
+    interp τ Δ v v' -∗ ⌜val_is_unboxed v ∧ val_is_unboxed v'⌝.
+  Proof.
+    induction 1; simpl;
+    first [iIntros "[% %]"
+          |iDestruct 1 as (?) "[% %]"
+          |iDestruct 1 as (? ?) "[% [% ?]]"];
+    simplify_eq/=; eauto with iFrame.
+  Qed.
+
+  Lemma eq_type_sound τ Δ v v' :
+    EqType τ →
+    interp τ Δ v v' -∗ ⌜v = v'⌝.
+  Proof.
+    intros HÏ„; revert v v'; induction HÏ„; iIntros (v v') "#H1 /=".
+    - by iDestruct "H1" as "[% %]"; subst.
+    - by iDestruct "H1" as (n) "[% %]"; subst.
+    - by iDestruct "H1" as (b) "[% %]"; subst.
+    - iDestruct "H1" as (?? ??) "[% [% [H1 H2]]]"; simplify_eq/=.
+      rewrite IHHÏ„1 IHHÏ„2.
+      by iDestruct "H1" as "%"; iDestruct "H2" as "%"; subst.
+    - iDestruct "H1" as (??) "[H1|H1]".
+      + iDestruct "H1" as "[% [% H1]]"; simplify_eq/=.
+        rewrite IHHÏ„1. by iDestruct "H1" as "%"; subst.
+      + iDestruct "H1" as "[% [% H1]]"; simplify_eq/=.
+        rewrite IHHÏ„2. by iDestruct "H1" as "%"; subst.
+  Qed.
+
   Definition bin_log_related (E : coPset)
              (Δ : list lty2) (Γ : stringmap type)
              (e e' : expr) (τ : type) : iProp Σ :=
diff --git a/theories/typing/types.v b/theories/typing/types.v
index a7a08a7..87da16a 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -26,6 +26,13 @@ Inductive EqType : type → Prop :=
   | EqTProd τ τ' : EqType τ → EqType τ' → EqType (TProd τ τ')
   | EqSum τ τ' : EqType τ → EqType τ' → EqType (TSum τ τ').
 
+(** Which types are unboxed *)
+Inductive UnboxedType : type → Prop :=
+  | UnboxedTUnit : UnboxedType TUnit
+  | UnboxedTNat : UnboxedType TNat
+  | UnboxedTBool : UnboxedType TBool
+  | UnboxedTref Ï„ : UnboxedType (Tref Ï„).
+
 (** Autosubst instances *)
 Instance Ids_type : Ids type. derive. Defined.
 Instance Rename_type : Rename type. derive. Defined.
-- 
GitLab