math-comp · proux01 · Dec 13, 2024 · Dec 12, 2024 · Dec 13, 2024
diff --git a/HB/instance.elpi b/HB/instance.elpi
@@ -14,15 +14,16 @@ declare-existing T0 F0 :- std.do! [
   std.assert! (coq.safe-dest-app FTy (global FactoryAlias) _)
      "The type of the instance is not a factory",
   factory-alias->gref FactoryAlias Factory,
-  private.declare-instance Factory T F Clauses _,
+  private.declare-instance Factory T F Clauses _ _,
   acc-clauses current Clauses,
 ].
 
-% [declare-const N B Ty] adds a Definition N : Ty := B where Ty is a factory
+% [declare-const N B Ty CFL CSL] adds a Definition N : Ty := B where Ty is a factory
 % and equips the type the factory is used on with all the canonical structures
-% that can be built using factory instance B
-pred declare-const i:id, i:term, i:arity, o:list (pair id constant).
-declare-const Name BodySkel TyWPSkel CSL :- std.do! [
+% that can be built using factory instance B. CFL contains the list of
+% factories being defined, CSL the list of canonical structures being defined.
+pred declare-const i:id, i:term, i:arity, o:list (pair id constant), o:list (pair id constant).
+declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [
   std.assert-ok! (coq.elaborate-arity-skeleton TyWPSkel _ TyWP) "Definition type illtyped",
   coq.arity->term TyWP Ty,
   std.assert-ok! (coq.elaborate-skeleton BodySkel Ty Body) "Definition illtyped",
@@ -71,7 +72,11 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [
 
   private.check-non-forgetful-inheritance TheType Factory,
 
-  private.declare-instance Factory TheType TheFactory Clauses CSL,
+  private.declare-instance Factory TheType TheFactory Clauses CFL CSL,
+
+  if (CSL = [])
+     (coq.warning "HB" "HB.no-new-instance" "HB: no new instance is generated")
+     true,
 
   % handle parameters via a section -- end
   if (TyWP = arity _) true (
@@ -206,10 +211,10 @@ declare-factory-sort-factory GR :- std.do! [
   Name is "SortInstances" ^ {std.any->string {new_int}},
   log.coq.env.begin-module Name none,
   log.coq.env.begin-section Name,
-  mk-factory-sort-factory GR CSL,
+  mk-factory-sort-factory GR CFL CSL,
   log.coq.env.end-section-name Name,
   log.coq.env.end-module-name Name _,
-  std.forall CSL (x\ sigma CS\ x = pr _ CS, log.coq.CS.declare-instance CS)
+  std.forall {std.append CFL CSL} (x\ sigma CS\ x = pr _ CS, log.coq.CS.declare-instance CS)
 ].
 
 pred context.declare i:factories, o:mixins, o:list term, o:term, o:list prop, o:list constant.
@@ -239,8 +244,8 @@ mk-factory-sort-deps AliasGR CSL :- std.do! [
       [declare-all KFSort {findall-classes-for ML} CSL]
 ].
 
-pred mk-factory-sort-factory i:gref, o:list (pair id constant).
-mk-factory-sort-factory 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,
   gref-deps GR MLwPRaw,
   context.declare MLwPRaw MLwP SortParams SortKey SortMSL _,
@@ -250,7 +255,7 @@ mk-factory-sort-factory AliasGR CSL :- std.do! [
   coq.mk-n-holes NMLArgs SortMLHoles,
   GCF = global (const CF),
   coq.mk-app (global GR) {std.append SortParams [GCF|SortMLHoles]} FGCF,
-  declare-const "_" GCF (arity FGCF) CSL
+  declare-const "_" GCF (arity FGCF) CFL CSL
 ].
 
 % create instances for all possible combinations of types and structure compatible 
@@ -286,20 +291,20 @@ namespace private {
 shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }.
 
 pred declare-instance i:factoryname, i:term, i:term,
-  o:list prop, o:list (pair id constant).
-declare-instance Factory T F Clauses CSL :-
+  o:list prop, o:list (pair id constant), o:list (pair id constant).
+declare-instance Factory T F Clauses CFL CSL :-
   current-mode (builder-from T TheFactory FGR _), !,
   if (get-option "local" tt)
     (coq.error "HB: declare-instance: cannot make builders local.
     If you want temporary instances, make an alias, e.g. with let T' := T") true,
   !,
   declare-canonical-instances-from-factory-and-local-builders Factory
-    T F TheFactory FGR Clauses CSL.
-declare-instance Factory T F Clauses CSL :-
-  declare-canonical-instances-from-factory Factory T F Clauses1 CSL,
+    T F TheFactory FGR Clauses CFL CSL.
+declare-instance Factory T F Clauses CFL CSL :-
+  declare-canonical-instances-from-factory Factory T F Clauses1 CFL CSL,
   if (get-option "export" tt)
      (coq.env.current-library File,
-      std.map CSL (x\r\ sigma i c\ x = pr i c, r = instance-to-export File i c) Clauses2)
+      std.map {std.append CFL CSL} (x\r\ sigma i c\ x = pr i c, r = instance-to-export File i c) Clauses2)
      (Clauses2 = []),
      std.append Clauses1 Clauses2 Clauses.
 
@@ -367,36 +372,34 @@ postulate-arity (arity Ty) ArgsRev X T Ty :-
 % can access their theory and notations
 pred declare-canonical-instances-from-factory-and-local-builders
    i:factoryname, i:term, i:term, i:term, i:factoryname,
-   o:list prop, o:list (pair id constant).
+   o:list prop, o:list (pair id constant), o:list (pair id constant).
 declare-canonical-instances-from-factory-and-local-builders
-    Factory T F _TheFactory FGR Clauses CSL :- std.do! [
+    Factory T F _TheFactory FGR Clauses CFL CSL :- std.do! [
   synthesis.under-new-mixin-src-from-factory.do! T F (NewMixins\ std.do! [
-      add-all-mixins T FGR NewMixins ff Clauses MCSL,
+      add-all-mixins T FGR NewMixins ff Clauses CFL,
   ]),
   list-w-params_list {factory-provides Factory} ML,
-  Clauses => declare-all T {findall-classes-for ML} CCSL,
-  std.append MCSL CCSL CSL
+  Clauses => declare-all T {findall-classes-for ML} CSL,
 ].
 
 % [declare-canonical-instances-from-factory T F] given a factory F
 % it uses all known builders to declare canonical instances of structures
 % on T
 pred declare-canonical-instances-from-factory
-  i:factoryname, i:term, i:term, o: list prop, o:list (pair id constant).
-declare-canonical-instances-from-factory Factory T F ClausesHas CSL :- std.do! [
+  i:factoryname, i:term, i:term, o: list prop, o:list (pair id constant), o:list (pair id constant).
+declare-canonical-instances-from-factory Factory T F ClausesHas CFL CSL :- std.do! [
   % The order of the following two "under...do!"  is crucial,
   % priority must be given to canonical mixins
   % as they are the ones which guarantee forgetful inheritance
   % hence we add these clauses last.
   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 Clauses MCSL,
+      add-all-mixins T Factory ML tt Clauses CFL,
       std.map-filter Clauses (mixin-src->has-mixin-instance ) ClausesHas,
-      ClausesHas => declare-all T {findall-classes-for ML} CCSL, % declare-all-on-type-constructor doesn't work here
+      ClausesHas => declare-all T {findall-classes-for ML} CSL, % declare-all-on-type-constructor doesn't work here
     ]
   ],
-  std.append MCSL CCSL CSL
 ].
 
 % If you don't mention the factory in a builder, then Coq won't make

diff --git a/HB/structures.v b/HB/structures.v
@@ -772,7 +772,7 @@ Elpi Accumulate lp:{{
 
 :name "start"
 main [const-decl Name (some BodySkel) TyWPSkel] :- !,
-  with-attributes (with-logging (instance.declare-const Name BodySkel TyWPSkel _)).
+  with-attributes (with-logging (instance.declare-const Name BodySkel TyWPSkel _ _)).
 main [T0, F0] :- !,
   coq.warning "HB" "HB.deprecated" "The syntax \"HB.instance Key FactoryInstance\" is deprecated, use \"HB.instance Definition\" instead",
   with-attributes (with-logging (instance.declare-existing T0 F0)).

diff --git a/Makefile.test-suite.coq.local b/Makefile.test-suite.coq.local
@@ -10,7 +10,9 @@ DIFF=\
 	@if [ -z "$$COQ_ELPI_ATTRIBUTES" ]; then \
 	echo OUTPUT DIFF $(1);\
 	$(COQTOP) $(COQFLAGS) $(COQLIBS) -topfile $(1) \
-	  < $(1) 2>/dev/null \
+	  < $(1) 2>&1 \
+	  | sed 's/Coq < *//g' \
+	  | grep -v '^$$' \
 	  | grep -v -e "Skipping rcfile" -e "is declared" -e "is defined" -e "Loading ML file" -e "Welcome to Coq" \
 	  | sed 's/characters \([0-9]\+\)-[0-9]\+/character \1/' \
 	  > $(1).out.aux;\
@@ -28,3 +30,4 @@ post-all::
 	$(call DIFF, tests/hnf.v)
 	$(call DIFF, tests/err_miss_dep.v)
 	$(call DIFF, tests/err_bad_mix.v)
+	$(call DIFF, tests/err_instance_nop.v)
diff --git a/tests/about.v.out b/tests/about.v.out
@@ -9,7 +9,6 @@ HB: AddMonoid_of_TYPE operations and axioms are:
 HB: AddMonoid_of_TYPE requires the following mixins:
 HB: AddMonoid_of_TYPE provides the following mixins:
     - AddMonoid_of_TYPE
-
 HB: AddMonoid_of_TYPE.Build is a factory constructor
     (from "./examples/demo1/hierarchy_5.v", line 10)
 HB: AddMonoid_of_TYPE.Build requires its subject to be already equipped with:
@@ -22,7 +21,6 @@ HB: arguments: AddMonoid_of_TYPE.Build S zero add addrA add0r addr0
     - addrA : associative add
     - add0r : left_id 0%G add
     - addr0 : right_id 0%G add
-
 HB: AddAG.type is a structure (from "./examples/demo1/hierarchy_5.v", line 73)
 HB: AddAG.type characterizing operations and axioms are:
     - addNr
@@ -36,7 +34,6 @@ HB: AddAG inherits from:
     - AddComoid
 HB: AddAG is inherited by:
     - Ring
-
 HB: AddMonoid.type is a structure
     (from "./examples/demo1/hierarchy_5.v", line 17)
 HB: AddMonoid.type characterizing operations and axioms are:
@@ -54,7 +51,6 @@ HB: AddMonoid is inherited by:
     - BiNearRing
     - SemiRing
     - Ring
-
 HB: Ring_of_AddAG is a factory
     (from "./examples/demo1/hierarchy_5.v", line 108)
 HB: Ring_of_AddAG operations and axioms are:
@@ -78,7 +74,6 @@ Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and
      in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics
      and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht,
      1995).
-
 HB: Ring_of_AddAG.Build is a factory constructor
     (from "./examples/demo1/hierarchy_5.v", line 108)
 HB: Ring_of_AddAG.Build requires its subject to be already equipped with:
@@ -103,21 +98,17 @@ Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and
      in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics
      and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht,
      1995).
-
 HB: add is an operation of structure AddMonoid
     (from "./examples/demo1/hierarchy_5.v", line 17)
 HB: add comes from mixin AddMonoid_of_TYPE
     (from "./examples/demo1/hierarchy_5.v", line 10)
-
 HB: AddAG.sort is a canonical projection
     (from "./examples/demo1/hierarchy_5.v", line 73)
 HB: AddAG.sort has the following canonical values:
     - Ring.sort (from "./examples/demo1/hierarchy_5.v", line 196)
     - Z 
-
 HB: AddAG.sort is a coercion from AddAG to Sortclass
     (from "./examples/demo1/hierarchy_5.v", line 73)
-
 HB: Z is canonically equipped with structures:
     - AddMonoid
       AddComoid
@@ -127,13 +118,16 @@ HB: Z is canonically equipped with structures:
       SemiRing
       Ring
       (from "(stdin)", line 10)
-
 HB: hierarchy_5_Ring_class__to__hierarchy_5_SemiRing_class is a coercion from
     Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196)
-
 HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from
     Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196)
-
+Toplevel input, character 15:
+> HB.about Builders_40.hierarchy_5_Ring_of_AddAG__to__hierarchy_5_BiNearRing_of_AddMonoid.
+> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error:
+HB: unable to locate 
+Builders_40.hierarchy_5_Ring_of_AddAG__to__hierarchy_5_BiNearRing_of_AddMonoid
 HB: synthesized in file File "(stdin)", line 5, column 0, character 127:
 Interactive Module hierarchy_5 started
 Interactive Module AddComoid started
@@ -146,4 +140,3 @@ HB: Z is canonically equipped with structures:
       SemiRing
       Ring
       (from "(stdin)", line 10)
-
diff --git a/tests/compress_coe.v.out b/tests/compress_coe.v.out
@@ -17,5 +17,4 @@ fun D D' : D.type =>
     |}
 |}
      : D.type -> D.type -> D.type
-
 Arguments Datatypes_prod__canonical__compress_coe_D D D'
diff --git a/tests/err_instance_nop.v b/tests/err_instance_nop.v
@@ -0,0 +1,6 @@
+From HB Require Import structures.
+
+HB.mixin Record M T := {}.
+HB.structure Definition S := { x of M x }.
+HB.instance Definition _ : M nat := M.Build nat.
+HB.instance Definition _ : M nat := M.Build nat.
diff --git a/tests/err_instance_nop.v.out b/tests/err_instance_nop.v.out
@@ -0,0 +1,3 @@
+Toplevel input, character 155:
+Warning: HB: no new instance is generated
+[HB.no-new-instance,HB,elpi,default]
diff --git a/tests/err_miss_dep.v.out b/tests/err_miss_dep.v.out
@@ -1,2 +1,9 @@
+Toplevel input, character 0:
+> HB.structure Definition AbelianGrp := { A of IsAbelianGrp A }.
+> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Warning:
+pulling in dependencies: [err_miss_dep_IsAddComoid] 
+Please list them or end the declaration with '&'
+[HB.implicit-structure-dependency,HB,elpi,default]
 The command has indeed failed with message:
 HB: Unable to find mixin err_miss_dep_IsAddComoid on subject K
diff --git a/tests/howto.v.out b/tests/howto.v.out
@@ -8,18 +8,14 @@ HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
     - AddComoid_of_TYPE; AddAG_of_AddComoid; Ring_of_AddAG
     - AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid
     - AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid
-
 For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances
-
 HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
     - Ring_of_TYPE
     - AddAG_of_TYPE; BiNearRing_of_AddMonoid
     - AddAG_of_TYPE; Ring_of_AddAG
     - AddAG_of_TYPE; SemiRing_of_AddComoid
     - AddComoid_of_TYPE; Ring_of_AddComoid
-
 For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances
-
 HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
     - Ring_of_TYPE
     - AddAG_of_TYPE; BiNearRing_of_AddMonoid
@@ -30,40 +26,30 @@ HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
     - AddComoid_of_TYPE; AddAG_of_AddComoid; Ring_of_AddAG
     - AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid
     - AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid
-
 For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances
-
 HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
     - Ring_of_TYPE
     - AddAG_of_TYPE; BiNearRing_of_AddMonoid
     - AddAG_of_TYPE; Ring_of_AddAG
     - AddAG_of_TYPE; SemiRing_of_AddComoid
     - AddComoid_of_TYPE; Ring_of_AddComoid
-
 For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances
-
 The command has indeed failed with message:
 HB: no solution found, try to increase search depth.
 HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
     - Ring_of_AddComoid
     - AddAG_of_AddComoid; BiNearRing_of_AddMonoid
     - AddAG_of_AddComoid; Ring_of_AddAG
     - AddAG_of_AddComoid; SemiRing_of_AddComoid
-
 For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances
-
 HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
     - BiNearRing_of_AddMonoid
     - Ring_of_AddAG
     - SemiRing_of_AddComoid
-
 For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances
-
 HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
     - BiNearRing_of_AddMonoid
     - Ring_of_AddAG
     - SemiRing_of_AddComoid
-
 For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances
-
 HB: nothing to do.
diff --git a/tests/missing_join_error.v.out b/tests/missing_join_error.v.out
@@ -1,3 +1,10 @@
+Toplevel input, character 0:
+> HB.structure Definition B2 :=  {M of isB2 M & isA2 M }.
+> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Warning:
+pulling in dependencies: [missing_join_error_isTop] 
+Please list them or end the declaration with '&'
+[HB.implicit-structure-dependency,HB,elpi,default]
 The command has indeed failed with message:
 You must declare the hierarchy bottom-up or add a missing join. 
 There are two ways out:
-Original file line number
+Diff line change
@@ Expand Up / @@ -17,5 +17,4 @@ fun D D' : D.type => @@
         |}
     |}
          : D.type -> D.type -> D.type
     Arguments Datatypes_prod__canonical__compress_coe_D D D'