attlabel

Author: gares

Changelog.md

@@ -1,5 +1,11 @@
 # Changelog
 
+## UNRELEASED
+
+### API
+- New `coq.parse-attributes` support for the `attlabel` specification,
+  see `coq-lib-common.elpi` for its documentation.
+
 ## [2.0.2] - 01/02/2024
 
 Requires Elpi 1.18.2 and Coq 8.19.

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

@@ -72,3 +72,27 @@ Elpi Accumulate lp:{{
 }}.
 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.
+
+
+
+
+