factor out the IO tape effects

_CoqProject

@@ -28,6 +28,13 @@ theories/gitree.v
 
 theories/program_logic.v
 
+theories/effects/store.v
+theories/effects/io_tape.v
+
+theories/lib/pairs.v
+theories/lib/while.v
+theories/lib/factorial.v
+theories/lib/iter.v
 
 theories/examples/delim_lang/lang.v
 theories/examples/delim_lang/interp.v
@@ -47,11 +54,4 @@ theories/examples/affine_lang/lang.v
 theories/examples/affine_lang/logrel1.v
 theories/examples/affine_lang/logrel2.v
 
-theories/effects/store.v
-
-theories/lib/pairs.v
-theories/lib/while.v
-theories/lib/factorial.v
-theories/lib/iter.v
-
 theories/utils/finite_sets.v

theories/effects/io_tape.v

@@ -0,0 +1,144 @@
+(** I/O on a tape effect *)
+From gitrees Require Import prelude gitree.
+
+Record state := State {
+                   inputs : list nat;
+                   outputs : list nat;
+                 }.
+#[export] Instance state_inhabited : Inhabited state := populate (State [] []).
+
+Definition update_input (s : state) : nat * state :=
+  match s.(inputs) with
+  | [] => (0, s)
+  | n::ns =>
+      (n, {| inputs := ns; outputs := s.(outputs) |})
+  end.
+Definition update_output (n:nat) (s : state) : state :=
+  {| inputs := s.(inputs); outputs := n::s.(outputs) |}.
+
+Notation stateO := (leibnizO state).
+
+Program Definition inputE : opInterp :=
+  {|
+    Ins := unitO;
+    Outs := natO;
+  |}.
+
+Program Definition outputE : opInterp :=
+  {|
+    Ins := natO;
+    Outs := unitO;
+  |}.
+
+Definition ioE := @[inputE;outputE].
+
+(* INPUT *)
+Definition reify_input X `{Cofe X} : unitO * stateO →
+                                      option (natO * stateO) :=
+    λ '(o, σ), Some (update_input σ : prodO natO stateO).
+#[export] Instance reify_input_ne X `{Cofe X} :
+  NonExpansive (reify_input X).
+Proof.
+  intros ?[[]][[]][_?]. simpl in *. f_equiv.
+  repeat f_equiv. done.
+Qed.
+
+(* OUTPUT *)
+Definition reify_output X `{Cofe X} : (natO * stateO) →
+                                       option (unitO * stateO) :=
+  λ '(n, σ), Some((), update_output n σ : stateO).
+#[export] Instance reify_output_ne X `{Cofe X} :
+  NonExpansive (reify_output X).
+Proof.
+  intros ?[][][]. simpl in *.
+  repeat f_equiv; done.
+Qed.
+
+Canonical Structure reify_io : sReifier NotCtxDep.
+Proof.
+  simple refine {| sReifier_ops := ioE;
+                   sReifier_state := stateO
+                |}.
+  intros X HX op.
+  destruct op as [[] | [ | []]]; simpl.
+  - simple refine (OfeMor (reify_input X)).
+  - simple refine (OfeMor (reify_output X)).
+Defined.
+
+Section constructors.
+  Context {E : opsInterp} {A} `{!Cofe A}.
+  Context {subEff0 : subEff ioE E}.
+  Context {subOfe0 : SubOfe natO A}.
+  Notation IT := (IT E A).
+  Notation ITV := (ITV E A).
+
+  Program Definition INPUT : (nat -n> IT) -n> IT := λne k, Vis (E:=E) (subEff_opid (inl ()))
+                                                             (subEff_ins (F:=ioE) (op:=(inl ())) ())
+                                                             (NextO ◎ k ◎ (subEff_outs (F:=ioE) (op:=(inl ())))^-1).
+  Solve Obligations with solve_proper.
+  Program Definition OUTPUT_ : nat -n> IT -n> IT :=
+    λne m α, Vis (E:=E) (subEff_opid (inr (inl ())))
+                        (subEff_ins (F:=ioE) (op:=(inr (inl ()))) m)
+                        (λne _, NextO α).
+  Solve All Obligations with solve_proper_please.
+  Program Definition OUTPUT : nat -n> IT := λne m, OUTPUT_ m (Ret 0).
+
+  Lemma hom_INPUT k f `{!IT_hom f} : f (INPUT k) ≡ INPUT (OfeMor f ◎ k).
+  Proof.
+    unfold INPUT.
+    rewrite hom_vis/=. repeat f_equiv.
+    intro x. cbn-[laterO_map]. rewrite laterO_map_Next.
+    done.
+  Qed.
+  Lemma hom_OUTPUT_ m α f `{!IT_hom f} : f (OUTPUT_ m α) ≡ OUTPUT_ m (f α).
+  Proof.
+    unfold OUTPUT.
+    rewrite hom_vis/=. repeat f_equiv.
+    intro x. cbn-[laterO_map]. rewrite laterO_map_Next.
+    done.
+  Qed.
+
+End constructors.
+
+Section weakestpre.
+  Context {sz : nat}.
+  Variable (rs : gReifiers NotCtxDep sz).
+  Context {subR : subReifier reify_io rs}.
+  Notation F := (gReifiers_ops rs).
+  Context {R} `{!Cofe R}.
+  Context `{!SubOfe natO R}.
+  Notation IT := (IT F R).
+  Notation ITV := (ITV F R).
+  Context `{!invGS Σ, !stateG rs R Σ}.
+  Notation iProp := (iProp Σ).
+
+  Lemma wp_input (σ σ' : stateO) (n : nat) (k : natO -n> IT) Φ s :
+    update_input σ = (n, σ') →
+    has_substate σ -∗
+    ▷ (£ 1 -∗ has_substate σ' -∗ WP@{rs} (k n) @ s {{ Φ }}) -∗
+    WP@{rs} (INPUT k) @ s {{ Φ }}.
+  Proof.
+    intros Hs. iIntros "Hs Ha".
+    unfold INPUT. simpl.
+    iApply (wp_subreify_ctx_indep with "Hs").
+    { simpl. rewrite Hs//=. }
+    { simpl. by rewrite ofe_iso_21. }
+    iModIntro. done.
+  Qed.
+
+  Lemma wp_output (σ σ' : stateO) (n : nat) Φ s :
+    update_output n σ = σ' →
+    has_substate σ -∗
+    ▷ (£ 1 -∗ has_substate σ' -∗ Φ (RetV 0)) -∗
+    WP@{rs} (OUTPUT n) @ s {{ Φ }}.
+  Proof.
+    intros Hs. iIntros "Hs Ha".
+    unfold OUTPUT. simpl.
+    iApply (wp_subreify_ctx_indep rs with "Hs").
+    { simpl. by rewrite Hs. }
+    { simpl. done. }
+    iModIntro. iIntros "H1 H2".
+    iApply wp_val. by iApply ("Ha" with "H1 H2").
+  Qed.
+
+End weakestpre.

theories/effects/store.v

@@ -1,3 +1,4 @@
+(** Higher-order store effect *)
 From iris.algebra Require Import gmap excl auth gmap_view.
 From iris.proofmode Require Import classes tactics.
 From iris.base_logic Require Import algebra.

theories/examples/affine_lang/lang.v

@@ -7,7 +7,7 @@ Require Import Binding.Resolver Binding.Lib Binding.Set Binding.Auto Binding.Env
 
 (* for namespace sake *)
 Module io_lang.
-  Definition state := input_lang.lang.state.
+  Definition state := io_tape.state.
   Definition ty := input_lang.lang.ty.
   Definition expr := input_lang.lang.expr.
   Definition tyctx {S : Set} := S → ty.

theories/examples/affine_lang/logrel1.v

@@ -1,7 +1,7 @@
 (** Unary (Kripke) logical relation for the affine lang *)
 From gitrees Require Export gitree program_logic greifiers.
 From gitrees.examples.affine_lang Require Import lang.
-From gitrees.effects Require Import store.
+From gitrees.effects Require Import io_tape store.
 From gitrees.lib Require Import pairs.
 From gitrees.utils Require Import finite_sets.
 
@@ -51,7 +51,7 @@ Section logrel.
   Context {sz : nat}.
   Variable rs : gReifiers NotCtxDep sz.
   Context `{!subReifier reify_store rs}.
-  Context `{!subReifier input_lang.interp.reify_io rs}.
+  Context `{!subReifier reify_io rs}.
   Notation F := (gReifiers_ops rs).
   Context {R} `{!Cofe R}.
   Context `{!SubOfe natO R}.
@@ -516,7 +516,7 @@ Arguments compat_destruct {_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _}.
 Arguments compat_replace {_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _}.
 
 Local Definition rs : gReifiers NotCtxDep 2 :=
-  gReifiers_cons reify_store (gReifiers_cons input_lang.interp.reify_io gReifiers_nil).
+  gReifiers_cons reify_store (gReifiers_cons reify_io gReifiers_nil).
 
 Variable Hdisj : ∀ (Σ : gFunctors) (P Q : iProp Σ), disjunction_property P Q.
 

theories/examples/affine_lang/logrel2.v

@@ -467,7 +467,7 @@ End glue.
 
 Local Definition rs : gReifiers NotCtxDep 2
   := gReifiers_cons reify_store
-       (gReifiers_cons input_lang.interp.reify_io gReifiers_nil).
+       (gReifiers_cons reify_io gReifiers_nil).
 
 Variable Hdisj : ∀ (Σ : gFunctors) (P Q : iProp Σ), disjunction_property P Q.
 

theories/examples/input_lang/interp.v

@@ -1,134 +1,9 @@
 From gitrees Require Import gitree lang_generic.
+From gitrees.effects Require Export io_tape.
 From gitrees.examples.input_lang Require Import lang.
 
 Require Import Binding.Lib Binding.Set.
 
-Notation stateO := (leibnizO state).
-
-Program Definition inputE : opInterp :=
-  {|
-    Ins := unitO;
-    Outs := natO;
-  |}.
-
-Program Definition outputE : opInterp :=
-  {|
-    Ins := natO;
-    Outs := unitO;
-  |}.
-
-Definition ioE := @[inputE;outputE].
-
-(* INPUT *)
-Definition reify_input X `{Cofe X} : unitO * stateO →
-                                      option (natO * stateO) :=
-    λ '(o, σ), Some (update_input σ : prodO natO stateO).
-#[export] Instance reify_input_ne X `{Cofe X} :
-  NonExpansive (reify_input X).
-Proof.
-  intros ?[[]][[]][_?]. simpl in *. f_equiv.
-  repeat f_equiv. done.
-Qed.
-
-(* OUTPUT *)
-Definition reify_output X `{Cofe X} : (natO * stateO) →
-                                       option (unitO * stateO) :=
-  λ '(n, σ), Some((), update_output n σ : stateO).
-#[export] Instance reify_output_ne X `{Cofe X} :
-  NonExpansive (reify_output X).
-Proof.
-  intros ?[][][]. simpl in *.
-  repeat f_equiv; done.
-Qed.
-
-Canonical Structure reify_io : sReifier NotCtxDep.
-Proof.
-  simple refine {| sReifier_ops := ioE;
-                   sReifier_state := stateO
-                |}.
-  intros X HX op.
-  destruct op as [[] | [ | []]]; simpl.
-  - simple refine (OfeMor (reify_input X)).
-  - simple refine (OfeMor (reify_output X)).
-Defined.
-
-Section constructors.
-  Context {E : opsInterp} {A} `{!Cofe A}.
-  Context {subEff0 : subEff ioE E}.
-  Context {subOfe0 : SubOfe natO A}.
-  Notation IT := (IT E A).
-  Notation ITV := (ITV E A).
-
-  Program Definition INPUT : (nat -n> IT) -n> IT := λne k, Vis (E:=E) (subEff_opid (inl ()))
-                                                             (subEff_ins (F:=ioE) (op:=(inl ())) ())
-                                                             (NextO ◎ k ◎ (subEff_outs (F:=ioE) (op:=(inl ())))^-1).
-  Solve Obligations with solve_proper.
-  Program Definition OUTPUT_ : nat -n> IT -n> IT :=
-    λne m α, Vis (E:=E) (subEff_opid (inr (inl ())))
-                        (subEff_ins (F:=ioE) (op:=(inr (inl ()))) m)
-                        (λne _, NextO α).
-  Solve All Obligations with solve_proper_please.
-  Program Definition OUTPUT : nat -n> IT := λne m, OUTPUT_ m (Ret 0).
-
-  Lemma hom_INPUT k f `{!IT_hom f} : f (INPUT k) ≡ INPUT (OfeMor f ◎ k).
-  Proof.
-    unfold INPUT.
-    rewrite hom_vis/=. repeat f_equiv.
-    intro x. cbn-[laterO_map]. rewrite laterO_map_Next.
-    done.
-  Qed.
-  Lemma hom_OUTPUT_ m α f `{!IT_hom f} : f (OUTPUT_ m α) ≡ OUTPUT_ m (f α).
-  Proof.
-    unfold OUTPUT.
-    rewrite hom_vis/=. repeat f_equiv.
-    intro x. cbn-[laterO_map]. rewrite laterO_map_Next.
-    done.
-  Qed.
-
-End constructors.
-
-Section weakestpre.
-  Context {sz : nat}.
-  Variable (rs : gReifiers NotCtxDep sz).
-  Context {subR : subReifier reify_io rs}.
-  Notation F := (gReifiers_ops rs).
-  Context {R} `{!Cofe R}.
-  Context `{!SubOfe natO R}.
-  Notation IT := (IT F R).
-  Notation ITV := (ITV F R).
-  Context `{!invGS Σ, !stateG rs R Σ}.
-  Notation iProp := (iProp Σ).
-
-  Lemma wp_input (σ σ' : stateO) (n : nat) (k : natO -n> IT) Φ s :
-    update_input σ = (n, σ') →
-    has_substate σ -∗
-    ▷ (£ 1 -∗ has_substate σ' -∗ WP@{rs} (k n) @ s {{ Φ }}) -∗
-    WP@{rs} (INPUT k) @ s {{ Φ }}.
-  Proof.
-    intros Hs. iIntros "Hs Ha".
-    unfold INPUT. simpl.
-    iApply (wp_subreify_ctx_indep with "Hs").
-    { simpl. rewrite Hs//=. }
-    { simpl. by rewrite ofe_iso_21. }
-    iModIntro. done.
-  Qed.
-
-  Lemma wp_output (σ σ' : stateO) (n : nat) Φ s :
-    update_output n σ = σ' →
-    has_substate σ -∗
-    ▷ (£ 1 -∗ has_substate σ' -∗ Φ (RetV 0)) -∗
-    WP@{rs} (OUTPUT n) @ s {{ Φ }}.
-  Proof.
-    intros Hs. iIntros "Hs Ha".
-    unfold OUTPUT. simpl.
-    iApply (wp_subreify_ctx_indep rs with "Hs").
-    { simpl. by rewrite Hs. }
-    { simpl. done. }
-    iModIntro. iIntros "H1 H2".
-    iApply wp_val. by iApply ("Ha" with "H1 H2").
-  Qed.
-
-End weakestpre.
 
 Section interp.
   Context {sz : nat}.

theories/examples/input_lang/lang.v

@@ -1,4 +1,4 @@
-From gitrees Require Export prelude.
+From gitrees Require Export prelude effects.io_tape.
 Require Import Binding.Resolver Binding.Lib Binding.Set Binding.Auto Binding.Env.
 
 
@@ -281,21 +281,6 @@ Qed.
 
 (*** Operational semantics *)
 
-Record state := State {
-                   inputs : list nat;
-                   outputs : list nat;
-                 }.
-#[export] Instance state_inhabited : Inhabited state := populate (State [] []).
-
-Definition update_input (s : state) : nat * state :=
-  match s.(inputs) with
-  | [] => (0, s)
-  | n::ns =>
-      (n, {| inputs := ns; outputs := s.(outputs) |})
-  end.
-Definition update_output (n:nat) (s : state) : state :=
-  {| inputs := s.(inputs); outputs := n::s.(outputs) |}.
-
 Inductive head_step {S} : expr S → state → expr S → state → nat*nat → Prop :=
 | BetaS e1 v2 σ :
   head_step (App (Val $ RecV e1) (Val v2)) σ (subst (Inc := inc) ((subst (F := expr) (Inc := inc) e1) (Val (shift (Inc := inc) v2))) (Val (RecV e1))) σ (1,0)

theories/examples/input_lang_callcc/hom.v

@@ -9,7 +9,8 @@ Open Scope stdpp_scope.
 Section hom.
   Context {sz : nat}.
   Context {rs : gReifiers CtxDep sz}.
-  Context {subR : subReifier reify_io rs}.
+  Context `{!subReifier reify_cont rs}.
+  Context `{!subReifier (sReifier_NotCtxDep_CtxDep reify_io) rs}.
   Notation F := (gReifiers_ops rs).
   Notation IT := (IT F natO).
   Notation ITV := (ITV F natO).