[refactor] instance declaration

HB/common/database.elpi

@@ -179,12 +179,20 @@ toposort-proj Proj ES In Out :- !, toposort-proj.acc Proj ES [] In Out.
 pred topo-find i:B, o:A.
 pred toposort-proj.acc i:(A -> B -> prop), i:list (pair B B), i:list B, i:list A, o:list A.
 toposort-proj.acc _ ES Acc [] Out :- !,
-  std.map {std.toposort ES Acc} topo-find Out.
+  std.map {std.toposort ES Acc} topo-find-all Out.
 toposort-proj.acc Proj ES Acc [A|In] Out :- std.do![
   Proj A B,
   topo-find B A => toposort-proj.acc Proj ES [B|Acc] In Out
 ].
 
+pred topo-find-all i:B, o:A.
+topo-find-all B A :- std.do! [
+  std.findall (topo-find B C_) L,
+  % if there were dusplicates, we ensure we keep the most instantiated, eg
+  % (triple m [X,Y] t) v.s. (triple m [a,b] t)
+  std.assert! (std.forall L (x\ x = topo-find B A)) "topofind bad",
+].
+
 % 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).
@@ -438,11 +446,14 @@ structure-nparams Structure NParams :-
   class-def (class Class Structure _),
   factory-nparams Class NParams.
 
+pred factory?-split i:term, o:factoryname, o:list term, o:term, o:list term.
+factory?-split (app[global GR|Args]) F [global GR|Params] T Rest :-
+  factory-alias->gref GR F, factory-nparams F NP, !,
+  std.split-at NP Args Params [T|Rest].
+
 pred factory? i:term, o:w-args factoryname.
 factory? S (triple F Params T) :-
-  not (var S), !,
-  safe-dest-app S (global GR) Args, factory-alias->gref GR F, factory-nparams F NP, !,
-  std.split-at NP Args Params [T|_].
+  factory?-split S F [_|Params] T _.
 
 % [find-max-classes Mixins Classes] states that Classes is a list of classes
 %   which contain all the mixins in Mixins.
@@ -462,3 +473,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/phant-abbreviation.elpi

@@ -27,6 +27,12 @@ add-abbreviation N (private.phant-term AL T1) C Abbrev :- std.do! [
   private.build-abbreviation 0 (global (const C)) AL NParams AbbrevT,
   @global! => log.coq.notation.add-abbreviation N NParams AbbrevT tt Abbrev,
 ].
+pred add-abbreviation2 i:gref, i:string, i:phant-term, o:constant, o:abbreviation.
+add-abbreviation2 GR N (private.phant-term _ _) C Abbrev :- std.do! [
+  NC is "phant_" ^ N,
+  log.coq.env.add-const-noimplicits NC (global GR) _ @transparent! C,
+  @global! => log.coq.notation.add-abbreviation N 0 (global (const C)) tt Abbrev,
+].
 
 % [of-gref WithCopy GR RealMixinArgs PT]
 % builds a phant-term taking all parameters,

HB/common/synthesis.elpi

@@ -74,6 +74,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
@@ -103,6 +110,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
@@ -242,6 +260,7 @@ instantiate-all-these-mixin-args (fun _ Tm F) T ML R :-
   coq.safe-dest-app Tm (global TmGR) _,
   factory-alias->gref TmGR M,
   std.mem! ML M,
+  factory? Tm (triple _ _ Subj), Subj = T, % check the subject is T (do not pass T to factory?)
   !,
   mixin-for T M X, !,
   instantiate-all-these-mixin-args (F X) T ML R.
@@ -261,6 +280,15 @@ 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,
+  (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,6 +24,8 @@ with-attributes P :-
     att "primitive" bool,
     att "non_forgetful_inheritance" bool,
     att "hnf" bool,
+    att "wrapper" bool,
+    att "unsafe.univ" bool,
   ] Opts, !,
   Opts => (save-docstring, P).
 

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 [{std.any->string {new_int}}|L]} ModName.
 pred gref->modname-label i:gref, i:int, i:string, o:string.
 gref->modname-label GR NComp Sep ModName :-
   coq.gref->path GR Path,
@@ -293,7 +293,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 :-
@@ -315,6 +315,46 @@ 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 failsafe-structure-inference i:term, o:term.
+failsafe-structure-inference T T1 :-
+  (pi T T2 F_Params F_Params1 Args Args1 Subject Subject1 NP ArgsOp ArgsOp1 OP S\
+    copy T T2 :-
+      factory?-split T _ F_Params Subject Args,
+      std.map F_Params copy F_Params1,
+      std.map Args copy Args1,
+      is-subject-lifter Subject NP Class,
+      coq.safe-dest-app Subject OP ArgsOp,
+      std.nth NP ArgsOp S,
+      (var S ; name S), % TODO: should be the subject of the structure, not a random name
+      !,
+      eta-structure-record S NP Class ArgsOp ArgsOp1,
+      coq.mk-app OP ArgsOp1 Subject1,
+      coq.mk-app (app F_Params1) [Subject1|Args1] T2) =>
+  copy T T1.
+
+pred eta-structure-record i:term, i:int, i:classname, i:list term, o:list term.
+eta-structure-record S NP Class L L1 :-
+  std.split-at NP L Params [_|Rest],
+  class-def (class Class Structure _),
+  get-constructor Structure K,
+  std.map Params copy Params1,
+  std.map Rest copy Rest1,
+  coq.mk-app {coq.env.global K} {std.append Params1 [S,_]} EtaS,
+  std.append Params1 [EtaS|Rest1] L1.
+
 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 :- !.
@@ -329,3 +369,12 @@ saturate-type-constructor T ET :-
   coq.typecheck T TH ok,
   coq.count-prods TH N,
   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,38 @@ 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 "_"},
 
@@ -69,12 +101,22 @@ postulate-mixin TheType (triple M Ps T) (triple CL MSL MLwP) (triple OutCL [MC|M
   std.assert-ok! (coq.elaborate-ty-skeleton TySkel _ Ty)
     "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
-  ].
+].
+
 }}

HB/factory.elpi

@@ -219,6 +219,53 @@ 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 _ Ty R) Out :-
+  @pi-parameter ID Ty p\
+    extract_from_record_decl P (R p) Out.
+extract_from_record_decl P (record _ _ _ (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 N Ty TF) Out1 :-
+  @pi-decl N Ty 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 :-
+  % TODO: use factory? from database.elpi
+  Ty = (app [global Gr0| Args]),
+  factory-alias->gref Gr0 Gr1,
+  factory-nparams Gr1 N,
+  std.nth N Args (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
@@ -229,6 +276,8 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
   RDeclSkel = record "axioms_" Sort1 Kname Fields,
   std.assert-ok! (coq.elaborate-indt-decl-skeleton RDeclSkel RDecl) "record declaration illtyped",
 
+  % scheck-no-mixin-or-factory-occurs RDecl,
+
   abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-indt-decl RDecl RDeclClosed _,
 
 
@@ -255,6 +304,12 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
 
   % TODO: should this be in the Exports module?
 
+  % if the wrapper option is on, build the wrapper clause 
+  if (get-option "wrapper" tt)
+     ((wrapper_mixin_aux (indt R) NSbj WMxn),
+      (WrapperClauses = [wrapper-mixin (indt R) NSbj WMxn]))
+     (WrapperClauses = []),
+
   if-verbose (coq.say {header} "declare notation Build"),
 
   GRDepsClauses => phant.of-gref ff GRK [] PhGRK,
@@ -271,7 +326,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,