ML_universe as a mixin (#112)

example_typed_store.v

@@ -5,6 +5,7 @@ From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.
 From infotheo Require Import ssrZ.
 Require monad_model.
+From HB Require Import structures.
 Require Import monae_lib hierarchy monad_lib typed_store_lib.
 
 (******************************************************************************)
@@ -84,16 +85,17 @@ Fixpoint coq_type_nat (T : ml_type) : Type :=
 End with_monad.
 
 (* use coq_type_nat (typed_store_model.v) *)
-Canonical MLU := @Build_ML_universe _ coq_type_nat ml_unit val_nonempty.
+HB.instance Definition _ := @isML_universe.Build ml_type
+  (Equality.class ml_type_eqType) coq_type_nat ml_unit val_nonempty.
 
 (* alternative: use coq_type_nat0 (monad_model.v) *)
-(*
-Definition coq_type_nat0 := @coq_type_nat idfun.
-Canonical MLU := @monad_model.MLU _ coq_type_nat0 ml_unit (val_nonempty idfun).
-*)
+(*Definition coq_type_nat0 := @coq_type_nat idfun.
+HB.instance Definition _ := @isML_universe.Build ml_type
+  (Equality.class ml_type_eqType) (fun M => @coq_type_nat0) ml_unit
+  (fun M => val_nonempty idfun).*)
 
 Section cyclic.
-Variables (M : typedStoreMonad MLU MLTypes.locT).
+Variables (M : typedStoreMonad ml_type MLTypes.locT).
 Local Notation coq_type := (hierarchy.coq_type (MonadTypedStore.sort M)).
 Local Open Scope do_notation.
 
@@ -128,7 +130,7 @@ Qed.
 End cyclic.
 
 Section factorial.
-Variable M : typedStoreMonad MLU MLTypes.locT.
+Variable M : typedStoreMonad ml_type MLTypes.locT.
 Notation coq_type := (@coq_type M).
 
 Fixpoint fact_ref (r : loc ml_int) (n : nat) : M unit :=
@@ -154,7 +156,7 @@ Qed.
 End factorial.
 
 Section fact_for.
-Variable M : typedStoreMonad MLU MLTypes.locT.
+Variable M : typedStoreMonad ml_type MLTypes.locT.
 Local Notation coq_type := (hierarchy.coq_type (MonadTypedStore.sort M)).
 Local Open Scope do_notation.
 
@@ -195,7 +197,7 @@ Qed.
 End fact_for.
 
 Section fibonacci.
-Variable M : typedStoreMonad MLU MLTypes.locT.
+Variable M : typedStoreMonad ml_type MLTypes.locT.
 Local Notation coq_type := (hierarchy.coq_type (MonadTypedStore.sort M)).
 
 Fixpoint fibo_rec n :=
@@ -421,10 +423,13 @@ Fixpoint coq_type63 (T : ml_type) : Type :=
 End with_monad.
 (******************************************************************************)
 
-Canonical ml_type63 := @Build_ML_universe _ coq_type63 ml_unit val_nonempty.
+HB.instance Definition _ := @isML_universe.Build ml_type
+  (Equality.class ml_type_eqType) coq_type63 ml_unit val_nonempty.
+
+(*Canonical ml_type63 := @Build_ML_universe _ coq_type63 ml_unit val_nonempty.*)
 
 Section fact_for_int63.
-Variable M : typedStoreMonad ml_type63 MLTypes.locT.
+Variable M : typedStoreMonad ml_type MLTypes.locT.
 Local Notation coq_type := (hierarchy.coq_type (MonadTypedStore.sort M)).
 Local Open Scope do_notation.
 
@@ -540,4 +545,29 @@ 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 Env := typed_store_model.Env ml_type.
+
+Definition empty_env := @typed_store_model.mkEnv ml_type nil.
+
+Definition W T := (Env * T)%type.
+
+Definition it0 : W unit := (empty_env, tt).
+
+Local Open Scope do_notation.
+
+Definition incr (l : loc ml_int) : M int :=
+  do x <- cget l; do _ <- cput l (Uint63.succ x); Ret (Uint63.succ x).
+
+Definition evalme := (do l <- @cnew ml_type ml_int 3; incr l)%int63 empty_env.
+
+Eval vm_compute in evalme.
+
+End eval.
+
 End MLtypes63.

hierarchy.v

@@ -1092,12 +1092,17 @@ Variant loc (ml_type : Type) (locT : eqType) : ml_type -> Type :=
 Definition loc_id (ml_type : Type) (locT : eqType) {T : ml_type} (l : loc locT T) : locT :=
   let: mkloc _ n := l in n.
 
-Structure ML_universe := {
-  ml_type :> eqType ;
+HB.mixin Structure isML_universe (ml_type : Type) := {
+  eqclass : Equality.class_of ml_type ;
   coq_type : forall M : Type -> Type, ml_type -> Type ;
   ml_nonempty : ml_type ;
   val_nonempty : forall M, coq_type M ml_nonempty }.
 
+#[short(type=ML_universe)]
+HB.structure Definition ML_UNIVERSE := {ml_type & isML_universe ml_type}.
+
+Canonical isML_universe_eqType (T : ML_universe) := EqType T eqclass.
+
 HB.mixin Record isMonadTypedStore (MLU : ML_universe) (locT : eqType) (M : UU0 -> UU0)
     of Monad M := {
   cnew : forall {T : MLU}, coq_type M T -> M (loc locT T) ;

monad_model.v

@@ -1666,27 +1666,31 @@ Definition locT_nat := [eqType of nat].
 Module ModelTypedStore.
 
 Section ModelTypedStore.
-Variables (ml_type0 : eqType) (coq_type0 : ml_type0 -> Type)
-          (ml_nonempty0 : ml_type0) (val_nonempty0 : coq_type0 ml_nonempty0).
+Variables (ml_type0' : eqType) (coq_type0 : ml_type0' -> Type)
+          (ml_nonempty0 : ml_type0') (val_nonempty0 : coq_type0 ml_nonempty0).
 
-Definition MLU : ML_universe :=
-  @Build_ML_universe (ml_type0) (fun M => @coq_type0)
-  (ml_nonempty0) (fun M => val_nonempty0).
+Definition ml_type0 : Type := ml_type0'.
+
+HB.instance Definition _ := @isML_universe.Build ml_type0
+  (Equality.class ml_type0') (fun M => @coq_type0) ml_nonempty0
+  (fun M => val_nonempty0).
 
 Record binding (M : Type -> Type) :=
-  mkbind { bind_type : MLU; bind_val : coq_type M bind_type }.
+  mkbind { bind_type : ml_type0; bind_val : coq_type M bind_type }.
+
 Arguments mkbind {M}.
 
-Definition acto : UU0 -> UU0 := MS (seq (binding idfun)) [the monad of option_monad].
+Definition acto : UU0 -> UU0 :=
+  MS (seq (binding idfun)) [the monad of option_monad].
 Local Notation M := acto.
 
-Local Notation coq_type' := (@coq_type MLU idfun).
+Local Notation coq_type' := (@coq_type ml_type0 idfun).
 
-Definition def : binding idfun := mkbind (ml_nonempty MLU) (val_nonempty MLU idfun).
+Definition def : binding idfun := mkbind ml_nonempty (val_nonempty idfun).
 
 Local Notation nth_error := List.nth_error.
 
-Notation loc := (@loc MLU locT_nat).
+Notation loc := (@loc ml_type0 locT_nat).
 
 Definition cnew T (v : coq_type M T) : M (loc T) :=
   fun st => let n := size st in
@@ -1715,23 +1719,23 @@ Definition crun (A : UU0) (m : M A) : option A :=
 
 Definition Env := seq (binding idfun).
 
-Definition fresh_loc (T : MLU) (e : Env) := mkloc T (size e).
+Definition fresh_loc (T : ml_type0) (e : Env) := mkloc T (size e).
 
 Section mkbind.
 Local Notation mkbind := (@mkbind idfun).
 
 Definition extend_env T (v : coq_type M T) (e : Env) :=
   rcons e (mkbind T v).
 
-Variant nth_error_spec (T : MLU) (e : Env) (r : loc T) : Type :=
+Variant nth_error_spec (T : ml_type0) (e : Env) (r : loc T) : Type :=
   | NthError : forall s : coq_type M T,
     nth_error e (loc_id r) = Some (mkbind T s) -> nth_error_spec e r
   | NthError_nocoerce : forall T' (s' : coq_type M T'),
     nth_error e (loc_id r) = Some (mkbind T' s') -> ~ coerce T s' ->
     nth_error_spec e r
   | NthError_None : nth_error e (loc_id r) = None -> nth_error_spec e r.
 
-Lemma ntherrorP (T : MLU) (e : Env) (r : loc T) : nth_error_spec e r.
+Lemma ntherrorP (T : ml_type0) (e : Env) (r : loc T) : nth_error_spec e r.
 Proof.
 case H : (nth_error e (loc_id r)) => [[T' s']|].
   have [Ts'|Ts'] := boolp.pselect (coerce T s').
@@ -1772,7 +1776,7 @@ Lemma nocoerce_cget T (r : loc T) T' (s' : coq_type M T') e :
   cget r e = fail.
 Proof. by move=> H Ts'; rewrite /cget H; case: coerce Ts'. Qed.
 
-Lemma nocoerce_cput T (r : loc T) (s : coq_type M T) T' (s' : coq_type M T') e :
+Lemma nocoerce_cput T (r : loc T) (s : coq_type M T) (T' : ml_type0) (s' : coq_type M T') e :
   nth_error e (loc_id r) = Some (mkbind T' s') ->
   ~ coerce T s' ->
   cput r s e = fail.
@@ -1854,7 +1858,7 @@ have [s' H|T' s' H Ts'|H] := ntherrorP e r.
 - by rewrite 2!MS_bindE None_cput.
 Qed.
 
-Lemma Some_cputput (T : MLU) (r : loc T) (s s' : coq_type M T)
+Lemma Some_cputput (T : ml_type0) (r : loc T) (s s' : coq_type M T)
   (e : Env) (s'' : coq_type M T) :
   nth_error e (loc_id r) = Some (mkbind T s'') ->
   (cput r s >> cput r s') e = cput r s' e.
@@ -2157,7 +2161,7 @@ Qed.
 
 HB.instance Definition _ := Monad.on M.
 HB.instance Definition isMonadTypedStoreModel :=
-  isMonadTypedStore.Build MLU locT_nat M cnewget cnewput cgetput cgetputskip
+  isMonadTypedStore.Build ml_type0 locT_nat M cnewget cnewput cgetput cgetputskip
     cgetget cputget cputput cgetC cgetnewD cgetnewE cgetputC cputC
     cputgetC cputnewC
     crunret crunskip crunnew crunnewget crungetnew crungetput.

typed_store_model.v

@@ -55,7 +55,7 @@ Local Notation coq_type := (@coq_type MLU M).
 
 Local Notation val_nonundef := (val_nonempty MLU).
 
-Definition def := mkbind (val_nonempty MLU M).
+Definition def := mkbind (@val_nonempty MLU M).
 
 Local Notation nth_error := List.nth_error.