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,
@@ -218,6 +219,49 @@ declare-asset Arg AssetKind :- std.do! [
   )
 ].
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%% auxiliary code for wrapper-mixin
+
+pred extract_from_record_decl i: (term -> gref -> prop), i:indt-decl, o:gref.
+extract_from_record_decl P (parameter ID _ _ R) Out :-
+   pi p\
+    extract_from_record_decl P (R p) Out.
+extract_from_record_decl P (record ID _ KID (field _ _ Ty (x\end-record))) GR0 :-
+    P Ty GR0.
+
+pred extract_from_rtty i: (term -> gref -> prop), i: term, o:gref.
+extract_from_rtty P (prod _ _ TF) Out1 :-
+  pi p\ 
+    extract_from_rtty P (TF p) Out1.
+extract_from_rtty P Ty Gr :- P Ty Gr.
+
+pred xtr_fst_op i:term, o:gref.
+xtr_fst_op Ty Gr1 :-
+  Ty = (app [global Gr0| _]),
+  factory-alias->gref Gr0 Gr1.
+
+pred xtr_snd_op i:term, o:gref.
+xtr_snd_op Ty Gr :-
+  Ty = (app [global _, app [global Gr| _]]).
+
+pred extract_wrapped i:indt-decl, o:gref.
+extract_wrapped In Out :-
+  extract_from_record_decl (extract_from_rtty xtr_fst_op) In Out.
+
+pred extract_subject i:indt-decl, o:gref.
+extract_subject In Out :-
+  extract_from_record_decl (extract_from_rtty xtr_snd_op) In Out.
+
+pred wrapper_mixin_aux i:gref, o:gref, o:gref.
+wrapper_mixin_aux XX Gr1 Gr2 :-
+  XX = (indt I),
+  coq.env.indt-decl I D,
+  extract_subject D Gr1,
+  extract_wrapped D Gr2.  
+
+%%% end auxiliary code for wrapper-mixin
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 pred declare-mixin-or-factory i:list prop, i:list constant, i:list term, i:term,
   i:term, i:record-decl, i:list-w-params factoryname, i:id, i:asset.
 declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
@@ -230,7 +274,9 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
 
   abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-indt-decl RDecl RDeclClosed _,
 
-  % coq.say RDecl RDeclClosed,
+%  coq.say "TEST" RDecl RDeclClosed,
+%  coq.say "TEST" RDecl,
+%  coq.say "TEST" (indt R),
 
   if (get-option "primitive" tt)
     (@primitive! => log.coq.env.add-indt RDeclClosed R)
@@ -250,6 +296,28 @@ 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,
+  % coq.say "TODO: extract useful info:" RDecl "AND THEN:" RDeclClosed,
+  % 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
+  % 
+
+  % coq.say "TEST 2" (indt R),
+
+  if (get-option "wrapper" tt)
+     ((wrapper_mixin_aux (indt R) NSbj WMxn),
+      (WrapperClauses = [wrapper-mixin (indt R) NSbj WMxn]))
+     (WrapperClauses = []),
+
+  % coq.say "aggiungiamo " WrapperClauses,
+
   % GRDepsClauses => mk-factory-sort MLwP (indt R) _ FactorySortCoe,
   % FactorySortCoe = coercion GRFSort _ _ _,
 
@@ -271,7 +339,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,

HB/instance.elpi

@@ -68,14 +68,57 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [
 
   private.declare-instance Factory TheType TheFactory Clauses CSL,
 
+% In a WRAPPING-RELEVANT INSTANCE, 
+% Factory is the wrapped mixin, TheType is the new subject, 
+% TheFactory is the wrapped instance for the new subject (in fact, 
+% it is the term for the instance that is being processed). 
+% E.g. in connection with our example in monoid_enriched_cat.v:
+%
+% HB.instance Definition funQ_isMon (A B: Type) : isMon (hom A B) :=
+%  funQ_isMonF A B.
+%
+% Factory = isMon
+% TheFactory = funQ_isMon
+% TheType = hom A B
+
+  coq.say "wrapping instance ???", 
+  coq.say "Factory = " Factory,
+  coq.say "TheFactory = " TheFactory,
+  coq.say "TheType = " TheType,
+
+  % extracts the head subterm (e.g. hom)
+  coq.safe-dest-app TheType TheTypeKey _,
+
+  coq.say "TheTypeKey = " TheTypeKey,
+
   % handle parameters via a section -- end
   if (TyWP = arity _) true (
     if-verbose (coq.say {header} "closing instance section"),
     log.coq.env.end-section-name SectionName
   ),
 
   % we accumulate clauses now that the section is over
-  acc-clauses current Clauses
+  acc-clauses current Clauses,
+
+  % As a general idea, we want to add wrapper instances
+  % for the original subjects that are covered by the current instances.
+  % Here we are processing a specific instance. We want to check
+  % whether it corresponds to a wrapper with respect to the new subject
+  % (associated with TheTypeKey and the Factory mixin).
+  % To this purpose, 
+  % 1) we find all the wrappers that agree with the given parameters, 
+  % using the wrapper-mixin predicate.    
+  % 2) we then apply derive_wrapper_instances to each wrapper, together 
+  % with the current instance, to create the derived wrapper instances.    
+  % Notice that derive_wrapper_instances calls declare-const. 
+  if (TheTypeKey = global TheTypeKeyGR)
+    (std.do! [
+     std.findall (wrapper-mixin _ TheTypeKeyGR Factory) Wrappers,
+     coq.say "WRAPPERS:" Wrappers,
+     std.forall Wrappers (private.derive_wrapper_instances TheFactory)
+     ]
+    )
+    true,
 ].
 
 % [declare-all T CL MCSTL] given a type T and a list of class definition
@@ -375,4 +418,84 @@ check-non-forgetful-inheritance T Factory :- std.do! [
     ) true
 ].
 
+% The type of the wrapper projection is... 
+% hom_isMon.hom_isMon_private :
+% forall (T : Type)
+%  (local_mixin_monoid_enriched_cat_isQuiver : isQuiver.axioms_ T),
+% hom_isMon.axioms_ T local_mixin_monoid_enriched_cat_isQuiver ->
+% forall
+%  A
+%   B : {|
+%         Quiver.sort := T;
+%         Quiver.class :=
+%           {|
+%             Quiver.monoid_enriched_cat_isQuiver_mixin :=
+%               local_mixin_monoid_enriched_cat_isQuiver
+%           |}
+%       |}, isMon.phant_axioms (hom A B)
+
+% Not used, but possible useful
+pred extract_string_name i:mixinname i:term o:string.
+extract_string_name W Trm Str.
+
+% Instance has morally type 'Mixin Subject'
+pred derive_wrapper_instances i:term, i:prop.
+derive_wrapper_instances Instance (wrapper-mixin WrapperMixin Subject Mixin) :- std.do! [
+    % K is the mixin constructor (Build) for WrapperMixin 
+     factory-constructor WrapperMixin K,
+     factory-nparams WrapperMixin NParams,
+     std.assert! (NParams = 0) "TODO support parameters",
+
+    % We are only interested in the last parameter of the constructor
+    % type, which is the current instance 
+    % (which is a Mixin instance on the new Subject).  
+    % In monoid_enriched_cat.v, we are targeting the code 
+    %
+    % HB.instance Definition funQ_hom_isMon :=
+    %             hom_isMon.Axioms_ _ _ funQ_isMon.
+    % which Coq can compute to stand for 
+    %              hom_isMon.Axioms_ Type funQ funQ_isMon.
+    %
+    % We compute the number of the underscores and we pass 
+    % them as arguments followed by Instance.
+     coq.env.typeof K KTy, 
+     coq.count-prods KTy KN, 
+     KN0 = KN - 1,
+     coq.mk-n-holes KN0 Holes,
+
+     std.append Holes [Instance] Args,
+
+     % the body of the new wrapper instance
+     NewInstance = app[global K| Args],
+
+     coq.say "NewInstance=" {coq.term->string NewInstance},
+
+     coq.typecheck NewInstance Ty Dgn,
+     if (Dgn = error S) (coq.say "errore" S)
+      (coq.count-prods Ty N0,
+        % we then call declare-const to add the new instance.
+        % the name needs to be fixed.
+       instance.declare-const "_" NewInstance {coq.term->arity Ty N0} _
+      )
+
+/*
+% 2) The existing instances of W correspond to the functions of type (Ty _)
+% that are already defined for different original subjects; 
+% or in other words, they correspond to wrapped instances, 
+% given a specific original subject T and two generic objects of that type. 
+% Should we consider only one function for each T?
+% This means that e.g. there is only one way a homset can be instance of the wrapped 
+% (here, a monoid).
+% Notice that it's good to assume all relevant functions have been 
+% defined using generic type syntax (otherwise recovering them would be much harder).
+% This means for a carrier there is only a quiver. 
+% The instances whould be filtered out from the current context, maybe EX?
+     filter_out_unique_defs_of_type Ty WrapperProjections,
+%     filter_out_unique_defs_of_type Ty AllInstances WrapperProjections,
+% 3) We can define the wrapper instances based on Ty, using the projection definitions.
+     std.forall WrapperProjections (export-wrapper-instance W)
+*/
+].
+derive_wrapper_instances _ _.
+
 }}

HB/structure.elpi

@@ -205,6 +205,46 @@ declare Module BSkel Sort :- std.do! [
   log.coq.env.end-module-name ElpiOperationModName ElpiOperations,
   export.module ElpiOperationModName ElpiOperations,
 
+  % factories-provide (line 16) gives the mixins provided from a factory. 
+  % line 23 (list-w-params_list) associates these mixins with their names (ML).
+  % we need to filter the wrappers out of ML. 
+  % then export the projection of each mixin wrapper. 
+  % can use exported-op to this purpose 
+
+  %% tentative pseudo-code::
+  % std.filter ML (x\ wrapper-mixin x _ _) WrapperML,
+  % std.forall WrapperML private.rexport-wrapper-as-instance,
+
+  %% write private code below:
+  % pred rexport-wrapper-as-instance i:mixinname.
+  % reexport-wrapper-as-instance M :-
+  %   exported-op M _ C,
+  %   declare-existing-instance C %fixme.
+
+  std.filter ML (x\ wrapper-mixin x _ _) WrapperML,
+  % we need to assert locally the clauses in EX, which is 
+  % [exported-op (indt «hom_isMon.axioms_») «hom_isMon.hom_isMon_private» 
+  % «hom_isMon_private»]
+  % crucially containing hom_isMon_private.
+  % In fact, these clauses get added to the global database by Accumulate,
+  % but this makes them available only at the end of the program run, and 
+  % this is too late.
+  % Then given WrapperML (the list of the wrapper mixins as grefs)
+  % i.e. [indt «hom_isMon.axioms_»]
+  % we can use reexport-wrapper-as-instance to get the projection and build 
+  % the instances. 
+  coq.say "???? WrapperML " WrapperML,  
+  coq.say "???? EX " EX,
+  EX => std.forall WrapperML private.reexport-wrapper-as-instance,
+
+  coq.say "???? NewClauses " NewClauses,
+
+  % tentative: generating wrapper instances from the available definitions.
+  % Wrong approach: we actually need to check each new defined instance to 
+  % see if it triggers a wrapper instance too. We do this in instance.elpi.
+  % EX => std.forall WrapperML private.derive_wrapper_instances, 
+  % NewClauses => std.forall WrapperML private.derive_wrapper_instances, 
+
   if-verbose (coq.say {header} "abbreviation factory-by-classname"),
 
   NewClauses => factory.declare-abbrev Module (factory.by-classname ClassName),
@@ -738,4 +778,21 @@ mk-hb-eta.arity Structure ClassName SortProjection
   Out = parameter {coq.name->id NT} explicit Ty s\ arity (Concl s)
 ].
 
+% M is the gref of the wrapper mixin.
+% C gets now instantiated to the projection, i.e. hom_isMon_private.
+% we need to count the parameters, we can get that from the type.
+% we then can construct the instance, using
+% instance.declare-const (notably used in the API, i.e. in structures.v, 
+% HB.instance)
+pred reexport-wrapper-as-instance i:mixinname.
+reexport-wrapper-as-instance M :- std.spy-do! [
+     exported-op M _ C,
+     coq.say "???? C=" C,
+     B = (global (const C)),
+     coq.env.typeof (const C) Ty,
+     coq.count-prods Ty N0,
+     coq.term->arity Ty N0 Arity,
+     instance.declare-const "xx" B Arity _
+ ]. 
+
 }}

_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

@@ -17,6 +17,35 @@ Definition ignore_disabled {T T'} (x : T) (x' : T') := x'.
 (* ********************* structures ****************************** *)
 From elpi Require Import elpi.
 
+(******* simple example of Elpi command *)
+Axiom m : Type -> Type.
+Record r (P : Type) := { private : m P }.
+
+(* command name *)
+Elpi Command foo_example_command.
+(* predicate definition *)
+Elpi Accumulate lp:{{
+
+pred extract i:indt-decl, o:gref.
+extract (parameter ID _ _ R) Out :-
+  pi p\
+    extract (R p) Out.
+extract (record ID _ KID (field _ _ Ty (x\end-record))) GR :-
+  Ty = app [global GR| _].
+
+}}.
+Elpi Typecheck.
+
+(* predicate query *)
+Elpi Query lp:{{
+
+  coq.locate "r" (indt I),
+  coq.env.indt-decl I D,
+  extract D GR.
+
+}}.
+(******* end simple example *)
+
 Register unify as hb.unify.
 Register id_phant as hb.id.
 Register id_phant_disabled as hb.id_disabled.
@@ -159,6 +188,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