From 125ecbc1054fcae6b7e949fcf21a082721880a58 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 28 Apr 2025 10:56:05 +0200 Subject: [PATCH 01/34] fix test-suite rocq 9 --- Makefile.test-suite.coq.local | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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' \ From dce339f718e9276ecd1c813883ab17eb56cbf665 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 28 Apr 2025 14:38:10 +0200 Subject: [PATCH 02/34] attribute #[unsafe(univ)] --- HB/common/utils.elpi | 9 +++++++++ HB/structures.v | 2 +- 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/HB/common/utils.elpi b/HB/common/utils.elpi index ae4216b6..17837653 100644 --- a/HB/common/utils.elpi +++ b/HB/common/utils.elpi @@ -330,3 +330,12 @@ saturate-type-constructor T ET :- coq.typecheck T TH ok, coq.count-prods TH N, coq.mk-app T {coq.mk-n-holes N} ET. + + +pred with-unsafe-univ i:prop. +with-unsafe-univ P :- get-option "unsafe.univ" tt, !, + coq.option.get ["Universe","Checking"] Old, + coq.option.set ["Universe","Checking"] (coq.option.bool ff), + P, + coq.option.set ["Universe","Checking"] Old. +with-unsafe-univ P :- P. diff --git a/HB/structures.v b/HB/structures.v index e3a0b52e..806968eb 100644 --- a/HB/structures.v +++ b/HB/structures.v @@ -660,7 +660,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 (structure.declare N B Univ))), ]. }}. From c7f868c6aec57c9301ac1f586054880239b1f0d8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 28 Apr 2025 14:37:41 +0200 Subject: [PATCH 03/34] wrapping [wip] Co-Authored-by: ptorrx --- HB/common/database.elpi | 18 +- HB/common/synthesis.elpi | 29 +++ HB/common/utils-synterp.elpi | 4 +- HB/common/utils.elpi | 16 +- HB/context.elpi | 50 +++++- HB/export.elpi | 4 +- HB/factory.elpi | 55 +++++- HB/instance.elpi | 231 +++++++++++++++++++----- HB/pack.elpi | 63 +++++-- HB/status.elpi | 13 +- HB/structure.elpi | 331 +++++++++++++++++++++++++++++++++-- HB/structures.v | 114 +++++++++++- _CoqProject.test-suite | 4 + tests/auto_wrap.v | 20 +++ tests/hnf.v | 2 +- tests/not_same_key.v.out | 3 +- tests/tag_wrap.v | 39 +++++ tests/wrap.v | 24 +++ 18 files changed, 935 insertions(+), 85 deletions(-) create mode 100644 tests/auto_wrap.v create mode 100644 tests/tag_wrap.v create mode 100644 tests/wrap.v diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 425a8b52..41fd251d 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -51,10 +51,10 @@ pred module-to-export_module-nice i:prop, o:id. module-to-export_module-nice (module-to-export _ M _) M. pred instance-to-export_instance i:prop, o:constant. -instance-to-export_instance (instance-to-export _ _ M) M. +instance-to-export_instance (instance-to-export _ M) M. pred instance-to-export_instance-nice i:prop, o:id. -instance-to-export_instance-nice (instance-to-export _ M _) M. +instance-to-export_instance-nice (instance-to-export _ M) ID :- coq.gref->id (const M) ID. pred abbrev-to-export_name i:prop, o:id. abbrev-to-export_name (abbrev-to-export _ N _) N. @@ -181,6 +181,8 @@ toposort-proj.acc Proj ES Acc [A|In] Out :- std.do![ topo-find B A => toposort-proj.acc Proj ES [B|Acc] In Out ]. +% TODO: check if topo-find-all is really needed + % Classes can be topologically sorted according to the subclass relation pred toposort-classes.mk-class-edge i:prop, o:pair classname classname. toposort-classes.mk-class-edge (sub-class C1 C2 _ _) (pr C2 C1). @@ -435,12 +437,15 @@ structure-nparams Structure NParams :- factory-nparams Class NParams. pred factory? i:term, o:w-args factoryname. -factory? S (triple F Params T) :- +factory? S (triple F Params T) :- factory?-split S F [_|Params] T _. + +pred factory?-split i:term, o:factoryname, o:list term, o:term, o:list term. +factory?-split S F [global GR|Params] T Rest :- not (var S), !, safe-dest-app S (global GR) Args, factory-alias->gref GR F ok, factory-nparams F NP, !, - std.split-at NP Args Params [T|_]. + std.split-at NP Args Params [T|Rest]. % [find-max-classes Mixins Classes] states that Classes is a list of classes % which contain all the mixins in Mixins. @@ -460,3 +465,8 @@ find-max-classes [M|Mixins] [C|Classes] :- ]. find-max-classes [M|_] _ :- coq.error "HB: cannot find a class containing mixin" M. +pred is-subject-lifter i:term, o:int, o:classname. +is-subject-lifter (global (const C)) N Class :- exported-op M _ C, wrapper-mixin _ (const C) _, factory-nparams M N, mixin-first-class M Class. +is-subject-lifter (app[global (const C)|_]) N Class :- exported-op M _ C, wrapper-mixin _ (const C) _, factory-nparams M N, mixin-first-class M Class. +is-subject-lifter (global GR) N Class :- tag GR Class N, wrapper-mixin _ GR _. +is-subject-lifter (app[global GR|_]) N Class :- tag GR Class N, wrapper-mixin _ GR _. diff --git a/HB/common/synthesis.elpi b/HB/common/synthesis.elpi index 6444e23c..0a353faa 100644 --- a/HB/common/synthesis.elpi +++ b/HB/common/synthesis.elpi @@ -74,6 +74,13 @@ infer-all-args-let Ps T GR X Diag :- std.do! [ private.instantiate-all-args-let FT T X Diag, ]. +pred try-infer-all-args-let i:list term, i:term, i:gref, o:term. +try-infer-all-args-let Ps T GR X :- std.do! [ + coq.env.typeof GR Ty, + coq.mk-eta (-1) Ty (global GR) EtaF, + coq.subst-fun {std.append Ps [T]} EtaF FT, + private.try-instantiate-all-args-let FT T X, +]. % [assert!-infer-mixin TheType M Out] infers one mixin M on TheType and % aborts with an error message if the mixin cannot be inferred @@ -112,6 +119,17 @@ under-mixin-src-from-factory.do! TheType TheFactory LP :- std.do! [ MLClauses => std.do! LP ]. + +% Given TheType makes the provided list of mixins and instances +% available for inference. +pred under-these-mixin-src.do! i:term, i:list mixinname, i:list constant, o:list prop, i:list prop. +under-these-mixin-src.do! TheType ML TheMixins ClausesHas LP :- std.do! [ + std.map2 ML TheMixins (m\mi\c\ c = mixin-src TheType m (global (const mi))) MLClauses, + std.map-filter MLClauses mixin-src->has-mixin-instance ClausesHas, + MLClauses => std.do! LP +]. + + % Given TheType and a factory instance (on it), builds all the *new* mixins % provided by the factory available for and passes them to the given % continuation @@ -251,6 +269,7 @@ instantiate-all-these-mixin-args (fun _ Tm F) T ML R :- coq.safe-dest-app Tm (global TmGR) _, factory-alias->gref TmGR M ok, 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}), !, instantiate-all-these-mixin-args (F X) T ML R. @@ -270,6 +289,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 diff --git a/HB/common/utils-synterp.elpi b/HB/common/utils-synterp.elpi index 73932c1a..6a6dccef 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). pred if-verbose i:prop. diff --git a/HB/common/utils.elpi b/HB/common/utils.elpi index 17837653..2aca7c13 100644 --- a/HB/common/utils.elpi +++ b/HB/common/utils.elpi @@ -76,7 +76,7 @@ gref->modname GR NComp Sep ModName :- std.length Path Len, if (Len >= NComp) true (coq.error "Not enough enclosing modules for" {coq.gref->string GR}), std.take NComp Mods L, - std.string.concat Sep {std.rev L} ModName. + std.string.concat Sep {std.rev L} ModName. % TODO: check if the new_int is needed pred gref->modname-label i:gref, i:int, i:string, o:string. gref->modname-label GR NComp Sep ModName :- coq.gref->path GR Path, @@ -294,7 +294,7 @@ pack? (indc K) C :- coq.env.indc K _ _ _ KTy, prod-last-gref KTy (indt I), % TODO: use new API class-def (class C (indt I) _). -pred distribute-w-params i:list-w-params A, o:list (one-w-params A). +pred distribute-w-params i:w-params (list A), o:list (w-params A). distribute-w-params (w-params.cons N T F) L :- pi x\ distribute-w-params (F x) (L1 x), std.map (L1 x) (bind-cons N T x) L. distribute-w-params (w-params.nil N T F) L :- @@ -316,6 +316,18 @@ re-enable-id-phant T T1 :- (pi f1 f2 t v\ copy {{lib:@hb.ignore_disabled lp:t lp:f1 lp:v lp:f2}} {{lib:@hb.ignore lp:t lp:v}} :- !) => copy T T1. +pred disable-id-phant-indt-decl i:indt-decl, o:indt-decl. +disable-id-phant-indt-decl D D1 :- + (pi fresh fresh1 t v\ copy {{lib:@hb.id lp:t lp:v}} {{lib:@hb.id_disabled lp:t lp:fresh lp:v lp:fresh1}} :- !) => + (pi fresh fresh1 t v\ copy {{lib:@hb.ignore lp:t lp:v}} {{lib:@hb.ignore_disabled lp:t lp:fresh lp:v lp:fresh1}} :- !) => + copy-indt-decl D D1. + +pred re-enable-id-phant-indt-decl i:indt-decl, o:indt-decl. +re-enable-id-phant-indt-decl D D1 :- + (pi f1 f2 t v\ copy {{lib:@hb.id_disabled lp:t lp:f1 lp:v lp:f2}} {{lib:@hb.id lp:t lp:v}} :- !) => + (pi f1 f2 t v\ copy {{lib:@hb.ignore_disabled lp:t lp:f1 lp:v lp:f2}} {{lib:@hb.ignore lp:t lp:v}} :- !) => + copy-indt-decl D D1. + pred prod-last i:term, o:term. prod-last (prod N S X) Y :- !, @pi-decl N S x\ prod-last (X x) Y. prod-last X X :- !. diff --git a/HB/context.elpi b/HB/context.elpi index 4b04e5f0..e9f7dd47 100644 --- a/HB/context.elpi +++ b/HB/context.elpi @@ -57,6 +57,40 @@ namespace private { % to the corresponding mixin using mixin-for pred postulate-mixin i:term, i:w-args mixinname, i:triple (list constant) (list prop) (list (w-args mixinname)), o:triple (list constant) (list prop) (list (w-args mixinname)). + +postulate-mixin TheType (triple M Ps T) (triple CL MSL MLwP) (triple OutCL [MC|MSL] [NewMwP|MLwP]) :- wrapper-mixin M _ _, !, MSL => std.do! [ + NameVar is "local_mixin_private_" ^ {gref->modname M 2 "_"}, + NameMixin is "local_mixin_" ^ {gref->modname M 2 "_"}, + + if-verbose (coq.say "HB: postulate and wrap" NameVar "on" {coq.term->string T}), + + synthesis.infer-all-gref-deps Ps T M TySkel, + % was synthesis.infer-all-mixin-args Ps T M TySkel, + % if-verbose (coq.say "HB: postulate-mixin checking" TySkel), + % std.assert-ok! (coq.typecheck Ty _) "postulate-mixin: Ty illtyped", + std.assert-ok! (coq.elaborate-ty-skeleton TySkel _ Ty) + "postulate-mixin: Ty illtyped", + + Ty = app[global M|Args], + factory-constructor M K, + coq.mk-app (global K) Args KArgs, + std.assert-ok! (coq.typecheck KArgs {{ lp:VarTy -> _ }}) "brrr", + + log.coq.env.add-section-variable-noimplicits NameVar VarTy V, + + coq.mk-app KArgs [global (const V)] TheMixin, + + log.coq.env.add-const-noimplicits NameMixin TheMixin Ty @transparent! C, + + factory? Ty NewMwP, + + declare-instances-from-postulated-mixin TheType M T C MC NewCL, + + std.append CL NewCL OutCL, + +]. + + postulate-mixin TheType (triple M Ps T) (triple CL MSL MLwP) (triple OutCL [MC|MSL] [NewMwP|MLwP]) :- MSL => std.do! [ Name is "local_mixin_" ^ {gref->modname M 2 "_"}, @@ -70,11 +104,19 @@ postulate-mixin TheType (triple M Ps T) (triple CL MSL MLwP) (triple OutCL [MC|M "postulate-mixin: Ty illtyped", log.coq.env.add-section-variable-noimplicits Name Ty C, factory? Ty NewMwP, + + declare-instances-from-postulated-mixin TheType M T C MC NewCL, + + std.append CL NewCL OutCL, + + ]. + +pred declare-instances-from-postulated-mixin i:term, i:mixinname, i:term, i:constant, o:prop, o:list constant. +declare-instances-from-postulated-mixin TheType M T C MC NewCL :- std.do! [ MC = mixin-src T M (global (const C)), MC => get-option "local" tt => - instance.declare-all TheType {findall-classes-for [M]} NewCSL, - std.map NewCSL snd NewCL, - std.append CL NewCL OutCL - ]. + instance.declare-all TheType {findall-classes-for [M]} NewCL, +]. + }} diff --git a/HB/export.elpi b/HB/export.elpi index 2fb15aa3..ea823332 100644 --- a/HB/export.elpi +++ b/HB/export.elpi @@ -47,7 +47,7 @@ export.reexport-all-modules-and-CS Filter :- std.do! [ std.forall2 NiceMods Mods log.coq.env.export-module, - std.findall (instance-to-export File NiceInstance_ Const_) InstCL, + std.findall (instance-to-export File Const_) InstCL, std.filter {std.list-uniq InstCL} (export.private.instance-in-module MFilter) InstCLFiltered, std.map InstCLFiltered instance-to-export_instance Insts, @@ -83,7 +83,7 @@ module-in-module PM (module-to-export _ _ M) :- std.appendR PM _ PC. % sublist pred instance-in-module i:list string, i:prop. -instance-in-module PM (instance-to-export _ _ C) :- +instance-in-module PM (instance-to-export _ C) :- coq.gref->path (const C) PC, std.appendR PM _ PC. % sublist diff --git a/HB/factory.elpi b/HB/factory.elpi index ef00f61a..81606565 100644 --- a/HB/factory.elpi +++ b/HB/factory.elpi @@ -226,6 +226,53 @@ declare-asset Arg AssetKind :- std.do! [ ) ]. +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%% auxiliary code for wrapper-mixin + +pred extract_from_record_decl i: (term -> gref -> prop), i:indt-decl, o:gref. +extract_from_record_decl P (parameter ID _ Ty R) Out :- + @pi-parameter ID Ty p\ + extract_from_record_decl P (R p) Out. +extract_from_record_decl P (record _ _ _ (field _ _ Ty (x\end-record))) GR0 :- + P Ty GR0. + +pred extract_from_rtty i: (term -> gref -> prop), i: term, o:gref. +extract_from_rtty P (prod N Ty TF) Out1 :- + @pi-decl N Ty p\ + extract_from_rtty P (TF p) Out1. +extract_from_rtty P Ty Gr :- P Ty Gr. + +pred xtr_fst_op i:term, o:gref. +xtr_fst_op Ty Gr1 :- + Ty = (app [global Gr0| _]), + factory-alias->gref Gr0 Gr1 ok. + +pred xtr_snd_op i:term, o:gref. +xtr_snd_op Ty Gr :- + % TODO: use factory? from database.elpi + Ty = (app [global Gr0| Args]), + factory-alias->gref Gr0 Gr1 ok, + factory-nparams Gr1 N, + std.nth N Args (app [global Gr| _]). + +pred extract_wrapped i:indt-decl, o:gref. +extract_wrapped In Out :- + extract_from_record_decl (extract_from_rtty xtr_fst_op) In Out. + +pred extract_subject i:indt-decl, o:gref. +extract_subject In Out :- + extract_from_record_decl (extract_from_rtty xtr_snd_op) In Out. + +pred wrapper_mixin_aux i:gref, o:gref, o:gref. +wrapper_mixin_aux XX Gr1 Gr2 :- + XX = (indt I), + coq.env.indt-decl I D, + extract_subject D Gr1, + extract_wrapped D Gr2. + +%%% end auxiliary code for wrapper-mixin +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + pred declare-mixin-or-factory i:list prop, i:list constant, i:list term, i:term, i:term, i:record-decl, i:list-w-params factoryname, i:id, i:asset. declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance @@ -262,6 +309,12 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance % TODO: should this be in the Exports module? + % if the wrapper option is on, build the wrapper clause + if (get-option "wrapper" tt) + ((wrapper_mixin_aux (indt R) NSbj WMxn), + (WrapperClauses = [wrapper-mixin (indt R) NSbj WMxn])) + (WrapperClauses = []), + if-verbose (coq.say {header} "declare notation Build"), GRDepsClauses => phant.of-gref ff GRK [] PhGRK, @@ -278,7 +331,7 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance if-verbose (coq.say {header} "start module Exports"), log.coq.env.begin-module "Exports" none, - std.flatten [Clauses, GRDepsClauses, [ + std.flatten [Clauses, GRDepsClauses, WrapperClauses, [ factory-constructor (indt R) GRK, factory-nparams (indt R) NParams, factory-builder-nparams BuildConst NParams, diff --git a/HB/instance.elpi b/HB/instance.elpi index 063b4fe0..2249e8d9 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 pred declare-existing i:argument, i:argument. @@ -22,7 +23,7 @@ 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. -pred declare-const i:id, i:term, i:arity, o:list (pair id constant), o:list (pair id constant). +pred declare-const i:id, i:term, i:arity, o:list constant, o:list constant. declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [ std.assert-ok! (coq.elaborate-arity-skeleton TyWPSkel _ TyWP) "Definition type illtyped", coq.arity->term TyWP Ty, @@ -71,17 +72,39 @@ declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [ 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 - ), + if (current-mode (builder-from TheType TheFactoryForBuilderSection FGR _)) + % instance in a builder section %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + (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 Clauses CFL CSL, + + private.close-section-if-has-params TyWP SectionName, + ]) + % instance in regular section %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + (std.do![ + + % derive all mixins the factory provides + private.declare-mixins-from-factory Factory TheType TheFactory ML TheMixins, + + % regular instance %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + if (get-option "wrapper" ff ; not(is-subject-lifter TheType _ _)) + % regular subject %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + (private.declare-regular-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL, CFL = CSL) + % wrapper %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + (private.declare-wrapper-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL, CFL = CSL) + , + + % shared to all branches + if (get-option "export" tt) + (coq.env.current-library File, + std.map CSL (c\r\ r = instance-to-export File c) ClausesExp) + (ClausesExp = []), + + std.append ClausesHas ClausesExp Clauses, + ]), % we accumulate clauses now that the section is over acc-clauses current Clauses @@ -97,11 +120,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. -pred declare-all i:term, i:list class, o:list (pair id constant). +pred declare-all i:term, i:list class, o: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, @@ -118,11 +141,11 @@ 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 -pred declare-all-on-type-constructor i:term, i:list class, o:list (pair id constant). +pred declare-all-on-type-constructor i:term, i:list class, o:list 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] :- +declare-all-on-type-constructor 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 @@ -224,7 +247,7 @@ namespace private { shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }. pred declare-instance i:factoryname, i:term, i:term, - o:list prop, o:list (pair id constant), o:list (pair id constant). + o:list prop, o:list constant, o:list constant. declare-instance Factory T F Clauses CFL CSL :- current-mode (builder-from T TheFactory FGR _), !, if (get-option "local" tt) @@ -237,15 +260,17 @@ declare-instance Factory T F Clauses CFL CSL :- declare-canonical-instances-from-factory Factory T F Clauses1 CFL CSL, if (get-option "export" tt) (coq.env.current-library File, - std.map {std.append CFL CSL} (x\r\ sigma i c\ x = pr i c, r = instance-to-export File i c) Clauses2) + std.map CSL (c\r\ r = instance-to-export File c) Clauses21, + std.map CFL (c\r\ r = instance-to-export File c) Clauses22, + std.append Clauses21 Clauses22 Clauses2) (Clauses2 = []), std.append Clauses1 Clauses2 Clauses. -% [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 -pred add-mixin i:term, i:factoryname, i:bool, i:mixinname, - o:list prop, o:list (pair id constant). -add-mixin T FGR MakeCanon MissingMixin [MixinSrcCl, BuilderDeclCl] CSL :- std.do! [ +pred add-mixin i:term, i:factoryname, i:mixinname, + o:prop, o:prop, o:constant. +add-mixin T FGR MissingMixin MixinSrcCl BuilderDeclCl C :- std.do! [ new_int N, % timestamp synthesis.assert!-infer-mixin T MissingMixin Bo, @@ -264,23 +289,16 @@ add-mixin T FGR MakeCanon MissingMixin [MixinSrcCl, BuilderDeclCl] CSL :- std.do (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 = []), ]. -pred add-all-mixins i:term, i:factoryname, i:list mixinname, i:bool, - o:list prop, o: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 -]. + +pred add-all-mixins i:term, i:factoryname, i:list mixinname, + o:list prop, o:list constant. +add-all-mixins _T _FGR [] [] []. +add-all-mixins T FGR [M|ML] [MixinSrcCL,BuilderDeclCL | CL] [C|CC] :- std.do! [ + add-mixin T FGR M MixinSrcCL BuilderDeclCL 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 @@ -305,21 +323,28 @@ postulate-arity (arity Ty) ArgsRev X T Ty :- % can access their theory and notations pred declare-canonical-instances-from-factory-and-local-builders i:factoryname, i:term, i:term, i:term, i:factoryname, - o:list prop, o:list (pair id constant), o:list (pair id constant). + o:list prop, o:list constant, o:list constant. declare-canonical-instances-from-factory-and-local-builders Factory T F _TheFactory FGR Clauses CFL CSL :- std.do! [ 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 Clauses CFL, ]), list-w-params_list {factory-provides Factory} ML, Clauses => declare-all T {findall-classes-for ML} CSL, ]. +pred make-mixin-canonical i:constant, o:option constant. +make-mixin-canonical C (some C) :- 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), +]. +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 pred declare-canonical-instances-from-factory - i:factoryname, i:term, i:term, o: list prop, o:list (pair id constant), o:list (pair id constant). + i:factoryname, i:term, i:term, o: list prop, o:list constant, o:list constant. declare-canonical-instances-from-factory Factory T F ClausesHas CFL CSL :- std.do! [ % The order of the following two "under...do!" is crucial, % priority must be given to canonical mixins @@ -329,13 +354,137 @@ 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.do! [ + % 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.do! [ + % 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.do![ + 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. +declare-wrapper-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL :- std.do![ + 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, + 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.do! [ + + % K is the mixin constructor (Build) for WrapperMixin + factory-constructor WrapperMixin K, + factory-nparams WrapperMixin NParams, + + % We are only interested in the last parameter of the constructor + % type, which is the current instance + % (which is a Mixin instance on the new Subject). + % In monoid_enriched_cat.v, we are targeting the code + % + % HB.instance Definition funQ_hom_isMon := + % hom_isMon.Axioms_ _ _ funQ_isMon. + % which Coq can compute to stand for + % hom_isMon.Axioms_ Type funQ funQ_isMon. + % + % We compute the number of the underscores and we pass + % them as arguments followed by Instance. + coq.env.typeof K KTy, + coq.count-prods KTy KN, + KN0 is KN - 1, + coq.mk-n-holes KN0 Holes, + + std.append Holes [Instance] Args, + + % the body of the new wrapper instance + NewInstance = app[global K| Args], + + std.assert-ok! (coq.typecheck NewInstance Ty) "cannot wrap", + + coq.safe-dest-app Ty _Factory FArgs, + std.nth NParams FArgs WrapperSubject, + + Name is "wrapped__" ^ {std.any->string {new_int}}, + + log.coq.env.add-const-noimplicits Name NewInstance Ty @transparent! C, + ]. + +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. pred hack-section-discharging i:term, o: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..b235ebe7 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 "", @@ -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 3702ce19..c8701e17 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,9 @@ 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 +184,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 +203,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 ------------------------------ */ /* ------------------------------------------------------------------------- */ @@ -608,16 +629,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.spy-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, @@ -627,6 +687,249 @@ 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'), std.spy(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.spy-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). +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. + +pred eta-structure-record i:term, i:int, i:classname, i:list term, o:list term. +eta-structure-record S NP Class L L1 :- + std.split-at NP L Params [_|Rest], + class-def (class Class Structure _), + get-constructor Structure K, + std.map Params copy Params1, + std.map Rest copy Rest1, + coq.mk-app {coq.env.global K} {std.append Params1 [S,_]} EtaS, + std.append Params1 [EtaS|Rest1] L1. }} diff --git a/HB/structures.v b/HB/structures.v index 806968eb..7de0d0c7 100644 --- a/HB/structures.v +++ b/HB/structures.v @@ -171,6 +171,18 @@ pred join o:classname, o:classname, o:classname. % in order to discover two mixins are the same) pred mixin-mem i:term, o:gref. +% [wrapper-mixin Wrapper NewSubject WrappedMixin] +% #[wrapper] HB.mixin Record hom_isMon T of Quiver T := +% { private : forall A B, isMon (@hom T A B) }. +% --> +% wrapper-mixin (indt "hom_isMon") (const "hom") (indt "isMon"). +pred wrapper-mixin o:mixinname, o:gref, o:mixinname. + +% 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,7 +194,9 @@ pred mixin-mem i:term, o:gref. % that contains the mixin M pred mixin-first-class o:mixinname, o: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 @@ -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. @@ -588,6 +602,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]. @@ -684,6 +726,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 20} (x\begin-section "x",end-section), + if (get-option "mathcomp" tt ; get-option "mathcomp.axiom" _) (actions-compat N) true. pred actions-compat i:id. @@ -1217,6 +1263,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/_CoqProject.test-suite b/_CoqProject.test-suite index 31c827eb..506a3242 100644 --- a/_CoqProject.test-suite +++ b/_CoqProject.test-suite @@ -65,6 +65,10 @@ 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 + -R tests HB.tests -R examples HB.examples diff --git a/tests/auto_wrap.v b/tests/auto_wrap.v new file mode 100644 index 00000000..018c9e8c --- /dev/null +++ b/tests/auto_wrap.v @@ -0,0 +1,20 @@ +From HB Require Import structures. + +HB.mixin Record isAssoc T (op : T -> T -> T) := { opA : forall x y z, op (op x y) z = op x (op y z) }. +HB.structure Definition Assop T := { op of isAssoc T op }. + + +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 }. *) +(* HB.structure Definition Monoid := { T of hasOp T & isAssoc _ (op : T -> _ -> _) }. *) +HB.structure Definition Monoid := { T of hasOp T & isAssoc _ (@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. +(* HB.instance Definition _ : isAssoc nat plus := isAssoc.Build nat plus plus_ass. *) +HB.instance Definition _ : isAssoc nat op := isAssoc.Build nat plus plus_ass. + +Check nat : Monoid.type. \ No newline at end of file diff --git a/tests/hnf.v b/tests/hnf.v index b219a6a8..a36d1e6f 100644 --- a/tests/hnf.v +++ b/tests/hnf.v @@ -14,5 +14,5 @@ Print HB_unnamed_mixin_8. 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__11. 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/wrap.v b/tests/wrap.v new file mode 100644 index 00000000..4914237e --- /dev/null +++ b/tests/wrap.v @@ -0,0 +1,24 @@ +From HB Require Import structures. + +HB.mixin Record isAssoc T (op : T -> T -> T) := { opA : forall x y z, op (op x y) z = op x (op y z) }. +HB.structure Definition Assop T := { op of isAssoc T op }. + + +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. +(* HB.instance Definition _ : isAssoc nat plus := isAssoc.Build nat plus plus_ass. *) +HB.instance Definition _ : isAssoc nat op := isAssoc.Build nat plus plus_ass. + +Check nat : Monoid.type. \ No newline at end of file From 2e66a7ce5e8e0bf0a220cc1da3914f18d3506820 Mon Sep 17 00:00:00 2001 From: Calosci Matteo Date: Tue, 13 May 2025 10:36:07 +0200 Subject: [PATCH 04/34] Minimal examples of HB bugs --- tests/MinimalWrapBugs/aboutAutowrap.v | 32 ++++++ tests/MinimalWrapBugs/aboutAutowrap2.v | 33 ++++++ tests/MinimalWrapBugs/buildersofwrap.v | 51 ++++++++ tests/MinimalWrapBugs/buildersofwrap2.v | 44 +++++++ tests/MinimalWrapBugs/canonicalByHand.v | 92 +++++++++++++++ tests/MinimalWrapBugs/mwb.v | 147 ++++++++++++++++++++++++ tests/MinimalWrapBugs/noglobref.v | 9 ++ tests/MinimalWrapBugs/typeNotInfered.v | 62 ++++++++++ 8 files changed, 470 insertions(+) create mode 100644 tests/MinimalWrapBugs/aboutAutowrap.v create mode 100644 tests/MinimalWrapBugs/aboutAutowrap2.v create mode 100644 tests/MinimalWrapBugs/buildersofwrap.v create mode 100644 tests/MinimalWrapBugs/buildersofwrap2.v create mode 100644 tests/MinimalWrapBugs/canonicalByHand.v create mode 100644 tests/MinimalWrapBugs/mwb.v create mode 100644 tests/MinimalWrapBugs/noglobref.v create mode 100644 tests/MinimalWrapBugs/typeNotInfered.v diff --git a/tests/MinimalWrapBugs/aboutAutowrap.v b/tests/MinimalWrapBugs/aboutAutowrap.v new file mode 100644 index 00000000..7fb56660 --- /dev/null +++ b/tests/MinimalWrapBugs/aboutAutowrap.v @@ -0,0 +1,32 @@ +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. +(* Anomaly "Uncaught exception Failure("split_dirpath")." + Please report at http://coq.inria.fr/bugs/. *) + +Print wrapper_xx_op'_mwb_isAssoc. \ No newline at end of file diff --git a/tests/MinimalWrapBugs/aboutAutowrap2.v b/tests/MinimalWrapBugs/aboutAutowrap2.v new file mode 100644 index 00000000..1495f928 --- /dev/null +++ b/tests/MinimalWrapBugs/aboutAutowrap2.v @@ -0,0 +1,33 @@ +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. +(* Anomaly "Uncaught exception Failure("split_dirpath")." + Please report at http://coq.inria.fr/bugs/. *) + +Print wrapper_xx_op'_mwb_isAssoc. \ No newline at end of file diff --git a/tests/MinimalWrapBugs/buildersofwrap.v b/tests/MinimalWrapBugs/buildersofwrap.v new file mode 100644 index 00000000..3cb221a2 --- /dev/null +++ b/tests/MinimalWrapBugs/buildersofwrap.v @@ -0,0 +1,51 @@ +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 +}. + +(* 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. + (* As expected, any one of the two following work*) + HB.structure Definition QPointed := {T of hasPoint T & Q__on__Pointed_x T }. + HB.structure Definition QPointed' := {T of isQPointed T}. *) + +HB.builders Context T of isQPointed T. + +HB.instance Definition _ := hasPoint.Build T y. + +HB.instance Definition _ := Q.Build T y qy. + +HB.end. + +HB.status. (* BUG: The builder targetting Q__on__Pointed_x is missing *) +Fail HB.structure Definition QPointed' := {T of isQPointed T}. +(* Structure buildersofwrap2_Pointed contains the same mixins as QPointed' *) + +(* Though, this keep working... *) +HB.structure Definition QPointed := {T of hasPoint T & Q__on__Pointed_x T }. diff --git a/tests/MinimalWrapBugs/buildersofwrap2.v b/tests/MinimalWrapBugs/buildersofwrap2.v new file mode 100644 index 00000000..eb483ac8 --- /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 y 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..59311f4f --- /dev/null +++ b/tests/MinimalWrapBugs/canonicalByHand.v @@ -0,0 +1,92 @@ +From HB Require Import structures. + +HB.mixin Record Q1 T (t:T) (l : T -> T) := { + q : True; +}. + +HB.structure Definition QPSMLaw1 T (t:T) := {l of Q1 T t l}. + +HB.mixin Record Q2 T (t:T) (l : T -> T) := { + q : True; +}. + +HB.structure Definition QPSMLaw2 T (t:T) := {l of Q2 T t l}. + +HB.structure Definition QPSMLaw12 T (t:T) := {l of QPSMLaw1 T t l & QPSMLaw2 T t l}. + + +HB.mixin Record hasPoint T := { + t : T +}. +HB.structure Definition Pointed := {T of hasPoint T}. + +HB.mixin Record hasSelfMap T := { + l : T -> T +}. +HB.structure Definition SelfMapped := {T of hasSelfMap T}. + +HB.structure Definition PointedSelfMapped + := {T of Pointed T & SelfMapped T}. + +#[wrapper] +HB.mixin Record Q1__on__PointedSelfMapped_t T of PointedSelfMapped T := { + private : Q1 T t l +}. +HB.structure Definition Q1PSM +:= {T of PointedSelfMapped T & Q1__on__PointedSelfMapped_t T}. + +#[wrapper] +HB.mixin Record Q2__on__PointedSelfMapped_t T of PointedSelfMapped T := { + private : Q2 T t l +}. +HB.structure Definition Q2PSM +:= {T of PointedSelfMapped T & Q2__on__PointedSelfMapped_t T}. + +HB.structure Definition Q12PSM + := {T of PointedSelfMapped T & Q1PSM T & Q2PSM T}. + +HB.factory Record isQ12PSM T := { + point : T; + selfmap : T -> T; + q1term : True; + q2term : True +}. + +HB.builders Context T of isQ12PSM T. + +HB.instance Definition _ := hasPoint.Build T point. +HB.instance Definition _ := hasSelfMap.Build T selfmap. + +HB.instance Definition temp1 := Q1.Build T point selfmap q1term. +HB.instance Definition _ := Q1__on__PointedSelfMapped_t.Build T temp1. +HB.instance Definition temp2 := Q2.Build T point selfmap q2term. +HB.instance Definition _ := Q2__on__PointedSelfMapped_t.Build T temp2. + +HB.end. + +HB.status. + +HB.about Q12PSM. + +Print Canonical Projections l. +Check fun (R : Q12PSM.type) => @l R : QPSMLaw1.type R (@t R). +Check fun (R : Q12PSM.type) => @l R : QPSMLaw2.type R (@t R). + +(*BUG: this should be inferred automatically*) +Fail Check fun (R : Q12PSM.type) => @l R : QPSMLaw12.type R (@t R). + +(*WORKAROUND*) +Definition missingProjection (R : Q12PSM.type) : QPSMLaw12.type R (@t R). +Proof. + apply (@QPSMLaw12.Pack _ _ (@l R)). + constructor. + apply (@l R : QPSMLaw1.type R (@t R)). + apply (@l R : QPSMLaw2.type R (@t R)). +Defined. + +Canonical missingProjection. + +Print Canonical Projections l. + +Check fun (R : Q12PSM.type) => @l R : QPSMLaw12.type R (@t R). + diff --git a/tests/MinimalWrapBugs/mwb.v b/tests/MinimalWrapBugs/mwb.v new file mode 100644 index 00000000..677cf263 --- /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..adf4ccde --- /dev/null +++ b/tests/MinimalWrapBugs/noglobref.v @@ -0,0 +1,9 @@ +From HB Require Import structures. + +HB.mixin Record isLaw T (l:T) (op : T) := { + opA : True; +}. + +HB.structure Definition Law T l := {op of isLaw T l op}. + +(*In the HB paper it is written that parameters (beside the first) are supposed to be mixin, is this the problem?*) \ No newline at end of file diff --git a/tests/MinimalWrapBugs/typeNotInfered.v b/tests/MinimalWrapBugs/typeNotInfered.v new file mode 100644 index 00000000..6f52358b --- /dev/null +++ b/tests/MinimalWrapBugs/typeNotInfered.v @@ -0,0 +1,62 @@ +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 From a0564ed3a87fa88c893d5fa3e91fb903b3e6bb65 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 May 2025 10:37:43 +0200 Subject: [PATCH 05/34] add wrap bugs to the test suite --- _CoqProject.test-suite | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite index 506a3242..fe9ed2dd 100644 --- a/_CoqProject.test-suite +++ b/_CoqProject.test-suite @@ -69,6 +69,16 @@ 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/canonicalByHand.v +tests/MinimalWrapBugs/mwb.v +tests/MinimalWrapBugs/noglobref.v +tests/MinimalWrapBugs/typeNotInfered.v + -R tests HB.tests -R examples HB.examples From a8e52b7007b2c16c510e5c5805a94518c3828646 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 May 2025 10:40:56 +0200 Subject: [PATCH 06/34] fix makefile --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 8f9d3f73..e6b6579d 100644 --- a/Makefile +++ b/Makefile @@ -170,6 +170,6 @@ 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) $@ From 96be31254633c607a6fd45aaeb2530584edb3df0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 May 2025 12:05:05 +0200 Subject: [PATCH 07/34] HB.about: print wrapped mixins nicely --- HB/about.elpi | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/HB/about.elpi b/HB/about.elpi index 0c2c2806..b0e3b944 100644 --- a/HB/about.elpi +++ b/HB/about.elpi @@ -72,6 +72,10 @@ bulletize L F (glue [brk 0 0 | PLB]) :- % Print shortest qualified identifier of the module containing a gref pred pp-module i:gref, o:coq.pp. +pp-module GR (str ID) :- wrapper-mixin GR Op WrappedMixin, !, + gref->modname_short WrappedMixin "." ID_W, + coq.gref->id Op ID_Op, + ID is ID_W ^ " " ^ ID_Op ^ " (* wrapped via " ^ {coq.gref->id GR} ^ " *)". pp-module GR (str ID) :- gref->modname_short GR "." ID. pred unif-hint? i:cs-instance. From e4990308737b7e87038be92533ba9928e5af3e9d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 May 2025 12:05:41 +0200 Subject: [PATCH 08/34] bugfix: gref->modname_short could have failed --- HB/common/utils.elpi | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/HB/common/utils.elpi b/HB/common/utils.elpi index 2aca7c13..4804bcb5 100644 --- a/HB/common/utils.elpi +++ b/HB/common/utils.elpi @@ -87,6 +87,7 @@ gref->modname-label GR NComp Sep ModName :- std.string.concat Sep {std.rev [{coq.gref->id GR}|L]} ModName. pred string->modpath i:string, o:modpath. +string->modpath "" _ :- !, fail. % bug is coq.locate-all if the string is empty string->modpath S MP :- std.filter {coq.locate-all S} (l\l = loc-modpath _) L, L = [loc-modpath MP]. @@ -96,7 +97,8 @@ gref->modname_short1 _ S [] S. gref->modname_short1 MP "" [X|L] L' :- gref->modname_short1 MP X L L'. gref->modname_short1 MP S _ S :- string->modpath S MP. gref->modname_short1 MP S [X|L] S' :- - gref->modname_short1 MP {std.string.concat "." [X,S]} L S'. + if (S = "") (P = X) (P is X ^ "." ^ S), + gref->modname_short1 MP P L S'. % Print shortest qualified identifier of the module containing a gref % Sep is used as separator @@ -105,7 +107,9 @@ gref->modname_short GR Sep IDS :- coq.gref->path GR Path, string->modpath {std.string.concat "." Path} MP, gref->modname_short1 MP "" {std.rev Path} ID, - rex.replace "[.]" Sep ID IDS. + rex.replace "[.]" Sep ID IDS, !. +gref->modname_short GR _ IDS :- coq.gref->id GR IDS. + pred avoid-name-collision i:string, o:string. avoid-name-collision S S1 :- From 150745c776cfdf59936781e8dfd56e4b403028be Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 May 2025 12:05:50 +0200 Subject: [PATCH 09/34] cleanup --- tests/MinimalWrapBugs/aboutAutowrap.v | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/tests/MinimalWrapBugs/aboutAutowrap.v b/tests/MinimalWrapBugs/aboutAutowrap.v index 7fb56660..652fb562 100644 --- a/tests/MinimalWrapBugs/aboutAutowrap.v +++ b/tests/MinimalWrapBugs/aboutAutowrap.v @@ -22,11 +22,7 @@ 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. -(* Anomaly "Uncaught exception Failure("split_dirpath")." - Please report at http://coq.inria.fr/bugs/. *) - -Print wrapper_xx_op'_mwb_isAssoc. \ No newline at end of file From 6534f144052bfe0b1ded4f1e0caf8ac180245d95 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 May 2025 14:24:13 +0200 Subject: [PATCH 10/34] nicer print of wrapper --- HB/about.elpi | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/HB/about.elpi b/HB/about.elpi index b0e3b944..bab0f8f1 100644 --- a/HB/about.elpi +++ b/HB/about.elpi @@ -75,7 +75,8 @@ pred pp-module i:gref, o:coq.pp. pp-module GR (str ID) :- wrapper-mixin GR Op WrappedMixin, !, gref->modname_short WrappedMixin "." ID_W, coq.gref->id Op ID_Op, - ID is ID_W ^ " " ^ ID_Op ^ " (* wrapped via " ^ {coq.gref->id GR} ^ " *)". + gref->modname_short GR "." ID_GR, + ID is ID_W ^ " " ^ ID_Op ^ " (* wrapped via " ^ ID_GR ^ " *)". pp-module GR (str ID) :- gref->modname_short GR "." ID. pred unif-hint? i:cs-instance. From 937677700bc95c51ab49a4ec5640dfffae9810b1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 May 2025 14:24:22 +0200 Subject: [PATCH 11/34] cleanup --- tests/MinimalWrapBugs/aboutAutowrap2.v | 4 ---- 1 file changed, 4 deletions(-) diff --git a/tests/MinimalWrapBugs/aboutAutowrap2.v b/tests/MinimalWrapBugs/aboutAutowrap2.v index 1495f928..3c6e87c7 100644 --- a/tests/MinimalWrapBugs/aboutAutowrap2.v +++ b/tests/MinimalWrapBugs/aboutAutowrap2.v @@ -27,7 +27,3 @@ 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. -(* Anomaly "Uncaught exception Failure("split_dirpath")." - Please report at http://coq.inria.fr/bugs/. *) - -Print wrapper_xx_op'_mwb_isAssoc. \ No newline at end of file From 4649651f7fcfcac11624d5e47d767131f784c47c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 May 2025 15:43:19 +0200 Subject: [PATCH 12/34] typo --- HB/builders.elpi | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/HB/builders.elpi b/HB/builders.elpi index 4c4ea543..0ad19350 100644 --- a/HB/builders.elpi +++ b/HB/builders.elpi @@ -28,7 +28,7 @@ begin CtxSkel :- std.do! [ } -% "end" is a keyword, be put it in the namespace by hand +% "end" is a keyword, we put it in the namespace by hand pred builders.end. builders.end :- std.do! [ current-mode (builder-from _ _ _ ModName), From 9a7e95f663af7b9d536dbce6fa2edafe654be03a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 May 2025 15:43:33 +0200 Subject: [PATCH 13/34] we found the bug, no fix --- HB/instance.elpi | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/HB/instance.elpi b/HB/instance.elpi index 2249e8d9..c7895c03 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -81,6 +81,10 @@ declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [ private.declare-canonical-instances-from-factory-and-local-builders Factory TheType TheFactory TheFactoryForBuilderSection FGR Clauses CFL CSL, + % NON SI PASSA DI QUI PERCHE: (lifter TheType) <> builder-from TheType + % nel ramo else però non si generano le clausole builder-decl, MA si + % fa il wrapping dei mixin, cosa che in questa branch non si fa + private.close-section-if-has-params TyWP SectionName, ]) % instance in regular section %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% From a33d16472ef93cb743c2a086c9db6ae58362c266 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 May 2025 15:43:47 +0200 Subject: [PATCH 14/34] cleanup --- HB/instance.elpi | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/HB/instance.elpi b/HB/instance.elpi index c7895c03..ca934ded 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -278,8 +278,6 @@ add-mixin T FGR MissingMixin MixinSrcCl BuilderDeclCl C :- std.do! [ 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)), std.assert-ok! (coq.typecheck Bo Ty) "declare-instances: mixin illtyped", safe-dest-app Ty (global MixinNameAlias) _, @@ -293,6 +291,9 @@ add-mixin T FGR MissingMixin MixinSrcCl BuilderDeclCl C :- std.do! [ (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), + + MixinSrcCl = mixin-src T MixinName (global (const C)), + BuilderDeclCl = builder-decl (builder N FGR MixinName (const C)), ]. From 3d78b9b92b18fa09acc58bc85202a373e072a3ec Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 May 2025 15:46:18 +0200 Subject: [PATCH 15/34] fix test: in order to autowrap, the subject must be the lifter --- tests/MinimalWrapBugs/buildersofwrap.v | 4 ++-- tests/MinimalWrapBugs/buildersofwrap2.v | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/MinimalWrapBugs/buildersofwrap.v b/tests/MinimalWrapBugs/buildersofwrap.v index 3cb221a2..8a864e48 100644 --- a/tests/MinimalWrapBugs/buildersofwrap.v +++ b/tests/MinimalWrapBugs/buildersofwrap.v @@ -39,7 +39,7 @@ HB.builders Context T of isQPointed T. HB.instance Definition _ := hasPoint.Build T y. -HB.instance Definition _ := Q.Build T y qy. +HB.instance Definition _ := Q.Build T x qy. HB.end. @@ -48,4 +48,4 @@ Fail HB.structure Definition QPointed' := {T of isQPointed T}. (* Structure buildersofwrap2_Pointed contains the same mixins as QPointed' *) (* Though, this keep working... *) -HB.structure Definition QPointed := {T of hasPoint T & Q__on__Pointed_x T }. +HB.structure Definition QPointed := {T of hasPoint T & Q__on__Pointed_x T }. \ No newline at end of file diff --git a/tests/MinimalWrapBugs/buildersofwrap2.v b/tests/MinimalWrapBugs/buildersofwrap2.v index eb483ac8..0ad1451b 100644 --- a/tests/MinimalWrapBugs/buildersofwrap2.v +++ b/tests/MinimalWrapBugs/buildersofwrap2.v @@ -37,7 +37,7 @@ HB.builders Context T of isQPointed T. HB.instance Definition _ := hasPoint.Build T y. -HB.instance Definition _ := Q.Build T y qy. +HB.instance Definition _ := Q.Build T x qy. HB.end. From e0b88c18829e58389e4fb11cdb87de7fc6a0288d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 May 2025 16:01:34 +0200 Subject: [PATCH 16/34] fix error message --- HB/common/synthesis.elpi | 1 + 1 file changed, 1 insertion(+) diff --git a/HB/common/synthesis.elpi b/HB/common/synthesis.elpi index 0a353faa..033a6755 100644 --- a/HB/common/synthesis.elpi +++ b/HB/common/synthesis.elpi @@ -181,6 +181,7 @@ infer-coercion-tgt (w-params.cons ID Ty F) CoeClass :- @pi-parameter ID Ty x\ infer-coercion-tgt (F x) CoeClass. infer-coercion-tgt (w-params.nil _ {{ Type }} _) sortclass. infer-coercion-tgt (w-params.nil _ {{ forall x, _ }} _) funclass. % do not use {{ _ -> _ }} since Funclass can be a dependent function! +infer-coercion-tgt (w-params.nil _ T _) (grefclass _) :- name T, coq.error "The type of the structure carrier cannot be a parameter". infer-coercion-tgt (w-params.nil _ T _) (grefclass GR) :- coq.term->gref T GR. pred w-args.check-key i:list term, i:term, i:list (w-args A), o:prop. From 0f6dba34fe333c11e6271d28c53ade851d0dd93a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 May 2025 16:01:59 +0200 Subject: [PATCH 17/34] fix test --- tests/MinimalWrapBugs/noglobref.v | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/tests/MinimalWrapBugs/noglobref.v b/tests/MinimalWrapBugs/noglobref.v index adf4ccde..ff07f008 100644 --- a/tests/MinimalWrapBugs/noglobref.v +++ b/tests/MinimalWrapBugs/noglobref.v @@ -4,6 +4,4 @@ HB.mixin Record isLaw T (l:T) (op : T) := { opA : True; }. -HB.structure Definition Law T l := {op of isLaw T l op}. - -(*In the HB paper it is written that parameters (beside the first) are supposed to be mixin, is this the problem?*) \ No newline at end of file +Fail HB.structure Definition Law T l := {op of isLaw T l op}. From fbceca1cf6e21a9011876b47095c118e1b8eb5b9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 14 May 2025 15:46:51 +0200 Subject: [PATCH 18/34] buildersofwrap works but need cleanup --- HB/instance.elpi | 51 +++++++++++++++----------- tests/MinimalWrapBugs/buildersofwrap.v | 22 +---------- 2 files changed, 31 insertions(+), 42 deletions(-) diff --git a/HB/instance.elpi b/HB/instance.elpi index ca934ded..a8887e5f 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -79,11 +79,11 @@ declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [ (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 Clauses CFL CSL, + Factory TheType TheFactory TheFactoryForBuilderSection FGR NM_CFL CSL, - % NON SI PASSA DI QUI PERCHE: (lifter TheType) <> builder-from TheType - % nel ramo else però non si generano le clausole builder-decl, MA si - % fa il wrapping dei mixin, cosa che in questa branch non si fa + 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))) Clauses, private.close-section-if-has-params TyWP SectionName, ]) @@ -92,22 +92,29 @@ declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [ % derive all mixins the factory provides private.declare-mixins-from-factory Factory TheType TheFactory ML TheMixins, + if (current-mode (builder-from _ _ FGR _), (get-option "wrapper" ff ; not(is-subject-lifter TheType _ _))) + (std.map2 ML TheMixins (MixinName\C\c\sigma N\ new_int N, c = builder-decl (builder N FGR MixinName (const C))) BdClauses) + (BdClauses = []), % regular instance %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% if (get-option "wrapper" ff ; not(is-subject-lifter TheType _ _)) % regular subject %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - (private.declare-regular-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL, CFL = CSL) + (private.declare-regular-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL, WM = [], WMC = [], CFL = CSL) % wrapper %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - (private.declare-wrapper-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL, CFL = CSL) + (private.declare-wrapper-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL WM WMC, CFL = CSL) , + if (current-mode (builder-from _ _ FGR _)) + (std.map2 WM WMC (MixinName\C\c\sigma N\ new_int N, c = builder-decl (builder N FGR MixinName (const C))) WBdClauses) + (WBdClauses = []), + % shared to all branches if (get-option "export" tt) (coq.env.current-library File, std.map CSL (c\r\ r = instance-to-export File c) ClausesExp) (ClausesExp = []), - std.append ClausesHas ClausesExp Clauses, + std.flatten [ClausesHas, ClausesExp, BdClauses, WBdClauses] Clauses, ]), % we accumulate clauses now that the section is over @@ -252,14 +259,15 @@ shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod } pred declare-instance i:factoryname, i:term, i:term, o:list prop, o:list constant, o:list constant. -declare-instance Factory T F Clauses CFL CSL :- +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, if (get-option "export" tt) @@ -273,9 +281,9 @@ declare-instance Factory T F Clauses CFL CSL :- % [add-mixin T F M Cl] adds a constant being the mixin instance for M on type % T built from factory F pred add-mixin i:term, i:factoryname, i:mixinname, - o:prop, o:prop, o:constant. -add-mixin T FGR MissingMixin MixinSrcCl BuilderDeclCl C :- std.do! [ - new_int N, % timestamp + o:prop, o:constant. +add-mixin T FGR MissingMixin MixinSrcCl C :- std.do! [ + % new_int N, % timestamp synthesis.assert!-infer-mixin T MissingMixin Bo, @@ -293,15 +301,15 @@ add-mixin T FGR MissingMixin MixinSrcCl BuilderDeclCl C :- std.do! [ log.coq.env.add-const-noimplicits Name Bo Ty @transparent! C), MixinSrcCl = mixin-src T MixinName (global (const C)), - BuilderDeclCl = builder-decl (builder N FGR MixinName (const C)), + % BuilderDeclCl = builder-decl (builder N FGR MixinName (const C)), ]. pred add-all-mixins i:term, i:factoryname, i:list mixinname, o:list prop, o:list constant. add-all-mixins _T _FGR [] [] []. -add-all-mixins T FGR [M|ML] [MixinSrcCL,BuilderDeclCL | CL] [C|CC] :- std.do! [ - add-mixin T FGR M MixinSrcCL BuilderDeclCL C, +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, ]. @@ -328,14 +336,15 @@ postulate-arity (arity Ty) ArgsRev X T Ty :- % can access their theory and notations pred declare-canonical-instances-from-factory-and-local-builders i:factoryname, i:term, i:term, i:term, i:factoryname, - o:list prop, o:list constant, o:list constant. + o:list (pair mixinname constant), o: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 CSL :- std.do! [ synthesis.under-new-mixin-src-from-factory.do! T F (NewMixins\ std.do! [ - add-all-mixins T FGR NewMixins 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, ]. pred make-mixin-canonical i:constant, o:option constant. @@ -422,8 +431,8 @@ declare-regular-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL :- std ]. pred declare-wrapper-inst i:term, i:list mixinname, i:list constant, i:arity, i:id, - o:list prop, o:list constant. -declare-wrapper-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL :- std.do![ + 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.do![ 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, diff --git a/tests/MinimalWrapBugs/buildersofwrap.v b/tests/MinimalWrapBugs/buildersofwrap.v index 8a864e48..9f840e1d 100644 --- a/tests/MinimalWrapBugs/buildersofwrap.v +++ b/tests/MinimalWrapBugs/buildersofwrap.v @@ -19,21 +19,6 @@ 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. - (* As expected, any one of the two following work*) - HB.structure Definition QPointed := {T of hasPoint T & Q__on__Pointed_x T }. - HB.structure Definition QPointed' := {T of isQPointed T}. *) HB.builders Context T of isQPointed T. @@ -43,9 +28,4 @@ HB.instance Definition _ := Q.Build T x qy. HB.end. -HB.status. (* BUG: The builder targetting Q__on__Pointed_x is missing *) -Fail HB.structure Definition QPointed' := {T of isQPointed T}. -(* Structure buildersofwrap2_Pointed contains the same mixins as QPointed' *) - -(* Though, this keep working... *) -HB.structure Definition QPointed := {T of hasPoint T & Q__on__Pointed_x T }. \ No newline at end of file +HB.structure Definition QPointed' := {T of isQPointed T}. From 0c7fc4520af6fa20679655d66cf427a0eebfd33b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 14 May 2025 15:50:51 +0200 Subject: [PATCH 19/34] cleanup --- HB/instance.elpi | 21 +++++++++------------ 1 file changed, 9 insertions(+), 12 deletions(-) diff --git a/HB/instance.elpi b/HB/instance.elpi index a8887e5f..80c1581f 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -73,7 +73,7 @@ declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [ private.check-non-forgetful-inheritance TheType Factory, if (current-mode (builder-from TheType TheFactoryForBuilderSection FGR _)) - % instance in a builder section %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + % 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, @@ -92,29 +92,26 @@ declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [ % derive all mixins the factory provides private.declare-mixins-from-factory Factory TheType TheFactory ML TheMixins, - if (current-mode (builder-from _ _ FGR _), (get-option "wrapper" ff ; not(is-subject-lifter TheType _ _))) - (std.map2 ML TheMixins (MixinName\C\c\sigma N\ new_int N, c = builder-decl (builder N FGR MixinName (const C))) BdClauses) - (BdClauses = []), % regular instance %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% if (get-option "wrapper" ff ; not(is-subject-lifter TheType _ _)) % regular subject %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - (private.declare-regular-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL, WM = [], WMC = [], CFL = CSL) + (private.declare-regular-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL, WBdClauses = []) % wrapper %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - (private.declare-wrapper-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL WM WMC, CFL = CSL) + (private.declare-wrapper-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL WM WMC, + if (current-mode (builder-from _ _ FGR _)) % we are in a builder section + (std.map2 WM WMC (MixinName\C\c\sigma N\ new_int N, c = builder-decl (builder N FGR MixinName (const C))) WBdClauses) + (WBdClauses = [])) , - - if (current-mode (builder-from _ _ FGR _)) - (std.map2 WM WMC (MixinName\C\c\sigma N\ new_int N, c = builder-decl (builder N FGR MixinName (const C))) WBdClauses) - (WBdClauses = []), - + CFL = CSL, + % shared to all branches if (get-option "export" tt) (coq.env.current-library File, std.map CSL (c\r\ r = instance-to-export File c) ClausesExp) (ClausesExp = []), - std.flatten [ClausesHas, ClausesExp, BdClauses, WBdClauses] Clauses, + std.flatten [ClausesHas, ClausesExp, WBdClauses] Clauses, ]), % we accumulate clauses now that the section is over From cf9340c9d011d0643bf6c636926b700cb9b52097 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 14 May 2025 16:15:43 +0200 Subject: [PATCH 20/34] blind fix --- HB/instance.elpi | 27 ++++++++++++++++----------- 1 file changed, 16 insertions(+), 11 deletions(-) diff --git a/HB/instance.elpi b/HB/instance.elpi index 80c1581f..6f29e9ad 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -79,11 +79,13 @@ declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [ (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 CSL, + 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))) Clauses, + 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, ]) @@ -96,12 +98,15 @@ declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [ % regular instance %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% if (get-option "wrapper" ff ; not(is-subject-lifter TheType _ _)) % regular subject %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - (private.declare-regular-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL, WBdClauses = []) + (private.declare-regular-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL, WMsClauses = [], WBdClauses = []) % wrapper %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% (private.declare-wrapper-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL WM WMC, - if (current-mode (builder-from _ _ FGR _)) % we are in a builder section - (std.map2 WM WMC (MixinName\C\c\sigma N\ new_int N, c = builder-decl (builder N FGR MixinName (const C))) WBdClauses) - (WBdClauses = [])) + if (current-mode (builder-from TheLiftedType _ FGR _)) % we are in a builder section + ( + 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, @@ -111,8 +116,8 @@ declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [ std.map CSL (c\r\ r = instance-to-export File c) ClausesExp) (ClausesExp = []), - std.flatten [ClausesHas, ClausesExp, WBdClauses] Clauses, - ]), + std.flatten [ClausesHas, ClausesExp, WMsClauses, WBdClauses] Clauses, + ]), % we accumulate clauses now that the section is over acc-clauses current Clauses @@ -263,7 +268,7 @@ declare-instance Factory T F [] CFL CSL :- 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 NM_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, @@ -333,9 +338,9 @@ postulate-arity (arity Ty) ArgsRev X T Ty :- % can access their theory and notations pred declare-canonical-instances-from-factory-and-local-builders i:factoryname, i:term, i:term, i:term, i:factoryname, - o:list (pair mixinname constant), o:list constant. + o:list (pair mixinname constant), o:list prop, o:list constant. declare-canonical-instances-from-factory-and-local-builders - Factory T F _TheFactory FGR NM_CFL CSL :- std.do! [ + Factory T F _TheFactory FGR NM_CFL MsClauses CSL :- std.do! [ synthesis.under-new-mixin-src-from-factory.do! T F (NewMixins\ std.do! [ add-all-mixins T FGR NewMixins MsClauses CFL, std.zip NewMixins CFL NM_CFL, From f507de002980d4cff439a68f71bd96732ba71703 Mon Sep 17 00:00:00 2001 From: Calosci Matteo Date: Thu, 15 May 2025 11:05:26 +0200 Subject: [PATCH 21/34] IMproved test --- tests/MinimalWrapBugs/canonicalByHand.v | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/tests/MinimalWrapBugs/canonicalByHand.v b/tests/MinimalWrapBugs/canonicalByHand.v index 59311f4f..096d91c0 100644 --- a/tests/MinimalWrapBugs/canonicalByHand.v +++ b/tests/MinimalWrapBugs/canonicalByHand.v @@ -57,10 +57,14 @@ HB.builders Context T of isQ12PSM T. HB.instance Definition _ := hasPoint.Build T point. HB.instance Definition _ := hasSelfMap.Build T selfmap. -HB.instance Definition temp1 := Q1.Build T point selfmap q1term. -HB.instance Definition _ := Q1__on__PointedSelfMapped_t.Build T temp1. -HB.instance Definition temp2 := Q2.Build T point selfmap q2term. -HB.instance Definition _ := Q2__on__PointedSelfMapped_t.Build T temp2. +HB.instance Definition temp1 := Q1.Build T t l q1term. +(* HB.instance Definition _ := Q1__on__PointedSelfMapped_t.Build T temp1. *) +HB.instance Definition temp2 := Q2.Build T t l q2term. +(* HB.instance Definition _ := Q2__on__PointedSelfMapped_t.Build T temp2. *) + +Check l : QPSMLaw1.type T (@t T). +Check l : QPSMLaw2.type T (@t T). +Fail Check l : QPSMLaw12.type T (@t T). HB.end. @@ -69,6 +73,10 @@ HB.status. HB.about Q12PSM. Print Canonical Projections l. + +Section test. + +End test. Check fun (R : Q12PSM.type) => @l R : QPSMLaw1.type R (@t R). Check fun (R : Q12PSM.type) => @l R : QPSMLaw2.type R (@t R). From 671d4f747141c2ee2bb5409f38bca20f18dde6a5 Mon Sep 17 00:00:00 2001 From: Calosci Matteo Date: Thu, 15 May 2025 11:09:16 +0200 Subject: [PATCH 22/34] Improved test --- tests/MinimalWrapBugs/canonicalByHand.v | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/tests/MinimalWrapBugs/canonicalByHand.v b/tests/MinimalWrapBugs/canonicalByHand.v index 096d91c0..6348dcda 100644 --- a/tests/MinimalWrapBugs/canonicalByHand.v +++ b/tests/MinimalWrapBugs/canonicalByHand.v @@ -57,14 +57,12 @@ HB.builders Context T of isQ12PSM T. HB.instance Definition _ := hasPoint.Build T point. HB.instance Definition _ := hasSelfMap.Build T selfmap. -HB.instance Definition temp1 := Q1.Build T t l q1term. -(* HB.instance Definition _ := Q1__on__PointedSelfMapped_t.Build T temp1. *) -HB.instance Definition temp2 := Q2.Build T t l q2term. -(* HB.instance Definition _ := Q2__on__PointedSelfMapped_t.Build T temp2. *) +HB.instance Definition _ := Q1.Build T t l q1term. +HB.instance Definition _ := Q2.Build T t l q2term. Check l : QPSMLaw1.type T (@t T). Check l : QPSMLaw2.type T (@t T). -Fail Check l : QPSMLaw12.type T (@t T). +Fail Check l : QPSMLaw12.type T (@t T). (*BUG: this should be inferred automatically*) HB.end. @@ -74,9 +72,6 @@ HB.about Q12PSM. Print Canonical Projections l. -Section test. - -End test. Check fun (R : Q12PSM.type) => @l R : QPSMLaw1.type R (@t R). Check fun (R : Q12PSM.type) => @l R : QPSMLaw2.type R (@t R). From 64966fd10a16b80b42b1155892a0687eb4468160 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 16 May 2025 13:42:12 +0200 Subject: [PATCH 23/34] HB.saturete: let the user specify how much to saturate the key --- HB/common/utils.elpi | 6 +- HB/instance.elpi | 28 +++---- HB/structure.elpi | 6 +- HB/structures.v | 8 +- tests/MinimalWrapBugs/canonicalByHand.v | 99 ++++++++++--------------- tests/unit/close_hole_term.v | 2 +- tests/unit/enrich_type.v | 8 +- 7 files changed, 71 insertions(+), 86 deletions(-) diff --git a/HB/common/utils.elpi b/HB/common/utils.elpi index 4804bcb5..5b6e6d0a 100644 --- a/HB/common/utils.elpi +++ b/HB/common/utils.elpi @@ -341,11 +341,13 @@ prod-last-gref (prod N S X) GR :- !, @pi-decl N S x\ prod-last-gref (X x) GR. prod-last-gref X GR :- coq.term->gref X GR. % saturate a type constructor with holes -pred saturate-type-constructor i:term, o:term . -saturate-type-constructor T ET :- +pred saturate-type-constructor i:int, i:term, o:term . +saturate-type-constructor 0 T ET :- !, coq.typecheck T TH ok, coq.count-prods TH N, coq.mk-app T {coq.mk-n-holes N} ET. +saturate-type-constructor N T ET :- + coq.mk-app T {coq.mk-n-holes N} ET. pred with-unsafe-univ i:prop. diff --git a/HB/instance.elpi b/HB/instance.elpi index 6f29e9ad..cdd749bd 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -154,15 +154,15 @@ 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 -pred declare-all-on-type-constructor i:term, i:list class, o:list 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] [CS|L] :- +pred declare-all-on-type-constructor i:int, i:term, i:list class, o: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, + saturate-type-constructor Nargs TK T, infer-class T Class Struct MLwP S Name _STy Clauses, @@ -173,12 +173,12 @@ declare-all-on-type-constructor TK [class Class Struct MLwP|Rest] [CS|L] :- decl-const-in-struct Name SC SCTy CS, - Clauses => declare-all-on-type-constructor TK Rest L. + Clauses => declare-all-on-type-constructor Nargs TK Rest L. -declare-all-on-type-constructor TK [class HasNoInstance _ _|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. pred has-instance i:term, i:structure. has-instance T Struct :- @@ -228,8 +228,8 @@ decl-const-in-struct Name S STy CS:- std.do![ ]. % create instances for all possible combinations of types and structure compatible -pred saturate-instances i:cs-pattern. -saturate-instances Filter :- std.do! [ +pred saturate-instances i:int, i:cs-pattern. +saturate-instances Nargs Filter :- std.do! [ findall-has-mixin-instance Filter ClausesHas, @@ -240,10 +240,10 @@ saturate-instances Filter :- std.do! [ findall-classes AllClasses, std.map ClausesHas has-mixin-instance->mixin-src Clauses, - - Clauses => std.forall2 TL UKL (t\k\sigma Classes\ + Clauses => std.forall2 TL UKL (t\k\sigma Classes\ std.do! [ std.filter AllClasses (no-instance-for k) Classes, - declare-all-on-type-constructor t Classes _), + declare-all-on-type-constructor Nargs t Classes _, + ]), ]. pred no-instance-for i:cs-pattern, i:class. diff --git a/HB/structure.elpi b/HB/structure.elpi index c8701e17..0597c2f0 100644 --- a/HB/structure.elpi +++ b/HB/structure.elpi @@ -646,7 +646,7 @@ 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.spy-do! [ +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, @@ -758,7 +758,7 @@ declare-wrapper F C0 C :- C0 => std.do! [ %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'), std.spy(expand-structures RSkel' WrappedDeps W'), + ((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', @@ -835,7 +835,7 @@ wrapper-deps.aux (parameter ID explicit T F1) X [triple M Params 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.spy-do! [ +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, diff --git a/HB/structures.v b/HB/structures.v index 7de0d0c7..c04bf04b 100644 --- a/HB/structures.v +++ b/HB/structures.v @@ -783,10 +783,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 (instance.saturate-instances 0 _)). +main [str "Type"] :- !, with-attributes (with-logging (instance.saturate-instances 0 (cs-sort _))). +main [str K] :- !, coq.locate K GR, with-attributes (with-logging (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 (instance.saturate-instances N P)). main _ :- coq.error "Usage: HB.saturate [key]". }}. Elpi Typecheck. diff --git a/tests/MinimalWrapBugs/canonicalByHand.v b/tests/MinimalWrapBugs/canonicalByHand.v index 6348dcda..622ef767 100644 --- a/tests/MinimalWrapBugs/canonicalByHand.v +++ b/tests/MinimalWrapBugs/canonicalByHand.v @@ -1,95 +1,78 @@ From HB Require Import structures. -HB.mixin Record Q1 T (t:T) (l : T -> T) := { - q : True; +HB.mixin Record IdLaw T (t:T) (l : T -> T) := { + is_id : l t = t; }. -HB.structure Definition QPSMLaw1 T (t:T) := {l of Q1 T t l}. +HB.structure Definition IdMap T (t:T) := {l of IdLaw T t l}. -HB.mixin Record Q2 T (t:T) (l : T -> T) := { - q : True; +HB.mixin Record IdempotentLaw T (t:T) (l : T -> T) := { + is_sinv : l (l t) = l t; }. -HB.structure Definition QPSMLaw2 T (t:T) := {l of Q2 T t l}. +HB.structure Definition IdempotentMap T (t:T) := {l of IdempotentLaw T t l}. -HB.structure Definition QPSMLaw12 T (t:T) := {l of QPSMLaw1 T t l & QPSMLaw2 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 := { - t : T + point : T }. HB.structure Definition Pointed := {T of hasPoint T}. HB.mixin Record hasSelfMap T := { - l : T -> 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 Q1__on__PointedSelfMapped_t T of PointedSelfMapped T := { - private : Q1 T t l +HB.mixin Record IdLaw__on__PointedSelfMapped_t T of PointedSelfMapped T := { + private : IdLaw T point selfmap }. -HB.structure Definition Q1PSM -:= {T of PointedSelfMapped T & Q1__on__PointedSelfMapped_t T}. +HB.structure Definition IdPSM +:= {T of PointedSelfMapped T & IdLaw__on__PointedSelfMapped_t T}. #[wrapper] -HB.mixin Record Q2__on__PointedSelfMapped_t T of PointedSelfMapped T := { - private : Q2 T t l +HB.mixin Record IdempotentLaw__on__PointedSelfMapped_t T of PointedSelfMapped T := { + private : IdempotentLaw T point selfmap }. -HB.structure Definition Q2PSM -:= {T of PointedSelfMapped T & Q2__on__PointedSelfMapped_t T}. - -HB.structure Definition Q12PSM - := {T of PointedSelfMapped T & Q1PSM T & Q2PSM T}. - -HB.factory Record isQ12PSM T := { - point : T; - selfmap : T -> T; - q1term : True; - q2term : True +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 isQ12PSM T. +HB.builders Context T of BuggyFactory T. -HB.instance Definition _ := hasPoint.Build T point. -HB.instance Definition _ := hasSelfMap.Build T selfmap. +HB.instance Definition _ := hasPoint.Build T p. +HB.instance Definition _ := hasSelfMap.Build T s. -HB.instance Definition _ := Q1.Build T t l q1term. -HB.instance Definition _ := Q2.Build T t l q2term. +HB.instance Definition _ := IdLaw.Build T point selfmap sid. +#[verbose] HB.instance Definition _ := IdempotentLaw.Build T point selfmap sinv. -Check l : QPSMLaw1.type T (@t T). -Check l : QPSMLaw2.type T (@t T). -Fail Check l : QPSMLaw12.type T (@t T). (*BUG: this should be inferred automatically*) +Check selfmap : IdMap.type T point. +Check selfmap : IdempotentMap.type T point. +Check selfmap : FooMap.type T point. HB.end. HB.status. -HB.about Q12PSM. - -Print Canonical Projections l. - -Check fun (R : Q12PSM.type) => @l R : QPSMLaw1.type R (@t R). -Check fun (R : Q12PSM.type) => @l R : QPSMLaw2.type R (@t R). - -(*BUG: this should be inferred automatically*) -Fail Check fun (R : Q12PSM.type) => @l R : QPSMLaw12.type R (@t R). - -(*WORKAROUND*) -Definition missingProjection (R : Q12PSM.type) : QPSMLaw12.type R (@t R). -Proof. - apply (@QPSMLaw12.Pack _ _ (@l R)). - constructor. - apply (@l R : QPSMLaw1.type R (@t R)). - apply (@l R : QPSMLaw2.type R (@t R)). -Defined. - -Canonical missingProjection. - -Print Canonical Projections l. - -Check fun (R : Q12PSM.type) => @l R : QPSMLaw12.type R (@t R). +Check fun (R : FooPSM.type) => @selfmap R : FooMap.type R (@point R). 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" }}. From 98a75ce47e2a5345ef8858f26cd220f6a1f99016 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 18 May 2025 13:02:18 +0200 Subject: [PATCH 24/34] wrapping: use the phant abbreviation for building "Foo.Build T extra" is like "Foo.Axioms T _ extra" but before typing "extra" it ensures/infers that T has the needed structue, eg "Foo.Axioms T T__hasThis extra" In turn this can make the typing of "extra" simpler since the _ could occur in the expected type of "extra". --- HB/instance.elpi | 39 +++++++++----------------- tests/MinimalWrapBugs/typeNotInfered.v | 3 +- 2 files changed, 16 insertions(+), 26 deletions(-) diff --git a/HB/instance.elpi b/HB/instance.elpi index cdd749bd..4d6922bc 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -447,38 +447,27 @@ derive-wrapper-instances Instance WrapperMixin WrapperSubject C :- std.do! [ % K is the mixin constructor (Build) for WrapperMixin factory-constructor WrapperMixin K, - factory-nparams WrapperMixin NParams, - - % We are only interested in the last parameter of the constructor - % type, which is the current instance - % (which is a Mixin instance on the new Subject). - % In monoid_enriched_cat.v, we are targeting the code - % - % HB.instance Definition funQ_hom_isMon := - % hom_isMon.Axioms_ _ _ funQ_isMon. - % which Coq can compute to stand for - % hom_isMon.Axioms_ Type funQ funQ_isMon. - % - % We compute the number of the underscores and we pass - % them as arguments followed by Instance. - coq.env.typeof K KTy, + + % 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, + std.assert-ok! (coq.typecheck AbbBo KTy) "canno type wrap constructor", + + % the arguments coq.count-prods KTy KN, KN0 is KN - 1, - coq.mk-n-holes KN0 Holes, - - std.append Holes [Instance] Args, - - % the body of the new wrapper instance - NewInstance = app[global K| Args], + std.append {coq.mk-n-holes KN0} [Instance] Args, + coq.mk-app AbbBo Args NewInstance, std.assert-ok! (coq.typecheck NewInstance Ty) "cannot wrap", + 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 WrapperSubject, - - Name is "wrapped__" ^ {std.any->string {new_int}}, - - log.coq.env.add-const-noimplicits Name NewInstance Ty @transparent! C, ]. pred wrap-a-mixin i:gref, i:mixinname, i:constant, o:term, o:mixinname, o:constant. diff --git a/tests/MinimalWrapBugs/typeNotInfered.v b/tests/MinimalWrapBugs/typeNotInfered.v index 6f52358b..10b31a07 100644 --- a/tests/MinimalWrapBugs/typeNotInfered.v +++ b/tests/MinimalWrapBugs/typeNotInfered.v @@ -54,9 +54,10 @@ HB.instance Definition _ := hasRight.Build T r. 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.instance Definition _ := Q__on__Ambidextrous_dx.Build T temp. *) HB.end. \ No newline at end of file From fbd362d1249b878c818db4addb3344bd9a7870f4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 19 May 2025 22:58:02 +0200 Subject: [PATCH 25/34] this limit makes MC compile --- HB/structures.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/HB/structures.v b/HB/structures.v index c04bf04b..df46bfaa 100644 --- a/HB/structures.v +++ b/HB/structures.v @@ -728,7 +728,7 @@ actions N :- coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File O)), % hack - std.forall {std.iota 20} (x\begin-section "x",end-section), + std.forall {std.iota 30} (x\begin-section "x",end-section), if (get-option "mathcomp" tt ; get-option "mathcomp.axiom" _) (actions-compat N) true. From cb1a6ec68e14cb325c7116da4995451fb929fbec Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 19 May 2025 23:00:57 +0200 Subject: [PATCH 26/34] wrap: wrapped subject is inferred [needs discussion] When we build the wrapped we infer the subject. If the subject has deps, it is inferred as the sort projection of its canon instance satisfying all deps. For now I do a whd, but one should probably be less aggressive. This needs discussion since subject are GIVEN not inferred, usually. --- HB/instance.elpi | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/HB/instance.elpi b/HB/instance.elpi index 4d6922bc..2c9f4eb6 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -452,11 +452,13 @@ derive-wrapper-instances Instance WrapperMixin WrapperSubject C :- std.do! [ phant-abbrev K _ Abb, coq.notation.abbreviation-body Abb NArgs _, coq.notation.abbreviation Abb {coq.mk-n-holes NArgs} AbbBo, - std.assert-ok! (coq.typecheck AbbBo KTy) "canno type wrap constructor", + + 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, + KN0 is KN - 1 - {std.length ActualArgs}, std.append {coq.mk-n-holes KN0} [Instance] Args, coq.mk-app AbbBo Args NewInstance, @@ -467,7 +469,14 @@ derive-wrapper-instances Instance WrapperMixin WrapperSubject C :- std.do! [ coq.safe-dest-app Ty _Factory FArgs, factory-nparams WrapperMixin NParams, - std.nth NParams FArgs WrapperSubject, + std.nth NParams FArgs WrapperSubjectAsInferred, + + % we may have inferred as the subject the sort projection of an instance + + if (coq.safe-dest-app WrapperSubjectAsInferred (global (const P)) [_],structure-key P _ _) + (unwind {whd WrapperSubjectAsInferred []} WrapperSubject) % TODO: do 1 step + (WrapperSubject = WrapperSubjectAsInferred) + ]. pred wrap-a-mixin i:gref, i:mixinname, i:constant, o:term, o:mixinname, o:constant. From 3c45eaefa412c79665845a43cb062a85220dd658 Mon Sep 17 00:00:00 2001 From: Calosci Matteo Date: Wed, 21 May 2025 16:25:13 +0200 Subject: [PATCH 27/34] Added tests --- tests/MinimalWrapBugs/structVS2mixin.v | 41 +++++++++++++++++++ tests/MinimalWrapBugs/structVS2mixinCorrect.v | 39 ++++++++++++++++++ 2 files changed, 80 insertions(+) create mode 100644 tests/MinimalWrapBugs/structVS2mixin.v create mode 100644 tests/MinimalWrapBugs/structVS2mixinCorrect.v 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 From 3d72ea74b065ca857bba52e8ded5fb5f53e686d2 Mon Sep 17 00:00:00 2001 From: Calosci Matteo Date: Fri, 23 May 2025 10:08:30 +0200 Subject: [PATCH 28/34] Added test exposing bug --- tests/MinimalWrapBugs/unwrappedSubject.v | 40 ++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 tests/MinimalWrapBugs/unwrappedSubject.v diff --git a/tests/MinimalWrapBugs/unwrappedSubject.v b/tests/MinimalWrapBugs/unwrappedSubject.v new file mode 100644 index 00000000..f0a2d5ff --- /dev/null +++ b/tests/MinimalWrapBugs/unwrappedSubject.v @@ -0,0 +1,40 @@ +(*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*) +Fail HB.instance Definition _ := hasLaw.Build nat (@selfmap nat) tt. + +Check @law nat _. From 81804fd4872294ace3ea1c73e84c7c7e4f319fc9 Mon Sep 17 00:00:00 2001 From: Calosci Matteo Date: Fri, 23 May 2025 15:09:20 +0200 Subject: [PATCH 29/34] Added test for factory.Build fails --- tests/MinimalWrapBugs/buggyFactories.v | 63 ++++++++++++++++++++++++++ 1 file changed, 63 insertions(+) create mode 100644 tests/MinimalWrapBugs/buggyFactories.v diff --git a/tests/MinimalWrapBugs/buggyFactories.v b/tests/MinimalWrapBugs/buggyFactories.v new file mode 100644 index 00000000..859feba0 --- /dev/null +++ b/tests/MinimalWrapBugs/buggyFactories.v @@ -0,0 +1,63 @@ +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 _ := isB.Build V point b. + +HB.end. + +HB.instance Definition _ := hasPoint.Build nat 0. +HB.instance Definition _ := isA.Build nat point tt. + +#[verbose] +HB.instance Definition _ := PointedA_isPointedAB.Build nat tt. \ No newline at end of file From 0d4f4896c9f20ffa2eb12d28307edd5f083d1e41 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 May 2025 08:58:12 +0200 Subject: [PATCH 30/34] apply builder without synthesizing the deps apparently something is off is deps are mixed between the subject and its lifted variants --- HB/common/synthesis.elpi | 36 +++++++++++++++++++------- _CoqProject.test-suite | 1 + tests/MinimalWrapBugs/buggyFactories.v | 20 +++++++++++--- tests/hnf.v | 4 +-- 4 files changed, 46 insertions(+), 15 deletions(-) diff --git a/HB/common/synthesis.elpi b/HB/common/synthesis.elpi index 033a6755..08ef5905 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, ]. @@ -203,16 +204,24 @@ namespace private { % the databases [mixin-src] and [from] pred mixin-for i:term, i:mixinname, o:term. mixin-for T M MICompressed :- mixin-src T M Tm, !, std.do! [ - %if-verbose (coq.say {header} "Trying to infer mixin for" M), + if-verbose (coq.say {header} "Inferring mixin" M "on" T), std.assert-ok! (coq.typecheck Tm Ty) "mixin-for: Tm illtyped", %%%%% mterm %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - factory? Ty (triple Factory Params _), + factory? Ty (triple Factory Params Subj), - if (M = Factory) (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 + ) + ( + 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 + % 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}), @@ -250,13 +259,20 @@ mixin-for_mixin-builder (mixin-for _ _ B) B. % [builder->term Params TheType Src Tgt MF] finds a builder from Src to Tgt % and fills in all the mixins required by the builder using mixin-src, obtaining % a function (MF = Builder Params TheType InferredStuff : Src -> Tgt) -pred builder->term i:list term, i:term, i:factoryname, i:mixinname, o:term. -builder->term Ps T Src Tgt B :- !, std.do! [ +pred builder->term i:list term, i:term, i:factoryname, i:term, i:mixinname, o:term. +% pred builder->term i:list term, i:term, i:factoryname, i:mixinname, o:term. +builder->term Ps T Src HasSrc Tgt B :- !, std.do! [ from Src Tgt FGR, F = global FGR, gref-deps Src MLwP, list-w-params_list MLwP ML, - infer-all-these-mixin-args Ps T ML F B, + if-verbose (coq.say {header} "Found builder" FGR "from" Src "to" Tgt), + if-verbose (coq.say {header} "Found builder" FGR "depends on" ML), + % infer-all-these-mixin-args Ps T ML F B, + coq.mk-n-holes {std.length ML} Holes, + coq.mk-app F {std.flatten [Ps,[T],Holes,[HasSrc]]} B, + std.assert-ok! (coq.typecheck B _) "builder illtyped", + ]. % [instantiate-all-these-mixin-args T F M_i TFX] where mixin-for T M_i X_i states that @@ -269,9 +285,11 @@ pred instantiate-all-these-mixin-args i:term, i:term, i:list mixinname, o:term. instantiate-all-these-mixin-args (fun _ Tm F) T ML R :- coq.safe-dest-app Tm (global TmGR) _, factory-alias->gref TmGR M ok, + if-verbose (coq.say {header} "Looking at argument" M), std.mem! ML M, - factory? Tm (triple _ _ Subj), Subj = T, % check the subject is T (do not pass T to factory?) + % factory? Tm (triple _ _ Subj), Subj = T, % check the subject is T (do not pass T to factory?) !, + if-verbose (coq.say {header} "We have to inhabit it on" T), if (mixin-for T M X) true (coq.error "HB: Unable to find mixin" {nice-gref->string M} "on subject" {coq.term->string T}), !, instantiate-all-these-mixin-args (F X) T ML R. instantiate-all-these-mixin-args (fun N Ty F) T ML (fun N Ty FX) :- !, diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite index fe9ed2dd..2003fc64 100644 --- a/_CoqProject.test-suite +++ b/_CoqProject.test-suite @@ -74,6 +74,7 @@ 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 diff --git a/tests/MinimalWrapBugs/buggyFactories.v b/tests/MinimalWrapBugs/buggyFactories.v index 859feba0..46d2e1d4 100644 --- a/tests/MinimalWrapBugs/buggyFactories.v +++ b/tests/MinimalWrapBugs/buggyFactories.v @@ -52,12 +52,24 @@ HB.factory Record PointedA_isPointedAB V of PointedA V := { HB.builders Context V of PointedA_isPointedAB V. -HB.instance Definition _ := isB.Build V point b. +HB.instance Definition foo := isB.Build V point b. HB.end. -HB.instance Definition _ := hasPoint.Build nat 0. -HB.instance Definition _ := isA.Build nat point tt. +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 _ := PointedA_isPointedAB.Build nat tt. \ No newline at end of file +HB.instance +Definition yy := PointedA_isPointedAB.Build nat tt. + +Check nat : PointedAB.type. \ No newline at end of file diff --git a/tests/hnf.v b/tests/hnf.v index a36d1e6f..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 hnf_f__to__hnf_M__11. +Print hnf_f__to__hnf_M__9. From 4d8daa595104fdb18da4043a70dedb06611f3ae2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 May 2025 09:13:47 +0200 Subject: [PATCH 31/34] mixed feelings --- HB/instance.elpi | 1 + _CoqProject.test-suite | 1 + tests/MinimalWrapBugs/unwrappedSubject.v | 3 ++- 3 files changed, 4 insertions(+), 1 deletion(-) diff --git a/HB/instance.elpi b/HB/instance.elpi index 2c9f4eb6..9df0a395 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -96,6 +96,7 @@ declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [ private.declare-mixins-from-factory Factory TheType TheFactory ML TheMixins, % regular instance %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + % TODO: we may do both here? if (get-option "wrapper" ff ; not(is-subject-lifter TheType _ _)) % regular subject %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% (private.declare-regular-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL, WMsClauses = [], WBdClauses = []) diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite index 2003fc64..335bc417 100644 --- a/_CoqProject.test-suite +++ b/_CoqProject.test-suite @@ -79,6 +79,7 @@ tests/MinimalWrapBugs/canonicalByHand.v tests/MinimalWrapBugs/mwb.v tests/MinimalWrapBugs/noglobref.v tests/MinimalWrapBugs/typeNotInfered.v +tests/MinimalWrapBugs/unwrappedSubject.v -R tests HB.tests -R examples HB.examples diff --git a/tests/MinimalWrapBugs/unwrappedSubject.v b/tests/MinimalWrapBugs/unwrappedSubject.v index f0a2d5ff..6bdc44e8 100644 --- a/tests/MinimalWrapBugs/unwrappedSubject.v +++ b/tests/MinimalWrapBugs/unwrappedSubject.v @@ -35,6 +35,7 @@ HB.mixin Record hasLaw T (x: T->T) := { HB.structure Definition Law T := {x of hasLaw T x}. (*BUG: this should work*) -Fail HB.instance Definition _ := hasLaw.Build nat (@selfmap nat) tt. +#[verbose,wrapper=off] HB.instance Definition _ := hasLaw.Build nat (@selfmap nat) tt. Check @law nat _. +Check @selfmap nat : Law.type nat. From 0803412fa3dce2a9f940c940500f48cf74c1cfa9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 May 2025 09:17:26 +0200 Subject: [PATCH 32/34] add test --- tests/wrap.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tests/wrap.v b/tests/wrap.v index 4914237e..54eb840b 100644 --- a/tests/wrap.v +++ b/tests/wrap.v @@ -21,4 +21,5 @@ HB.instance Definition _ : hasOp nat := hasOp.Build nat plus. (* HB.instance Definition _ : isAssoc nat plus := isAssoc.Build nat plus plus_ass. *) HB.instance Definition _ : isAssoc nat op := isAssoc.Build nat plus plus_ass. -Check nat : Monoid.type. \ No newline at end of file +Check nat : Monoid.type. +Check plus : Assop.type _. \ No newline at end of file From c7857f24eaa4149d9021955666b48eb4ef346c69 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 20 May 2025 08:21:25 +0200 Subject: [PATCH 33/34] surgical reduction of subject --- HB/instance.elpi | 54 ++++++++++++++++++++++++++++--------- HB/structures.v | 2 +- tests/MinimalWrapBugs/mwb.v | 2 +- tests/auto_wrap.v | 16 ++++++----- tests/wrap.v | 10 +++---- 5 files changed, 57 insertions(+), 27 deletions(-) diff --git a/HB/instance.elpi b/HB/instance.elpi index 9df0a395..a3fa5c2c 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -60,12 +60,15 @@ 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, + log.coq.env.add-const-noimplicits-failondup RealName OptimizedBody SectionTyUnfolded @transparent! C, TheFactory = (global (const C)), @@ -88,20 +91,22 @@ declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [ 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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - % TODO: we may do both here? - if (get-option "wrapper" ff ; not(is-subject-lifter TheType _ _)) + if (get-option "wrapper" ff ; not(is-subject-lifter TheTypeAsInferred _ _)) % regular subject %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - (private.declare-regular-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL, WMsClauses = [], WBdClauses = []) + ( if-verbose (coq.say {header} "Not a lifted subject" {coq.term->string TheTypeAsInferred}), + WMsClauses = [], WBdClauses = [], ClausesHas2 = [], CSL2 = []) % wrapper %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - (private.declare-wrapper-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL WM WMC, + (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 ( std.map2 WM WMC (MixinName\C\c\sigma N\ new_int N, c = builder-decl (builder N FGR MixinName (const C))) WBdClauses, @@ -109,15 +114,15 @@ declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [ ) (WMsClauses = [], WBdClauses = [])) , - CFL = CSL, + CFL = CSL, % ??? % shared to all branches if (get-option "export" tt) (coq.env.current-library File, - std.map CSL (c\r\ r = instance-to-export File c) ClausesExp) + std.map {std.append CSL CSL2} (c\r\ r = instance-to-export File c) ClausesExp) (ClausesExp = []), - std.flatten [ClausesHas, ClausesExp, WMsClauses, WBdClauses] Clauses, + std.flatten [ClausesHas, ClausesHas2, ClausesExp, WMsClauses, WBdClauses] Clauses, ]), % we accumulate clauses now that the section is over @@ -436,6 +441,7 @@ declare-regular-inst TheType ML TheMixins TyWP SectionName ClausesHas CSL :- std 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.do![ + 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, @@ -473,13 +479,35 @@ derive-wrapper-instances Instance WrapperMixin WrapperSubject C :- std.do! [ std.nth NParams FArgs WrapperSubjectAsInferred, % we may have inferred as the subject the sort projection of an instance - - if (coq.safe-dest-app WrapperSubjectAsInferred (global (const P)) [_],structure-key P _ _) - (unwind {whd WrapperSubjectAsInferred []} WrapperSubject) % TODO: do 1 step - (WrapperSubject = WrapperSubjectAsInferred) + expose-real-subject WrapperSubjectAsInferred WrapperSubject, ]. +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 :- + std.findall (decl-location (const _) _) LC, + std.map LC (x\r\sigma c\x = decl-location (const c) _, r = coq.redflags.const c) CL, + 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, + 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, + @redflags! F => coq.reduction.lazy.whd T TN, + coq.reduction.eta-contract TN TE, + 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 !!!! +pred hack-primproj i:term, o: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, diff --git a/HB/structures.v b/HB/structures.v index df46bfaa..6cb6c1a7 100644 --- a/HB/structures.v +++ b/HB/structures.v @@ -199,7 +199,7 @@ pred mixin-first-class o:mixinname, o:classname. % 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) diff --git a/tests/MinimalWrapBugs/mwb.v b/tests/MinimalWrapBugs/mwb.v index 677cf263..e8ebd23d 100644 --- a/tests/MinimalWrapBugs/mwb.v +++ b/tests/MinimalWrapBugs/mwb.v @@ -139,7 +139,7 @@ HB.instance Definition temp := isUnital.Build T one op' op1m'' opm1''. *) -HB.instance Definition _ := isMonoidLaw__on__BaseUMagma_MulOne.Build G pippo. +(* HB.instance Definition _ := isMonoidLaw__on__BaseUMagma_MulOne.Build G pippo. *) Check isUnital.phant_axioms T one' op'. Check isUnital.phant_axioms T one op'. diff --git a/tests/auto_wrap.v b/tests/auto_wrap.v index 018c9e8c..e07ba7cd 100644 --- a/tests/auto_wrap.v +++ b/tests/auto_wrap.v @@ -1,20 +1,22 @@ From HB Require Import structures. -HB.mixin Record isAssoc T (op : T -> T -> T) := { opA : forall x y z, op (op x y) z = op x (op y z) }. -HB.structure Definition Assop T := { op of isAssoc T op }. +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 }. *) -(* HB.structure Definition Monoid := { T of hasOp T & isAssoc _ (op : T -> _ -> _) }. *) -HB.structure Definition Monoid := { T of hasOp T & isAssoc _ (@op 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. -(* HB.instance Definition _ : isAssoc nat plus := isAssoc.Build nat plus plus_ass. *) +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. \ No newline at end of file +Check nat : Monoid.type. diff --git a/tests/wrap.v b/tests/wrap.v index 54eb840b..1e6298b8 100644 --- a/tests/wrap.v +++ b/tests/wrap.v @@ -1,7 +1,7 @@ From HB Require Import structures. -HB.mixin Record isAssoc T (op : T -> T -> T) := { opA : forall x y z, op (op x y) z = op x (op y z) }. -HB.structure Definition Assop T := { op of isAssoc T op }. +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 }. @@ -18,8 +18,8 @@ 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. -(* HB.instance Definition _ : isAssoc nat plus := isAssoc.Build nat plus plus_ass. *) -HB.instance Definition _ : isAssoc nat op := isAssoc.Build nat plus plus_ass. +Check nat : Magma.type. +HB.instance Definition _ : isAssoc nat op := isAssoc.Build nat plus plus_ass. Check nat : Monoid.type. -Check plus : Assop.type _. \ No newline at end of file +Check plus : AssociativeOperation.type nat. From bd8f5d130c492a28cd75d0fc8cf31279f6d2010e Mon Sep 17 00:00:00 2001 From: Calosci Matteo Date: Thu, 24 Jul 2025 17:12:47 +0200 Subject: [PATCH 34/34] Added test for 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 --- .../MinimalWrapBugs/factoryBuildingWrapper.v | 69 +++++++++++++++++++ 1 file changed, 69 insertions(+) create mode 100644 tests/MinimalWrapBugs/factoryBuildingWrapper.v 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