[feat] support for multiple subjects

HB/about.elpi

@@ -72,6 +72,11 @@ bulletize L F (glue [brk 0 0 | PLB]) :-
 
 % Print shortest qualified identifier of the module containing a gref
 pred pp-module i:gref, o:coq.pp.
+pp-module GR (str ID) :- wrapper-mixin GR Op WrappedMixin, !,
+  gref->modname_short WrappedMixin "." ID_W,
+  coq.gref->id Op ID_Op,
+  gref->modname_short GR "." ID_GR,
+  ID is ID_W ^ " " ^ ID_Op ^ " (* wrapped via " ^ ID_GR ^ " *)".
 pp-module GR (str ID) :- gref->modname_short GR "." ID.
 
 pred unif-hint? i:cs-instance.

HB/builders.elpi

@@ -28,7 +28,7 @@ begin CtxSkel :- std.do! [
 
 }
 
-% "end" is a keyword, be put it in the namespace by hand
+% "end" is a keyword, we put it in the namespace by hand
 pred builders.end.
 builders.end :- std.do! [
   current-mode (builder-from _ _ _ ModName),

HB/common/database.elpi

@@ -51,10 +51,10 @@ pred module-to-export_module-nice i:prop, o:id.
 module-to-export_module-nice (module-to-export _ M _) M.
 
 pred instance-to-export_instance i:prop, o:constant.
-instance-to-export_instance (instance-to-export _ _ M) M.
+instance-to-export_instance (instance-to-export _ M) M.
 
 pred instance-to-export_instance-nice i:prop, o:id.
-instance-to-export_instance-nice (instance-to-export _ M _) M.
+instance-to-export_instance-nice (instance-to-export _ M) ID :- coq.gref->id (const M) ID.
 
 pred abbrev-to-export_name i:prop, o:id.
 abbrev-to-export_name (abbrev-to-export _ N _) N.
@@ -181,6 +181,8 @@ toposort-proj.acc Proj ES Acc [A|In] Out :- std.do![
   topo-find B A => toposort-proj.acc Proj ES [B|Acc] In Out
 ].
 
+% TODO: check if topo-find-all is really needed
+
 % Classes can be topologically sorted according to the subclass relation
 pred toposort-classes.mk-class-edge i:prop, o:pair classname classname.
 toposort-classes.mk-class-edge (sub-class C1 C2 _ _) (pr C2 C1).
@@ -435,12 +437,15 @@ structure-nparams Structure NParams :-
   factory-nparams Class NParams.
 
 pred factory? i:term, o:w-args factoryname.
-factory? S (triple F Params T) :-
+factory? S (triple F Params T) :- factory?-split S F [_|Params] T _.
+
+pred factory?-split i:term, o:factoryname, o:list term, o:term, o:list term.
+factory?-split S F [global GR|Params] T Rest :-
   not (var S), !,
   safe-dest-app S (global GR) Args,
   factory-alias->gref GR F ok,
   factory-nparams F NP, !,
-  std.split-at NP Args Params [T|_].
+  std.split-at NP Args Params [T|Rest].
 
 % [find-max-classes Mixins Classes] states that Classes is a list of classes
 %   which contain all the mixins in Mixins.
@@ -460,3 +465,8 @@ find-max-classes [M|Mixins] [C|Classes] :-
   ].
 find-max-classes [M|_] _ :- coq.error "HB: cannot find a class containing mixin" M.
 
+pred is-subject-lifter i:term, o:int, o:classname.
+is-subject-lifter (global (const C)) N  Class :- exported-op M _ C, wrapper-mixin _ (const C) _, factory-nparams M N, mixin-first-class M Class.
+is-subject-lifter (app[global (const C)|_]) N Class :- exported-op M _ C, wrapper-mixin _ (const C) _, factory-nparams M N, mixin-first-class M Class.
+is-subject-lifter (global GR) N Class :- tag GR Class N, wrapper-mixin _ GR _.
+is-subject-lifter (app[global GR|_]) N Class :- tag GR Class N, wrapper-mixin _ GR _.

HB/common/synthesis.elpi

@@ -20,6 +20,7 @@ infer-all-these-mixin-args Ps T ML F SFX :- std.do! [
   std.assert-ok! (coq.typecheck F Ty) "try-infer-these-mixin-args: F illtyped",
   coq.mk-eta (-1) Ty F EtaF,
   coq.subst-fun {std.append Ps [T]} EtaF FT,
+  % coq.say "instantiate-all-these-mixin-args on" {coq.term->string FT}, 
   private.instantiate-all-these-mixin-args FT T ML SFX,
 ].
 
@@ -74,6 +75,13 @@ infer-all-args-let Ps T GR X Diag :- std.do! [
   private.instantiate-all-args-let FT T X Diag,
 ].
 
+pred try-infer-all-args-let i:list term, i:term, i:gref, o:term.
+try-infer-all-args-let Ps T GR X :- std.do! [
+  coq.env.typeof GR Ty,
+  coq.mk-eta (-1) Ty (global GR) EtaF,
+  coq.subst-fun {std.append Ps [T]} EtaF FT,
+  private.try-instantiate-all-args-let FT T X,
+].
 
 % [assert!-infer-mixin TheType M Out] infers one mixin M on TheType and
 % aborts with an error message if the mixin cannot be inferred
@@ -112,6 +120,17 @@ under-mixin-src-from-factory.do! TheType TheFactory LP :- std.do! [
   MLClauses => std.do! LP
 ].
 
+
+% Given TheType makes the provided list of mixins and instances
+% available for inference.
+pred under-these-mixin-src.do! i:term, i:list mixinname, i:list constant, o:list prop, i:list prop.
+under-these-mixin-src.do! TheType ML TheMixins ClausesHas LP :- std.do! [
+  std.map2 ML TheMixins (m\mi\c\ c = mixin-src TheType m (global (const mi))) MLClauses,
+  std.map-filter MLClauses mixin-src->has-mixin-instance ClausesHas,
+  MLClauses => std.do! LP
+].
+
+
 % Given TheType and a factory instance (on it), builds all the *new* mixins
 % provided by the factory available for and passes them to the given
 % continuation
@@ -163,6 +182,7 @@ infer-coercion-tgt (w-params.cons ID Ty F) CoeClass :-
   @pi-parameter ID Ty x\ infer-coercion-tgt (F x) CoeClass.
 infer-coercion-tgt (w-params.nil _ {{ Type }} _) sortclass.
 infer-coercion-tgt (w-params.nil _ {{ forall x, _ }} _) funclass. % do not use {{ _ -> _ }} since Funclass can be a dependent function!
+infer-coercion-tgt (w-params.nil _ T _) (grefclass _) :- name T, coq.error "The type of the structure carrier cannot be a parameter".
 infer-coercion-tgt (w-params.nil _ T _) (grefclass GR) :- coq.term->gref T GR.
 
 pred w-args.check-key i:list term, i:term, i:list (w-args A), o:prop.
@@ -184,16 +204,24 @@ namespace private {
 % the databases [mixin-src] and [from]
 pred mixin-for i:term, i:mixinname, o:term.
 mixin-for T M MICompressed :- mixin-src T M Tm, !, std.do! [
-  %if-verbose (coq.say {header} "Trying to infer mixin for" M),
+  if-verbose (coq.say {header} "Inferring mixin" M "on" T),
   std.assert-ok! (coq.typecheck Tm Ty) "mixin-for: Tm illtyped",
 
 %%%%% mterm %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-  factory? Ty (triple Factory Params _),
+  factory? Ty (triple Factory Params Subj),
+
+  if (M = Factory)
+  (
+      if-verbose (coq.say {header} "Found mixin has type" Factory "on" Subj "no need to apply a builder"),
+      MI = Tm
+  )
+  (
+      if-verbose (coq.say {header} "Found mixin has type" Factory "on" Subj "hence we apply a builder"),
 
-  if (M = Factory) (MI = Tm) (
-      private.builder->term Params T Factory M B,
-      coq.subst-fun [Tm] B MI
+      private.builder->term Params T Factory Tm M MI
+      % private.builder->term Params T Factory M B,
+      % coq.subst-fun [Tm] B MI
   ),
 
   %if-verbose (coq.say {header} "Trying to compress mixin for" {coq.term->string MI}),
@@ -231,13 +259,20 @@ mixin-for_mixin-builder (mixin-for _ _ B) B.
 % [builder->term Params TheType Src Tgt MF] finds a builder from Src to Tgt
 % and fills in all the mixins required by the builder using mixin-src, obtaining
 % a function (MF = Builder Params TheType InferredStuff : Src -> Tgt)
-pred builder->term i:list term, i:term, i:factoryname, i:mixinname, o:term.
-builder->term Ps T Src Tgt B :- !, std.do! [
+pred builder->term i:list term, i:term, i:factoryname, i:term, i:mixinname, o:term.
+% pred builder->term i:list term, i:term, i:factoryname, i:mixinname, o:term.
+builder->term Ps T Src HasSrc Tgt B :- !, std.do! [
   from Src Tgt FGR,
   F = global FGR,
   gref-deps Src MLwP,
   list-w-params_list MLwP ML,
-  infer-all-these-mixin-args Ps T ML F B,
+  if-verbose (coq.say {header} "Found builder" FGR "from" Src "to" Tgt),
+  if-verbose (coq.say {header} "Found builder" FGR "depends on" ML),
+  % infer-all-these-mixin-args Ps T ML F B,
+  coq.mk-n-holes {std.length ML} Holes,
+  coq.mk-app F {std.flatten [Ps,[T],Holes,[HasSrc]]} B,
+  std.assert-ok! (coq.typecheck B _) "builder illtyped",
+
 ].
 
 % [instantiate-all-these-mixin-args T F M_i TFX] where mixin-for T M_i X_i states that
@@ -250,8 +285,11 @@ pred instantiate-all-these-mixin-args i:term, i:term, i:list mixinname, o:term.
 instantiate-all-these-mixin-args (fun _ Tm F) T ML R :-
   coq.safe-dest-app Tm (global TmGR) _,
   factory-alias->gref TmGR M ok,
+  if-verbose (coq.say {header} "Looking at argument" M),
   std.mem! ML M,
+  % factory? Tm (triple _ _ Subj), Subj = T, % check the subject is T (do not pass T to factory?)
   !,
+  if-verbose (coq.say {header} "We have to inhabit it on" T),
   if (mixin-for T M X) true (coq.error "HB: Unable to find mixin" {nice-gref->string M} "on subject" {coq.term->string T}), !,
   instantiate-all-these-mixin-args (F X) T ML R.
 instantiate-all-these-mixin-args (fun N Ty F) T ML (fun N Ty FX) :- !,
@@ -270,6 +308,16 @@ instantiate-all-args-let (fun N Tm F) T (let N Tm X R) Diag :- !, std.do! [
 ].
 instantiate-all-args-let F _ F ok.
 
+pred try-instantiate-all-args-let i:term, i:term, o:term.
+try-instantiate-all-args-let (fun N Tm F) T (let N Tm X R) :- !, std.do! [
+  coq.safe-dest-app Tm (global TmGR) _,
+  factory-alias->gref TmGR M ok,
+  (mixin-for T M X ; true),
+  (@pi-def N Tm X m\ try-instantiate-all-args-let (F m) T (R m)),
+].
+try-instantiate-all-args-let F _ F.
+
+
 % [structure-instance->mixin-srcs TheType Structure] finds a CS instance for
 % Structure on TheType (if any) and builds mixin-src clauses for all the mixins
 % which can be candidates from that class instance. It finds instances which are

HB/common/utils-synterp.elpi

@@ -24,7 +24,9 @@ with-attributes P :-
     att "primitive" bool,
     att "non_forgetful_inheritance" bool,
     att "hnf" bool,
-  ] Opts, !,
+    att "wrapper" bool,
+    att "unsafe.univ" bool,
+ ] Opts, !,
   Opts => (save-docstring, P).
 
 pred if-verbose i:prop.

HB/common/utils.elpi

@@ -76,7 +76,7 @@ gref->modname GR NComp Sep ModName :-
   std.length Path Len,
   if (Len >= NComp) true (coq.error "Not enough enclosing modules for" {coq.gref->string GR}),
   std.take NComp Mods L,
-  std.string.concat Sep {std.rev L} ModName.
+  std.string.concat Sep {std.rev L} ModName. % TODO: check if the new_int is needed
 pred gref->modname-label i:gref, i:int, i:string, o:string.
 gref->modname-label GR NComp Sep ModName :-
   coq.gref->path GR Path,
@@ -87,6 +87,7 @@ gref->modname-label GR NComp Sep ModName :-
   std.string.concat Sep {std.rev [{coq.gref->id GR}|L]} ModName.
 
 pred string->modpath i:string, o:modpath.
+string->modpath "" _ :- !, fail. % bug is coq.locate-all if the string is empty
 string->modpath S MP :-
   std.filter {coq.locate-all S} (l\l = loc-modpath _) L,
   L = [loc-modpath MP].
@@ -96,7 +97,8 @@ gref->modname_short1 _ S [] S.
 gref->modname_short1 MP "" [X|L] L' :- gref->modname_short1 MP X L L'.
 gref->modname_short1 MP S _ S :- string->modpath S MP.
 gref->modname_short1 MP S [X|L] S' :-
-  gref->modname_short1 MP {std.string.concat "." [X,S]} L S'.
+  if (S = "") (P = X) (P is X ^ "." ^ S),
+  gref->modname_short1 MP P L S'.
 
 % Print shortest qualified identifier of the module containing a gref
 % Sep is used as separator
@@ -105,7 +107,9 @@ gref->modname_short GR Sep IDS :-
   coq.gref->path GR Path,
   string->modpath {std.string.concat "." Path} MP,
   gref->modname_short1 MP "" {std.rev Path} ID,
-  rex.replace "[.]" Sep ID IDS.
+  rex.replace "[.]" Sep ID IDS, !.
+gref->modname_short GR _ IDS :- coq.gref->id GR IDS.
+
 
 pred avoid-name-collision i:string, o:string.
 avoid-name-collision S S1 :-
@@ -294,7 +298,7 @@ pack? (indc K) C :-
   coq.env.indc K _ _ _ KTy, prod-last-gref KTy (indt I), % TODO: use new API
   class-def (class C (indt I) _).
 
-pred distribute-w-params i:list-w-params A, o:list (one-w-params A).
+pred distribute-w-params i:w-params (list A), o:list (w-params A).
 distribute-w-params (w-params.cons N T F) L :-
   pi x\ distribute-w-params (F x) (L1 x), std.map (L1 x) (bind-cons N T x) L.
 distribute-w-params (w-params.nil N T F) L :-
@@ -316,6 +320,18 @@ re-enable-id-phant T T1 :-
   (pi f1 f2 t v\ copy {{lib:@hb.ignore_disabled lp:t lp:f1 lp:v lp:f2}} {{lib:@hb.ignore lp:t lp:v}} :- !) =>
   copy T T1.
 
+pred disable-id-phant-indt-decl i:indt-decl, o:indt-decl.
+disable-id-phant-indt-decl D D1 :-
+  (pi fresh fresh1 t v\ copy {{lib:@hb.id lp:t lp:v}} {{lib:@hb.id_disabled lp:t lp:fresh lp:v lp:fresh1}} :- !) =>
+  (pi fresh fresh1 t v\ copy {{lib:@hb.ignore lp:t lp:v}} {{lib:@hb.ignore_disabled lp:t lp:fresh lp:v lp:fresh1}} :- !) =>
+  copy-indt-decl D D1.
+
+pred re-enable-id-phant-indt-decl i:indt-decl, o:indt-decl.
+re-enable-id-phant-indt-decl D D1 :-
+  (pi f1 f2 t v\ copy {{lib:@hb.id_disabled lp:t lp:f1 lp:v lp:f2}} {{lib:@hb.id lp:t lp:v}} :- !) =>
+  (pi f1 f2 t v\ copy {{lib:@hb.ignore_disabled lp:t lp:f1 lp:v lp:f2}} {{lib:@hb.ignore lp:t lp:v}} :- !) =>
+  copy-indt-decl D D1.
+
 pred prod-last i:term, o:term.
 prod-last (prod N S X) Y :- !, @pi-decl N S x\ prod-last (X x) Y.
 prod-last X X :- !.
@@ -325,8 +341,19 @@ prod-last-gref (prod N S X) GR :- !, @pi-decl N S x\ prod-last-gref (X x) GR.
 prod-last-gref X GR :- coq.term->gref X GR.
 
 % saturate a type constructor with holes
-pred saturate-type-constructor i:term, o:term .
-saturate-type-constructor T ET :- 
+pred saturate-type-constructor i:int, i:term, o:term .
+saturate-type-constructor 0 T ET :- !,
   coq.typecheck T TH ok,
   coq.count-prods TH N,
   coq.mk-app T {coq.mk-n-holes N} ET.
+saturate-type-constructor N T ET :- 
+  coq.mk-app T {coq.mk-n-holes N} ET.
+
+
+pred with-unsafe-univ i:prop.
+with-unsafe-univ P :- get-option "unsafe.univ" tt, !,
+  coq.option.get ["Universe","Checking"] Old,
+  coq.option.set ["Universe","Checking"] (coq.option.bool ff),
+  P,
+  coq.option.set ["Universe","Checking"] Old.
+with-unsafe-univ P :- P.

HB/context.elpi

@@ -57,6 +57,40 @@ namespace private {
 % to the corresponding mixin using mixin-for
 pred postulate-mixin i:term, i:w-args mixinname, i:triple (list constant) (list prop) (list (w-args mixinname)),
                      o:triple (list constant) (list prop) (list (w-args mixinname)).
+
+postulate-mixin TheType (triple M Ps T) (triple CL MSL MLwP) (triple OutCL [MC|MSL] [NewMwP|MLwP]) :- wrapper-mixin M _ _, !, MSL => std.do! [
+  NameVar is "local_mixin_private_" ^ {gref->modname M 2 "_"},
+  NameMixin is "local_mixin_" ^ {gref->modname M 2 "_"},
+
+  if-verbose (coq.say "HB: postulate and wrap" NameVar "on" {coq.term->string T}),
+
+  synthesis.infer-all-gref-deps Ps T M TySkel,
+  % was synthesis.infer-all-mixin-args Ps T M TySkel,
+  % if-verbose (coq.say "HB: postulate-mixin checking" TySkel),
+  % std.assert-ok! (coq.typecheck Ty _) "postulate-mixin: Ty illtyped",
+  std.assert-ok! (coq.elaborate-ty-skeleton TySkel _ Ty)
+    "postulate-mixin: Ty illtyped",
+
+  Ty = app[global M|Args],
+  factory-constructor M K,
+  coq.mk-app (global K) Args KArgs,
+  std.assert-ok! (coq.typecheck KArgs {{ lp:VarTy -> _ }}) "brrr",
+
+  log.coq.env.add-section-variable-noimplicits NameVar VarTy V,
+
+  coq.mk-app KArgs [global (const V)] TheMixin,
+
+  log.coq.env.add-const-noimplicits NameMixin TheMixin Ty @transparent! C,
+
+  factory? Ty NewMwP,
+
+  declare-instances-from-postulated-mixin TheType M T C MC NewCL,
+
+  std.append CL NewCL OutCL,
+
+].
+
+
 postulate-mixin TheType (triple M Ps T) (triple CL MSL MLwP) (triple OutCL [MC|MSL] [NewMwP|MLwP]) :- MSL => std.do! [
   Name is "local_mixin_" ^ {gref->modname M 2 "_"},
 
@@ -70,11 +104,19 @@ postulate-mixin TheType (triple M Ps T) (triple CL MSL MLwP) (triple OutCL [MC|M
     "postulate-mixin: Ty illtyped",
   log.coq.env.add-section-variable-noimplicits Name Ty C,
   factory? Ty NewMwP,
+
+  declare-instances-from-postulated-mixin TheType M T C MC NewCL,
+
+  std.append CL NewCL OutCL,
+
+  ].
+
+pred declare-instances-from-postulated-mixin i:term, i:mixinname, i:term, i:constant, o:prop, o:list constant.
+declare-instances-from-postulated-mixin TheType M T C MC NewCL :- std.do! [
 
   MC = mixin-src T M (global (const C)),
   MC => get-option "local" tt =>
-    instance.declare-all TheType {findall-classes-for [M]} NewCSL,
-  std.map NewCSL snd NewCL,
-  std.append CL NewCL OutCL
-  ].
+    instance.declare-all TheType {findall-classes-for [M]} NewCL,
+].
+
 }}

HB/export.elpi

@@ -47,7 +47,7 @@ export.reexport-all-modules-and-CS Filter :- std.do! [
   std.forall2 NiceMods Mods log.coq.env.export-module,
 
 
-  std.findall (instance-to-export File NiceInstance_ Const_) InstCL,
+  std.findall (instance-to-export File Const_) InstCL,
   std.filter {std.list-uniq InstCL} (export.private.instance-in-module MFilter) InstCLFiltered,
   std.map InstCLFiltered instance-to-export_instance Insts,
 
@@ -83,7 +83,7 @@ module-in-module PM (module-to-export _ _ M) :-
   std.appendR PM _ PC. % sublist
 
 pred instance-in-module i:list string, i:prop.
-instance-in-module PM (instance-to-export _ _ C) :-
+instance-in-module PM (instance-to-export _ C) :-
   coq.gref->path (const C) PC,
   std.appendR PM _ PC. % sublist