From c017b971ac923a4774f227b3bb29d27132baaad8 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 13 Dec 2024 16:56:42 +0100 Subject: [PATCH] Hard failure on missing factories + better error message --- HB/about.elpi | 2 +- HB/builders.elpi | 2 +- HB/common/database.elpi | 27 +++++++++++++++----------- HB/common/synthesis.elpi | 4 ++-- HB/export.elpi | 10 ++++++++++ HB/factory.elpi | 18 ++++++++--------- HB/instance.elpi | 11 +++++------ HB/structure.elpi | 7 ++++--- HB/structures.v | 30 +++++++++++++++++------------ _CoqProject.test-suite | 3 +++ tests/err_bad_mix.v.out | 3 +-- tests/unimported_irrelevant_class.v | 18 +++++++++++++++++ tests/unimported_relevant_class.v | 17 ++++++++++++++++ 13 files changed, 105 insertions(+), 47 deletions(-) create mode 100644 tests/unimported_irrelevant_class.v create mode 100644 tests/unimported_relevant_class.v diff --git a/HB/about.elpi b/HB/about.elpi index 971b99967..0c2c2806d 100644 --- a/HB/about.elpi +++ b/HB/about.elpi @@ -29,7 +29,7 @@ main-located S (loc-gref (const C)) :- factory-constructor (const C) _, !, main-located S (loc-gref (const C)) :- exported-op M _ C, !, private.main-operation S M C. -main-located S (loc-gref GR) :- factory-alias->gref GR F, not (F = GR), !, +main-located S (loc-gref GR) :- factory-alias->gref GR F ok, not (F = GR), !, main-located S (loc-gref F). main-located S (loc-abbreviation A) :- phant-abbrev GR PhB A, factory-constructor (indt F) GR, !, diff --git a/HB/builders.elpi b/HB/builders.elpi index 81aad47ac..6606d2efe 100644 --- a/HB/builders.elpi +++ b/HB/builders.elpi @@ -100,7 +100,7 @@ declare-shadowed-located Id (loc-abbreviation Abbrev) :- pred postulate-factory-abbrev i:term, i:list term, i:id, i:factoryname, o:term. postulate-factory-abbrev TheType Params Name Falias TheFactory :- std.do! [ - factory-alias->gref Falias F, + std.assert-ok! (factory-alias->gref Falias F) "HB", phant-abbrev F _ Fabv, coq.notation.abbreviation Fabv {std.append Params [TheType]} Package, Msg is "Unable to declare factory " ^ Name, diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 39fd0274c..425a8b525 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -61,6 +61,9 @@ abbrev-to-export_name (abbrev-to-export _ N _) N. pred abbrev-to-export_body i:prop, o:term. abbrev-to-export_body (abbrev-to-export _ _ B) (global B). +pred clause-to-export_clause i:prop, o:prop. +clause-to-export_clause (clause-to-export _ C) C. + pred extract-builder i:prop, o:builder. extract-builder (builder-decl B) B. @@ -77,7 +80,7 @@ sub-class? (class C1 _ ML1P) (class C2 _ ML2P) :- % [factory-provides F MLwP] computes the mixins MLwP generated by F pred factory-provides i:factoryname, o:mixins. factory-provides FactoryAlias MLwP :- std.do! [ - factory-alias->gref FactoryAlias Factory, + std.assert-ok! (factory-alias->gref FactoryAlias Factory) "HB", gref-deps Factory RMLwP, w-params.map RMLwP (factory-provides.base Factory) MLwP ]. @@ -107,11 +110,11 @@ factory-provides.one Params T B M (triple M PL T) :- std.do! [ pred extract-conclusion-params i:term, i:term, o:list term. extract-conclusion-params TheType (prod _ S T) R :- !, @pi-decl _ S x\ extract-conclusion-params TheType (T x) R. -extract-conclusion-params TheType (app [global GR|Args]) R :- !, - factory-alias->gref GR Factory, +extract-conclusion-params TheType (app [global GR|Args]) R :- !, std.do! [ + std.assert-ok! (factory-alias->gref GR Factory) "HB", factory-nparams Factory NP, std.map Args (copy-pack-holes TheType TheType) NewArgs, - std.take NP NewArgs R. + std.take NP NewArgs R]. extract-conclusion-params TheType T R :- whd1 T T1, !, extract-conclusion-params TheType T1 R. @@ -128,17 +131,17 @@ factories-provide FLwP MLwP :- std.do! [ pred undup-grefs i:list gref, o:list gref. undup-grefs L UL :- std.do! [ - coq.gref.list->set L S, + coq.gref.list->set L S, coq.gref.set.elements S 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, ]. @@ -352,7 +355,7 @@ mixin-src->has-mixin-instance (mixin-src (global GR) M I) (has-mixin-instance ( 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. @@ -360,9 +363,9 @@ mixin-src->has-mixin-instance (mixin-src (sort U) M I) (has-mixin-instance (cs-s 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 create the necessary unify condition for each arguments % and at the end returns the mixin-src clause with all the conditions -pred mixin-instance-type->mixin-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 @@ -434,7 +437,9 @@ structure-nparams Structure NParams :- pred factory? i:term, o:w-args factoryname. factory? S (triple F Params T) :- not (var S), !, - safe-dest-app S (global GR) Args, factory-alias->gref GR F, factory-nparams F NP, !, + safe-dest-app S (global GR) Args, + factory-alias->gref GR F ok, + factory-nparams F NP, !, std.split-at NP Args Params [T|_]. % [find-max-classes Mixins Classes] states that Classes is a list of classes diff --git a/HB/common/synthesis.elpi b/HB/common/synthesis.elpi index 5cd83382e..8aa135b15 100644 --- a/HB/common/synthesis.elpi +++ b/HB/common/synthesis.elpi @@ -240,7 +240,7 @@ builder->term Ps T Src Tgt B :- !, std.do! [ pred instantiate-all-these-mixin-args i:term, i:term, i:list mixinname, o:term. instantiate-all-these-mixin-args (fun _ Tm F) T ML R :- coq.safe-dest-app Tm (global TmGR) _, - factory-alias->gref TmGR M, + factory-alias->gref TmGR M ok, std.mem! ML M, !, if (mixin-for T M X) true (coq.error "HB: Unable to find mixin" {nice-gref->string M} "on subject" {coq.term->string T}), !, @@ -252,7 +252,7 @@ instantiate-all-these-mixin-args F _ _ F. pred instantiate-all-args-let i:term, i:term, o:term, o:diagnostic. instantiate-all-args-let (fun N Tm F) T (let N Tm X R) Diag :- !, std.do! [ coq.safe-dest-app Tm (global TmGR) _, - factory-alias->gref TmGR M, + factory-alias->gref TmGR M ok, if (mixin-for T M X) (@pi-def N Tm X m\ instantiate-all-args-let (F m) T (R m) Diag) (Diag = error Msg, diff --git a/HB/export.elpi b/HB/export.elpi index 58df695d3..2fb15aa3b 100644 --- a/HB/export.elpi +++ b/HB/export.elpi @@ -25,6 +25,11 @@ export.abbrev NiceName GR :- !, coq.env.current-library File, acc-clause current (abbrev-to-export File NiceName GR). +pred export.clause i:prop. +export.clause Clause :- !, + coq.env.current-library File, + acc-clauses current [Clause, clause-to-export File Clause]. + pred export.reexport-all-modules-and-CS i:option string. export.reexport-all-modules-and-CS Filter :- std.do! [ coq.env.current-library File, @@ -57,6 +62,11 @@ export.reexport-all-modules-and-CS Filter :- std.do! [ if-verbose (coq.say {header} "exporting Abbreviations" AbbNames), std.forall2 AbbNames AbbBodies (n\b\@global! => log.coq.notation.add-abbreviation n 0 b ff _), + std.findall (clause-to-export File Clause_) ClausesL, + if-verbose (coq.say {header} "exporting Clauses" Clauses), + std.map ClausesL clause-to-export_clause Clauses, + acc-clauses current Clauses + ]. diff --git a/HB/factory.elpi b/HB/factory.elpi index 339721907..98658b249 100644 --- a/HB/factory.elpi +++ b/HB/factory.elpi @@ -13,13 +13,13 @@ kind factory-abbrev type. type by-classname gref -> factory-abbrev. type by-phantabbrev abbreviation -> factory-abbrev. -pred declare-abbrev i:id, i:factory-abbrev. -declare-abbrev Name (by-classname GR) :- +pred declare-abbrev i:id, i:factory-abbrev, o:abbreviation. +declare-abbrev Name (by-classname GR) 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! [ + @global! => log.coq.notation.add-abbreviation Name 1 (fun _ _ t\ app[global GR,t]) tt Abbrev. +declare-abbrev Name (by-phantabbrev Abbr) Abbrev :- std.do! [ coq.notation.abbreviation-body Abbr Nargs AbbrTrm, - @global! => log.coq.notation.add-abbreviation Name Nargs AbbrTrm tt _, + @global! => log.coq.notation.add-abbreviation Name Nargs AbbrTrm tt Abbrev, ]. pred argument->w-mixins i:argument, o:w-mixins argument. @@ -186,7 +186,7 @@ declare-id-builder.aux GR Params TheType (fun `x` Ty x\x) :- % FactAbbrev is the short name for the factory (either an alias of the class record) pred mk-factory-abbrev i:string, i:gref, o:list prop, o:factory-abbrev. mk-factory-abbrev Str GR Aliases FactAbbrev :- !, std.do! [ - if (factory-alias->gref GR _) + if (factory-alias->gref GR _ ok) (Aliases = [], FactAbbrev = by-classname GR) (phant.of-gref ff GR [] PhTerm, @@ -303,7 +303,7 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance export.module {calc (Module ^ ".Exports")} Exports, - GRDepsClauses => declare-abbrev Module FactAbbrev, + GRDepsClauses => declare-abbrev Module FactAbbrev _, ]. @@ -319,7 +319,7 @@ declare-factory-alias MixinSrcClauses SectionCanonicalInstance log.coq.env.add-const-noimplicits "axioms_" Ty1Closed _ @transparent! C, std.assert! (safe-dest-app Ty1 (global PhF) _Args) "Argument must be a factory", - std.assert! (factory-alias->gref PhF F) "BUG: Factory alias declaration missing", + std.assert-ok! (factory-alias->gref PhF F) "HB", std.assert! (factory-constructor F FK) "BUG: Factory constructor missing", MixinSrcClauses => synthesis.infer-all-gref-deps TheParams TheType FK MFK, @@ -375,7 +375,7 @@ declare-factory-alias MixinSrcClauses SectionCanonicalInstance export.module {calc (Module ^ ".Exports")} Exports, - GRDepsClauses => declare-abbrev Module FactAbbrev, + GRDepsClauses => declare-abbrev Module FactAbbrev _, ]. % [build-deps-for-projections I ML CL] builds a [gref-dep] for each projection P diff --git a/HB/instance.elpi b/HB/instance.elpi index aa552724b..d94946c20 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -13,7 +13,7 @@ declare-existing T0 F0 :- std.do! [ "HB: declare-existing illtyped factory instance", std.assert! (coq.safe-dest-app FTy (global FactoryAlias) _) "The type of the instance is not a factory", - factory-alias->gref FactoryAlias Factory, + std.assert-ok! (factory-alias->gref FactoryAlias Factory) "HB: ", private.declare-instance Factory T F Clauses _ _, acc-clauses current Clauses, ]. @@ -43,8 +43,7 @@ declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [ % identify the factory std.assert! (coq.safe-dest-app SectionTy (global FactoryAlias) Args) "The type of the instance is not a factory", - if (factory-alias->gref FactoryAlias Factory) true - (coq.error "HB:" {coq.term->string (global FactoryAlias)} "is not a factory or its library was not correctly imported"), + std.assert-ok! (factory-alias->gref FactoryAlias Factory) "HB", std.assert! (factory-nparams Factory NParams) "Not a factory synthesized by HB", % declare the constant for the factory instance @@ -221,7 +220,7 @@ pred context.declare i:factories, o:mixins, o:list term, o:term, o:list prop, o: pred mk-factory-sort-deps i:gref, o:list (pair id constant). mk-factory-sort-deps AliasGR CSL :- std.do! [ - factory-alias->gref AliasGR GR, + std.assert-ok! (factory-alias->gref AliasGR GR) "HB: mk-factory-sort-deps", gref-deps GR MLwPRaw, context.declare MLwPRaw MLwP SortParams SortKey SortMSL _, SortMSL => synthesis.infer-all-gref-deps SortParams SortKey GR FSort, @@ -246,7 +245,7 @@ mk-factory-sort-deps AliasGR CSL :- std.do! [ pred mk-factory-sort-factory i:gref, o:list (pair id constant), o:list (pair id constant). mk-factory-sort-factory AliasGR CFL CSL :- std.do! [ - factory-alias->gref AliasGR GR, + std.assert-ok! (factory-alias->gref AliasGR GR) "HB", gref-deps GR MLwPRaw, context.declare MLwPRaw MLwP SortParams SortKey SortMSL _, SortMSL => synthesis.infer-all-gref-deps SortParams SortKey GR FSort, @@ -321,7 +320,7 @@ add-mixin T FGR MakeCanon MissingMixin [MixinSrcCl, BuilderDeclCl] CSL :- std.do std.assert-ok! (coq.typecheck Bo Ty) "declare-instances: mixin illtyped", safe-dest-app Ty (global MixinNameAlias) _, - factory-alias->gref MixinNameAlias MixinName, + std.assert-ok! (factory-alias->gref MixinNameAlias MixinName) "HB", std.assert! (MissingMixin = MixinName) "HB: anomaly: we built the wrong mixin", diff --git a/HB/structure.elpi b/HB/structure.elpi index 097cd6e36..3702ce191 100644 --- a/HB/structure.elpi +++ b/HB/structure.elpi @@ -41,7 +41,7 @@ declare Module BSkel Sort :- std.do! [ ClassName Structure SortProjection ClassProjection Factories StructKeyClause, w-params.map MLwP (_\_\_\ mk-nil) NilwP, - ClassAlias = (factory-alias->gref ClassName ClassName), + ClassAlias = (factory-alias->gref ClassName ClassName ok), CurrentClass = (class ClassName Structure MLwP), ClassName = indt ClassInd, coq.env.indt ClassInd _ _ _ _ [ClassK] _, GRDepsClauses = @@ -124,7 +124,7 @@ declare Module BSkel Sort :- std.do! [ if-verbose (coq.say {header} "accumulating various props"), std.flatten [ - Factories, [ClassAlias], [is-structure Structure], + Factories, [is-structure Structure], NewJoins, [class-def CurrentClass], GRDepsClauses, [gref-deps GRPack MLwP], MixinMems, [StructKeyClause] ] @@ -177,7 +177,8 @@ declare Module BSkel Sort :- std.do! [ if-verbose (coq.say {header} "abbreviation factory-by-classname"), - NewClauses => factory.declare-abbrev Module (factory.by-classname ClassName), + ClassAlias => NewClauses => factory.declare-abbrev Module (factory.by-classname ClassName) ClassAbbrev, + export.clause (phant-abbrev ClassName ClassName ClassAbbrev), NewClauses => if-MC-compat (private.mc-compat-structure Module ModulePath MLToExport {w-params.nparams MLwP} ClassProjection GRPack), diff --git a/HB/structures.v b/HB/structures.v index f9e85b427..9657cfcce 100644 --- a/HB/structures.v +++ b/HB/structures.v @@ -129,9 +129,14 @@ pred phant-abbrev o:gref, o:gref, o:abbreviation. % [factory-alias->gref X GR] when X is already a factory X = GR % however, when X is a phantom abbreviated gref, we find the underlying % factory gref GR associated to it. -pred factory-alias->gref i:gref, o:gref. -factory-alias->gref PhGR GR :- phant-abbrev GR PhGR _, !. -factory-alias->gref GR GR :- phant-abbrev GR _ _, !. +pred factory-alias->gref i:gref, o:gref, o: diagnostic. +factory-alias->gref PhGR GR ok :- phant-abbrev GR PhGR _, !. +factory-alias->gref GR GR ok :- phant-abbrev GR _ _, !. +factory-alias->gref GR _ (error Msg) :- !, + Msg is {coq.term->string (global GR)} ^ + " is not a factory or its library (" ^ + { std.string.concat "." {std.drop-last 1 {coq.gref->path GR} } } ^ + ") was not correctly imported". %%%%% Cache of known facts %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -230,6 +235,7 @@ pred current-mode o:declaration. pred module-to-export o:string, o:id, o:modpath. pred instance-to-export o:string, o:id, o:constant. pred abbrev-to-export o:string, o:id, o:gref. +pred clause-to-export o:string, o:prop. %% database for HB.locate and HB.about %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -268,7 +274,7 @@ Elpi Accumulate lp:{{ main [str S] :- !, if (decl-location {coq.locate S} Loc) (coq.say "HB: synthesized in file" Loc) - (coq.say "HB:" S "not synthesized by HB"). + (coq.say "HB" S "not synthesized by HB"). main _ :- coq.error "Usage: HB.locate .". }}. @@ -482,7 +488,7 @@ actions N :- coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File E)). main [indt-decl D] :- record-decl->id D N, with-attributes (actions N). - + main _ :- coq.error "Usage: HB.mixin Record T of F A & … := { … }.". }}. @@ -495,7 +501,7 @@ Elpi Export HB.mixin. (** [HB.pack] and [HB.pack_for] are tactic-in-term synthesizing a structure instance. - + In the middle of a term, in a context expecting a [Structure.type], you can write [HB.pack T F] to use factory [F] to equip type [T] with [Structure]. If [T] is already a rich type, eg [T : OtherStructure.type] @@ -504,7 +510,7 @@ Elpi Export HB.mixin. If the context does not impose a [Structure.type] typing constraint, then you can use [HB.pack_for Structure.type T F]. - + You can pass zero or more factories like [F] but they must all typecheck in the current context (the type is not enriched progressively). Structure instances are projected to their class in order to obtain a @@ -645,7 +651,7 @@ 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, + if (ground_term Ty) (Sort = Ty) (Sort = {{Type}}), sort Univ = Sort, with-attributes (with-logging (structure.declare N B Univ)), ]. @@ -686,7 +692,7 @@ actions-compat ModuleName :- true. main [const-decl N _ _] :- !, with-attributes (actions N). - + main _ :- coq.error "Usage: HB.structure Definition := { A of A & … & A }". }}. Elpi Typecheck. @@ -839,7 +845,7 @@ actions N :- main [indt-decl D] :- record-decl->id D N, with-attributes (actions N). main [const-decl N _ _] :- with-attributes (actions N). - + main _ :- coq.error "Usage: HB.factory Record T of F A & … := { … }.\nUsage: HB.factory Definition T of F A := t.". }}. @@ -916,7 +922,7 @@ actions N :- begin-section N. main [ctx-decl _] :- !, with-attributes (actions {calc ("Builders_" ^ {std.any->string {new_int} })}). - + main _ :- coq.error "Usage: HB.builders Context A (f : F1 A).". }}. Elpi Typecheck. @@ -1208,5 +1214,5 @@ Notation "`Error_cannot_unify: t1 'with' t2" := (unify t1 t2 None) Notation "`Error: t msg T" := (unify t _ (Some (msg%string, T))) (at level 0, msg, T at level 0, format "`Error: t msg T", only printing) : form_scope. - + Global Open Scope string_scope. diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite index 9f943cb9b..bf2afd776 100644 --- a/_CoqProject.test-suite +++ b/_CoqProject.test-suite @@ -99,6 +99,9 @@ tests/saturate_on.v tests/bug_435.v tests/bug_447.v +tests/unimported_relevant_class.v +tests/unimported_irrelevant_class.v + -R tests HB.tests -R examples HB.examples diff --git a/tests/err_bad_mix.v.out b/tests/err_bad_mix.v.out index a33d3e833..b184000c0 100644 --- a/tests/err_bad_mix.v.out +++ b/tests/err_bad_mix.v.out @@ -1,5 +1,4 @@ Interactive Module Test started Interactive Module Exports started The command has indeed failed with message: -HB: Test.Mixin.axioms_ -is not a factory or its library was not correctly imported +HB: Test.Mixin.axioms_ is not a factory or its library (HB.tests.err_bad_mix.Test) was not correctly imported diff --git a/tests/unimported_irrelevant_class.v b/tests/unimported_irrelevant_class.v new file mode 100644 index 000000000..7eb651b36 --- /dev/null +++ b/tests/unimported_irrelevant_class.v @@ -0,0 +1,18 @@ +From HB Require Import structures. + +Module A. +HB.mixin Record isA T := {}. +HB.structure Definition A := {T of isA T}. +End A. + +HB.mixin Record isB T := {}. +HB.structure Definition B := {T of isB T}. + +Module Export C. +Import A. +HB.mixin Record isC T of A T & B T := {}. +HB.structure Definition C := {T of isB T & isA T & isC T}. +End C. + +(* Should not fail: A is irrelevant *) +HB.instance Definition _ := isB.Build unit. \ No newline at end of file diff --git a/tests/unimported_relevant_class.v b/tests/unimported_relevant_class.v new file mode 100644 index 000000000..d43dd7f5f --- /dev/null +++ b/tests/unimported_relevant_class.v @@ -0,0 +1,17 @@ +From HB Require Import structures. + +Module A. +HB.mixin Record isA T := {}. +HB.structure Definition A := {T of isA T}. +End A. + +Module Export B. +Import A. +HB.factory Record isB T := {}. +HB.builders Context T of isB T. + HB.instance Definition _ := isA.Build T. +HB.end. +End B. + +(* legitimate failure: A is relevant *) +Fail HB.instance Definition _ := isB.Build unit. \ No newline at end of file