test for step 0 of CoREACT

_CoqProject.test-suite

@@ -80,6 +80,8 @@ tests/hnf.v
 tests/fun_instance.v
 tests/issue284.v
 tests/issue287.v
+tests/monoid_law_structure.v
+tests/monoid_law_structure_clone.v
 
 -R tests HB.tests
 -R examples HB.examples

tests/monoid_enriched_cat.v

@@ -0,0 +1,61 @@
+From HB Require Import structures.
+From Coq Require Import ssreflect ssrfun.
+
+HB.mixin Record isQuiver Obj := { hom : Obj -> Obj -> Type }.
+
+HB.structure Definition Quiver := { Obj of isQuiver Obj }.
+
+HB.mixin Record isMon A := {
+ zero : A;
+ add : A -> A -> A;
+ addrA : associative add;
+ add0r : left_id zero add;
+ addr0 : right_id zero add;
+ }.
+
+HB.structure
+ Definition Monoid := { A of isMon A }.
+
+Fail HB.structure
+ Definition Monoid_enriched_quiver :=
+ { Obj of isQuiver Obj &
+ (forall A B : Obj, isMon (@hom (Quiver.clone Obj _) A B)) }.
+
+
+(* Step 0: define a wrapper predicate in coq-elpi *)
+(* 5 lines of documentation + 1 line of elpi code in structure.v
+ `pred wrapper-mixin o:mixinname, o:gref, o:mixinname`
+*)
+(* Step 1: add a wrapper attribute to declare wrappers,
+ they should index:
+ - the wrapped mixin (`isMon`)
+ - the wrapper mixin (`hom_isMon`)
+ - the new subject (`hom`)
+ This attribute will add an entry in the `wrapper-mixin` database.
+ As an addition substep, we should check that the wrapper has
+ exactly one field, which is the wrapped mixin.
+ *)
+#[wrapper]
+HB.mixin Record hom_isMon T of Quiver T :=
+ { private : forall A B, isMon (@hom T A B) }.
+
+(* Step 2: at structure declaration, export the main and only projection
+ of each declared wrapper as an instance of the wrapped structure on
+ its subject *)
+HB.structure
+ Definition Monoid_enriched_quiver :=
+ { Obj of isQuiver Obj & hom_isMon Obj }.
+
+HB.instance Definition _ (T : Monoid_enriched_quiver.type) (A B : T) : isMon (@hom T A B) :=
+ @private T A B.
+
+ (* each instance of isMon should be tried as an instance of hom_isMon *)
+
+(* Step 3: for each instance of a wrapped mixin on a subject known 
+ to be wrapped, automatically produce an instance of the wrapper mixin too. *)
+HB.instance Definition _ := isQuiver.Build Type (fun A B => A -> B).
+Fail HB.instance Definition homTypeMon (A B : Quiver.type) := isMon.Build (hom A B) (* ... *).
+(* This last command should create a `Monoid_enriched_quiver`, in order to do so it should
+ automatically instanciate the wrapper `hom_isMon`:
+ HB.instance Definition _ := hom_isMon.Build Type homTypeMon.
+ *)

tests/monoid_law_structure.v

@@ -0,0 +1,18 @@
+From HB Require Import structures.
+
+HB.mixin Record isMonLaw T (e : T) (op : T -> T -> T) := {
+ opmA : forall a b c, op (op a b) c = op a (op b c);
+ op1m : forall x, op e x = x;
+ opm1 : forall x, op x e = x;
+}.
+
+HB.structure Definition MonLaw T e := { op of isMonLaw T e op }.
+
+HB.mixin Record isPreMonoid T := {
+ zero : T;
+ add : T -> T -> T;
+}.
+HB.structure Definition PreMonoid := { T of isPreMonoid T }.
+
+HB.structure Definition Monoid :=
+ { T of isPreMonoid T & isMonLaw T zero add }.

tests/monoid_law_structure_clone.v

@@ -0,0 +1,19 @@
+From HB Require Import structures.
+
+HB.mixin Record isMonLaw T (e : T) (op : T -> T -> T) := {
+ opmA : forall a b c, op (op a b) c = op a (op b c);
+ op1m : forall x, op e x = x;
+ opm1 : forall x, op x e = x;
+}.
+
+HB.structure Definition MonLaw T e := { op of isMonLaw T e op }.
+
+HB.mixin Record isPreMonoid T := {
+ zero : T;
+ add : T -> T -> T;
+}.
+HB.structure Definition PreMonoid := { T of isPreMonoid T }.
+
+HB.structure Definition Monoid :=
+ { T of isPreMonoid T &
+ isMonLaw T (@zero (PreMonoid.clone T _)) (@add (PreMonoid.clone T _)) }.