Skip to content

Commit 717ef2b

Browse files
proux01proux01
authored
Merge pull request #482 from math-comp/fix-instance-nop-error
warning if HB.instance does nothing
2 parents 4cac323 + 23d1894 commit 717ef2b

File tree

10 files changed

+64
-57
lines changed

10 files changed

+64
-57
lines changed

‎HB/instance.elpi‎

Lines changed: 30 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -14,15 +14,16 @@ declare-existing T0 F0 :- std.do! [
1414
std.assert! (coq.safe-dest-app FTy (global FactoryAlias) _)
1515
"The type of the instance is not a factory",
1616
factory-alias->gref FactoryAlias Factory,
17-
private.declare-instance Factory T F Clauses _,
17+
private.declare-instance Factory T F Clauses _ _,
1818
acc-clauses current Clauses,
1919
].
2020

21-
% [declare-const N B Ty] adds a Definition N : Ty := B where Ty is a factory
21+
% [declare-const N B Ty CFL CSL] adds a Definition N : Ty := B where Ty is a factory
2222
% and equips the type the factory is used on with all the canonical structures
23-
% that can be built using factory instance B
24-
pred declare-const i:id, i:term, i:arity, o:list (pair id constant).
25-
declare-const Name BodySkel TyWPSkel CSL :- std.do! [
23+
% that can be built using factory instance B. CFL contains the list of
24+
% factories being defined, CSL the list of canonical structures being defined.
25+
pred declare-const i:id, i:term, i:arity, o:list (pair id constant), o:list (pair id constant).
26+
declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [
2627
std.assert-ok! (coq.elaborate-arity-skeleton TyWPSkel _ TyWP) "Definition type illtyped",
2728
coq.arity->term TyWP Ty,
2829
std.assert-ok! (coq.elaborate-skeleton BodySkel Ty Body) "Definition illtyped",
@@ -71,7 +72,11 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [
7172

7273
private.check-non-forgetful-inheritance TheType Factory,
7374

74-
private.declare-instance Factory TheType TheFactory Clauses CSL,
75+
private.declare-instance Factory TheType TheFactory Clauses CFL CSL,
76+
77+
if (CSL = [])
78+
(coq.warning "HB" "HB.no-new-instance" "HB: no new instance is generated")
79+
true,
7580

7681
% handle parameters via a section -- end
7782
if (TyWP = arity _) true (
@@ -206,10 +211,10 @@ declare-factory-sort-factory GR :- std.do! [
206211
Name is "SortInstances" ^ {std.any->string {new_int}},
207212
log.coq.env.begin-module Name none,
208213
log.coq.env.begin-section Name,
209-
mk-factory-sort-factory GR CSL,
214+
mk-factory-sort-factory GR CFL CSL,
210215
log.coq.env.end-section-name Name,
211216
log.coq.env.end-module-name Name _,
212-
std.forall CSL (x\ sigma CS\ x = pr _ CS, log.coq.CS.declare-instance CS)
217+
std.forall {std.append CFL CSL} (x\ sigma CS\ x = pr _ CS, log.coq.CS.declare-instance CS)
213218
].
214219

215220
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! [
239244
[declare-all KFSort {findall-classes-for ML} CSL]
240245
].
241246

242-
pred mk-factory-sort-factory i:gref, o:list (pair id constant).
243-
mk-factory-sort-factory AliasGR CSL :- std.do! [
247+
pred mk-factory-sort-factory i:gref, o:list (pair id constant), o:list (pair id constant).
248+
mk-factory-sort-factory AliasGR CFL CSL :- std.do! [
244249
factory-alias->gref AliasGR GR,
245250
gref-deps GR MLwPRaw,
246251
context.declare MLwPRaw MLwP SortParams SortKey SortMSL _,
@@ -250,7 +255,7 @@ mk-factory-sort-factory AliasGR CSL :- std.do! [
250255
coq.mk-n-holes NMLArgs SortMLHoles,
251256
GCF = global (const CF),
252257
coq.mk-app (global GR) {std.append SortParams [GCF|SortMLHoles]} FGCF,
253-
declare-const "_" GCF (arity FGCF) CSL
258+
declare-const "_" GCF (arity FGCF) CFL CSL
254259
].
255260

256261
% create instances for all possible combinations of types and structure compatible
@@ -286,20 +291,20 @@ namespace private {
286291
shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }.
287292

288293
pred declare-instance i:factoryname, i:term, i:term,
289-
o:list prop, o:list (pair id constant).
290-
declare-instance Factory T F Clauses CSL :-
294+
o:list prop, o:list (pair id constant), o:list (pair id constant).
295+
declare-instance Factory T F Clauses CFL CSL :-
291296
current-mode (builder-from T TheFactory FGR _), !,
292297
if (get-option "local" tt)
293298
(coq.error "HB: declare-instance: cannot make builders local.
294299
If you want temporary instances, make an alias, e.g. with let T' := T") true,
295300
!,
296301
declare-canonical-instances-from-factory-and-local-builders Factory
297-
T F TheFactory FGR Clauses CSL.
298-
declare-instance Factory T F Clauses CSL :-
299-
declare-canonical-instances-from-factory Factory T F Clauses1 CSL,
302+
T F TheFactory FGR Clauses CFL CSL.
303+
declare-instance Factory T F Clauses CFL CSL :-
304+
declare-canonical-instances-from-factory Factory T F Clauses1 CFL CSL,
300305
if (get-option "export" tt)
301306
(coq.env.current-library File,
302-
std.map CSL (x\r\ sigma i c\ x = pr i c, r = instance-to-export File i c) Clauses2)
307+
std.map {std.append CFL CSL} (x\r\ sigma i c\ x = pr i c, r = instance-to-export File i c) Clauses2)
303308
(Clauses2 = []),
304309
std.append Clauses1 Clauses2 Clauses.
305310

@@ -367,36 +372,34 @@ postulate-arity (arity Ty) ArgsRev X T Ty :-
367372
% can access their theory and notations
368373
pred declare-canonical-instances-from-factory-and-local-builders
369374
i:factoryname, i:term, i:term, i:term, i:factoryname,
370-
o:list prop, o:list (pair id constant).
375+
o:list prop, o:list (pair id constant), o:list (pair id constant).
371376
declare-canonical-instances-from-factory-and-local-builders
372-
Factory T F _TheFactory FGR Clauses CSL :- std.do! [
377+
Factory T F _TheFactory FGR Clauses CFL CSL :- std.do! [
373378
synthesis.under-new-mixin-src-from-factory.do! T F (NewMixins\ std.do! [
374-
add-all-mixins T FGR NewMixins ff Clauses MCSL,
379+
add-all-mixins T FGR NewMixins ff Clauses CFL,
375380
]),
376381
list-w-params_list {factory-provides Factory} ML,
377-
Clauses => declare-all T {findall-classes-for ML} CCSL,
378-
std.append MCSL CCSL CSL
382+
Clauses => declare-all T {findall-classes-for ML} CSL,
379383
].
380384

381385
% [declare-canonical-instances-from-factory T F] given a factory F
382386
% it uses all known builders to declare canonical instances of structures
383387
% on T
384388
pred declare-canonical-instances-from-factory
385-
i:factoryname, i:term, i:term, o: list prop, o:list (pair id constant).
386-
declare-canonical-instances-from-factory Factory T F ClausesHas CSL :- std.do! [
389+
i:factoryname, i:term, i:term, o: list prop, o:list (pair id constant), o:list (pair id constant).
390+
declare-canonical-instances-from-factory Factory T F ClausesHas CFL CSL :- std.do! [
387391
% The order of the following two "under...do!" is crucial,
388392
% priority must be given to canonical mixins
389393
% as they are the ones which guarantee forgetful inheritance
390394
% hence we add these clauses last.
391395
synthesis.under-mixin-src-from-factory.do! T F [
392396
synthesis.under-local-canonical-mixins-of.do! T [
393397
list-w-params_list {factory-provides Factory} ML,
394-
add-all-mixins T Factory ML tt Clauses MCSL,
398+
add-all-mixins T Factory ML tt Clauses CFL,
395399
std.map-filter Clauses (mixin-src->has-mixin-instance ) ClausesHas,
396-
ClausesHas => declare-all T {findall-classes-for ML} CCSL, % declare-all-on-type-constructor doesn't work here
400+
ClausesHas => declare-all T {findall-classes-for ML} CSL, % declare-all-on-type-constructor doesn't work here
397401
]
398402
],
399-
std.append MCSL CCSL CSL
400403
].
401404

402405
% If you don't mention the factory in a builder, then Coq won't make

‎HB/structures.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -772,7 +772,7 @@ Elpi Accumulate lp:{{
772772

773773
:name "start"
774774
main [const-decl Name (some BodySkel) TyWPSkel] :- !,
775-
with-attributes (with-logging (instance.declare-const Name BodySkel TyWPSkel _)).
775+
with-attributes (with-logging (instance.declare-const Name BodySkel TyWPSkel _ _)).
776776
main [T0, F0] :- !,
777777
coq.warning "HB" "HB.deprecated" "The syntax \"HB.instance Key FactoryInstance\" is deprecated, use \"HB.instance Definition\" instead",
778778
with-attributes (with-logging (instance.declare-existing T0 F0)).

‎Makefile.test-suite.coq.local‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,9 @@ DIFF=\
1010
@if [ -z "$$COQ_ELPI_ATTRIBUTES" ]; then \
1111
echo OUTPUT DIFF $(1);\
1212
$(COQTOP) $(COQFLAGS) $(COQLIBS) -topfile $(1) \
13-
< $(1) 2>/dev/null \
13+
< $(1) 2>&1 \
14+
| sed 's/Coq < *//g' \
15+
| grep -v '^$$' \
1416
| grep -v -e "Skipping rcfile" -e "is declared" -e "is defined" -e "Loading ML file" -e "Welcome to Coq" \
1517
| sed 's/characters \([0-9]\+\)-[0-9]\+/character \1/' \
1618
> $(1).out.aux;\
@@ -28,3 +30,4 @@ post-all::
2830
$(call DIFF, tests/hnf.v)
2931
$(call DIFF, tests/err_miss_dep.v)
3032
$(call DIFF, tests/err_bad_mix.v)
33+
$(call DIFF, tests/err_instance_nop.v)

‎tests/about.v.out‎

Lines changed: 6 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,6 @@ HB: AddMonoid_of_TYPE operations and axioms are:
99
HB: AddMonoid_of_TYPE requires the following mixins:
1010
HB: AddMonoid_of_TYPE provides the following mixins:
1111
- AddMonoid_of_TYPE
12-
1312
HB: AddMonoid_of_TYPE.Build is a factory constructor
1413
(from "./examples/demo1/hierarchy_5.v", line 10)
1514
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
2221
- addrA : associative add
2322
- add0r : left_id 0%G add
2423
- addr0 : right_id 0%G add
25-
2624
HB: AddAG.type is a structure (from "./examples/demo1/hierarchy_5.v", line 73)
2725
HB: AddAG.type characterizing operations and axioms are:
2826
- addNr
@@ -36,7 +34,6 @@ HB: AddAG inherits from:
3634
- AddComoid
3735
HB: AddAG is inherited by:
3836
- Ring
39-
4037
HB: AddMonoid.type is a structure
4138
(from "./examples/demo1/hierarchy_5.v", line 17)
4239
HB: AddMonoid.type characterizing operations and axioms are:
@@ -54,7 +51,6 @@ HB: AddMonoid is inherited by:
5451
- BiNearRing
5552
- SemiRing
5653
- Ring
57-
5854
HB: Ring_of_AddAG is a factory
5955
(from "./examples/demo1/hierarchy_5.v", line 108)
6056
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
7874
in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics
7975
and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht,
8076
1995).
81-
8277
HB: Ring_of_AddAG.Build is a factory constructor
8378
(from "./examples/demo1/hierarchy_5.v", line 108)
8479
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
10398
in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics
10499
and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht,
105100
1995).
106-
107101
HB: add is an operation of structure AddMonoid
108102
(from "./examples/demo1/hierarchy_5.v", line 17)
109103
HB: add comes from mixin AddMonoid_of_TYPE
110104
(from "./examples/demo1/hierarchy_5.v", line 10)
111-
112105
HB: AddAG.sort is a canonical projection
113106
(from "./examples/demo1/hierarchy_5.v", line 73)
114107
HB: AddAG.sort has the following canonical values:
115108
- Ring.sort (from "./examples/demo1/hierarchy_5.v", line 196)
116109
- Z
117-
118110
HB: AddAG.sort is a coercion from AddAG to Sortclass
119111
(from "./examples/demo1/hierarchy_5.v", line 73)
120-
121112
HB: Z is canonically equipped with structures:
122113
- AddMonoid
123114
AddComoid
@@ -127,13 +118,16 @@ HB: Z is canonically equipped with structures:
127118
SemiRing
128119
Ring
129120
(from "(stdin)", line 10)
130-
131121
HB: hierarchy_5_Ring_class__to__hierarchy_5_SemiRing_class is a coercion from
132122
Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196)
133-
134123
HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from
135124
Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196)
136-
125+
Toplevel input, character 15:
126+
> HB.about Builders_40.hierarchy_5_Ring_of_AddAG__to__hierarchy_5_BiNearRing_of_AddMonoid.
127+
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
128+
Error:
129+
HB: unable to locate
130+
Builders_40.hierarchy_5_Ring_of_AddAG__to__hierarchy_5_BiNearRing_of_AddMonoid
137131
HB: synthesized in file File "(stdin)", line 5, column 0, character 127:
138132
Interactive Module hierarchy_5 started
139133
Interactive Module AddComoid started
@@ -146,4 +140,3 @@ HB: Z is canonically equipped with structures:
146140
SemiRing
147141
Ring
148142
(from "(stdin)", line 10)
149-

‎tests/compress_coe.v.out‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,5 +17,4 @@ fun D D' : D.type =>
1717
|}
1818
|}
1919
: D.type -> D.type -> D.type
20-
2120
Arguments Datatypes_prod__canonical__compress_coe_D D D'

‎tests/err_instance_nop.v‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
From HB Require Import structures.
2+
3+
HB.mixin Record M T := {}.
4+
HB.structure Definition S := { x of M x }.
5+
HB.instance Definition _ : M nat := M.Build nat.
6+
HB.instance Definition _ : M nat := M.Build nat.

‎tests/err_instance_nop.v.out‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
Toplevel input, character 155:
2+
Warning: HB: no new instance is generated
3+
[HB.no-new-instance,HB,elpi,default]

‎tests/err_miss_dep.v.out‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,9 @@
1+
Toplevel input, character 0:
2+
> HB.structure Definition AbelianGrp := { A of IsAbelianGrp A }.
3+
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
4+
Warning:
5+
pulling in dependencies: [err_miss_dep_IsAddComoid]
6+
Please list them or end the declaration with '&'
7+
[HB.implicit-structure-dependency,HB,elpi,default]
18
The command has indeed failed with message:
29
HB: Unable to find mixin err_miss_dep_IsAddComoid on subject K

‎tests/howto.v.out‎

Lines changed: 0 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -8,18 +8,14 @@ HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
88
- AddComoid_of_TYPE; AddAG_of_AddComoid; Ring_of_AddAG
99
- AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid
1010
- AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid
11-
1211
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
13-
1412
HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
1513
- Ring_of_TYPE
1614
- AddAG_of_TYPE; BiNearRing_of_AddMonoid
1715
- AddAG_of_TYPE; Ring_of_AddAG
1816
- AddAG_of_TYPE; SemiRing_of_AddComoid
1917
- AddComoid_of_TYPE; Ring_of_AddComoid
20-
2118
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
22-
2319
HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
2420
- Ring_of_TYPE
2521
- 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):
3026
- AddComoid_of_TYPE; AddAG_of_AddComoid; Ring_of_AddAG
3127
- AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid
3228
- AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid
33-
3429
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
35-
3630
HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
3731
- Ring_of_TYPE
3832
- AddAG_of_TYPE; BiNearRing_of_AddMonoid
3933
- AddAG_of_TYPE; Ring_of_AddAG
4034
- AddAG_of_TYPE; SemiRing_of_AddComoid
4135
- AddComoid_of_TYPE; Ring_of_AddComoid
42-
4336
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
44-
4537
The command has indeed failed with message:
4638
HB: no solution found, try to increase search depth.
4739
HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
4840
- Ring_of_AddComoid
4941
- AddAG_of_AddComoid; BiNearRing_of_AddMonoid
5042
- AddAG_of_AddComoid; Ring_of_AddAG
5143
- AddAG_of_AddComoid; SemiRing_of_AddComoid
52-
5344
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
54-
5545
HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
5646
- BiNearRing_of_AddMonoid
5747
- Ring_of_AddAG
5848
- SemiRing_of_AddComoid
59-
6049
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
61-
6250
HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
6351
- BiNearRing_of_AddMonoid
6452
- Ring_of_AddAG
6553
- SemiRing_of_AddComoid
66-
6754
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
68-
6955
HB: nothing to do.

‎tests/missing_join_error.v.out‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,10 @@
1+
Toplevel input, character 0:
2+
> HB.structure Definition B2 := {M of isB2 M & isA2 M }.
3+
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
4+
Warning:
5+
pulling in dependencies: [missing_join_error_isTop]
6+
Please list them or end the declaration with '&'
7+
[HB.implicit-structure-dependency,HB,elpi,default]
18
The command has indeed failed with message:
29
You must declare the hierarchy bottom-up or add a missing join.
310
There are two ways out:

0 commit comments

Comments
 (0)