Command driven attributes.

Commands need to request the attributes they use, with the API
encouraging them to error on unsupported attributes.

1 files changed, 105 insertions, 65 deletions

diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index c93ff2a63a..b35a4428f9 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -11,6 +11,55 @@
 open CErrors
 open Vernacexpr
 
+let unsupported_attributes ?loc = function
+  | [] -> ()
+  | atts ->
+    let keys = List.map fst atts in
+    let keys = List.sort_uniq String.compare keys in
+    let conj = match keys with [_] -> "this attribute: " | _ -> "these attributes: " in
+    user_err ?loc Pp.(str "This command does not support " ++ str conj ++ prlist str keys ++ str".")
+
+type 'a key_parser = 'a option -> Vernacexpr.vernac_flag_value -> 'a
+
+type 'a attribute = ('a -> Vernacexpr.vernac_flag_value -> 'a) CString.Map.t * 'a
+
+let parse_drop_extra (p,v:'a attribute) (atts:vernac_flags) : 'a =
+  List.fold_left (fun v (k,args) ->
+      match CString.Map.find k p with
+      | exception Not_found -> v
+      | parser -> parser v args)
+    v atts
+
+let parse_with_extra (p,v:'a attribute) (atts:vernac_flags) : 'a * vernac_flags =
+  let v, extra = List.fold_left (fun (v,extra) (k,args as att) ->
+      match CString.Map.find k p with
+      | exception Not_found -> (v,att::extra)
+      | parser -> (parser v args, extra))
+      (v,[]) atts
+  in
+  v, List.rev extra
+
+let parse (p:'a attribute) atts : 'a =
+  let v, extra = parse_with_extra p atts in
+  unsupported_attributes extra;
+  v
+
+module Notations = struct
+
+  let (++) (p1,v1:'a attribute) (p2,v2:'b attribute) : ('a*'b) attribute =
+    let p = CString.Map.merge (fun key p1 p2 -> match p1, p2 with
+        | Some p1, None -> Some (fun (x,y) args -> (p1 x args, y))
+        | None, Some p2 -> Some (fun (x,y) args -> (x, p2 y args))
+        | None, None -> None
+        | Some _, Some _ ->
+          anomaly Pp.(str "Attribute collision on " ++ str key))
+        p1 p2
+    in
+    p, (v1, v2)
+
+end
+open Notations
+
 type deprecation = { since : string option ; note : string option }
 
 let mk_deprecation ?(since=None) ?(note=None) () =
@@ -24,71 +73,62 @@ type t = {
   deprecated : deprecation option;
 }
 
-let default = {
-  locality = None;
-  polymorphic = false;
-  template = None;
-  program = false;
-  deprecated = None;
-}
+let assert_empty k v =
+  if v <> VernacFlagEmpty
+  then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments")
 
-let mk_atts ?(polymorphic=default.polymorphic) ?(program=default.program) () =
-  { default with polymorphic; program }
+let assert_once ~name prev =
+  if Option.has_some prev then
+    user_err Pp.(str "Attribute for " ++ str name ++ str " specified twice.")
 
-let attributes_of_flags f atts =
-  let assert_empty k v =
-    if v <> VernacFlagEmpty
-    then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments")
+let attribute_of_list (l:(string * 'a key_parser) list) : 'a option attribute =
+  List.fold_left (fun acc (k,p) -> CString.Map.add k (fun prev args -> Some (p prev args)) acc)
+    CString.Map.empty l, None
+
+let single_key_parser ~name ~key v prev args =
+  assert_empty key args;
+  assert_once ~name prev;
+  v
+
+let bool_attribute ~name ~on ~off : bool option attribute =
+  attribute_of_list [(on, single_key_parser ~name ~key:on true);
+               (off, single_key_parser ~name ~key:off false)]
+
+let polymorphic = bool_attribute ~name:"Polymorphism" ~on:"polymorphic" ~off:"monomorphic"
+
+let program = bool_attribute ~name:"Program mode" ~on:"program" ~off:"noprogram"
+
+let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global"
+
+let template = bool_attribute ~name:"Template" ~on:"template" ~off:"notemplate"
+
+let deprecation_parser : deprecation key_parser = fun orig args ->
+  assert_once ~name:"deprecation" orig;
+  match args with
+  | VernacFlagList [ "since", VernacFlagLeaf since ; "note", VernacFlagLeaf note ]
+  | VernacFlagList [ "note", VernacFlagLeaf note ; "since", VernacFlagLeaf since ] ->
+    let since = Some since and note = Some note in
+    mk_deprecation ~since ~note ()
+  | VernacFlagList [ "since", VernacFlagLeaf since ] ->
+    let since = Some since in
+    mk_deprecation ~since ()
+  | VernacFlagList [ "note", VernacFlagLeaf note ] ->
+    let note = Some note in
+    mk_deprecation ~note ()
+  |  _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute")
+
+let deprecation = attribute_of_list ["deprecated",deprecation_parser]
+
+let attributes_of_flags f =
+  let (((locality, template), deprecated), polymorphic), program =
+    parse (locality ++ template ++ deprecation ++ polymorphic ++ program) f
   in
-  List.fold_left
-    (fun (polymorphism, atts) (k, v) ->
-       match k with
-       | "program" when not atts.program ->
-         assert_empty k v;
-         (polymorphism, { atts with program = true })
-       | "program" ->
-         user_err Pp.(str "Program mode specified twice")
-       | "polymorphic" when polymorphism = None ->
-         assert_empty k v;
-         (Some true, atts)
-       | "monomorphic" when polymorphism = None ->
-         assert_empty k v;
-         (Some false, atts)
-       | ("polymorphic" | "monomorphic") ->
-         user_err Pp.(str "Polymorphism specified twice")
-       | "template" when atts.template = None ->
-         assert_empty k v;
-         polymorphism, { atts with template = Some true }
-       | "notemplate" when atts.template = None ->
-         assert_empty k v;
-         polymorphism, { atts with template = Some false }
-       | "template" | "notemplate" ->
-         user_err Pp.(str "Templateness specified twice")
-       | "local" when Option.is_empty atts.locality ->
-         assert_empty k v;
-         (polymorphism, { atts with locality = Some true })
-       | "global" when Option.is_empty atts.locality ->
-         assert_empty k v;
-         (polymorphism, { atts with locality = Some false })
-       | ("local" | "global") ->
-         user_err Pp.(str "Locality specified twice")
-       | "deprecated" when Option.is_empty atts.deprecated ->
-           begin match v with
-             | VernacFlagList [ "since", VernacFlagLeaf since ; "note", VernacFlagLeaf note ]
-             | VernacFlagList [ "note", VernacFlagLeaf note ; "since", VernacFlagLeaf since ] ->
-               let since = Some since and note = Some note in
-               (polymorphism, { atts with deprecated = Some (mk_deprecation ~since ~note ()) })
-             | VernacFlagList [ "since", VernacFlagLeaf since ] ->
-               let since = Some since in
-               (polymorphism, { atts with deprecated = Some (mk_deprecation ~since ()) })
-             | VernacFlagList [ "note", VernacFlagLeaf note ] ->
-               let note = Some note in
-               (polymorphism, { atts with deprecated = Some (mk_deprecation ~note ()) })
-             |  _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute")
-           end
-       | "deprecated" ->
-         user_err Pp.(str "Deprecation specified twice")
-       | _ -> user_err Pp.(str "Unknown attribute " ++ str k)
-    )
-    (None, atts)
-    f
+  let polymorphic = Option.default (Flags.is_universe_polymorphism()) polymorphic in
+  let program = Option.default (Flags.is_program_mode()) program in
+  { polymorphic; program; locality; template; deprecated }
+
+let only_locality atts = parse locality atts
+
+let only_polymorphism atts =
+  let att = parse polymorphic atts in
+  Option.default (Flags.is_universe_polymorphism ()) att