From e1c2b252a91dabe62e735b52641413178fb3e94f Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Thu, 4 Jun 2020 15:18:54 +0200
Subject: [PATCH] Mapper example

---
 theories/logrel/examples/mapper.v | 43 +++++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)
 create mode 100644 theories/logrel/examples/mapper.v

diff --git a/theories/logrel/examples/mapper.v b/theories/logrel/examples/mapper.v
new file mode 100644
index 0000000..e33c44d
--- /dev/null
+++ b/theories/logrel/examples/mapper.v
@@ -0,0 +1,43 @@
+From actris.channel Require Import proofmode proto channel.
+From actris.logrel Require Import subtyping_rules term_typing_judgment term_typing_rules environments.
+From iris.proofmode Require Import tactics.
+
+Section with_Σ.
+  Context `{heapG Σ, chanG Σ}.
+
+  Definition mapper_service_type : lsty Σ :=
+    <??> TY (lty_int ⊸ lty_bool); <??> TY lty_int; <!!> TY lty_bool; END.
+
+  Definition mapper_service : expr := λ: "c",
+    let: "f" := recv "c" in
+    let: "v" := recv "c" in
+    send "c" ("f" "v");; "c".
+
+  Lemma mapper_typed :
+    ⊢ ∅ ⊨ mapper_service : (lty_chan (mapper_service_type) ⊸ (lty_chan END))%lty ⫤ ∅.
+  Proof.
+    iApply ltyped_lam.
+    iApply ltyped_let.
+    { iApply ltyped_recv. by rewrite lookup_insert. }
+    rewrite insert_insert /=.
+    iApply ltyped_let.
+    { iApply ltyped_recv. by rewrite insert_commute // lookup_insert. }
+    rewrite (insert_commute _ "c" "f") // insert_insert.
+    iApply (ltyped_let _ (<["c":= lty_chan END]>_))=> /=; last first.
+    { iApply ltyped_var. apply lookup_insert. }
+    rewrite (insert_commute _ "f" "c") // (insert_commute _ "v" "c") //.
+    iApply ltyped_send. apply lookup_insert.
+    iApply (ltyped_frame _ _ _ _ {["c":=_]}).
+    { iApply env_split_right=> //. iApply env_split_id_r. }
+    { iApply env_split_right=> //. shelve. iApply env_split_id_r. }
+    iApply ltyped_app.
+    - iApply ltyped_var. apply lookup_insert.
+    - rewrite insert_commute //.
+      iApply (ltyped_frame _ _ _ _ {["f":=_]}).
+      { iApply env_split_right=> //. iApply env_split_id_r. }
+      { iApply env_split_right=> //. shelve. iApply env_split_id_r. }
+      iApply ltyped_var. apply lookup_insert.
+      Unshelve. eauto. eauto.
+  Qed.
+
+End with_Σ.
-- 
GitLab