Merge pull request #480 from math-comp/fix-error-miss

detect bogus #[key] attribute

Author: CohenCyril

HB/factory.elpi

@@ -96,19 +96,26 @@ kind asset type.
 type asset-mixin asset.
 type asset-factory asset.
 
+pred check-key-attribute-consistency i:id.
+check-key-attribute-consistency _ :- not(get-option "key" _), !.
+check-key-attribute-consistency ID :- get-option "key" ID, !.
+check-key-attribute-consistency ID :- get-option "key" ID1,
+  coq.error "HB:" {calc ("The #[key=\"" ^ ID1 ^ "\"] attribute")}
+    "does not match the selected subject" ID.
+
 pred is-key i:indt-decl.
 pred is-key i:arity.
 pred is-key i:context-decl.
-is-key (parameter _ _ _ _\ record _ _ _ _) :- !.
-is-key (parameter _ _ _ _\ inductive _ _ _ _) :- !.
-is-key (parameter _ _ _ _\ arity _) :- !.
-is-key (context-item _ _ _ _ _\ context-end) :- !.
+is-key (parameter ID _ _ _\ record _ _ _ _) :- !, check-key-attribute-consistency ID.
+is-key (parameter ID _ _ _\ inductive _ _ _ _) :- !, check-key-attribute-consistency ID.
+is-key (parameter ID _ _ _\ arity _) :- !, check-key-attribute-consistency ID.
+is-key (context-item ID _ _ _ _\ context-end) :- !, check-key-attribute-consistency ID.
 is-key (parameter ID _ _ _) :- get-option "key" ID, !.
 is-key (context-item ID _ _ _ _) :- get-option "key" ID, !.
-is-key (parameter _ _ _ p\ parameter _ _ (M p) _) :-
-  pi p\ factory? (M p) _, !.
-is-key (context-item _ _ _ _ p\ context-item _ _ (M p) _ _) :-
-  pi p\ factory? (M p) _, !.
+is-key (parameter ID _ _ p\ parameter _ _ (M p) _) :-
+  pi p\ factory? (M p) _, !, check-key-attribute-consistency ID.
+is-key (context-item ID _ _ _ p\ context-item _ _ (M p) _ _) :-
+  pi p\ factory? (M p) _, !, check-key-attribute-consistency ID.
 
 pred mixin-decl-w-mixins i:string, i:string, i:term, i:(term -> A),
   i:(A -> pair (list (w-args mixinname)) A -> prop),

Makefile.test-suite.coq.local

@@ -22,6 +22,7 @@ post-all::
 	$(call DIFF, tests/compress_coe.v)
 	$(call DIFF, tests/about.v)
 	$(call DIFF, tests/howto.v)
+	$(call DIFF, tests/err_miss_key.v)
 	$(call DIFF, tests/missing_join_error.v)
 	$(call DIFF, tests/not_same_key.v)
 	$(call DIFF, tests/hnf.v)

tests/err_miss_key.v

@@ -0,0 +1,4 @@
+From HB Require Import structures.
+
+Fail #[key="Tmiss"]
+HB.mixin Record Foo T := {}.

tests/err_miss_key.v.out

@@ -0,0 +1,2 @@
+The command has indeed failed with message:
+HB: The #[key="Tmiss"] attribute does not match the selected subject T