From f3ad9e36433f57617e986ba41499a94230741c5a Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Fri, 5 Jun 2020 11:54:38 +0200
Subject: [PATCH] Added a typing example of a mapper client

---
 theories/logrel/examples/mapper.v | 36 +++++++++++++++++++++++++++++--
 1 file changed, 34 insertions(+), 2 deletions(-)

diff --git a/theories/logrel/examples/mapper.v b/theories/logrel/examples/mapper.v
index 8f365ff..e85fdea 100644
--- a/theories/logrel/examples/mapper.v
+++ b/theories/logrel/examples/mapper.v
@@ -1,10 +1,18 @@
 From actris.channel Require Import proofmode proto channel.
-From actris.logrel Require Import subtyping_rules term_typing_judgment term_typing_rules environments.
+From actris.logrel Require Import subtyping_rules term_typing_judgment term_typing_rules environments operators.
 From iris.proofmode Require Import tactics.
 
 Section with_Σ.
   Context `{heapG Σ, chanG Σ}.
 
+  Definition mapper_client_type : lsty Σ :=
+    <!!> TY (lty_int ⊸ lty_bool); <!!> TY lty_int; <??> TY lty_bool; END.
+
+  Definition mapper_client : expr := λ: "c",
+    let: "f" := send "c" (λ: "x", #9000 < "x") in
+    let: "v" := send "c" #42 in
+    recv "c".
+
   Definition mapper_service_type : lsty Σ :=
     <??> TY (lty_int ⊸ lty_bool); <??> TY lty_int; <!!> TY lty_bool; END.
 
@@ -13,7 +21,31 @@ Section with_Σ.
     let: "v" := recv "c" in
     send "c" ("f" "v");; "c".
 
-  Lemma mapper_typed Γ :
+  Lemma mapper_client_typed Γ :
+    ⊢ Γ ⊨ mapper_client : (lty_chan (mapper_client_type) ⊸ lty_bool)%lty ⫤ Γ.
+  Proof.
+    iApply (ltyped_frame _ _ _ _ Γ).
+    { iApply env_split_id_l. }
+    2: { iApply env_split_id_l. }
+    iApply ltyped_lam.
+    iApply ltyped_let.
+    { iApply ltyped_send. apply lookup_insert.
+      iApply (ltyped_frame _ _ _ _ {["c":=_]}).
+      { iApply env_split_id_l. }
+      { iApply ltyped_lam. iApply ltyped_bin_op.
+        - iApply ltyped_var. apply lookup_insert.
+        - iApply ltyped_int. }
+      { iApply env_split_id_l. } }
+    rewrite insert_insert /=.
+    iApply ltyped_let.
+    { iApply ltyped_send. apply lookup_insert.
+      rewrite insert_commute=> //.
+      iApply ltyped_int. }
+    rewrite insert_insert /= (insert_commute _ "v" "c") //.
+    iApply ltyped_recv. apply lookup_insert.
+  Qed.
+
+  Lemma mapper_service_typed Γ :
     ⊢ Γ ⊨ mapper_service : (lty_chan (mapper_service_type) ⊸ (lty_chan END))%lty ⫤ Γ.
   Proof.
     iApply (ltyped_frame _ _ _ _ Γ).
-- 
GitLab