From 3154feeeb7fb667af91d50053bbf89207413e79a Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 24 Apr 2018 22:10:34 +0200
Subject: [PATCH] cont.v
---
_CoqProject | 1 +
theories/typing/cont.v | 58 ++++++++++++++++++++++++++++++++++++++++++
2 files changed, 59 insertions(+)
create mode 100644 theories/typing/cont.v
diff --git a/_CoqProject b/_CoqProject
index 01846539..daf46408 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -37,3 +37,4 @@ theories/typing/borrow.v
theories/typing/product_split.v
theories/typing/type_sum.v
theories/typing/fixpoint.v
+theories/typing/cont.v
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
new file mode 100644
index 00000000..639f0a55
--- /dev/null
+++ b/theories/typing/cont.v
@@ -0,0 +1,58 @@
+From lrust.typing Require Export type.
+From lrust.typing Require Import programs.
+Set Default Proof Using "Type".
+
+Section typing.
+ Context `{typeG Σ}.
+
+ (** Jumping to and defining a continuation. *)
+ Lemma type_jump args argsv E L C T k T' :
+ (* We use this rather complicated way to state that
+ args = of_val <$> argsv, only because then solve_typing
+ is able to prove it easily. *)
+ Forall2 (λ a av, to_val a = Some av ∨ a = of_val av) args argsv →
+ k ◁cont(L, T') ∈ C →
+ tctx_incl E L T (T' (list_to_vec argsv)) →
+ typed_body E L C T (k args).
+ Proof.
+ iIntros (Hargs HC Hincl tid) "#LFT #HE Hna HL HC HT".
+ iMod (Hincl with "[LFT //] HE HL HT") as "(HL & HT)".
+ iSpecialize ("HC" with "[]"); first done.
+ assert (args = of_val <$> argsv) as ->.
+ { clear -Hargs. induction Hargs as [|a av ?? [<-%of_to_val| ->] _ ->]=>//=. }
+ rewrite -{3}(vec_to_list_of_list argsv). iApply ("HC" with "Hna HL HT").
+ Qed.
+
+ Lemma type_cont argsb L1 (T' : vec val (length argsb) → _) E L2 C T econt e2 kb :
+ Closed (kb :b: argsb +b+ []) econt → Closed (kb :b: []) e2 →
+ (∀ k, typed_body E L2 (k ◁cont(L1, T') :: C) T (subst' kb k e2)) -∗
+ □ (∀ k (args : vec val (length argsb)),
+ typed_body E L1 (k ◁cont(L1, T') :: C) (T' args)
+ (subst_v (kb::argsb) (k:::args) econt)) -∗
+ typed_body E L2 C T (letcont: kb argsb := econt in e2).
+ Proof.
+ iIntros (Hc1 Hc2) "He2 #Hecont". iIntros (tid) "#LFT #HE Htl HL HC HT".
+ rewrite (_ : (rec: kb argsb := econt)%E = of_val (rec: kb argsb := econt)%V); last by unlock.
+ wp_let. iApply ("He2" with "LFT HE Htl HL [HC] HT").
+ iLöb as "IH". iIntros (x) "H".
+ iDestruct "H" as %[->|?]%elem_of_cons; last by iApply "HC".
+ iIntros (args) "Htl HL HT". wp_rec.
+ iApply ("Hecont" with "LFT HE Htl HL [HC] HT"). by iApply "IH".
+ Qed.
+
+ Lemma type_cont_norec argsb L1 (T' : vec val (length argsb) → _) E L2 C T econt e2 kb :
+ Closed (kb :b: argsb +b+ []) econt → Closed (kb :b: []) e2 →
+ (∀ k, typed_body E L2 (k ◁cont(L1, T') :: C) T (subst' kb k e2)) -∗
+ (∀ k (args : vec val (length argsb)),
+ typed_body E L1 C (T' args) (subst_v (kb :: argsb) (k:::args) econt)) -∗
+ typed_body E L2 C T (letcont: kb argsb := econt in e2).
+ Proof.
+ iIntros (Hc1 Hc2) "He2 Hecont". iIntros (tid) "#LFT #HE Htl HL HC HT".
+ rewrite (_ : (rec: kb argsb := econt)%E = of_val (rec: kb argsb := econt)%V); last by unlock.
+ wp_let. iApply ("He2" with "LFT HE Htl HL [HC Hecont] HT").
+ iIntros (x) "H".
+ iDestruct "H" as %[->|?]%elem_of_cons; last by iApply "HC".
+ iIntros (args) "Htl HL HT". wp_rec.
+ iApply ("Hecont" with "LFT HE Htl HL HC HT").
+ Qed.
+End typing.
--
GitLab