From 0fb03249cf363a1d7dffe5c0b60fc5f1b4549667 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Thu, 7 Mar 2019 18:21:04 +0100
Subject: [PATCH] add the typing rule for `pack`

---
 theories/typing/fundamental.v | 73 ++++++++++++-----------------------
 theories/typing/types.v       |  3 +-
 2 files changed, 27 insertions(+), 49 deletions(-)

diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 37d1a09..c6b2641 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -463,68 +463,45 @@ Section fundamental.
     by rewrite -interp_subst.
   Qed.
 
-(*
-  Lemma bin_log_related_pack' Δ Γ e e' τ τ' :
-    {Δ;Γ} ⊨ e ≤log≤ e' : τ.[τ'/] -∗
-    {Δ;Γ} ⊨ Pack e ≤log≤ Pack e' : TExists τ.
+  Lemma bin_log_related_pack' Δ Γ e e' (τ τ' : type) :
+    ({Δ;Γ} ⊨ e ≤log≤ e' : τ.[τ'/]) -∗
+    {Δ;Γ} ⊨ e ≤log≤ e' : TExists τ.
   Proof.
     iIntros "IH".
+    intro_clause.
     rel_bind_ap e e' "IH" v v' "#IH".
     value_case.
-    iExists (v, v'). iModIntro. simpl; iSplit; eauto.
-    iExists (⟦ τ' ⟧ Δ).
+    iModIntro. iExists (interp τ' Δ).
     by rewrite interp_subst.
   Qed.
 
-  Lemma bin_log_related_pack (τi : D) Δ Γ e e' τ :
-    {τi::Δ;⤉Γ} ⊨ e ≤log≤ e' : τ -∗
-    {Δ;Γ} ⊨ Pack e ≤log≤ Pack e' : TExists τ.
+  Lemma bin_log_related_pack (τi : lty2 Σ) Δ Γ e e' τ :
+    ({τi::Δ;⤉Γ} ⊨ e ≤log≤ e' : τ) -∗
+    {Δ;Γ} ⊨ e ≤log≤ e' : TExists τ.
   Proof.
-    rewrite bin_log_related_eq.
     iIntros "IH".
-    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
-    wp_bind (env_subst _ e).
-    tp_bind j (env_subst _ e').
-    iSpecialize ("IH" with "Hs [HΓ] Hj").
-    { by rewrite interp_env_ren. }
-    iMod "IH" as "IH /=". iModIntro.
-    iApply (wp_wand with "IH").
-    iIntros (v). iDestruct 1 as (v') "[Hj #IH]".
-    iApply wp_value.
-    iExists (PackV v'). simpl. iFrame.
-    iExists (v, v'). simpl; iSplit; eauto.
+    intro_clause.
+    iSpecialize ("IH" $! vs with "[Hvs]").
+    { by rewrite interp_ren. }
+    rel_bind_ap e e' "IH" v v' "#IH".
+    value_case.
+    iModIntro. by iExists Ï„i.
   Qed.
 
+(*
   Lemma bin_log_related_unpack Δ Γ e1 e1' e2 e2' τ τ2 :
-    {Δ;Γ} ⊨ e1 ≤log≤ e1' : TExists τ -∗
-    (∀ τi : D,
+    ({Δ;Γ} ⊨ e1 ≤log≤ e1' : TExists τ) -∗
+    (∀ τi : lty2 Σ,
       {τi::Δ;⤉Γ} ⊨
-        e2 ≤log≤ e2' : TArrow τ (asubst (ren (+1)) τ2)) -∗
-    {Δ;Γ} ⊨ Unpack e1 e2 ≤log≤ Unpack e1' e2' : τ2.
+        e2 ≤log≤ e2' : TArrow τ (subst (ren (+1)) τ2)) -∗
+    {Δ;Γ} ⊨ unpack e1 e2 ≤log≤ unpack e1' e2' : τ2.
   Proof.
-    rewrite bin_log_related_eq.
     iIntros "IH1 IH2".
-    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
-    smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v v' "IH1".
-    iDestruct "IH1" as ([w w']) "[% #HÏ„i]"; simplify_eq/=.
-    iDestruct "HÏ„i" as (Ï„i) "#HÏ„i"; simplify_eq/=.
-    wp_unpack.
-    iApply fupd_wp.
-    tp_pack j; eauto. iModIntro.
-    iSpecialize ("IH2" $! τi with "Hs [HΓ]"); auto.
-    { by rewrite interp_env_ren. }
-    tp_bind j (env_subst (snd <$> vvs) e2').
-    iMod ("IH2" with "Hj") as "IH2". simpl.
-    wp_bind (env_subst (fst <$> vvs) e2).
-    iApply (wp_wand with "IH2").
-    iIntros (v). iDestruct 1 as (v') "[Hj #Hvv']".
-    iSpecialize ("Hvv'" $! (w,w') with "HÏ„i Hj"). simpl.
-    iMod "Hvv'".
-    iApply (wp_wand with "Hvv'"). clear v v'.
-    iIntros (v). iDestruct 1 as (v') "[Hj #Hvv']".
-    rewrite (interp_weaken [] [τi] Δ _ τ2) /=.
-    eauto.
-  Qed.
+    intro_clause.
+    Abort.
+    iSpecialize ("IH2" $! vs with "[Hvs]").
+    { by rewrite interp_ren. }
+    rel_bind_ap e2 e2' "IH2" v v' "#IH2".
 *)
 
   Theorem binary_fundamental Δ Γ e τ :
@@ -551,7 +528,7 @@ Section fundamental.
     - by iApply bin_log_related_tapp'.
     - by iApply bin_log_related_fold.
     - by iApply bin_log_related_unfold.
-    (* - by iApply bin_log_related_pack'. *)
+    - by iApply bin_log_related_pack'.
     (* - iApply (bin_log_related_unpack with "[]"); eauto. *)
     - by iApply bin_log_related_fork.
     - by iApply bin_log_related_alloc.
diff --git a/theories/typing/types.v b/theories/typing/types.v
index 3885f43..d227fdc 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -127,7 +127,8 @@ Inductive typed (Γ : stringmap type) : expr → type → Prop :=
      Γ ⊢ₜ e #() : τ.[τ'/]
   | TFold e τ : Γ ⊢ₜ e : τ.[TRec τ/] → Γ ⊢ₜe : TRec τ
   | TUnfold e τ : Γ ⊢ₜ e : TRec τ → Γ ⊢ₜ rec_unfold e : τ.[TRec τ/]
-  (* | TPack e τ τ' : Γ ⊢ₜ e : τ.[τ'/] → Γ ⊢ₜ e : TExists τ *)
+  | TPack e τ τ' : Γ ⊢ₜ e : τ.[τ'/] → Γ ⊢ₜ e : TExists τ
+  (* todo *)
   (* | TUnpack e1 e2 τ τ2 : Γ ⊢ₜ e1 : TExists τ → *)
   (*     (subst (ren (+1%nat)) <$> Γ) ⊢ₜ e2 : TArrow τ (subst (ren (+1%nat)) τ2) → *)
   (*     Γ ⊢ₜ unpack e1 e2 : τ2 *)
-- 
GitLab