Merge pull request #487 from CohenCyril/fix-432

Hard failure on missing factories + better error message

Author: CohenCyril

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, !,

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,

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,17 +355,17 @@ 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.
 
 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 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

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,

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
+
 ].
 
 

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

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",
 

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),

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 <name>.".
 }}.
@@ -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 <MixinName> 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 <ModuleName> := { A of <Factory1> A & … & <FactoryN> 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 <FactoryName> T of F A & … := { … }.\nUsage: HB.factory Definition <FactoryName> 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.

_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