Merge branch 'delim_staging' of github.com:logsem/gitrees into delim_…

…staging

README.md

@@ -30,7 +30,7 @@ to the code structure.
 - `examples/input_lang/` -- formalization of the language with io, the soundness and adequacy
 - `examples/affine_lang/` -- formalization of the affine language, type safety of the language interoperability
 - `examples/input_lang_callcc/` -- formalization of the language with io, throw and call/cc, the soundness and adequacy
-- `examples/delim_lang/` -- formalization shift/reset effects, of a language with delimited continuations and its soundness
+- `examples/delim_lang/` -- formalization of the language with shift/reset and its soundness/adequacy wrt abstract machine semantics
 - `prelude.v` -- some stuff that is missing from Iris
 - `lang_generic.v` -- generic facts about languages with binders and their interpretations, shared by `input_lang` and `affine_lang`
 

theories/effects/delim.v

@@ -1,3 +1,4 @@
+(** * Representation of delimited continuations *)
 From gitrees Require Import prelude gitree.
 From iris.algebra Require Import list.
 
@@ -14,26 +15,29 @@ Proof. apply _. Qed.
 
 (** * Signatures *)
 
+(** Bind the innermost continuation *)
 Program Definition shiftE : opInterp :=
   {|
     Ins := ((▶ ∙ -n> ▶ ∙) -n> ▶ ∙);
     Outs := (▶ ∙);
   |}.
 
+(** Delimit the continuation *)
 Program Definition resetE : opInterp :=
   {|
     Ins := (▶ ∙);
     Outs := (▶ ∙);
   |}.
 
-(* to apply the head of the meta continuation *)
+(** Explicitly pop a continuation from the meta-continuation and jump
+to it *)
 Program Definition popE : opInterp :=
   {|
     Ins := (▶ ∙);
     Outs := Empty_setO;
   |}.
 
-(* apply continuation, pushes outer context in meta *)
+(** Applies continuation, pushes outer context in meta *)
 Program Definition appContE : opInterp :=
   {|
     Ins := (▶ ∙ * (▶ (∙ -n> ∙)));

theories/effects/io_tape.v

@@ -1,4 +1,4 @@
-(** I/O on a tape effect *)
+(** * I/O on a tape effect *)
 From gitrees Require Import prelude gitree.
 
 Record state := State {

theories/examples/delim_lang/example.v

@@ -1,3 +1,4 @@
+(** * Example of a program in delim_lang and its symbolic execution *)
 From gitrees Require Import gitree lang_generic.
 From gitrees.effects Require Import delim.
 From gitrees.examples.delim_lang Require Import lang interp.
@@ -6,6 +7,8 @@ From iris.base_logic Require Import algebra.
 
 Open Scope syn_scope.
 
+(** The program captures the inner continuation, invokes it with 5 and
+6, and adds the results to 1. The result is 1+(3+5)+(3+6)=18 *)
 Example p : expr Empty_set :=
   ((#1) + (reset ((#3) + (shift/cc ((($0) @k #5) + (($0) @k #6)))))).
 

theories/examples/delim_lang/hom.v

@@ -16,6 +16,11 @@ Section hom.
   Notation IT := (IT F R).
   Notation ITV := (ITV F R).
 
+  Program Definition 𝒫_HOM : HOM (A:=natO) := exist _ 𝒫 _.
+  Next Obligation.
+    apply _.
+  Qed.
+
   Program Definition AppContRSCtx_HOM {S : Set}
     (α : @interp_scope F R _ S -n> IT)
     (env : @interp_scope F R _ S)
@@ -32,10 +37,7 @@ Section hom.
   Next Obligation.
     intros; simpl.
     simple refine (IT_HOM _ _ _ _ _); intros; simpl.
-    - intros ???.
-      do 2 f_equiv.
-      intros ?; simpl.
-      solve_proper.
+    - solve_proper_please.
     - rewrite get_val_ITV.
       rewrite get_val_ITV.
       simpl.

theories/examples/delim_lang/interp.v

@@ -1,3 +1,4 @@
+(** Interpretation of delim_lang into gitrees *)
 From gitrees Require Import gitree lang_generic.
 From gitrees.effects Require Import delim.
 From gitrees.examples.delim_lang Require Import lang.
@@ -762,7 +763,7 @@ Section interp.
       trans (reify (gReifiers_sReifier rs)
                (APP_CONT_ (Next (interp_val v env))
                   fin kk)
-            (gState_recomp σr (sR_state (σ)))).
+            (gState_recomp σr (sR_state σ))).
       {
         repeat f_equiv. rewrite get_val_ITV. simpl. rewrite get_fun_fun. simpl.
         rewrite !hom_vis. f_equiv. subst kk. rewrite ccompose_id_l. intro. simpl.

theories/examples/delim_lang/lang.v

@@ -1,3 +1,8 @@
+(** * delim-lang: a language with shift/reset and the abstract machine semantics
+
+Based on Malgorzata Biernacka; Dariusz Biernacki; Olivier Danvy
+An Operational Foundation for Delimited Continuations in the CPS Hierarchy
+ *)
 From gitrees Require Export prelude.
 From stdpp Require Import gmap.
 Require Import Binding.Resolver Binding.Lib Binding.Set Binding.Auto Binding.Env.

theories/examples/delim_lang/logpred.v

@@ -213,11 +213,6 @@ Section logrel.
     iApply "H".
   Qed.
 
-  Program Definition 𝒫_HOM : @HOM sz CtxDep R _ rs := exist _ 𝒫 _.
-  Next Obligation.
-    apply _.
-  Qed.
-
   Lemma compat_shift {S : Set} (Γ : S -> ty) e σ α τ β :
     ⊢ valid (Γ ▹ (Tcont τ α)) e σ σ β -∗ valid Γ (interp_shift _ e) τ α β.
   Proof.

theories/examples/delim_lang/logrel.v

@@ -52,6 +52,15 @@ Section logrel.
   Solve All Obligations with solve_proper.
   Fail Next Obligation.
 
+  (** The configuration of the abstract machine (e, k, m) corresponds
+   to the "denotational configuration" tuple (t, κ, σ).
+
+   The meta-continuation is stored in the state and the top-level
+   current continuation is explicitly invoked.
+
+   At the top-level the refinement is explicitly about fully-evaluated
+   terms which compute to natural numbers. *)
+
   Definition obs_ref' {S : Set}
     (t : IT) (κ : HOM) (σ : stateF ♯ IT)
     (e : exprO S) (k : contO S) (m : mcontO S)
@@ -77,11 +86,8 @@ Section logrel.
                      -n> exprO S -n> contO S -n> mcontO S -n> iProp :=
     λne x y z a b c, obs_ref' x y z a b c.
   Solve All Obligations with try solve_proper.
-  Next Obligation.
-    intros.
-    intros ????????; simpl.
-    solve_proper.
-  Qed.
+  Next Obligation. solve_proper_please. Qed.
+
 
   Definition logrel_mcont' {S : Set}
     (P : ITV -n> valO S -n> iProp) (F : stateF ♯ IT) (m : mcontO S) :=
@@ -196,14 +202,7 @@ Section logrel.
                     -∗ ∀ F F', logrel_mcont δ F F'
                             -∗ obs_ref e E F e' E' F')%I.
   Solve All Obligations with try solve_proper.
-  Next Obligation.
-    intros; intros ????; simpl.
-    do 2 (f_equiv; intro; simpl).
-    f_equiv.
-    do 2 (f_equiv; intro; simpl).
-    f_equiv.
-    solve_proper.
-  Qed.
+  Next Obligation. solve_proper_please. Qed.
 
   Definition logrel {S : Set} (τ α β : ty) : IT -n> exprO S -n> iProp
     := logrel_expr (interp_ty τ) (interp_ty α) (interp_ty β).
@@ -219,7 +218,7 @@ Section logrel.
     (e' : exprO S)
     (τ α σ : ty) : iProp :=
     (□ ∀ γ (γ' : S [⇒] Empty_set), ssubst_valid Γ γ γ'
-          -∗ @logrel Empty_set τ α σ (e γ) (bind (F := expr) γ' e'))%I.
+          -∗ logrel τ α σ (e γ) (bind (F := expr) γ' e'))%I.
 
   Lemma compat_HOM_id {S : Set} P :
     ⊢ @logrel_ectx S P P HOM_id END.
@@ -315,11 +314,6 @@ Section logrel.
     assumption.
   Qed.
 
-  Program Definition 𝒫_HOM : @HOM sz CtxDep R _ rs := exist _ 𝒫 _.
-  Next Obligation.
-    apply _.
-  Qed.
-
   Lemma compat_shift {S : Set} (Γ : S -> ty) e (e' : exprO (inc S)) σ α τ β :
     ⊢ valid (Γ ▹ (τ ⤑ α)) e e' σ σ β -∗ valid Γ (interp_shift _ e) (shift/cc e') τ α β.
   Proof.

theories/examples/delim_lang/typing.v

@@ -1,3 +1,8 @@
+(** * Type sytem for delim-lang
+
+The system is based on
+ O. Danvy and A. Filinski. A functional abstraction of typed contexts.
+*)
 From gitrees.examples.delim_lang Require Import lang.
 
 Require Import Binding.Lib Binding.Set Binding.Env.

theories/examples/input_lang_callcc/hom.v

@@ -1,5 +1,4 @@
-(** In this module, we package up IT homomorphism in a sigma type, and
-we will use it as a domain for logical relations on continuations *)
+(** Particular homomorphisms for the call/cc lang *)
 From gitrees Require Import gitree lang_generic.
 From gitrees Require Export hom.
 From gitrees.examples.input_lang_callcc Require Import lang interp.
@@ -74,8 +73,8 @@ Section hom.
   Qed.
 
   Program Definition OutputSCtx_HOM {S : Set}
-    (env : @interp_scope F A _ S)
-    : @HOM _ _ A _ _ := exist _ ((interp_outputk rs (λne env, idfun) env)) _.
+    (env : @interp_scope F A _ S) : HOM (A:=natO)
+    := exist _ ((interp_outputk rs (λne env, idfun) env)) _.
   Next Obligation.
     intros; simpl.
     apply _.

theories/hom.v

@@ -1,15 +1,14 @@
+(** In this module, we package up IT homomorphism in a sigma type, and
+we will use it as a domain for logical relations on continuations *)
 From gitrees Require Import gitree lang_generic.
 Require Import Binding.Lib Binding.Set Binding.Env.
 
 Open Scope stdpp_scope.
 
 Section hom.
-  Context {sz : nat}.
-  Context {a : is_ctx_dep}.
   Context {A : ofe}.
   Context {CA : Cofe A}.
-  Context {rs : gReifiers a sz}.
-  Notation F := (gReifiers_ops rs).
+  Context {F : opsInterp}.
   Notation IT := (IT F A).
   Notation ITV := (ITV F A).