separate crun out of MonadTypedStore (#138)

* separate MonadTypedStore into MonadTypedStore (without crun) and MonadTypedStoreRun

* generalize some lemmas in typed_store_lib.v

* finer sectioning in example_typed_store

example_typed_store.v

@@ -87,6 +87,9 @@ HB.instance Definition _ := @isML_universe.Build ml_type coq_type_nat ml_unit va
 Definition typedStoreMonad (N : monad) :=
   typedStoreMonad ml_type N monad_model.locT_nat.
 
+Definition typedStoreRunMonad (N : monad) :=
+  typedStoreRunMonad ml_type N monad_model.locT_nat.
+
 Section cyclic.
 Variables (N : monad) (M : typedStoreMonad N).
 
@@ -105,19 +108,6 @@ Definition rhd (T : ml_type) (def : coq_type N T)
   (param : loc (ml_rlist T)) : M (coq_type N T) :=
   do v <- cget param; Ret (match v with Nil => def | Cons a _ => a end).
 
-Lemma rhd_is_true :
-  crun (do l <- cycle ml_bool true false; rhd ml_bool false l) = Some true.
-Proof.
-rewrite bindA.
-under eq_bind do rewrite !bindA.
-under eq_bind do under eq_bind do
- rewrite !bindA bindretf !bindA bindretf cputget.
-rewrite -bindA_uncurry -bindA crunret // crunchkput // bindA.
-under eq_bind do rewrite !bindA.
-under eq_bind do under eq_bind do rewrite bindretf /=.
-by rewrite crunnewchkC // crunnewchk0.
-Qed.
-
 Definition rtl (T : ml_type) (param : loc (ml_rlist T))
   : M (loc (ml_rlist T)) :=
   do v <- cget param; Ret (match v with Nil => param | Cons _ t => t end).
@@ -165,15 +155,6 @@ rewrite cnewchk.
 by under [RHS]eq_bind do (rewrite bindA; under eq_bind do rewrite bindretf).
 Qed.
 
-Lemma rhd_tl_tl_is_true :
-  crun (do l <- cycle ml_bool true false; do l1 <- rtl l; do l2 <- rtl l1;
-        rhd ml_bool false l2) = Some true.
-Proof.
-rewrite -rhd_is_true -[in RHS]rtl_tl_self [in RHS]bindA.
-under [in RHS]eq_bind do rewrite bindA.
-done.
-Qed.
-
 Lemma perm3 T (s1 s2 s3 s4 : coq_type N T) :
   do r1 <- cnew s1; do r2 <- cnew s2; do r3 <- cnew s3; cput r1 s4 =
   do r1 <- cnew s4; do r2 <- cnew s2; do r3 <- cnew s3; skip :> M _.
@@ -300,28 +281,6 @@ under eq_bind do under eq_bind do
 by rewrite cchk_mkrlist_put_drop mkrlist_drop.
 Qed.
 
-Lemma rnth_is_true n :
-  crun (do l <- cyclel ml_bool true (nseq n false); rnth ml_bool false n.+1 l)
-  = Some true.
-Proof.
-rewrite /rnth -bindA -[in n.+1](size_nseq n false) cyclel_rdrop_self.
-rewrite /rhd !bindA.
-under eq_bind=> r.
-  rewrite !bindA.
-  under eq_bind do rewrite bindA bindretf cputget.
-  rewrite -bindA.
-  over.
-rewrite -bindA crunret // -bindA_uncurry crunchkput // bindA -cnewchk.
-under eq_bind => r.
-  rewrite bindA.
-  under eq_bind do under eq_bind do rewrite bindretf /= -[cchk _]bindmskip.
-  rewrite cchkmkrlistC.
-  over.
-rewrite cnewchk -bindA crunmskip.
-elim: n => /= [|n IH]. by rewrite bindmret crunnew0.
-by rewrite -bindA crunnew.
-Qed.
-
 Fixpoint iappend (h : nat) (l1 l2 : coq_type N (ml_rlist ml_int))
   : M (coq_type N (ml_rlist ml_int)) :=
   if h is h.+1 then
@@ -355,6 +314,67 @@ Fixpoint loc_ids_rlist (l : list nat) (rl : rlist nat ml_int)
           do rl' <- cget r; do rs <- loc_ids_rlist t rl'; Ret (loc_id r :: rs)
       end
   end.
+End cyclic.
+
+Section cyclic_run.
+Variables (N : monad) (M : typedStoreRunMonad N).
+
+Local Notation coq_type := hierarchy.coq_type.
+Local Open Scope do_notation.
+
+Local Notation cycle := (cycle N M).
+Local Notation rhd := (rhd N M).
+Local Notation rtl := (rtl N M _).
+Local Notation cyclel := (cyclel N M).
+Local Notation rnth := (rnth N M).
+
+Lemma rhd_is_true :
+  crun (do l <- cycle ml_bool true false; rhd ml_bool false l) = Some true.
+Proof.
+rewrite bindA.
+under eq_bind do rewrite !bindA.
+under eq_bind do under eq_bind do
+ rewrite !bindA bindretf !bindA bindretf cputget.
+rewrite -bindA_uncurry -bindA crunret // crunchkput // bindA.
+under eq_bind do rewrite !bindA.
+under eq_bind do under eq_bind do rewrite bindretf /=.
+by rewrite crunnewchkC // crunnewchk0.
+Qed.
+
+Lemma rhd_tl_tl_is_true :
+  crun (do l <- cycle ml_bool true false; do l1 <- rtl l; do l2 <- rtl l1;
+        rhd ml_bool false l2) = Some true.
+Proof.
+rewrite -rhd_is_true -[in RHS]rtl_tl_self [in RHS]bindA.
+under [in RHS]eq_bind do rewrite bindA.
+done.
+Qed.
+
+Lemma rnth_is_true n :
+  crun (do l <- cyclel ml_bool true (nseq n false); rnth ml_bool false n.+1 l)
+  = Some true.
+Proof.
+rewrite /rnth -bindA -[in n.+1](size_nseq n false) cyclel_rdrop_self.
+rewrite /rhd !bindA.
+under eq_bind=> r.
+  rewrite !bindA.
+  under eq_bind do rewrite bindA bindretf cputget.
+  rewrite -bindA.
+  over.
+rewrite -bindA crunret // -bindA_uncurry crunchkput // bindA -cnewchk.
+under eq_bind => r.
+  under eq_bind do rewrite bindA.
+  under eq_bind do under eq_bind do rewrite bindretf /= -[cchk _]bindmskip.
+  rewrite cchkmkrlistC.
+  over.
+rewrite cnewchk -bindA crunmskip.
+elim: n => /= [|n IH]. by rewrite bindmret crunnew0.
+by rewrite -bindA crunnew.
+Qed.
+
+Local Notation is_int_list := (is_int_list N M).
+Local Notation loc_ids_rlist := (loc_ids_rlist N M).
+Local Notation iappend := (iappend N M).
 
 Lemma iappend_correct m l1 l2 :
   crun (do p : rlist nat ml_int * rlist nat ml_int <- m; let (rl1, rl2) := p in
@@ -368,14 +388,13 @@ Lemma iappend_correct m l1 l2 :
 Proof.
 (* need more abstractions *)
 Abort.
-End cyclic.
+End cyclic_run.
 
 Module eval_cyclic.
 Section eval.
-Import monad_model.ModelTypedStore.
+Import monad_model.ModelTypedStoreRun.
 
-Definition M :=
-  [the typedStoreMonad idfun of @acto ml_type idfun].
+Definition M := @acto ml_type idfun.
 
 Definition Env := Env ml_type idfun.
 
@@ -427,11 +446,17 @@ End eval.
 End eval_cyclic.
 
 Section factorial.
-Variable (N : monad) (M : typedStoreMonad N).
+Variable (N : monad) (M : typedStoreRunMonad N).
 
 Fixpoint fact_ref (r : loc ml_int) (n : nat) : M unit :=
   if n is m.+1 then cget r >>= fun p => cput r (n * p) >> fact_ref r m
   else skip.
+End factorial.
+
+Section factorial_run.
+Variable (N : monad) (M : typedStoreRunMonad N).
+
+Local Notation fact_ref := (fact_ref N M).
 
 Theorem fact_ref_ok n :
   crun (cnew ml_int 1 >>= fun r => fact_ref r n >> cget r) = Some (fact_rec n).
@@ -449,7 +474,7 @@ rewrite cnewget.
 under eq_bind do rewrite bindA.
 by rewrite cnewput IH // (mulnC m.+1) -mulnA.
 Qed.
-End factorial.
+End factorial_run.
 
 Section fact_for.
 Variable (N : monad) (M : typedStoreMonad N).
@@ -466,6 +491,14 @@ Definition fact_for (n : coq_type ml_int) : M (coq_type ml_int) :=
         do v_1 <- (do v_1 <- cget v; Ret (v_1 * i));
         cput v v_1));
   cget v.
+End fact_for.
+
+Section fact_for_run.
+Variable (N : monad) (M : typedStoreRunMonad N).
+Local Notation coq_type := (hierarchy.coq_type N).
+Local Open Scope do_notation.
+
+Local Notation fact_for := (fact_for N M).
 
 Theorem fact_for_ok n : crun (fact_for n) = Some (fact_rec n).
 Proof.
@@ -490,7 +523,7 @@ under eq_bind do rewrite bindretf.
 rewrite cnewput -IH; last by apply ltnW.
 by rewrite subnS mulnC -(@prednK (n-m)) // lt0n subn_eq0 -ltnNge.
 Qed.
-End fact_for.
+End fact_for_run.
 
 Section fibonacci.
 Variables (N : monad) (M : typedStoreMonad N).
@@ -506,6 +539,13 @@ Fixpoint fibo_ref n (a b : loc ml_int) : M unit :=
            >> fibo_ref n a b
   else skip.
 
+End fibonacci.
+
+Section fibonacci_run.
+Variables (N : monad) (M : typedStoreRunMonad N).
+
+Local Notation fibo_ref := (fibo_ref N M).
+
 Theorem fibo_ref_ok n :
   crun (cnew ml_int 1 >>=
              (fun a => cnew ml_int 1 >>= fun b => fibo_ref n a b >> cget a))
@@ -546,7 +586,7 @@ rewrite cnewput.
 by under eq_bind do rewrite cnewput.
 Qed.
 
-End fibonacci.
+End fibonacci_run.
 
 End CoqTypeNat.
 
@@ -771,7 +811,7 @@ Definition fact_for63 (n : coq_type ml_int) : M (coq_type ml_int) :=
         cput v v_1));
   cget v.
 
-Section fact_for63_ok.
+Section fact_for63_lemmas.
 Variable n : nat.
 (* Note: assuming n < max_int rather than n <= max_int is not strictly
    needed, but it simplifies reasoning about loops in concrete code *)
@@ -805,6 +845,21 @@ rewrite /N2int -!Sint63.is_int //.
   by split; apply N2int_bounded, Z.lt_le_incl, (Z.lt_trans _ _ _ Hm).
 Qed.
 
+End fact_for63_lemmas.
+
+End fact_for_int63.
+
+Section fact_for63_ok.
+Variable N : monad.
+Variable M : typedStoreRunMonad ml_type N monad_model.locT_nat.
+Local Notation coq_type := (hierarchy.coq_type N).
+Local Open Scope do_notation.
+
+Local Notation fact_for63 := (fact_for63 N M).
+
+Variable n : nat.
+Hypothesis Hn : (Z.of_nat n < Sint63.to_Z Sint63.max_int)%Z.
+
 Theorem fact_for63_ok : crun (fact_for63 (N2int n)) = Some (N2int (fact_rec n)).
 Proof.
 rewrite /fact_for63.
@@ -837,13 +892,11 @@ rewrite cnewput -IH (ltnW,subnS) // -N2int_mul mulnC -(@prednK (n-m.+1)) //.
 by rewrite lt0n subn_eq0 -ltnNge.
 Qed.
 End fact_for63_ok.
-End fact_for_int63.
 
 Section eval.
 Require Import typed_store_model.
 
-Definition M := [the typedStoreMonad ml_type _ monad_model.locT_nat of
-                 acto ml_type].
+Definition M := acto ml_type.
 
 Definition Env := typed_store_model.Env ml_type.
 

hierarchy.v

@@ -70,6 +70,7 @@ From HB Require Import structures.
 (*                         OCaml type together with its Coq representation    *)
 (*                         in the type of a Tarski universe                   *)
 (*      typedStoreMonad == A monad for OCaml computations                     *)
+(*   typedStoreRunMonad == typedStoreMonad + crun                             *)
 (*                                                                            *)
 (* Trace monads:                                                              *)
 (*            traceMonad == trace monad                                       *)
@@ -1096,7 +1097,6 @@ HB.mixin Record isMonadTypedStore (MLU : ML_universe) (N : monad) (locT : eqType
   cnew : forall {T : MLU}, coq_type N T -> M (loc locT T) ;
   cget : forall {T}, loc locT T -> M (coq_type N T) ;
   cput : forall {T}, loc locT T -> coq_type N T -> M unit ;
-  crun : forall {A : UU0}, M A -> option A ; (* execute in empty store *)
   cnewget : forall T (s : coq_type N T) A (k : loc locT T -> coq_type N T -> M A),
     cnew s >>= (fun r => cget r >>= k r) = cnew s >>= (fun r => k r s) ;
   cnewput : forall T (s t : coq_type N T) A (k : loc locT T -> M A),
@@ -1144,16 +1144,29 @@ HB.mixin Record isMonadTypedStore (MLU : ML_universe) (N : monad) (locT : eqType
            (k : loc locT T' -> M A),
       cget r >> (cnew s' >>= fun r' => cput r s >> k r') =
       cput r s >> (cnew s' >>= k) ;
+}.
+
+#[short(type=typedStoreMonad)]
+HB.structure Definition MonadTypedStore (ml_type : ML_universe) (N : monad) (locT : eqType) :=
+  { M of isMonadTypedStore ml_type N locT M & }.
+
+Arguments cnew {ml_type N locT s}.
+Arguments cget {ml_type N locT s} [T].
+Arguments cput {ml_type N locT s} [T].
+
+HB.mixin Record isMonadTypedStoreRun (MLU : ML_universe) (N : monad) (locT : eqType)
+    (M : UU0 -> UU0) of MonadTypedStore MLU N locT M := {
+  crun : forall {A : UU0}, M A -> option A ; (* execute in empty store *)
   crunret : forall (A B : UU0) (m : M A) (s : B),
       crun m -> crun (m >> Ret s) = Some s ;
   crunskip :
       crun skip = Some tt ;
   crunnew : forall (A : UU0) T (m : M A) (s : A -> coq_type N T),
-      crun m -> crun (m >>= fun x => cnew (s x)) ;
+      crun m -> crun (m >>= fun x => cnew T (s x)) ;
   crunnewgetC : forall (A : UU0) T1 T2 (m : M A) (r : A -> loc locT T1)
                       (s : A -> coq_type N T2),
       crun (m >>= fun x => cget (r x)) ->
-      crun (m >>= fun x => cnew (s x) >> cget (r x)) ;
+      crun (m >>= fun x => cnew T2 (s x) >> cget (r x)) ;
   crungetput : forall (A : UU0) T (m : M A) (r : A -> loc locT T)
                       (s : A -> coq_type N T),
       crun (m >>= fun x => cget (r x)) ->
@@ -1162,13 +1175,10 @@ HB.mixin Record isMonadTypedStore (MLU : ML_universe) (N : monad) (locT : eqType
       crun (m >> skip) = crun m :> bool ;
 }.
 
-#[short(type=typedStoreMonad)]
-HB.structure Definition MonadTypedStore (ml_type : ML_universe) (N : monad) (locT : eqType) :=
-  { M of isMonadTypedStore ml_type N locT M & isMonad M & isFunctor M }.
+#[short(type=typedStoreRunMonad)]
+HB.structure Definition MonadTypedStoreRun (ml_type : ML_universe) (N : monad) (locT : eqType) :=
+  { M of isMonadTypedStoreRun ml_type N locT M & }.
 
-Arguments cnew {ml_type N locT s}.
-Arguments cget {ml_type N locT s} [T].
-Arguments cput {ml_type N locT s} [T].
 Arguments crun {ml_type N locT s} [A].
 
 HB.mixin Record isMonadTrace (T : UU0) (M : UU0 -> UU0) of Monad M :=

monad_model.v

@@ -63,7 +63,7 @@ Require Import monad_transformer.
 (* Module ModelMonadStateRun       == stateRunMonad for MS                    *)
 (* Module ModelMonadExceptStateRun == exceptStateRunMonad                     *)
 (*                                                                            *)
-(* Module ModelTypedStore == model for typed store                            *)
+(* Module ModelTypedStoreRun == model for typed store (and crun)              *)
 (*                                                                            *)
 (* Module TrivialPlusArray == another, degenerate model of MonadPlusArray     *)
 (*                                                                            *)
@@ -1737,9 +1737,9 @@ End TrivialPlusArray.
 
 Definition locT_nat : eqType := nat.
 
-Module ModelTypedStore.
+Module ModelTypedStoreRun.
 
-Section ModelTypedStore.
+Section ModelTypedStoreRun.
 Variables (MLU : ML_universe) (N : monad).
 
 Local Notation coq_type := (@coq_type MLU N).
@@ -2215,12 +2215,14 @@ HB.instance Definition _ := Monad.on M.
 HB.instance Definition isMonadTypedStoreModel :=
   isMonadTypedStore.Build ml_type N locT_nat M cnewget cnewput cgetput cgetputskip
     cgetget cputget cputput cgetC cgetnewD cgetnewE cgetputC cputC
-    cputgetC cputnewC
+    cputgetC cputnewC.
+HB.instance Definition isMonadTypedStoreRunModel :=
+  isMonadTypedStoreRun.Build ml_type N locT_nat M
     crunret crunskip crunnew crunnewgetC crungetput crunmskip.
 
 End mkbind.
-End ModelTypedStore.
-End ModelTypedStore.
+End ModelTypedStoreRun.
+End ModelTypedStoreRun.
 
 (* TODO?
 (* result of a discussion with Maxime and Enrico on 2019-09-12 *)