Command driven attributes.

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

7 files changed, 216 insertions, 94 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
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index b9191c3f3e..5b03c26cb1 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -8,10 +8,34 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Vernacexpr
+
+type 'a attribute
+(** The type of attributes. When parsing attributes if an ['a
+   attribute] is present then an ['a] value will be produced. *)
+
+val parse : 'a attribute -> vernac_flags -> 'a
+(** Errors on unsupported attributes. *)
+
+module Notations : sig
+  (** Notations to combine attributes. *)
+
+  val (++) : 'a attribute -> 'b attribute -> ('a * 'b) attribute
+  (** Combine 2 attributes. If any keys are in common an error will be raised. *)
+end
+
+(** Definitions for some standard attributes. *)
+
 type deprecation = { since : string option ; note : string option }
 
 val mk_deprecation : ?since: string option -> ?note: string option -> unit -> deprecation
 
+val polymorphic : bool option attribute
+val program : bool option attribute
+val template : bool option attribute
+val locality : bool option attribute
+val deprecation : deprecation option attribute
+
 type t = {
   locality : bool option;
   polymorphic : bool;
@@ -19,10 +43,58 @@ type t = {
   program : bool;
   deprecated : deprecation option;
 }
+(** Some attributes gathered in a adhoc record. Will probably be
+   removed at some point. *)
+
+val attributes_of_flags : vernac_flags -> t
+(** Parse the attributes supported by type [t]. Errors on other
+   attributes. Polymorphism and Program use the global flags as
+   default values. *)
+
+val only_locality : vernac_flags -> bool option
+(** Parse attributes allowing only locality. *)
+
+val only_polymorphism : vernac_flags -> bool
+(** Parse attributes allowing only polymorphism.
+    Uses the global flag for the default value. *)
+
+val parse_drop_extra : 'a attribute -> vernac_flags -> 'a
+(** Ignores unsupported attributes. *)
+
+val parse_with_extra : 'a attribute -> vernac_flags -> 'a * vernac_flags
+(** Returns unsupported attributes. *)
+
+(** * Defining attributes. *)
+
+type 'a key_parser = 'a option -> Vernacexpr.vernac_flag_value -> 'a
+(** A parser for some key in an attribute. It is given a nonempty ['a
+    option] when the attribute is multiply set for some command.
+
+    eg in [#[polymorphic] Monomorphic Definition foo := ...], when
+   parsing [Monomorphic] it will be given [Some true]. *)
+
+val attribute_of_list : (string * 'a key_parser) list -> 'a option attribute
+(** Make an attribute from a list of key parsers together with their
+   associated key. *)
+
+val bool_attribute : name:string -> on:string -> off:string -> bool option attribute
+(** Define boolean attribute [name] with value [true] when [on] is
+   provided and [false] when [off] is provided. The attribute may only
+   be set once for a command. *)
+
+(** Combinators to help define your own parsers. See the
+   implementation of [bool_attribute] for practical use. *)
+
+val assert_empty : string -> vernac_flag_value -> unit
+(** [assert_empty key v] errors if [v] is not empty. [key] is used in
+   the error message as the name of the attribute. *)
 
-val mk_atts :
-  ?polymorphic: bool ->
-  ?program: bool -> unit -> t
+val assert_once : name:string -> 'a option -> unit
+(** [assert_once ~name v] errors if [v] is not empty. [name] is used
+   in the error message as the name of the attribute. Used to ensure
+   that a given attribute is not reapeated. *)
 
-val attributes_of_flags : Vernacexpr.vernac_flags -> t ->
-  bool option (* polymorphism attr *) * t
+val single_key_parser : name:string -> key:string -> 'a -> 'a key_parser
+(** [single_key_parser ~name ~key v] makes a parser for attribute
+    [name] giving the constant value [v] for key [key] taking no
+    arguments. [name] may only be given once. *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 12feb07051..b02d482761 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2109,7 +2109,6 @@ let vernac_load interp fname =
  * still parsed as the obsolete_locality grammar entry for retrocompatibility.
  * loc is the Loc.t of the vernacular command being interpreted. *)
 let interp ?proof ~atts ~st c =
-  vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
   match c with
 
   (* Loading a file requires access to the control interpreter *)
@@ -2259,11 +2258,7 @@ let interp ?proof ~atts ~st c =
     Option.iter vernac_set_used_variables using
   | VernacProofMode mn -> Proof_global.set_proof_mode mn [@ocaml.warning "-3"]
 
-  (* Extensions *)
-  | VernacExtend (opn,args) ->
-    (* XXX: Here we are returning the state! :) *)
-    let _st : Vernacstate.t = Vernacinterp.call ~atts opn args ~st in
-    ()
+  | VernacExtend _ -> assert false
 
 (* Vernaculars that take a locality flag *)
 let check_vernac_supports_locality c l =
@@ -2291,6 +2286,21 @@ let check_vernac_supports_locality c l =
     | VernacInductive _) -> ()
   | Some _, _ -> user_err Pp.(str "This command does not support Locality")
 
+
+let interp  ?proof ~atts ~st c =
+  vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
+  match c with
+  (* Extensions *)
+  | VernacExtend (opn,args) ->
+    (* XXX: Here we are returning the state! :) *)
+    let _st : Vernacstate.t = Vernacinterp.call ~atts opn args ~st in
+    ()
+
+  | _ ->
+    let atts = Attributes.attributes_of_flags atts in
+    check_vernac_supports_locality c atts.locality;
+    interp ?proof ~atts ~st c
+
 (* Vernaculars that take a polymorphism flag *)
 let check_vernac_supports_polymorphism c p =
   match p, c with
@@ -2374,9 +2384,8 @@ let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} =
   let orig_univ_poly = Flags.is_universe_polymorphism () in
   let orig_program_mode = Flags.is_program_mode () in
   let rec control = function
-  | VernacExpr (f, v) ->
-    let (polymorphism, atts) = attributes_of_flags f (mk_atts ~program:orig_program_mode ()) in
-    aux ~polymorphism ~atts v
+  | VernacExpr (atts, v) ->
+    aux ~atts v
   | VernacFail v -> with_fail st true (fun () -> control v)
   | VernacTimeout (n,v) ->
     current_timeout := Some n;
@@ -2386,28 +2395,28 @@ let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} =
   | VernacTime (batch, {v}) ->
     System.with_time ~batch control v;
 
-  and aux ~polymorphism ~atts : _ -> unit =
+  and aux ~atts : _ -> unit =
     function
 
     | VernacLoad (_,fname) -> vernac_load control fname
 
     | c ->
-      check_vernac_supports_locality c atts.locality;
-      check_vernac_supports_polymorphism c polymorphism;
-      let polymorphic = Option.default (Flags.is_universe_polymorphism ()) polymorphism in
-      Flags.make_universe_polymorphism polymorphic;
-      Obligations.set_program_mode atts.program;
+      let poly, program = Attributes.(parse_drop_extra Notations.(polymorphic ++ program) atts) in
+      (* NB: we keep polymorphism and program in the attributes, we're
+         just parsing them to do our option magic. *)
+      check_vernac_supports_polymorphism c poly;
+      Option.iter Flags.make_universe_polymorphism poly;
+      Option.iter Obligations.set_program_mode program;
       try
         vernac_timeout begin fun () ->
-          let atts = { atts with polymorphic } in
           if verbosely
           then Flags.verbosely (interp ?proof ~atts ~st) c
           else Flags.silently  (interp ?proof ~atts ~st) c;
           (* If the command is `(Un)Set Program Mode` or `(Un)Set Universe Polymorphism`,
              we should not restore the previous state of the flag... *)
-          if orig_program_mode || not !Flags.program_mode || atts.program then
+          if Option.has_some program then
             Flags.program_mode := orig_program_mode;
-          if (Flags.is_universe_polymorphism() = polymorphic) then
+          if Option.has_some poly then
             Flags.make_universe_polymorphism orig_univ_poly;
           end
         with
@@ -2446,7 +2455,7 @@ open Extend
 type classifier = Genarg.raw_generic_argument list -> vernac_classification
 
 type (_, _) ty_sig =
-| TyNil : (atts:Attributes.t -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
+| TyNil : (atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
 | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
 | TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig
 
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index f95bdaa539..3aa4ec12c0 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -44,7 +44,7 @@ val universe_polymorphism_option_name : string list
 type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification
 
 type (_, _) ty_sig =
-| TyNil : (atts:Attributes.t -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
+| TyNil : (atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
 | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
 | TyNonTerminal :
   ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig ->
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 27b485d94d..594e9eca48 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -395,7 +395,8 @@ type nonrec vernac_expr =
   (* For extension *)
   | VernacExtend of extend_name * Genarg.raw_generic_argument list
 
-type vernac_flags = (string * vernac_flag_value) list
+type vernac_flags = vernac_flag list
+and vernac_flag = string * vernac_flag_value
 and vernac_flag_value =
   | VernacFlagEmpty
   | VernacFlagLeaf of string
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index b16784eb22..eb4282705e 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -12,7 +12,7 @@ open Util
 open Pp
 open CErrors
 
-type 'a vernac_command = 'a -> atts:Attributes.t -> st:Vernacstate.t -> Vernacstate.t
+type 'a vernac_command = 'a -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
 
 type plugin_args = Genarg.raw_generic_argument list
 
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index ba3d911810..0fc02c6915 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -10,7 +10,7 @@
 
 (** Interpretation of extended vernac phrases. *)
 
-type 'a vernac_command = 'a -> atts:Attributes.t -> st:Vernacstate.t -> Vernacstate.t
+type 'a vernac_command = 'a -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
 
 type plugin_args = Genarg.raw_generic_argument list
 
@@ -18,4 +18,4 @@ val vinterp_init : unit -> unit
 val vinterp_add : bool -> Vernacexpr.extend_name -> plugin_args vernac_command -> unit
 val overwriting_vinterp_add : Vernacexpr.extend_name -> plugin_args vernac_command -> unit
 
-val call : Vernacexpr.extend_name -> plugin_args -> atts:Attributes.t -> st:Vernacstate.t -> Vernacstate.t
+val call : Vernacexpr.extend_name -> plugin_args -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t