From 3bf41e484bd651068bd0dc93d1e3ca7b72d955e8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 11 Feb 2017 12:00:53 +0100
Subject: [PATCH] type the join function
---
theories/typing/unsafe/spawn.v | 24 ++++++++++++++++++++++++
1 file changed, 24 insertions(+)
diff --git a/theories/typing/unsafe/spawn.v b/theories/typing/unsafe/spawn.v
index fcb84daa..faebd070 100644
--- a/theories/typing/unsafe/spawn.v
+++ b/theories/typing/unsafe/spawn.v
@@ -89,4 +89,28 @@ Section spawn.
eapply type_delete; [solve_typing..|].
eapply (type_jump [_]); solve_typing.
Qed.
+
+ Definition join : val :=
+ funrec: <> ["c"] :=
+ let: "c'" := !"c" in
+ let: "r" := join ["c'"] in
+ delete [ #1; "c"];; "return" ["r"].
+
+ Lemma join_type retty :
+ typed_instruction_ty [] [] [] join
+ (fn([]; join_handle retty) → retty).
+ Proof.
+ eapply type_fn; [solve_typing..|]=>- _ ret /= arg. inv_vec arg=>c. simpl_subst.
+ eapply type_deref; [solve_typing..|exact: read_own_move|done|]. move=>c'; simpl_subst.
+ eapply type_let with (T1 := [c' â— _]%TC)
+ (T2 := λ r, [r ◠box retty]%TC); try solve_typing; [|].
+ { iAlways. iIntros (tid qE) "#LFT $ $ $".
+ rewrite tctx_interp_singleton tctx_hasty_val. iIntros "Hc'".
+ destruct c' as [[|c'|]|]; try by iDestruct "Hc'" as "[]".
+ iApply (join_spec with "Hc'"). iIntros "!> * Hret".
+ rewrite tctx_interp_singleton tctx_hasty_val. auto. }
+ move=>r; simpl_subst.
+ eapply type_delete; [solve_typing..|].
+ eapply (type_jump [_]); solve_typing.
+ Qed.
End spawn.
--
GitLab