From 72d1a646accdb8252da01eb082986de52bc6052c Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 30 Oct 2001 16:10:21 +0000 Subject: Reorganisation de Goption. Passage des options l'utilisant en synchrone git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2145 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/extraction/table.ml | 28 ++++--- library/goptions.ml | 196 ++++++++++++++++---------------------------- library/goptions.mli | 38 ++++----- library/impargs.ml | 8 +- pretyping/detyping.ml | 24 +++--- toplevel/vernacentries.ml | 55 +++++++------ 6 files changed, 148 insertions(+), 201 deletions(-) diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index 6b5abf41c..7953f1182 100644 --- a/contrib/extraction/table.ml +++ b/contrib/extraction/table.ml @@ -22,21 +22,29 @@ open Declarations (*s AutoInline parameter *) -let auto_inline_params = - {optsyncname = "Extraction AutoInline"; - optsynckey = SecondaryTable ("Extraction", "AutoInline"); - optsyncdefault = true } +let auto_inline_ref = ref true -let auto_inline = declare_sync_bool_option auto_inline_params +let auto_inline () = !auto_inline_ref + +let _ = declare_bool_option + {optsync = true; + optname = "Extraction AutoInline"; + optkey = SecondaryTable ("Extraction", "AutoInline"); + optread = auto_inline; + optwrite = (:=) auto_inline_ref} (*s Optimize parameter *) -let optim_params = - {optsyncname = "Extraction Optimize"; - optsynckey = SecondaryTable ("Extraction", "Optimize"); - optsyncdefault = true } +let optim_ref = ref true + +let optim () = !optim_ref -let optim = declare_sync_bool_option optim_params +let _ = declare_bool_option + {optsync = true; + optname = "Extraction Optimize"; + optkey = SecondaryTable ("Extraction", "Optimize"); + optread = optim; + optwrite = (:=) optim_ref} (*s Set and Map over global reference *) diff --git a/library/goptions.ml b/library/goptions.ml index 77ce794ce..9af867ce7 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -197,120 +197,73 @@ module MakeIdentTable = (****************************************************************************) (* 2- Options *) -type option_value_ref = - | OptionBoolRef of bool ref - | OptionIntRef of int ref - | OptionStringRef of string ref +type 'a option_sig = { + optsync : bool; + optname : string; + optkey : option_name; + optread : unit -> 'a; + optwrite : 'a -> unit } + +type option_type = bool * (unit -> value) -> (value -> unit) module Key = struct type t = option_name let compare = Pervasives.compare end module OptionMap = Map.Make(Key) -let sync_value_init_tab = ref OptionMap.empty -let sync_value_tab = ref OptionMap.empty -let async_value_tab = ref OptionMap.empty - - -(* Tools for synchronous options *) - -let load_sync_value _ = () -let cache_sync_value (_,(k,v)) = - sync_value_tab := OptionMap.add k v !sync_value_tab -let export_sync_value fp = Some fp -let (inOptVal,_) = - Libobject.declare_object ("Sync_option_value", - { Libobject.load_function = load_sync_value; - Libobject.open_function = cache_sync_value; - Libobject.cache_function = cache_sync_value; - Libobject.export_function = export_sync_value }) +let value_tab = ref OptionMap.empty -let freeze_sync_table () = !sync_value_tab -let unfreeze_sync_table l = sync_value_tab := l -let init_sync_table () = sync_value_tab := !sync_value_init_tab -let _ = - Summary.declare_summary "Sync_option" - { Summary.freeze_function = freeze_sync_table; - Summary.unfreeze_function = unfreeze_sync_table; - Summary.init_function = init_sync_table; - Summary.survive_section = true } +(* This raises Not_found if option of key [key] is unknown *) -(* Tools for handling options *) +let get_option key = OptionMap.find key !value_tab -type option_type = - | Sync of value - | Async of (unit -> value) * (value -> unit) +let check_key key = try + let _ = get_option key in + error "Sorry, this option name is already used" +with Not_found -> + if List.mem_assoc (nickname key) !string_table + or List.mem_assoc (nickname key) !ident_table + then error "Sorry, this option name is already used" -(* This raises Not_found if option of key [key] is unknown *) -let get_option key = - try - let (name,(r,w)) = OptionMap.find key !async_value_tab in - (name,Async (r,w)) - with Not_found -> - let (name,i) = OptionMap.find key !sync_value_tab in (name, Sync i) - - -(* 2-a. Declaring synchronous options *) -type 'a sync_option_sig = { - optsyncname : string; - optsynckey : option_name; - optsyncdefault : 'a } - -let declare_sync_option (cast,uncast) - { optsyncname=name; optsynckey=key; optsyncdefault=default } = - try - let _ = get_option key in - error "Sorry, this option name is already used" - with Not_found -> - if List.mem_assoc (nickname key) !string_table - or List.mem_assoc (nickname key) !ident_table - then error "Sorry, this option name is already used"; - sync_value_tab := OptionMap.add key (name,(cast default)) !sync_value_tab; - sync_value_init_tab := - OptionMap.add key (name,(cast default)) !sync_value_init_tab; - fun () -> uncast (snd (OptionMap.find key !sync_value_tab)) - -type 'a value_function = unit -> 'a - -let declare_sync_int_option = declare_sync_option - ((function vr -> IntValue vr), - function IntValue x -> x | _ -> anomaly "MakeOption") -let declare_sync_bool_option = declare_sync_option - ((function vr -> BoolValue vr), - function BoolValue x -> x | _ -> anomaly "MakeOption") -let declare_sync_string_option = declare_sync_option - ((function vr -> StringValue vr), - function StringValue x -> x | _ -> anomaly "MakeOption") - -(* 2-b. Declaring synchronous options *) - -type 'a async_option_sig = { - optasyncname : string; - optasynckey : option_name; - optasyncread : unit -> 'a; - optasyncwrite : 'a -> unit } - -let declare_async_option cast uncast - {optasyncname=name;optasynckey=key;optasyncread=read;optasyncwrite=write} = - try - let _ = get_option key in - error "Sorry, this option name is already used" - with Not_found -> - if List.mem_assoc (nickname key) !string_table - or List.mem_assoc (nickname key) !ident_table then - error "Sorry, this option name is already used"; - let cread () = cast (read ()) in - let cwrite v = write (uncast v) in - async_value_tab := OptionMap.add key (name,(cread,cwrite)) !async_value_tab - -let declare_async_int_option = - declare_async_option +open Summary +open Libobject +open Lib + +let declare_option cast uncast + { optsync=sync; optname=name; optkey=key; optread=read; optwrite=write } = + check_key key; + let write = if sync then + let (decl_obj,_) = + declare_object ((nickname key), + {load_function = (fun _ -> ()); + open_function = (fun _ -> ()); + cache_function = (fun (_,v) -> write v); + export_function = (fun x -> None)}) + in + let _ = declare_summary (nickname key) + {freeze_function = read; + unfreeze_function = write; + init_function = (let default = read() in fun () -> write default); + survive_section = true} + in + fun v -> add_anonymous_leaf (decl_obj v) + else write + in + let cread () = cast (read ()) in + let cwrite v = write (uncast v) in + value_tab := OptionMap.add key (name,(sync,cread,cwrite)) !value_tab; + write + +type 'a write_function = 'a -> unit + +let declare_int_option = + declare_option (fun v -> IntValue v) (function IntValue v -> v | _ -> anomaly "async_option") -let declare_async_bool_option = - declare_async_option +let declare_bool_option = + declare_option (fun v -> BoolValue v) (function BoolValue v -> v | _ -> anomaly "async_option") -let declare_async_string_option = - declare_async_option +let declare_string_option = + declare_option (fun v -> StringValue v) (function StringValue v -> v | _ -> anomaly "async_option") @@ -319,15 +272,11 @@ let declare_async_string_option = (* Setting values of options *) let set_option_value check_and_cast key v = - let (name,info) = + let (name,(_,read,write)) = try get_option key with Not_found -> error ("There is no option "^(nickname key)^".") in - match info with - | Sync current -> - Lib.add_anonymous_leaf - (inOptVal (key,(name,check_and_cast v current))) - | Async (read,write) -> write (check_and_cast v (read ())) + write (check_and_cast v (read ())) let bad_type_error () = error "Bad type of value for this option" @@ -346,7 +295,7 @@ let set_string_option_value = set_option_value (* Printing options/tables *) -let msg_sync_option_value (name,v) = +let msg_option_value (name,v) = match v with | BoolValue true -> [< 'sTR "true" >] | BoolValue false -> [< 'sTR "false" >] @@ -354,36 +303,33 @@ let msg_sync_option_value (name,v) = | StringValue s -> [< 'sTR s >] | IdentValue id -> [< 'sTR (Global.string_of_global id) >] -let msg_async_option_value (name,vref) = - match vref with - | OptionBoolRef {contents=true} -> [< 'sTR "true" >] - | OptionBoolRef {contents=false} -> [< 'sTR "false" >] - | OptionIntRef r -> [< 'iNT !r >] - | OptionStringRef r -> [< 'sTR !r >] - let print_option_value key = - let (name,info) = get_option key in - let s = match info with Sync v -> v | Async (read,write) -> read () in + let (name,(_,read,_)) = get_option key in + let s = read () in match s with | BoolValue b -> mSG [< 'sTR("The "^name^" mode is "^(if b then "on" else "off"));'fNL>] | _ -> mSG [< 'sTR ("Current value of "^name^" is "); - msg_sync_option_value (name,s); 'fNL >] + msg_option_value (name,s); 'fNL >] let print_tables () = mSG [< 'sTR "Synchronous options:"; 'fNL; OptionMap.fold - (fun key (name,v) p -> [< p; 'sTR (" "^(nickname key)^": "); - msg_sync_option_value (name,v); 'fNL >]) - !sync_value_tab [<>]; + (fun key (name,(sync,read,write)) p -> + if sync then [< p; 'sTR (" "^(nickname key)^": "); + msg_option_value (name,read()); 'fNL >] + else [< p >]) + !value_tab [<>]; 'sTR "Asynchronous options:"; 'fNL; OptionMap.fold - (fun key (name,(read,write)) p -> [< p; 'sTR (" "^(nickname key)^": "); - msg_sync_option_value (name,read()); 'fNL >]) - !async_value_tab [<>]; + (fun key (name,(sync,read,write)) p -> + if sync then [< p >] + else [< p; 'sTR (" "^(nickname key)^": "); + msg_option_value (name,read()); 'fNL >]) + !value_tab [<>]; 'sTR "Tables:"; 'fNL; List.fold_right (fun (nickkey,_) p -> [< p; 'sTR (" "^nickkey); 'fNL >]) diff --git a/library/goptions.mli b/library/goptions.mli index cece47bf2..92eeb4108 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -13,7 +13,7 @@ (* Two kinds of things are managed : tables and options value - Tables are created by applying the [MakeTable] functor. - Variables storing options value are created by applying one of the - [declare_sync_int_option], [declare_async_bool_option], ... functions. + [declare_int_option], [declare_bool_option], ... functions. Each table/option is uniquely identified by a key of type [option_name]. There are two kinds of table/option idenfiers: the primary ones @@ -127,36 +127,26 @@ module MakeIdentTable : (*s Options. *) -(*s a. Synchronous options. *) - (* These types and function are for declaring a new option of name [key] - and default value [default]; the parameter [name] is the option name + and access functions [read] and [write]; the parameter [name] is the option name used when printing the option value (command "Print Toto Titi." *) -type 'a sync_option_sig = { - optsyncname : string; - optsynckey : option_name; - optsyncdefault : 'a +type 'a option_sig = { + optsync : bool; + optname : string; + optkey : option_name; + optread : unit -> 'a; + optwrite : 'a -> unit } -type 'a value_function = unit -> 'a - -val declare_sync_int_option : int sync_option_sig -> int value_function -val declare_sync_bool_option : bool sync_option_sig -> bool value_function -val declare_sync_string_option: string sync_option_sig -> string value_function - - -(*s b. Asynchronous options. *) +(* When an option is declared synchronous ([optsync] is [true]), the output is + a synchronous write function. Otherwise it is [optwrite] *) -type 'a async_option_sig = { - optasyncname : string; - optasynckey : option_name; - optasyncread : unit -> 'a; - optasyncwrite : 'a -> unit } +type 'a write_function = 'a -> unit -val declare_async_int_option : int async_option_sig -> unit -val declare_async_bool_option : bool async_option_sig -> unit -val declare_async_string_option : string async_option_sig -> unit +val declare_int_option : int option_sig -> int write_function +val declare_bool_option : bool option_sig -> bool write_function +val declare_string_option: string option_sig -> string write_function (*s Special functions supposed to be used only in vernacentries.ml *) diff --git a/library/impargs.ml b/library/impargs.ml index 63351392e..e203a594d 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -318,8 +318,7 @@ let implicits_of_global = function (*s Registration as global tables and rollback. *) -type frozen_t = bool - * implicits Spmap.t +type frozen_t = implicits Spmap.t * implicits Indmap.t * implicits Constrmap.t * implicits Spmap.t @@ -331,11 +330,10 @@ let init () = var_table := Spmap.empty let freeze () = - (!implicit_args, !constants_table, !inductives_table, + (!constants_table, !inductives_table, !constructors_table, !var_table) -let unfreeze (imps,ct,it,const,vt) = - implicit_args := imps; +let unfreeze (ct,it,const,vt) = constants_table := ct; inductives_table := it; constructors_table := const; diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index e0c1db169..2026bdb21 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -195,22 +195,22 @@ open Goptions let wildcard_value = ref true let force_wildcard () = !wildcard_value -let _ = - declare_async_bool_option - { optasyncname = "forced wildcard"; - optasynckey = SecondaryTable ("Printing","Wildcard"); - optasyncread = force_wildcard; - optasyncwrite = (fun v -> wildcard_value := v) } +let _ = declare_bool_option + { optsync = true; + optname = "forced wildcard"; + optkey = SecondaryTable ("Printing","Wildcard"); + optread = force_wildcard; + optwrite = (:=) wildcard_value } let synth_type_value = ref true let synthetize_type () = !synth_type_value -let _ = - declare_async_bool_option - { optasyncname = "synthesizability"; - optasynckey = SecondaryTable ("Printing","Synth"); - optasyncread = synthetize_type; - optasyncwrite = (fun v -> synth_type_value := v) } +let _ = declare_bool_option + { optsync = true; + optname = "synthesizability"; + optkey = SecondaryTable ("Printing","Synth"); + optread = synthetize_type; + optwrite = (:=) synth_type_value } (* Auxiliary function for MutCase printing *) (* [computable] tries to tell if the predicate typing the result is inferable*) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 715270e39..187391e24 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -469,22 +469,25 @@ let _ = make_focus 0; reset_top_of_tree (); show_open_subgoals ()) | _ -> bad_vernac_args "UNFOCUS") -let _ = declare_async_bool_option - {optasyncname = "implicit arguments"; - optasynckey = (SecondaryTable ("Implicit","Arguments")); - optasyncread = Impargs.is_implicit_args; - optasyncwrite = Impargs.make_implicit_args } +let _ = declare_bool_option + {optsync = true; + optname = "implicit arguments"; + optkey = (SecondaryTable ("Implicit","Arguments")); + optread = Impargs.is_implicit_args; + optwrite = Impargs.make_implicit_args } let _ = add "IMPLICIT_ARGS_ON" (function - | [] -> (fun () -> Impargs.make_implicit_args true) + | [] -> (fun () -> set_bool_option_value + (SecondaryTable ("Implicit","Arguments")) true) | _ -> bad_vernac_args "IMPLICIT_ARGS_ON") let _ = add "IMPLICIT_ARGS_OFF" (function - | [] -> (fun () -> Impargs.make_implicit_args false) + | [] -> (fun () -> set_bool_option_value + (SecondaryTable ("Implicit","Arguments")) false) | _ -> bad_vernac_args "IMPLICIT_ARGS_OFF") let _ = @@ -506,11 +509,12 @@ let coercion_of_qualid loc qid = [< Printer.pr_global ref; 'sTR" is not a coercion" >]; coe -let _ = declare_async_bool_option - {optasyncname = "coercion printing"; - optasynckey = (SecondaryTable ("Printing","Coercions")); - optasyncread = (fun () -> !Termast.print_coercions); - optasyncwrite = (fun b -> Termast.print_coercions := b) } +let _ = declare_bool_option + {optsync = true; + optname = "coercion printing"; + optkey = (SecondaryTable ("Printing","Coercions")); + optread = (fun () -> !Termast.print_coercions); + optwrite = (fun b -> Termast.print_coercions := b) } let number_list = List.map (function VARG_NUMBER n -> n | _ -> bad_vernac_args "Number list") @@ -771,22 +775,23 @@ let _ = | [VARG_QUALID qid] -> (fun () -> mSG(print_sec_context_typ qid)) | _ -> bad_vernac_args "PrintSec") -let _ = declare_async_bool_option - {optasyncname = "silent"; - optasynckey = (PrimaryTable "Silent"); - optasyncread = is_silent; - optasyncwrite = make_silent } +let _ = declare_bool_option + {optsync = true; + optname = "silent"; + optkey = (PrimaryTable "Silent"); + optread = is_silent; + optwrite = make_silent } let _ = add "BeginSilent" (function - | [] -> (fun () -> make_silent true) + | [] -> (fun () -> set_bool_option_value (PrimaryTable "Silent") true) | _ -> bad_vernac_args "BeginSilent") let _ = add "EndSilent" (function - | [] -> (fun () -> make_silent false) + | [] -> (fun () -> set_bool_option_value (PrimaryTable "Silent") false) | _ -> bad_vernac_args "EndSilent") let _ = @@ -1426,12 +1431,12 @@ let _ = open Goptions -let _ = - declare_async_int_option - { optasynckey=SecondaryTable("Printing","Depth"); - optasyncname="the printing depth"; - optasyncread=Pp_control.get_depth_boxes; - optasyncwrite=Pp_control.set_depth_boxes } +let _ = declare_int_option + { optsync=true; + optkey=SecondaryTable("Printing","Depth"); + optname="the printing depth"; + optread=Pp_control.get_depth_boxes; + optwrite=Pp_control.set_depth_boxes } let _ = add "SetTableField" -- cgit v1.2.3