From a9ab999a3cd452584ea78341eb6e5b9f3fb857b1 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 9 Jan 2017 07:54:43 +0100
Subject: [PATCH] Type unbox.

---
 theories/typing/borrow.v      | 60 ++++++++++++++++++++++++++++++-----
 theories/typing/tests/unbox.v | 29 +++++++++++++++++
 2 files changed, 81 insertions(+), 8 deletions(-)
 create mode 100644 theories/typing/tests/unbox.v

diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 9cc162d9..d6204fdb 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -46,11 +46,12 @@ Section borrow.
     apply (tctx_incl_frame_r _ [_] [_;_]). rewrite ->tctx_share; solve_typing.
   Qed.
 
-  Lemma type_deref_uniq_own {E L} κ p n ty :
+  Lemma type_deref_uniq_own_instr {E L} κ p n ty :
     lctx_lft_alive E L κ →
     typed_instruction_ty E L [p ◁ &uniq{κ} own n ty] (!p) (&uniq{κ} ty).
   Proof.
-    iIntros (Hκ) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
+    iIntros (Hκ) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp".
+    rewrite tctx_interp_singleton.
     iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
     iDestruct "Hown" as (l P) "[[Heq #HPiff] HP]". iDestruct "Heq" as %[=->].
@@ -69,11 +70,22 @@ Section borrow.
       rewrite -heap_mapsto_vec_singleton. iFrame. iExists _. by iFrame.
   Qed.
 
-  Lemma type_deref_shr_own {E L} κ p n ty :
+  Lemma type_deref_uniq_own {E L} κ x p e n ty C T T' :
+    Closed (x :b: []) e →
+    tctx_extract_hasty E L p (&uniq{κ} own n ty) T T' →
+    lctx_lft_alive E L κ →
+    (∀ (v:val), typed_body E L C ((v ◁ &uniq{κ} ty) :: T') (subst' x v e)) →
+    typed_body E L C T (let: x := !p in e).
+  Proof.
+    intros. eapply type_let; [done|by apply type_deref_uniq_own_instr|solve_typing|done].
+  Qed.
+
+  Lemma type_deref_shr_own_instr {E L} κ p n ty :
     lctx_lft_alive E L κ →
     typed_instruction_ty E L [p ◁ &shr{κ} own n ty] (!p) (&shr{κ} ty).
   Proof.
-    iIntros (Hκ) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
+    iIntros (Hκ) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp".
+    rewrite tctx_interp_singleton.
     iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
     iDestruct "Hown" as (l) "[Heq #H↦]". iDestruct "Heq" as %[=->].
@@ -81,16 +93,28 @@ Section borrow.
     iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
     iApply (wp_fupd_step _ (_∖_) with "[Hown Htok2]"); try done.
     - iApply ("Hown" with "* [%] Htok2"). set_solver+.
-    - wp_read. iIntros "!>[#Hshr Htok2]". iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
+    - wp_read. iIntros "!>[#Hshr Htok2]".
+      iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
       iMod ("Hclose" with "[Htok1 Htok2]") as "($ & $)"; first by iFrame.
       rewrite tctx_interp_singleton tctx_hasty_val' //. iExists _. auto.
   Qed.
 
-  Lemma type_deref_uniq_uniq {E L} κ κ' p ty :
+  Lemma type_deref_shr_own {E L} κ x p e n ty C T T' :
+    Closed (x :b: []) e →
+    tctx_extract_hasty E L p (&shr{κ} own n ty) T T' →
+    lctx_lft_alive E L κ →
+    (∀ (v:val), typed_body E L C ((v ◁ &shr{κ} ty) :: T') (subst' x v e)) →
+    typed_body E L C T (let: x := !p in e).
+  Proof.
+    intros. eapply type_let; [done|by apply type_deref_shr_own_instr|solve_typing|done].
+  Qed.
+
+  Lemma type_deref_uniq_uniq_instr {E L} κ κ' p ty :
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
     typed_instruction_ty E L [p ◁ &uniq{κ} &uniq{κ'} ty] (!p) (&uniq{κ} ty).
   Proof.
-    iIntros (Hκ Hincl) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
+    iIntros (Hκ Hincl) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp".
+    rewrite tctx_interp_singleton.
     iPoseProof (Hincl with "[#] [#]") as "Hincl".
     { by iApply elctx_interp_persist. } { by iApply llctx_interp_persist. }
     iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
@@ -116,7 +140,17 @@ Section borrow.
     iApply (lft_incl_glb with "Hincl"). iApply lft_incl_refl.
   Qed.
 
-  Lemma type_deref_shr_uniq {E L} κ κ' p ty :
+  Lemma type_deref_uniq_uniq {E L} κ κ' x p e ty C T T' :
+    Closed (x :b: []) e →
+    tctx_extract_hasty E L p (&uniq{κ} &uniq{κ'} ty) T T' →
+    lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
+    (∀ (v:val), typed_body E L C ((v ◁ &uniq{κ} ty) :: T') (subst' x v e)) →
+    typed_body E L C T (let: x := !p in e).
+  Proof.
+    intros. eapply type_let; [done|by apply type_deref_uniq_uniq_instr|solve_typing|done].
+  Qed.
+
+  Lemma type_deref_shr_uniq_instr {E L} κ κ' p ty :
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
     typed_instruction_ty E L [p ◁ &shr{κ} &uniq{κ'} ty] (!p) (&shr{κ} ty).
   Proof.
@@ -139,6 +173,16 @@ Section borrow.
       rewrite tctx_interp_singleton tctx_hasty_val' //.
       iExists _. iSplitR. done. by iApply (ty_shr_mono with "LFT Hincl' Hshr").
   Qed.
+
+  Lemma type_deref_shr_uniq {E L} κ κ' x p e ty C T T' :
+    Closed (x :b: []) e →
+    tctx_extract_hasty E L p (&shr{κ} &uniq{κ'} ty) T T' →
+    lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
+    (∀ (v:val), typed_body E L C ((v ◁ &shr{κ} ty) :: T') (subst' x v e)) →
+    typed_body E L C T (let: x := !p in e).
+  Proof.
+    intros. eapply type_let; [done|by apply type_deref_shr_uniq_instr|solve_typing|done].
+  Qed.
 End borrow.
 
 Hint Resolve tctx_extract_hasty_borrow tctx_extract_hasty_borrow_share
diff --git a/theories/typing/tests/unbox.v b/theories/typing/tests/unbox.v
new file mode 100644
index 00000000..73a22b1a
--- /dev/null
+++ b/theories/typing/tests/unbox.v
@@ -0,0 +1,29 @@
+From lrust.lifetime Require Import definitions.
+From lrust.lang Require Import new_delete.
+From lrust.typing Require Import programs product product_split own uniq_bor
+                    shr_bor int function lft_contexts uninit cont borrow.
+Set Default Proof Using "Type".
+
+Section unbox.
+  Context `{typeG Σ}.
+
+  Definition unbox :=
+    (funrec: <> ["b"] :=
+       let: "b'" := !"b" in let: "bx" := !"b'" in
+       letalloc: "r" := "bx" +â‚— #0 in
+       delete [ #1; "b"] ;; "return" ["r":expr])%E.
+
+  Lemma ubox_type :
+    typed_instruction_ty [] [] [] unbox
+        (fn (λ α, [☀α])%EL (λ α, [# own 1 (&uniq{α}own 2 (Π[int; int]))])
+            (λ α, own 1 (&uniq{α} int))).
+  Proof.
+    apply type_fn; try apply _. move=> /= α ret b. inv_vec b=>b. simpl_subst.
+    eapply type_deref; try solve_typing. by apply read_own_move. done.
+      intros b'; simpl_subst.
+    eapply type_deref_uniq_own; (try solve_typing)=>bx; simpl_subst.
+    eapply (type_letalloc_1 (&uniq{α}int)); (try solve_typing)=>r. simpl_subst.
+    eapply type_delete; try solve_typing.
+    eapply (type_jump [_]); solve_typing.
+  Qed.
+End unbox.
-- 
GitLab