diff --git a/HB/about.elpi b/HB/about.elpi index b3c3b071..c5030718 100644 --- a/HB/about.elpi +++ b/HB/about.elpi @@ -73,6 +73,11 @@ bulletize L F (glue [brk 0 0 | PLB]) :- % Print shortest qualified identifier of the module containing a gref func pp-module gref -> 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. func unif-hint? cs-instance -> . diff --git a/HB/builders.elpi b/HB/builders.elpi index 56aeec11..9081d0c3 100644 --- a/HB/builders.elpi +++ b/HB/builders.elpi @@ -28,7 +28,7 @@ begin CtxSkel :- } -% "end" is a keyword, be put it in the namespace by hand +% "end" is a keyword, we put it in the namespace by hand func builders.end. builders.end :- std.do! [ current-mode (builder-from _ _ _ ModName), diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 1b299919..b8fbf849 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -51,10 +51,10 @@ func module-to-export_module-nice prop -> id. module-to-export_module-nice (module-to-export _ M _) M. func instance-to-export_instance prop -> constant. -instance-to-export_instance (instance-to-export _ _ M) M. +instance-to-export_instance (instance-to-export _ M) M. func instance-to-export_instance-nice prop -> 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. func abbrev-to-export_name prop -> id. abbrev-to-export_name (abbrev-to-export _ N _) N. @@ -77,6 +77,10 @@ sub-class? (class C1 _ ML1P) (class C2 _ ML2P) :- list-w-params_list ML2P ML2, std.forall ML2 (m2\ std.exists! ML1 (m1\ m1 = m2)). +func sub-classname? classname, classname -> . +sub-classname? C1 C2 :- + sub-class? {classname->def C1} {classname->def C2}. + % [factory-provides F MLwP] computes the mixins MLwP generated by F func factory-provides factoryname -> mixins. factory-provides FactoryAlias MLwP :- std.do! [ @@ -177,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 func toposort-classes.mk-class-edge prop -> pair classname classname. toposort-classes.mk-class-edge (sub-class C1 C2 _ _) (pr C2 C1). @@ -439,12 +445,15 @@ structure-nparams Structure NParams :- factory->nparams Class NParams. func factory? term -> w-args factoryname. -factory? S (triple F Params T) :- +factory? S (triple F Params T) :- factory?-split S F [_|Params] T _. + +func factory?-split term -> factoryname, list term, term, 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. @@ -464,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 _. diff --git a/HB/common/synthesis.elpi b/HB/common/synthesis.elpi index 8a0b5752..500d6a3c 100644 --- a/HB/common/synthesis.elpi +++ b/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,12 +75,19 @@ 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 -func assert!-infer-mixin term, mixinname -> term. -assert!-infer-mixin T M B :- - if (private.mixin-for T M B) +func assert!-infer-mixin term, mixinname -> term, term. +assert!-infer-mixin T M B Ty :- + if (private.mixin-for T M B Ty) true (coq.error "HB: cannot inhabit mixin" {nice-gref->string M} "on"{coq.term->string T}). @@ -96,7 +104,7 @@ local-canonical-mixins-of.aux T [S|Ss] MSL'' :- std.do! [ ]. func local-canonical-mixins-of term -> list prop. -local-canonical-mixins-of T MSL :- std.do! [ +local-canonical-mixins-of T MSL :- std.time-do! "local-canonical-mixins-of" [ get-canonical-structures T CS, std.map CS (s\c\ sigma w\ class-def (class c s w)) Cl, toposort-classes Cl ClSorted, @@ -112,6 +120,17 @@ under-mixin-src-from-factory.do! TheType TheFactory LP :- std.map ML (m\c\ c = mixin-src TheType m TheFactory) MLClauses, 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. :index (_ _ 2) @@ -183,18 +203,26 @@ namespace private { % [mixin-for T M MI] synthesizes an instance of mixin M on type T using % the databases [mixin-src] and [from] -func mixin-for term, mixinname -> term. -mixin-for T M MICompressed :- mixin-src T M Tm, !, +func mixin-for term, mixinname -> term, term. +mixin-for T M MICompressed MICompressedTy :- mixin-src T M Tm, !, %if-verbose (coq.say {header} "Trying to infer mixin for" M), 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) (MI = Tm) ( - private.builder->term Params T Factory M B, - coq.subst-fun [Tm] B MI + if (M = Factory) + ( + if-verbose (coq.say {header} "Found mixin has type" Factory "on" Subj "no need to apply a builder"), + MI = Tm, MICompressedTy = Ty + ) + ( + if-verbose (coq.say {header} "Found mixin has type" Factory "on" Subj "hence we apply a builder"), + + private.builder->term Params T Factory Tm M MI MITy, MICompressedTy = MITy + % 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}), @@ -226,18 +254,25 @@ compress-coercion-paths MI MICompressed :- (MI = MICompressed). func mixin-for_mixin-builder prop -> term. -mixin-for_mixin-builder (mixin-for _ _ B) B. +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) -func builder->term list term, term, factoryname, mixinname -> term. -builder->term Ps T Src Tgt B :- !, std.do! [ +func builder->term list term, term, factoryname, term, mixinname -> term, term. +builder->term Ps T Src HasSrc Tgt B1 BTy :- !, 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.time (std.assert-ok! (coq.typecheck B BTy) "builder illtyped") _Time1, + B = B1 + ]. % [instantiate-all-these-mixin-args T F M_i TFX] where mixin-for T M_i X_i states that @@ -250,9 +285,12 @@ func instantiate-all-these-mixin-args term, term, list mixinname -> 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 (mixin-for T M X) true (coq.error "HB: Unable to find mixin" {nice-gref->string M} "on subject" {coq.term->string T}), !, + 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) :- !, @pi-decl N Ty m\ instantiate-all-these-mixin-args (F m) T ML (FX m). @@ -262,7 +300,7 @@ func instantiate-all-args-let term, term -> term, diagnostic. instantiate-all-args-let (fun N Tm F) T (let N Tm X R) Diag :- !, std.do! [ coq.safe-dest-app Tm (global TmGR) _, factory-alias->gref TmGR M ok, - if (mixin-for T M X) + if (mixin-for T M X _) (@pi-def N Tm X m\ instantiate-all-args-let (F m) T (R m) Diag) (Diag = error Msg, Msg is "cannot synthesize mixin " ^ {nice-gref->string M} ^ @@ -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 @@ -315,7 +363,7 @@ structure-instance->mixin-srcs.aux T F CL :- % which can be generated by the factory instance FI which are not part of % OldMixins (that is, the contribution of FI to the current context) func factory-instance->new-mixins list mixinname, term -> list mixinname. -factory-instance->new-mixins OldMixins X NewML :- +factory-instance->new-mixins OldMixins X NewML :- std.time-do! "factory-instance->new-mixins" [ std.assert-ok! (coq.typecheck X XTy) "mixin-src: X illtyped", if (not (coq.safe-dest-app XTy (global _) _)) (coq.error "Term:\n" {coq.term->string X} @@ -325,6 +373,7 @@ factory-instance->new-mixins OldMixins X NewML :- coq.term->gref XTy Src, factory-provides Src MLwP, list-w-params_list MLwP ML, - std.filter ML (m\ not(std.mem! OldMixins m)) NewML. + std.filter ML (m\ not(std.mem! OldMixins m)) NewML, +]. }} diff --git a/HB/common/utils-synterp.elpi b/HB/common/utils-synterp.elpi index 014d513c..9e49d6fb 100644 --- a/HB/common/utils-synterp.elpi +++ b/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). func if-verbose (func) -> . diff --git a/HB/common/utils.elpi b/HB/common/utils.elpi index 07d859b3..1f221106 100644 --- a/HB/common/utils.elpi +++ b/HB/common/utils.elpi @@ -95,6 +95,7 @@ cs-pattern->name (cs-gref GR) Name :- gref->modname-label GR 1 "_" Name. func string->modpath string -> modpath. +string->modpath "" _ :- !, fail. % bug in 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]. @@ -104,7 +105,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 @@ -113,7 +115,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. + func avoid-name-collision string -> string. avoid-name-collision S S1 :- @@ -314,7 +318,7 @@ pack? (indc K) C :- coq.env.indc K _ _ _ KTy, prod-last-gref KTy (indt I), % TODO: use new API std.once (class-def (class C (indt I) _)). -func distribute-w-params list-w-params A -> list (one-w-params A). +func distribute-w-params w-params (list A) -> 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 :- @@ -336,6 +340,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. +func disable-id-phant-indt-decl indt-decl -> 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. + +func re-enable-id-phant-indt-decl indt-decl -> 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. + func prod-last term -> term. prod-last (prod N S X) Y :- !, @pi-decl N S x\ prod-last (X x) Y. prod-last X X :- !. @@ -345,8 +361,56 @@ 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 -func saturate-type-constructor term -> term. -saturate-type-constructor T ET :- +func saturate-type-constructor int, term -> 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. + +pred time-ctx o:string. +func time-ctx->id (pred) -> string. +time-ctx->id (time-ctx S) S. + +func with-time string, (func). +with-time Cmd P :- + std.once(get-option "elpi.loc" L), + loc.fields L File _ _ Line _, + std.any->string Line LineS, + Header is File ^ ": " ^ LineS ^ ": " ^ Cmd ^ ": ", + time-ctx Header => P. + +func std.time-do!-report float -> . +std.time-do!-report Begin :- std.do! [ + gettimeofday End, + T is End - Begin, + std.findall (time-ctx _) CTX, + std.map CTX time-ctx->id CTXS, + std.rev CTXS [Header | Rest], + coq.say {calc (Header ^ {std.string.concat "." Rest} ^": " ^ {std.any->string T})} +]. + +func std.time-do! string, list (pred). +std.time-do! S L :- get-option "verbose" tt, !, + gettimeofday Begin, + time-ctx S => if (std.do! L) (std.time-do!-report Begin) (std.time-do!-report Begin, fail). +std.time-do! _ L :- !, std.do! L. + +func term->size term -> int. +term->size (app L) N :- !, + std.fold {std.map L term->size} 0 (x\a\r\r is x + a) M, + N is M + 1. +term->size (fun _ T B) O :- !, term->size T N, pi x\ term->size (B x) M, O is N + M + 1. +term->size (prod _ T B) O :- !, term->size T N, pi x\ term->size (B x) M, O is N + M + 1. +term->size (let _ T X B) O :- !, term->size T N, term->size X N', pi x\ term->size (B x) M, O is N + N' + M + 1. +term->size _ 1. \ No newline at end of file diff --git a/HB/context.elpi b/HB/context.elpi index 28c917d0..9940498c 100644 --- a/HB/context.elpi +++ b/HB/context.elpi @@ -59,6 +59,40 @@ namespace private { :index (1) func postulate-mixin term, w-args mixinname, triple (list constant) (list prop) (list (w-args mixinname)) -> 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 "_"}, @@ -72,11 +106,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, +]. + }} diff --git a/HB/export.elpi b/HB/export.elpi index fc66845b..a14639f1 100644 --- a/HB/export.elpi +++ b/HB/export.elpi @@ -48,7 +48,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, @@ -89,7 +89,7 @@ module-in-module PM (module-to-export _ _ M) :- prefixL PM PC. func instance-in-module list string, prop ->. -instance-in-module PM (instance-to-export _ _ C) :- +instance-in-module PM (instance-to-export _ C) :- coq.gref->path (const C) PC, prefixL PM PC. diff --git a/HB/factory.elpi b/HB/factory.elpi index cd8794b9..4365137e 100644 --- a/HB/factory.elpi +++ b/HB/factory.elpi @@ -245,6 +245,53 @@ declare-asset Arg AssetKind :- std.do! [ ) ]. +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%% auxiliary code for wrapper-mixin + +func extract_from_record_decl (func term -> gref), indt-decl -> 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. + +func extract_from_rtty (func term -> gref), term -> 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. + +func xtr_fst_op term -> gref. +xtr_fst_op Ty Gr1 :- + Ty = (app [global Gr0| _]), + factory-alias->gref Gr0 Gr1 ok. + +func xtr_snd_op term -> gref. +xtr_snd_op Ty Gr :- + % TODO: use factory? from database.elpi + Ty = (app [global Gr0| Args]), + factory-alias->gref Gr0 Gr1 ok, + factory->nparams Gr1 N, + std.nth N Args (app [global Gr| _]). + +func extract_wrapped indt-decl -> gref. +extract_wrapped In Out :- + extract_from_record_decl (extract_from_rtty xtr_fst_op) In Out. + +func extract_subject indt-decl -> gref. +extract_subject In Out :- + extract_from_record_decl (extract_from_rtty xtr_snd_op) In Out. + +func wrapper_mixin_aux gref -> gref, 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 @@ -266,7 +313,7 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance % since closing the section purges the unused universe level we may have % allocated by typechecking the skeleton just above - coq.env.indt R tt _ _ _ [K] _, + coq.env.indt R tt _ _ _ [K] [KTy], GRK = indc K, @global! => log.coq.arguments.set-implicit (indt R) [[]], @global! => log.coq.arguments.set-implicit GRK [[]], @@ -276,11 +323,22 @@ 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], + % check mlwp is minimal to cover the operators used in KTy + if (D = asset-mixin) + (warn-unneeded-dep NParams KTy {list-w-params_list MLwP}) + true, % we should wait HB.end in order to know what is really useless + % GRDepsClauses => mk-factory-sort MLwP (indt R) _ FactorySortCoe, % FactorySortCoe = coercion GRFSort _ _ _, % 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, @@ -297,7 +355,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, [ is-factory (indt R), factory->constructor (indt R) GRK, factory->nparams (indt R) NParams, @@ -323,6 +381,75 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance GRDepsClauses => declare-abbrev Module FactAbbrev _, ]. +func ops-in-term term -> coq.gref.set. +ops-in-term T S :- + (pi C X A A1\ + fold-map (global (const C) as X) A X A1 :- exported-op _ _ C, !, coq.gref.set.add (const C) A A1) => + fold-map T {coq.gref.set.empty} _ S. + +func mixin-has-op-in coq.gref.set, mixinname -> . +mixin-has-op-in S M :- + exported-op M _ C, coq.gref.set.mem (const C) S, !. + +func covers list mixinname -> list classname. +covers Needed CL :- + coq.gref.list->set Needed NeededS, + findall-classes-for Needed AllCDefs, + std.map AllCDefs class_name AllC, + std.filter AllC (c\ sigma Cov\ class-coverage [c] Cov, coq.gref.set.subset NeededS Cov) CL. + +func not-covers list mixinname, classname -> pair (list mixinname) classname. +not-covers ML C (pr EM C) :- + classname->mixins C CMLwP, + list-w-params_list CMLwP CML, + std.filter ML (m\not(std.mem! CML m)) EM, (not(EM = [])). + +func longer-excluded (pair (list mixinname) classname), (pair (list mixinname) classname) -> . +longer-excluded (pr L1 _) (pr L2 _) :- {std.length L1} < {std.length L2}. + +{ + +shorten coq.pp.{ str, h, v, hov, spc, nl, box, brk }. + +func pp-better-dep pair (list mixinname) classname -> coq.pp. +pp-better-dep (pr ML C) PP :- + nice-gref->string C CS, + std.map ML nice-gref->string MLS, + std.map MLS (x\r\ r = str x) MLP, + PP = box h [str "- class", spc, str CS, spc, str "leaves out unneeded mixins:", spc | {std.intersperse spc MLP} ]. + +func better-deps->string list mixinname, list mixinname, list (pair (list mixinname) classname) -> string. +better-deps->string Needed ML BD S :- + std.map ML nice-gref->string MLS, std.map MLS (x\r\ r = str x) MLP, + std.map Needed nice-gref->string NeededS, std.map NeededS (x\r\ r = str x) NP, + MLPP = box h [str "Unneeded dependencies:", spc |{std.intersperse spc MLP}], + if (BD = []) + (FIXES = [box (hov 2) [str "- no existing class, you may create one for", spc|{std.intersperse spc NP}]]) + (FIXES = {std.intersperse (brk 0 0) {std.map BD pp-better-dep}}), + PP = box (v 0) [MLPP, brk 0 0, str"Proposed fixes:", brk 0 0 | FIXES], + coq.pp->string PP S. +} + +func keep-minimals list classname, list classname -> list classname. +keep-minimals [] X X. +keep-minimals [X|XS] A R :- std.exists A (sub-classname? X), !, keep-minimals XS A R. +keep-minimals [X|XS] A R :- keep-minimals XS [X|A] R. + +func warn-unneeded-dep int, term, list mixinname -> . +warn-unneeded-dep 0 Ty L :- !, std.do! [ + ops-in-term Ty OPS, + std.partition L (mixin-has-op-in OPS) Needed Extra, + covers Needed CoversUnsorted, + toposort-classes CoversUnsorted Covers, + keep-minimals Covers [] MinimalCovers, + std.map-filter MinimalCovers (not-covers Extra) BetterDeps, + if (Extra = []) true + (coq.warning "HB" "HB.unneded-dependency" {better-deps->string Needed Extra BetterDeps}) +]. +warn-unneeded-dep N (prod Na T F) L :- !, M is N - 1, + @pi-decl Na T x\ + warn-unneeded-dep M (F x) L. +warn-unneeded-dep _ T _ :- coq.error "warn-unneeded-dep" T. :index (1) func declare-factory-alias list prop, list constant, list term, term, diff --git a/HB/instance.elpi b/HB/instance.elpi index f7f6eb1a..7266bd10 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -3,6 +3,7 @@ namespace instance { +% DEPRECATED % [declare-existing T F] equips T with all the canonical structures that can be % built using factory instance F func declare-existing argument, argument ->. @@ -22,8 +23,8 @@ declare-existing T0 F0 :- std.do! [ % and equips the type the factory is used on with all the canonical structures % that can be built using factory instance B. CFL contains the list of % factories being defined, CSL the list of canonical structures being defined. -func declare-const id, term, arity -> list (pair id constant), list (pair id constant). -declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [ +func declare-const id, term, arity -> list constant, list constant. +declare-const Name BodySkel TyWPSkel CFL CSL :- std.time-do! "declare-const" [ std.assert-ok! (coq.elaborate-arity-skeleton TyWPSkel _ TyWP) "Definition type illtyped", coq.arity->term TyWP Ty, std.assert-ok! (coq.elaborate-skeleton BodySkel Ty Body) "Definition illtyped", @@ -59,29 +60,73 @@ declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [ ]) (SectionTy = SectionTyUnfolded), % call HB.instance TheType TheFactory - std.drop NParams Args [TheType|_], + std.drop NParams Args [TheTypeAsInferred|_], - if (var TheType) + + if (var TheTypeAsInferred) (coq.error "HB: The instance subject must be explicitly given.\nUse:\n HB.instance Definition _ : M := ...\n HB.instance Definition _ := M.Build ...") true, + private.expose-real-subject TheTypeAsInferred TheType, + + coq.term->string TheType TheTypeStr1, + rex.replace " " "_" TheTypeStr1 TheTypeStr, + log.coq.env.add-const-noimplicits-failondup RealName OptimizedBody SectionTyUnfolded @transparent! C, TheFactory = (global (const C)), private.check-non-forgetful-inheritance TheType Factory, - private.declare-instance Factory TheType TheFactory Clauses CFL CSL, - - if (CSL = []) - (coq.warning "HB" "HB.no-new-instance" "HB: no new instance is generated") - true, - - % 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 - ), + time-ctx TheTypeStr => if (current-mode (builder-from TheType TheFactoryForBuilderSection FGR _)) + % instance in a builder section for this subject %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + (std.do![ + if (get-option "local" tt) + (coq.error "HB: declare-instance: cannot make builders local. If you want temporary instances, make an alias, e.g. with let T' := T") true, + + private.declare-canonical-instances-from-factory-and-local-builders + Factory TheType TheFactory TheFactoryForBuilderSection FGR NM_CFL MsClauses CSL, + + std.map NM_CFL snd CFL, + + std.map NM_CFL (x\c\sigma N MixinName C\ new_int N, x = pr MixinName C, c = builder-decl (builder N FGR MixinName (const C))) BdClauses, + + std.append MsClauses BdClauses Clauses, + + private.close-section-if-has-params TyWP SectionName, + CSL2 = [], + ]) + % instance in regular section %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + (std.do![ + + % derive all mixins the factory provides + private.declare-mixins-from-factory Factory TheType TheFactory ML TheMixins, + private.declare-regular-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL, + + % regular instance %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + if (get-option "wrapper" ff ; not(is-subject-lifter TheTypeAsInferred _ _)) + % regular subject %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + ( if-verbose (coq.say {header} "Not a lifted subject" {coq.term->string TheTypeAsInferred}), + WMsClauses = [], WBdClauses = [], ClausesHas2 = [], CSL2 = []) + % wrapper %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + (private.declare-wrapper-inst TheTypeAsInferred ML TheMixins TyWP SectionName ClausesHas2 CSL2 WM WMC, + if (current-mode (builder-from TheLiftedType _ FGR _)) % we are in a builder section + ( % TODO: should we verify that TheLiftedType is what we obtain by wrapping? + std.map2 WM WMC (MixinName\C\c\sigma N\ new_int N, c = builder-decl (builder N FGR MixinName (const C))) WBdClauses, + std.map2 WM WMC (MixinName\C\c\c = mixin-src TheLiftedType MixinName (global (const C))) WMsClauses + ) + (WMsClauses = [], WBdClauses = [])) + , + CFL = CSL, % ??? + + % shared to all branches + if (get-option "export" tt) + (coq.env.current-library File, + std.map {std.append CSL CSL2} (c\r\ r = instance-to-export File c) ClausesExp) + (ClausesExp = []), + + std.flatten [ClausesHas, ClausesHas2, ClausesExp, WMsClauses, WBdClauses] Clauses, + ]), % we accumulate clauses now that the section is over acc-clauses current Clauses @@ -97,11 +142,11 @@ not-subclass-of HasNoInstance (class C _ _) :- not(sub-class C HasNoInstance _ _ % rest. For each fulfilled class it declares a local constant inhabiting the % corresponding structure and declares it canonical. % Each mixin used in order to fulfill a class is returned together with its name. -func declare-all term, list hbclass -> list (pair id constant). +func declare-all term, list hbclass -> list constant. declare-all _ [] []. declare-all T [class _ Struct _|Rest] L :- has-instance T Struct, !, declare-all T Rest L. -declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :- +declare-all T [class Class Struct MLwP|Rest] [CS|L] :- infer-class T Class Struct MLwP S Name STy Clauses, !, decl-const-in-struct Name S STy CS, Clauses => declare-all T Rest L. @@ -113,28 +158,32 @@ declare-all T [class HasNoInstance _ _|Rest] L :- % for generic types, we need first to instantiate them by giving them holes, % so they can be used to instantiate the classes -:index (_ 2) -func declare-all-on-type-constructor term, list hbclass -> list (pair id constant). -declare-all-on-type-constructor _ [] []. -declare-all-on-type-constructor TK [class _ Struct _|Rest] L :- saturate-type-constructor TK T, has-instance T Struct, !, - declare-all-on-type-constructor TK Rest L. -declare-all-on-type-constructor TK [class Class Struct MLwP|Rest] [pr Name CS|L] :- +:index (_ _ 1) +func declare-all-on-type-constructor int, term, list hbclass -> list constant. +declare-all-on-type-constructor _ _ [] []. +declare-all-on-type-constructor Nargs TK [class _ Struct _|Rest] L :- saturate-type-constructor Nargs TK T, has-instance T Struct, !, + declare-all-on-type-constructor Nargs TK Rest L. +declare-all-on-type-constructor Nargs TK [class Class Struct MLwP|Rest] [CS|L] :- %TODO: compute the arity of the Class subject and saturate up to that point % there may even be more than one possibility - saturate-type-constructor TK T, - infer-class T Class Struct MLwP S Name _STy Clauses, !, + saturate-type-constructor Nargs TK T, + + infer-class T Class Struct MLwP S Name _STy Clauses, + + !, abstract-holes.main S SC, std.assert-ok! (coq.typecheck SC SCTy) "declare-all-on-type-constructor: badly closed", decl-const-in-struct Name SC SCTy CS, - Clauses => declare-all-on-type-constructor TK Rest L. -declare-all-on-type-constructor TK [class HasNoInstance _ _|Rest] L :- + Clauses => declare-all-on-type-constructor Nargs TK Rest L. + +declare-all-on-type-constructor Nargs TK [class HasNoInstance _ _|Rest] L :- % filter out classes we can't build for sure std.filter Rest (not-subclass-of HasNoInstance) Rest1, - declare-all-on-type-constructor TK Rest1 L. + declare-all-on-type-constructor Nargs TK Rest1 L. func has-instance term, structure ->. has-instance T Struct :- @@ -145,7 +194,7 @@ has-instance T Struct :- fail. % we build it func infer-class term, classname, gref, factories -> term, string, term, list prop. -infer-class T Class Struct MLwP S Name STy Clauses:- std.do![ +infer-class T Class Struct MLwP S Name STy Clauses:- std.time-do! "infer-class" [ params->holes MLwP Params, get-constructor Class KC, @@ -193,7 +242,7 @@ declare-factory-sort-deps GR :- std.do! [ mk-factory-sort-deps GR CSL, log.coq.env.end-section-name Name, log.coq.env.end-module-name Name _, - std.forall CSL (x\ sigma CS\ x = pr _ CS, log.coq.CS.declare-instance CS) + std.forall CSL log.coq.CS.declare-instance ]. func declare-factory-sort-factory gref ->. @@ -205,12 +254,12 @@ declare-factory-sort-factory GR :- std.do! [ mk-factory-sort-factory GR CFL CSL, log.coq.env.end-section-name Name, log.coq.env.end-module-name Name _, - std.forall {std.append CFL CSL} (x\ sigma CS\ x = pr _ CS, log.coq.CS.declare-instance CS) + std.forall {std.append CFL CSL} log.coq.CS.declare-instance ]. pred context.declare i:factories, o:mixins, o:list term, o:term, o:list prop, o:list constant. -func mk-factory-sort-deps gref -> list (pair id constant). +func mk-factory-sort-deps gref -> list constant. mk-factory-sort-deps AliasGR CSL :- std.do! [ std.assert-ok! (factory-alias->gref AliasGR GR) "HB: mk-factory-sort-deps", gref->deps GR MLwPRaw, @@ -235,7 +284,7 @@ mk-factory-sort-deps AliasGR CSL :- std.do! [ [declare-all KFSort {findall-classes-for ML} CSL] ]. -func mk-factory-sort-factory gref -> list (pair id constant), list (pair id constant). +func mk-factory-sort-factory gref -> list constant, list constant. mk-factory-sort-factory AliasGR CFL CSL :- std.do! [ std.assert-ok! (factory-alias->gref AliasGR GR) "HB", gref->deps GR MLwPRaw, @@ -250,8 +299,8 @@ mk-factory-sort-factory AliasGR CFL CSL :- std.do! [ ]. % create instances for all possible combinations of types and structure compatible -func saturate-instances cs-pattern -> . -saturate-instances Filter :- std.do! [ +func saturate-instances int, cs-pattern -> . +saturate-instances Nargs Filter :- std.do! [ findall-has-mixin-instance Filter ClausesHas, @@ -265,7 +314,7 @@ saturate-instances Filter :- std.do! [ Clauses => std.map2 TL UKL (t\k\CI\sigma Classes\ std.filter AllClasses (no-instance-for k) Classes, - declare-all-on-type-constructor t Classes CI) CIL, + declare-all-on-type-constructor Nargs t Classes CI) CIL, private.clauses-for-export {std.flatten CIL} ClausesExport, @@ -285,69 +334,63 @@ namespace private { shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }. -func declare-instance factoryname, term, term - -> list prop, list (pair id constant), list (pair id constant). -declare-instance Factory T F Clauses CFL CSL :- +func declare-instance factoryname, term, term -> list prop, list constant, list constant. +declare-instance Factory T F [] CFL CSL :- current-mode (builder-from T TheFactory FGR _), !, if (get-option "local" tt) (coq.error "HB: declare-instance: cannot make builders local. If you want temporary instances, make an alias, e.g. with let T' := T") true, !, declare-canonical-instances-from-factory-and-local-builders Factory - T F TheFactory FGR Clauses CFL CSL. + T F TheFactory FGR NM_CFL _ CSL, + std.map NM_CFL snd CFL. declare-instance Factory T F Clauses CFL CSL :- declare-canonical-instances-from-factory Factory T F Clauses1 CFL CSL, clauses-for-export {std.append CFL CSL} Clauses2, std.append Clauses1 Clauses2 Clauses. -func clauses-for-export list (pair id constant) -> list prop. +func clauses-for-export list constant -> list prop. clauses-for-export CL ECL :- if (get-option "export" tt) (coq.env.current-library File, - std.map CL (x\r\ sigma i c\ x = pr i c, r = instance-to-export File i c) ECL) + std.map CL (c\r\r = instance-to-export File c) ECL) (ECL = []). -% [add-mixin T F _ M Cl] adds a constant being the mixin instance for M on type +% [add-mixin T F M Cl] adds a constant being the mixin instance for M on type % T built from factory F -func add-mixin term, factoryname, bool, mixinname - -> list prop, list (pair id constant). -add-mixin T FGR MakeCanon MissingMixin [MixinSrcCl, BuilderDeclCl] CSL :- std.do! [ - new_int N, % timestamp +func add-mixin term, factoryname, mixinname -> prop, constant. +add-mixin T FGR MissingMixin MixinSrcCl C :- std.time-do! "add-mixin" [ + % new_int N, % timestamp - synthesis.assert!-infer-mixin T MissingMixin Bo, - MixinSrcCl = mixin-src T MixinName (global (const C)), - BuilderDeclCl = builder-decl (builder N FGR MixinName (const C)), + synthesis.assert!-infer-mixin T MissingMixin Bo Ty1, - std.assert-ok! (coq.typecheck Bo Ty) "declare-instances: mixin illtyped", - safe-dest-app Ty (global MixinNameAlias) _, + %std.assert-ok! (coq.typecheck Bo Ty1) "declare-instances: mixin illtyped", + safe-dest-app Ty1 (global MixinNameAlias) _, std.assert-ok! (factory-alias->gref MixinNameAlias MixinName) "HB", std.assert! (MissingMixin = MixinName) "HB: anomaly: we built the wrong mixin", + % cleanup-wrapped Ty1 Ty, + Ty = Ty1, + % If the mixin instance is already a constant there is no need to % alias it. if (Bo = global (const C)) true (Name is {gref->modname FGR 2 "_"} ^"__to__" ^ {gref->modname MixinName 2 "_"}, if-verbose (coq.say {header} "declare mixin instance" Name), log.coq.env.add-const-noimplicits Name Bo Ty @transparent! C), - if (MakeCanon = tt, whd (global (const C)) [] (global (indc _)) _) - (std.do! [ - if-verbose (coq.say {header} "declare canonical mixin instance" C), - with-locality (log.coq.CS.declare-instance C), - CSL = [pr "_" C] - ]) (CSL = []), -]. -func add-all-mixins term, factoryname, list mixinname, bool - -> list prop, list (pair id constant). -add-all-mixins T FGR ML MakeCanon Clauses CSL :- std.do! [ - std.map ML (m\ o\ sigma ClL CSL\ - add-mixin T FGR MakeCanon m ClL CSL, o = pr ClL CSL) ClLxCSL_L, - std.unzip ClLxCSL_L ClLL CSLL, - std.flatten ClLL Clauses, - std.flatten CSLL CSL + MixinSrcCl = mixin-src T MixinName (global (const C)), + % BuilderDeclCl = builder-decl (builder N FGR MixinName (const C)), ]. +func add-all-mixins term, factoryname, list mixinname -> list prop, list constant. +add-all-mixins _T _FGR [] [] []. +add-all-mixins T FGR [M|ML] [MixinSrcCL | CL] [C|CC] :- std.do! [ + add-mixin T FGR M MixinSrcCL C, + add-all-mixins T FGR ML CL CC, +]. + % [postulate-arity A Acc T TS] postulates section variables % corresponding to parameters in arity A. TS is T applied % to all section variables (and hd-beta reduced). Acc should @@ -371,22 +414,36 @@ postulate-arity (arity Ty) ArgsRev X T Ty :- % can access their theory and notations func declare-canonical-instances-from-factory-and-local-builders factoryname, term, term, term, factoryname - -> list prop, list (pair id constant), list (pair id constant). + -> list (pair mixinname constant), list prop, list constant. declare-canonical-instances-from-factory-and-local-builders - Factory T F _TheFactory FGR Clauses CFL CSL :- std.do! [ + Factory T F _TheFactory FGR NM_CFL MsClauses CSL :- std.time-do! "declare-canonical-instances-from-factory-and-local-builders" [ synthesis.under-new-mixin-src-from-factory.do! T F (NewMixins\ std.do! [ - add-all-mixins T FGR NewMixins ff Clauses CFL, + add-all-mixins T FGR NewMixins MsClauses CFL, + std.zip NewMixins CFL NM_CFL, ]), list-w-params_list {factory-provides Factory} ML, - Clauses => declare-all T {findall-classes-for ML} CSL, + MsClauses => declare-all T {findall-classes-for ML} CSL, ]. +func whd-hd term -> term. +whd-hd X Y :- std.time-do! "whd-hd" [ + coq.reduction.lazy.whd X T, + coq.safe-dest-app T Y _, +]. + +pred make-mixin-canonical i:constant, o:option constant. +make-mixin-canonical C (some C) :- whd-hd (global (const C)) (global (indc _)), !, std.time-do! "make-mixin-canonical" [ + if-verbose (coq.say {header} "declare canonical mixin instance" C), + with-locality (log.coq.CS.declare-instance C), +]. +make-mixin-canonical _ none. + % [declare-canonical-instances-from-factory T F] given a factory F % it uses all known builders to declare canonical instances of structures % on T func declare-canonical-instances-from-factory - factoryname, term, term -> list prop, list (pair id constant), list (pair id constant). -declare-canonical-instances-from-factory Factory T F ClausesHas CFL CSL :- std.do! [ + factoryname, term, term -> list prop, list constant, list constant. +declare-canonical-instances-from-factory Factory T F ClausesHas CFL CSL :- std.time-do! "declare-canonical-instances-from-factory" [ % The order of the following two "under...do!" is crucial, % priority must be given to canonical mixins % as they are the ones which guarantee forgetful inheritance @@ -395,13 +452,201 @@ declare-canonical-instances-from-factory Factory T F ClausesHas CFL CSL :- std.d synthesis.under-mixin-src-from-factory.do! T F [ MLCano => std.do! [ list-w-params_list {factory-provides Factory} ML, - add-all-mixins T Factory ML tt Clauses CFL, + add-all-mixins T Factory ML Clauses CFL, std.map-filter Clauses (mixin-src->has-mixin-instance ) ClausesHas, ClausesHas => declare-all T {findall-classes-for ML} CSL, % declare-all-on-type-constructor doesn't work here ] ], ]. +% [declare-mixins-from-factory T F] given a factory F +% it uses all known builders to declare canonical instances of structures +% on T +pred declare-mixins-from-factory + i:factoryname, i:term, i:term, o:list mixinname, o:list constant. +declare-mixins-from-factory Factory T F ML TheMixins :- std.time-do! "declare-mixins-from-factory" [ + % The order of the following two "under...do!" is crucial, + % priority must be given to canonical mixins + % as they are the ones which guarantee forgetful inheritance + % hence we add these clauses last. + synthesis.local-canonical-mixins-of T MLCano, + synthesis.under-mixin-src-from-factory.do! T F [ + MLCano => std.do! [ + list-w-params_list {factory-provides Factory} ML, + add-all-mixins T Factory ML _ TheMixins, + ] + ], +]. + +% [declare-structure-instance-from-mixins T ML MLI] given mixins ML and +% their implementation MLI declares all structure instances for T +pred declare-structure-instance-from-mixins i:term, i:list mixinname, i:list constant, o:list prop, o:list constant. +declare-structure-instance-from-mixins T ML TheMixins ClausesHas CL :- std.time-do! "declare-structure-instance-from-mixins" [ + % The order of the following two "under...do!" is crucial, + % priority must be given to canonical mixins + % as they are the ones which guarantee forgetful inheritance + % hence we add these clauses last. + synthesis.local-canonical-mixins-of T MLCano, + synthesis.under-these-mixin-src.do! T ML TheMixins ClausesHas [ + MLCano => std.do! [ + instance.declare-all T {findall-classes-for ML} CL, + ] + ], +]. + +pred close-section-if-has-params i:arity, i:id. +close-section-if-has-params (arity _) _ :- !. +close-section-if-has-params _ SectionName :- + if-verbose (coq.say {header} "closing instance section"), + log.coq.env.end-section-name SectionName. + +pred declare-regular-inst i:term, i:list mixinname, i:list constant, i:arity, i:id, + o:list prop, o:list constant. +declare-regular-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL :- std.time-do! "declare-regular-inst" [ + private.declare-structure-instance-from-mixins TheType ML TheMixins ClausesHas CCSL, + + % TODO: share between the two cases and put just after declare-mixins-from-factory + % since it talks about the unwrapped mixins + std.map TheMixins private.make-mixin-canonical TheCanonicalMixins, + std.map-filter TheCanonicalMixins (x\r\x = some r) MCSL, + std.append MCSL CCSL CSL, + + private.close-section-if-has-params TyWP SectionName, +]. + +pred declare-wrapper-inst i:term, i:list mixinname, i:list constant, i:arity, i:id, + o:list prop, o:list constant, o:list mixinname, o:list constant. +declare-wrapper-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL WML TheWrappedMixins :- std.time-do! "declare-wrapper-inst" [ + if-verbose (coq.say {header} "Wrapping" ML "for" TheType), + coq.safe-dest-app TheType TheTypeKey _, + std.assert! (TheTypeKey = global TheTypeKeyGR) "The subject to be wrapped has no key", + private.close-section-if-has-params TyWP SectionName, + private.wrap-mixins TheTypeKeyGR ML TheMixins TheNewType WML TheWrappedMixins, % TODO: give TheNewType in output and check it agrees with the factory (when in a builder section) + private.declare-structure-instance-from-mixins TheNewType WML TheWrappedMixins ClausesHas CSL, +]. + +pred derive-wrapper-instances i:term, i:mixinname, o:term, o:constant. +derive-wrapper-instances Instance WrapperMixin WrapperSubject C :- std.time-do! "derive-wrapper-instances" [ + + % K is the mixin constructor (Build) for WrapperMixin + factory->constructor WrapperMixin K, + + % the constructor of the new wrapper instance + phant-abbrev K _ Abb, + coq.notation.abbreviation-body Abb NArgs _, + coq.notation.abbreviation Abb {coq.mk-n-holes NArgs} AbbBo, + + coq.safe-dest-app AbbBo Hd ActualArgs, + std.assert-ok! (coq.typecheck Hd KTy) "wrap: cannot type constructor", + + % the arguments + coq.count-prods KTy KN, + KN0 is KN - 1 - {std.length ActualArgs}, + std.append {coq.mk-n-holes KN0} [Instance] Args, + + coq.mk-app AbbBo Args NewInstance, + std.assert-ok! (coq.typecheck NewInstance Ty1) "cannot wrap", + + cleanup-wrapped Ty1 Ty, + + Name is "wrapped__" ^ {std.any->string {new_int}}, + log.coq.env.add-const-noimplicits Name NewInstance Ty @transparent! C, + + coq.safe-dest-app Ty _Factory FArgs, + factory->nparams WrapperMixin NParams, + std.nth NParams FArgs WrapperSubjectAsInferred, + + % we may have inferred as the subject the sort projection of an instance + expose-real-subject WrapperSubjectAsInferred WrapperSubject, + + ]. + +func cleanup-wrapped term -> term. +cleanup-wrapped (app L) (app L1) :- !, std.time-do! "cleanup-wrapped" [ + % all constants generated by HB + std.findall (decl-location (const _) _) LC, + std.map LC (x\r\sigma c\x = decl-location (const c) _, r = coq.redflags.const c) CL, + % all projection from structures + std.findall (structure-key _ _ _) LP, + std.map LP (x\r\sigma c\x = structure-key c _ _, r = coq.redflags.const c) PSL, + std.map LP (x\r\sigma c\x = structure-key _ c _, r = coq.redflags.const c) PCL, + % options for lazy + coq.redflags.add coq.redflags.nored + {std.append [coq.redflags.beta, coq.redflags.cofix, coq.redflags.fix, coq.redflags.zeta, coq.redflags.match, coq.redflags.delta] + {std.append CL {std.append PSL PCL}}} F, + % call lazy only on the head + @redflags! F => + std.map L cleanup-wrapped1 L1, +]. +cleanup-wrapped X X. + +func cleanup-wrapped1 term -> term. +cleanup-wrapped1 X Y :- + cleanup-wrapped.aux X X1, + if ({term->size X1} =< {term->size X}) (Y = X1) (coq.warn "cleanup counter productive", Y = X). + +func cleanup-wrapped.aux term -> term. +cleanup-wrapped.aux T T1 :- + coq.reduction.lazy.whd T TN, + coq.reduction.eta-contract TN TE, + hack-primproj TE TX, + if (same_term T TX) (T1 = TX) (cleanup-wrapped.aux TX T1). + +pred expose-real-subject i:term, o:term. +expose-real-subject X Y :- + expose-real-subject.aux X X1, + if (X1 = global _ ; X1 = app[global _|_]) (Y = X1) (Y = X). + +pred expose-real-subject.aux i:term, o:term. +expose-real-subject.aux T T1 :- + % all constants generated by HB + std.findall (decl-location (const _) _) LC, + std.map LC (x\r\sigma c\x = decl-location (const c) _, r = coq.redflags.const c) CL, + % all projection from structures + std.findall (structure-key _ _ _) LP, + std.map LP (x\r\sigma c\x = structure-key c _ _, r = coq.redflags.const c) PSL, + std.map LP (x\r\sigma c\x = structure-key _ c _, r = coq.redflags.const c) PCL, + % options for lazy + coq.redflags.add coq.redflags.nored + {std.append [coq.redflags.beta, coq.redflags.cofix, coq.redflags.fix, coq.redflags.zeta, coq.redflags.match, coq.redflags.delta] + {std.append CL {std.append PSL PCL}}} F, + % call lazy only on the head + @redflags! F => coq.reduction.lazy.whd T TN, + % eta contract + coq.reduction.eta-contract TN TE, + % reduce all primproj + hack-primproj TE TX, + if (same_term T TX) (T1 = TX) (expose-real-subject.aux TX T1). + +% BUG in coq-elpi: coq.reflags.proj not bound !!!! +func hack-primproj term -> term. +hack-primproj T T1 :- + (pi N A Rest X\ + copy (app[primitive (proj _ N),A]) X :- + whd A [] (global (indc _)) Rest, + std.nth N Rest X, !) => + copy T T1. + +pred wrap-a-mixin i:gref, i:mixinname, i:constant, o:term, o:mixinname, o:constant. +wrap-a-mixin TheTypeKeyGR M TheMixin TheNewType WM TheWrappedMixin :- std.do! [ + std.findall (wrapper-mixin _ TheTypeKeyGR M) Wrappers, + std.assert! (not(Wrappers = [])) "wrap-a-mixin: no wrapper found", + if (Wrappers = [wrapper-mixin WM TheTypeKeyGR M]) + (TM = global (const TheMixin), + private.derive-wrapper-instances TM WM TheNewType TheWrappedMixin) + (coq.error "wrap-a-mixin: more than one way to wrap" TheTypeKeyGR "for" M), +]. + +pred wrap-mixins i:gref, i:list mixinname, i:list constant, + o:term, o:list mixinname, o:list constant. +wrap-mixins TheTypeKeyGR [ M | ML ] [ TheMixinInstance | TheMixins ] + TheNewType [ WM | WML ] [ TheWrappedMixin | TheWrappedMixins ] :- + wrap-a-mixin TheTypeKeyGR M TheMixinInstance TheNewType1 WM TheWrappedMixin, + std.assert! (TheNewType = TheNewType1) "wrapping leads to different subjects", + wrap-mixins TheTypeKeyGR ML TheMixins TheNewType WML TheWrappedMixins. +wrap-mixins _ [] [] _ [] []. + + % If you don't mention the factory in a builder, then Coq won't make % a lambda for it at section closing time. func hack-section-discharging term -> term. diff --git a/HB/pack.elpi b/HB/pack.elpi index 3bd0d2cc..074da964 100644 --- a/HB/pack.elpi +++ b/HB/pack.elpi @@ -12,7 +12,6 @@ main Ty Args Instance :- std.do! [ std.assert! (Args = [trm TSkel|FactoriesSkel]) "HB.pack: not enough arguments", get-constructor Class KC, - get-constructor Structure KS, std.assert-ok! (d\ (coq.elaborate-ty-skeleton TSkel _ T d, d = ok) ; @@ -29,31 +28,73 @@ main Ty Args Instance :- std.do! [ (AllFactories = Factories) (AllFactories = Factories, Tkey = T), % it's a factory, won't add anything - private.synth-instance Params KC KS T Tkey AllFactories Instance, + private.synth-instance Params KC T Tkey AllFactories ClassInstance, + + get-constructor Structure KS, + std.append Params [T, ClassInstance] InstanceArgs, + Instance = app[global KS | InstanceArgs] + +]. + +pred main-use-factories i:term, i:list argument, o:term. +main-use-factories Ty FactoriesSkel ClassInstance :- std.do! [ + std.assert! (not(var Ty)) "HB.from: the class cannot be unknown", + + factory? {unwind {whd Ty []}} (triple Class Params T), + + std.assert! (class-def (class Class _ _)) "HB.from: not a class", + + get-constructor Class KC, + + private.elab-factories FactoriesSkel T Factories, + + if (var T) (coq.error "HB.from: you must pass a type or at least one factory") true, + if2 (T = app[global (const SortProj)|ProjParams], structure-key SortProj ClassProj _) + (AllFactories = [app[global (const ClassProj)|ProjParams] | Factories], Tkey = T) % already existing class on T + (def T _ _ Tkey) % we unfold letins if we can, they may hide constants with CS instances + (AllFactories = Factories) + (AllFactories = Factories, Tkey = T), % it's a factory, won't add anything + + private.try-synth-instance Params KC Tkey AllFactories ClassInstance, + ]. + + + /* ------------------------------------------------------------------------- */ /* ----------------------------- private code ------------------------------ */ /* ------------------------------------------------------------------------- */ namespace private { -pred synth-instance.aux i:list term, i:gref, i:gref, i:term, i:term, i:list term, i:list prop, o:term. -synth-instance.aux Params KC KS T Tkey [Factory|Factories] MLCano Instance :- +pred synth-instance.aux i:list term, i:gref, i:term, i:term, i:list term, i:list prop, o:term. +synth-instance.aux Params KC T Tkey [Factory|Factories] MLCano ClassInstance :- synthesis.under-new-mixin-src-from-factory.do! Tkey Factory (_\ - synth-instance.aux Params KC KS T Tkey Factories MLCano Instance). -synth-instance.aux Params KC KS T Tkey [] MLCano Instance :- + synth-instance.aux Params KC T Tkey Factories MLCano ClassInstance). +synth-instance.aux Params KC _T Tkey [] MLCano ClassInstance :- MLCano => std.do! [ std.assert-ok! (synthesis.infer-all-args-let Params Tkey KC ClassInstance) "HB.pack: cannot infer the instance", - std.append Params [T, ClassInstance] InstanceArgs, - Instance = app[global KS | InstanceArgs] ]. -pred synth-instance i:list term, i:gref, i:gref, i:term, i:term, i:list term, o:term. -synth-instance Params KC KS T Tkey Factories Instance :- +pred synth-instance i:list term, i:gref, i:term, i:term, i:list term, o:term. +synth-instance Params KC T Tkey Factories ClassInstance :- if (coq.safe-dest-app Tkey (global _) _) (synthesis.local-canonical-mixins-of Tkey MLCano) (MLCano = []), - synth-instance.aux Params KC KS T Tkey Factories MLCano Instance. + synth-instance.aux Params KC T Tkey Factories MLCano ClassInstance. + +pred try-synth-instance i:list term, i:gref, i:term, i:list term, o:term. +try-synth-instance Params KC Tkey [Factory|Factories] ClassInstance :- + synthesis.under-new-mixin-src-from-factory.do! Tkey Factory (_\ + try-synth-instance Params KC Tkey Factories ClassInstance). +try-synth-instance Params KC Tkey [] ClassInstance :- coq.safe-dest-app Tkey (global _) _, !, + synthesis.local-canonical-mixins-of Tkey MLCano, + MLCano => std.do! [ + synthesis.try-infer-all-args-let Params Tkey KC ClassInstance, +]. +try-synth-instance Params KC Tkey [] ClassInstance :- std.do! [ + synthesis.try-infer-all-args-let Params Tkey KC ClassInstance, +]. pred elab-factories i:list argument, i:term, o:list term. elab-factories [] _ []. diff --git a/HB/status.elpi b/HB/status.elpi index e6bf3684..cd730223 100644 --- a/HB/status.elpi +++ b/HB/status.elpi @@ -28,6 +28,13 @@ print-hierarchy :- std.do! [ std.forall BDL private.pp-builder-decl ), + std.findall (wrapper-mixin _ _ _) WL, + if (WL = []) true ( + coq.say "", + coq.say "--------------------- Wrappers ----------------------", + std.forall WL private.pp-wrapper + ), + std.findall (current-mode BF_) BFL, if (BFL = []) true ( coq.say "", @@ -51,10 +58,10 @@ pp-from (from F M T) :- pred pp-list-w-params i:mixins, i:term. pred pp-list-w-params.list-triple i:list (w-args mixinname), i:term. pred pp-list-w-params.triple i:w-args mixinname. -pp-list-w-params (w-params.cons N Ty LwP) T :- - @pi-parameter N Ty p\ pp-list-w-params (LwP p) {coq.mk-app T [p]}. -pp-list-w-params (w-params.nil N TTy LwP) T :- - @pi-parameter N TTy t\ pp-list-w-params.list-triple (LwP t) {coq.mk-app T [t]}. +pp-list-w-params (w-params.cons N' Ty LwP) T :- + @pi-parameter N' Ty p\ pp-list-w-params (LwP p) {coq.mk-app T [p]}. +pp-list-w-params (w-params.nil N' TTy LwP) T :- + @pi-parameter N' TTy t\ pp-list-w-params.list-triple (LwP t) {coq.mk-app T [t]}. pp-list-w-params.list-triple L S :- coq.say {coq.term->string S} ":=", std.forall L pp-list-w-params.triple. @@ -80,5 +87,9 @@ pred pp-current-mode i:prop. pp-current-mode (current-mode (builder-from TheType TheFactory GRF Mod)) :- coq.say "The current key is" TheType "with factory" TheFactory "corresponding to Global Ref" GRF "in module" Mod. - + +pred pp-wrapper i:prop. +pp-wrapper (wrapper-mixin W O M) :- + coq.say "wrapper" W "for mixin" M "for lifter" O. + }} diff --git a/HB/structure.elpi b/HB/structure.elpi index 52036dfd..077cb75d 100644 --- a/HB/structure.elpi +++ b/HB/structure.elpi @@ -6,12 +6,19 @@ namespace structure { % HB.structure Definition S P1 P2 := { T of F1 P1 T & F2 P1 (P2*P2) T } % cons p1\ cons p2\ nil t\ [triple f1 [p1] t,triple f2 [p1, {{p1 * p2}}] t] pred declare i:string, i:term, i:sort. -declare Module BSkel Sort :- std.do! [ +declare Module BSkel Sort :- private.declare-wrappers BSkel WrapperClauses, % move to factory.elpi + + WrapperClauses => std.do! [ disable-id-phant BSkel BSkelNoId, - std.assert-ok! (coq.elaborate-skeleton BSkelNoId _ BNoId) "illtyped structure definition", + private.failsafe-structure-inference BSkelNoId BSkelNoIdX, + %coq.say {coq.term->string BSkelNoIdX} BSkelNoIdX, + std.assert-ok! (coq.elaborate-skeleton BSkelNoIdX _ BNoId) "illtyped structure definition", re-enable-id-phant BNoId B, - private.sigT->list-w-params B GRFSwP ClosureCheck, - + private.sigT->list-w-params B GRFSwP_or_ThingtoBeWrapped ClosureCheck, + + % do some work to go back to factories on a single subject + private.lift-to-the-subject GRFSwP_or_ThingtoBeWrapped GRFSwP, + factories-provide GRFSwP PMLwP, list-w-params.flatten-map GRFSwP gref->deps RMLwP, % TODO: extract code from factories-provide @@ -126,7 +133,8 @@ declare Module BSkel Sort :- std.do! [ std.flatten [ Factories, [is-structure Structure], NewJoins, [class-def CurrentClass], GRDepsClauses, - [gref->deps GRPack MLwP], MixinMems, [StructKeyClause] + [gref->deps GRPack MLwP], MixinMems, [StructKeyClause], + WrapperClauses ] NewClauses, acc-clauses current NewClauses, @@ -175,6 +183,13 @@ declare Module BSkel Sort :- std.do! [ log.coq.env.end-module-name ElpiOperationModName ElpiOperations, export.module ElpiOperationModName ElpiOperations, + % we need to assert locally the clauses in EX + EX => std.forall ML private.reexport-wrapper-as-instance, + + %hack + hack, + + if-verbose (coq.say {header} "abbreviation factory-by-classname"), ClassAlias => NewClauses => factory.declare-abbrev Module (factory.by-classname ClassName) ClassAbbrev, @@ -187,6 +202,11 @@ declare Module BSkel Sort :- std.do! [ % NewClauses => instance.saturate-instances, ]. +pred hack. +hack :- coq.next-synterp-action (begin-section X), coq.env.begin-section X, hack. +hack :- coq.next-synterp-action end-section, coq.env.end-section, hack. +hack. + /* ------------------------------------------------------------------------- */ /* ----------------------------- private code ------------------------------ */ /* ------------------------------------------------------------------------- */ @@ -610,16 +630,55 @@ if-coverage-not-good-error.one MS M :- mixin->first-class M C, !, "which contains at most" {std.map {coq.gref.set.elements {coq.gref.set.inter CMS MS}} nice-gref->string}). if-coverage-not-good-error.one _ _. % new class is the first covering M -pred product->triples i:term, o:list (w-args factoryname), o:bool. -product->triples {{ lib:hb.prod lp:A lp:B }} L ClosureCheck :- !, - product->triples B GRB ClosureCheck, - product->triples A GRA _, +% 1. write a predicate to recognize factory applied to op, maybe under a forall prefix +% factory-on-some-structure-op? +% 2. change the type of product->triples and sigT->list-w-params to +% return a list-w-params of either a factoryname or a thing-to-be-wrapper +% (eg mixin to be wrapped, operation) +% 3. the caller of sigT->list-w-params has to pre-process the list +% and generate wrapper mixins for each thing-to-be-wrapper and replace +% in the list the thing-to-be-wrapper with the wrapper mixin +% - one needs to find to which structure the operation belongs and +% use that structure to synthesize the type of the wrapper, eg +% hom belongs to Quiver, hence hom_isMon takes a "T of Quiver T" + +% checks if the term is forall A B C, Factory ... (Op A B C) ... +pred factory-on-some-structure-op? i:term, i:list term, o:gref, o:gref. +factory-on-some-structure-op? (prod N Ty Bo) VS F OP :- + @pi-decl N Ty x\ + factory-on-some-structure-op? (Bo x) [x|VS] F OP. +factory-on-some-structure-op? T VS F (const OP) :- std.do! [ + factory? T (triple F _ Subject), + hd-beta-zeta Subject [] (global (const OP)) Args, + exported-op _ _ OP, + std.appendR _ {std.rev VS} Args, +]. +factory-on-some-structure-op? T VS F GR :- std.do! [ + factory? T (triple F _ Subject), + hd-beta-zeta Subject [] (global GR) Args, + tag GR _ _, + std.appendR _ {std.rev VS} Args, +]. + +kind factory-on-subject type. +type factory-on-the-type w-args factoryname -> factory-on-subject. +type factory-on-subject-lifter term -> factoryname -> gref -> factory-on-subject. + +pred product->triples i:term, i:term, o:list factory-on-subject, o:bool. +product->triples {{ lib:hb.prod lp:A lp:B }} T L ClosureCheck :- !, + product->triples B T GRB ClosureCheck, + product->triples A T GRA _, std.append GRA GRB L. -product->triples {{ True }} [] tt :- !. -product->triples {{ False }} [] ff :- !. -product->triples A [GR] tt :- std.assert! (factory? A GR) "A structure can only mention known factories". +product->triples {{ True }} _ [] tt :- !. +product->triples {{ False }} _ [] ff :- !. +product->triples A T [factory-on-the-type F] tt :- (factory? A F), (F = triple _ _ T), !. +product->triples A _ [factory-on-subject-lifter A F OP] tt :- factory-on-some-structure-op? A [] F OP, !. +product->triples A T _ _ :- + coq.error "HB: expecting a factory on" {coq.term->string T} + "or a factory on a structure operation or tag. Got:" {coq.term->string A}. -pred sigT->list-w-params i:term, o:list-w-params factoryname, o:bool. + +pred sigT->list-w-params i:term, o:w-params (list factory-on-subject), o:bool. sigT->list-w-params (fun N T B) L C :- coq.name->id N ID, % TODO: we should read the ID from the definition type which is an arity containing ids L = w-params.cons ID T Rest, @@ -629,6 +688,251 @@ sigT->list-w-params {{ lib:@hb.sigT _ lp:{{ fun N Ty B }} }} L C :- coq.name->id N ID, % TODO: we should read the ID from the definition type which is an arity containing ids L = w-params.nil ID Ty Rest, @pi-decl N Ty t\ - product->triples (B t) (Rest t) C. + product->triples (B t) t (Rest t) C. + +%TODO expand factories in lift +pred lift-to-the-subject i:w-params (list factory-on-subject), o:list-w-params factoryname. +lift-to-the-subject (w-params.cons ID T Rest) (w-params.cons ID T Rest1) :- + @pi-parameter ID T x\ + lift-to-the-subject (Rest x) (Rest1 x). +lift-to-the-subject (w-params.nil ID T Rest) (w-params.nil ID T Rest1) :- + @pi-parameter ID T x\ + lift-to-the-subject.aux (Rest x) x (Rest1 x). +lift-to-the-subject.aux [] _ []. +lift-to-the-subject.aux [factory-on-the-type F|Rest] T [F|Rest1] :- + lift-to-the-subject.aux Rest T Rest1. +lift-to-the-subject.aux [factory-on-subject-lifter _ F OP|Rest] T [WF|Rest1] :- + wrapper-mixin Wrapper OP F, !, std.do! [ + factory->nparams Wrapper NParams, + coq.mk-app {coq.env.global Wrapper} {std.append {coq.mk-n-holes NParams} [T]} W, + factory? W WF, + lift-to-the-subject.aux Rest T Rest1, +]. +lift-to-the-subject.aux [factory-on-subject-lifter Expr _ _|_] _ _ :- + coq.error "NYI: automatic wrapping for" {coq.term->string Expr}. + +pred declare-wrappers i:term, o:list prop. +declare-wrappers B C :- std.do! [ + private.sigT->list-w-params B X _, + declare-wrappers.filter-lifted X Wrappers, + w-params.map Wrappers (_\_\std.flatten) Wrappers1, + distribute-w-params Wrappers1 WrappersWP, + std.fold WrappersWP [] declare-wrapper C, +]. +pred declare-wrappers.filter-lifted i:w-params (list factory-on-subject), o:w-params (list (list (pair gref (w-args mixinname)))). +declare-wrappers.filter-lifted (w-params.cons ID T F) (w-params.cons ID T F1) :- + @pi-parameter ID T x\ declare-wrappers.filter-lifted (F x) (F1 x). +declare-wrappers.filter-lifted (w-params.nil ID T F) (w-params.nil ID T F1) :- + @pi-parameter ID T x\ declare-wrappers.filter-lifted.aux (F x) (F1 x). +declare-wrappers.filter-lifted.aux [factory-on-the-type _|XS] R :- declare-wrappers.filter-lifted.aux XS R. +declare-wrappers.filter-lifted.aux [factory-on-subject-lifter T F G|XS] [WL|R] :- + factory? T (triple _ Params S), + factory-provides F MLwP, + apply-w-params MLwP Params S Triples, + std.map-filter Triples (declare-wrappers.filter-new G) WL, + declare-wrappers.filter-lifted.aux XS R. +declare-wrappers.filter-lifted.aux [] []. + +pred declare-wrappers.filter-new i:gref, i:w-args mixinname, o:pair gref (w-args mixinname). +declare-wrappers.filter-new G (triple F _ _ as T) (pr G T) :- not (wrapper-mixin _ G F). + +pred wrap-deps i:gref, i:mixins, o:mixins. +wrap-deps OP (w-params.cons ID T F) (w-params.cons ID T F1) :- + @pi-parameter ID T x\ wrap-deps OP (F x) (F1 x). +wrap-deps OP (w-params.nil ID T F) (w-params.nil ID T F1) :- + @pi-parameter ID T x\ wrap-deps.mixins OP (F x) (F1 x). + +pred wrap-deps.mixins i:gref, i:list (w-args mixinname), o:list (w-args mixinname). +wrap-deps.mixins _ [] []. +wrap-deps.mixins OP [triple M P X|ML] [triple WM P X|ML1] :- + std.assert! (wrapper-mixin WM OP M) "no wrapper for the lifter on a dep", + wrap-deps.mixins OP ML ML1. + +pred declare-wrapper i:w-params (pair gref (w-args mixinname)), i:list prop, o:list prop. +declare-wrapper F C0 C :- C0 => std.do! [ + %coq.say "Missing" F, + missing-wrapper->record F RSkel OP M, + %coq.say "Wrapper skel" F "=" RSkel, + %disable-id-phant-indt-decl RSkel RSkelNoId, + %std.assert-ok! (coq.elaborate-indt-decl-skeleton RSkelNoId RDeclNoId) "illtyped wrapper", + %re-enable-id-phant-indt-decl RDeclNoId RDecl, + %coq.say "Record wrapper" RDecl, + gref->deps M MDeps, + wrap-deps OP MDeps WrappedDeps, + ((pi X Y L\ copy X Y :- var X _ L, prune Y L) => copy-indt-decl RSkel RSkel'), expand-structures RSkel' WrappedDeps W', + %coq.say "Expanded record wrapper" W', + %std.assert-ok! (coq.typecheck-indt-decl W) "illtyped wrapper record", + coq.say "Wrapper for" OP "and" M "is" W', + std.assert-ok! (coq.elaborate-indt-decl-skeleton W' W) "illtyped wrapper record", + %coq.say W, + log.coq.env.add-indt W R, + coq.env.indt R tt _ _ _ [K] _, + GRK = indc K, + GR = indt R, + + coq.gref->id GR Name, + + wrapper-deps F W MLwP, + %coq.say "W deps" F "=" MLwP, + + w-params.nparams MLwP NParams, + factory.private.build-deps-for-projections R MLwP GRDepsClausesProjs, + GRDepsClauses = [ gref->deps GR MLwP, gref->deps (indc K) MLwP | GRDepsClausesProjs], + GRDepsClauses => phant.of-gref ff GRK [] PhGRK, + GRDepsClauses => phant.add-abbreviation {calc (Name ^ "_Build")} PhGRK BuildConst BuildAbbrev, + GRDepsClauses => phant.of-gref ff GR [] PhTerm, + GRDepsClauses => phant.add-abbreviation {calc (Name ^ "_axiom")} PhTerm PhC Abbrv, + + FRClauses = [ + phant-abbrev GRK (const BuildConst) BuildAbbrev, + phant-abbrev GR (const PhC) Abbrv, + ], + + GRDepsClauses => FRClauses => factory.private.declare-id-builder GR IdBuilderClause, + + std.flatten [ C0, + [ wrapper-mixin GR OP M, + factory->constructor GR GRK, + factory->nparams GR NParams, + IdBuilderClause], + FRClauses, + GRDepsClauses, + ] C, + %factory-builder-nparams BuildConst NParams, + coq.say "Wrapper DONE" F, +]. + +pred missing-wrapper->record i:w-params (pair gref (w-args mixinname)), o:indt-decl, o:gref, o:mixinname. +missing-wrapper->record (w-params.cons ID T F) (parameter ID explicit T F1) OP M:- + @pi-parameter ID T x\ missing-wrapper->record (F x) (F1 x) OP M. +missing-wrapper->record (w-params.nil ID T F) (parameter ID explicit T F1) OP M:- + @pi-parameter ID T x\ missing-wrapper->record.body (F x) (F1 x) OP M. + +pred unfold-phant i:term, o:term. +unfold-phant (app [global (const C)|A]) R :- + coq.env.const C (some B) _, + unwind {hd-beta B A} R. + +pred missing-wrapper->record.body i:pair gref (w-args mixinname), o:indt-decl, o:gref, o:mixinname. +missing-wrapper->record.body (pr OP (triple M Params Subject)) + (record Name _ Bname (field [] Fname T (x\end-record))) OP M :- std.do! [ + coq.mk-app {coq.env.global M} {std.append Params [Subject]} T, + + Name is "wrapper_" ^ {std.any->string {new_int}} ^ "_" ^ {coq.gref->id OP} ^ "_" ^ {nice-gref->string M}, + Fname is Name ^ "_private", + Bname is Name ^ "_build", +]. + +pred wrapper-deps i:w-params (pair gref (w-args gref)), i:indt-decl, o:mixins. +wrapper-deps (w-params.cons _ _ F) (parameter ID explicit T F1) (w-params.cons ID T ML) :- + @pi-parameter ID T x\ wrapper-deps (F x) (F1 x) (ML x). +wrapper-deps (w-params.nil _ _ _) (parameter ID explicit T F1) (w-params.nil ID T ML) :- + @pi-parameter ID T x\ wrapper-deps.aux (F1 x) x (ML x). +wrapper-deps.aux (parameter ID explicit T F1) X [triple M Params X|ML] :- + coq.safe-dest-app T Mixin ParamsXStuff, + coq.env.global M Mixin, + std.appendR Params [X|_] ParamsXStuff, + @pi-parameter ID T x\ wrapper-deps.aux (F1 x) X ML. +wrapper-deps.aux (record _ _ _ _) _ []. + +pred expand-structures i:indt-decl, i:mixins, o:indt-decl. +expand-structures (parameter ID I T ((s\record _ _ _ (field _ _ (X s) _\end-record)) as R)) Deps (parameter ID I _ R1) :- !, std.do! [ + (@pi-decl `TheType` T x\ coq.typecheck-ty T _ ok, std.assert-ok! (coq.typecheck (X x) (Ty_ x)) "illtyped subject"), + coq.safe-dest-app T (global GR) Args, is-structure GR, class-def (class C GR ML), + coq.mk-n-holes {w-params.nparams Deps} Holes, + get-constructor C K, + get-constructor GR SK, + coq.mk-app (global SK) Args SKArgs, + (@pi-decl `TheType` T x\ % TYPE is wrong + apply-w-params ML Args x (F x), + apply-w-params Deps Holes x (DepsX x), + %toposort-mixins {std.append (F x) (DepsX x)} (MoreParams x), + expand-structures.aux (F x) (DepsX x) [] {coq.mk-app SKArgs [x]} K Args x R (R1 x)), +]. +expand-structures(parameter ID I T F) Deps (parameter ID I T F1) :- + @pi-parameter ID T x\ expand-structures (F x) Deps (F1 x). + +pred expand-structures.aux list (w-args mixinname), list (w-args mixinname), list term, term, gref, list term, term, (term -> indt-decl) -> indt-decl. +expand-structures.aux [triple M PS X|MS] D ACC Pack K KA Subj R (parameter "m" explicit Ty R1) :- std.do! [ + synthesis.infer-all-gref->deps PS X M Ty, + (@pi-decl `m` Ty m\ mixin-src X M m => + expand-structures.aux MS D ACC Pack K KA Subj R (R1 m)), +]. +expand-structures.aux [] [triple M PS X|D] ACC Pack K KA Subj R (parameter "m" explicit Ty R1) :- std.do! [ + synthesis.infer-all-gref->deps PS X M Ty, + coq.safe-dest-app Ty _ Args, + M = indt I, + std.assert! (coq.env.projections I [some Priv]) "wrapper with no projection", + (@pi-decl `m` Ty m\ sigma PM\ + coq.mk-app (app [{coq.env.global (const Priv)}|Args]) [m] PM, + mixin-src X M m => + expand-structures.aux [] D [PM|ACC] Pack K KA Subj R (R1 m)), +]. +expand-structures.aux [] [] WrappedDepsRev Pack K KA Subj R R2 :- std.do! [ + synthesis.infer-all-gref->deps KA Subj K Class, + R1 = R {coq.mk-app Pack [Class]}, + R1 = record N S NK (field FA FN T _\end-record), + R2 = record N S NK (field FA FN T1 _\end-record), + factory? T (triple F Params LiftedSubject), + %std.assert! (std.forall Deps var) "wrapper: deps should be inferred, not given", + %CONVOLUTED + std.rev WrappedDepsRev WrappedDeps, + coq.mk-app (app [global F|Params]) [LiftedSubject|WrappedDeps] T1, +]. + +% 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 :- wrapper-mixin M _ _, !, std.do! [ + + % need the body of the wrapper projection type + exported-op M _ C, + B = (global (const C)), + coq.env.typeof (const C) Ty, + coq.count-prods Ty N0, + coq.term->arity Ty N0 Arity, + + % need a recognisable valid idenfier for the derived instance + Str0 is "Op_isMx" ^ "__" ^ {std.any->string {new_int}}, + std.string.concat "__" [Str0, "ELIM"] Str, + + get-option "wrapper" ff => instance.declare-const Str B Arity _ _ + ]. +reexport-wrapper-as-instance _ :- + std.assert! (coq.next-synterp-action (begin-section SectionName)) "synterp code did not open section", + coq.env.begin-section SectionName, + std.assert! (coq.next-synterp-action (end-section)) "synterp code did not close section", + coq.env.end-section. + +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 (app [global _|_] as 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. + +func eta-structure-record term, int, classname, list term -> 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. }} diff --git a/HB/structures.v b/HB/structures.v index ab1c8fec..27257905 100644 --- a/HB/structures.v +++ b/HB/structures.v @@ -171,6 +171,18 @@ pred join o:classname, o:classname, o:classname. % `Clauses =>` in infer-class. Should perform a dynamic check? func mixin-mem term -> 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. + +% designated identity function for wrapping (sometimes you don't have a +% structure op for it). +% [tag GR Class NParams] +pred tag o:gref, o:classname, o:int. + %%%%%% 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 @@ -182,10 +194,12 @@ func mixin-mem term -> gref. % that contains the mixin M func mixin->first-class mixinname -> classname. -% memory of exported operations (TODO: document fiels) +% memory of exported operations. +% [exported-op Mixin MixinProjection Operation], where Operation is a +% structure projection. pred exported-op o:mixinname, o:constant, o:constant. -% memory of factory sort coercion +% memory of factory sort coercion (Unused?) pred factory-sort o:coercion. % memory of canonical projections for a structure (X.sort, X.class, X.type) @@ -232,7 +246,7 @@ pred current-mode o:declaration. % library, nice-name, object pred module-to-export o:string, o:id, o:modpath. -pred instance-to-export o:string, o:id, o:constant. +pred instance-to-export o:string, o:constant. pred abbrev-to-export o:string, o:id, o:gref. pred clause-to-export o:string, o:prop. @@ -581,6 +595,34 @@ Elpi Export HB.pack. (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) +Elpi Tactic HB.from. +Elpi Accumulate Db hb.db. +Elpi Accumulate File "HB/common/stdpp.elpi". +Elpi Accumulate File "HB/common/database.elpi". +Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". +#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi". +#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi". +Elpi Accumulate File "HB/common/utils.elpi". +Elpi Accumulate File "HB/common/log.elpi". +Elpi Accumulate File "HB/common/synthesis.elpi". +Elpi Accumulate File "HB/pack.elpi". +Elpi Accumulate lp:{{ + +solve (goal _ _ Ty _ Args as G) GLS :- with-attributes (with-logging (std.do! [ + pack.main-use-factories Ty Args Instance, + refine Instance G GLS, +])). + +}}. +Elpi Typecheck. + +Tactic Notation "HB.from" open_constr_list(L) := + elpi HB.from ltac_term_list:(L). + +(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) +(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) +(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) + (** [HB.structure] declares a packed structure. Syntax to declare a structure combing the axioms from [Factory1] … [FactoryN]. @@ -652,7 +694,7 @@ main [const-decl N (some B) Arity] :- std.do! [ % compute the universe for the structure (default ) prod-last {coq.arity->term Arity} Ty, if (ground_term Ty) (Sort = Ty) (Sort = {{Type}}), sort Univ = Sort, - with-attributes (with-logging (structure.declare N B Univ)), + with-attributes (with-logging (with-unsafe-univ (with-time "HB.structure" (structure.declare N B Univ)))), ]. }}. @@ -676,6 +718,10 @@ actions N :- coq.env.current-library File, coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File E)), coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File O)), + + % hack + std.forall {std.iota 30} (x\begin-section "x",end-section), + if (get-option "mathcomp" tt ; get-option "mathcomp.axiom" _) (actions-compat N) true. pred actions-compat i:id. @@ -728,10 +774,10 @@ Elpi Accumulate File "HB/instance.elpi". Elpi Accumulate File "HB/context.elpi". Elpi Accumulate File "HB/factory.elpi". Elpi Accumulate lp:{{ -main [] :- !, with-attributes (with-logging (instance.saturate-instances _)). -main [str "Type"] :- !, with-attributes (with-logging (instance.saturate-instances (cs-sort _))). -main [str K] :- !, coq.locate K GR, with-attributes (with-logging (instance.saturate-instances (cs-gref GR))). -main [trm T] :- !, term->cs-pattern T P, with-attributes (with-logging (instance.saturate-instances P)). +main [] :- !, with-attributes (with-logging (with-time "HB.saturate" (instance.saturate-instances 0 _))). +main [str "Type"] :- !, with-attributes (with-logging (with-time "HB.saturate" (instance.saturate-instances 0 (cs-sort _)))). +main [str K] :- !, coq.locate K GR, with-attributes (with-logging (with-time "HB.saturate" (instance.saturate-instances 0 (cs-gref GR)))). +main [trm T] :- !, term->cs-pattern T P, coq.safe-dest-app T _ L, std.length L N, with-attributes (with-logging (with-time "HB.saturate" (instance.saturate-instances N P))). main _ :- coq.error "Usage: HB.saturate [key]". }}. Elpi Typecheck. @@ -778,7 +824,7 @@ Elpi Accumulate lp:{{ :name "start" main [const-decl Name (some BodySkel) TyWPSkel] :- !, - with-attributes (with-logging (instance.declare-const Name BodySkel TyWPSkel _ _)). + with-attributes (with-logging (with-time "HB.instance" (instance.declare-const Name BodySkel TyWPSkel _ _))). main [T0, F0] :- !, coq.warning "HB" "HB.deprecated" "The syntax \"HB.instance Key FactoryInstance\" is deprecated, use \"HB.instance Definition\" instead", with-attributes (with-logging (instance.declare-existing T0 F0)). @@ -1200,6 +1246,70 @@ check-or-not Skel :- Elpi Typecheck. Elpi Export HB.check. + +(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) +(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) +(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) + +(** [HB.tag] declares a tag for mixin subjects + +[[ +HB.tag Definition N Params (x : S.type) : Type := x +]] + +*) + +#[arguments(raw)] Elpi Command HB.tag. +Elpi Accumulate Db hb.db. +Elpi Accumulate File "HB/common/stdpp.elpi". +Elpi Accumulate File "HB/common/database.elpi". +Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". +Elpi Accumulate File "HB/common/utils.elpi". +Elpi Accumulate File "HB/common/log.elpi". +Elpi Accumulate File "HB/common/synthesis.elpi". +Elpi Accumulate File "HB/context.elpi". +Elpi Accumulate File "HB/instance.elpi". +Elpi Accumulate lp:{{ + +main [const-decl Name (some BodySkel) AritySkel] :- !, std.do! [ + std.assert-ok! (coq.elaborate-arity-skeleton AritySkel _ Arity) "HB: type illtyped", + coq.arity->nparams Arity N, + coq.arity->term Arity Ty, + std.assert-ok! (coq.elaborate-skeleton BodySkel Ty Body) "HB: body illtyped", + with-attributes (with-logging (std.do! [ + log.coq.env.add-const Name Body Ty @transparent! C, + coq.arity->implicits Arity CImpls, + if (coq.any-implicit? CImpls) + (@global! => coq.arguments.set-implicit (const C) [CImpls]) + true, + ])), + M is N - 1, + class-of-nth-arg M Ty Class, + acc-clause current (tag (const C) Class M), +]. +main [str G, str"|", int M] :- !, + coq.locate G GR, + coq.env.typeof GR Ty, + class-of-nth-arg M Ty Class, + acc-clause current (tag GR Class M). + +main _ :- coq.error "Usage: HB.tag Definition ... := T ...\nUsage: HB.tag | ". + +pred class-of-nth-arg i:int, i:term, o:classname. +class-of-nth-arg 0 (prod _ (global S) _\_) Class :- class-def (class Class S _). +class-of-nth-arg 0 (prod _ (app [global S|_]) _\_) Class :- class-def (class Class S _). +class-of-nth-arg N (prod Name Ty Bo) Class :- N > 0, !, M is N - 1, + @pi-decl Name Ty x\ class-of-nth-arg M (Bo x) Class. +class-of-nth-arg 0 T _ :- !, + coq.error "HB: the last parameter of a tag must be of a structure type:" {coq.term->string T}. +class-of-nth-arg _ T _ :- !, + coq.error "HB: not enough argsuments:" {coq.term->string T}. + +}}. +Elpi Typecheck. +Elpi Export HB.tag. + + (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) diff --git a/Makefile b/Makefile index ddb7d560..949125b3 100644 --- a/Makefile +++ b/Makefile @@ -164,7 +164,7 @@ endif structures.vo : %.vo: __always__ Makefile.coq +$(COQMAKE) $@ -$(addsuffix o,$(wildcard examples/*.v examples/*/*.v tests/*.v tests/unit/*.v)): __always__ config build Makefile.test-suite.coq Makefile.test-suite-stdlib.coq +$(addsuffix o,$(wildcard examples/*.v examples/*/*.v tests/*.v tests/*/*.v tests/unit/*.v)): __always__ config build Makefile.test-suite.coq Makefile.test-suite-stdlib.coq +$(COQMAKE_TESTSUITE) $@ +$(COQMAKE_TESTSUITE_stdlib) $@ diff --git a/Makefile.test-suite.coq.local b/Makefile.test-suite.coq.local index fcba0fe2..96db64e3 100644 --- a/Makefile.test-suite.coq.local +++ b/Makefile.test-suite.coq.local @@ -9,7 +9,7 @@ output_for=`\ DIFF=\ @if [ -z "$$COQ_ELPI_ATTRIBUTES" ]; then \ echo OUTPUT DIFF $(1);\ - $(COQTOP) $(COQFLAGS) $(COQLIBS) -topfile $(1) \ + $(COQTOP) $(COQFLAGS) $(COQLIBS) -w -deprecated-from-Coq -topfile $(1) \ < $(1) 2>&1 \ | sed 's/Coq < *//g' \ | sed 's/Rocq < *//g' \ diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite index b235f8a0..7505817e 100644 --- a/_CoqProject.test-suite +++ b/_CoqProject.test-suite @@ -67,6 +67,24 @@ tests/bug_447.v tests/unimported_relevant_class.v tests/unimported_irrelevant_class.v +tests/tag_wrap.v +tests/wrap.v +tests/auto_wrap.v + + +tests/MinimalWrapBugs/aboutAutowrap.v +tests/MinimalWrapBugs/aboutAutowrap2.v +tests/MinimalWrapBugs/buildersofwrap.v +tests/MinimalWrapBugs/buildersofwrap2.v +tests/MinimalWrapBugs/buggyFactories.v +tests/MinimalWrapBugs/canonicalByHand.v +tests/MinimalWrapBugs/mwb.v +tests/MinimalWrapBugs/noglobref.v +tests/MinimalWrapBugs/typeNotInfered.v +tests/MinimalWrapBugs/unwrappedSubject.v + +tests/mindep.v + -R tests HB.tests -R examples HB.examples diff --git a/tests/MinimalWrapBugs/aboutAutowrap.v b/tests/MinimalWrapBugs/aboutAutowrap.v new file mode 100644 index 00000000..652fb562 --- /dev/null +++ b/tests/MinimalWrapBugs/aboutAutowrap.v @@ -0,0 +1,28 @@ +From HB Require Import structures. + +HB.mixin Record Q T (t : T) := { + q : True +}. + +HB.mixin Record hasPoint T := { + x : T +}. + +HB.structure Definition Pointed := {T of hasPoint T}. + +(* WORKAROUND: *) +(* +#[wrapper] +HB.mixin Record Q__on__Pointed_x T ( _ : Pointed T) := { + private : Q T x +}. + +HB.structure Definition QPointed := {T of hasPoint T & Q__on__Pointed_x T }. + +HB.about QPointed. *) + +HB.structure Definition QPointed := {T of hasPoint T & Q _ (@x T) }. +(* BUG: HB.about fails on structure defined relying on autowrap *) + +HB.about QPointed. +HB.about QPointed.type. diff --git a/tests/MinimalWrapBugs/aboutAutowrap2.v b/tests/MinimalWrapBugs/aboutAutowrap2.v new file mode 100644 index 00000000..3c6e87c7 --- /dev/null +++ b/tests/MinimalWrapBugs/aboutAutowrap2.v @@ -0,0 +1,29 @@ +From HB Require Import structures. + +HB.mixin Record isAssoc T (op : T -> T -> T) := { + opA : True; +}. + +HB.mixin Record hasOp T := { + op' : T -> T -> T +}. + +HB.structure Definition Magma := {T of hasOp T}. + +(* WORKAROUND: *) +(* +#[wrapper] +HB.mixin Record isAssoc__on__Magma_op' T ( _ : Magma T) := { + private : isAssoc T op' +}. + +#[short(type="semigroupType")] +HB.structure Definition Semigroup := {T of Magma T & isAssoc__on__Magma_op' T }. + +HB.about Semigroup. *) + +HB.structure Definition Semigroup := {T of hasOp T & isAssoc _ (@op' T) }. + +(* BUG: HB.about fails on structure defined relying on autowrap *) +HB.about Semigroup. +HB.about Semigroup.type. diff --git a/tests/MinimalWrapBugs/buggyFactories.v b/tests/MinimalWrapBugs/buggyFactories.v new file mode 100644 index 00000000..46d2e1d4 --- /dev/null +++ b/tests/MinimalWrapBugs/buggyFactories.v @@ -0,0 +1,75 @@ +From HB Require Import structures. + +HB.mixin Record hasPoint T := { + point: T +}. + +(*Two property of a point: A and B*) +HB.mixin Record isA T (p : T) := { + propA : unit +}. +HB.mixin Record isB T (p : T) := { + propB : unit +}. + +HB.structure Definition Pointed := {T of hasPoint T}. + +#[wrapper] +HB.mixin Record isA__on__Pointed_point T of Pointed T := { + private : isA T point +}. + +#[wrapper] +HB.mixin Record isB__on__Pointed_point T of Pointed T := { + private : isB T point +}. + + +HB.structure Definition PointedA := + { T of Pointed T + & isA__on__Pointed_point T }. + +HB.structure Definition PointedAB := + {T of PointedA T & isB__on__Pointed_point T}. + +HB.factory Record isPointedAB T := { + p : T; + a : unit; + b : unit +}. + +HB.builders Context T of isPointedAB T. +HB.instance Definition _ := hasPoint.Build T p. +HB.instance Definition _ := isA.Build T point a. +HB.instance Definition _ := isB.Build T point b. +HB.end. + +HB.status. + +HB.factory Record PointedA_isPointedAB V of PointedA V := { + b : unit +}. + +HB.builders Context V of PointedA_isPointedAB V. + +HB.instance Definition foo := isB.Build V point b. + +HB.end. + +HB.status. + +HB.instance Definition lui := hasPoint.Build nat 0. +HB.instance Definition dove_finisce := isA.Build nat point tt. +(* HB.instance Definition xxx := isB.Build nat point tt. *) + +Check nat : PointedA.type. + +About Builders_3.local_mixin_buggyFactories_isA__on__Pointed_point. + +HB.status. + +#[verbose] +HB.instance +Definition yy := PointedA_isPointedAB.Build nat tt. + +Check nat : PointedAB.type. \ No newline at end of file diff --git a/tests/MinimalWrapBugs/buildersofwrap.v b/tests/MinimalWrapBugs/buildersofwrap.v new file mode 100644 index 00000000..9f840e1d --- /dev/null +++ b/tests/MinimalWrapBugs/buildersofwrap.v @@ -0,0 +1,31 @@ +From HB Require Import structures. + +HB.mixin Record Q T (t : T) := { + q : True +}. + +HB.mixin Record hasPoint T := { + x : T +}. + +HB.structure Definition Pointed := {T of hasPoint T}. + +#[wrapper] +HB.mixin Record Q__on__Pointed_x T ( _ : Pointed T) := { + private : Q T x +}. + +HB.factory Record isQPointed T := { + y : T; + qy : True +}. + +HB.builders Context T of isQPointed T. + +HB.instance Definition _ := hasPoint.Build T y. + +HB.instance Definition _ := Q.Build T x qy. + +HB.end. + +HB.structure Definition QPointed' := {T of isQPointed T}. diff --git a/tests/MinimalWrapBugs/buildersofwrap2.v b/tests/MinimalWrapBugs/buildersofwrap2.v new file mode 100644 index 00000000..0ad1451b --- /dev/null +++ b/tests/MinimalWrapBugs/buildersofwrap2.v @@ -0,0 +1,44 @@ +From HB Require Import structures. + +HB.mixin Record Q T (t : T) := { + q : True +}. + +HB.mixin Record hasPoint T := { + x : T +}. + +HB.structure Definition Pointed := {T of hasPoint T}. + +#[wrapper] +HB.mixin Record Q__on__Pointed_x T ( _ : Pointed T) := { + private : Q T x +}. + +HB.structure Definition QPointed := {T of hasPoint T & Q__on__Pointed_x T }. + +HB.factory Record isQPointed T := { + y : T; + qy : True +}. + +(* WORKAROUND *) + (* HB.builders Context T of isQPointed T. + + HB.instance Definition _ := hasPoint.Build T y. + + HB.instance Definition temp := Q.Build T y qy. + HB.instance Definition _ := Q__on__Pointed_x.Build T temp. + + HB.end. + HB.status. *) + +HB.builders Context T of isQPointed T. + +HB.instance Definition _ := hasPoint.Build T y. + +HB.instance Definition _ := Q.Build T x qy. + +HB.end. + +HB.status. (* BUG: The builder targetting Q__on__Pointed_x is missing *) diff --git a/tests/MinimalWrapBugs/canonicalByHand.v b/tests/MinimalWrapBugs/canonicalByHand.v new file mode 100644 index 00000000..622ef767 --- /dev/null +++ b/tests/MinimalWrapBugs/canonicalByHand.v @@ -0,0 +1,78 @@ +From HB Require Import structures. + +HB.mixin Record IdLaw T (t:T) (l : T -> T) := { + is_id : l t = t; +}. + +HB.structure Definition IdMap T (t:T) := {l of IdLaw T t l}. + +HB.mixin Record IdempotentLaw T (t:T) (l : T -> T) := { + is_sinv : l (l t) = l t; +}. + +HB.structure Definition IdempotentMap T (t:T) := {l of IdempotentLaw T t l}. + + +(* nove very meaningful *) +HB.structure Definition FooMap T (t:T) := {l of IdLaw T t l & IdempotentLaw T t l}. + + +HB.mixin Record hasPoint T := { + point : T +}. +HB.structure Definition Pointed := {T of hasPoint T}. + +HB.mixin Record hasSelfMap T := { + selfmap : T -> T +}. +HB.structure Definition SelfMapped := {T of hasSelfMap T}. + + +HB.structure Definition PointedSelfMapped + := {T of Pointed T & SelfMapped T}. + +#[wrapper] +HB.mixin Record IdLaw__on__PointedSelfMapped_t T of PointedSelfMapped T := { + private : IdLaw T point selfmap +}. +HB.structure Definition IdPSM +:= {T of PointedSelfMapped T & IdLaw__on__PointedSelfMapped_t T}. + +#[wrapper] +HB.mixin Record IdempotentLaw__on__PointedSelfMapped_t T of PointedSelfMapped T := { + private : IdempotentLaw T point selfmap +}. +HB.structure Definition IdemPSM := {T of PointedSelfMapped T & IdempotentLaw__on__PointedSelfMapped_t T}. + +(* HB.structure Definition FooPSM := {T of PointedSelfMapped T & IdPSM T & IdemPSM T}. *) +HB.structure Definition FooPSM := {T of PointedSelfMapped T & IdLaw__on__PointedSelfMapped_t T & IdempotentLaw__on__PointedSelfMapped_t T}. + +Print Canonical Projections selfmap. +HB.saturate (@selfmap _). (* for the instance FooMap on selfmap to exist, one needs the join FooPSM *) +Print Canonical Projections selfmap. + +HB.factory Record BuggyFactory T := { + p : T; + s : T -> T; + sid : s p = p; + sinv : s (s p) = s p +}. + +HB.builders Context T of BuggyFactory T. + +HB.instance Definition _ := hasPoint.Build T p. +HB.instance Definition _ := hasSelfMap.Build T s. + +HB.instance Definition _ := IdLaw.Build T point selfmap sid. +#[verbose] HB.instance Definition _ := IdempotentLaw.Build T point selfmap sinv. + +Check selfmap : IdMap.type T point. +Check selfmap : IdempotentMap.type T point. +Check selfmap : FooMap.type T point. + +HB.end. + +HB.status. + + +Check fun (R : FooPSM.type) => @selfmap R : FooMap.type R (@point R). diff --git a/tests/MinimalWrapBugs/factoryBuildingWrapper.v b/tests/MinimalWrapBugs/factoryBuildingWrapper.v new file mode 100644 index 00000000..10db2ea3 --- /dev/null +++ b/tests/MinimalWrapBugs/factoryBuildingWrapper.v @@ -0,0 +1,69 @@ +From HB Require Import structures. + +(* From mathcomp Require Import all_boot. +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. *) + +From Coq Require Import Arith.PeanoNat. + +(*BUG: factories on the wrapper subjects do not trigger both the instances on +the wrapped subject. The beahviour when not using the factory is the expected +one*) + +Module M. + +HB.mixin Record hasOp {T:Type} := { + op : T -> T ->T +}. +HB.structure Definition Magma := { T of hasOp T }. + +HB.mixin Record isAssoc {T:Type} (op : T -> T ->T) := { + assoc : forall x y z : T, op x (op y z) = op (op x y) z +}. + +HB.structure Definition AssLaw T + := {op of isAssoc T op}. + +#[wrapper] +HB.mixin Record isAssoc__on__Magma_op T of Magma T := { + private : isAssoc _ (@op T) +}. +HB.structure Definition Semigroup := { T of hasOp T & isAssoc__on__Magma_op T }. + +(* HB.structure Definition Semigroup := { T of hasOp T & isAssoc _ (@op T) }. *) + + +HB.factory Record fac_er (T : Type) := { + o : T -> T -> T; + ass : forall x y z : T, o x (o y z) = o (o x y) z +}. + + +(*BUG: a factory on the wrapper declare the instance always only on @op*) +HB.builders Context (T : Type) of fac_er T. + + HB.instance Definition _ := hasOp.Build T o. + HB.instance Definition _ := isAssoc.Build T (@op _) ass. + +HB.end. + +HB.instance Definition _ := fac_er.Build nat Nat.add Nat.add_assoc. + +Check @op nat : AssLaw.type _. +Fail Check Nat.add : AssLaw.type _. (*<-*) +Check nat : Magma.type. +Check nat : Semigroup.type. + +(*/BUG*) + +(*Expected behaviour without using the factory:*) + +(* HB.instance Definition _ := hasOp.Build nat Nat.add. +HB.instance Definition _ := isAssoc.Build nat (@op _) Nat.add_assoc. +Check @op nat : AssLaw.type _. +Check Nat.add : AssLaw.type _. +Check nat : Magma.type. +Check nat : Semigroup.type. *) + +End M. \ No newline at end of file diff --git a/tests/MinimalWrapBugs/mwb.v b/tests/MinimalWrapBugs/mwb.v new file mode 100644 index 00000000..e8ebd23d --- /dev/null +++ b/tests/MinimalWrapBugs/mwb.v @@ -0,0 +1,147 @@ +(*Random things to try: +-) replece "True" with "unit" and/or with the actual proerties/definitions +-) Use Module and #[export] +-) Remove the primes "'" +-) make op unary and/or nullary +-) maybe the problem lies in the join with choice? +*) + +From HB Require Import structures. + +HB.mixin Record isAssoc T (op : T -> T -> T) := { + opA : True; +}. + +#[short(type="AssocOpType")] +HB.structure Definition AssocOp T := {op of isAssoc T op}. + +HB.mixin Record isUnital T (idm : T) (op : T -> T -> T) := { + op1m : True; + opm1 : True; +}. + +(* #[short(type="UnitalOpType")] *) +#[export] +HB.structure Definition UnitalOp T idm := {op of isUnital T idm op}. + +(* #[short(type="MonoidOpType")] *) +#[export] +HB.structure Definition MonoidOp T idm + := {op of isAssoc T op & isUnital T idm op}. + +HB.factory Record isMonoidOp T (idm : T) (op : T -> T -> T) := { + opA' : True; + op1m' : True; + opm1' : True; +}. + +HB.builders Context T idm op of isMonoidOp T idm op. + +HB.instance Definition _ := isAssoc.Build T op opA'. +HB.instance Definition _ := isUnital.Build T idm op op1m' opm1'. + +HB.end. + + +HB.mixin Record hasOp T := { + op' : T -> T -> T +}. + +(* #[short(type="MagmaType")] *) +HB.structure Definition Magma := {T of hasOp T}. + +(* +(*BUG: HB.about fails on structure defined relying on autowrap *) + (* #[short(type="semigroupType")] *) + HB.structure Definition Semigroup := {T of hasOp T & isAssoc _ (@op' T) }. + HB.about Semigroup. + HB.about Semigroup.type. + (* Anomaly "Uncaught exception Failure("split_dirpath")."*) + Print wrapper_xx_op'_mwb_isAssoc. *) + +#[wrapper] +HB.mixin Record isAssoc__on__Magma_op' T ( _ : Magma T) := { + private : isAssoc T op' +}. + +#[short(type="semigroupType")] +HB.structure Definition Semigroup := {T of Magma T & isAssoc__on__Magma_op' T }. + +HB.about Semigroup. +HB.about Semigroup.type. + + +HB.factory Record isSemigroup T := { + op'' : T -> T -> T; + opA'' : True +}. + +HB.builders Context G of isSemigroup G. + +HB.instance Definition _ := hasOp.Build G op''. + +(*BUG: the following line does not generate the correspoinding builder*) + (* HB.instance Definition _ := isAssoc.Build G op'' opA''. *) + +HB.instance Definition temp := isAssoc.Build G op'' opA''. +HB.instance Definition _ := isAssoc__on__Magma_op'.Build G temp. + +HB.end. + +HB.mixin Record hasOne T := { + one : T +}. + +HB.structure Definition PointedMagma := {G of hasOne G & Magma G}. + +#[wrapper] +HB.mixin Record isUnital__on__Magma_op' T of PointedMagma T := { + private : isUnital T one op' +}. + +#[short(type="UnitalMagmaType")] +HB.structure Definition UnitalMagma + := {T of PointedMagma T & isUnital__on__Magma_op' T }. + +HB.factory Record isUnitalMagma T of Magma T := { + one' : T; + op1m'' : True; + opm1'' : True +}. + +HB.builders Context T of isUnitalMagma T. + +HB.instance Definition _ := hasOne.Build T one'. + +(*BUG: The one' (from the factory) is not recognized as the one (from hasOne) if the type of temp is not explicity given*) +(* HB.instance Definition temp + : isUnital.phant_axioms T one' op' + (*you can either comment or not the previous line specifying the type, the instruction will fail anyway (the workaround is to remove the prime from one)*) + (*BUG: the "correct" type is not infered *) + := isUnital.Build T one' op' op1m'' opm1''. *) +(* [...] The [...] term has type "isUnital.phant_axioms T one' op'" + which should be a subtype of "isUnital.phant_axioms T one op'". *) +(* NOTE: They are judgmentally equal though*) +Check eq_refl +: isUnital.phant_axioms T one' op' += isUnital.phant_axioms T one op'. + +(* In monoid.v the T can be implicit, is it correctly infered? *) +(* In monoid.v one and one' have the same name*) + + +HB.instance Definition temp +: isUnital.phant_axioms T one op' +:= isUnital.Build T one' op' op1m'' opm1''. + +(* other working alternative: *) +(* HB.instance Definition temp +:= isUnital.Build T one op' op1m'' opm1''. *) + + +(* HB.instance Definition _ := isMonoidLaw__on__BaseUMagma_MulOne.Build G pippo. *) +Check isUnital.phant_axioms T one' op'. +Check isUnital.phant_axioms T one op'. + +HB.end. + diff --git a/tests/MinimalWrapBugs/noglobref.v b/tests/MinimalWrapBugs/noglobref.v new file mode 100644 index 00000000..ff07f008 --- /dev/null +++ b/tests/MinimalWrapBugs/noglobref.v @@ -0,0 +1,7 @@ +From HB Require Import structures. + +HB.mixin Record isLaw T (l:T) (op : T) := { + opA : True; +}. + +Fail HB.structure Definition Law T l := {op of isLaw T l op}. diff --git a/tests/MinimalWrapBugs/structVS2mixin.v b/tests/MinimalWrapBugs/structVS2mixin.v new file mode 100644 index 00000000..f35e655c --- /dev/null +++ b/tests/MinimalWrapBugs/structVS2mixin.v @@ -0,0 +1,41 @@ +From HB Require Import structures. + +HB.mixin Record Q T (x y : T) := { + q : unit +}. + +HB.mixin Record hasPointX T := { + x : T +}. + +HB.structure Definition XPointed := {T of hasPointX T}. + +HB.mixin Record hasPointY T := { + y : T +}. + +HB.structure Definition YPointed := {T of hasPointY T}. +(* +HB.structure Definition BiPointed + := {T of hasPointX T & hasPointY T}. + *) +#[wrapper] +HB.mixin Record Q__on__BiPointed_xy + T of hasPointX T & hasPointY T := { + private : Q T x y +}. + +HB.structure Definition QBiPointed + := {T of hasPointX T & hasPointY T & Q__on__BiPointed_xy T}. + +HB.factory Record isQBiPointed T of hasPointX T & hasPointY T := { + qq: unit +}. + +HB.builders Context T of isQBiPointed T. + +Check T : QBiPointed.type. + +HB.instance Definition _ := Q.Build T x y qq. + +HB.end. diff --git a/tests/MinimalWrapBugs/structVS2mixinCorrect.v b/tests/MinimalWrapBugs/structVS2mixinCorrect.v new file mode 100644 index 00000000..76423b22 --- /dev/null +++ b/tests/MinimalWrapBugs/structVS2mixinCorrect.v @@ -0,0 +1,39 @@ +From HB Require Import structures. + +HB.mixin Record Q T (x y : T) := { + q : unit +}. + +HB.mixin Record hasPointX T := { + x : T +}. + +HB.structure Definition XPointed := {T of hasPointX T}. + +HB.mixin Record hasPointY T := { + y : T +}. + +HB.structure Definition YPointed := {T of hasPointY T}. + +HB.structure Definition BiPointed + := {T of hasPointX T & hasPointY T}. + +#[wrapper] +HB.mixin Record Q__on__BiPointed_xy + T of BiPointed T := { + private : Q T x y +}. + +HB.structure Definition QBiPointed + := {T of hasPointX T & hasPointY T & Q__on__BiPointed_xy T}. + +HB.factory Record isQBiPointed T of hasPointX T & hasPointY T := { + qq: unit +}. + +HB.builders Context T of isQBiPointed T. + +HB.instance Definition _ := Q.Build T x y qq. + +HB.end. \ No newline at end of file diff --git a/tests/MinimalWrapBugs/typeNotInfered.v b/tests/MinimalWrapBugs/typeNotInfered.v new file mode 100644 index 00000000..10b31a07 --- /dev/null +++ b/tests/MinimalWrapBugs/typeNotInfered.v @@ -0,0 +1,63 @@ +From HB Require Import structures. + +HB.mixin Record Q T (l r : T) := { + q : True +}. + +HB.mixin Record hasLeft T := { + sx : T +}. +HB.structure Definition Lefted := {T of hasLeft T}. + +HB.mixin Record hasRight T := { + dx : T +}. +HB.structure Definition Righted := {T of hasRight T}. + +HB.structure Definition Ambidextrous + := {T of Lefted T & Righted T}. + +#[wrapper] +HB.mixin Record Q__on__Ambidextrous_dx T of Ambidextrous T := { + private : Q T sx dx +}. + +HB.structure Definition QAmbidextrous + := {T of Ambidextrous T & Q__on__Ambidextrous_dx T}. + +HB.factory Record isQAmbidextrous T := { + l : T; + r : T; + qlr : True +}. + +HB.builders Context T of isQAmbidextrous T. + +HB.instance Definition _ := hasLeft.Build T l. +HB.instance Definition _ := hasRight.Build T r. + +(*WORKAROUND*) + (* HB.instance Definition temp + : Q.axioms_ T sx dx + := Q.Build T l dx qlr. *) + +(*other WORKAROUND*) + (* HB.instance Definition temp + := Q.Build T sx dx qlr. *) + +(*other WORKAROUND*) + (* HB.instance Definition temp + := Q.Build T sx r qlr. *) + (* is it ok that this work?*) + +(*BUG: Despite being judgmentally equal using the data from the factory or from the infered structure is relevant (note that, in practice, they can have the same name)*) +Check eq_refl : l = sx. +Check eq_refl : r = dx. + + +HB.instance Definition temp +(* : Q.axioms_ T l dx *) +:= Q.Build T l dx qlr. + +(* HB.instance Definition _ := Q__on__Ambidextrous_dx.Build T temp. *) +HB.end. \ No newline at end of file diff --git a/tests/MinimalWrapBugs/unwrappedSubject.v b/tests/MinimalWrapBugs/unwrappedSubject.v new file mode 100644 index 00000000..6bdc44e8 --- /dev/null +++ b/tests/MinimalWrapBugs/unwrappedSubject.v @@ -0,0 +1,41 @@ +(*It seems, once a subject is linked with a wrapped mixin, +it can't be instantiated as an unwrapped subject*) + +From HB Require Import structures. + +HB.mixin Record Q T (f: T->T) := { + q : unit +}. + +HB.mixin Record hasSelfMap T := { + selfmap : T -> T +}. + +HB.structure Definition SelfMapped := {T of hasSelfMap T}. + +(* Comment this to avoid the fail, from here *) + + #[wrapper] + HB.mixin Record Q__on__SelfMapped_selfmap T of SelfMapped T := { + private : Q T selfmap + }. + + HB.structure Definition QSelfMapped := {T of hasSelfMap T & Q__on__SelfMapped_selfmap T}. + +(* to here *) + +HB.instance Definition _ := hasSelfMap.Build nat (fun n => n). + +Check @selfmap nat. + +HB.mixin Record hasLaw T (x: T->T) := { + law : unit +}. + +HB.structure Definition Law T := {x of hasLaw T x}. + +(*BUG: this should work*) +#[verbose,wrapper=off] HB.instance Definition _ := hasLaw.Build nat (@selfmap nat) tt. + +Check @law nat _. +Check @selfmap nat : Law.type nat. diff --git a/tests/auto_wrap.v b/tests/auto_wrap.v new file mode 100644 index 00000000..e07ba7cd --- /dev/null +++ b/tests/auto_wrap.v @@ -0,0 +1,22 @@ +From HB Require Import structures. + +HB.mixin Record isAssoc T (f : T -> T -> T) := { opA : forall x y z, f (f x y) z = f x (f y z) }. +HB.structure Definition AssociativeOperation T := { f of isAssoc T f }. + + +HB.mixin Record hasOp T := { op : T -> T -> T }. +HB.structure Definition Magma := { T of hasOp T }. + +(* HB.structure Definition Monoid := { T of hasOp T & isAssoc T op }. BUG *) +(* HB.structure Definition Monoid := { T of hasOp T & isAssoc _ (op : T -> _ -> _) }. BUG *) +HB.structure Definition Monoid := { T of hasOp T & isAssoc _ (@op T) }. (* and the unit .. *) + +Axiom plus_ass : forall x y z, plus (plus x y) z = plus x (plus y z). + +HB.instance Definition _ : hasOp nat := hasOp.Build nat plus. +Check nat : Magma.type. + +HB.instance Definition _ : isAssoc nat op := isAssoc.Build nat plus plus_ass. +Check plus : AssociativeOperation.type nat. + +Check nat : Monoid.type. diff --git a/tests/hnf.v b/tests/hnf.v index b219a6a8..e37b2626 100644 --- a/tests/hnf.v +++ b/tests/hnf.v @@ -10,9 +10,9 @@ HB.end. #[hnf] HB.instance Definition _ := f.Build nat (3 + 2). Print Datatypes_nat__canonical__hnf_S. -Print HB_unnamed_mixin_8. +Print HB_unnamed_mixin_7. HB.instance Definition _ := f.Build bool (3 + 2). Print Datatypes_bool__canonical__hnf_S. -Print HB_unnamed_mixin_12. +Print hnf_f__to__hnf_M__9. diff --git a/tests/mindep.v b/tests/mindep.v new file mode 100644 index 00000000..40d74695 --- /dev/null +++ b/tests/mindep.v @@ -0,0 +1,20 @@ +From HB Require Import structures. + +HB.mixin Record m1 T := { t1 : T }. +(* HB.structure Definition Pointed1 := { T of m1 T }. *) + +HB.mixin Record m2 T := { t2 : T }. +(* HB.structure Definition Pointed2 := { T of m2 T }. *) + +(* HB.structure Definition Pointed12 := { T of m1 T & m2 T }. *) + +HB.mixin Record m3 T := { t3 : T }. +HB.structure Definition TPointed123 := { T of m2 T & m1 T & m3 T }. + +HB.mixin Record m4 T := { t4 : T }. +(* HB.structure Definition TPointed124 := { T of m2 T & m1 T & m4 T }. *) + + +HB.mixin Record m T of TPointed123 T := { + p : t1 = t2 :> T +}. diff --git a/tests/not_same_key.v.out b/tests/not_same_key.v.out index b04461f4..21820874 100644 --- a/tests/not_same_key.v.out +++ b/tests/not_same_key.v.out @@ -1,2 +1,3 @@ The command has indeed failed with message: -HB: all mixins must have the same key +HB: expecting a factory on T +or a factory on a structure operation or tag. Got: B.phant_axioms T T1 diff --git a/tests/tag_wrap.v b/tests/tag_wrap.v new file mode 100644 index 00000000..d8768fc4 --- /dev/null +++ b/tests/tag_wrap.v @@ -0,0 +1,39 @@ +From HB Require Import structures. + +HB.mixin Record isSomething T := { clearly : True }. +HB.structure Definition Something := { T of isSomething T }. + +HB.mixin Record isSomethingElse (T : Type) := { p : True }. + +HB.tag Definition tag1 (T : Something.type) : Type := T. + +#[wrapper] +HB.mixin Record tag1_isSomethingElse T of Something T := { + private : isSomethingElse (tag1 T) +}. + +HB.tag Definition tag2 (T : Something.type) : Type := T. + +#[wrapper] +HB.mixin Record tag2_isSomethingElse T of Something T := { + private : isSomethingElse (tag2 T) +}. + +(* This is a bug, maybe even in master. If I declare an instance on a mixin + which leads to no new structure instance, then the mixin is not use later + on *) +HB.structure Definition magic1 := { T of + isSomething T & + isSomethingElse (tag1 T) +}. + +HB.structure Definition magic := { T of + isSomething T & + isSomethingElse (tag1 T) & + isSomethingElse (tag2 T) +}. + +HB.instance Definition _ : isSomething nat := isSomething.Build nat I. +HB.instance Definition _ : isSomethingElse (tag1 nat) := isSomethingElse.Build nat I. +HB.instance Definition _ : isSomethingElse (tag2 nat) := isSomethingElse.Build nat I. +Check nat : magic.type. diff --git a/tests/unit/close_hole_term.v b/tests/unit/close_hole_term.v index 6370fe04..61ff98f9 100644 --- a/tests/unit/close_hole_term.v +++ b/tests/unit/close_hole_term.v @@ -21,7 +21,7 @@ inj x y : S (f x) (f y) -> R x y. Elpi Query HB.structure lp:{{ Y = {{Inj}}, %Inj has 5 implicit arguments - saturate-type-constructor Y X, + saturate-type-constructor 0 Y X, % X needs to be typechecked here to get rid of the holes of the types of its arguments coq.typecheck X _ ok, abstract-holes.main X Z, diff --git a/tests/unit/enrich_type.v b/tests/unit/enrich_type.v index b25bdeba..21e9061c 100644 --- a/tests/unit/enrich_type.v +++ b/tests/unit/enrich_type.v @@ -3,18 +3,18 @@ From elpi Require Import elpi. From Corelib Require Export Setoid. Elpi Query HB.structure lp:{{ - saturate-type-constructor {{nat}} X, + saturate-type-constructor 0 {{nat}} X, std.assert! (X = {{nat}}) "wrong enriched type" }}. Elpi Query HB.structure lp:{{ - saturate-type-constructor {{list}} X, + saturate-type-constructor 0 {{list}} X, std.assert! (X = app [{{list}}, Y_]) "wrong enriched type" }}. Elpi Query HB.structure lp:{{ Y = (x \ (y \ {{(prod (list lp:x) (list lp:y))}})), - saturate-type-constructor (Y _ _) X, + saturate-type-constructor 0 (Y _ _) X, std.assert! (X = (app [{{prod}}, (app[{{list}},X1_]), app[{{list}},C_]])) "wrong enriched type" }}. @@ -22,6 +22,6 @@ Class Inj {A B} (R : relation A) (S : relation B) (f : A -> B) : Prop := inj x y : S (f x) (f y) -> R x y. Elpi Query HB.structure lp:{{ - saturate-type-constructor {{Inj}} X, + saturate-type-constructor 0 {{Inj}} X, std.assert! (X = app [(global (const Inj_)), A_, B_, R_, S_, F_]) "wrong enriched type" }}. diff --git a/tests/wrap.v b/tests/wrap.v new file mode 100644 index 00000000..1e6298b8 --- /dev/null +++ b/tests/wrap.v @@ -0,0 +1,25 @@ +From HB Require Import structures. + +HB.mixin Record isAssoc T (f : T -> T -> T) := { opA : forall x y z, f (f x y) z = f x (f y z) }. +HB.structure Definition AssociativeOperation T := { f of isAssoc T f }. + + +HB.mixin Record hasOp T := { op : T -> T -> T }. +HB.structure Definition Magma := { T of hasOp T }. + + +#[wrapper] +HB.mixin Record isAssoc__for__Magma_op T of Magma T := { + private : isAssoc T op +}. + +HB.structure Definition Monoid := { T of hasOp T & isAssoc__for__Magma_op T }. + +Axiom plus_ass : forall x y z, plus (plus x y) z = plus x (plus y z). + +HB.instance Definition _ : hasOp nat := hasOp.Build nat plus. +Check nat : Magma.type. + +HB.instance Definition _ : isAssoc nat op := isAssoc.Build nat plus plus_ass. +Check nat : Monoid.type. +Check plus : AssociativeOperation.type nat.