diff --git a/.nix/config.nix b/.nix/config.nix index bd392b3cb..e340153a2 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -1,7 +1,7 @@ { format = "1.0.0"; attribute = "hierarchy-builder"; - default-bundle = "coq-8.15"; + default-bundle = "coq-8.16"; bundles = let mcHBcommon = { mathcomp.override.version = "hierarchy-builder"; @@ -26,6 +26,9 @@ coq.override.version = "8.15"; } // mcHBcommon; + "coq-8.17".coqPackages = { + coq.override.version = "8.17"; + }; "coq-8.16".coqPackages = { coq.override.version = "8.16"; mathcomp.override.version = "mathcomp-1.15.0"; diff --git a/HB/common/utils.elpi b/HB/common/utils.elpi index 000826a2a..4b2a6816a 100644 --- a/HB/common/utils.elpi +++ b/HB/common/utils.elpi @@ -44,6 +44,7 @@ with-attributes P :- att "primitive" bool, att "non_forgetful_inheritance" bool, att "hnf" bool, + att "wrapper" bool, ] Opts, !, Opts => (save-docstring, P). diff --git a/HB/factory.elpi b/HB/factory.elpi index 2b599df10..31ce5cfa8 100644 --- a/HB/factory.elpi +++ b/HB/factory.elpi @@ -15,9 +15,13 @@ type by-phantabbrev abbreviation -> factory-abbrev. pred declare-abbrev i:id, i:factory-abbrev. declare-abbrev Name (by-classname GR) :- + + coq.say "DA!!!!!!&&& NOW RUNNING declare-abbrev", + % looks fishy (the parameters are not taken into account) @global! => log.coq.notation.add-abbreviation Name 1 (fun _ _ t\ app[global GR,t]) tt _. declare-abbrev Name (by-phantabbrev Abbr) :- std.do! [ + coq.say "DA!!!!!!&&& NOW RUNNING declare-abbrev", coq.notation.abbreviation-body Abbr Nargs AbbrTrm, @global! => log.coq.notation.add-abbreviation Name Nargs AbbrTrm tt _, ]. @@ -192,6 +196,7 @@ mk-factory-abbrev Str GR Aliases FactAbbrev :- !, std.do! [ pred declare-asset i:argument, i:asset. declare-asset Arg AssetKind :- std.do! [ argument-name Arg Module, + if-verbose (coq.say {header} "start module and section" Module), log.coq.env.begin-module Module none, log.coq.env.begin-section Module, @@ -218,11 +223,65 @@ declare-asset Arg AssetKind :- std.do! [ ) ]. +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%% auxiliary code for wrapper-mixin + +pred extract_from_record_decl i: (term -> gref -> prop), i:indt-decl, o:gref. +extract_from_record_decl P (parameter ID _ _ R) Out :- + pi p\ + extract_from_record_decl P (R p) Out. +extract_from_record_decl P (record ID _ KID (field _ _ Ty (x\end-record))) GR0 :- + P Ty GR0. + +pred extract_from_rtty i: (term -> gref -> prop), i: term, o:gref. +extract_from_rtty P (prod _ _ TF) Out1 :- + pi p\ + extract_from_rtty P (TF p) Out1. +extract_from_rtty P Ty Gr :- P Ty Gr. + +pred xtr_fst_op i:term, o:gref. +xtr_fst_op Ty Gr1 :- + Ty = (app [global Gr0| _]), + factory-alias->gref Gr0 Gr1. + +pred xtr_snd_op i:term, o:gref. +xtr_snd_op Ty Gr :- + Ty = (app [global _, app [global Gr| _]]). + +pred extract_wrapped i:indt-decl, o:gref. +extract_wrapped In Out :- + extract_from_record_decl (extract_from_rtty xtr_fst_op) In Out. + +pred extract_subject i:indt-decl, o:gref. +extract_subject In Out :- + extract_from_record_decl (extract_from_rtty xtr_snd_op) In Out. + +pred wrapper_mixin_aux i:gref, o:gref, o:gref. +wrapper_mixin_aux XX Gr1 Gr2 :- + XX = (indt I), + coq.env.indt-decl I D, + extract_subject D Gr1, + extract_wrapped D Gr2. + +%%% end auxiliary code for wrapper-mixin +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + pred declare-mixin-or-factory i:list prop, i:list constant, i:list term, i:term, i:term, i:record-decl, i:list-w-params factoryname, i:id, i:asset. declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance TheParams TheType Sort1 Fields GRFSwP Module D :- std.do! [ + coq.say "DMOF!!!!!!!!!!!!!!!!!!!! NOW RUNNING declare-mixin-or-factory", + coq.say "DMOF!!!!!!!! MixinSrcClauses" MixinSrcCaluses, + coq.say "DMOF!!!!!!!! SectionCanonicalInstance" SectionCanonicalInstance, + coq.say "DMOF!!!!!!!! TheParams" TheParams, + coq.say "DMOF!!!!!!!! TheType" TheType, + coq.say "DMOF!!!!!!!! Sort1" Sort1, + coq.say "DMOF!!!!!!!! Fields" Fields, + coq.say "DMOF!!!!!!!! GRFSwP" GRFSwP, + coq.say "DMOF!!!!!!!! Module" Module, + coq.say "DMOF!!!!!!!! D" D, + if-verbose (coq.say {header} "declare record axioms_"), Kname = "Axioms_", RDeclSkel = record "axioms_" Sort1 Kname Fields, @@ -230,7 +289,9 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-indt-decl RDecl RDeclClosed _, - % coq.say RDecl RDeclClosed, +% coq.say "TEST" RDecl RDeclClosed, +% coq.say "TEST" RDecl, +% coq.say "TEST" (indt R), if (get-option "primitive" tt) (@primitive! => log.coq.env.add-indt RDeclClosed R) @@ -250,6 +311,27 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance build-deps-for-projections R MLwP GRDepsClausesProjs, GRDepsClauses = [gref-deps (indt R) MLwP, gref-deps (indc K) MLwP|GRDepsClausesProjs], + % coq.say "TODO: extract useful info:" RDecl, + % coq.say "TODO: extract useful info:" RDecl "AND THEN:" RDeclClosed, + % record-decl in https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi#L429 + % per trovare il vero nome del mixin database.elpi:factory-alias->gref + % per sapere quanti argomenti skippare prima del soggetto del mixin + % factory-nparams + % + % in generale hai: + % forall ....., app[mixin_alias, p1 ... pn | [ app[subject, ...] , extra]] + % mixin_alias -> mixin via factory-alias->gref + % factory-nparams mixin -> n + % + % coq.say "TEST 2" (indt R), + + if (get-option "wrapper" tt) + ((wrapper_mixin_aux (indt R) NSbj WMxn), + (WrapperClauses = [wrapper-mixin (indt R) NSbj WMxn])) + (WrapperClauses = []), + + coq.say "DMOF!!!!!!!! adding WrapperClauses " WrapperClauses, + % GRDepsClauses => mk-factory-sort MLwP (indt R) _ FactorySortCoe, % FactorySortCoe = coercion GRFSort _ _ _, @@ -271,7 +353,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 0b793248c..73b453cbc 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -23,10 +23,20 @@ declare-existing T0 F0 :- std.do! [ % that can be built using factory instance B pred declare-const i:id, i:term, i:arity, o:list (pair id constant). declare-const Name BodySkel TyWPSkel CSL :- std.do! [ + + coq.say "DC************************ NOW RUNNING (entry point) declare-const Name BodySkel TyWPSkel CSL", + coq.say "DC!!!!!!!!!!!!! In Name = " Name, + coq.say "DC!!!!!!!!!!!!! In BodySkel = " BodySkel, + coq.say "DC!!!!!!!!!!!!! In TyWPSkel = " TyWPSkel, + std.assert-ok! (coq.elaborate-arity-skeleton TyWPSkel _ TyWP) "Definition type illtyped", coq.arity->term TyWP Ty, std.assert-ok! (coq.elaborate-skeleton BodySkel Ty Body) "Definition illtyped", + coq.say "DC!!!!!!!!!!!!! Ex Body = " Body, + coq.say "DC!!!!!!!!!!!!! Ex TyWP = " TyWP, + coq.say "DC!!!!!!!!!!!!! Ex Ty = " Ty, + % handle parameters via a section -- begin if (TyWP = arity SectionTy) ( % Do not open a section when it is not necessary (no parameters) @@ -40,16 +50,27 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [ private.postulate-arity TyWP [] Body SectionBody SectionTy ), + coq.say "DC!!!!!!!!!!!!! Ex SectionName = " SectionName, + coq.say "DC!!!!!!!!!!!!! Ex SectionBody = " SectionBody, + coq.say "DC!!!!!!!!!!!!! Ex SectionTy = " SectionTy, + % identify the factory std.assert! (coq.safe-dest-app SectionTy (global FactoryAlias) Args) "The type of the instance is not a factory", factory-alias->gref FactoryAlias Factory, std.assert! (factory-nparams Factory NParams) "Not a factory synthesized by HB", + coq.say "DC!!!!!!!!!!!!! Ex Factory = " Factory, + coq.say "DC!!!!!!!!!!!!! Ex FactoryAlias = " FactoryAlias, + coq.say "DC!!!!!!!!!!!!! Ex Args = " Args, + coq.say "DC!!!!!!!!!!!!! Ex NParams = " NParams, + % declare the constant for the factory instance private.hack-section-discharging SectionBody SectionBodyHack, private.optimize-body SectionBodyHack OptimizedBody, if (Name = "_") (RealName is "HB_unnamed_factory_" ^ {std.any->string {new_int} }) (RealName = Name), + coq.say "DC!!!!!!!!!!!!! Ex RealName = " RealName, + % unfold local instances in the type of C if (current-mode (builder-from _ _ _ _)) (std.do![ findall-local-canonical LocalCSL, @@ -57,26 +78,62 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [ UnfoldClauses => copy SectionTy SectionTyUnfolded, ]) (SectionTy = SectionTyUnfolded), + coq.say "DC!!!!!!!!!!!! Ex LocalCSL = " LocalCSL, + coq.say "DC!!!!!!!!!!!! Ex UnfoldClauses = " UnfoldClauses, + coq.say "DC!!!!!!!!!!!! Ex SectionTyUnfolded = " SectionTyUnfolded, + + % Here the body of the definition (OptimizedBody) is associated with a name (C) log.coq.env.add-const-noimplicits-failondup RealName OptimizedBody SectionTyUnfolded @transparent! C, TheFactory = (global (const C)), + coq.say "DC!!!!!!!!!!!! Ex OptimizedBody (linking point with TheFactory) = " OptimizedBody, + coq.say "DC!!!!!!!!!!!! Ex C = " C, + % call HB.instance TheType TheFactory std.drop NParams Args [TheType|_], private.check-non-forgetful-inheritance TheType Factory, - private.declare-instance Factory TheType TheFactory Clauses CSL, + coq.say "DC!!!!!!!!!!!!! Ex TheType = " TheType, + coq.say "DC!!!!!!!!!!!!! Ex TheFactory = " TheFactory, + + % Clauses and CSL are outputs. QUESTION: what is the context here? + % private.declare-instance Factory TheType TheFactory Clauses CSL, + private.redirect-instances RealName Factory TheType TheFactory Body TyWP SectionName Clauses CSL, + /* % 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 ), + */ + /* + %%%%%%%%%%%%%%% temporary test code + %%% (type-check failure if called from inside the section) + coq.safe-dest-app TheType TheTypeKey _, + if (TheTypeKey = global TheTypeKeyGR) + (std.do! [ + std.findall (wrapper-mixin _ TheTypeKeyGR Factory) Wrappers, + coq.say "REDIN!!!!!!! WRAPPERS = " Wrappers, + if (Wrappers = [W|_]) + % there is a wrapper (we actually don't want more than one) + (private.dry-run Body W _ _) + % there happens to be no wrapper, just treat it as a normal instance + true + ] + ) + true, + %%%%%%%%%%%%%%%%%%%%%%%% + */ % we accumulate clauses now that the section is over - acc-clauses current Clauses -]. + % QUESTION - what is this really accumulating? appears to be always empty + acc-clauses current Clauses, + + coq.say "DC!!!!!!!!!!!!! Out Clauses = " Clauses, +]. % [declare-all T CL MCSTL] given a type T and a list of class definition % CL in topological order (from least dep to most) looks for classes @@ -86,6 +143,13 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [ % 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). declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :- + + coq.say "NOW RUNNING!!!!!!!!!!!!!! declare-all", + coq.say "DALL!!!!!!!!!! In T = " T, + coq.say "DALL!!!!!!!!!! In Class = " Class, + coq.say "DALL!!!!!!!!!! In Struct = " Struct, + coq.say "DALL!!!!!!!!!! In MLwP = " MLwP, + if (not(has-CS-instance? T Struct)) true % we build it (if-verbose (coq.say {header} "skipping already existing" @@ -96,6 +160,8 @@ declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :- params->holes MLwP Params, get-constructor Class KC, + coq.say "DALL!!!!!!!!!!!!!! Exec1 ", + if (synthesis.infer-all-args-let Params T KC KCApp ok) (if-verbose (coq.say {header} "we can build a" {nice-gref->string Struct} "on" {coq.term->string T})) @@ -103,6 +169,8 @@ declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :- !, + coq.say "DALL!!!!!!!!!!!!!! Exec2 ", + Name is {cs-pattern->name {term->cs-pattern T}} ^ "__canonical__" ^ {gref->modname Struct 2 "_" }, @@ -122,7 +190,43 @@ declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :- if-verbose (coq.say {header} "structure instance" Name "declared"), + coq.say "DALL!!!!!!!!!! Out Name = " Name, + coq.say "DALL!!!!!!!!!! Out CS = " CS, + coq.say "DALL!!!!!!!!!! Env Clauses = " Clauses, + Clauses => declare-all T Rest L. + +/* +% In a WRAPPING-RELEVANT INSTANCE, +% Factory is the wrapped mixin, TheType is the new subject, +% TheFactory is the wrapped instance for the new subject (in fact, +% it is the term for the instance that is being processed). +% E.g. in connection with our example in monoid_enriched_cat.v: +% +% HB.instance Definition funQ_isMon (A B: Type) : isMon (hom A B) := +% funQ_isMonF A B. +% +% Factory = isMon +% TheFactory = funQ_isMon +% TheType = hom A B +*/ +/* +% Trying to reinsert here the call to derive-wrapper-instances (which was in declare-const). +% Is it still needed? (not clear). +% Apart from other problems, this assumes that CS is the canonical instance generated +% in place of funQ_isMon (not evident at all). +% Probably doesn't make sense. + if (THD = global TheTypeKeyGR) + (std.do! [ + % Name1 is nothing, should find the right mixin + std.findall (wrapper-mixin _ TheTypeKeyGR Name1) Wrappers, + coq.say "WRAPPERS:" Wrappers, + std.forall Wrappers (private.derive-wrapper-instances (local.canonical CS)) + ] + ) + true. +% +*/ declare-all T [_|Rest] L :- declare-all T Rest L. declare-all _ [] []. @@ -200,6 +304,12 @@ 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). declare-instance Factory T F Clauses CSL :- + + coq.say "DI!!!!!!!!!!!!!!! NOW RUNNING (C1) private.declare-instance Factory T F Clauses CSL", + coq.say "DI!!!!!!!! Factory = " Factory, + coq.say "DI!!!!!!!! T = " T, + coq.say "DI!!!!!!!! F = " F, + current-mode (builder-from T TheFactory FGR _), !, if (get-option "local" tt) (coq.error "HB: declare-instance: cannot make builders local. @@ -208,17 +318,30 @@ declare-instance Factory T F Clauses CSL :- declare-canonical-instances-from-factory-and-local-builders Factory T F TheFactory FGR Clauses CSL. declare-instance Factory T F Clauses CSL :- + + coq.say "DI!!!!!!!!!!!!!!!! NOW RUNNING (C2) private.declare-instance Factory T F Clauses CSL", + coq.say "DI!!!!!!!!! In Factory = " Factory, + coq.say "DI!!!!!!!!! In T = " T, + coq.say "DI!!!!!!!!! In F = " F, + declare-canonical-instances-from-factory Factory T F CSL, if (get-option "export" tt) (coq.env.current-library File, std.map CSL (x\r\ sigma i c\ x = pr i c, r = instance-to-export File i c) Clauses) - (Clauses = []). + (Clauses = []), + + coq.say "DI!!!!!!!!! In Clauses = " Clauses. % [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! [ + + coq.say "AM!!!!!!!!!!!!!!!!!!!! NOW RUNNING add-mixin", + coq.say "AM!!!!!!!!!! In T (for the subject) = " T, + coq.say "AM!!!!!!!!!! In MissingMixin (the mixin, might be a base one) = " MissingMixin, + new_int N, % timestamp synthesis.assert!-infer-mixin T MissingMixin Bo, @@ -231,6 +354,10 @@ add-mixin T FGR MakeCanon MissingMixin [MixinSrcCl, BuilderDeclCl] CSL :- std.do std.assert! (MissingMixin = MixinName) "HB: anomaly: we built the wrong mixin", + coq.say "AM!!!!!!!!!! Ex Bo = " Bo, + coq.say "AM!!!!!!!!!! Ex Ty = " Ty, + coq.say "AM!!!!!!!!!! Ex MixinName = " MixinName, + % If the mixin instance is already a constant there is no need to % alias it. if (Bo = global (const C)) true @@ -241,19 +368,85 @@ add-mixin T FGR MakeCanon MissingMixin [MixinSrcCl, BuilderDeclCl] CSL :- std.do (std.do! [ if-verbose (coq.say {header} "declare canonical mixin instance" C), with-locality (log.coq.CS.declare-instance C), - CSL = [pr "_" C] + CSL = [pr "_" C], ]) (CSL = []), + + coq.say "AM!!!!!!!!!! Out C (instance name) = " C, + coq.say "AM!!!!!!!!!! Out MixinSrcCl = " MixinSrcCl, + coq.say "AM!!!!!!!!!! Out BuilderDeclCl = " BuilderDeclCl, + coq.say "AM!!!!!!!!!! Out CSL = " 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! [ + o:list prop, o:list (pair id constant), o:list term. +add-all-mixins T FGR ML MakeCanon Clauses CSL Sbjs:- std.do! [ + + Sbjs = [T], + coq.say "AAM!!!!!!!!!!!!!!!!! NOW RUNNING add-all-mixins", + coq.say "AAM!!!!!!!!!! In T (subject, possibly a wrapping one, e.g. 'hom ...') = " T, + coq.say "AAM!!!!!!!!!! In Factory (FGR, the factory mixin) = " FGR, + coq.say "AAM!!!!!!!!!! In ML (atomic mixins for FGR; there might be a base one, e.g. 'isMonoid') = " ML, + coq.say "AAM!!!!!!!!!! In MakeCanon = " MakeCanon, + + 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, + + coq.say "AAM!!!!!!!!!! Out Clauses = " Clauses, + coq.say "AAM!!!!!!!!!! Out CSL = " CSL, + coq.say "AAM!!!!!!!!!! Out Sbjs = " Sbjs, +]. + +/* +pred add-mixin i:term, i:factoryname, i:bool, i:mixinname, + o:list prop, o:list (pair id constant), o:list term. +add-mixin T FGR MakeCanon MissingMixin [MixinSrcCl, BuilderDeclCl] CSL Subj :- std.do! [ + + coq.say "AM!!!!!!!!! NOW RUNNING add-mixin", + + new_int N, % timestamp + + synthesis.assert!-infer-mixin T MissingMixin Bo, + MixinSrcCl = mixin-src T MixinName (global (const C)), + BuilderDeclCl = builder-decl (builder N FGR MixinName (const C)), + + std.assert-ok! (coq.typecheck Bo Ty) "declare-instances: mixin illtyped", + safe-dest-app Ty (global MixinNameAlias) _, + factory-alias->gref MixinNameAlias MixinName, + + std.assert! (MissingMixin = MixinName) "HB: anomaly: we built the wrong mixin", + + % If the mixin instance is already a constant there is no need to + % alias it. + if (Bo = global (const C)) true + (Name is {gref->modname FGR 2 "_"} ^"__to__" ^ {gref->modname MixinName 2 "_"}, + if-verbose (coq.say {header} "declare mixin instance" Name), + log.coq.env.add-const-noimplicits Name Bo Ty @transparent! C), + if (MakeCanon = tt, whd (global (const C)) [] (global (indc _)) _) + (std.do! [ + if-verbose (coq.say {header} "declare canonical mixin instance" C), + with-locality (log.coq.CS.declare-instance C), + CSL = [pr "_" C], Subj = [T], + ]) (CSL = []), (Subj = []), +]. +*/ +/* +pred add-all-mixins i:term, i:factoryname, i:list mixinname, i:bool, + o:list prop, o:list (pair id constant), o: list term. +add-all-mixins T FGR ML MakeCanon Clauses CSL Sbjs :- std.do! [ + std.map ML (m\ o\ sigma ClL CSL\ - add-mixin T FGR MakeCanon m ClL CSL, o = pr ClL CSL) ClLxCSL_L, + add-mixin T FGR MakeCanon m ClL CSL Sbj, o = pr (pr ClL CSL) Sbj) ClLxCSLxSbj_L, + stf.unzip ClLxCSLxSbj ClLxCSL_L Sbj_L, std.unzip ClLxCSL_L ClLL CSLL, std.flatten ClLL Clauses, - std.flatten CSLL CSL + std.flatten CSLL CSL, + std.flatten Sbj_L Sbjs, ]. +*/ % [postulate-arity A Acc T TS] postulates section variables % corresponding to parameters in arity A. TS is T applied @@ -281,19 +474,53 @@ pred declare-canonical-instances-from-factory-and-local-builders declare-canonical-instances-from-factory-and-local-builders Factory T F _TheFactory FGR Clauses CSL :- std.do! [ synthesis.under-new-mixin-src-from-factory.do! T F (NewMixins\ std.do! [ - add-all-mixins T FGR NewMixins ff Clauses MCSL, + add-all-mixins T FGR NewMixins ff Clauses MCSL _, ]), list-w-params_list {factory-provides Factory} ML, Clauses => instance.declare-all T {findall-classes-for ML} CCSL, std.append MCSL CCSL CSL ]. +%%%%%%%%%%%%%% + +% cumulates output over forall +pred cumul-forall i:list A, i:(A -> B -> prop), o:list B. +cumul-forall [] _ []. +cumul-forall [X|L] P [Y|M] :- P X Y, cumul-forall L P M. + +% flattens cumulated list output +pred flat-cumul-forall i:list A, i:(A -> list B -> prop), o:list B. +flat-cumul-forall X P Y :- cumul-forall X P W, flatten W Y. + +% merges list1 and list2 so that list1 doesn't introduce k-duplicates +pred hmerge i:list (pair B C), i:list (pair B C), o:list (pair B C). +hmerge [] A A. +hmerge [(pr K _)|LA] LX LY :- coq.lookup! LX K _, hmerge LA LX LY. +hmerge [(pr K V)|LA] LX [(pr K V)|LY] :- hmerge LA LX LY. +%hmerge [(pr K1 V1)|LA] LX LY1 :- if (coq.lookup! LX K1 _) (LY1 = LY0) (LY1 = [(pr K1 V1)|LY0), +% hmerge LA LX LY0. + +% cumulates without k-duplicates +pred hcumul-forall i:list A, i:(A -> list (pair B C) -> prop), o:list (pair B C). +hcumul-forall [] _ []. +hcumul-forall [X|L] P M2 :- P X M1, hmerge M1 M0 M2, hcumul-forall L P M0. + +%%%%%%%%%%%%%%%%% + % [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 (pair id constant). declare-canonical-instances-from-factory Factory T F CSL :- std.do! [ + + coq.say "DCIFF!!!!!!!!!!! NOW RUNNING declare-canonical-instances-from-factory", + + coq.say "DCIFF!!!!!!! In Factory = " Factory, + coq.say "DCIFF!!!!!!! In T = " T, + coq.say "DCIFF!!!!!!! In F = " F, + coq.safe-dest-app T Key _, + % 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 @@ -301,13 +528,57 @@ declare-canonical-instances-from-factory Factory T F CSL :- std.do! [ synthesis.under-mixin-src-from-factory.do! T F [ synthesis.under-local-canonical-mixins-of.do! T [ list-w-params_list {factory-provides Factory} ML, - add-all-mixins T Factory ML tt _ MCSL, - instance.declare-all T {findall-classes-for ML} CCSL, + coq.say "DCIFF!!!!!!! Ex ML (mixin names) = " ML, + %std.findall (mixin-src (sort _) _ _) YYY, + + /* + % POSSIBLE CHANGE? + + (std.forall ML (m\ sigma Wrappers\ sigma KeyGR\ + Key = global KeyGR, + std.findall (wrapper-mixin _ KeyGR m) Wrappers, + coq.say "DOVREMMO FARE" Wrappers) ; true), + */ + + % Clauses, MCSL and AllSubjects are outputs. currently, AllSubjects = [T] + add-all-mixins T Factory ML tt ClausesFromF MCSL AllSubjects, + coq.say "DCIFF!!!!!!!!!!! Ex AllSubjects = " AllSubjects, + % old (Clauses not used) + % instance.declare-all T {findall-classes-for ML} CCSL, + hcumul-forall AllSubjects (s \ + instance.declare-all s {findall-classes-for ML}) CCSL, + ] + ], + + % Clauses => instance.declare-all T {findall-classes-for ML} CCSL, + % new (should use Clauses and AllSubjects) + %std.findall (mixin-src (sort _) _ _) XXX, + %coq.say "XXX" XXX, + %coq.say "Clauses" Clauses, + %coq.say "YYY dentro il under-*" YYY, + %std.spy( + %Clauses => hcumul-forall AllSubjects (s \ + % instance.declare-all s {findall-classes-for ML}) CCSL + %), +/* +%% New code: + % this should output all the candidate subjects too, as a new output argument. + add-all-mixins T Factory ML tt Clauses MCSL AllSubjects, ] ], - std.append MCSL CCSL CSL + % AllSubjects = [T], % change this using the additional output in add-all-mixins + % declare-all now is mapped on all the subjects, while Clauses is added to the context. + Clauses => std.forall AllSubjects + (s \ instance.declare-all s {findall-classes-for ML} CCSL), +%% +*/ + coq.say "DCIFF!!!!!!!!!! Ex Clauses = " Clauses, + coq.say "DCIFF!!!!!!!!!! Ex CCSL = " CCSL, + + std.append MCSL CCSL CSL, + coq.say "DCIFF!!!!!!!!!! Out CSL = " CSL, ]. - + % 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. @@ -320,7 +591,8 @@ hack-section-discharging B B. % unfolds the constant used for the phant abbreviation to avoid storing all % the phantom abstrctions and idfun that were used to trigger inference pred optimize-body i:term, o:term. -optimize-body (app[global (const C)| Args]) Red :- (phant-abbrev _ (const C) _ ; (rex_match "phant_" {coq.gref->id (const C)})), !, +optimize-body (app[global (const C)| Args]) Red :- + (phant-abbrev _ (const C) _ ; (rex_match "phant_" {coq.gref->id (const C)})), !, coq.env.const C (some B) _, hd-beta B Args HD Stack, unwind HD Stack Red. @@ -375,4 +647,294 @@ check-non-forgetful-inheritance T Factory :- std.do! [ ) true ]. +% The type of the wrapper projection is... +% hom_isMon.hom_isMon_private : +% forall (T : Type) +% (local_mixin_monoid_enriched_cat_isQuiver : isQuiver.axioms_ T), +% hom_isMon.axioms_ T local_mixin_monoid_enriched_cat_isQuiver -> +% forall +% A +% B : {| +% Quiver.sort := T; +% Quiver.class := +% {| +% Quiver.monoid_enriched_cat_isQuiver_mixin := +% local_mixin_monoid_enriched_cat_isQuiver +% |} +% |}, isMon.phant_axioms (hom A B) + +pred mk_wrapper_instance_name i:mixinname i:term o:string. +mk_wrapper_instance_name W Ins Str :- + coq.gref->modname W Str0, + coq.term->string Ins Str1, + % coq.term->string (global W) Str0, + std.string.concat "__" [Str1, Str0] Str. + +% Not used, but possible useful +pred mk_wrapper_instance_name i:mixinname i:term o:string. +mk_wrapper_instance_name W Ins Str :- + coq.gref->modname W Str0, + coq.term->string Ins Str1, + % coq.term->string (global W) Str0, + std.string.concat "__" [Str1, Str0] Str. + +% Instance has morally type 'Mixin Subject'. +% Has to change, no instance as input but a definition (like BodySkel in declare_instance, +% still a term, and its type TySkel). +% Morever, in general this may apply to more than a mixin (if the base mixin is not a trivially +% atomic one). +% Important to ensure there is a consistent naming scheme. +pred derive-wrapper-instances i:term, i:prop, o:list prop, o:list (pair id constant). +derive-wrapper-instances Instance (wrapper-mixin WrapperMixin Subject Mixin) + Clauses CSL :- std.do! [ + + coq.say "DWI!!!!!!!!!! NOW RUNNING derive-wrapper-instances Instance _", + coq.say "DWI!!!!!!! Instance = " Instance, + + % K is the mixin constructor (Build) for WrapperMixin + factory-constructor WrapperMixin K, + factory-nparams WrapperMixin NParams, + std.assert! (NParams = 0) "TODO support parameters", + + % We are only interested in the last parameter of the constructor + % type, which is the current instance + % (which is a Mixin instance on the new Subject). + % In monoid_enriched_cat.v, we are targeting the code + % + % HB.instance Definition funQ_hom_isMon := + % hom_isMon.Axioms_ _ _ funQ_isMon. + % which Coq can compute to stand for + % hom_isMon.Axioms_ Type funQ funQ_isMon. + % + % We compute the number of the underscores and we pass + % them as arguments followed by Instance. + coq.env.typeof K KTy, + coq.count-prods KTy KN, + KN0 = KN - 1, + coq.mk-n-holes KN0 Holes, + + std.append Holes [Instance] Args, + + % the body of the new wrapper instance + NewInstance = app[global K| Args], + + coq.say "DWI!!!!!!!!! NewInstance =" {coq.term->string NewInstance}, + + coq.typecheck NewInstance Ty Dgn, + coq.say "DWI!!!!!!!!!! Ty = " Ty, + + if (Dgn = error S) (coq.say "DWI!!!!!!!!! error in NewInstance" S) + (coq.count-prods Ty N0, + % we then call declare-const to add the new instance. + % the name needs to be fixed. + % name generation doesn't work because of dot occurrences + % mk_wrapper_instance_name Wrapper_Mixin Instance Nm, + % instance.declare-const "funq_instance_name" NewInstance {coq.term->arity Ty N0} _ + coq.safe-dest-app Ty _Factory FArgs, + std.nth NParams FArgs WrapperSubject, + + coq.say "DWI!!!!!!!!!!! OK", + coq.say "DWI!!!!!!!!!!! WrapperMixin = " WrapperMixin, + coq.say "DWI!!!!!!!!!!! NewInstance = " NewInstance, + coq.say "DWI!!!!!!!!!!! WrapperSubject = " WrapperSubject, + + private.declare-instance WrapperMixin WrapperSubject NewInstance Clauses CSL + ) + +/* +% 2) The existing instances of W correspond to the functions of type (Ty _) +% that are already defined for different original subjects; +% or in other words, they correspond to wrapped instances, +% given a specific original subject T and two generic objects of that type. +% Should we consider only one function for each T? +% This means that e.g. there is only one way a homset can be instance of the wrapped +% (here, a monoid). +% Notice that it's good to assume all relevant functions have been +% defined using generic type syntax (otherwise recovering them would be much harder). +% This means for a carrier there is only a quiver. +% The instances whould be filtered out from the current context, maybe EX? + filter_out_unique_defs_of_type Ty WrapperProjections, +% filter_out_unique_defs_of_type Ty AllInstances WrapperProjections, +% 3) We can define the wrapper instances based on Ty, using the projection definitions. + std.forall WrapperProjections (export-wrapper-instance W) +*/ +]. +derive-wrapper-instances _ _ [] []. + +pred dec-inst-and-close i:factoryname, i:term, i:term, i:arity, i:id, + o:list prop, o:list (pair id constant). +dec-inst-and-close Factory TheType TheFactory TyWP SectionName Clauses CSL :- std.do! [ + + private.declare-instance Factory TheType TheFactory Clauses CSL, + % 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 + ) +]. + +% split between direct call to declare-instance and indirect one through derive-wrapper-instances +pred redirect-instances i:id, i:factoryname, i:term, i:term, i:term, i:arity, i:id, + o:list prop, o:list (pair id constant). +redirect-instances RealName Factory TheType TheFactory Body TyWP SectionName Clauses CSL :- + std.do! [ + coq.safe-dest-app TheType TheTypeKey _, + + coq.say "NOW RUNNING****************************** REDIN " + coq.say "REDIN!!!!!!! TheTypeKey = " TheTypeKey, + + if (rex.match ".*__ELIM" RealName) % meant to rule out generated instances + (private.dec-inst-and-close Factory TheType TheFactory TyWP SectionName Clauses CSL) + (if (TheTypeKey = global TheTypeKeyGR) + (std.do! [ + std.findall (wrapper-mixin _ TheTypeKeyGR Factory) Wrappers, + coq.say "REDIN!!!!!!! WRAPPERS = " Wrappers, + if (Wrappers = [W|_]) + % there is a wrapper (we actually don't want more than one) + ( if (TyWP = arity _) true ( + if-verbose (coq.say {header} "closing instance section"), + log.coq.env.end-section-name SectionName ), + % we accumulate clauses now that the section is over + %acc-clauses current Clauses0, + %coq.say "REDIN!!!!!!! Clauses0 = " Clauses0, + %Clauses0 => + private.derive-wrapper-instances TheFactory W Clauses CSL + % private.declare-instance Factory TheType TheFactory Clauses CSL + ) + % there happens to be no wrapper, just treat it as a normal instance + (private.dec-inst-and-close Factory TheType TheFactory TyWP SectionName Clauses CSL) + ] + ) + % there can be no wrapper, just treat it as a normal instance + (private.dec-inst-and-close Factory TheType TheFactory TyWP SectionName Clauses CSL) + ) +]. + +% test predicate +pred dry-run i:term, i:prop, o:list prop, o:list (pair id constant). +dry-run Instance (wrapper-mixin WrapperMixin Subject Mixin) [] [] :- std.do! [ + + coq.say "DWI!!!!!!!!! NOW RUNNING derive-wrapper-instances Instance _", + coq.say "DWI!!!!!!! Instance = " Instance, + + % K is the mixin constructor (Build) for WrapperMixin + factory-constructor WrapperMixin K, + factory-nparams WrapperMixin NParams, + std.assert! (NParams = 0) "TODO support parameters", + + coq.say "DWI!!!!!!! K = " K, + coq.say "DWI!!!!!!! NParams = " NParams, + + coq.env.typeof K KTy, + coq.count-prods KTy KN, + KN0 = KN - 1, + coq.mk-n-holes KN0 Holes, + + std.append Holes [Instance] Args, + + coq.say "DWI!!!!!!! KTy = " KTy, + coq.say "DWI!!!!!!! KN = " KN, + coq.say "DWI!!!!!!! Args = " Args, + + % the body of the new wrapper instance + NewInstance = app[global K| Args], + + coq.say "DWI!!!!!!!!! NewInstance = " {coq.term->string NewInstance}, + + coq.typecheck NewInstance Ty Dgn, + + coq.say "DWI!!!!!!!!! Ty = " Ty, + coq.say "DWI!!!!!!!!! Dgn = " Dgn, + + if (Dgn = error S) (coq.say "error in NewInstance" S) + (coq.count-prods Ty N0 + % instance.declare-instance WrapperMixin Ty NewInstance Clauses CSL + ), +]. +dry-run _ _ [] []. + + +/* +GENERAL COMMENT 05/07/2023. +We have already implemented the elimination rule for wrapper +instances (adding the projection means that given a wrapper instance +we can get a base mixin one). +We are now implementing the introduction rule for wrapper mixins, +that is, given a function definition (prospected instance) that has +the type of the wrapper projection specialized to the base mixin +(base = wrapped), we can derive a wrapper instance. +The current proposed solution assumes that the prospected instance +has already been lifted to a base mixin instance, and additionally +introduces the wrapper instance. +This is undesirable, as in fact, given the wrapper projection, the +base mixin instance can be derived from the wrapper instance. +So we actually want to use the prospected instance to introduce +the wrapper instance directly. +Moreoever, our solution only works when the base mixin is atomic (note this +is why we need to get down to add-all-mixins). +Finally, the current solution involves iterating over all the wrappers, +given an instance, in order to check whether it is a base mixin instance +for some wrapper. +So it is not good to call 'derive-wrapper-instances' in 'declare-const'. + +Top-level (called in structures.v): 'instance.declare-const', 'structure.declare'. + +Our real entry point should be 'instance.private.declare-instance' (after line 243) +Notice that 'declare-instance' is only called in 'instance.declare-const' +(ignore 'instance.declare-existing', deprecated). + +'instance.declare-const' is called in 'instance.mk-factory-sort-factory' +(called in instance.declare-factory-sort-deps and + instance.declare-factory-sort-factory), +in 'instance.private.derive-wrapper-instance' (our predicate, + called in instance.declare-const), +in 'structure.declare', +in 'structure.private.reexport-wrapper-as-instance' (our predicate, + called in structure.declare). + +There are two clauses for this predicate (some refactoring needed?) +We will focus on the latter (after line 253), which calls +'declare-canonical-instances-from-factory' (defined after line 337). + +At line 3**, Factory is the mixin (base mixin), + T is actually the subject (a type, e.g. the new subject (@hom T0 A B)), + F is the prospective instance (e.g. funQ, funQ_isMon), + ML are the mixins (the axioms that are needed for the subject...) ???, + CSL are the clauses so far. +Notably: + Line 3**, 'synthesis.under-mixin-src-from-factory.do!'. + Line 3**, 'add-all-mixins'. + Line 3**, 'declare-all'. + +In the implemention of 'under-mixin-src-from-factory.do!' +(line 99, synthesis.elpi), +- the first two arguments of 'mixin-src', i.e 'TheType' and 'm', + should be related by 'wrapper-mixin' + (with 'hom' extracted from 'TheType' ??) + (with 'm' as base mixin ??) +- 'std.map' ranges over 'ML' (the mixins) and produces clauses + collected in MLClauses +- the third argument is the continuation (executed after locally + adding MLClauses to the context). + Here 'add-all-mixins' is called (line 347, instance.elpi). + +'add-all-mixins' (defined after line 291) calls +'add-mixin' (defined after line 262). +In 'add-mixin' we should check when 'MissingMixin' is a wrapped one. +Change then will affect 'C'. +Also check 'assert!-infer-mixin' (synthesis.elpi, line 81) which +calls 'mixin-for' (synthesis.elpi, line 176). +'mixin-for' actually produces a mixin instance for a mixin and a type, +given a database. + +Main targets for change: +- add-all-mixins: see the proposed change +- ? 'add-mixin': check 'MissingMixin', change 'C'. +- ? discussion about overloading of 'mixin-src': used in different predicates, + not really understood (??) +- ? possible refactoring of 'declare-instance' +- ? 'under-mixin-src-from-factory.do!' : actually no need to change the subject + +*/ + }} diff --git a/HB/structure.elpi b/HB/structure.elpi index addf308a4..4b18fbfbf 100644 --- a/HB/structure.elpi +++ b/HB/structure.elpi @@ -8,6 +8,9 @@ namespace structure { pred declare i:string, i:term, i:sort. pred declare i:string, i:term, i:universe. declare Module BSkel Sort :- std.do! [ + + coq.say "D!!!!!!!!!!!!!! NOW RUNNING declare", + disable-id-phant BSkel BSkelNoId, std.assert-ok! (coq.elaborate-skeleton BSkelNoId _ BNoId) "illtyped structure definition", re-enable-id-phant BNoId B, @@ -205,6 +208,43 @@ declare Module BSkel Sort :- std.do! [ log.coq.env.end-module-name ElpiOperationModName ElpiOperations, export.module ElpiOperationModName ElpiOperations, + % factories-provide (line 16) gives the mixins provided from a factory. + % line 23 (list-w-params_list) associates these mixins with their names (ML). + % we need to filter the wrappers out of ML. + % then export the projection of each mixin wrapper. + % can use exported-op to this purpose + + %% tentative pseudo-code:: + % std.filter ML (x\ wrapper-mixin x _ _) WrapperML, + % std.forall WrapperML private.rexport-wrapper-as-instance, + + %% write private code below: + % pred rexport-wrapper-as-instance i:mixinname. + % reexport-wrapper-as-instance M :- + % exported-op M _ C, + % declare-existing-instance C %fixme. + + std.filter ML (x\ wrapper-mixin x _ _) WrapperML, + % we need to assert locally the clauses in EX, which is + % [exported-op (indt «hom_isMon.axioms_») «hom_isMon.hom_isMon_private» + % «hom_isMon_private»] + % crucially containing hom_isMon_private. + % In fact, these clauses get added to the global database by Accumulate, + % but this makes them available only at the end of the program run, and + % this is too late. + % Then given WrapperML (the list of the wrapper mixins as grefs) + % i.e. [indt «hom_isMon.axioms_»] + % we can use reexport-wrapper-as-instance to get the projection and build + % the instances. + coq.say "D!!!!!!!!!!!! WrapperML " WrapperML, + coq.say "D!!!!!!!!!!!! EX (local context): " EX, + + EX => std.forall WrapperML private.reexport-wrapper-as-instance, + + % tentative: generating wrapper instances from the available definitions. + % Wrong approach: we actually need to check each new defined instance to + % see if it triggers a wrapper instance too. We do this in instance.elpi. + if-verbose (coq.say {header} "abbreviation factory-by-classname"), NewClauses => factory.declare-abbrev Module (factory.by-classname ClassName), @@ -738,4 +778,32 @@ mk-hb-eta.arity Structure ClassName SortProjection Out = parameter {coq.name->id NT} explicit Ty s\ arity (Concl s) ]. +% M is the gref of the wrapper mixin. +% C gets now instantiated to the projection, i.e. hom_isMon_private. +% we need to count the parameters, we can get that from the type. +% we then can construct the instance, using +% instance.declare-const (notably used in the API, i.e. in structures.v, +% HB.instance) +pred reexport-wrapper-as-instance i:mixinname. +% reexport-wrapper-as-instance M :- std.spy-do! [ +reexport-wrapper-as-instance M :- std.do! [ + coq.say "RWAI!!!!!!!!!!! NOW RUNNING private.reexport-wrapper-as-instance", + + exported-op M _ C, + + coq.say "RWAI!!!!!!! M = " M, + coq.say "RWAI!!!!!!! C = " C, + + B = (global (const C)), + coq.env.typeof (const C) Ty, + coq.count-prods Ty N0, + coq.term->arity Ty N0 Arity, +% coq.term->string (global M) Str1, +% need to get a valid idenfier out of a term, no @ or . +% std.string.concat "__" [Str1, "ELIM"] Str2, + Str0 is "Op_isMx" ^ "__" ^ {std.any->string {new_int}}, + std.string.concat "__" [Str0, "ELIM"] Str, + instance.declare-const Str B Arity _ + ]. + }} diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite index 98c20167e..4eae43b8b 100644 --- a/_CoqProject.test-suite +++ b/_CoqProject.test-suite @@ -80,6 +80,10 @@ tests/hnf.v tests/fun_instance.v tests/issue284.v tests/issue287.v +tests/monoid_law_structure.v +tests/monoid_law_structure_clone.v +tests/enriched_cat.v +tests/monoid_enriched_cat.v -R tests HB.tests -R examples HB.examples diff --git a/structures.v b/structures.v index 30c9015f4..b4d1cad8c 100644 --- a/structures.v +++ b/structures.v @@ -17,6 +17,35 @@ Definition ignore_disabled {T T'} (x : T) (x' : T') := x'. (* ********************* structures ****************************** *) From elpi Require Import elpi. +(******* simple example of Elpi command *) +Axiom m : Type -> Type. +Record r (P : Type) := { private : m P }. + +(* command name *) +Elpi Command foo_example_command. +(* predicate definition *) +Elpi Accumulate lp:{{ + +pred extract i:indt-decl, o:gref. +extract (parameter ID _ _ R) Out :- + pi p\ + extract (R p) Out. +extract (record ID _ KID (field _ _ Ty (x\end-record))) GR :- + Ty = app [global GR| _]. + +}}. +Elpi Typecheck. + +(* predicate query *) +Elpi Query lp:{{ + + coq.locate "r" (indt I), + coq.env.indt-decl I D, + extract D GR. + +}}. +(******* end simple example *) + Register unify as hb.unify. Register id_phant as hb.id. Register id_phant_disabled as hb.id_disabled. @@ -159,6 +188,13 @@ pred join o:classname, o:classname, o:classname. % in order to discover two mixins are the same) pred mixin-mem i:term, o:gref. +% [wrapper-mixin Wrapper NewSubject WrappedMixin] +% #[wrapper] HB.mixin Record hom_isMon T of Quiver T := +% { private : forall A B, isMon (@hom T A B) }. +% --> +% wrapper-mixin (indt "hom_isMon") (const "hom") (indt "isMon"). +pred wrapper-mixin o:mixinname, o:gref, o:mixinname. + %%%%%% Memory of exported mixins (HB.structure) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Operations (named mixin fields) need to be exported exactly once, % but the same mixin can be used in many structure, hence this memory diff --git a/tests/cmonoid_enriched_cat.v b/tests/cmonoid_enriched_cat.v new file mode 100644 index 000000000..79b9c4247 --- /dev/null +++ b/tests/cmonoid_enriched_cat.v @@ -0,0 +1,634 @@ +From HB Require Import structures. +From Coq Require Import ssreflect ssrfun. + +(** Quiver *) + +HB.mixin Record isQuiver Obj := { hom : Obj -> Obj -> Type }. + +HB.structure Definition Quiver := { Obj of isQuiver Obj }. + +(** Ohter base mixins *) + +HB.mixin Record isMon A := { + zero : A; + add : A -> A -> A; + addrA : associative add; + add0r : left_id zero add; + addr0 : right_id zero add; + }. + +HB.mixin Record isIAlg A := { + iadd : A -> A -> A; + iaddI : idempotent iadd; + }. + +HB.mixin Record isCAlg A := { + cadd : A -> A -> A; + caddrC : commutative cadd; + }. + +(** Base structures *) + +HB.structure Definition Monoid := { A of isMon A }. + +HB.structure Definition CAlgebra := { A of isCAlg A }. + +HB.structure Definition IAlgebra := { A of isIAlg A }. + +(** Complex mixins *) + +(*******************************************************************) +(********** Combining mixins ***************************************) + +(***** Vanilla Coq (no HB) *) + +Record isMon0 A := { + zero0 : A; + add0 : A -> A -> A; + addrA0 : associative add0; + add0r0 : left_id zero0 add0; + addr00 : right_id zero0 add0; + }. + +Record isIAlg0 A := { + iadd0 : A -> A -> A; + iaddI0 : idempotent iadd0; + }. + +Record isIMon0 A := { is_mon0 : isMon0 A; + is_ialg0 : isIAlg0 A; + mon_ialg_ch0 : add0 _ is_mon0 = iadd0 _ is_ialg0 ; + }. + + +(***** The analogous of vanilla does not work in HB *) + +Fail HB.mixin Record isIMonM A := { is_mon : isMon A; + is_ialg : isIAlg A; + mon_ialg_ch : add _ is_mon = iadd _ is_ialg ; + }. + +Fail HB.mixin Record isIMonS A := { is_mon : Monoid A; + is_ialg : IAlgebra A; + mon_ialg_ch : add _ is_mon = iadd _ is_ialg ; + }. + +(***** Basic approach (can be cumbersome) *) + +HB.mixin Record isIMonB A := { + zero : A; + add : A -> A -> A; + addrA : associative add; + add0r : left_id zero add; + addr0 : right_id zero add; + addI : idempotent add; +}. + +HB.mixin Record isCMonB A := { + zero : A; + add : A -> A -> A; + addrA : associative add; + add0r : left_id zero add; + addr0 : right_id zero add; + addC : commutative add; +}. + + +(***** Operator mixins *) + +(**** single dependent pair parameter *) + +HB.mixin Record isOpMon1 (S: sigT (fun A => A -> A -> A)) := { + zero : projT1 S; + addrA : associative (projT2 S); + add0r : left_id zero (projT2 S); + addr0 : right_id zero (projT2 S); + }. + +HB.structure Definition OpMonoid1 := { C of isOpMon1 C }. + +HB.mixin Record isOpIAlg1 (S: sigT (fun A => A -> A -> A)) := { + addI : idempotent (projT2 S); + }. + +HB.structure Definition OpIAlgebra1 := { C of isOpIAlg1 C }. + +HB.mixin Record isOpIMon1 A of OpMonoid1 A & OpIAlgebra1 A. + + +(**** two parameters (subject is Add) *) + +(**) +HB.mixin Record isOpAAlg2 A (Add: A -> A -> A) := { + addA : associative Add; + }. + +HB.mixin Record isOpAAlgebra2 A := { add: A -> A -> A; + is_op_aalg : isOpAAlg2 A add }. + +HB.structure Definition OpAAlgebra2 := { A of isOpAAlgebra2 A }. + +(**) +HB.mixin Record isOpZAlg2 A (Add: A -> A -> A) (Zero: A) := { + add0r : left_id Zero Add; + addr0 : right_id Zero Add; + }. + +HB.mixin Record isOpZAlgebra2 A := { add: A -> A -> A; + zero: A; + is_op_zalg : isOpZAlg2 A add zero }. + +HB.structure Definition OpZAlgebra2 := { A of isOpZAlgebra2 A }. + +(**) +HB.mixin Record isOpMon2 A (Add: A -> A -> A) (Zero: A) := { + is_op_zalg : isOpZAlg2 A Add Zero ; + is_op_aalg : isOpAAlg2 A Add ; + }. + +HB.mixin Record isOpMonoid2 A := { add: A -> A -> A; + zero: A; + is_op_mon : isOpMon2 A add zero }. + +HB.structure Definition OpMonoid2 := { A of isOpMonoid2 A }. + +(**) +HB.mixin Record isOpIAlg2 A (Add: A -> A -> A) := { + addI : idempotent Add; + }. + +HB.mixin Record isOpIAlgebra2 A := { add: A -> A -> A; + is_op_ialg : isOpIAlg2 A add }. + +HB.structure Definition OpIAlgebra2 := { A of isOpIAlgebra2 A }. + +(**) +HB.mixin Record isOpCAlg2 A (Add: A -> A -> A) := { + addC : commutative Add; + }. + +HB.mixin Record isOpCAlgebra2 A := { add: A -> A -> A; + is_op_calg : isOpCAlg2 A add }. + +HB.structure Definition OpCAlgebra2 := { A of isOpCAlgebra2 A }. + +(**) +HB.mixin Record isOpIMon2 A (Add: A -> A -> A) (Zero: A) := { + is_op_mon : isOpMon2 A Add Zero ; + is_op_ialg : isOpIAlg2 A Add ; + }. + +HB.mixin Record isOpIMonoid2 A := { add: A -> A -> A; + zero: A; + is_op_imon : isOpIMon2 A add zero }. + +HB.structure Definition OpIMonoid2 := { A of isOpIMonoid2 A }. + +(**) +HB.mixin Record isOpCMon2 A (Add: A -> A -> A) (Zero: A) := { + is_op_mon : isOpMon2 A Add Zero ; + is_op_calg : isOpCAlg2 A Add ; + }. + +HB.mixin Record isOpCMonoid2 A := { add: A -> A -> A; + zero: A; + is_op_imon : isOpCMon2 A add zero }. + +HB.structure Definition OpCMonoid2 := { A of isOpCMonoid2 A }. + +(**) +HB.mixin Record isOpCIAlg2 A (Add: A -> A -> A) := { + is_op_ialg : isOpIAlg2 A Add ; + is_op_calg : isOpCAlg2 A Add ; + }. + +HB.mixin Record isOpCIAlgebra2 A := { add: A -> A -> A; + is_op_cialg : isOpCIAlg2 A add }. + +HB.structure Definition OpCIAlgebra2 := { A of isOpCIAlgebra2 A }. + +(**) +HB.mixin Record isOpICAlg2 A (Add: A -> A -> A) := { + is_op_calg : isOpCAlg2 A Add ; + is_op_ialg : isOpIAlg2 A Add ; + }. + +HB.mixin Record isOpICAlgebra2 A := { add: A -> A -> A; + is_op_calg : isOpICAlg2 A add }. + +HB.structure Definition OpICAlgebra2 := { A of isOpICAlgebra2 A }. + +(**) +HB.mixin Record isOpACIAlg2 A (Add: A -> A -> A) := { + is_op_ialg : isOpIAlg2 A Add ; + is_op_calg : isOpCAlg2 A Add ; + is_op_aalg : isOpAAlg2 A Add ; + }. + +HB.mixin Record isOpACIAlgebra2 A := { add: A -> A -> A; + is_op_acialg : isOpACIAlg2 A add }. + +HB.structure Definition OpACIAlgebra2 := { A of isOpACIAlgebra2 A }. + +(**) +HB.mixin Record isOpCIMon2 A (Add: A -> A -> A) (Zero: A) := { + is_op_mon : isOpIMon2 A Add Zero ; + is_op_calg : isOpCAlg2 A Add ; + }. + +HB.mixin Record isOpCIMonoid2 A := { add: A -> A -> A; + zero: A; + is_op_cimon : isOpCIMon2 A add zero }. + +HB.structure Definition OpCIMonoid2 := { A of isOpCIMonoid2 A }. + +(**) +HB.mixin Record isOpICMon2 A (Add: A -> A -> A) (Zero: A) := { + is_op_mon : isOpCMon2 A Add Zero ; + is_op_calg : isOpIAlg2 A Add ; + }. + +HB.mixin Record isOpICMonoid2 A := { add: A -> A -> A; + zero: A; + is_op_cimon : isOpICMon2 A add zero }. + +HB.structure Definition OpICMonoid2 := { A of isOpICMonoid2 A }. + + +(*******************************************************************) + +(** Wrapper mixins *) + +#[wrapper] +HB.mixin Record hom_isAAlg T of Quiver T := + { hom_isAAlg_private : forall A B, isOpAAlgebra2 (@hom T A B) }. + +#[wrapper] +HB.mixin Record hom_isZAlg T of Quiver T := + { hom_isZAlg_private : forall A B, isOpZAlgebra2 (@hom T A B) }. + +#[wrapper] +HB.mixin Record hom_isMon T of Quiver T := + { hom_isMon_private : forall A B, isOpMonoid2 (@hom T A B) }. + +#[wrapper] +HB.mixin Record hom_isIAlg T of Quiver T := + { hom_isIAlg_private : forall A B, isOpIAlgebra2 (@hom T A B) }. + +#[wrapper] +HB.mixin Record hom_isCAlg T of Quiver T := + { hom_isCAlg_private : forall A B, isOpCAlgebra2 (@hom T A B) }. + +#[wrapper] +HB.mixin Record hom_isIMon T of Quiver T := + { hom_isIMon_private : forall A B, isOpIMonoid2 (@hom T A B) }. + +#[wrapper] +HB.mixin Record hom_isCMon T of Quiver T := + { hom_isCMon_private : forall A B, isOpCMonoid2 (@hom T A B) }. + +#[wrapper] +HB.mixin Record hom_isCIAlg T of Quiver T := + { hom_isCIAlg_private : forall A B, isOpCIAlgebra2 (@hom T A B) }. + +#[wrapper] +HB.mixin Record hom_isICAlg T of Quiver T := + { hom_isICAlg_private : forall A B, isOpICAlgebra2 (@hom T A B) }. + +#[wrapper] +HB.mixin Record hom_isACIAlg T of Quiver T := + { hom_isACIAlg_private : forall A B, isOpACIAlgebra2 (@hom T A B) }. + +#[wrapper] +HB.mixin Record hom_isCIMon T of Quiver T := + { hom_isCIMon_private : forall A B, isOpCIMonoid2 (@hom T A B) }. + +#[wrapper] +HB.mixin Record hom_isICMon T of Quiver T := + { hom_isICMon_private : forall A B, isOpICMonoid2 (@hom T A B) }. + + +(** Base enriched structures *) + +HB.structure + Definition Monoid_enriched_quiver := + { Obj of isQuiver Obj & hom_isMon Obj }. + +HB.structure + Definition IAlgebra_enriched_quiver := + { Obj of isQuiver Obj & hom_isIAlg Obj }. + +HB.structure + Definition CAlgebra_enriched_quiver := + { Obj of isQuiver Obj & hom_isCAlg Obj }. + +(** Complex enriched structures *) + +HB.structure + Definition IMonoid_enriched_quiver := + { Obj of isQuiver Obj & hom_isMon Obj & hom_isIAlg Obj}. + +HB.structure + Definition CIAlgebra_enriched_quiver := + { Obj of isQuiver Obj & hom_isIAlg Obj & hom_isCAlg Obj}. + +HB.structure + Definition ACIAlgebra_enriched_quiver := + { Obj of isQuiver Obj & hom_isIAlg Obj & hom_isCAlg Obj & hom_isAAlg Obj}. + +HB.structure + Definition CIMonoid_enriched_quiver := + { Obj of isQuiver Obj & hom_isMon Obj & hom_isIAlg Obj & hom_isCAlg Obj}. + + +(********* INSTANCES *****************************) + +Require Import FunctionalExtensionality. + +(** SAMPLE INSTANCE 1 *) + +HB.instance Definition funQ := isQuiver.Build Type + (fun A B => A -> option B). + +Definition funQ_comp {A B: Type} (f g: hom A B) : hom A B := + fun x => + match f x with + | Some _ => f x + | _ => g x end. + +Program Definition funQ_isMon (A B: Type) : + isOpMon2 (hom A B) funQ_comp (fun (_:A) => None) := + isOpMon2.Build _ _ (fun (_:A) => None) _ _. +Obligation 1. +econstructor. +{- unfold left_id; intros. + unfold funQ_comp; auto. +} +{- unfold right_id; intros. + eapply functional_extensionality; intro a. + unfold funQ_comp. + destruct (x a); auto. +} +Qed. +Obligation 2. +econstructor. +{- unfold associative; intros. + eapply functional_extensionality; intro a. + unfold funQ_comp. + destruct (x a) eqn:K1. + simpl; auto. + destruct (y a); auto. +} +Qed. + +Program Definition funQ_isIAlg (A B: Type) : + isOpIAlg2 (hom A B) funQ_comp := + isOpIAlg2.Build _ _ _. +Obligation 1. +unfold idempotent; intros. +eapply functional_extensionality; intro a. +unfold funQ_comp. +destruct (x a); auto. +Qed. + +Program Definition funQ_isIMon (A B: Type) : + isOpIMon2 (hom A B) funQ_comp (fun (_:A) => None) := + isOpIMon2.Build (hom A B) _ _ _ _. +Obligation 1. +eapply funQ_isMon. +Qed. +Obligation 2. +eapply funQ_isIAlg. +Qed. + +HB.instance Definition funQ_isMonoid (A B: Type) : + isOpMonoid2 (hom A B) := + isOpMonoid2.Build (hom A B) funQ_comp (fun (_:A) => None) (funQ_isMon A B). + +HB.instance Definition funQ_isIAlgebra (A B: Type) : + isOpIAlgebra2 (hom A B) := + isOpIAlgebra2.Build (hom A B) funQ_comp (funQ_isIAlg A B). + +HB.instance Definition funQ_isIMonoid (A B: Type) : + isOpIMonoid2 (hom A B) := + isOpIMonoid2.Build (hom A B) funQ_comp (fun (_:A) => None) + (funQ_isIMon A B). + +Elpi Print HB.structure. + + +(** SAMPLE INSTANCE 2 *) + +Lemma zero_unique {B} (X: B -> B -> B) (zz0 zz1:B) : + left_id zz0 X -> right_id zz0 X -> left_id zz1 X -> right_id zz1 X -> + zz0 = zz1. + unfold left_id, right_id. + intros. + specialize (H0 zz1). + specialize (H1 zz0). + rewrite H1 in H0. + auto. +Qed. + +Open Scope type. + +HB.instance Definition cmfunQ := + isQuiver.Build (sigT (fun A => (A -> A -> A) * A)) + (fun X Y => isOpCMon2 (projT1 X) (fst (projT2 X)) (snd (projT2 X)) -> + isOpCMon2 (projT1 Y) (fst (projT2 Y)) (snd (projT2 Y)) -> + (projT1 X) -> (projT1 Y)). + +Definition cmfunQ_comp {A B: sigT (fun A => (A -> A -> A) * A)} + (f g: @hom _ A B) : hom A B := + fun (ca: isOpCMon2 (projT1 A) (fst (projT2 A)) (snd (projT2 A))) + (cb: isOpCMon2 (projT1 B) (fst (projT2 B)) (snd (projT2 B))) a => + match (f ca cb a, g ca cb a) with + | (b1, b2) => (fst (projT2 B)) b1 b2 end. + +Program Definition cmfunQ_zero {A B: sigT (fun A => (A -> A -> A) * A)} : + hom A B. +Proof. + unfold hom; intros. + unfold isQuiver.hom. + unfold Quiver.cmonoid_enriched_cat4_isQuiver_mixin. + unfold Quiver.class. + simpl; intros. + destruct B as [X [f x1]]; simpl. + exact x1. +Defined. + +Program Definition cmfunQ_isCMon (A B: sigT (fun A => (A -> A -> A) * A)) : + isOpCMon2 (hom A B) cmfunQ_comp cmfunQ_zero := + isOpCMon2.Build (hom A B) cmfunQ_comp _ _ _. +Obligation 1. +unfold cmfunQ_comp; simpl. +econstructor. +econstructor. +{- unfold left_id; intros. + eapply functional_extensionality; intro CMa. + eapply functional_extensionality; intro CMb. + eapply functional_extensionality; intro v. + remember CMb as CMb1. + destruct CMb. + destruct is_op_mon0. + destruct is_op_zalg0. + unfold left_id in add0r1. + simpl in add0r1. + unfold cmfunQ_zero. + eapply add0r1. +} +{- unfold right_id; intros. + eapply functional_extensionality; intro CMa. + eapply functional_extensionality; intro CMb. + eapply functional_extensionality; intro v. + remember CMb as CMb1. + destruct CMb. + destruct is_op_mon0. + destruct is_op_zalg0. + unfold right_id in addr1. + simpl in addr1. + unfold cmfunQ_zero. + eapply addr1. +} +econstructor. +{- unfold associative; intros. + eapply functional_extensionality; intro CMa. + eapply functional_extensionality; intro CMb. + eapply functional_extensionality; intro v. + remember CMb as CMb1. + destruct CMb. + destruct is_op_mon0. + destruct is_op_aalg0. + unfold associative in addA. + simpl in addA. + eapply addA. +} +Qed. +Obligation 2. + econstructor. + unfold cmfunQ_comp. + unfold commutative; simpl; intros. + eapply functional_extensionality; intro CMa. + eapply functional_extensionality; intro CMb. + eapply functional_extensionality; intro v. + remember CMb as CMb1. + destruct CMb. + destruct is_op_calg0. + simpl in addC. + eapply addC. +Qed. + +HB.instance Definition cmfunQ_isCMonoid + (A B: sigT (fun A => (A -> A -> A) * A)) : + isOpCMonoid2 (hom A B) := + isOpCMonoid2.Build (hom A B) cmfunQ_comp cmfunQ_zero (cmfunQ_isCMon A B). + +Elpi Print HB.structure. + + +(** SAMPLE INSTANCE 3 *) + +HB.instance Definition cimfunQ := + isQuiver.Build (sigT (fun A => A -> A -> A)) + (fun X Y => isOpACIAlg2 (projT1 X) (projT2 X) -> + isOpACIAlg2 (projT1 Y) (projT2 Y) -> + (projT1 X) -> option (projT1 Y)). + +Definition cimfunQ_comp {A B: sigT (fun A => A -> A -> A)} + (f g: hom A B) : hom A B := + fun (ca: isOpACIAlg2 (projT1 A) (projT2 A)) + (cb: isOpACIAlg2 (projT1 B) (projT2 B)) a => + match (f ca cb a, g ca cb a) with + | (Some b1, Some b2) => Some (projT2 B b1 b2) + | (Some b, None) => Some b + | (None, Some b) => Some b + | _ => None end. + +Definition cimfunQ_zero {A B: sigT (fun A => A -> A -> A)} : hom A B := + fun _ _ _ => None. + +Program Definition cimfunQ_isCIMon (A B: sigT (fun A => A -> A -> A)) : + isOpCIMon2 (hom A B) cimfunQ_comp cimfunQ_zero := + isOpCIMon2.Build _ _ cimfunQ_zero _ _. +Obligation 1. +econstructor. +econstructor. +econstructor. +{- unfold left_id; intros. + unfold cimfunQ_comp; simpl. + eapply functional_extensionality; intro ca. + eapply functional_extensionality; intro cb. + eapply functional_extensionality; intro v. + destruct (x ca cb v); auto. +} +{- unfold right_id; intros. + unfold cimfunQ_comp; simpl. + eapply functional_extensionality; intro ca. + eapply functional_extensionality; intro cb. + eapply functional_extensionality; intro v. + destruct (x ca cb v); auto. +} +econstructor. +{- unfold associative; intros. + unfold cimfunQ_comp; simpl. + eapply functional_extensionality; intro ca. + eapply functional_extensionality; intro cb. + eapply functional_extensionality; intro v. + remember cb as cb1. + destruct cb. + destruct is_op_aalg0. + simpl in addA. + unfold associative in addA. + destruct (x ca cb1 v); simpl; eauto. + {+ destruct (y ca cb1 v); simpl; eauto. + destruct (z ca cb1 v); simpl; eauto. + rewrite addA; auto. + destruct (z ca cb1 v); simpl; eauto. + } + {+ destruct (y ca cb1 v); simpl; eauto. + destruct (z ca cb1 v); simpl; eauto. + destruct (z ca cb1 v); simpl; eauto. + } +} +econstructor. +{- unfold idempotent; intros. + unfold cimfunQ_comp; simpl. + eapply functional_extensionality; intro ca. + eapply functional_extensionality; intro cb. + eapply functional_extensionality; intro v. + remember cb as cb1. + destruct cb. + destruct is_op_ialg0. + unfold idempotent in addI0. + simpl in addI0. + destruct (x ca cb1 v) eqn:K1. + rewrite addI0; auto. + auto. +} +Qed. +Obligation 2. +econstructor. +unfold commutative; intros. +unfold cimfunQ_comp; simpl. +eapply functional_extensionality; intro ca. +eapply functional_extensionality; intro cb. +eapply functional_extensionality; intro v. +remember cb as cb1. +destruct cb. +destruct is_op_calg0. +unfold commutative in addC. +simpl in addC. +destruct (x ca cb1 v); simpl; eauto. +destruct (y ca cb1 v); simpl; eauto. +rewrite addC; auto. +Qed. + +HB.instance Definition cimfunQ_isCIMonoid + (A B: sigT (fun A => A -> A -> A)) : + isOpCIMonoid2 (hom A B) := + isOpCIMonoid2.Build (hom A B) cimfunQ_comp cimfunQ_zero + (cimfunQ_isCIMon A B). + +Elpi Print HB.structure. + + diff --git a/tests/enriched_cat.v b/tests/enriched_cat.v new file mode 100644 index 000000000..641acac05 --- /dev/null +++ b/tests/enriched_cat.v @@ -0,0 +1,156 @@ +(* testing enriched categories *) + +From HB Require Import structures. +From Coq Require Import ssreflect ssrfun. + +HB.mixin Record isQuiver (Obj: Type) : Type := { hom : Obj -> Obj -> Type }. + +HB.structure Definition Quiver : Type := { Obj of isQuiver Obj }. + +HB.mixin Record isMon (A: Type) : Type := { + zero : A; + add : A -> A -> A; + addrA : associative add; + add0r : left_id zero add; + addr0 : right_id zero add; + }. + +HB.structure + Definition Monoid : Type := { A of isMon A }. + +(* original wrapper *) +HB.mixin Record hom_isMon T of Quiver T := + { private : forall A B, isMon (@hom T A B) }. + +(* just an abbreviation with a parameter for homset *) +Definition hom_isMon_ty {T} (H: T -> T -> Type) (A B: T) : + Type := isMon (H A B). + +(* write two versions of Monoid_enriched_quiver: one using hom_isMon +(a mixin, hence a record), the other one using hom_isMon_ty as naked +field type. The former corresponds to the wrapped version, the latter +to the intuitive, wrapper-less version. Now the latter should agree +with the former... (broadly corresponding to 2?) *) + +(* alternative wrapper definition *) +HB.mixin Record hom_isMon1 T of Quiver T := + { private : forall A B, hom_isMon_ty (@hom (Quiver.clone T _)) A B }. + +(* GENERIC WRAPPER instantiated. + abbreviation with parameters for homset and monoid *) +Definition HT_isM (M: Type -> Type) {T} (H: T -> T -> Type) (A B: T) : + Type := M (H A B). + +Lemma wrap_up (M: Type -> Type) {T} (H: T -> T -> Type) (A B: T) + (x: M (H A B)) : HT_isM M H A B. +auto. +Qed. + +Lemma unwrap (M: Type -> Type) {T} (H: T -> T -> Type) (A B: T) + (x: HT_isM M H A B) : M (H A B). +auto. +Qed. + +Lemma wrap_eq (M: Type -> Type) {T} (H: T -> T -> Type) (A B: T) : + M (H A B) = HT_isM M H A B. + auto. +Qed. + +(* GENERIC WRAPPER *) +Definition wrapper (M: Type -> Type) {T} (H: T -> T -> Type) : + Type := forall A B, HT_isM M H A B. + +(* one more wrapper definition (no real change) *) +HB.mixin Record hom_isMon2 T of Quiver T := + { private : wrapper (fun X => isMon X) + (@hom (Quiver.clone T _)) }. + +(* the parametric definition works, though it is problematic *) +HB.mixin Record hom_isM2 (M: Type -> Type) T of Quiver T := + { private : wrapper M (@hom (Quiver.clone T _)) }. + +(* just a copy of hom_isM2 *) +HB.mixin Record hom_isM3 (M: Type -> Type) T of Quiver T := + { private : wrapper M (@hom (Quiver.clone T _)) }. + +(* structure based on one of the wrappers *) +HB.structure Definition Monoid_enriched_quiver := + { Obj of isQuiver Obj & hom_isMon2 Obj }. + +(* structure based on the parametric wrappers *) +HB.structure Definition Monoid_enriched_quiver2 := + { Obj of isQuiver Obj & hom_isM2 (fun X => isMon X) Obj }. + +(* parametric stucture, cannot use hom_isM2 as it has been already used, + but works with a copy (hom_isM3) *) +HB.structure Definition M_enriched_quiver3 (M: Type -> Type) := + { Obj of isQuiver Obj & hom_isM3 M Obj }. + + +(******************) + +(* unique projection from the wrapper *) +HB.instance Definition _ (T : Monoid_enriched_quiver.type) (A B : T) : + isMon (@hom T A B) := @private T A B. + +(* quiver instance (simply typed functions between two types) *) +HB.instance Definition funQ := isQuiver.Build Type (fun A B => A -> B). + +(* prove that for every two types the quiver is a monoid *) +Lemma funQ_isMonF (A B: Type) : isMon (A -> B). +Admitted. + +(* use the lemma to instantiate isMon *) +HB.instance Definition funQ_isMon (A B: Type) : isMon (A -> B) := + funQ_isMonF A B. + +(* use the generic isMon instance to instantiate 'private' *) +HB.instance Definition funQ_hom_isMon := + hom_isMon2.Build Type (fun A B => funQ_isMon A B). + +(* making it work with HB *) +Record Monoid_enriched_quiverN1 := { + ObjN1: Type; + iQ1: isQuiver ObjN1; + hsM1: forall A B, HT_isM (fun X => isMon X) (@hom (HB.pack ObjN1 iQ1)) + A B }. + +(* HB.instance Definition _ := Monoid_enriched_quiver.Build ... *) + +(********************) + +(* without HB *) +Record isQuiverS (Obj: Type) : Type := { homS : Obj -> Obj -> Type }. + +(* structure without wrapper and out of HB, trivially type-checks *) +Structure Monoid_enriched_quiverN := { + ObjN: Type; + iQ: isQuiverS ObjN; + hsM: forall A B, HT_isM (fun X => isMon X) (homS ObjN iQ) + A B }. + + +(*************************************************************) + +(* shows that if a mixin can be decomposed into atomic ones, then its +wrapper can be decompoed into atomic wrappers *) +Lemma hom_isM_ty_split (M1 M2 M3: Type -> Type) : + ((forall X: Type, (M1 X * M2 X) -> M3 X) * + (forall X: Type, M3 X -> (M1 X * M2 X))) + -> + forall (T:Type) (H: T -> T -> Type), + ((forall x1 x2, M1 (H x1 x2)) * (forall x1 x2, M2 (H x1 x2)) -> + (forall x1 x2, M3 (H x1 x2))) * + ((forall x1 x2, M3 (H x1 x2)) -> + (forall x1 x2, M1 (H x1 x2)) * (forall x1 x2, M2 (H x1 x2))). + intros X T H; destruct X as [X1 X2]; split; intro X. + intros x1 x2. + eapply X1; eauto. + destruct X as [X3 X4]. + split; eauto. + + split; intros x1 x2; specialize (X2 (H x1 x2)); + specialize (X x1 x2); intuition. +Qed. + + diff --git a/tests/monoid_enriched_cat.v b/tests/monoid_enriched_cat.v new file mode 100644 index 000000000..c0b511700 --- /dev/null +++ b/tests/monoid_enriched_cat.v @@ -0,0 +1,320 @@ +From HB Require Import structures. +From Coq Require Import ssreflect ssrfun. + +HB.mixin Record isQuiver Obj := { hom : Obj -> Obj -> Type }. + +HB.structure Definition Quiver := { Obj of isQuiver Obj }. + +HB.mixin Record isMon A := { + zero : A; + add : A -> A -> A; + addrA : associative add; + add0r : left_id zero add; + addr0 : right_id zero add; + }. + +HB.structure + Definition Monoid := { A of isMon A }. + +(* This is expected to fail, as it isn't a mixin *) +Fail HB.structure + Definition Monoid_enriched_quiver := + { Obj of isQuiver Obj & + (forall A B : Obj, isMon (@hom (Quiver.clone Obj _) A B)) }. + +(* About zero. + Print zero. +*) +(* Step 0: define a wrapper predicate in coq-elpi *) +(* 5 lines of documentation + 1 line of elpi code in structure.v + `pred wrapper-mixin o:mixinname, o:gref, o:mixinname` +*) +(* Step 1: add a wrapper attribute to declare wrappers, + they should index: + - the wrapped mixin (`isMon`) + - the wrapper mixin (`hom_isMon`) + - the new subject (`hom`) + This attribute will add an entry in the `wrapper-mixin` database. + As an addition substep, we should check that the wrapper has + exactly one field, which is the wrapped mixin. + *) +(* added wrapper attribute in utils.elpi. + added pred wrapper-mixin in structures.v. + added conditional rule for wrapper-mixin in factory.elpi. +*) +#[wrapper] +HB.mixin Record hom_isMon T of Quiver T := + { hom_isMon_private : forall A B, isMon (@hom T A B) }. + +(* Print Canonical Projections. *) +(* About hom_isMon.hom_isMon_private. *) +(* About hom_isMon_private. *) + +(* Step 2: at structure declaration, export the main and only projection + of each declared wrapper as an instance of the wrapped structure on + its subject *) +HB.structure + Definition Monoid_enriched_quiver := + { Obj of isQuiver Obj & hom_isMon Obj }. + +(* About hom_isMon.hom_isMon_private. *) +(* About hom_isMon_private. *) + +(* as expected from step 2, now this instance declaration is no more necessay *) +(* + HB.instance Definition _ (T : Monoid_enriched_quiver.type) (A B : T) : isMon (@hom T A B) := + @hom_isMon_private T A B. +*) +(* each instance of isMon should be tried as an instance of hom_isMon *) +(* + (* Step 3: for each instance of a wrapped mixin on a subject known + to be wrapped, automatically produce an instance of the wrapper mixin too. *) + HB.instance Definition _ := isQuiver.Build Type (fun A B => A -> B). + Fail HB.instance Definition homTypeMon (A B : Quiver.type) := isMon.Build (hom A B) (* ... *). + (* This last command should create a `Monoid_enriched_quiver`, in order to do so it should + automatically instanciate the wrapper `hom_isMon`: + HB.instance Definition _ := hom_isMon.Build Type homTypeMon. + *) +*) + +(* Essentially, step 2 is the elimination rule for the wrapper, step 3 is the introduction one *) + +(* quiver instance (simply typed functions between two types) *) +(* Elpi Trace Browser. *) + +HB.instance Definition funQ := isQuiver.Build Type + (fun A B => A -> option B). + +(* Print Canonical Projections. *) + +(* prove that for every two types the quiver is a monoid *) + +Require Import FunctionalExtensionality. + +Definition funQ_comp {A B} (f g: A -> option B) (x: A) : option B := + match f x with + | Some _ => f x + | _ => g x end. + + (* + Program Definition funQ_isMonF_alt (A B: Type) : isMon (hom A B) := + isMon.Build (A -> option B) (fun (_:A) => None) funQ_comp _ _ _. + Obligations. + Obligation 1. + unfold associative; intros. + eapply functional_extensionality; intro a. + unfold funQ_comp. + destruct (x a) eqn:K1. + simpl; auto. + destruct (y a); auto. + Qed. + Obligation 2. + unfold left_id; intros. + unfold funQ_comp; auto. + Qed. + Obligation 3. + unfold right_id; intros. + eapply functional_extensionality; intro a. + unfold funQ_comp. + destruct (x a); auto. + Qed. +*) + +Program Definition funQ_isMonF (A B: Type) : isMon (A -> option B) := + isMon.Build (A -> option B) (fun (_:A) => None) funQ_comp _ _ _. +(* Obligations. *) +Obligation 1. +unfold associative; intros. +eapply functional_extensionality; intro a. +unfold funQ_comp. +destruct (x a) eqn:K1. +simpl; auto. +destruct (y a); auto. +Qed. +Obligation 2. +unfold left_id; intros. +unfold funQ_comp; auto. +Qed. +Obligation 3. +unfold right_id; intros. +eapply functional_extensionality; intro a. +unfold funQ_comp. +destruct (x a); auto. +Qed. + +(* +Print Canonical Projections. +*) + +(* +Fail Check (nat -> option nat) : Monoid.type. + +Check 1. + +Print Canonical Projections. + +Check 2. +Set Printing All. +*) + +(* use the lemma to instantiate isMon. Notice the genericity of the type. + In principle this instance should be derivable from the wrapper instance. + But since we haven't introduced the wrapper instance yet, we use this + HB command to actually introduce it. *) + +Check Type : Quiver.type. +Fail Check Type : Monoid_enriched_quiver.type. + +HB.instance Definition funQ_isMon (A B: Type) : isMon (hom A B) := + funQ_isMonF A B. + +Check Type : Monoid_enriched_quiver.type. + + + +(* Check (fun A B : Type => hom A B : Monoid.type). *) + +(* instantiate hom_isMon by using the generic isMon instance to define 'private' *) +(* HB.instance Definition funQ_hom_isMon := + hom_isMon.Build Type funQ_isMonF. + *) + +(* Print Canonical Projections. *) + +(* Check (fun A B : Type => hom A B : Monoid.type). *) + +(* HB.about private. *) +(* Print Canonical Projections. *) +(* this has to be changed, it should be something like (hom nat nat): + Check (nat -> option nat) : Monoid.type. *) +(* +HB.about funQ_isMonF. +Fail HB.about funQ_hom_isMon. +About funQ_hom_isMon. +*) + +Elpi Print HB.structure. + + +(**************************************************************) +(* Elpi code moved to factory.elpi *) +(* +Elpi Command x. +Elpi Accumulate File "HB/common/stdpp.elpi". +Elpi Accumulate File "HB/common/database.elpi". +Elpi Accumulate File "HB/common/utils.elpi". +Elpi Accumulate File "HB/status.elpi". +Elpi Accumulate Db hb.db. + +(* extracts isMon *) +Elpi Accumulate lp:{{ + +pred extract_ret_type_name i:term, o:gref. +extract_ret_type_name (prod _ _ TF) Out1 :- + pi p\ + extract_ret_type_name (TF p) Out1. +extract_ret_type_name Ty GR1 :- + Ty = app [global GR0| _], + factory-alias->gref GR0 GR1. + +pred extract_wrapped1 i:indt-decl, o:gref. +extract_wrapped1 (parameter ID _ _ R) Out :- + pi p\ + extract_wrapped1 (R p) Out. +extract_wrapped1 (record ID _ KID (field _ _ Ty (x\end-record))) GR0 :- + extract_ret_type_name Ty GR0. + +}}. +Elpi Typecheck. + +(* extracts hom *) +Elpi Accumulate lp:{{ + +pred extract_inner_type_name i:term, o:gref. +extract_inner_type_name (prod _ _ TF) Out1 :- + pi p\ + extract_inner_type_name (TF p) Out1. +extract_inner_type_name Ty Gr :- + Ty = (app [global _, app [global Gr| _]]). + +pred extract_subject1 i:indt-decl, o:gref. +extract_subject1 (parameter ID _ _ R) Out :- + pi p\ + extract_subject1 (R p) Out. +extract_subject1 (record ID _ KID (field _ _ Ty (x\end-record))) GR0 :- + extract_inner_type_name Ty GR0. + +}}. +Elpi Typecheck. + +(* better version, with predicate parameters *) +Elpi Accumulate lp:{{ + +pred extract_from_record_decl i: (term -> gref -> prop), i:indt-decl, o:gref. +extract_from_record_decl P (parameter ID _ _ R) Out :- + pi p\ + extract_from_record_decl P (R p) Out. +extract_from_record_decl P (record ID _ KID (field _ _ Ty (x\end-record))) GR0 :- + P Ty GR0. + +pred extract_from_rtty i: (term -> gref -> prop), i: term, o:gref. +extract_from_rtty P (prod _ _ TF) Out1 :- + pi p\ + extract_from_rtty P (TF p) Out1. +extract_from_rtty P Ty Gr :- P Ty Gr. + +pred xtr_fst_op i:term, o:gref. +xtr_fst_op Ty Gr1 :- + Ty = (app [global Gr0| _]), + factory-alias->gref Gr0 Gr1. + +pred xtr_snd_op i:term, o:gref. +xtr_snd_op Ty Gr :- + Ty = (app [global _, app [global Gr| _]]). + +pred extract_wrapped i:indt-decl, o:gref. +extract_wrapped In Out :- + extract_from_record_decl (extract_from_rtty xtr_fst_op) In Out. + +pred extract_subject i:indt-decl, o:gref. +extract_subject In Out :- + extract_from_record_decl (extract_from_rtty xtr_snd_op) In Out. + +pred wrapper_mixin_aux i:gref, o:gref, o:gref. +wrapper_mixin_aux XX Gr1 Gr2 :- + XX = (indt I), + coq.env.indt-decl I D, + extract_subject D Gr1, + extract_wrapped D Gr2. + +}}. +Elpi Typecheck. + +(*for debugging - check /tmp/traced.tmp.json with Elpi Tracer *) +(* Elpi Trace Browser. *) +(* Elpi Bound Steps 1000. *) + +(* OK *) +Elpi Query lp:{{ + + coq.locate "hom_isMon.axioms_" XX, + wrapper_mixin_aux XX Gr1 Gr2. + +}}. + +(* also OK *) +Elpi Query lp:{{ + + coq.locate "hom_isMon.axioms_" XX, + XX = (indt I), + coq.env.indt-decl I D, + extract_wrapped1 D GR11, + extract_subject1 D GR12. + +}}. + +Elpi Print HB.structure. + +stop. +*) + diff --git a/tests/monoid_enriched_cat_factory.v b/tests/monoid_enriched_cat_factory.v new file mode 100644 index 000000000..f5374330f --- /dev/null +++ b/tests/monoid_enriched_cat_factory.v @@ -0,0 +1,359 @@ +From HB Require Import structures. +From Coq Require Import ssreflect ssrfun. + +HB.mixin Record isQuiver Obj := { hom : Obj -> Obj -> Type }. + +HB.structure Definition Quiver := { Obj of isQuiver Obj }. + +HB.mixin Record isMon A := { + zero : A; + add : A -> A -> A; + addrA : associative add; + add0r : left_id zero add; + addr0 : right_id zero add; + }. + +HB.structure + Definition Monoid := { A of isMon A }. + +(* This is expected to fail, as it isn't a mixin *) +Fail HB.structure + Definition Monoid_enriched_quiver := + { Obj of isQuiver Obj & + (forall A B : Obj, isMon (@hom (Quiver.clone Obj _) A B)) }. + +(* About zero. + Print zero. +*) +(* Step 0: define a wrapper predicate in coq-elpi *) +(* 5 lines of documentation + 1 line of elpi code in structure.v + `pred wrapper-mixin o:mixinname, o:gref, o:mixinname` +*) +(* Step 1: add a wrapper attribute to declare wrappers, + they should index: + - the wrapped mixin (`isMon`) + - the wrapper mixin (`hom_isMon`) + - the new subject (`hom`) + This attribute will add an entry in the `wrapper-mixin` database. + As an addition substep, we should check that the wrapper has + exactly one field, which is the wrapped mixin. + *) +(* added wrapper attribute in utils.elpi. + added pred wrapper-mixin in structures.v. + added conditional rule for wrapper-mixin in factory.elpi. +*) +#[wrapper] +HB.mixin Record hom_isMon T of Quiver T := + { hom_isMon_private : forall A B, isMon (@hom T A B) }. + +(* Print Canonical Projections. *) +(* About hom_isMon.hom_isMon_private. *) +(* About hom_isMon_private. *) + +(* Step 2: at structure declaration, export the main and only projection + of each declared wrapper as an instance of the wrapped structure on + its subject *) +HB.structure + Definition Monoid_enriched_quiver := + { Obj of isQuiver Obj & hom_isMon Obj }. + +(* + HB.factory Record isMon2 A := + { + zero : A; + add : A -> A -> A; + addrA : associative add; + add0r : left_id zero add; + addr0 : right_id zero add; + foo : A; + }. + HB.builders Context X (f : isMon2 X). + + HB.instance Definition _ : isMon X := isMon.Build X zero add addrA add0r addr0. + + + HB.end. + *) +(* +HB.factory Record isMon2 A of Quiver A := +{ + zero : A; + add : A -> A -> A; + addrA : associative add; + add0r : left_id zero add; + addr0 : right_id zero add; + foo : forall X Y, isMon (@hom A X Y); +}. +HB.builders Context X (f : isMon2 X). + +HB.instance Definition _ : isMon X := isMon.Build X zero add addrA add0r addr0. + +HB.instance Definition _ : hom_isMon X := + hom_isMon.Build X foo. + +HB.end. +*) + + + +(* About hom_isMon.hom_isMon_private. *) +(* About hom_isMon_private. *) + +(* as expected from step 2, now this instance declaration is no more necessay *) +(* + HB.instance Definition _ (T : Monoid_enriched_quiver.type) (A B : T) : isMon (@hom T A B) := + @hom_isMon_private T A B. +*) +(* each instance of isMon should be tried as an instance of hom_isMon *) +(* + (* Step 3: for each instance of a wrapped mixin on a subject known + to be wrapped, automatically produce an instance of the wrapper mixin too. *) + HB.instance Definition _ := isQuiver.Build Type (fun A B => A -> B). + Fail HB.instance Definition homTypeMon (A B : Quiver.type) := isMon.Build (hom A B) (* ... *). + (* This last command should create a `Monoid_enriched_quiver`, in order to do so it should + automatically instanciate the wrapper `hom_isMon`: + HB.instance Definition _ := hom_isMon.Build Type homTypeMon. + *) +*) + +(* Essentially, step 2 is the elimination rule for the wrapper, step 3 is the introduction one *) + +(* quiver instance (simply typed functions between two types) *) +(* Elpi Trace Browser. *) + +HB.instance Definition funQ := isQuiver.Build Type + (fun A B => A -> option B). + +(* Print Canonical Projections. *) + +(* prove that for every two types the quiver is a monoid *) + +Require Import FunctionalExtensionality. + +Definition funQ_comp {A B} (f g: A -> option B) (x: A) : option B := + match f x with + | Some _ => f x + | _ => g x end. + + (* + Program Definition funQ_isMonF_alt (A B: Type) : isMon (hom A B) := + isMon.Build (A -> option B) (fun (_:A) => None) funQ_comp _ _ _. + Obligations. + Obligation 1. + unfold associative; intros. + eapply functional_extensionality; intro a. + unfold funQ_comp. + destruct (x a) eqn:K1. + simpl; auto. + destruct (y a); auto. + Qed. + Obligation 2. + unfold left_id; intros. + unfold funQ_comp; auto. + Qed. + Obligation 3. + unfold right_id; intros. + eapply functional_extensionality; intro a. + unfold funQ_comp. + destruct (x a); auto. + Qed. +*) + +Program Definition funQ_isMonF (A B: Type) : isMon2 (A -> option B) := + isMon2.Build (A -> option B) (fun (_:A) => None) funQ_comp _ _ _ (fun (_:A) => None). +(* Obligations. *) +Obligation 1. +unfold associative; intros. +eapply functional_extensionality; intro a. +unfold funQ_comp. +destruct (x a) eqn:K1. +simpl; auto. +destruct (y a); auto. +Qed. +Obligation 2. +unfold left_id; intros. +unfold funQ_comp; auto. +Qed. +Obligation 3. +unfold right_id; intros. +eapply functional_extensionality; intro a. +unfold funQ_comp. +destruct (x a); auto. +Qed. + +(* +Print Canonical Projections. +*) + +(* +Fail Check (nat -> option nat) : Monoid.type. + +Check 1. + +Print Canonical Projections. + +Check 2. +Set Printing All. +*) + +(* use the lemma to instantiate isMon. Notice the genericity of the type. + In principle this instance should be derivable from the wrapper instance. + But since we haven't introduced the wrapper instance yet, we use this + HB command to actually introduce it. *) + +Check Type : Quiver.type. +Fail Check Type : Monoid_enriched_quiver.type. + +HB.instance Definition funQ_isMon (A B: Type) : isMon2 (hom A B) := + funQ_isMonF A B. + +Check Type : Monoid_enriched_quiver.type. + + + +(* Check (fun A B : Type => hom A B : Monoid.type). *) + +(* instantiate hom_isMon by using the generic isMon instance to define 'private' *) +(* HB.instance Definition funQ_hom_isMon := + hom_isMon.Build Type funQ_isMonF. + *) + +(* Print Canonical Projections. *) + +(* Check (fun A B : Type => hom A B : Monoid.type). *) + +(* HB.about private. *) +(* Print Canonical Projections. *) +(* this has to be changed, it should be something like (hom nat nat): + Check (nat -> option nat) : Monoid.type. *) +(* +HB.about funQ_isMonF. +Fail HB.about funQ_hom_isMon. +About funQ_hom_isMon. +*) + +Elpi Print HB.structure. + + +(**************************************************************) +(* Elpi code moved to factory.elpi *) +(* +Elpi Command x. +Elpi Accumulate File "HB/common/stdpp.elpi". +Elpi Accumulate File "HB/common/database.elpi". +Elpi Accumulate File "HB/common/utils.elpi". +Elpi Accumulate File "HB/status.elpi". +Elpi Accumulate Db hb.db. + +(* extracts isMon *) +Elpi Accumulate lp:{{ + +pred extract_ret_type_name i:term, o:gref. +extract_ret_type_name (prod _ _ TF) Out1 :- + pi p\ + extract_ret_type_name (TF p) Out1. +extract_ret_type_name Ty GR1 :- + Ty = app [global GR0| _], + factory-alias->gref GR0 GR1. + +pred extract_wrapped1 i:indt-decl, o:gref. +extract_wrapped1 (parameter ID _ _ R) Out :- + pi p\ + extract_wrapped1 (R p) Out. +extract_wrapped1 (record ID _ KID (field _ _ Ty (x\end-record))) GR0 :- + extract_ret_type_name Ty GR0. + +}}. +Elpi Typecheck. + +(* extracts hom *) +Elpi Accumulate lp:{{ + +pred extract_inner_type_name i:term, o:gref. +extract_inner_type_name (prod _ _ TF) Out1 :- + pi p\ + extract_inner_type_name (TF p) Out1. +extract_inner_type_name Ty Gr :- + Ty = (app [global _, app [global Gr| _]]). + +pred extract_subject1 i:indt-decl, o:gref. +extract_subject1 (parameter ID _ _ R) Out :- + pi p\ + extract_subject1 (R p) Out. +extract_subject1 (record ID _ KID (field _ _ Ty (x\end-record))) GR0 :- + extract_inner_type_name Ty GR0. + +}}. +Elpi Typecheck. + +(* better version, with predicate parameters *) +Elpi Accumulate lp:{{ + +pred extract_from_record_decl i: (term -> gref -> prop), i:indt-decl, o:gref. +extract_from_record_decl P (parameter ID _ _ R) Out :- + pi p\ + extract_from_record_decl P (R p) Out. +extract_from_record_decl P (record ID _ KID (field _ _ Ty (x\end-record))) GR0 :- + P Ty GR0. + +pred extract_from_rtty i: (term -> gref -> prop), i: term, o:gref. +extract_from_rtty P (prod _ _ TF) Out1 :- + pi p\ + extract_from_rtty P (TF p) Out1. +extract_from_rtty P Ty Gr :- P Ty Gr. + +pred xtr_fst_op i:term, o:gref. +xtr_fst_op Ty Gr1 :- + Ty = (app [global Gr0| _]), + factory-alias->gref Gr0 Gr1. + +pred xtr_snd_op i:term, o:gref. +xtr_snd_op Ty Gr :- + Ty = (app [global _, app [global Gr| _]]). + +pred extract_wrapped i:indt-decl, o:gref. +extract_wrapped In Out :- + extract_from_record_decl (extract_from_rtty xtr_fst_op) In Out. + +pred extract_subject i:indt-decl, o:gref. +extract_subject In Out :- + extract_from_record_decl (extract_from_rtty xtr_snd_op) In Out. + +pred wrapper_mixin_aux i:gref, o:gref, o:gref. +wrapper_mixin_aux XX Gr1 Gr2 :- + XX = (indt I), + coq.env.indt-decl I D, + extract_subject D Gr1, + extract_wrapped D Gr2. + +}}. +Elpi Typecheck. + +(*for debugging - check /tmp/traced.tmp.json with Elpi Tracer *) +(* Elpi Trace Browser. *) +(* Elpi Bound Steps 1000. *) + +(* OK *) +Elpi Query lp:{{ + + coq.locate "hom_isMon.axioms_" XX, + wrapper_mixin_aux XX Gr1 Gr2. + +}}. + +(* also OK *) +Elpi Query lp:{{ + + coq.locate "hom_isMon.axioms_" XX, + XX = (indt I), + coq.env.indt-decl I D, + extract_wrapped1 D GR11, + extract_subject1 D GR12. + +}}. + +Elpi Print HB.structure. + +stop. +*) + diff --git a/tests/monoid_law_structure.v b/tests/monoid_law_structure.v new file mode 100644 index 000000000..b78f06c69 --- /dev/null +++ b/tests/monoid_law_structure.v @@ -0,0 +1,18 @@ +From HB Require Import structures. + +HB.mixin Record isMonLaw T (e : T) (op : T -> T -> T) := { + opmA : forall a b c, op (op a b) c = op a (op b c); + op1m : forall x, op e x = x; + opm1 : forall x, op x e = x; +}. + +HB.structure Definition MonLaw T e := { op of isMonLaw T e op }. + +HB.mixin Record isPreMonoid T := { + zero : T; + add : T -> T -> T; +}. +HB.structure Definition PreMonoid := { T of isPreMonoid T }. + +HB.structure Definition Monoid := + { T of isPreMonoid T & isMonLaw T zero add }. diff --git a/tests/monoid_law_structure_clone.v b/tests/monoid_law_structure_clone.v new file mode 100644 index 000000000..5df341567 --- /dev/null +++ b/tests/monoid_law_structure_clone.v @@ -0,0 +1,19 @@ +From HB Require Import structures. + +HB.mixin Record isMonLaw T (e : T) (op : T -> T -> T) := { + opmA : forall a b c, op (op a b) c = op a (op b c); + op1m : forall x, op e x = x; + opm1 : forall x, op x e = x; +}. + +HB.structure Definition MonLaw T e := { op of isMonLaw T e op }. + +HB.mixin Record isPreMonoid T := { + zero : T; + add : T -> T -> T; +}. +HB.structure Definition PreMonoid := { T of isPreMonoid T }. + +HB.structure Definition Monoid := + { T of isPreMonoid T & + isMonLaw T (@zero (PreMonoid.clone T _)) (@add (PreMonoid.clone T _)) }.