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 --- library/goptions.ml | 196 +++++++++++++++++++-------------------------------- library/goptions.mli | 38 ++++------ library/impargs.ml | 8 +-- 3 files changed, 88 insertions(+), 154 deletions(-) (limited to 'library') 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; -- cgit v1.2.3