From 839ed4e80ca4dc068422c7c9fdb0c00e4ff1ebab Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 1 Apr 2019 13:44:54 +0200 Subject: Unify Set and Unset handling for options Not sure if the idetop.set_options was correctly changed, ocaml types pass at least. --- ide/idetop.ml | 17 +++++++++-------- plugins/ssr/ssrvernac.mlg | 2 +- stm/vernac_classifier.ml | 8 +++----- toplevel/coqloop.ml | 4 +--- vernac/g_vernac.mlg | 20 ++++++++++---------- vernac/ppvernac.ml | 21 ++++++--------------- vernac/proof_using.ml | 3 ++- vernac/proof_using.mli | 3 +++ vernac/vernacentries.ml | 18 +++++------------- vernac/vernacexpr.ml | 13 ++++++------- 10 files changed, 46 insertions(+), 63 deletions(-) diff --git a/ide/idetop.ml b/ide/idetop.ml index 10b8a2cdc5..543ff924bd 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -57,9 +57,9 @@ let coqide_known_option table = List.mem table [ ["Diffs"]] let is_known_option cmd = match Vernacprop.under_control cmd with - | VernacSetOption (_, o, BoolValue true) - | VernacSetOption (_, o, StringValue _) - | VernacUnsetOption (_, o) -> coqide_known_option o + | VernacSetOption (_, o, OptionSetTrue) + | VernacSetOption (_, o, OptionSetString _) + | VernacSetOption (_, o, OptionUnset) -> coqide_known_option o | _ -> false (** Check whether a command is forbidden in the IDE *) @@ -366,12 +366,13 @@ let get_options () = Goptions.OptionMap.fold fold table [] let set_options options = + let open Goptions in let iter (name, value) = match import_option_value value with - | BoolValue b -> Goptions.set_bool_option_value name b - | IntValue i -> Goptions.set_int_option_value name i - | StringValue s -> Goptions.set_string_option_value name s - | StringOptValue (Some s) -> Goptions.set_string_option_value name s - | StringOptValue None -> Goptions.unset_option_value_gen name + | BoolValue b -> set_bool_option_value name b + | IntValue i -> set_int_option_value name i + | StringValue s -> set_string_option_value name s + | StringOptValue (Some s) -> set_string_option_value name s + | StringOptValue None -> unset_option_value_gen name in List.iter iter options diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 0a0d9b12fa..bf7f082192 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -183,7 +183,7 @@ GRAMMAR EXTEND Gram GLOBAL: gallina_ext; gallina_ext: [ [ IDENT "Import"; IDENT "Prenex"; IDENT "Implicits" -> - { Vernacexpr.VernacUnsetOption (false, ["Printing"; "Implicit"; "Defensive"]) } + { Vernacexpr.VernacSetOption (false, ["Printing"; "Implicit"; "Defensive"], Vernacexpr.OptionUnset) } ] ] ; END diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 58fe923f9e..243b5c333d 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -57,6 +57,7 @@ let options_affecting_stm_scheduling = stm_allow_nested_proofs_option_name; Vernacentries.proof_mode_opt_name; Attributes.program_mode_option_name; + Proof_using.proof_using_opt_name; ] let classify_vernac e = @@ -64,7 +65,7 @@ let classify_vernac e = (* Univ poly compatibility: we run it now, so that we can just * look at Flags in stm.ml. Would be nicer to have the stm * look at the entire dag to detect this option. *) - | ( VernacSetOption (_, l,_) | VernacUnsetOption (_, l)) + | VernacSetOption (_, l,_) when CList.exists (CList.equal String.equal l) options_affecting_stm_scheduling -> VtSideff [], VtNow @@ -91,9 +92,6 @@ let classify_vernac e = VtProofStep { parallel = `No; proof_block_detection = Some "curly" }, VtLater - (* Options changing parser *) - | VernacUnsetOption (_, ["Default";"Proof";"Using"]) - | VernacSetOption (_, ["Default";"Proof";"Using"],_) -> VtSideff [], VtNow (* StartProof *) | VernacDefinition ((Decl_kinds.DoDischarge,_),({v=i},_),ProveBody _) -> VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i), VtLater @@ -156,7 +154,7 @@ let classify_vernac e = | VernacReserve _ | VernacGeneralizable _ | VernacSetOpacity _ | VernacSetStrategy _ - | VernacUnsetOption _ | VernacSetOption _ + | VernacSetOption _ | VernacAddOption _ | VernacRemoveOption _ | VernacMemOption _ | VernacPrintOption _ | VernacGlobalCheck _ diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index b3de8dd85f..4129562065 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -340,9 +340,7 @@ let print_anyway_opts = [ let print_anyway c = let open Vernacexpr in match c with - | VernacExpr (_, VernacSetOption (_, opt, _)) - | VernacExpr (_, VernacUnsetOption (_, opt)) -> - List.mem opt print_anyway_opts + | VernacExpr (_, VernacSetOption (_, opt, _)) -> List.mem opt print_anyway_opts | _ -> false (* We try to behave better when goal printing raises an exception diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 1533d0ccd3..3f491d1dd4 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -875,10 +875,10 @@ GRAMMAR EXTEND Gram GLOBAL: command query_command class_rawexpr gallina_ext; gallina_ext: - [ [ IDENT "Export"; "Set"; table = option_table; v = option_value -> + [ [ IDENT "Export"; "Set"; table = option_table; v = option_setting -> { VernacSetOption (true, table, v) } | IDENT "Export"; IDENT "Unset"; table = option_table -> - { VernacUnsetOption (true, table) } + { VernacSetOption (true, table, OptionUnset) } ] ]; command: @@ -943,10 +943,10 @@ GRAMMAR EXTEND Gram { VernacAddMLPath (true, dir) } (* For acting on parameter tables *) - | "Set"; table = option_table; v = option_value -> + | "Set"; table = option_table; v = option_setting -> { VernacSetOption (false, table, v) } | IDENT "Unset"; table = option_table -> - { VernacUnsetOption (false, table) } + { VernacSetOption (false, table, OptionUnset) } | IDENT "Print"; IDENT "Table"; table = option_table -> { VernacPrintOption table } @@ -1057,10 +1057,10 @@ GRAMMAR EXTEND Gram | IDENT "Library"; qid = global -> { LocateLibrary qid } | IDENT "Module"; qid = global -> { LocateModule qid } ] ] ; - option_value: - [ [ -> { BoolValue true } - | n = integer -> { IntValue (Some n) } - | s = STRING -> { StringValue s } ] ] + option_setting: + [ [ -> { OptionSetTrue } + | n = integer -> { OptionSetInt n } + | s = STRING -> { OptionSetString s } ] ] ; option_ref_value: [ [ id = global -> { QualidRefValue id } @@ -1130,10 +1130,10 @@ GRAMMAR EXTEND Gram (* Tactic Debugger *) | IDENT "Debug"; IDENT "On" -> - { VernacSetOption (false, ["Ltac";"Debug"], BoolValue true) } + { VernacSetOption (false, ["Ltac";"Debug"], OptionSetTrue) } | IDENT "Debug"; IDENT "Off" -> - { VernacSetOption (false, ["Ltac";"Debug"], BoolValue false) } + { VernacSetOption (false, ["Ltac";"Debug"], OptionUnset) } (* registration of a custom reduction *) diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index b602e134da..4e4d431e89 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -173,15 +173,10 @@ open Pputils pr_opt (prlist_with_sep sep pr_option_ref_value) b let pr_set_option a b = - let pr_opt_value = function - | IntValue None -> assert false - (* This should not happen because of the grammar *) - | IntValue (Some n) -> spc() ++ int n - | StringValue s -> spc() ++ str s - | StringOptValue None -> mt() - | StringOptValue (Some s) -> spc() ++ str s - | BoolValue b -> mt() - in pr_printoption a None ++ pr_opt_value b + pr_printoption a None ++ (match b with + | OptionUnset | OptionSetTrue -> mt() + | OptionSetInt n -> spc() ++ int n + | OptionSetString s -> spc() ++ quote (str s)) let pr_opt_hintbases l = match l with | [] -> mt() @@ -1140,15 +1135,11 @@ open Pputils hov 1 (keyword "Strategy" ++ spc() ++ hv 0 (prlist_with_sep sep pr_line l)) ) - | VernacUnsetOption (export, na) -> - let export = if export then keyword "Export" ++ spc () else mt () in - return ( - hov 1 (export ++ keyword "Unset" ++ spc() ++ pr_printoption na None) - ) | VernacSetOption (export, na,v) -> let export = if export then keyword "Export" ++ spc () else mt () in + let set = if v == OptionUnset then "Unset" else "Set" in return ( - hov 2 (export ++ keyword "Set" ++ spc() ++ pr_set_option na v) + hov 2 (export ++ keyword set ++ spc() ++ pr_set_option na v) ) | VernacAddOption (na,l) -> return ( diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index 526845084a..1d089d0a55 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -172,11 +172,12 @@ let value = ref None let using_to_string us = Pp.string_of_ppcmds (Ppvernac.pr_using us) let using_from_string us = Pcoq.Entry.parse G_vernac.section_subset_expr (Pcoq.Parsable.make (Stream.of_string us)) +let proof_using_opt_name = ["Default";"Proof";"Using"] let () = Goptions.(declare_stringopt_option { optdepr = false; optname = "default value for Proof using"; - optkey = ["Default";"Proof";"Using"]; + optkey = proof_using_opt_name; optread = (fun () -> Option.map using_to_string !value); optwrite = (fun b -> value := Option.map using_from_string b); }) diff --git a/vernac/proof_using.mli b/vernac/proof_using.mli index 7d1110aaa2..702043a4a9 100644 --- a/vernac/proof_using.mli +++ b/vernac/proof_using.mli @@ -21,3 +21,6 @@ val suggest_constant : Environ.env -> Names.Constant.t -> unit val suggest_variable : Environ.env -> Names.Id.t -> unit val get_default_proof_using : unit -> Vernacexpr.section_subset_expr option + +val proof_using_opt_name : string list +(** For the stm *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 6c24b9ec75..3a305c3b61 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1707,18 +1707,17 @@ let get_option_locality export local = let vernac_set_option0 ~local export key opt = let locality = get_option_locality export local in match opt with - | StringValue s -> set_string_option_value_gen ~locality key s - | StringOptValue (Some s) -> set_string_option_value_gen ~locality key s - | StringOptValue None -> unset_option_value_gen ~locality key - | IntValue n -> set_int_option_value_gen ~locality key n - | BoolValue b -> set_bool_option_value_gen ~locality key b + | OptionUnset -> unset_option_value_gen ~locality key + | OptionSetString s -> set_string_option_value_gen ~locality key s + | OptionSetInt n -> set_int_option_value_gen ~locality key (Some n) + | OptionSetTrue -> set_bool_option_value_gen ~locality key true let vernac_set_append_option ~local export key s = let locality = get_option_locality export local in set_string_option_append_value_gen ~locality key s let vernac_set_option ~local export table v = match v with -| StringValue s -> +| OptionSetString s -> (* We make a special case for warnings because appending is their natural semantics *) if CString.List.equal table ["Warnings"] then @@ -1731,10 +1730,6 @@ let vernac_set_option ~local export table v = match v with vernac_set_option0 ~local export table v | _ -> vernac_set_option0 ~local export table v -let vernac_unset_option ~local export key = - let locality = get_option_locality export local in - unset_option_value_gen ~locality key - let vernac_add_option key lv = let f = function | StringRefValue s -> (get_string_table key)#add s @@ -2462,9 +2457,6 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option = | VernacSetOption (export, key,v) -> vernac_set_option ~local:(only_locality atts) export key v; pstate - | VernacUnsetOption (export, key) -> - vernac_unset_option ~local:(only_locality atts) export key; - pstate | VernacRemoveOption (key,v) -> unsupported_attributes atts; vernac_remove_option key v; diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index ebfc473522..d5f4576ea2 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -109,11 +109,11 @@ type onlyparsing_flag = Flags.compat_version option which this notation is trying to be compatible with *) type locality_flag = bool (* true = Local *) -type option_value = Goptions.option_value = - | BoolValue of bool - | IntValue of int option - | StringValue of string - | StringOptValue of string option +type option_setting = + | OptionUnset + | OptionSetTrue + | OptionSetInt of int + | OptionSetString of string type option_ref_value = | StringRefValue of string @@ -363,8 +363,7 @@ type nonrec vernac_expr = | VernacSetOpacity of (Conv_oracle.level * qualid or_by_notation list) | VernacSetStrategy of (Conv_oracle.level * qualid or_by_notation list) list - | VernacUnsetOption of export_flag * Goptions.option_name - | VernacSetOption of export_flag * Goptions.option_name * option_value + | VernacSetOption of export_flag * Goptions.option_name * option_setting | VernacAddOption of Goptions.option_name * option_ref_value list | VernacRemoveOption of Goptions.option_name * option_ref_value list | VernacMemOption of Goptions.option_name * option_ref_value list -- cgit v1.2.3