From 17784b939e0384c1efec77f8f1c501b4a9c54412 Mon Sep 17 00:00:00 2001 From: Thomas Date: Tue, 7 Feb 2023 13:02:19 +0100 Subject: [PATCH 1/2] HB.saturate: saturating instances on new structure declaration MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit When a new structure `S` is created it may be the case that some type which is already equipped with some mixins is an instance of `S`, but was not declared as such since `S` was not declared yet. Similarly, mixin instances which have parameters may not be available on a single type until there is a structure for the parameter which is rich enough. We store in the predicate `has-mixin-instance` the list of types which have mixin instances, so that we can reconsider them later. Out of these we craft `mixin-src` clauses (used by `HB/common/inference.elpi`) which have premises using Coq's unifyer (which in turn can compute the smallest structure having all requirements thanks to the hints we declare on joins). Example: When such an instance is declared: ```coq HB.instance Definition I1 (X:t1) : mixin1 (list X) := ... . ``` a clause of this form is generated: ```coq has-mixin-instance (cs-gref (indt «list»)) (indt «mixin1.axioms_») (const «I1») ``` When `HB.saturate` is called, we generate conditional `mixin-src` clauses with conditions on parameters (via the function `has-mixin-instance->mixin-src`). Then for each type constructor mentioned in a `has-mixin-src` clause we try to declare new instances with the new clauses via `declare-all-on-type-constructor`. Unresolved parameters are abstracted out. Their type is the smallest structure which can satisfy all the constraints coming from single mixins. --- .gitignore | 1 + HB/common/database.elpi | 107 +++++++++++++++++- HB/common/stdpp.elpi | 6 + HB/common/utils.elpi | 2 +- HB/context.elpi | 2 +- HB/factory.elpi | 3 +- HB/instance.elpi | 121 +++++++++++++++++---- HB/structure.elpi | 15 ++- _CoqProject | 6 +- _CoqProject.test-suite | 11 ++ instance.md | 73 +++++++++++++ structures.v | 41 ++++++- tests/instance_before_structure.v | 37 +++++++ tests/instance_merge.v | 20 ++++ tests/instance_merge_with_distinct_param.v | 43 ++++++++ tests/instance_params_no_type.v | 40 ++++++- tests/two_hier.v | 72 ++++++++++++ tests/unit/close_hole_term.v | 29 +++++ tests/unit/enrich_type.v | 27 +++++ tests/unit/mixin_src_has_mixin_instance.v | 30 +++++ tests/unit/mk_src_map.v | 26 +++++ tests/unit/struct.v | 36 ++++++ 22 files changed, 713 insertions(+), 35 deletions(-) create mode 100644 instance.md create mode 100644 tests/instance_before_structure.v create mode 100644 tests/instance_merge.v create mode 100644 tests/instance_merge_with_distinct_param.v create mode 100644 tests/two_hier.v create mode 100644 tests/unit/close_hole_term.v create mode 100644 tests/unit/enrich_type.v create mode 100644 tests/unit/mixin_src_has_mixin_instance.v create mode 100644 tests/unit/mk_src_map.v create mode 100644 tests/unit/struct.v diff --git a/.gitignore b/.gitignore index 80a4d7d4e..554a47d4b 100644 --- a/.gitignore +++ b/.gitignore @@ -58,3 +58,4 @@ _minted-* *.vtc *.dot +*.json diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 05182bafa..22b1a8740 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -1,7 +1,7 @@ /* Hierarchy Builder: algebraic hierarchies made easy This software is released under the terms of the MIT license */ -shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }. +shorten coq.{ term->gref, term-is-gref?, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }. %%%%%%%%% HB database %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -14,6 +14,13 @@ from_mixin (from _ X _) X. pred from_builder i:prop, o:term. from_builder (from _ _ X) (global X). +% for a given clause mixin-src with eventually a condition, +% returns the type of the first argument +pred mixin-src-w-cond_type i:prop, o:term. +mixin-src-w-cond_type(mixin-src (global G) _ _ :- _) (global G). +mixin-src-w-cond_type (mixin-src (app [T|_]) _ _ :- _) T. +mixin-src-w-cond_type (pi x \ (C x)) T :- pi y \ mixin-src-w-cond_type (C y) T. + pred mixin-src_mixin i:prop, o:mixinname. mixin-src_mixin (mixin-src _ M _) M. @@ -133,6 +140,23 @@ factories-provide FLwP MLwP :- std.do! [ w-params.map UnsortedMLwP (p\t\ toposort-mixins) MLwP, ]. +pred undup-grefs i:list gref, o:list gref. +undup-grefs L UL :- std.do! [ + coq.gref.list->set L S, + coq.gref.set.elements S UL, +]. + +% remove duplicates from a list of terms, but all the terms have to be global references +pred undup-terms i:list term, o:list term. +undup-terms L UL :- std.do! [ + std.map L coq.term->gref LG, + undup-grefs LG ULG, + std.map ULG (coq.env.global ) UL, +]. + + + + % Mixins can be topologically sorted according to their dependencies pred toposort-mixins i:list (w-args mixinname), o:list (w-args mixinname). toposort-mixins In Out :- std.do! [ @@ -192,10 +216,14 @@ findall-builders LFIL :- std.map {std.findall (builder-decl B_)} extract-builder LFILunsorted, std.bubblesort LFILunsorted leq-builder LFIL. +pred findall-has-mixin-instance o:list prop. +findall-has-mixin-instance CL :- + std.findall (has-mixin-instance _ _ _) CL. + pred findall-mixin-src i:term, o:list mixinname. findall-mixin-src T ML :- std.map {std.findall (mixin-src T M_ V_)} mixin-src_mixin ML. - + pred findall-local-canonical o:list constant. findall-local-canonical CL :- std.map {std.findall (local-canonical C_)} local-canonical-gref CL. @@ -272,6 +300,7 @@ assert-good-coverage! MLSortedRev CNL :- std.do! [ true ]. + %%%%% Coq Database %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % [get-structure-coercion S1 S2 F] finds the coecion F from the structure S1 to S2 @@ -299,7 +328,7 @@ get-constructor (indt R) (indc K) :- !, if (coq.env.indt R _ _ _ _ [K] _) true (coq.error "Not a record" R). get-constructor I _ :- coq.error "get-constructor: not an inductive" I. -%% finding for locally defined structures +% finding for locally defined structures pred get-cs-structure i:cs-instance, o:structure. get-cs-structure (cs-instance _ _ (const Inst)) Struct :- std.do! [ coq.env.typeof (const Inst) InstTy, @@ -313,6 +342,78 @@ get-cs-instance (cs-instance _ _ (const Inst)) Inst. pred has-cs-instance i:gref, i:cs-instance. has-cs-instance GTy (cs-instance _ (cs-gref GTy) _). + +pred mixin-src->has-mixin-instance i:prop, o:prop. +mixin-src->has-mixin-instance (mixin-src (global GR) M I) (has-mixin-instance (cs-gref GR) M IHd) :- + term->gref I IHd. + +mixin-src->has-mixin-instance (mixin-src (app [global GR|_] ) M I) (has-mixin-instance (cs-gref GR) M IHd) :- + term->gref I IHd. + +mixin-src->has-mixin-instance (mixin-src (prod _ _ _ ) M I) (has-mixin-instance cs-prod M IHd):- + term->gref I IHd. + +mixin-src->has-mixin-instance (mixin-src (sort U) M I) (has-mixin-instance (cs-sort U) M IHd):- + term->gref I IHd. + +% this auxiliary function iterates over the list of arguments of an application, +% and create the necessary unify condition for each arguments +% and at the end returns the mixin-src clause with all the conditions +pred mk-src-aux + i:list term, % list of arguments + i:term, % head of the original application + i:mixinname, % name of mixin + i:term, % instance body + i:list prop, % Cond list + o:prop. +mk-src-aux [] T M I Cond (mixin-src T M I :- Cond). +mk-src-aux [A|Args] T M I Cond (pi a \ C a) :- + pi a \ + sigma Ta\ + coq.mk-app T [a] Ta, + mk-src-aux Args Ta M I [coq.unify-eq A a ok|Cond] (C a). + + +% transforms the has-mixin-instance clause arguments into a +% mixin-src clause with eventuals conditions regarding its parameters +pred mk-src + i:term, % type of the instance Ty + i:mixinname, % name of mixin + i:term, % instance body I of type Ty + i:list prop, % Cond list + o:prop. + +mk-src (app [_|Args]) M I Cond C :- + std.last Args Last, + safe-dest-app Last Hd ArgsLast, + mk-src-aux ArgsLast Hd M I Cond C. + +mk-src (prod N_ _ F) M I Cond (pi a \ C a) :- + pi a\ + sigma Ia \ + coq.mk-app I [a] Ia, + mk-src (F a) M Ia Cond (C a). + + +% for a type T, create as many holes as there are foralls and returns that enriched type +pred enrich-type i:term, o:term . +enrich-type T ET :- + coq.typecheck T TH ok, + coq.count-prods TH N, + if (N = 0) (ET = T) (coq.mk-app T {coq.mk-n-holes N} ET). + +% wrapper for mk-src so it can be called by a map on a list of clauses has-mixin-instance +pred mk-src-map i:prop, o:prop. +mk-src-map (has-mixin-instance _ M IHd) C :- std.do![ + T = global IHd, + coq.env.typeof IHd Ty, + mk-src Ty M T [] C, + ]. + +pred cs-pattern->term i:cs-pattern, o:term. +cs-pattern->term (cs-gref GR) (global GR). +cs-pattern->term (cs-sort U) (sort U). + pred term->cs-pattern i:term, o:cs-pattern. term->cs-pattern (prod _ _ _) cs-prod. term->cs-pattern (sort U) (cs-sort U). diff --git a/HB/common/stdpp.elpi b/HB/common/stdpp.elpi index cd1ffaa4d..85366b424 100644 --- a/HB/common/stdpp.elpi +++ b/HB/common/stdpp.elpi @@ -123,6 +123,12 @@ pred coq.env.current-library o:string. coq.env.current-library L :- loc.fields {get-option "elpi.loc"} L _ _ _ _. coq.env.current-library "dummy.v". +pred coq.term-is-gref? i:term, o:gref. +coq.term-is-gref? (global GR) GR :- !. +coq.term-is-gref? (pglobal GR _) GR :- !. +coq.term-is-gref? (app [Hd|_]) GR :- !, coq.term-is-gref? Hd GR. +coq.term-is-gref? (let _ _ T x\x) GR :- !, coq.term-is-gref? T GR. + pred coq.prod-tgt->gref i:term, o:gref. coq.prod-tgt->gref T GR :- whd1 T T1, !, coq.prod-tgt->gref T1 GR. coq.prod-tgt->gref (prod N Src Tgt) GR :- !, @pi-decl N Src x\ coq.prod-tgt->gref (Tgt x) GR. diff --git a/HB/common/utils.elpi b/HB/common/utils.elpi index 3f94a7ed0..fcd66647c 100644 --- a/HB/common/utils.elpi +++ b/HB/common/utils.elpi @@ -374,4 +374,4 @@ prod-last X X :- !. pred prod-last-gref i:term, o:gref. 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. \ No newline at end of file +prod-last-gref X GR :- coq.term->gref X GR. diff --git a/HB/context.elpi b/HB/context.elpi index 4b04e5f0b..d7fd4d5e6 100644 --- a/HB/context.elpi +++ b/HB/context.elpi @@ -73,7 +73,7 @@ postulate-mixin TheType (triple M Ps T) (triple CL MSL MLwP) (triple OutCL [MC|M MC = mixin-src T M (global (const C)), MC => get-option "local" tt => - instance.declare-all TheType {findall-classes-for [M]} NewCSL, + instance.declare-all-generic-type TheType {findall-classes-for [M]} NewCSL, std.map NewCSL snd NewCL, std.append CL NewCL OutCL ]. diff --git a/HB/factory.elpi b/HB/factory.elpi index 6fe74186e..8ff726654 100644 --- a/HB/factory.elpi +++ b/HB/factory.elpi @@ -53,7 +53,7 @@ argument->w-mixins (ctx-decl Decl) (pr MLwP ArgwP) :- !, std.do! [ pred argument-name i:argument, o:string. argument-name (const-decl Id _ _) Id :- !. argument-name (indt-decl (parameter _ _ _ R)) Id :- !, - argument-name (indt-decl (R (sort prop))) Id. +argument-name (indt-decl (R (sort prop))) Id. argument-name (indt-decl (record Id _ _ _)) Id :- !. argument-name (indt-decl (inductive Id _ _ _)) Id :- !. argument-name (ctx-decl _) "_" :- !. @@ -231,7 +231,6 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-indt-decl RDecl RDeclClosed _, - % coq.say RDecl RDeclClosed, if (get-option "primitive" tt) (@primitive! => log.coq.env.add-indt RDeclClosed R) diff --git a/HB/instance.elpi b/HB/instance.elpi index 0b793248c..f48f56b33 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -15,7 +15,7 @@ declare-existing T0 F0 :- std.do! [ "The type of the instance is not a factory", factory-alias->gref FactoryAlias Factory, private.declare-instance Factory T F Clauses _, - acc-clauses current Clauses + acc-clauses current Clauses, ]. % [declare-const N B Ty] adds a Definition N : Ty := B where Ty is a factory @@ -37,7 +37,7 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [ ) ( SectionName is "hb_instance_" ^ {std.any->string {new_int}}, log.coq.env.begin-section SectionName, - private.postulate-arity TyWP [] Body SectionBody SectionTy + private.postulate-arity TyWP [] Body SectionBody SectionTy ), % identify the factory @@ -76,8 +76,47 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [ % we accumulate clauses now that the section is over acc-clauses current Clauses + + +]. + +% we add a new constructor to terms to represent terms to be abstracted +type abs int -> term. + +% bind back abstracted subterms +pred bind i:int, i:int, i:term, o:term. +bind I M T T1 :- M > I, + T1 = {{ fun x => lp:(B x) }}, + N is I + 1, + pi x\ % we allocate the fresh symbol for (abs M) + (copy (abs N) x :- !) => % we schedule the replacement (abs M) -> x + bind N M T (B x). +bind M M T T1 :- copy T T1. % we perform all the replacements + +% for a term with M holes, returns a term with M variables to fill these holes +% the clause see is only generated for a term if it hasn't been seen before +% the term might need to be typechecked first or close-hole-term generates extra holes for the +% type of the parameters +pred close-hole-term i:term, o:term. +close-hole-term T1 T3 :- std.do! [ + (pi T Ty N N' M \ fold-map T N (abs M) M :- var T, not (seen T _), !, coq.typecheck T Ty ok, fold-map Ty N _ N', M is N' + 1, see T M) => + (pi T N M \ fold-map T N (abs M) N :- var T, seen T M, !) => + fold-map T1 0 T2 M, + bind 0 M T2 T3, ]. + +pred seen i:term, o:int. +seen X Y :- declare_constraint (seen X Y) [X]. + +pred see i:term, o:int. +see X Y :- declare_constraint (see X Y) [X]. + +constraint seen see { +rule (see X N) \ (seen X M) <=> (M = N). +rule \ (seen X _) <=> false. +} + % [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 % for which all the dependencies (mixins) were postulated so far and skips the @@ -86,6 +125,35 @@ 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] :- + + infer-class T Class Struct MLwP S Name STy Clauses, + + decl-const-in-struct Name S STy CS, + + Clauses => declare-all T Rest L. + +declare-all T [_|Rest] L :- declare-all T Rest L. +declare-all _ [] []. + +% 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-generic-type i:term, i:list class, o:list (pair id constant). +declare-all-generic-type T [class Class Struct MLwP|Rest] [pr Name CS|L] :- + + enrich-type T Ty, + infer-class Ty Class Struct MLwP S Name _STy Clauses, + close-hole-term S SC, + std.assert-ok! (coq.typecheck SC SCTy) "badly closed", + decl-const-in-struct Name SC SCTy CS, + + Clauses => declare-all-generic-type T Rest L. + +declare-all-generic-type T [_|Rest] L :- declare-all-generic-type T Rest L. +declare-all-generic-type _ [] []. + +pred infer-class i:term, i:classname, i:gref, i:factories, o:term, o:string, o:term, o:list prop. +infer-class T Class Struct MLwP S Name STy Clauses:- std.do![ + if (not(has-CS-instance? T Struct)) true % we build it (if-verbose (coq.say {header} "skipping already existing" @@ -101,30 +169,29 @@ declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :- {coq.term->string T})) fail, - !, - Name is {cs-pattern->name {term->cs-pattern T}} ^ "__canonical__" ^ {gref->modname Struct 2 "_" }, if-verbose (coq.say {header} "declare canonical structure instance" Name), + get-constructor Struct KS, coq.safe-dest-app T THD _, private.optimize-class-body THD {std.length Params} KCApp KCAppNames Clauses, coq.mk-app (global KS) {std.append Params [T, KCAppNames]} S, if-verbose (coq.say {header} "structure instance for" Name "is" {coq.term->string S}), - std.assert-ok! (coq.typecheck S STy) "declare-all: S illtyped", + std.assert-ok! (coq.typecheck S STy) "infer1: S illtyped", +]. + +pred decl-const-in-struct i:string, i:term, i:term, i:constant. +decl-const-in-struct Name S STy CS:- std.do![ log.coq.env.add-const-noimplicits Name S STy @transparent! CS, % Bug coq/coq#11155, could be a Let with-locality (log.coq.CS.declare-instance CS), % Bug coq/coq#11155, should be local - acc-clause current (local-canonical CS), - if-verbose (coq.say {header} "structure instance" Name "declared"), +]. - Clauses => declare-all T Rest L. -declare-all T [_|Rest] L :- declare-all T Rest L. -declare-all _ [] []. pred declare-factory-sort-deps i:gref. declare-factory-sort-deps GR :- std.do! [ @@ -172,7 +239,7 @@ mk-factory-sort-deps AliasGR CSL :- std.do! [ KFSortMSL, KFSortMSL => synthesis.under-mixin-src-from-factory.do! KFSort GCF - [declare-all KFSort {findall-classes-for ML} CSL] + [declare-all-generic-type KFSort {findall-classes-for ML} CSL] ]. pred mk-factory-sort-factory i:gref, o:list (pair id constant). @@ -189,6 +256,19 @@ mk-factory-sort-factory AliasGR CSL :- std.do! [ declare-const "_" GCF (arity FGCF) CSL ]. +% create instances for all possible combinations of types and structure compatible +pred saturate-instances. +saturate-instances :- std.do! [ + findall-has-mixin-instance ClausesHas, + std.map ClausesHas mk-src-map Clauses, + std.map-filter Clauses mixin-src-w-cond_type TLD, + undup-terms TLD TL, + findall-classes Classes, + Clauses => std.forall TL (t\ (declare-all-generic-type t Classes _)), +]. + + + /* ------------------------------------------------------------------------- */ /* ----------------------------- private code ------------------------------ */ /* ------------------------------------------------------------------------- */ @@ -208,11 +288,12 @@ 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 :- - declare-canonical-instances-from-factory Factory T F CSL, + declare-canonical-instances-from-factory Factory T F Clauses1 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 = []). + std.map CSL (x\r\ sigma i c\ x = pr i c, r = instance-to-export File i c) Clauses2) + (Clauses2 = []), + std.append Clauses1 Clauses2 Clauses. % [add-mixin T F _ M Cl] adds a constant being the mixin instance for M on type % T built from factory F @@ -271,6 +352,7 @@ postulate-arity (arity Ty) ArgsRev X T Ty :- hd-beta X {std.rev ArgsRev} X1 Stack1, unwind X1 Stack1 T. + % We find the new mixins that F build, we build them and shedule them % for becoming builders at section closing time. We also declare % all canonical instances these new mixins allow for, so that the user @@ -284,7 +366,7 @@ declare-canonical-instances-from-factory-and-local-builders 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, + Clauses => declare-all-generic-type T {findall-classes-for ML} CCSL, std.append MCSL CCSL CSL ]. @@ -292,8 +374,8 @@ declare-canonical-instances-from-factory-and-local-builders % 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! [ + i:factoryname, i:term, i:term, o: list prop, o:list (pair id constant). +declare-canonical-instances-from-factory Factory T F ClausesHas CSL :- 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 @@ -301,8 +383,9 @@ 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, + add-all-mixins T Factory ML tt Clauses MCSL, + std.map-filter Clauses (mixin-src->has-mixin-instance ) ClausesHas, + ClausesHas => declare-all T {findall-classes-for ML} CCSL, % declare-all-generic-type doesn't work here ] ], std.append MCSL CCSL CSL diff --git a/HB/structure.elpi b/HB/structure.elpi index 2fd1132d4..13b0ad59b 100644 --- a/HB/structure.elpi +++ b/HB/structure.elpi @@ -187,7 +187,10 @@ declare Module BSkel Sort :- std.do! [ NewClauses => factory.declare-abbrev Module (factory.by-classname ClassName), NewClauses => if-MC-compat (private.mc-compat-structure Module ModulePath MLToExport - {w-params.nparams MLwP} ClassProjection GRPack) + {w-params.nparams MLwP} ClassProjection GRPack), + + NewClauses => instance.saturate-instances, + ]. /* ------------------------------------------------------------------------- */ @@ -331,6 +334,9 @@ mk-coe-structure-body StructureF StructureT TC Coercion SortProjection ClassProj lp:PackPH (lp:SortP s) (lp:CoercionP (lp:SortP s) (lp:ClassP s)) }}, ]. +pred std.error-and-fail i:(diagnostic -> prop), i:string. +std.error-and-fail P M :- P D, if (D = error X) (coq.error M X, fail) true. + % [declare-coercion P1 P2 C1 C2] declares a structure and a class coercion % from C1 to C2 given P1 P2 the two projections from the structure of C1 pred declare-coercion i:term, i:term, i:class, i:class. @@ -346,8 +352,8 @@ declare-coercion SortProjection ClassProjection w-params.then FMLwP mk-fun mk-fun (mk-coe-class-body FC TC TMLwP) CoeBody, - - std.assert-ok! (coq.elaborate-skeleton CoeBody Ty CoeBody') "declare-coercion: CoeBody illtyped", + ErrorMessage is "The structures " ^ ModNameF ^ " and " ^ ModNameT ^ " are incompatible: the coercion between them cannot be synthesized", + std.error-and-fail (coq.elaborate-skeleton CoeBody Ty CoeBody') ErrorMessage, if-verbose (coq.say {header} "declare coercion hint" CName), @@ -359,7 +365,8 @@ declare-coercion SortProjection ClassProjection (mk-coe-structure-body StructureF StructureT TC Coercion SortProjection ClassProjection) SCoeBody, - std.assert-ok! (coq.elaborate-skeleton SCoeBody STy SCoeBody') "declare-coercion: SCoeBody illtyped", + ErrorMessage is "The structures " ^ ModNameF ^ " and " ^ ModNameT ^ " are incompatible: the coercion between them cannot be synthesized", + std.error-and-fail (coq.elaborate-skeleton SCoeBody STy SCoeBody') ErrorMessage, if-verbose (coq.say {header} "declare unification hint" SName), diff --git a/_CoqProject b/_CoqProject index b8cf8cf7e..057e90014 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,3 +1,7 @@ structures.v -arg -w -arg -elpi.accumulate-syntax --Q . HB \ No newline at end of file +-arg -w -arg +elpi.typecheck +-Q . HB + +-R tests HB.tests +-R examples HB.examples \ No newline at end of file diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite index 98c20167e..f806edf89 100644 --- a/_CoqProject.test-suite +++ b/_CoqProject.test-suite @@ -3,6 +3,7 @@ -arg -w -arg -abstract-large-number -arg -w -arg -disj-pattern-notation -arg -w -arg -notation-overridden +-arg -w -arg +elpi.typecheck examples/readme.v examples/hulk.v @@ -72,6 +73,7 @@ tests/not_same_key.v tests/hb_pack.v tests/declare.v tests/short.v +tests/instance_before_structure.v tests/primitive_records.v tests/non_forgetful_inheritance.v tests/fix_loop.v @@ -80,6 +82,15 @@ tests/hnf.v tests/fun_instance.v tests/issue284.v tests/issue287.v +tests/instance_merge_with_distinct_param.v +tests/instance_merge.v +tests/two_hier.v + +tests/unit/enrich_type.v +tests/unit/mixin_src_has_mixin_instance.v +tests/unit/mk_src_map.v +tests/unit/close_hole_term.v +tests/unit/struct.v -R tests HB.tests -R examples HB.examples diff --git a/instance.md b/instance.md new file mode 100644 index 000000000..9ad34ff91 --- /dev/null +++ b/instance.md @@ -0,0 +1,73 @@ + Saturating instances on new structure declaration + +When a new structure S_new is created, the instances of factories that the new structure implements are not recorded in the database, instead they are in the coq databse. We want to get the list of factories attached to S_new and create properly the instances that implements those factories with the new structure. + +See the test file tests/instance_before_structure.v for an example + +functions get-canonical-instances and get canonical-structures let us interact with the coq database + +```coq +1. has-mixin-instance CS-pattern mixinname inst. +2. mixin-src {{list lp:X}} {{hasmx}} {{i: eq I}} :- coq unification X eqType I (with X = sort I) +3. has-struct-instance CS-KEY class. +``` + +To create the list of booleans we need to have the section paramaters from the instance definition passed down through the clauses, so the information is saved in the database. + +- This list of booleans is created by sect-params-in-term which given a list of section parameters SP and a term T, returns a list of boolean corresponding to whether or not a parameter in SP appears in T. + +- This information is crucial in creating the right clauses to saturate the right instances later. + +We'll also need later to add parameters from user-created section by interrogating the coq database. + + +Hierarchy builder is supposed to find links within the hierarchy of structures and instances (joins betweens elements). + + +Let's say we have an instance I1 for the structure S1 verifying a mixin M1 and similarly I2, S2, and M2. +If we were to introduce a structure S3 which needs a type verifying both M1 and M2 for a type T compatible with I1 and I2, an instance for S3 and T should be generated automatically, and not only upon encountering a new instance. + +So order matters greatly as a new structure wouldn't know about all the previously defined instances, until a new instace is created. + +--- + +Saturating instances works on instances with parameters this way : + +1. When an instance is created by the user, some clauses of the form mixin-src are created for each mixin instance successfully created. + Such a clause has the form + ```prolog + mixin-src Ty, M, I. + ``` + + where I can be used to reconstruct an instance of M Ty. + + Those clauses were used to then infer new structures. +But we need more information kept in the database. +For each of those clauses, we now store instead a new clause `has-mixin-instance` generated by the translation predicate +`mixin-src->has-mixin-instance`. + + The clauses `has-mixin-instance` still link some concrete instance with the mixins it satisfies but now instead of storing the type of the instance which is too restrictive, we store the canonical structure pattern which allows to be more generic. + + Now when such an instance is declared : + ```coq + HB.instance Definition I1 (X:t1) : mixin1 (list X) := ... . + ``` + a clause of this form is generated + ```coq + has-mixin-instance (cs-gref (indt «list»)) (indt «mixin1.axioms_») (const «I1») + ``` + +2. When a structure S is declared, we want to try to populate it with types already encountered at step 1, which wasn't done before. + + To do so, at the end of a structure declaration, we call a function `saturate-instances`. + We need parametrised `mixin-src` clauses with conditions on parameters. For this we call `mk-src-map` which takes the `has-mixin-instance` and creates the right `mixin-src` clauses. + + Then for each type at the head of the clauses, we try to declare new instances with the new clauses at our disposal with the function `declare-all-generic-type`. + + This function preprocesses the type with `enrich_type` which takes a term, and for each forall quantifiers in it, applies as many holes as necessary. + + Then the function `infer_1` is called which actually tries to create an instance on that enriched type. If it is succesful we need to close the term we got with elpi quantifiers and save the instance in the coq database with `save_1`. + + + + diff --git a/structures.v b/structures.v index be0c29fa1..c5c32a8e9 100644 --- a/structures.v +++ b/structures.v @@ -193,6 +193,11 @@ pred mixin-class o:mixinname, o:classname. % Coq's CS database (which is just for structures). pred mixin-src o:term, o:mixinname, o:term. +% [has-mixin-instance P M G] states that G is a reference to an instance +% which can be used to reconstruct an instance +% of the form [M P …] with eventually some parameters for P. +pred has-mixin-instance o:cs-pattern, o:mixinname, o:gref. + %% database for HB.builders %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % [builder N TheFactory TheMixin S] is used to @@ -525,6 +530,7 @@ solve (goal _ _ Ty _ Args as G) GLS :- with-attributes (with-logging (std.do! [ Elpi Typecheck. Elpi Export HB.pack. + (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) @@ -604,9 +610,10 @@ Elpi Accumulate File "HB/structure.elpi". Elpi Accumulate lp:{{ 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)) + if (ground_term Ty) (Sort = Ty) (Sort = {{Type}}), sort Univ = Sort, + with-attributes (with-logging (structure.declare N B Univ)), ]. main _ :- coq.error "Usage: HB.structure Definition := { A of A & … & A }". @@ -618,6 +625,35 @@ Elpi Export HB.structure. (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) +(* [HB.saturate_instances] saturates all instances possible *) + + +#[arguments(raw)] Elpi Command HB.saturate_instances. +#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". +#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". +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/common/log.elpi". +Elpi Accumulate File "HB/common/synthesis.elpi". +Elpi Accumulate File "HB/structure.elpi". +Elpi Accumulate File "HB/context.elpi". +Elpi Accumulate File "HB/instance.elpi". +Elpi Accumulate File "HB/common/phant-abbreviation.elpi". +Elpi Accumulate File "HB/factory.elpi". +Elpi Accumulate File "HB/export.elpi". +Elpi Accumulate Db hb.db. +Elpi Accumulate lp:{{ +main [] :- !, with-attributes (with-logging (instance.saturate-instances)). +main _ :- coq.error "Usage: HB.saturate_instances". +}}. +Elpi Typecheck. +Elpi Export HB.saturate_instances. + +(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) +(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) +(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) + (** [HB.instance] associates to a type all the structures that can be obtained from the provided factory inhabitant. @@ -665,6 +701,7 @@ main _ :- coq.error "Usage: HB.instance Definition := T ...". Elpi Typecheck. Elpi Export HB.instance. + (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) diff --git a/tests/instance_before_structure.v b/tests/instance_before_structure.v new file mode 100644 index 000000000..ec8300c90 --- /dev/null +++ b/tests/instance_before_structure.v @@ -0,0 +1,37 @@ +From HB Require Import structures. + +HB.mixin Record m1 T := { default1 : T }. + +HB.mixin Record m2 T := { default2 : T }. + +HB.mixin Record m3 T := { default3 : T }. + +HB.structure Definition s1 := { T of m1 T }. + +HB.instance Definition _ : m1 nat := m1.Build nat 1. + +HB.about nat. + +(* too early *) +HB.instance Definition _ : m2 nat := m2.Build nat 2. + +HB.about nat. (* only s1 on nat *) + +HB.instance Definition _ : m3 nat := m3.Build nat 3. + +HB.structure Definition s2 := { T of m1 T & m2 T }. +HB.about nat. (* s2 is not there yet *) + +HB.structure Definition s3 := { T of m3 T }. +HB.about nat. (* s2 has been instanciated but not s3 *) + + +(* here it works *) +HB.saturate_instances. +HB.about nat. (* all there *) + +Check @default1 nat. +Check @default2 nat. +Check @default3 nat. + + diff --git a/tests/instance_merge.v b/tests/instance_merge.v new file mode 100644 index 000000000..9e48dff3d --- /dev/null +++ b/tests/instance_merge.v @@ -0,0 +1,20 @@ +From HB Require Import structures. + +HB.mixin Record m1 T := { default1 : T }. + +HB.mixin Record m2 T := { default2 : T }. + +HB.structure Definition s1 := { T of m1 T }. +HB.structure Definition s2 := { T of m2 T }. + +HB.instance Definition _ : m1 nat := m1.Build nat 1. +HB.instance Definition nat_m2 : m2 nat := m2.Build nat 2. + +HB.structure Definition s3 := { T of m1 T & m2 T }. + +Check nat:s3.type. +(* The s3 instance on nat should be synthetized automatically, *) +(* But since it's defined afterwards, it's not taken into account. *) +(* A simple recall suffices: *) +(* HB.instance Definition _ := nat_m2. +HB.about nat. *) diff --git a/tests/instance_merge_with_distinct_param.v b/tests/instance_merge_with_distinct_param.v new file mode 100644 index 000000000..89588adb6 --- /dev/null +++ b/tests/instance_merge_with_distinct_param.v @@ -0,0 +1,43 @@ +From HB Require Import structures. + +HB.mixin Record m1 T := { default1 : T }. + +HB.mixin Record m2 T := { default2 : T }. + +(* since s1 only requires m1 there is a 1:1 correspondence +between the structure s1 and the mixin m1 *) +HB.structure Definition s1 := { T of m1 T }. +HB.structure Definition s2 := { T of m2 T }. + +HB.instance Definition nat_m1 := m1.Build nat 0. +HB.instance Definition nat_m2 := m2.Build nat 1. + +(* with the following example we want to show that list +preserves the s1 structure ie. if x:s1.type then (list x):s1.type, +in practice we can use this for the type of polynomials *) +HB.instance Definition list_m1 (X : s1.type) : m1 (list X) := + m1.Build (list X) (cons default1 nil). +(* similarly list preserves s2 structure *) +HB.instance Definition list_m2 (X : s2.type) : m2 (list X) := + m2.Build (list X) (cons default2 nil). + + +HB.structure Definition s3 := { T of m1 T & m2 T }. +(* since we can preserve m1 and m2 with list, we can preserve s3 as well ! *) + +(* +if we have a file A with definitions of S1 and S2, +file B importing Awith definitions of instance nat_m1 and nat_m2 +file C importing A with the definition of s3 +in a file D that imports B and C if we call saturate_instance, we create the instance for s3. +this example shows the need for a separate command +*) + +Check nat : s3.type. +(* since nat satisfies s3.type, so does list nat *) +Check list nat : s3.type. +Check list (list nat) : s3.type. + +Fail Check fun t : s1.type => (list t : s3.type). +Fail Check fun t : s2.type => (list t : s3.type). +Check fun t : s3.type => (list t : s3.type). diff --git a/tests/instance_params_no_type.v b/tests/instance_params_no_type.v index 5220be111..5fdd953e9 100644 --- a/tests/instance_params_no_type.v +++ b/tests/instance_params_no_type.v @@ -1,7 +1,43 @@ From HB Require Import structures. HB.mixin Record is_foo P A := { op : P -> A -> A }. + +HB.instance Definition nat_foo P := is_foo.Build P nat (fun _ x => x). +HB.instance Definition list_foo P := is_foo.Build P (list P) (fun _ x => x). +HB.instance Definition list_foo' P A:= is_foo.Build P (list A) (fun _ x => x). + +About list_foo'. + HB.structure Definition foo P := { A of is_foo P A }. -Axiom f : forall T, T -> nat -> nat. -HB.instance Definition bar P := is_foo.Build P nat (f P). \ No newline at end of file +Section try1. +Variable A : Type. +(* .... list A .... + +(fun A => {| + foo.sort := list..; + foo.class := + {| foo.instance_params_no_type_is_foo_mixin := list_foo A |} + |} ). + + +HB.about foo. *) + +(* Elpi Trace Browser. *) +Check nat_foo. +Check list_foo. +HB.mixin Record is_b A:= { default : A }. +Check foo.type. +Print foo.type. +Print Module foo. +Print foo.axioms_. +(*Elpi Trace Browser. *) +HB.structure Definition b := { A of is_b A}. +HB.instance Definition nat_b := is_b.Build nat 0. + +HB.mixin Record is_bar (P : b.type) A := { test : P -> A -> A }. + +HB.structure Definition bar P := { A of is_bar P A}. +HB.instance Definition list_bar P := is_bar.Build P (list P) (fun _ x => x). +Check list_bar. + diff --git a/tests/two_hier.v b/tests/two_hier.v new file mode 100644 index 000000000..5942064ee --- /dev/null +++ b/tests/two_hier.v @@ -0,0 +1,72 @@ +From HB Require Import structures. + +HB.mixin Record m1 T := { default1 : T }. + +HB.mixin Record m2 T := { default2 : T }. + +(* since s1 only requires m1 there is a 1:1 correspondence +between the structure s1 and the mixin m1 *) +HB.structure Definition s1 := { T of m1 T }. +HB.structure Definition s2 := { T of m2 T }. + +HB.instance Definition nat_m1 := m1.Build nat 0. +HB.instance Definition nat_m2 := m2.Build nat 1. + +(* with the following example we want to show that list +preserves the s1 structure ie. if x:s1.type then (list x):s1.type, +in practice we can use this for the type of polynomials *) +HB.instance Definition list_m1 (X : s1.type) : m1 (list X) := + m1.Build (list X) (cons default1 nil). +(* similarly list preserves s2 structure *) +HB.instance Definition list_m2 (X : s2.type) : m2 (list X) := + m2.Build (list X) (cons default2 nil). + + +HB.structure Definition s3 := { T of m1 T & m2 T }. +(* since we can preserve m1 and m2 with list, we can preserve s3 as well ! *) + +(* +if we have a file A with definitions of S1 and S2, +file B importing Awith definitions of instance nat_m1 and nat_m2 +file C importing A with the definition of s3 +in a file D that imports B and C if we call saturate_instance, we create the instance for s3. +this example shows the need for a separate command +*) + +Check nat : s3.type. +(* since nat satisfies s3.type, so does list nat *) +Check list nat : s3.type. +Check list (list nat) : s3.type. + +Fail Check fun t : s1.type => (list t : s3.type). +Fail Check fun t : s2.type => (list t : s3.type). +Check fun t : s3.type => (list t : s3.type). + +HB.mixin Record m1' (P : s1.type) T := { f1 : P -> T }. + +HB.mixin Record m2' (P : s2.type) T := { f2 : P -> T }. + +(* since s1 only requires m1 there is a 1:1 correspondence +between the structure s1 and the mixin m1 *) +HB.structure Definition s1' P := { T of m1' P T }. +HB.structure Definition s2' P := { T of m2' P T }. + +HB.instance Definition nat_m1' := m1'.Build nat nat (fun _ => 0). +HB.instance Definition nat_m2' := m2'.Build nat nat (fun _ => 1). + +(* with the following example we want to show that list +preserves the s1 structure ie. if x:s1.type then (list x):s1.type, +in practice we can use this for the type of polynomials *) +HB.instance Definition list_m1' (P : s1.type) (X : s1'.type P) : m1' P (list X) := +m1'.Build P (list X) (fun x => cons (f1 x) nil). +(* similarly list preserves s2 structure *) +HB.instance Definition list_m2' (P : s2.type) (X : s2'.type P) : m2' P (list X) := + m2'.Build P (list X) (fun x => cons (f2 x) nil). + + +HB.structure Definition s3' (P : s3.type) := { T of m1' P T & m2' P T }. +Check nat : s3'.type _. +(* since nat satisfies s3'.type, so does list nat *) +Check list nat : s3'.type _. +Check Datatypes_list__canonical__two_hier_s3'. +Check list (list nat) : s3'.type _. \ No newline at end of file diff --git a/tests/unit/close_hole_term.v b/tests/unit/close_hole_term.v new file mode 100644 index 000000000..ed0739738 --- /dev/null +++ b/tests/unit/close_hole_term.v @@ -0,0 +1,29 @@ +From HB Require Import structures. +From elpi Require Import elpi. +From Coq Require Export Setoid. + +Elpi Query HB.instance lp:{{ + X = app [{{list}}, Y], + % X needs to be typechecked here to get rid of the hole for the type of Y + coq.typecheck X _ ok, + instance.close-hole-term X Z, + std.assert! (Z = {{fun x => list x}}) "term badly closed" +}}. + +Elpi Query HB.instance lp:{{ + instance.close-hole-term {{nat}} Z, + std.assert! (Z = {{nat}}) "term badly closed" +}}. + + +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:{{ + Y = {{Inj}}, %Inj has 5 implicit arguments + enrich-type Y X, + % X needs to be typechecked here to get rid of the holes of the types of its arguments + coq.typecheck X _ ok, + instance.close-hole-term X Z, + std.assert! (Z = {{ fun a b c d e => @Inj a b c d e }}) "term badly closed" +}}. \ No newline at end of file diff --git a/tests/unit/enrich_type.v b/tests/unit/enrich_type.v new file mode 100644 index 000000000..c7ee7bd16 --- /dev/null +++ b/tests/unit/enrich_type.v @@ -0,0 +1,27 @@ +From HB Require Import structures. +From elpi Require Import elpi. +From Coq Require Export Setoid. + +Elpi Query HB.structure lp:{{ + enrich-type {{nat}} X, + std.assert! (X = {{nat}}) "wrong enriched type" +}}. + +Elpi Query HB.structure lp:{{ + enrich-type {{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))}})), + enrich-type (Y _ _) X, + std.assert! (X = (app [{{prod}}, (app[{{list}},X1]), app[{{list}},C]])) "wrong enriched type" +}}. + +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:{{ + enrich-type {{Inj}} X, + std.assert! (X = app [(global (const Inj)), A, B, R, S, F]) "wrong enriched type" +}}. diff --git a/tests/unit/mixin_src_has_mixin_instance.v b/tests/unit/mixin_src_has_mixin_instance.v new file mode 100644 index 000000000..0694875fd --- /dev/null +++ b/tests/unit/mixin_src_has_mixin_instance.v @@ -0,0 +1,30 @@ +From HB Require Import structures. +From elpi Require Import elpi. + +HB.mixin Record m1 T := { default1 : T }. +HB.mixin Record m2 T := { default2 : T }. + +HB.structure Definition s1 := { T of m1 T }. +HB.instance Definition i1 (X : s1.type) : m1 (list X) := +m1.Build (list X) (cons default1 nil). + +HB.instance Definition nat_m1 : m1 nat := m1.Build nat 1. +HB.instance Definition nat_m2 : m2 nat := m2.Build nat 1. + + +Elpi Query HB.instance lp:{{ +mixin-src->has-mixin-instance (mixin-src {{nat}} M1 {{nat_m1}}) Y, +Y = has-mixin-instance (cs-gref {{:gref nat}}) {{:gref m1.phant_axioms}} {{:gref nat_m1}}. + +}}. + +Section Test. +Variable X:s1.type. + +Elpi Query HB.instance lp:{{ +mixin-src->has-mixin-instance (mixin-src {{list X}} M1 {{i1 X}}) Y, +Y = has-mixin-instance (cs-gref {{:gref list}}) {{:gref m1.phant_axioms}} {{:gref i1}}. + +}}. +End Test. + diff --git a/tests/unit/mk_src_map.v b/tests/unit/mk_src_map.v new file mode 100644 index 000000000..68dde5765 --- /dev/null +++ b/tests/unit/mk_src_map.v @@ -0,0 +1,26 @@ +From HB Require Import structures. + +HB.mixin Record is_foo P A := { op : P -> A -> A }. +HB.mixin Record is_foo' P A := { op : P -> A -> A }. + +HB.instance Definition list_foo P := is_foo.Build P (list P) (fun _ x => x). + +HB.instance Definition list_foo' P A := is_foo.Build P (list A) (fun _ x => x). +Check list_foo'. +Check list_foo. + +Elpi Query HB.structure lp:{{ + +mk-src-map (has-mixin-instance (cs-gref{{:gref list}}) {{:gref is_foo.axioms_}} {{:gref list_foo}}) MS, + MS = (pi a b \ + mixin-src (app [{{list}}, b]) ({{:gref is_foo.axioms_}}) (app [{{list_foo}}, a]) + :- [coq.unify-eq a b ok]) +}}. + +Elpi Query HB.structure lp:{{ + +mk-src-map (has-mixin-instance (cs-gref{{:gref list}}) {{:gref is_foo.axioms_}} {{:gref list_foo'}}) MS', +MS' = (pi p a b \ + mixin-src (app [{{list}}, b]) {{:gref is_foo.axioms_}} (app [{{list_foo'}}, p,a]) + :- [coq.unify-eq a b ok]). +}}. \ No newline at end of file diff --git a/tests/unit/struct.v b/tests/unit/struct.v new file mode 100644 index 000000000..2be5f2e69 --- /dev/null +++ b/tests/unit/struct.v @@ -0,0 +1,36 @@ +From HB Require Import structures. + +HB.mixin Record m1 T := { default1 : T }. +HB.mixin Record m2 T := { default2 : T }. +HB.mixin Record is_foo P A := { op : P -> A -> A }. +HB.structure Definition foo P := { A of is_foo P A}. +HB.structure Definition foo1 := { A of is_foo (option nat) A & m1 A}. + + +Elpi Query HB.structure lp:{{ +std.findall (has-mixin-instance _ _ _) H +}}. + +(* here we don't have any declared instances but a clause is still created by the system : +has-mixin-instance (cs-gref (const «eta»)) (indt «is_foo.axioms_») (const «struct_foo1__to__struct_is_foo») +struct_foo1__to__struct_is_foo is an instance created by the system upon structure declaration to allow +coercions from foo1 to other structures with the mixin is_foo. +*) +Print struct_foo1__to__struct_is_foo. + +(* its type is +forall A : foo1.type, is_foo.axioms_ (option nat) (eta A)) +which means it can't serve as a coercion for foo2 or foo3, + +however foo3 can still be declared because it has another mixin, +while foo2 can't because it has the exact same mixins than foo + +*) + + +Fail HB.structure Definition foo2 := { A of is_foo bool A}. + + +HB.structure Definition foo3 := { A of is_foo bool A & m2 A}. + +Fail HB.structure Definition fooj := { A of foo1 A & foo3 A}. From 81cdb25a7869a8c62556f4a3beda963545cfddc1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 4 Oct 2023 22:23:27 +0200 Subject: [PATCH 2/2] Fixes and cleanups --- .gitignore | 1 - Changelog.md | 1 + HB/common/database.elpi | 101 +++++++++------------ HB/common/stdpp.elpi | 83 +++++++++++++++++ HB/common/utils.elpi | 7 ++ HB/context.elpi | 2 +- HB/instance.elpi | 97 ++++++++------------ HB/structure.elpi | 11 +-- Makefile | 2 +- README.md | 2 + _CoqProject.test-suite | 5 +- instance.md | 73 --------------- structures.v | 30 +++--- tests/instance_before_structure.v | 2 +- tests/instance_merge.v | 20 ---- tests/instance_merge_with_distinct_param.v | 2 + tests/instance_merge_with_param.v | 26 ++++++ tests/instance_params_no_type.v | 2 - tests/two_hier.v | 5 +- tests/unit/close_hole_term.v | 8 +- tests/unit/enrich_type.v | 8 +- tests/unit/mk_src_map.v | 4 +- tests/unit/struct.v | 2 +- 23 files changed, 245 insertions(+), 249 deletions(-) delete mode 100644 instance.md create mode 100644 tests/instance_merge_with_param.v diff --git a/.gitignore b/.gitignore index 554a47d4b..80a4d7d4e 100644 --- a/.gitignore +++ b/.gitignore @@ -58,4 +58,3 @@ _minted-* *.vtc *.dot -*.json diff --git a/Changelog.md b/Changelog.md index 76ab679fc..246a3c991 100644 --- a/Changelog.md +++ b/Changelog.md @@ -3,6 +3,7 @@ ## Unreleased - **Removed** the `#[primitive_class]` attribute, making it the default. +- **New** `HB.saturate` to saturate instances w.r.t. the current hierarchy ## [1.6.0] - 2023-09-20 diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 22b1a8740..d583b4c37 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -1,7 +1,7 @@ /* Hierarchy Builder: algebraic hierarchies made easy This software is released under the terms of the MIT license */ -shorten coq.{ term->gref, term-is-gref?, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }. +shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }. %%%%%%%%% HB database %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -14,13 +14,6 @@ from_mixin (from _ X _) X. pred from_builder i:prop, o:term. from_builder (from _ _ X) (global X). -% for a given clause mixin-src with eventually a condition, -% returns the type of the first argument -pred mixin-src-w-cond_type i:prop, o:term. -mixin-src-w-cond_type(mixin-src (global G) _ _ :- _) (global G). -mixin-src-w-cond_type (mixin-src (app [T|_]) _ _ :- _) T. -mixin-src-w-cond_type (pi x \ (C x)) T :- pi y \ mixin-src-w-cond_type (C y) T. - pred mixin-src_mixin i:prop, o:mixinname. mixin-src_mixin (mixin-src _ M _) M. @@ -146,16 +139,31 @@ undup-grefs L UL :- std.do! [ coq.gref.set.elements S UL, ]. -% remove duplicates from a list of terms, but all the terms have to be global references -pred undup-terms i:list term, o:list term. -undup-terms L UL :- std.do! [ - std.map L coq.term->gref LG, - undup-grefs LG ULG, - std.map ULG (coq.env.global ) UL, +pred undup-sorts i:list sort, o:list sort. +undup-sorts L R :- std.do! [ + + if (std.mem L prop) (R1 = [prop]) (R1 = []), + if (std.mem L sprop) (R2 = [sprop]) (R2 = []), + if (std.mem L (typ _)) (R3 = [typ _]) (R3 = []), + + std.flatten [R1, R2, R3] R, ]. +% also prunes cs-default +pred undup-cs-patterns i:list cs-pattern, o:list cs-pattern. +undup-cs-patterns L R :- std.do! [ + std.map-filter L (x\r\ x = cs-gref r) LGR, + undup-grefs LGR ULGR, + std.map ULGR (x\r\ r = cs-gref x) R1, + std.map-filter L (x\r\ x = cs-sort r) LS, + undup-sorts LS ULS, + std.map ULS (x\r\ r = cs-sort x) R2, + if (std.mem L cs-prod) (R3 = [cs-prod]) (R3 = []), + + std.flatten [R1, R2, R3] R, +]. % Mixins can be topologically sorted according to their dependencies pred toposort-mixins i:list (w-args mixinname), o:list (w-args mixinname). @@ -220,10 +228,13 @@ pred findall-has-mixin-instance o:list prop. findall-has-mixin-instance CL :- std.findall (has-mixin-instance _ _ _) CL. +pred has-mixin-instance_key i:prop, o:cs-pattern. +has-mixin-instance_key (has-mixin-instance P _ _) P. + pred findall-mixin-src i:term, o:list mixinname. findall-mixin-src T ML :- std.map {std.findall (mixin-src T M_ V_)} mixin-src_mixin ML. - + pred findall-local-canonical o:list constant. findall-local-canonical CL :- std.map {std.findall (local-canonical C_)} local-canonical-gref CL. @@ -300,7 +311,6 @@ assert-good-coverage! MLSortedRev CNL :- std.do! [ true ]. - %%%%% Coq Database %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % [get-structure-coercion S1 S2 F] finds the coecion F from the structure S1 to S2 @@ -359,72 +369,47 @@ mixin-src->has-mixin-instance (mixin-src (sort U) M I) (has-mixin-instance (cs-s % this auxiliary function iterates over the list of arguments of an application, % and create the necessary unify condition for each arguments % and at the end returns the mixin-src clause with all the conditions -pred mk-src-aux +pred mixin-instance-type->mixin-src.aux i:list term, % list of arguments i:term, % head of the original application i:mixinname, % name of mixin i:term, % instance body i:list prop, % Cond list o:prop. -mk-src-aux [] T M I Cond (mixin-src T M I :- Cond). -mk-src-aux [A|Args] T M I Cond (pi a \ C a) :- +mixin-instance-type->mixin-src.aux [] T M I Cond (mixin-src T M I :- Cond). +mixin-instance-type->mixin-src.aux [A|Args] T M I Cond (pi a \ C a) :- pi a \ sigma Ta\ coq.mk-app T [a] Ta, - mk-src-aux Args Ta M I [coq.unify-eq A a ok|Cond] (C a). + mixin-instance-type->mixin-src.aux Args Ta M I [coq.unify-eq A a ok|Cond] (C a). -% transforms the has-mixin-instance clause arguments into a -% mixin-src clause with eventuals conditions regarding its parameters -pred mk-src +% transforms the type of a mixin instance into a +% mixin-src clause with eventual conditions regarding its parameters +pred mixin-instance-type->mixin-src i:term, % type of the instance Ty i:mixinname, % name of mixin i:term, % instance body I of type Ty i:list prop, % Cond list o:prop. -mk-src (app [_|Args]) M I Cond C :- - std.last Args Last, - safe-dest-app Last Hd ArgsLast, - mk-src-aux ArgsLast Hd M I Cond C. +mixin-instance-type->mixin-src (app _ as F) M I Cond C :- + factory? F (triple _ _ Subject), + safe-dest-app Subject Hd Args, + mixin-instance-type->mixin-src.aux Args Hd M I Cond C. -mk-src (prod N_ _ F) M I Cond (pi a \ C a) :- +mixin-instance-type->mixin-src (prod N_ _ F) M I Cond (pi a \ C a) :- pi a\ sigma Ia \ coq.mk-app I [a] Ia, - mk-src (F a) M Ia Cond (C a). - - -% for a type T, create as many holes as there are foralls and returns that enriched type -pred enrich-type i:term, o:term . -enrich-type T ET :- - coq.typecheck T TH ok, - coq.count-prods TH N, - if (N = 0) (ET = T) (coq.mk-app T {coq.mk-n-holes N} ET). + mixin-instance-type->mixin-src (F a) M Ia Cond (C a). -% wrapper for mk-src so it can be called by a map on a list of clauses has-mixin-instance -pred mk-src-map i:prop, o:prop. -mk-src-map (has-mixin-instance _ M IHd) C :- std.do![ +pred has-mixin-instance->mixin-src i:prop, o:prop. +has-mixin-instance->mixin-src (has-mixin-instance _ M IHd) C :- std.do![ T = global IHd, coq.env.typeof IHd Ty, - mk-src Ty M T [] C, - ]. - -pred cs-pattern->term i:cs-pattern, o:term. -cs-pattern->term (cs-gref GR) (global GR). -cs-pattern->term (cs-sort U) (sort U). - -pred term->cs-pattern i:term, o:cs-pattern. -term->cs-pattern (prod _ _ _) cs-prod. -term->cs-pattern (sort U) (cs-sort U). -term->cs-pattern T (cs-gref GR) :- term->gref T GR. -term->cs-pattern T _ :- coq.error T "HB database: is not a valid canonical key". - -pred cs-pattern->name i:cs-pattern, o:string. -cs-pattern->name cs-prod "prod". -cs-pattern->name (cs-sort _) "sort". -cs-pattern->name cs-default "default". -cs-pattern->name (cs-gref GR) Name :- gref->modname-label GR 1 "_" Name. + mixin-instance-type->mixin-src Ty M T [] C, +]. pred get-canonical-structures i:term, o:list structure. get-canonical-structures TyTrm StructL :- std.do! [ diff --git a/HB/common/stdpp.elpi b/HB/common/stdpp.elpi index 85366b424..fac753e44 100644 --- a/HB/common/stdpp.elpi +++ b/HB/common/stdpp.elpi @@ -251,3 +251,86 @@ coq.fold-map (primitive _ as C) A C A :- !. coq.fold-map (uvar M L as X) A W A1 :- var X, !, std.fold-map L A coq.fold-map L1 A1, coq.mk-app-uvar M L1 W. % when used in CHR rules coq.fold-map (uvar X L) A (uvar X L1) A1 :- std.fold-map L A coq.fold-map L1 A1. + +pred cs-pattern->term i:cs-pattern, o:term. +cs-pattern->term (cs-gref GR) T :- coq.env.global GR T. +cs-pattern->term (cs-sort prop) (sort prop). +cs-pattern->term (cs-sort sprop) (sort sprop). +cs-pattern->term (cs-sort _) T :- coq.elaborate-skeleton {{ Type }} _ T ok. +cs-pattern->term cs-prod T :- coq.elaborate-skeleton (prod `x` Ty_ x\ Bo_ x) _ T ok. + +pred term->cs-pattern i:term, o:cs-pattern. +term->cs-pattern (prod _ _ _) cs-prod. +term->cs-pattern (sort U) (cs-sort U). +term->cs-pattern T (cs-gref GR) :- coq.term->gref T GR. +term->cs-pattern T _ :- coq.error T "HB database: is not a valid canonical key". + +pred cs-pattern->name i:cs-pattern, o:string. +cs-pattern->name cs-prod "prod". +cs-pattern->name (cs-sort _) "sort". +cs-pattern->name cs-default "default". +cs-pattern->name (cs-gref GR) Name :- gref->modname-label GR 1 "_" Name. + +% --------------------------------------------------------------------- +% kit for closing a term by abstracting evars with lambdas +% we use constraints to attach to holes a number +% and replace them by a special node, to later be bound +% via a lambda + +namespace abstract-holes { + +% we add a new constructor to terms to represent terms to be abstracted +type abs int -> term. + +% bind back abstracted subterms +pred bind i:int, i:int, i:term, o:term. +bind I M T T1 :- M > I, !, + T1 = {{ fun x => lp:(B x) }}, + N is I + 1, + pi x\ % we allocate the fresh symbol for (abs M) + (copy (abs N) x :- !) => % we schedule the replacement (abs M) -> x + bind N M T (B x). +bind M M T T1 :- copy T T1. % we perform all the replacements + +% for a term with M holes, returns a term with M variables to fill these holes +% the clause see is only generated for a term if it hasn't been seen before +% the term might need to be typechecked first or main generates extra holes for the +% type of the parameters +pred main i:term, o:term. +main T1 T3 :- std.do! [ + % we put (abs N) in place of each occurrence of the same hole + (pi T Ty N N' M \ fold-map T N (abs M) M :- var T, not (seen? T _), !, coq.typecheck T Ty ok, fold-map Ty N _ N', M is N' + 1, seen! T M) => + (pi T N M \ fold-map T N (abs M) N :- var T, seen? T M, !) => + fold-map T1 0 T2 M, + % we abstract M holes (M abs nodes) + bind 0 M T2 T3, + % cleanup constraint store + purge-seen!, +]. + +% all constraints are also on _ so that they share +% a variable with the constraint to purge the store + +% we query if the hole was seen before, and if so +% we fetch its number +pred seen? i:term, o:int. +seen? X Y :- declare_constraint (seen? X Y) [X,_]. + +% we declare it is now seen and label it with a number +pred seen! i:term, i:int. +seen! X Y :- declare_constraint (seen! X Y) [X,_]. + +% to empty the store +pred purge-seen!. +purge-seen! :- declare_constraint purge-seen! [_]. + +constraint seen? seen! purge-seen! { + % a succesful query, give the label back via M + rule (seen! X N) \ (seen? X M) <=> (M = N). + % an unsuccesful query + rule \ (seen? X _) <=> false. + + rule purge-seen! \ (seen! _ _). + rule \ purge-seen!. +} +} \ No newline at end of file diff --git a/HB/common/utils.elpi b/HB/common/utils.elpi index fcd66647c..fa7552b0d 100644 --- a/HB/common/utils.elpi +++ b/HB/common/utils.elpi @@ -375,3 +375,10 @@ prod-last X X :- !. pred prod-last-gref i:term, o:gref. 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 :- + coq.typecheck T TH ok, + coq.count-prods TH N, + coq.mk-app T {coq.mk-n-holes N} ET. diff --git a/HB/context.elpi b/HB/context.elpi index d7fd4d5e6..4b04e5f0b 100644 --- a/HB/context.elpi +++ b/HB/context.elpi @@ -73,7 +73,7 @@ postulate-mixin TheType (triple M Ps T) (triple CL MSL MLwP) (triple OutCL [MC|M MC = mixin-src T M (global (const C)), MC => get-option "local" tt => - instance.declare-all-generic-type TheType {findall-classes-for [M]} NewCSL, + instance.declare-all TheType {findall-classes-for [M]} NewCSL, std.map NewCSL snd NewCL, std.append CL NewCL OutCL ]. diff --git a/HB/instance.elpi b/HB/instance.elpi index f48f56b33..7e931d49b 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -37,7 +37,7 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [ ) ( SectionName is "hb_instance_" ^ {std.any->string {new_int}}, log.coq.env.begin-section SectionName, - private.postulate-arity TyWP [] Body SectionBody SectionTy + private.postulate-arity TyWP [] Body SectionBody SectionTy ), % identify the factory @@ -76,47 +76,8 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [ % we accumulate clauses now that the section is over acc-clauses current Clauses - - ]. -% we add a new constructor to terms to represent terms to be abstracted -type abs int -> term. - -% bind back abstracted subterms -pred bind i:int, i:int, i:term, o:term. -bind I M T T1 :- M > I, - T1 = {{ fun x => lp:(B x) }}, - N is I + 1, - pi x\ % we allocate the fresh symbol for (abs M) - (copy (abs N) x :- !) => % we schedule the replacement (abs M) -> x - bind N M T (B x). -bind M M T T1 :- copy T T1. % we perform all the replacements - -% for a term with M holes, returns a term with M variables to fill these holes -% the clause see is only generated for a term if it hasn't been seen before -% the term might need to be typechecked first or close-hole-term generates extra holes for the -% type of the parameters -pred close-hole-term i:term, o:term. -close-hole-term T1 T3 :- std.do! [ - (pi T Ty N N' M \ fold-map T N (abs M) M :- var T, not (seen T _), !, coq.typecheck T Ty ok, fold-map Ty N _ N', M is N' + 1, see T M) => - (pi T N M \ fold-map T N (abs M) N :- var T, seen T M, !) => - fold-map T1 0 T2 M, - bind 0 M T2 T3, -]. - - -pred seen i:term, o:int. -seen X Y :- declare_constraint (seen X Y) [X]. - -pred see i:term, o:int. -see X Y :- declare_constraint (see X Y) [X]. - -constraint seen see { -rule (see X N) \ (seen X M) <=> (M = N). -rule \ (seen X _) <=> false. -} - % [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 % for which all the dependencies (mixins) were postulated so far and skips the @@ -128,6 +89,8 @@ declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :- infer-class T Class Struct MLwP S Name STy Clauses, + !, + decl-const-in-struct Name S STy CS, Clauses => declare-all T Rest L. @@ -137,19 +100,26 @@ declare-all _ [] []. % 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-generic-type i:term, i:list class, o:list (pair id constant). -declare-all-generic-type T [class Class Struct MLwP|Rest] [pr Name CS|L] :- +pred declare-all-on-type-constructor i:term, i:list class, o:list (pair id constant). +declare-all-on-type-constructor T [class Class Struct MLwP|Rest] [pr Name 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 T Ty, - enrich-type T Ty, infer-class Ty Class Struct MLwP S Name _STy Clauses, - close-hole-term S SC, - std.assert-ok! (coq.typecheck SC SCTy) "badly closed", + + !, + + abstract-holes.main S SC, + std.assert-ok! (coq.typecheck SC SCTy) "declare-all-on-type-constructor: badly closed", + decl-const-in-struct Name SC SCTy CS, - Clauses => declare-all-generic-type T Rest L. + Clauses => declare-all-on-type-constructor T Rest L. -declare-all-generic-type T [_|Rest] L :- declare-all-generic-type T Rest L. -declare-all-generic-type _ [] []. +declare-all-on-type-constructor T [_|Rest] L :- declare-all-on-type-constructor T Rest L. +declare-all-on-type-constructor _ [] []. pred infer-class i:term, i:classname, i:gref, i:factories, o:term, o:string, o:term, o:list prop. infer-class T Class Struct MLwP S Name STy Clauses:- std.do![ @@ -174,13 +144,12 @@ infer-class T Class Struct MLwP S Name STy Clauses:- std.do![ if-verbose (coq.say {header} "declare canonical structure instance" Name), - get-constructor Struct KS, coq.safe-dest-app T THD _, private.optimize-class-body THD {std.length Params} KCApp KCAppNames Clauses, coq.mk-app (global KS) {std.append Params [T, KCAppNames]} S, if-verbose (coq.say {header} "structure instance for" Name "is" {coq.term->string S}), - std.assert-ok! (coq.typecheck S STy) "infer1: S illtyped", + std.assert-ok! (coq.typecheck S STy) "infer-class: S illtyped", ]. pred decl-const-in-struct i:string, i:term, i:term, i:constant. @@ -239,7 +208,7 @@ mk-factory-sort-deps AliasGR CSL :- std.do! [ KFSortMSL, KFSortMSL => synthesis.under-mixin-src-from-factory.do! KFSort GCF - [declare-all-generic-type KFSort {findall-classes-for ML} CSL] + [declare-all KFSort {findall-classes-for ML} CSL] ]. pred mk-factory-sort-factory i:gref, o:list (pair id constant). @@ -260,14 +229,24 @@ mk-factory-sort-factory AliasGR CSL :- std.do! [ pred saturate-instances. saturate-instances :- std.do! [ findall-has-mixin-instance ClausesHas, - std.map ClausesHas mk-src-map Clauses, - std.map-filter Clauses mixin-src-w-cond_type TLD, - undup-terms TLD TL, - findall-classes Classes, - Clauses => std.forall TL (t\ (declare-all-generic-type t Classes _)), -]. + std.map ClausesHas has-mixin-instance_key KL, + undup-cs-patterns KL UKL, + std.map UKL cs-pattern->term TL, + + findall-classes AllClasses, + + std.map ClausesHas has-mixin-instance->mixin-src Clauses, + + Clauses => std.forall2 TL UKL (t\k\sigma Classes\ + std.filter AllClasses (no-instance-for k) Classes, + declare-all-on-type-constructor t Classes _), +]. +pred no-instance-for i:cs-pattern, i:class. +no-instance-for K (class _ S _) :- + get-structure-sort-projection S (global Proj), + coq.CS.db-for Proj K []. /* ------------------------------------------------------------------------- */ /* ----------------------------- private code ------------------------------ */ @@ -366,7 +345,7 @@ declare-canonical-instances-from-factory-and-local-builders add-all-mixins T FGR NewMixins ff Clauses MCSL, ]), list-w-params_list {factory-provides Factory} ML, - Clauses => declare-all-generic-type T {findall-classes-for ML} CCSL, + Clauses => declare-all T {findall-classes-for ML} CCSL, std.append MCSL CCSL CSL ]. @@ -385,7 +364,7 @@ declare-canonical-instances-from-factory Factory T F ClausesHas CSL :- std.do! [ list-w-params_list {factory-provides Factory} ML, add-all-mixins T Factory ML tt Clauses MCSL, std.map-filter Clauses (mixin-src->has-mixin-instance ) ClausesHas, - ClausesHas => declare-all T {findall-classes-for ML} CCSL, % declare-all-generic-type doesn't work here + ClausesHas => declare-all T {findall-classes-for ML} CCSL, % declare-all-on-type-constructor doesn't work here ] ], std.append MCSL CCSL CSL diff --git a/HB/structure.elpi b/HB/structure.elpi index 13b0ad59b..89bf33139 100644 --- a/HB/structure.elpi +++ b/HB/structure.elpi @@ -189,8 +189,8 @@ declare Module BSkel Sort :- std.do! [ NewClauses => if-MC-compat (private.mc-compat-structure Module ModulePath MLToExport {w-params.nparams MLwP} ClassProjection GRPack), - NewClauses => instance.saturate-instances, - +% Automatic saturation disabled since it is expensive +% NewClauses => instance.saturate-instances, ]. /* ------------------------------------------------------------------------- */ @@ -334,9 +334,6 @@ mk-coe-structure-body StructureF StructureT TC Coercion SortProjection ClassProj lp:PackPH (lp:SortP s) (lp:CoercionP (lp:SortP s) (lp:ClassP s)) }}, ]. -pred std.error-and-fail i:(diagnostic -> prop), i:string. -std.error-and-fail P M :- P D, if (D = error X) (coq.error M X, fail) true. - % [declare-coercion P1 P2 C1 C2] declares a structure and a class coercion % from C1 to C2 given P1 P2 the two projections from the structure of C1 pred declare-coercion i:term, i:term, i:class, i:class. @@ -353,7 +350,7 @@ declare-coercion SortProjection ClassProjection w-params.then FMLwP mk-fun mk-fun (mk-coe-class-body FC TC TMLwP) CoeBody, ErrorMessage is "The structures " ^ ModNameF ^ " and " ^ ModNameT ^ " are incompatible: the coercion between them cannot be synthesized", - std.error-and-fail (coq.elaborate-skeleton CoeBody Ty CoeBody') ErrorMessage, + std.assert-ok! (coq.elaborate-skeleton CoeBody Ty CoeBody') ErrorMessage, if-verbose (coq.say {header} "declare coercion hint" CName), @@ -366,7 +363,7 @@ declare-coercion SortProjection ClassProjection SCoeBody, ErrorMessage is "The structures " ^ ModNameF ^ " and " ^ ModNameT ^ " are incompatible: the coercion between them cannot be synthesized", - std.error-and-fail (coq.elaborate-skeleton SCoeBody STy SCoeBody') ErrorMessage, + std.assert-ok! (coq.elaborate-skeleton SCoeBody STy SCoeBody') ErrorMessage, if-verbose (coq.say {header} "declare unification hint" SName), diff --git a/Makefile b/Makefile index 2b86211fa..14cfc4a9a 100644 --- a/Makefile +++ b/Makefile @@ -141,5 +141,5 @@ endif structures.vo : %.vo: __always__ Makefile.coq +$(COQMAKE) $@ -$(addsuffix o,$(wildcard examples/*.v examples/*/*.v tests/*.v)): __always__ config build Makefile.test-suite.coq +$(addsuffix o,$(wildcard examples/*.v examples/*/*.v tests/*.v tests/unit/*.v)): __always__ config build Makefile.test-suite.coq +$(COQMAKE_TESTSUITE) $@ diff --git a/README.md b/README.md index df51bc7e4..38b2bf8e6 100644 --- a/README.md +++ b/README.md @@ -134,6 +134,8 @@ opam install coq-hierarchy-builder - `HB.builders` and `HB.end` declare a set of builders, - `HB.instance` declares a structure instance, - `HB.declare` declares a context with parameters, key and mixins. + - `HB.saturate` reconsiders all mixin instances to see if some newly declared + structure can be inhabited - HB core tactic-in-term: - `HB.pack` to synthesize a structure instance in the middle of a term. diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite index f806edf89..391e6c394 100644 --- a/_CoqProject.test-suite +++ b/_CoqProject.test-suite @@ -53,6 +53,8 @@ examples/Coq2020_material/CoqWS_abstract.v examples/Coq2020_material/CoqWS_expansion/withHB.v examples/Coq2020_material/CoqWS_expansion/withoutHB.v +# examples/cat/cat.v + tests/type_of_exported_ops.v tests/duplicate_structure.v tests/instance_params_no_type.v @@ -82,9 +84,10 @@ tests/hnf.v tests/fun_instance.v tests/issue284.v tests/issue287.v +tests/two_hier.v +tests/instance_merge_with_param.v tests/instance_merge_with_distinct_param.v tests/instance_merge.v -tests/two_hier.v tests/unit/enrich_type.v tests/unit/mixin_src_has_mixin_instance.v diff --git a/instance.md b/instance.md deleted file mode 100644 index 9ad34ff91..000000000 --- a/instance.md +++ /dev/null @@ -1,73 +0,0 @@ - Saturating instances on new structure declaration - -When a new structure S_new is created, the instances of factories that the new structure implements are not recorded in the database, instead they are in the coq databse. We want to get the list of factories attached to S_new and create properly the instances that implements those factories with the new structure. - -See the test file tests/instance_before_structure.v for an example - -functions get-canonical-instances and get canonical-structures let us interact with the coq database - -```coq -1. has-mixin-instance CS-pattern mixinname inst. -2. mixin-src {{list lp:X}} {{hasmx}} {{i: eq I}} :- coq unification X eqType I (with X = sort I) -3. has-struct-instance CS-KEY class. -``` - -To create the list of booleans we need to have the section paramaters from the instance definition passed down through the clauses, so the information is saved in the database. - -- This list of booleans is created by sect-params-in-term which given a list of section parameters SP and a term T, returns a list of boolean corresponding to whether or not a parameter in SP appears in T. - -- This information is crucial in creating the right clauses to saturate the right instances later. - -We'll also need later to add parameters from user-created section by interrogating the coq database. - - -Hierarchy builder is supposed to find links within the hierarchy of structures and instances (joins betweens elements). - - -Let's say we have an instance I1 for the structure S1 verifying a mixin M1 and similarly I2, S2, and M2. -If we were to introduce a structure S3 which needs a type verifying both M1 and M2 for a type T compatible with I1 and I2, an instance for S3 and T should be generated automatically, and not only upon encountering a new instance. - -So order matters greatly as a new structure wouldn't know about all the previously defined instances, until a new instace is created. - ---- - -Saturating instances works on instances with parameters this way : - -1. When an instance is created by the user, some clauses of the form mixin-src are created for each mixin instance successfully created. - Such a clause has the form - ```prolog - mixin-src Ty, M, I. - ``` - - where I can be used to reconstruct an instance of M Ty. - - Those clauses were used to then infer new structures. -But we need more information kept in the database. -For each of those clauses, we now store instead a new clause `has-mixin-instance` generated by the translation predicate -`mixin-src->has-mixin-instance`. - - The clauses `has-mixin-instance` still link some concrete instance with the mixins it satisfies but now instead of storing the type of the instance which is too restrictive, we store the canonical structure pattern which allows to be more generic. - - Now when such an instance is declared : - ```coq - HB.instance Definition I1 (X:t1) : mixin1 (list X) := ... . - ``` - a clause of this form is generated - ```coq - has-mixin-instance (cs-gref (indt «list»)) (indt «mixin1.axioms_») (const «I1») - ``` - -2. When a structure S is declared, we want to try to populate it with types already encountered at step 1, which wasn't done before. - - To do so, at the end of a structure declaration, we call a function `saturate-instances`. - We need parametrised `mixin-src` clauses with conditions on parameters. For this we call `mk-src-map` which takes the `has-mixin-instance` and creates the right `mixin-src` clauses. - - Then for each type at the head of the clauses, we try to declare new instances with the new clauses at our disposal with the function `declare-all-generic-type`. - - This function preprocesses the type with `enrich_type` which takes a term, and for each forall quantifiers in it, applies as many holes as necessary. - - Then the function `infer_1` is called which actually tries to create an instance on that enriched type. If it is succesful we need to close the term we got with elpi quantifiers and save the instance in the coq database with `save_1`. - - - - diff --git a/structures.v b/structures.v index c5c32a8e9..ca6ae584b 100644 --- a/structures.v +++ b/structures.v @@ -530,7 +530,6 @@ solve (goal _ _ Ty _ Args as G) GLS :- with-attributes (with-logging (std.do! [ Elpi Typecheck. Elpi Export HB.pack. - (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) @@ -625,30 +624,36 @@ Elpi Export HB.structure. (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) -(* [HB.saturate_instances] saturates all instances possible *) +(* [HB.saturate] saturates all instances w.r.t. the current hierarchy. + + When two (unrelated) files are imported it might be that the instances + declared in one file are sufficient to instantiate structures declared + in the other file. + This command reconsiders all types with a canonical structure instance + and see if the they are also equipped with new ones. +*) -#[arguments(raw)] Elpi Command HB.saturate_instances. -#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". -#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". +#[arguments(raw)] Elpi Command HB.saturate. +Elpi Accumulate Db hb.db. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". +#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". +#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.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/structure.elpi". -Elpi Accumulate File "HB/context.elpi". -Elpi Accumulate File "HB/instance.elpi". Elpi Accumulate File "HB/common/phant-abbreviation.elpi". -Elpi Accumulate File "HB/factory.elpi". Elpi Accumulate File "HB/export.elpi". -Elpi Accumulate Db hb.db. +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 _ :- coq.error "Usage: HB.saturate_instances". +main _ :- coq.error "Usage: HB.saturate". }}. Elpi Typecheck. -Elpi Export HB.saturate_instances. +Elpi Export HB.saturate. (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) @@ -701,7 +706,6 @@ main _ :- coq.error "Usage: HB.instance Definition := T ...". Elpi Typecheck. Elpi Export HB.instance. - (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) diff --git a/tests/instance_before_structure.v b/tests/instance_before_structure.v index ec8300c90..e8e3cb220 100644 --- a/tests/instance_before_structure.v +++ b/tests/instance_before_structure.v @@ -27,7 +27,7 @@ HB.about nat. (* s2 has been instanciated but not s3 *) (* here it works *) -HB.saturate_instances. +HB.saturate. HB.about nat. (* all there *) Check @default1 nat. diff --git a/tests/instance_merge.v b/tests/instance_merge.v index 9e48dff3d..e69de29bb 100644 --- a/tests/instance_merge.v +++ b/tests/instance_merge.v @@ -1,20 +0,0 @@ -From HB Require Import structures. - -HB.mixin Record m1 T := { default1 : T }. - -HB.mixin Record m2 T := { default2 : T }. - -HB.structure Definition s1 := { T of m1 T }. -HB.structure Definition s2 := { T of m2 T }. - -HB.instance Definition _ : m1 nat := m1.Build nat 1. -HB.instance Definition nat_m2 : m2 nat := m2.Build nat 2. - -HB.structure Definition s3 := { T of m1 T & m2 T }. - -Check nat:s3.type. -(* The s3 instance on nat should be synthetized automatically, *) -(* But since it's defined afterwards, it's not taken into account. *) -(* A simple recall suffices: *) -(* HB.instance Definition _ := nat_m2. -HB.about nat. *) diff --git a/tests/instance_merge_with_distinct_param.v b/tests/instance_merge_with_distinct_param.v index 89588adb6..413b58343 100644 --- a/tests/instance_merge_with_distinct_param.v +++ b/tests/instance_merge_with_distinct_param.v @@ -33,6 +33,8 @@ in a file D that imports B and C if we call saturate_instance, we create the ins this example shows the need for a separate command *) +Fail Check nat : s3.type. +HB.saturate. Check nat : s3.type. (* since nat satisfies s3.type, so does list nat *) Check list nat : s3.type. diff --git a/tests/instance_merge_with_param.v b/tests/instance_merge_with_param.v new file mode 100644 index 000000000..9fbc0759b --- /dev/null +++ b/tests/instance_merge_with_param.v @@ -0,0 +1,26 @@ +From HB Require Import structures. + +HB.mixin Record m1 T := { default1 : T }. + +HB.mixin Record m2 T := { default2 : T }. + +HB.structure Definition s1 := { T of m1 T }. +HB.structure Definition s2 := { T of m2 T }. + +HB.instance Definition _ (X : s1.type) : m1 (list X) := + m1.Build (list X) (cons default1 nil). +HB.instance Definition list_m2 (X : s1.type) : m2 (list X) := + m2.Build (list X) nil. + +HB.structure Definition s3 := { T of m1 T & m2 T }. + +HB.about list. (* should have s3 *) + +(* The s3 instance on list should be synthetized automatically, *) +(* But since it's defined afterwards, it's not taken into account. *) +(* The subtelty now is that there is a parameter, but it's always the same *) +(* A simple recall suffices: *) +HB.instance Definition _ (X : s1.type) := list_m2 X. +HB.about list. + + diff --git a/tests/instance_params_no_type.v b/tests/instance_params_no_type.v index 5fdd953e9..070874576 100644 --- a/tests/instance_params_no_type.v +++ b/tests/instance_params_no_type.v @@ -10,8 +10,6 @@ About list_foo'. HB.structure Definition foo P := { A of is_foo P A }. -Section try1. -Variable A : Type. (* .... list A .... (fun A => {| diff --git a/tests/two_hier.v b/tests/two_hier.v index 5942064ee..9d4881f62 100644 --- a/tests/two_hier.v +++ b/tests/two_hier.v @@ -32,7 +32,8 @@ file C importing A with the definition of s3 in a file D that imports B and C if we call saturate_instance, we create the instance for s3. this example shows the need for a separate command *) - +Fail Check nat : s3.type. +HB.saturate. Check nat : s3.type. (* since nat satisfies s3.type, so does list nat *) Check list nat : s3.type. @@ -65,6 +66,8 @@ HB.instance Definition list_m2' (P : s2.type) (X : s2'.type P) : m2' P (list X) HB.structure Definition s3' (P : s3.type) := { T of m1' P T & m2' P T }. +Fail Check nat : s3'.type _. +HB.saturate. Check nat : s3'.type _. (* since nat satisfies s3'.type, so does list nat *) Check list nat : s3'.type _. diff --git a/tests/unit/close_hole_term.v b/tests/unit/close_hole_term.v index ed0739738..4b63a08a5 100644 --- a/tests/unit/close_hole_term.v +++ b/tests/unit/close_hole_term.v @@ -6,12 +6,12 @@ Elpi Query HB.instance lp:{{ X = app [{{list}}, Y], % X needs to be typechecked here to get rid of the hole for the type of Y coq.typecheck X _ ok, - instance.close-hole-term X Z, + abstract-holes.main X Z, std.assert! (Z = {{fun x => list x}}) "term badly closed" }}. Elpi Query HB.instance lp:{{ - instance.close-hole-term {{nat}} Z, + abstract-holes.main {{nat}} Z, std.assert! (Z = {{nat}}) "term badly closed" }}. @@ -21,9 +21,9 @@ inj x y : S (f x) (f y) -> R x y. Elpi Query HB.structure lp:{{ Y = {{Inj}}, %Inj has 5 implicit arguments - enrich-type Y X, + saturate-type-constructor Y X, % X needs to be typechecked here to get rid of the holes of the types of its arguments coq.typecheck X _ ok, - instance.close-hole-term X Z, + abstract-holes.main X Z, std.assert! (Z = {{ fun a b c d e => @Inj a b c d e }}) "term badly closed" }}. \ No newline at end of file diff --git a/tests/unit/enrich_type.v b/tests/unit/enrich_type.v index c7ee7bd16..72947365c 100644 --- a/tests/unit/enrich_type.v +++ b/tests/unit/enrich_type.v @@ -3,18 +3,18 @@ From elpi Require Import elpi. From Coq Require Export Setoid. Elpi Query HB.structure lp:{{ - enrich-type {{nat}} X, + saturate-type-constructor {{nat}} X, std.assert! (X = {{nat}}) "wrong enriched type" }}. Elpi Query HB.structure lp:{{ - enrich-type {{list}} X, + saturate-type-constructor {{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))}})), - enrich-type (Y _ _) X, + saturate-type-constructor (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:{{ - enrich-type {{Inj}} X, + saturate-type-constructor {{Inj}} X, std.assert! (X = app [(global (const Inj)), A, B, R, S, F]) "wrong enriched type" }}. diff --git a/tests/unit/mk_src_map.v b/tests/unit/mk_src_map.v index 68dde5765..2be9718a4 100644 --- a/tests/unit/mk_src_map.v +++ b/tests/unit/mk_src_map.v @@ -11,7 +11,7 @@ Check list_foo. Elpi Query HB.structure lp:{{ -mk-src-map (has-mixin-instance (cs-gref{{:gref list}}) {{:gref is_foo.axioms_}} {{:gref list_foo}}) MS, +has-mixin-instance->mixin-src (has-mixin-instance (cs-gref{{:gref list}}) {{:gref is_foo.axioms_}} {{:gref list_foo}}) MS, MS = (pi a b \ mixin-src (app [{{list}}, b]) ({{:gref is_foo.axioms_}}) (app [{{list_foo}}, a]) :- [coq.unify-eq a b ok]) @@ -19,7 +19,7 @@ mk-src-map (has-mixin-instance (cs-gref{{:gref list}}) {{:gref is_foo.axioms_}} Elpi Query HB.structure lp:{{ -mk-src-map (has-mixin-instance (cs-gref{{:gref list}}) {{:gref is_foo.axioms_}} {{:gref list_foo'}}) MS', +has-mixin-instance->mixin-src (has-mixin-instance (cs-gref{{:gref list}}) {{:gref is_foo.axioms_}} {{:gref list_foo'}}) MS', MS' = (pi p a b \ mixin-src (app [{{list}}, b]) {{:gref is_foo.axioms_}} (app [{{list_foo'}}, p,a]) :- [coq.unify-eq a b ok]). diff --git a/tests/unit/struct.v b/tests/unit/struct.v index 2be5f2e69..16e6afd11 100644 --- a/tests/unit/struct.v +++ b/tests/unit/struct.v @@ -16,7 +16,7 @@ has-mixin-instance (cs-gref (const «eta»)) (indt «is_foo.axioms_») (const « struct_foo1__to__struct_is_foo is an instance created by the system upon structure declaration to allow coercions from foo1 to other structures with the mixin is_foo. *) -Print struct_foo1__to__struct_is_foo. +Print struct_foo1__to__struct_foo. (* its type is forall A : foo1.type, is_foo.axioms_ (option nat) (eta A))