From c6253c6e70b5dc9f089a504356c415cb4fe94e14 Mon Sep 17 00:00:00 2001
From: jihgfee <jkas@itu.dk>
Date: Sun, 30 Jun 2019 16:53:10 +0200
Subject: [PATCH] Updated list sort elem with top-level to receive comparison
 function

---
 theories/examples/list_sort_elem.v | 29 ++++++++++++++++++++++++++++-
 1 file changed, 28 insertions(+), 1 deletion(-)

diff --git a/theories/examples/list_sort_elem.v b/theories/examples/list_sort_elem.v
index 3152d73..c342dc9 100644
--- a/theories/examples/list_sort_elem.v
+++ b/theories/examples/list_sort_elem.v
@@ -47,8 +47,16 @@ Definition list_sort_elem_service : val :=
     let: "x" := (if: recv "c1" then recv "c1" else assert #false) in
     list_sort_elem_service_merge "cmp" "c" "x" "c1" "c2".
 
+Definition list_sort_elem_service_top : val :=
+  λ: "c",
+    let: "cmp" := recv "c" in
+    list_sort_elem_service "cmp" "c".
+
+
 Section list_sort_elem.
   Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
+
+  Section list_sort_elem_inner.
   Context {A} (I : A → val → iProp Σ) (R : relation A) `{!RelDecision R, !Total R}.
 
   Definition tail_protocol_aux (xs : list (A * val))
@@ -78,7 +86,7 @@ Section list_sort_elem.
   Proof. apply proto_unfold_eq, (fixpoint_unfold head_protocol_aux). Qed.
 
   Definition list_sort_elem_protocol : iProto Σ := head_protocol [].
-
+  
   Lemma list_sort_elem_service_split_spec c c1 c2 xs xs1 xs2 :
     {{{
       c ↣ iProto_dual (head_protocol xs) @ N ∗ 
@@ -211,4 +219,23 @@ Section list_sort_elem.
         by wp_apply (select_spec with "[$Hc]").
     - by wp_apply (select_spec with "[$Hc]").
   Qed.
+  End list_sort_elem_inner.
+
+  Definition list_sort_elem_top_protocol : iProto Σ :=
+    (<!> A (I : A → val → iProp Σ) (R : A → A → Prop)
+         `{!RelDecision R, !Total R} (cmp : val),
+       MSG cmp {{ cmp_spec I R cmp }};
+     head_protocol I R [])%proto.
+
+  Lemma list_sort_elem_service_top_spec c :
+    {{{ c ↣ iProto_dual list_sort_elem_top_protocol @ N }}}
+      list_sort_elem_service_top c
+    {{{ RET #(); c ↣ END @ N }}}.
+  Proof.
+    iIntros (Ψ) "Hc HΨ".
+    wp_lam.
+    wp_recv (? I R ? ? cmp) as "#Hcmp".
+    wp_apply (list_sort_elem_service_spec with "Hcmp Hc")=> //.
+  Qed.
+
 End list_sort_elem.
-- 
GitLab