From 288bda11bf869ca593e2051c4b907f84fdf891d8 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Mon, 7 Sep 2020 16:09:10 +0200
Subject: [PATCH] Updated typing rules to algorithmic typing

---
 theories/logrel/lib/mutex.v         |  4 ++--
 theories/logrel/term_typing_rules.v | 16 ++++++++--------
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/theories/logrel/lib/mutex.v b/theories/logrel/lib/mutex.v
index b2ca4e9..6cd4177 100644
--- a/theories/logrel/lib/mutex.v
+++ b/theories/logrel/lib/mutex.v
@@ -104,8 +104,8 @@ Section rules.
   Context `{heapG Σ, lockG Σ}.
 
   (** Mutex properties *)
-  Lemma ltyped_mutex_alloc A :
-    ⊢ ∅ ⊨ mutex_alloc : A → mutex A.
+  Lemma ltyped_mutex_alloc Γ A :
+    ⊢ Γ ⊨ mutex_alloc : A → mutex A ⫤ ∅.
   Proof.
     iIntros (vs) "!> HΓ /=". iApply wp_value.
     iSplitL; last by iApply env_ltyped_empty.
diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index f8aef55..408d8e2 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -216,8 +216,8 @@ Section properties.
   Qed.
 
   (** Sum Properties *)
-  Lemma ltyped_injl Γ e A1 A2 :
-    (Γ ⊨ e : A1) -∗ Γ ⊨ InjL e : A1 + A2.
+  Lemma ltyped_injl Γ1 Γ2 e A1 A2 :
+    (Γ1 ⊨ e : A1 ⫤ Γ2) -∗ Γ1 ⊨ InjL e : A1 + A2 ⫤ Γ2.
   Proof.
     iIntros "#HA" (vs) "!> HΓ /=".
     wp_apply (wp_wand with "(HA [HΓ //])").
@@ -225,8 +225,8 @@ Section properties.
     iLeft. iExists v. auto.
   Qed.
 
-  Lemma ltyped_injr Γ e A1 A2 :
-    (Γ ⊨ e : A2) -∗ Γ ⊨ InjR e : A1 + A2.
+  Lemma ltyped_injr Γ1 Γ2 e A1 A2 :
+    (Γ1 ⊨ e : A2 ⫤ Γ2) -∗ Γ1 ⊨ InjR e : A1 + A2 ⫤ Γ2.
   Proof.
     iIntros "#HA" (vs) "!> HΓ /=".
     wp_apply (wp_wand with "(HA [HΓ //])").
@@ -276,8 +276,8 @@ Section properties.
   Qed.
 
   (** Existential properties *)
-  Lemma ltyped_pack Γ e k (C : lty Σ k → ltty Σ) M :
-    (Γ ⊨ e : C M) -∗ Γ ⊨ e : ∃ M, C M.
+  Lemma ltyped_pack Γ1 Γ2 e k (C : lty Σ k → ltty Σ) M :
+    (Γ1 ⊨ e : C M ⫤ Γ2) -∗ Γ1 ⊨ e : ∃ M, C M ⫤ Γ2.
   Proof.
     iIntros "#He" (vs) "!> HΓ /=".
     wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB $]". by iExists M.
@@ -454,8 +454,8 @@ Section properties.
   Section with_chan.
     Context `{chanG Σ}.
 
-    Lemma ltyped_new_chan S :
-      ⊢ ∅ ⊨ new_chan : () → (chan S * chan (lty_dual S)).
+    Lemma ltyped_new_chan Γ S :
+      ⊢ Γ ⊨ new_chan : () → (chan S * chan (lty_dual S)) ⫤ ∅.
     Proof.
       iIntros (vs) "!> HΓ /=". iApply wp_value.
       iSplitL; last by iApply env_ltyped_empty.
-- 
GitLab