wrapper mixin step0

HB/common/utils.elpi

@@ -44,6 +44,7 @@ with-attributes P :-
     att "primitive" bool,
     att "non_forgetful_inheritance" bool,
     att "hnf" bool,
+    att "wrapper" bool,
   ] Opts, !,
   Opts => (save-docstring, P).
 

HB/factory.elpi

@@ -192,6 +192,7 @@ mk-factory-abbrev Str GR Aliases FactAbbrev :- !, std.do! [
 pred declare-asset i:argument, i:asset.
 declare-asset Arg AssetKind :- std.do! [
   argument-name Arg Module,
+
   if-verbose (coq.say {header} "start module and section" Module),
   log.coq.env.begin-module Module none,
   log.coq.env.begin-section Module,
@@ -232,6 +233,7 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
 
   % coq.say RDecl RDeclClosed,
 
+
   if (get-option "primitive" tt)
     (@primitive! => log.coq.env.add-indt RDeclClosed R)
     (log.coq.env.add-indt RDeclClosed R),
@@ -250,6 +252,25 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
   build-deps-for-projections R MLwP GRDepsClausesProjs,
   GRDepsClauses = [gref-deps (indt R) MLwP, gref-deps (indc K) MLwP|GRDepsClausesProjs],
 
+  coq.say "TODO: extract useful info:" RDecl,
+  % record-decl in https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi#L429
+  % per trovare il vero nome del mixin   database.elpi:factory-alias->gref
+  % per sapere quanti argomenti skippare prima del soggetto del mixin
+  %   factory-nparams
+  %
+  % in generale hai:
+  %  forall ....., app[mixin_alias, p1 ... pn | [  app[subject, ...] , extra]]
+  %  mixin_alias -> mixin via factory-alias->gref
+  %  factory-nparams mixin -> n
+  % 
+
+  if (get-option "wrapper" tt)
+     ((factory-alias->gref (indt R) X),
+      (WrapperClauses = [wrapper-mixin X (indt R) (indt R)]))
+     (WrapperClauses = []),
+
+  coq.say "aggiungiamo " WrapperClauses,
+
   % GRDepsClauses => mk-factory-sort MLwP (indt R) _ FactorySortCoe,
   % FactorySortCoe = coercion GRFSort _ _ _,
 
@@ -271,7 +292,7 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
   if-verbose (coq.say {header} "start module Exports"),
 
   log.coq.env.begin-module "Exports" none,
-  std.flatten [Clauses, GRDepsClauses, [
+  std.flatten [Clauses, GRDepsClauses, WrapperClauses, [
     factory-constructor (indt R) GRK,
     factory-nparams (indt R) NParams,
     factory-builder-nparams BuildConst NParams,

_CoqProject.test-suite

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

structures.v

@@ -159,6 +159,13 @@ pred join o:classname, o:classname, o:classname.
 % in order to discover two mixins are the same)
 pred mixin-mem i:term, o:gref.
 
+% [wrapper-mixin Wrapper NewSubject WrappedMixin]
+%  #[wrapper] HB.mixin Record hom_isMon T of Quiver T :=
+%      { private : forall A B, isMon (@hom T A B) }.
+%  -->
+%  wrapper-mixin (indt "hom_isMon") (const "hom") (indt "isMon").
+pred wrapper-mixin o:mixinname, o:gref, o:mixinname.
+
 %%%%%% Memory of exported mixins (HB.structure) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Operations (named mixin fields) need to be exported exactly once,
 % but the same mixin can be used in many structure, hence this memory

tests/enriched_cat.v

@@ -0,0 +1,105 @@
+(* testing enriched categories *)
+
+From HB Require Import structures.
+From Coq Require Import ssreflect ssrfun.
+
+HB.mixin Record isQuiver (Obj: Type) : Type := { hom : Obj -> Obj -> Type }.
+
+HB.structure Definition Quiver : Type := { Obj of isQuiver Obj }.
+
+HB.mixin Record isMon (A: Type) : Type := {
+    zero  : A;
+    add   : A -> A -> A;
+    addrA : associative add;
+    add0r : left_id zero add;
+    addr0 : right_id zero add;
+  }.
+
+HB.structure
+  Definition Monoid : Type := { A of isMon A }.
+
+(* original wrapper *)
+HB.mixin Record hom_isMon T of Quiver T :=
+    { private : forall A B, isMon (@hom T A B) }.
+
+(* just an abbreviation with a parameter for homset *)
+Definition hom_isMon_ty {T} (H: T -> T -> Type) (A B: T) :
+  Type := isMon (H A B). 
+
+(* write two versions of Monoid_enriched_quiver: one using hom_isMon
+(a mixin, hence a record), the other one using hom_isMon_ty as naked
+field type. The former corresponds to the wrapped version, the latter
+to the intuitive, wrapper-less version. Now the latter should agree
+with the former... (broadly corresponding to 2?) *)
+
+(* alternative wrapper definition *)
+HB.mixin Record hom_isMon1 T of Quiver T :=
+    { private : forall A B, hom_isMon_ty (@hom (Quiver.clone T _)) A B }.
+
+(* abbreviation with parameters for homset and monoid *)
+Definition hom_isM_ty {T} (H: T -> T -> Type) (M: Type -> Type) (A B: T) :
+  Type := M (H A B). 
+
+(* three parameter relation *)
+Definition wrapper_spec {T} (H: T -> T -> Type) (M HM: Type -> Type) :
+  Prop := HM T = forall A B, hom_isM_ty H M A B.
+
+(* one more wrapper definition (no real change) *)                           
+HB.mixin Record hom_isMon2 T of Quiver T :=
+  { private : forall A B, hom_isM_ty (@hom (Quiver.clone T _))
+                                     (fun X => isMon X)
+                                     A B }.
+
+(* trying parametric definition however doesn't work *)
+Fail HB.mixin Record hom_isM2 T (M: Type -> Type) of Quiver T :=
+  { private : forall (A B: T), @hom_isM_ty T (@hom (Quiver.clone T _))
+                                     M
+                                     A B }.
+
+(* structure based on one of the wrappers *)
+HB.structure Definition Monoid_enriched_quiver :=
+    { Obj of isQuiver Obj & hom_isMon2 Obj }.
+
+(******************)
+
+(* unique projection from the wrapper *)
+HB.instance Definition _ (T : Monoid_enriched_quiver.type) (A B : T) :
+  isMon (@hom T A B) := @private T A B.
+
+(* quiver instance (simply typed functions between two types) *)
+HB.instance Definition funQ := isQuiver.Build Type (fun A B => A -> B).
+
+(* prove that for every two types the quiver is a monoid *)
+Lemma funQ_isMonF (A B: Type) : isMon (A -> B).
+Admitted.
+
+(* use the lemma to instantiate isMon *)
+HB.instance Definition funQ_isMon (A B: Type) : isMon (A -> B) :=
+  funQ_isMonF A B.
+
+(* use the generic isMon instance to instantiate 'private' *)
+HB.instance Definition funQ_hom_isMon :=
+  hom_isMon2.Build Type (fun A B => funQ_isMon A B).
+
+(* HB.instance Definition _ := Monoid_enriched_quiver.Build ... *)
+
+(********************)
+
+(* without HB *)
+Record isQuiverS (Obj: Type) : Type := { homS : Obj -> Obj -> Type }.
+
+(* structure without wrapper and out of HB, trivially type-checks *)
+Structure Monoid_enriched_quiverN := {
+    ObjN: Type;
+    iQ: isQuiverS ObjN;
+    hsM: forall A B, hom_isM_ty (homS ObjN iQ)
+                                (fun X => isMon X) A B }.
+
+(* but mixing with HB doesn't work *)
+Fail Record Monoid_enriched_quiverN1 := {
+    ObjN: Type;
+    iQ: isQuiver ObjN;
+    hsM: forall A B, hom_isM_ty (@hom iQ)
+                                (fun X => isMon X) A B }.
+
+

tests/monoid_enriched_cat.v

@@ -0,0 +1,72 @@
+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.
+ *)
+
+(*  added wrapper attribute in coq-builtin.elpi. 
+    added pred wrapper-mixin in structures.v.
+    added conditional rule for wrapper-mixin in factory.elpi.
+    tentative use of factory-alias->gref, but the parameters 
+    aren't right yet -- see HB.structure.html. 
+*)
+#[wrapper]
+HB.mixin Record hom_isMon T of Quiver T :=
+    { private : forall A B, isMon (@hom T A B) }.
+
+Elpi Print HB.structure.
+
+stop.
+
+(* 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 _)) }.