From 93535ddcdbf379d7d8fe062acdb9428d1b83ec4f Mon Sep 17 00:00:00 2001 From: filliatr Date: Fri, 26 Nov 1999 09:03:12 +0000 Subject: module Goptions (etait Options) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@148 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/goptions.ml | 307 +++++++++++++++++++++++++++++++++++++++++++++++++++ library/goptions.mli | 145 ++++++++++++++++++++++++ 2 files changed, 452 insertions(+) create mode 100644 library/goptions.ml create mode 100644 library/goptions.mli (limited to 'library') diff --git a/library/goptions.ml b/library/goptions.ml new file mode 100644 index 000000000..4f5133226 --- /dev/null +++ b/library/goptions.ml @@ -0,0 +1,307 @@ + +(* $Id$ *) + +(* This module manages customization parameters at the vernacular level *) + +open Pp +open Util +open Libobject +open Names + +(****************************************************************************) +(* 0- Common things *) + +type option_name = + | PrimaryTable of string + | SecondaryTable of string * string + +let nickname = function + | PrimaryTable s -> s + | SecondaryTable (s1,s2) -> s1^" "^s2 + +let error_undeclared_key key = + error ((nickname key)^": no such table or option") + +(****************************************************************************) +(* 1- Tables *) + +let param_table = ref [] + +let get_option_table k = List.assoc (nickname k) !param_table + +module MakeTable = + functor + (A : sig + type t + val encode : identifier -> t + val check : t -> unit + val decode : t -> section_path + val key : option_name + val title : string + val member_message : identifier -> bool -> string + val synchronous : bool + end) -> + struct + type option_mark = + | GOadd + | GOrmv + + let kn = nickname A.key + + let _ = + if List.mem_assoc kn !param_table then + error "Sorry, this table name is already used" + + module MyType = struct type t = A.t let compare = Pervasives.compare end + module MySet = Set.Make(MyType) + + let t = ref (MySet.empty : MySet.t) + + let _ = + if A.synchronous then + let freeze () = !t in + let unfreeze c = t := c in + let init () = t := MySet.empty in + Summary.declare_summary kn + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init } + + let (add_option,remove_option) = + if A.synchronous then + let load_options _ = () in + let open_options _ = () in + let cache_options (_,(f,p)) = match f with + | GOadd -> t := MySet.add p !t + | GOrmv -> t := MySet.remove p !t in + let specification_options fp = fp in + let (inGo,outGo) = + Libobject.declare_object (kn, + { Libobject.load_function = load_options; + Libobject.open_function = open_options; + Libobject.cache_function = cache_options; + Libobject.specification_function = specification_options}) in + ((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))), + (fun c -> Lib.add_anonymous_leaf (inGo (GOrmv, c)))) + else + ((fun c -> t := MySet.add c !t), + (fun c -> t := MySet.remove c !t)) + + let print_table table_name printer table = + mSG ([< 'sTR table_name ; (hOV 0 + (if MySet.is_empty table then [< 'sTR "None" ; 'fNL >] + else MySet.fold (fun a b -> [< printer a; b >]) table [<>])) >]) + + class table_of_A () = + object + method add id = + let c = A.encode id in + A.check c; + add_option c + method remove id = remove_option (A.encode id) + method mem id = + let answer = MySet.mem (A.encode id) !t in + mSG [< 'sTR (A.member_message id answer) >] + method print = + let pr x = [< 'sTR(string_of_path (A.decode x)); 'fNL >] in + print_table A.title pr !t + end + + let _ = param_table := (kn,new table_of_A ())::!param_table + let active c = MySet.mem c !t + + end + +(****************************************************************************) +(* 2- Options *) + +type option_value_ref = + | OptionBoolRef of bool ref + | OptionIntRef of int ref + | OptionStringRef of string ref + +type option_value = + | OptionBool of bool + | OptionInt of int + | OptionString of string + +module Key = struct type t = option_name let compare = Pervasives.compare end +module OptionMap = Map.Make(Key) + +let sync_value_tab = ref OptionMap.empty +let async_value_tab = ref OptionMap.empty + +(* Tools for synchronous options *) + +let load_sync_value _ = () +let open_sync_value _ = () +let cache_sync_value (_,(k,v)) = + sync_value_tab := OptionMap.add k v !sync_value_tab +let spec_sync_value fp = fp +let (inOptVal,_) = + Libobject.declare_object ("Sync_option_value", + {Libobject.load_function = load_sync_value; + Libobject.open_function = open_sync_value; + Libobject.cache_function = cache_sync_value; + Libobject.specification_function = spec_sync_value}) + +let freeze_sync_table () = !sync_value_tab +let unfreeze_sync_table l = sync_value_tab := l +let init_sync_table () = sync_value_tab := OptionMap.empty +let _ = + Summary.declare_summary "Sync_option" + { Summary.freeze_function = freeze_sync_table; + Summary.unfreeze_function = unfreeze_sync_table; + Summary.init_function = init_sync_table } + +(* Tools for handling options *) + +type option_type = + | Sync of option_value + | Async of (unit -> option_value) * (option_value -> unit) + +(* 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) !param_table + then error "Sorry, this option name is already used"; + sync_value_tab := OptionMap.add key (name,(cast default)) !sync_value_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 -> OptionInt vr), + function OptionInt x -> x | _ -> anomaly "MakeOption") +let declare_sync_bool_option = declare_sync_option + ((function vr -> OptionBool vr), + function OptionBool x -> x | _ -> anomaly "MakeOption") +let declare_sync_string_option = declare_sync_option + ((function vr -> OptionString vr), + function OptionString 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) !param_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 + (fun v -> OptionInt v) + (function OptionInt v -> v | _ -> anomaly "async_option") +let declare_async_bool_option = + declare_async_option + (fun v -> OptionBool v) + (function OptionBool v -> v | _ -> anomaly "async_option") +let declare_async_string_option = + declare_async_option + (fun v -> OptionString v) + (function OptionString v -> v | _ -> anomaly "async_option") + + +(* 3- User accessible commands *) + +(* Setting values of options *) + +let set_option_value check_and_cast key v = + let (name,info) = + 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 ())) + +let bad_type_error () = error "Bad type of value for this option" + +let set_int_option_value = set_option_value + (fun v -> function + | (OptionInt _) -> OptionInt v + | _ -> bad_type_error ()) +let set_bool_option_value = set_option_value + (fun v -> function + | (OptionBool _) -> OptionBool v + | _ -> bad_type_error ()) +let set_string_option_value = set_option_value + (fun v -> function + | (OptionString _) -> OptionString v + | _ -> bad_type_error ()) + +(* Printing options/tables *) + +let msg_sync_option_value (name,v) = + match v with + | OptionBool true -> [< 'sTR "true" >] + | OptionBool false -> [< 'sTR "false" >] + | OptionInt n -> [< 'iNT n >] + | OptionString s -> [< 'sTR s >] + +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 -> msg_sync_option_value (name,v) + | Async (read,write) -> msg_sync_option_value (name,read ()) + in mSG [< 'sTR ("Current value of "^name^" is "); 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 [<>]; + '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 [<>]; + 'sTR "Tables:"; 'fNL; + List.fold_right + (fun (nickkey,_) p -> [< p; 'sTR (" "^nickkey); 'fNL >]) + !param_table [<>]; + 'fNL + >] + diff --git a/library/goptions.mli b/library/goptions.mli new file mode 100644 index 000000000..73d49421b --- /dev/null +++ b/library/goptions.mli @@ -0,0 +1,145 @@ + +(* $Id$ *) + +(* This module manages customization parameters at the vernacular level *) + +(* 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. + + Each table/option is uniquely identified by a key of type [option_name]. + There are two kinds of table/option idenfiers: the primary ones + (supposed to be more global) and the secondary ones + + The declaration of a table, say of name [SecondaryTable("Toto","Titi")] + automatically makes available the following vernacular commands: + + Add Toto Titi foo. + Remove Toto Titi foo. + Print Toto Titi. + Test Toto Titi. + + The declaration of a non boolean option value, say of name + [SecondaryTable("Tata","Tutu")], automatically makes available the + following vernacular commands: + + Set Tata Tutu val. + Print Tata Tutu. + + If it is the declaration of a boolean value, the following + vernacular commands are made available: + + Set Tata Tutu. + Unset Tata Tutu. + Print Tata Tutu. + + For a primary table, say of name [PrimaryTable("Bidule")], the + vernacular commands look like + + Add Bidule foo. + Print Bidule foo. + Set Bidule foo. + ... + + The created table/option may be declared synchronous or not + (synchronous = consistent with the resetting commands) *) + +(*i*) +open Names +(*i*) + +(*s Things common to tables and options. *) + +(* The type of primary or secondary table/option keys *) +type option_name = + | PrimaryTable of string + | SecondaryTable of string * string + +val error_undeclared_key : option_name -> 'a + + +(*s Tables. *) + +(* The functor [MakeTable] is for declaring a new table of key [key] + containing objects of type [A.t]; in spite the objects are internally + of type [A.t], they are supposed to be added at the vernacular level + as objects of type [identifier] and to be printed as [section_path]; + thus two functions [encode : identifier -> A.t] and [decode : A.t + -> section_path] have to be provided; this limitation can be make + softer in a future version (!); the function [check] is for testing + if a given object is allowed to be added to the table; the function + [member_message] say what to print when invoking the "Test Toto + Titi foo." command; at the end [title] is the table name printed + when invoking the "Print Toto Titi." command; [active] is roughly + the internal version of the vernacular "Test ...": it tells if a + given object is in the table. *) + +module MakeTable : + functor + (A : sig + type t + val encode : identifier -> t + val check : t -> unit + val decode : t -> section_path + val key : option_name + val title : string + val member_message : identifier -> bool -> string + val synchronous : bool + end) -> + sig + val active : A.t -> bool + end + + +(*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 + used when printing the option value (command "Print Toto Titi." *) + +type 'a sync_option_sig = { + optsyncname : string; + optsynckey : option_name; + optsyncdefault : 'a +} + +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. *) + +type 'a async_option_sig = { + optasyncname : string; + optasynckey : option_name; + optasyncread : unit -> 'a; + optasyncwrite : '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 + + +(*s Special functions supposed to be used only in vernacentries.ml *) + +val get_option_table : + option_name -> + < add : identifier -> unit; + remove : identifier -> unit; + mem : identifier -> unit; + print : unit > + +val set_int_option_value : option_name -> int -> unit +val set_bool_option_value : option_name -> bool -> unit +val set_string_option_value : option_name -> string -> unit + +val print_option_value : option_name -> unit + +val print_tables : unit -> unit + -- cgit v1.2.3