diff options
| -rw-r--r-- | CHANGES | 3 | ||||
| -rw-r--r-- | dev/ci/user-overlays/06923-ppedrot-export-options.sh | 7 | ||||
| -rw-r--r-- | ide/ide_slave.ml | 6 | ||||
| -rw-r--r-- | intf/vernacexpr.ml | 5 | ||||
| -rw-r--r-- | library/goptions.ml | 57 | ||||
| -rw-r--r-- | library/goptions.mli | 15 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 35 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.ml4 | 2 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 15 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 8 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 56 | ||||
| -rw-r--r-- | vernac/vernacprop.ml | 2 |
12 files changed, 123 insertions, 88 deletions
@@ -81,6 +81,9 @@ Vernacular Commands - An experimental command "Show Extraction" allows to extract the content of the current ongoing proof (grant wish #4129). - Coercion now accepts the type of its argument to be "Prop" or "Type". +- The "Export" modifier can now be used when setting and unsetting options, and + will result in performing the same change when the module corresponding the + command is imported. Universes diff --git a/dev/ci/user-overlays/06923-ppedrot-export-options.sh b/dev/ci/user-overlays/06923-ppedrot-export-options.sh new file mode 100644 index 000000000..333a9e84b --- /dev/null +++ b/dev/ci/user-overlays/06923-ppedrot-export-options.sh @@ -0,0 +1,7 @@ +if [ "$CI_PULL_REQUEST" = "6923" ] || [ "$CI_BRANCH" = "export-options" ]; then + ltac2_CI_BRANCH=export-options + ltac2_CI_GITURL=https://github.com/ppedrot/ltac2 + + Equations_CI_BRANCH=export-options + Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations +fi diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 0ba1b3a4f..55b4fa87e 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -57,8 +57,8 @@ let coqide_known_option table = List.mem table [ ["Printing";"Unfocused"]] let is_known_option cmd = match Vernacprop.under_control cmd with - | VernacSetOption (o,BoolValue true) - | VernacUnsetOption o -> coqide_known_option o + | VernacSetOption (_, o, BoolValue true) + | VernacUnsetOption (_, o) -> coqide_known_option o | _ -> false (** Check whether a command is forbidden in the IDE *) @@ -340,7 +340,7 @@ let set_options options = | 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 None name + | StringOptValue None -> Goptions.unset_option_value_gen name in List.iter iter options diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 0a6e5b3b3..dca491057 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -425,9 +425,8 @@ type nonrec vernac_expr = | VernacSetOpacity of (Conv_oracle.level * reference or_by_notation list) | VernacSetStrategy of (Conv_oracle.level * reference or_by_notation list) list - | VernacUnsetOption of Goptions.option_name - | VernacSetOption of Goptions.option_name * option_value - | VernacSetAppendOption of Goptions.option_name * string + | VernacUnsetOption of export_flag * Goptions.option_name + | VernacSetOption of export_flag * Goptions.option_name * option_value | 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 diff --git a/library/goptions.ml b/library/goptions.ml index 5681421ca..76071ebcc 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -196,7 +196,7 @@ type 'a option_sig = { optread : unit -> 'a; optwrite : 'a -> unit } -type option_locality = OptLocal | OptDefault | OptGlobal +type option_locality = OptDefault | OptLocal | OptExport | OptGlobal type option_mod = OptSet | OptAppend @@ -229,11 +229,6 @@ let warn_deprecated_option = (fun key -> str "Option" ++ spc () ++ str (nickname key) ++ strbrk " is deprecated") -let get_locality = function - | Some true -> OptLocal - | Some false -> OptGlobal - | None -> OptDefault - let declare_option cast uncast append ?(preprocess = fun x -> x) { optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } = check_key key; @@ -247,16 +242,30 @@ let declare_option cast uncast append ?(preprocess = fun x -> x) match m with | OptSet -> write v | OptAppend -> write (append (read ()) v) in - let load_options i o = cache_options o in + let load_options i (_, (l, _, _) as o) = match l with + | OptGlobal -> cache_options o + | OptExport -> () + | OptLocal | OptDefault -> + (** Ruled out by classify_function *) + assert false + in + let open_options i (_, (l, _, _) as o) = match l with + | OptExport -> if Int.equal i 1 then cache_options o + | OptGlobal -> () + | OptLocal | OptDefault -> + (** Ruled out by classify_function *) + assert false + in let subst_options (subst,obj) = obj in let discharge_options (_,(l,_,_ as o)) = - match l with OptLocal -> None | _ -> Some o in + match l with OptLocal -> None | (OptExport | OptGlobal | OptDefault) -> Some o in let classify_options (l,_,_ as o) = - match l with OptGlobal -> Substitute o | _ -> Dispose in + match l with (OptExport | OptGlobal) -> Substitute o | (OptLocal | OptDefault) -> Dispose in let options : option_locality * option_mod * _ -> obj = declare_object { (default_object (nickname key)) with load_function = load_options; + open_function = open_options; cache_function = cache_options; subst_function = subst_options; discharge_function = discharge_options; @@ -302,12 +311,12 @@ let warn_unknown_option = (fun key -> strbrk "There is no option " ++ str (nickname key) ++ str ".") -let set_option_value locality check_and_cast key v = +let set_option_value ?(locality = OptDefault) check_and_cast key v = let opt = try Some (get_option key) with Not_found -> None in match opt with | None -> warn_unknown_option key | Some (name, depr, (read,write,append)) -> - write (get_locality locality) (check_and_cast v (read ())) + write locality (check_and_cast v (read ())) let bad_type_error () = user_err Pp.(str "Bad type of value for this option.") @@ -334,25 +343,25 @@ let check_unset_value v = function warning. This allows a script to refer to an option that doesn't exist anymore *) -let set_int_option_value_gen locality = - set_option_value locality check_int_value -let set_bool_option_value_gen locality key v = - set_option_value locality check_bool_value key v -let set_string_option_value_gen locality = - set_option_value locality check_string_value -let unset_option_value_gen locality key = - set_option_value locality check_unset_value key () +let set_int_option_value_gen ?locality = + set_option_value ?locality check_int_value +let set_bool_option_value_gen ?locality key v = + set_option_value ?locality check_bool_value key v +let set_string_option_value_gen ?locality = + set_option_value ?locality check_string_value +let unset_option_value_gen ?locality key = + set_option_value ?locality check_unset_value key () -let set_string_option_append_value_gen locality key v = +let set_string_option_append_value_gen ?(locality = OptDefault) key v = let opt = try Some (get_option key) with Not_found -> None in match opt with | None -> warn_unknown_option key | Some (name, depr, (read,write,append)) -> - append (get_locality locality) (check_string_value v (read ())) + append locality (check_string_value v (read ())) -let set_int_option_value = set_int_option_value_gen None -let set_bool_option_value = set_bool_option_value_gen None -let set_string_option_value = set_string_option_value_gen None +let set_int_option_value opt v = set_int_option_value_gen opt v +let set_bool_option_value opt v = set_bool_option_value_gen opt v +let set_string_option_value opt v = set_string_option_value_gen opt v (* Printing options/tables *) diff --git a/library/goptions.mli b/library/goptions.mli index 31920b832..6c14d19ee 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -50,6 +50,8 @@ open Mod_subst type option_name = string list +type option_locality = OptDefault | OptLocal | OptExport | OptGlobal + (** {6 Tables. } *) (** The functor [MakeStringTable] declares a table containing objects @@ -150,13 +152,12 @@ val get_ref_table : mem : reference -> unit; print : unit > -(** The first argument is a locality flag. - [Some true] = "Local", [Some false]="Global". *) -val set_int_option_value_gen : bool option -> option_name -> int option -> unit -val set_bool_option_value_gen : bool option -> option_name -> bool -> unit -val set_string_option_value_gen : bool option -> option_name -> string -> unit -val set_string_option_append_value_gen : bool option -> option_name -> string -> unit -val unset_option_value_gen : bool option -> option_name -> unit +(** The first argument is a locality flag. *) +val set_int_option_value_gen : ?locality:option_locality -> option_name -> int option -> unit +val set_bool_option_value_gen : ?locality:option_locality -> option_name -> bool -> unit +val set_string_option_value_gen : ?locality:option_locality -> option_name -> string -> unit +val set_string_option_append_value_gen : ?locality:option_locality -> option_name -> string -> unit +val unset_option_value_gen : ?locality:option_locality -> option_name -> unit val set_int_option_value : option_name -> int option -> unit val set_bool_option_value : option_name -> bool -> unit diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index feaef3161..f1ec49623 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -822,7 +822,14 @@ GEXTEND Gram END GEXTEND Gram - GLOBAL: command query_command class_rawexpr; + GLOBAL: command query_command class_rawexpr gallina_ext; + + gallina_ext: + [ [ IDENT "Export"; "Set"; table = option_table; v = option_value -> + VernacSetOption (true, table, v) + | IDENT "Export"; IDENT "Unset"; table = option_table -> + VernacUnsetOption (true, table) + ] ]; command: [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l @@ -887,24 +894,9 @@ GEXTEND Gram (* For acting on parameter tables *) | "Set"; table = option_table; v = option_value -> - begin match v with - | StringValue s -> - (* We make a special case for warnings because appending is their - natural semantics *) - if CString.List.equal table ["Warnings"] then - VernacSetAppendOption (table, s) - else - let (last, prefix) = List.sep_last table in - if String.equal last "Append" && not (List.is_empty prefix) then - VernacSetAppendOption (prefix, s) - else - VernacSetOption (table, v) - | _ -> VernacSetOption (table, v) - end - | "Set"; table = option_table -> - VernacSetOption (table,BoolValue true) + VernacSetOption (false, table, v) | IDENT "Unset"; table = option_table -> - VernacUnsetOption table + VernacUnsetOption (false, table) | IDENT "Print"; IDENT "Table"; table = option_table -> VernacPrintOption table @@ -1010,7 +1002,8 @@ GEXTEND Gram | IDENT "Module"; qid = global -> LocateModule qid ] ] ; option_value: - [ [ n = integer -> IntValue (Some n) + [ [ -> BoolValue true + | n = integer -> IntValue (Some n) | s = STRING -> StringValue s ] ] ; option_ref_value: @@ -1081,10 +1074,10 @@ GEXTEND Gram (* Tactic Debugger *) | IDENT "Debug"; IDENT "On" -> - VernacSetOption (["Ltac";"Debug"], BoolValue true) + VernacSetOption (false, ["Ltac";"Debug"], BoolValue true) | IDENT "Debug"; IDENT "Off" -> - VernacSetOption (["Ltac";"Debug"], BoolValue false) + VernacSetOption (false, ["Ltac";"Debug"], BoolValue false) (* registration of a custom reduction *) diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index e3941c1c5..c3b6a7c59 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -178,7 +178,7 @@ GEXTEND Gram GLOBAL: gallina_ext; gallina_ext: [ [ IDENT "Import"; IDENT "Prenex"; IDENT "Implicits" -> - Vernacexpr.VernacUnsetOption (["Printing"; "Implicit"; "Defensive"]) + Vernacexpr.VernacUnsetOption (false, ["Printing"; "Implicit"; "Defensive"]) ] ] ; END diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 2b7d643d6..ea1ca26fb 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1118,18 +1118,15 @@ open Decl_kinds hov 1 (keyword "Strategy" ++ spc() ++ hv 0 (prlist_with_sep sep pr_line l)) ) - | VernacUnsetOption (na) -> + | VernacUnsetOption (export, na) -> + let export = if export then keyword "Export" ++ spc () else mt () in return ( - hov 1 (keyword "Unset" ++ spc() ++ pr_printoption na None) + hov 1 (export ++ keyword "Unset" ++ spc() ++ pr_printoption na None) ) - | VernacSetOption (na,v) -> + | VernacSetOption (export, na,v) -> + let export = if export then keyword "Export" ++ spc () else mt () in return ( - hov 2 (keyword "Set" ++ spc() ++ pr_set_option na v) - ) - | VernacSetAppendOption (na,v) -> - return ( - hov 2 (keyword "Set" ++ spc() ++ pr_printoption na None ++ - spc() ++ keyword "Append" ++ spc() ++ qs v) + hov 2 (export ++ keyword "Set" ++ spc() ++ pr_set_option na v) ) | VernacAddOption (na,l) -> return ( diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 48ccb8f4c..f68c8b326 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -61,7 +61,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,_) | VernacUnsetOption (_, l)) when CList.equal String.equal l Vernacentries.universe_polymorphism_option_name -> VtSideff [], VtNow (* Qed *) @@ -87,8 +87,8 @@ let classify_vernac e = proof_block_detection = Some "curly" }, VtLater (* Options changing parser *) - | VernacUnsetOption (["Default";"Proof";"Using"]) - | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow + | VernacUnsetOption (_, ["Default";"Proof";"Using"]) + | VernacSetOption (_, ["Default";"Proof";"Using"],_) -> VtSideff [], VtNow (* StartProof *) | VernacDefinition ((Decl_kinds.DoDischarge,_),({v=i},_),ProveBody _) -> VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity, idents_of_name i), VtLater @@ -149,7 +149,7 @@ let classify_vernac e = | VernacReserve _ | VernacGeneralizable _ | VernacSetOpacity _ | VernacSetStrategy _ - | VernacUnsetOption _ | VernacSetOption _ | VernacSetAppendOption _ + | VernacUnsetOption _ | VernacSetOption _ | VernacAddOption _ | VernacRemoveOption _ | VernacMemOption _ | VernacPrintOption _ | VernacGlobalCheck _ diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4c9b41b21..7764920d9 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1539,18 +1539,45 @@ let vernac_set_opacity ~atts (v,l) = let l = List.map glob_ref l in Redexpr.set_strategy local [v,l] -let vernac_set_option ~atts key = function - | StringValue s -> set_string_option_value_gen atts.locality key s - | StringOptValue (Some s) -> set_string_option_value_gen atts.locality key s - | StringOptValue None -> unset_option_value_gen atts.locality key - | IntValue n -> set_int_option_value_gen atts.locality key n - | BoolValue b -> set_bool_option_value_gen atts.locality key b - -let vernac_set_append_option ~atts key s = - set_string_option_append_value_gen atts.locality key s +let get_option_locality export local = + if export then + if Option.is_empty local then OptExport + else user_err Pp.(str "Locality modifiers forbidden with Export") + else match local with + | Some true -> OptLocal + | Some false -> OptGlobal + | None -> OptDefault + +let vernac_set_option0 ~atts export key opt = + let locality = get_option_locality export atts.locality 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 + +let vernac_set_append_option ~atts export key s = + let locality = get_option_locality export atts.locality in + set_string_option_append_value_gen ~locality key s + +let vernac_set_option ~atts export table v = match v with +| StringValue s -> + (* We make a special case for warnings because appending is their + natural semantics *) + if CString.List.equal table ["Warnings"] then + vernac_set_append_option ~atts export table s + else + let (last, prefix) = List.sep_last table in + if String.equal last "Append" && not (List.is_empty prefix) then + vernac_set_append_option ~atts export prefix s + else + vernac_set_option0 ~atts export table v +| _ -> vernac_set_option0 ~atts export table v -let vernac_unset_option ~atts key = - unset_option_value_gen atts.locality key +let vernac_unset_option ~atts export key = + let locality = get_option_locality export atts.locality in + unset_option_value_gen ~locality key let vernac_add_option key lv = let f = function @@ -2083,9 +2110,8 @@ let interp ?proof ~atts ~st c = | VernacGeneralizable gen -> vernac_generalizable ~atts gen | VernacSetOpacity qidl -> vernac_set_opacity ~atts qidl | VernacSetStrategy l -> vernac_set_strategy ~atts l - | VernacSetOption (key,v) -> vernac_set_option ~atts key v - | VernacSetAppendOption (key,v) -> vernac_set_append_option ~atts key v - | VernacUnsetOption key -> vernac_unset_option ~atts key + | VernacSetOption (export, key,v) -> vernac_set_option ~atts export key v + | VernacUnsetOption (export, key) -> vernac_unset_option ~atts export key | VernacRemoveOption (key,v) -> vernac_remove_option key v | VernacAddOption (key,v) -> vernac_add_option key v | VernacMemOption (key,v) -> vernac_mem_option key v @@ -2148,7 +2174,7 @@ let check_vernac_supports_locality c l = | VernacArgumentsScope _ | VernacDeclareImplicits _ | VernacArguments _ | VernacGeneralizable _ | VernacSetOpacity _ | VernacSetStrategy _ - | VernacSetOption _ | VernacSetAppendOption _ | VernacUnsetOption _ + | VernacSetOption _ | VernacUnsetOption _ | VernacDeclareReduction _ | VernacExtend _ | VernacInductive _) -> () diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml index 44a7a9b15..a837b77a3 100644 --- a/vernac/vernacprop.ml +++ b/vernac/vernacprop.ml @@ -52,7 +52,7 @@ let is_reset = function | _ -> false let is_debug cmd = match under_control cmd with - | VernacSetOption (["Ltac";"Debug"], _) -> true + | VernacSetOption (_, ["Ltac";"Debug"], _) -> true | _ -> false let is_undo cmd = match under_control cmd with |