attlabel

Changelog.md

@@ -3,6 +3,8 @@
 ## UNRELEASED
 
 ### API
+- New `coq.parse-attributes` support for the `attlabel` specification,
+  see `coq-lib-common.elpi` for its documentation.
 - New `coq.goal->pp`
 
 ## [2.0.2] - 01/02/2024

elpi/coq-lib-common.elpi

@@ -67,8 +67,9 @@ type int attribute-type.
 type string attribute-type.
 type bool attribute-type.
 type oneof list attribute-mapping -> attribute-type.
-type attmap attribute-type.
-type attlist attribute-type.
+type attmap attribute-type.    % #[map(k1="v1",k2="v2")]
+type attlist attribute-type.   % #[set(b1,b2,b3)]
+type attlabel attribute-type.    % #[label( a(..), b, .. )] if #[label(a, b), a(..), ..]
 type loc attribute-type.
 
 kind attribute-mapping type.
@@ -123,6 +124,9 @@ pred append-string i:string, i:string, o:string.
 append-string "" A A :- !.
 append-string A B R :- R is A ^ "." ^ B.
 
+pred keep-only-label i:attribute, o:attribute.
+keep-only-label (attribute L _) (attribute L (leaf-str "")).
+
 coq.parse-attributes L S O :-
   std.map S (x\r\ r = supported-attribute x) CS,
   CS => parse-attributes.aux L "" O, !.
@@ -137,6 +141,13 @@ parse-attributes.aux [attribute S (node L)|AS] Prefix R :-
   parse-attributes.aux AS Prefix R1,
   (pi x\ supported-attribute (att x string) :- !) => parse-attributes.aux L "" Map,
   std.append R1 [get-option PS Map] R.
+parse-attributes.aux [attribute S (node L)|AS] Prefix R :- 
+  append-string Prefix S PS, supported-attribute (att PS attlabel), !,
+  parse-attributes.aux AS Prefix R1,
+  std.map L keep-only-label Ll,
+  (pi x\ supported-attribute (att x bool) :- !) => parse-attributes.aux Ll "" Map,
+  parse-attributes.aux L Prefix R2,
+  std.append R1 [get-option PS Map|R2] R.
 parse-attributes.aux [attribute S (node L)|AS] Prefix R :- !,
   parse-attributes.aux AS Prefix R1,
   append-string Prefix S PS,

tests/test_vernacular1.v

@@ -44,7 +44,7 @@
 
 }}.
 Elpi Typecheck.
 #[foo="bar"]
 Elpi test.att.
 
 Elpi Export test.att.
@@ -72,3 +72,27 @@
 }}.
 Elpi test.scope (_ * _)%type.
 Fail Elpi test.scope ((_ * _)%type).
+
+Elpi Command test_attlabel.
+Elpi Accumulate lp:{{
+  main _ :-
+    attributes A,
+    coq.parse-attributes A [
+      att "only" attlabel,
+      att "foo.x" string,
+      att "foo.y" bool,
+      ] CL,
+    CL = [get-option "elpi.loc" _, get-option "elpi.phase" _,
+          get-option "only" [get-option "foo" tt],
+          get-option "foo.x" "a",
+          get-option "foo.y" ff].
+}}.
+Elpi Typecheck.
+Elpi Export test_attlabel.
+
+#[only(foo(x="a",y=no))] test_attlabel.
+
+
+
+
+