Delimited continuations

.gitignore

@@ -19,7 +19,7 @@
 # these rules might exclude image files for figures etc.
 # *.ps
 # *.eps
-*.pdf
+# *.pdf
 
 ## Generated if empty string is given at "Please type another file name for output:"
 .pdf

_CoqProject

@@ -38,6 +38,7 @@ theories/lib/iter.v
 
 theories/examples/delim_lang/lang.v
 theories/examples/delim_lang/interp.v
+theories/examples/delim_lang/tactics.v
 theories/examples/delim_lang/example.v
 
 theories/examples/input_lang_callcc/lang.v

notes/notes.org

@@ -0,0 +1,36 @@
+* what is done
+extension of reifiers in GITrees to allow to access continuation
+** language with call/cc + throw :
+- operational
+- interpretation into gitrees
+  - untyped terms
+- type system
+- soundness + adequacy (using logrel)
+  - soundness untyped
+  - adequacy typed
+- wp rules (for call/cc throw)
+  - used to prove adequacy/define logrel
+** delimited continuations
+- abstract machine operational sem
+- interpretation into gitrees
+  - untyped terms
+- soundness
+- wp rules (for shift/reset)
+  - used to prove a small example
+- some sketch of a type system
+  from [[https://www.tilk.eu/shift0/materzok-biernacki-icfp11.pdf][Subtyping Delimited Continuations]]
+
+* what's next?
+
+** TODO adequacy for shift/reset?
+- defining logical relation using a type system?
+  - [ ] type system
+  - [ ] logrel
+- OR untyped relation between confiugrations and
+  tree state
+  - [ ] relation
+
+** TODO more concrete example for shift/reset
+
+** TODO example on language interaction w/ continuations
+for example between λ_call/cc & a WHILE language w/ long jumps?

theories/examples/delim_lang/example.v

@@ -1,16 +1,14 @@
 From gitrees Require Import gitree lang_generic.
-From gitrees.examples.delim_lang Require Import lang interp.
+From gitrees.examples.delim_lang Require Import lang interp tactics.
 From iris.proofmode Require Import base classes tactics environments.
 From iris.base_logic Require Import algebra.
 
 Open Scope syn_scope.
 
 Example p : expr Empty_set :=
-  ((#1) + (reset ((#3) + (shift/cc ((($0) @k #5) + (($0) @k #6)))))).
+  ((#7) + (reset ((#7) * (shift/cc ((($0) @k #2) + (($0) @k #3)))))).
 
 Local Definition rs : gReifiers _ _ := gReifiers_cons reify_delim gReifiers_nil.
-(* Local Definition Hrs : subReifier reify_delim rs. *)
-(* Proof. unfold rs. apply subReifier_here. Qed. *)
 
 Notation F := (gReifiers_ops rs).
 Context {R} `{!Cofe R}.
@@ -28,81 +26,52 @@ Context `{!invGS Σ, !stateG rs R Σ, !heapG rs R Σ}.
 Notation iProp := (iProp Σ).
 
 
-Ltac shift_hom :=
-  match goal with
-  | |- envs_entails _ (wp _ (ofe_mor_car _ _ (λne x, ?k1 x) (?k2 ?t)) _ _ _) =>
-      assert ((ofe_mor_car _ _ (λne x, k1 x) (k2 t)) ≡ (λne x, k1 (k2 x)) t) as -> by done
-  | |- envs_entails _ (wp _ (?k ?t) _ _ _) =>
-      assert (k t ≡ (λne x, k x) t) as -> by done
-  end.
-
-Ltac shift_natop_l :=
-  match goal with
-  | |- envs_entails _ (wp _ (ofe_mor_car _ _ (λne x, ?k1 x)
-                               (ofe_mor_car _ _
-                                  (ofe_mor_car _ _
-                                     (NATOP (do_natop lang.Add)) ?t) (IT_of_V ?e))) _ _ _) =>
-      assert ((ofe_mor_car _ _ (λne x, k1 x) (NATOP (do_natop lang.Add) t (IT_of_V e))) ≡
-                (λne x, k1 (NATOP (do_natop lang.Add) x (IT_of_V e))) t) as -> by done
-  end.
-
 Lemma wp_t (s : gitree.weakestpre.stuckness) :
   has_substate σ -∗
-  WP@{rs} t @ s {{βv, βv ≡ RetV 18}}.
+  WP@{rs} t @ s {{βv, βv ≡ RetV 42}}.
 Proof.
   Opaque SHIFT APP_CONT.
   iIntros "Hσ".
   cbn.
   (* first, reset *)
-  do 2 shift_hom.
+  do 2 wp_ctx.
   iApply (wp_reset with "Hσ").
   iIntros "!> _ Hσ". simpl.
 
   (* then, shift *)
-  do 2 shift_hom.
-  iApply (wp_shift with "Hσ").
-  { rewrite laterO_map_Next. done. }
-  iIntros "!>_ Hσ".
-  simpl.
+  do 2 wp_ctx.
+  iApply (wp_shift with "Hσ"); first by rewrite laterO_map_Next.
+  iIntros "!>_ Hσ". simpl.
 
   (* the rest *)
-  rewrite -(IT_of_V_Ret 6) get_val_ITV'. simpl.
+  rewrite (get_val_ret _ 3). simpl.
   rewrite get_fun_fun. simpl.
-  do 2 shift_hom.
+  do 2 wp_ctx.
   iApply (wp_app_cont with "Hσ"); first done.
   iIntros "!> _ Hσ". simpl.
+
   rewrite later_map_Next -Tick_eq.
   iApply wp_tick. iNext.
-  shift_hom.
-  rewrite IT_of_V_Ret NATOP_Ret. simpl.
-  rewrite -(IT_of_V_Ret 9).
+  rewrite NATOP_Ret. simpl.
   iApply (wp_pop_cons with "Hσ").
-  iIntros "!> _ Hσ".
-  simpl.
+  iIntros "!> _ Hσ". simpl.
 
-  shift_hom. shift_natop_l.
-  rewrite -(IT_of_V_Ret 5) get_val_ITV'. simpl.
-  shift_hom. shift_natop_l.
-  rewrite get_fun_fun. simpl.
-  shift_hom. shift_natop_l.
+  do 2 wp_ctx. name_ctx k.                    (* so that it does't simpl *)
+  rewrite (get_val_ret _ 2). simpl.
+  rewrite get_fun_fun. simpl. subst k.
   iApply (wp_app_cont with "Hσ"); first done.
   iIntros "!> _ Hσ". simpl.
+
   rewrite later_map_Next -Tick_eq.
   iApply wp_tick. iNext.
-  rewrite (IT_of_V_Ret 5) NATOP_Ret. simpl.
-  rewrite -(IT_of_V_Ret 8).
+  rewrite NATOP_Ret. simpl.
   iApply (wp_pop_cons with "Hσ").
-  iIntros "!> _ Hσ".
-  simpl.
-  shift_hom.
-  shift_natop_l.
-  rewrite (IT_of_V_Ret 8).
-  simpl. rewrite IT_of_V_Ret NATOP_Ret.
-  simpl. rewrite -(IT_of_V_Ret 17).
+  iIntros "!> _ Hσ". simpl.
+
+  rewrite NATOP_Ret. simpl.
   iApply (wp_pop_cons with "Hσ").
   iIntros "!> _ Hσ". simpl.
-  rewrite IT_of_V_Ret NATOP_Ret.
-  simpl. rewrite -(IT_of_V_Ret 18).
+  rewrite NATOP_Ret. simpl.
   iApply (wp_pop_end with "Hσ").
   iIntros "!> _ _".
   iApply wp_val. done.

theories/examples/delim_lang/interp.v

@@ -57,8 +57,6 @@ Notation op_reset := (inr (inl ())).
 Notation op_pop := (inr (inr (inl ()))).
 Notation op_app_cont := (inr (inr (inr (inl ())))).
 
-
-
 Section reifiers.
 
   Context {X} `{!Cofe X}.
@@ -262,30 +260,29 @@ Section weakestpre.
     - iApply "Ha".
   Qed.
 
-  (** XXX: Formulate the rules using AsVal *)
-  Lemma wp_pop_end (v : ITV)
+  Lemma wp_pop_end (e : IT) `{!AsVal e}
     Φ s :
     has_substate [] -∗
-    ▷ (£ 1 -∗ has_substate [] -∗ WP@{rs} IT_of_V v @ s {{ Φ }}) -∗
-    WP@{rs} 𝒫 (IT_of_V v) @ s {{ Φ }}.
+    ▷ (£ 1 -∗ has_substate [] -∗ WP@{rs} e @ s {{ Φ }}) -∗
+    WP@{rs} 𝒫 e @ s {{ Φ }}.
   Proof.
     iIntros "Hs Ha".
     rewrite get_val_ITV. simpl.
-    iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ ((Next $ IT_of_V v)) with "Hs").
+    iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ ((Next $ e)) with "Hs").
     - simpl. reflexivity.
     - reflexivity.
     - done.
   Qed.
 
-  Lemma wp_pop_cons (σ : state) (v : ITV) (k : IT -n> IT)
+  Lemma wp_pop_cons (σ : state) (e : IT) `{!AsVal e} (k : IT -n> IT)
     Φ s :
     has_substate ((laterO_map k) :: σ) -∗
-    ▷ (£ 1 -∗ has_substate σ -∗ WP@{rs} k $ IT_of_V v @ s {{ Φ }}) -∗
-    WP@{rs} 𝒫 (IT_of_V v) @ s {{ Φ }}.
+    ▷ (£ 1 -∗ has_substate σ -∗ WP@{rs} k e @ s {{ Φ }}) -∗
+    WP@{rs} 𝒫 e @ s {{ Φ }}.
   Proof.
     iIntros "Hs Ha".
     rewrite get_val_ITV. simpl.
-    iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ ((laterO_map k (Next $ IT_of_V v))) with "Hs").
+    iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ ((laterO_map k (Next e))) with "Hs").
     - simpl. reflexivity.
     - reflexivity.
     - done.