From 4371ff2357c11d913b163dde193255f538f3565f Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Mon, 25 Jun 2018 09:35:25 +0000 Subject: [vernac] Generic syntax for flags/attributes --- vernac/g_vernac.mlg | 42 +++++++++++++++++------------------------- vernac/ppvernac.ml | 32 +++++++++++--------------------- vernac/vernacentries.ml | 46 +++++++++++++++++++++++++++++++++------------- vernac/vernacentries.mli | 2 +- vernac/vernacexpr.ml | 12 ++++++------ 5 files changed, 68 insertions(+), 66 deletions(-) (limited to 'vernac') diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 49fcda849..92c685741 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -87,50 +87,42 @@ GRAMMAR EXTEND Gram | fv = vernac -> fv ]] ; - attributes: [[ "#[" ; a = LIST1 attribute SEP "," ; "]" -> a ]] - ; - attribute: - [[ - IDENT "polymorphic" -> VernacPolymorphic true - | IDENT "monomorphic" -> VernacPolymorphic false - | IDENT "program" -> VernacProgram - | IDENT "local" -> VernacLocal true - | IDENT "global" -> VernacLocal false - | IDENT "coercion" -> VernacCoercion - | IDENT "deprecated" ; v = attribute_value -> - match v with - | `List [ k1, `Leaf since ; k2, `Leaf note ] when Names.Id.equal k1 (Names.Id.of_string "since") && Names.Id.equal k2 (Names.Id.of_string "note") -> VernacDeprecated (since, note) - | _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute") + attributes: + [[ "#[" ; a = attribute_list ; "]" -> a ]] ; - attribute_value: - [[ "=" ; v = string -> `Leaf v - | "(" ; m = LIST0 attribute_pair SEP "," ; ")" -> `List m - | -> `Empty + attribute_list: + [[ a = LIST0 attribute SEP "," -> a ]] ; - attribute_pair: + attribute: [[ k = ident ; v = attribute_value -> (k, v) ]] ; + attribute_value: + [[ "=" ; v = string -> VernacFlagLeaf v + | "(" ; a = attribute_list ; ")" -> VernacFlagList a + | -> VernacFlagEmpty + ]] + ; vernac: - [ [ IDENT "Local"; v = vernac_poly -> { let (f, v) = v in (VernacLocal true :: f, v) } - | IDENT "Global"; v = vernac_poly -> { let (f, v) = v in (VernacLocal false :: f, v) } + [ [ IDENT "Local"; v = vernac_poly -> { let (f, v) = v in ((Names.Id.of_string "local", VernacFlagEmpty) :: f, v) } + | IDENT "Global"; v = vernac_poly -> { let (f, v) = v in ((Names.Id.of_string "global", VernacFlagEmpty) :: f, v) } | v = vernac_poly -> { v } ] ] ; vernac_poly: - [ [ IDENT "Polymorphic"; v = vernac_aux -> { let (f, v) = v in (VernacPolymorphic true :: f, v) } - | IDENT "Monomorphic"; v = vernac_aux -> { let (f, v) = v in (VernacPolymorphic false :: f, v) } + [ [ IDENT "Polymorphic"; v = vernac_aux -> { let (f, v) = v in ((Names.Id.of_string "polymorphic", VernacFlagEmpty) :: f, v) } + | IDENT "Monomorphic"; v = vernac_aux -> { let (f, v) = v in ((Names.Id.of_string "monomorphic", VernacFlagEmpty) :: f, v) } | v = vernac_aux -> { v } ] ] ; vernac_aux: (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *) (* "." is still in the stream and discard_to_dot works correctly *) - [ [ IDENT "Program"; g = gallina; "." -> { ([VernacProgram], g) } - | IDENT "Program"; g = gallina_ext; "." -> { ([VernacProgram], g) } + [ [ IDENT "Program"; g = gallina; "." -> { ([Names.Id.of_string "program", VernacFlagEmpty], g) } + | IDENT "Program"; g = gallina_ext; "." -> { ([Names.Id.of_string "program", VernacFlagEmpty], g) } | g = gallina; "." -> { ([], g) } | g = gallina_ext; "." -> { ([], g) } | c = command; "." -> { ([], c) } diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index f9237c775..024c145aa 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1193,34 +1193,24 @@ open Pputils | VernacEndSubproof -> return (str "}") -let rec pr_vernac_flag_data (k, v) = - let k = keyword k in +let rec pr_vernac_flag (k, v) = + let k = keyword (Names.Id.to_string k) in match v with - | `Empty -> k - | `Leaf v -> k ++ str " = " ++ qs v - | `Node m -> k ++ str "( " ++ prlist_with_sep (fun () -> str ", ") pr_vernac_flag_data m ++ str " )" - -let pr_vernac_flag f = - match f with - | VernacPolymorphic true -> keyword "polymorphic" - | VernacPolymorphic false -> keyword "monomorphic" - | VernacProgram -> keyword "program" - | VernacLocal true -> keyword "local" - | VernacLocal false -> keyword "global" - | VernacDeprecated (since, note) -> - pr_vernac_flag_data ("deprecated", `Node [ - "since", `Leaf since; "note", `Leaf note - ]) - -let pr_vernac_flag_list = + | VernacFlagEmpty -> k + | VernacFlagLeaf v -> k ++ str " = " ++ qs v + | VernacFlagList m -> k ++ str "( " ++ pr_vernac_flags m ++ str " )" +and pr_vernac_flags m = + prlist_with_sep (fun () -> str ", ") pr_vernac_flag m + +let pr_vernac_attributes = function | [] -> mt () - | flags -> str "#[" ++ prlist_with_sep (fun () -> str ", ") pr_vernac_flag flags ++ str "]" ++ cut () + | flags -> str "#[" ++ pr_vernac_flags flags ++ str "]" ++ cut () let rec pr_vernac_control v = let return = tag_vernac v in match v with - | VernacExpr (f, v') -> pr_vernac_flag_list f ++ pr_vernac_expr v' ++ sep_end v' + | VernacExpr (f, v') -> pr_vernac_attributes f ++ pr_vernac_expr v' ++ sep_end v' | VernacTime (_,{v}) -> return (keyword "Time" ++ spc() ++ pr_vernac_control v) | VernacRedirect (s, {v}) -> diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index af0f19834..e61687290 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2320,25 +2320,45 @@ let with_fail st b f = end 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") + in List.fold_left - (fun (polymorphism, atts) f -> - match f with - | VernacProgram when not atts.program -> + (fun (polymorphism, atts) (k, v) -> + let k = Names.Id.to_string k in + match k with + | "program" when not atts.program -> + assert_empty k v; (polymorphism, { atts with program = true }) - | VernacProgram -> + | "program" -> user_err Pp.(str "Program mode specified twice") - | VernacPolymorphic b when polymorphism = None -> - (Some b, atts) - | VernacPolymorphic _ -> + | "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") - | VernacLocal b when Option.is_empty atts.locality -> - (polymorphism, { atts with locality = Some b }) - | VernacLocal _ -> + | "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") - | VernacDeprecated (since, note) when Option.is_empty atts.deprecated -> - (polymorphism, { atts with deprecated = Some (since, note) }) - | VernacDeprecated _ -> + | "deprecated" when Option.is_empty atts.deprecated -> + begin match v with + | VernacFlagList [ k1, VernacFlagLeaf since ; k2, VernacFlagLeaf note ] + when Names.Id.(equal k1 (of_string "since") && equal k2 (of_string "note")) -> + (polymorphism, { atts with deprecated = Some (since, 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 diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 79f9b602a..79f9c05ad 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -41,4 +41,4 @@ val universe_polymorphism_option_name : string list (** Elaborate a [atts] record out of a list of flags. Also returns whether polymorphism is explicitly (un)set. *) -val attributes_of_flags : Vernacexpr.vernac_flag list -> Vernacinterp.atts -> bool option * Vernacinterp.atts +val attributes_of_flags : Vernacexpr.vernac_flags -> Vernacinterp.atts -> bool option * Vernacinterp.atts diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 57ccb6006..2287630c7 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -459,14 +459,14 @@ type nonrec vernac_expr = (* For extension *) | VernacExtend of extend_name * Genarg.raw_generic_argument list -type nonrec vernac_flag = - | VernacProgram - | VernacPolymorphic of bool - | VernacLocal of bool - | VernacDeprecated of string * string (* Since, Note *) +type vernac_flags = (Names.Id.t * vernac_flag_value) list +and vernac_flag_value = + | VernacFlagEmpty + | VernacFlagLeaf of string + | VernacFlagList of vernac_flags type vernac_control = - | VernacExpr of vernac_flag list * vernac_expr + | VernacExpr of vernac_flags * vernac_expr (* boolean is true when the `-time` batch-mode command line flag was set. the flag is used to print differently in `-time` vs `Time foo` *) | VernacTime of bool * vernac_control CAst.t -- cgit v1.2.3