clean up attribute handling for elpi.loc

Changelog.md

@@ -1,5 +1,15 @@
 # Changelog
 
+## [1.10.3] - 18-06-2021
+
+Requires Elpi 1.13.6 and Coq 8.13.
+
+### Lib
+- Cleanup `elpi.loc` attribute, which now carries a real loc and not a string.
+  Thanks to elpi 1.13.6 we can project out the components without messing
+  with regular expressions. Moreover loc are printed in a consistent way on
+  Unix and Windows.
+
 ## [1.10.2] - 11-06-2021
 
 Requires Elpi 1.13.5 and Coq 8.13.

coq-builtin.elpi

@@ -929,7 +929,8 @@ external pred coq.notation.abbreviation-body i:abbreviation, o:int,
 
 % Generic attribute value
 kind attribute-value type.
-type leaf string -> attribute-value.
+type leaf-str string -> attribute-value.
+type leaf-loc loc -> attribute-value.
 type node list attribute -> attribute-value.
 
 % Generic attribute

coq-elpi.opam

@@ -13,7 +13,7 @@ build: [ [ make "build"   "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" "OCAML
        ]
 install: [ make "install" "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" ]
 depends: [
-  "elpi" {>= "1.13.5" & < "1.14.0~"}
+  "elpi" {>= "1.13.6" & < "1.14.0~"}
   "coq" {>= "8.13" & < "8.14~" }
   ]
 tags: [ "logpath:elpi" ]

elpi-builtin.elpi

@@ -274,6 +274,10 @@ external pred quote_syntax i:string, i:string, o:list A, o:A.
 typeabbrev loc (ctype "Loc.t").
 
 
+% [loc.fields Loc File StartChar StopChar Line LineStartsAtChar] Decomposes
+% a loc into its fields
+external pred loc.fields i:loc, o:string, o:int, o:int, o:int, o:int.
+
 % == Regular Expressions =====================================
 
 % [rex.match Rex Subject] checks if Subject matches Rex. Matching is based
@@ -373,6 +377,14 @@ primitive? X S :- is_cdata X (ctype S).
 % of N are guaranteed to be incresing.
 external pred new_int o:int.
 
+% [findall_solution P L] finds all the solved instances of P and puts them
+% in L
+% in the order in which they are found. Instances can contain
+% eigenvariables
+% and unification variables.
+
+external pred findall_solutions i:prop, o:list prop.
+
 % Holds data across bracktracking; can only contain closed terms
 typeabbrev safe (ctype "safe").
 
@@ -691,11 +703,8 @@ max N M N :- N >= M, !.
 max _ M M.
 
 % [findall P L] L is the list [P1,P2,P3..] where each Pi is a solution to P.
-% Solutions must be closed (no unification variables nor eigenvariables).
 pred findall i:prop, o:list prop.
-findall P L :- new_safe F, findall.aux P F, open_safe F L.
-findall.aux P F :- P, stash_in_safe F P, fail.
-findall.aux _ _.
+findall P L :- findall_solutions P L.
 
 }
 

elpi/coq-lib.elpi

@@ -525,6 +525,7 @@ type att string -> attribute-type -> attribute-signature.
 type att-ignore-unknown attribute-signature.
 
 type supported-attribute attribute-signature -> prop.
+supported-attribute (att "elpi.loc" loc).
 supported-attribute (att Name string) :- rex_match "^elpi\\." Name.
 
 kind attribute-type type.
@@ -533,16 +534,23 @@ type string attribute-type.
 type bool attribute-type.
 type oneof list attribute-mapping -> attribute-type.
 type attmap attribute-type.
+type loc attribute-type.
 
 kind attribute-mapping type.
 type (`->) string -> any -> attribute-mapping.
 
-pred coq.valid-attribute i:string, i:string, o:option any, o:diagnostic.
-coq.valid-attribute Name Value V Diag :-
+pred coq.valid-str-attribute i:string, i:string, o:option any, o:diagnostic.
+coq.valid-str-attribute Name Value V Diag :-
   if (supported-attribute (att Name Type))
      (coq.typecheck-attribute Name Type Value LPV Diag, V = some LPV)
      (if (supported-attribute att-ignore-unknown) (V = none, Diag = ok)
          (Diag = error {calc ( "Attribute " ^ Name ^ " is not supported")})).
+pred coq.valid-loc-attribute i:string, i:loc, o:diagnostic.
+coq.valid-loc-attribute Name Loc Diag :-
+  if (supported-attribute (att Name loc))
+     (if (primitive? Loc "Loc.t") (Diag = ok) (Diag = error {calc ( "Attribute " ^ Name ^ " takes a loc, got " ^ {std.any->string Loc} ) } ))
+     (if (supported-attribute att-ignore-unknown) (Diag = ok)
+         (Diag = error {calc ( "Attribute " ^ Name ^ " is not supported")})).
 
 :index (_ 1 1)
 pred coq.typecheck-attribute i:string, o:attribute-type, i:string, o:any, o:diagnostic.
@@ -591,10 +599,15 @@ parse-attributes.aux [attribute S (node L)|AS] Prefix R :- !,
   if (Prefix = "") (PS = S) (PS is Prefix ^ "." ^ S),
   parse-attributes.aux L PS R2,
   std.append R1 R2 R.
-parse-attributes.aux [attribute S (leaf V)|AS] Prefix CLS :- !,
+parse-attributes.aux [attribute S (leaf-str V)|AS] Prefix CLS :- !,
   if (Prefix = "") (PS = S) (PS is Prefix ^ "." ^ S),
-  coq.valid-attribute PS V V1 Diag,
+  coq.valid-str-attribute PS V V1 Diag,
   if (Diag = error Msg) (coq.error Msg) true,
   if (V1 = some Val) (CLS = [get-option PS Val|R]) (CLS = R), % ignored
   parse-attributes.aux AS Prefix R.
-
+parse-attributes.aux [attribute S (leaf-loc V)|AS] Prefix CLS :- !,
+  if (Prefix = "") (PS = S) (PS is Prefix ^ "." ^ S),
+  coq.valid-loc-attribute PS V Diag,
+  if (Diag = error Msg) (coq.error Msg) true,
+  CLS = [get-option PS V|R],
+  parse-attributes.aux AS Prefix R.

src/coq_elpi_builtins.ml

@@ -631,17 +631,36 @@ let attribute a = let open API.AlgebraicData in declare {
   ]
 } |> CConv.(!<)
 
-let attribute_value = let open API.AlgebraicData in let open Attributes in let open CConv in declare {
+type attribute_data =
+  | AttributeString of string
+  | AttributeLoc of API.Ast.Loc.t
+type attribute_value =
+  | AttributeEmpty
+  | AttributeList of (string * attribute_value) list
+  | AttributeLeaf of attribute_data
+
+let attribute_value = let open API.AlgebraicData in let open CConv in declare {
   ty = Conv.TyName "attribute-value";
   doc = "Generic attribute value";
   pp = (fun fmt a -> Format.fprintf fmt "TODO");
   constructors = [
-    K("leaf","",A(B.string,N),
-      B (fun s -> if s = "" then VernacFlagEmpty else VernacFlagLeaf (FlagString s)),
-      M (fun ~ok ~ko -> function VernacFlagEmpty -> ok "" | VernacFlagLeaf (FlagString x | FlagIdent x) -> ok x | _ -> ko ()));
+    K("leaf-str","",A(B.string,N),
+      B (fun s ->
+          if s = "" then AttributeEmpty
+          else AttributeLeaf (AttributeString s)),
+      M (fun ~ok ~ko -> function
+          | AttributeEmpty -> ok ""
+          | AttributeLeaf (AttributeString x) -> ok x
+          | _ -> ko ()));
+    K("leaf-loc","",A(B.loc,N),
+      B (fun s ->
+          AttributeLeaf (AttributeLoc s)),
+      M (fun ~ok ~ko -> function
+           | AttributeLeaf (AttributeLoc x) -> ok x
+           | _ -> ko ()));
     K("node","",C((fun self -> !> (B.list (attribute (!< self)))),N),
-      B (fun l -> VernacFlagList l),
-      M (fun ~ok ~ko -> function VernacFlagList l -> ok l | _ -> ko ())
+      B (fun l -> AttributeList l),
+      M (fun ~ok ~ko -> function AttributeList l -> ok l | _ -> ko ())
     )
   ]
 } |> CConv.(!<)

src/coq_elpi_builtins.mli

@@ -12,7 +12,15 @@ val clauses_for_later :
   (string list * Ast.program * Names.Id.t list * Coq_elpi_utils.clause_scope) list State.component
 val set_accumulate_to_db : ((string list -> Ast.program -> Names.Id.t list -> scope:Coq_elpi_utils.clause_scope -> unit)) -> unit
 
-val attribute : (string * Attributes.vernac_flag_value) Conversion.t
+type attribute_data =
+  | AttributeString of string
+  | AttributeLoc of Ast.Loc.t
+type attribute_value =
+  | AttributeEmpty
+  | AttributeList of (string * attribute_value) list
+  | AttributeLeaf of attribute_data
+
+val attribute : (string * attribute_value) Conversion.t
 
 (* In tactic mode some APIs are disabled *)
 val tactic_mode : bool ref

src/coq_elpi_vernacular.ml

@@ -596,14 +596,23 @@ let mainc = ET.Constants.declare_global_symbol "main"
 let attributesc = ET.Constants.declare_global_symbol "attributes"
 
 let atts2impl loc ~depth state atts q =
-  let atts = ("elpi.loc", Attributes.(VernacFlagLeaf (FlagString (API.Ast.Loc.show loc)))) :: atts in
+  let open Coq_elpi_builtins in
+  let rec convert_att = function
+    | (name,Attributes.VernacFlagEmpty) -> name, AttributeEmpty
+    | (name,Attributes.VernacFlagList l) -> name, AttributeList (convert_atts l)
+    | (name,Attributes.VernacFlagLeaf v) -> name, AttributeLeaf (convert_att_value v)
+  and convert_atts l = List.map convert_att l
+  and convert_att_value = function
+    Attributes.FlagIdent s | Attributes.FlagString s -> AttributeString s
+  in
+  let atts = ("elpi.loc", AttributeLeaf (AttributeLoc loc)) :: convert_atts atts in
   let atts =
     match Sys.getenv_opt "COQ_ELPI_ATTRIBUTES" with
     | None -> atts
     | Some txt ->
         match Pcoq.parse_string (Pvernac.main_entry None) (Printf.sprintf "#[%s] Qed." txt) |> Option.map (fun x -> x.CAst.v) with
         | None -> atts
-        | Some { Vernacexpr.attrs ; _ } -> List.map (fun (name,v) -> "elpi."^name,v) attrs @ atts
+        | Some { Vernacexpr.attrs ; _ } -> List.map (fun (name,v) -> convert_att ("elpi."^name,v)) attrs @ atts
         | exception Stream.Error msg ->
             CErrors.user_err ~hdr:"elpi" Pp.(str"Environment variable COQ_ELPI_ATTRIBUTES contains ill formed value:" ++ spc () ++ str txt ++ cut () ++ str msg) in
   let state, atts, _ = EU.map_acc (Coq_elpi_builtins.attribute.API.Conversion.embed ~depth) state atts in

tests/test_vernacular1.v

@@ -36,7 +36,7 @@ Elpi Accumulate lp:{{
   main _ :-
     attributes A,
     coq.say A,
-    A = [attribute "elpi.loc" _, attribute "foo" (leaf "bar")| _],
+    A = [attribute "elpi.loc" _, attribute "foo" (leaf-str "bar")| _],
     coq.parse-attributes A [att "foo" string,
                         att "poly" bool,
                         att-ignore-unknown] CL,