From a62ffb11d33222001e63092700afb6507d3b1f5e Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 21 Sep 2001 20:55:55 +0000 Subject: RĂ©paration des options Set Printing and co MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2052 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile | 4 +- library/goptions.ml | 26 ++++--- library/goptions.mli | 25 +++---- parsing/g_basevernac.ml4 | 49 ++++--------- pretyping/detyping.ml | 23 +++--- toplevel/vernacentries.ml | 174 ++++++++++++++++++++++++++-------------------- 6 files changed, 151 insertions(+), 150 deletions(-) diff --git a/Makefile b/Makefile index 5fb3bb2c9..39e61a611 100644 --- a/Makefile +++ b/Makefile @@ -82,8 +82,8 @@ KERNEL=kernel/names.cmo kernel/univ.cmo \ kernel/indtypes.cmo kernel/cooking.cmo kernel/safe_typing.cmo LIBRARY=library/libobject.cmo library/summary.cmo library/nametab.cmo \ - library/lib.cmo library/goptions.cmo \ - library/global.cmo library/opaque.cmo \ + library/lib.cmo library/global.cmo \ + library/goptions.cmo library/opaque.cmo \ library/library.cmo library/states.cmo \ library/impargs.cmo library/indrec.cmo library/declare.cmo diff --git a/library/goptions.ml b/library/goptions.ml index 8c0c08cef..94fb12668 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -14,6 +14,7 @@ open Pp open Util open Libobject open Names +open Term (****************************************************************************) (* 0- Common things *) @@ -33,7 +34,7 @@ type value = | BoolValue of bool | IntValue of int | StringValue of string - | IdentValue of identifier + | IdentValue of global_reference (****************************************************************************) (* 1- Tables *) @@ -167,19 +168,19 @@ let get_ident_table k = List.assoc (nickname k) !ident_table module type IdentConvertArg = sig type t - val encode : identifier -> t + val encode : global_reference -> t val check : t -> unit val printer : t -> std_ppcmds val key : option_name val title : string - val member_message : identifier -> bool -> string + val member_message : global_reference -> bool -> string val synchronous : bool end module IdentConvert = functor (A : IdentConvertArg) -> struct type t = A.t - type key = identifier + type key = global_reference let table = ident_table let encode = A.encode let check = A.check @@ -207,6 +208,7 @@ 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 _ = () @@ -246,7 +248,6 @@ let get_option key = (* 2-a. Declaring synchronous options *) - type 'a sync_option_sig = { optsyncname : string; optsynckey : option_name; @@ -310,7 +311,6 @@ let declare_async_string_option = (fun v -> StringValue v) (function StringValue v -> v | _ -> anomaly "async_option") - (* 3- User accessible commands *) (* Setting values of options *) @@ -349,7 +349,7 @@ let msg_sync_option_value (name,v) = | BoolValue false -> [< 'sTR "false" >] | IntValue n -> [< 'iNT n >] | StringValue s -> [< 'sTR s >] - | IdentValue id -> [< pr_id id >] + | IdentValue id -> [< 'sTR (Global.string_of_global id) >] let msg_async_option_value (name,vref) = match vref with @@ -360,10 +360,14 @@ let msg_async_option_value (name,vref) = 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 s = match info with Sync v -> v | Async (read,write) -> 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 >] + let print_tables () = mSG diff --git a/library/goptions.mli b/library/goptions.mli index 012967561..cece47bf2 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -32,20 +32,20 @@ following vernacular commands: Set Tata Tutu val. - Print Tata Tutu. + Print Table 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. + Print Table Tata Tutu. (* synonym: Test Table Tata Tutu. *) For a primary table, say of name [PrimaryTable("Bidule")], the vernacular commands look like Add Bidule foo. - Print Bidule foo. + Print Table Bidule foo. Set Bidule foo. ... @@ -55,6 +55,7 @@ (*i*) open Pp open Names +open Term (*i*) (*s Things common to tables and options. *) @@ -93,11 +94,11 @@ sig val elements : unit -> string list end -(* The functor [MakeIdentTable] declares a new table of [identifier]; +(* The functor [MakeIdentTable] declares a new table of [global_reference]; for generality, identifiers may be internally encode in other type - which is [A.t] through an encoding function [encode : identifier -> - A.t] (typically, [A.t] is the persistent [section_path] associated - to the currentdenotation of the [identifier] and the encoding function + which is [A.t] through an encoding function [encode : global_reference -> + A.t] (typically, [A.t] is the persistent [global_reference] associated + to the currentdenotation of the [global_reference] and the encoding function is the globalization function); 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 @@ -110,12 +111,12 @@ module MakeIdentTable : functor (A : sig type t - val encode : identifier -> t + val encode : global_reference -> t val check : t -> unit val printer : t -> std_ppcmds val key : option_name val title : string - val member_message : identifier -> bool -> string + val member_message : global_reference -> bool -> string val synchronous : bool end) -> sig @@ -169,9 +170,9 @@ val get_string_table : val get_ident_table : option_name -> - < add : identifier -> unit; - remove : identifier -> unit; - mem : identifier -> unit; + < add : global_reference -> unit; + remove : global_reference -> unit; + mem : global_reference -> unit; print : unit > val set_int_option_value : option_name -> int -> unit diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index b2b04a2d7..2a447a910 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -185,37 +185,6 @@ GEXTEND Gram | IDENT "Unset"; IDENT "Hyps_limit" -> <:ast< (UNSETHYPSLIMIT) >> - (* Standardized syntax for Implicit Arguments *) - | "Set"; IDENT "Implicit"; IDENT "Arguments" -> - <:ast< (IMPLICIT_ARGS_ON) >> - | IDENT "Unset"; IDENT "Implicit"; IDENT "Arguments" -> - <:ast< (IMPLICIT_ARGS_OFF) >> - | IDENT "Test"; IDENT "Implicit"; IDENT "Arguments" -> - <:ast< (TEST_IMPLICIT_ARGS) >> - - (* Set printing depth *) - (* An explicit entry, to be factorized with Printing Coercions *) - | "Set"; table = IDENT "Printing"; field = IDENT "Depth"; n = numarg -> - <:ast< (SetTableField ($VAR $table) ($VAR $field) $n) >> - - (* Set printing of coercions *) - | "Set"; IDENT "Printing"; IDENT "Coercion"; - qidl = ne_qualidarg_list -> - <:ast< (PRINTING_COERCIONS_ON ($LIST $qidl)) >> - | "Set"; IDENT "Printing"; IDENT "Coercions" -> - <:ast< (PRINTING_COERCIONS_ON) >> - | IDENT "Unset"; IDENT "Printing"; IDENT "Coercion"; - qidl = ne_qualidarg_list -> - <:ast< (PRINTING_COERCIONS_OFF ($LIST $qidl)) >> - | IDENT "Unset"; IDENT "Printing"; IDENT "Coercions" -> - <:ast< (PRINTING_COERCIONS_OFF) >> - | IDENT "Test"; IDENT "Printing"; IDENT "Coercion"; - qidl = ne_qualidarg_list -> - <:ast< (TEST_PRINTING_COERCIONS ($LIST $qidl)) >> - | IDENT "Test"; IDENT "Printing"; IDENT "Coercions" -> - <:ast< (TEST_PRINTING_COERCIONS) >> - - (* Pour intervenir sur les tables de paramètres *) | "Set"; table = identarg; field = identarg; value = option_value -> @@ -224,6 +193,8 @@ GEXTEND Gram <:ast< (SetTableField $table $field) >> | IDENT "Unset"; table = identarg; field = identarg -> <:ast< (UnsetTableField $table $field) >> + | IDENT "Unset"; table = identarg; field = identarg; id = qualidarg -> + <:ast< (RemoveTableField $table $field $id) >> | "Set"; table = identarg; value = option_value -> <:ast< (SetTableField $table $value) >> | "Set"; table = identarg -> @@ -236,33 +207,37 @@ GEXTEND Gram (* Le cas suivant inclut aussi le "Print id" standard *) | IDENT "Print"; IDENT "Table"; table = identarg -> <:ast< (PrintOption $table) >> - | IDENT "Add"; table = identarg; field = identarg; id = identarg + | IDENT "Add"; table = identarg; field = identarg; id = qualidarg -> <:ast< (AddTableField $table $field $id) >> | IDENT "Add"; table = identarg; field = identarg; id = stringarg -> <:ast< (AddTableField $table $field $id) >> - | IDENT "Add"; table = identarg; id = identarg + | IDENT "Add"; table = identarg; id = qualidarg -> <:ast< (AddTableField $table $id) >> | IDENT "Add"; table = identarg; id = stringarg -> <:ast< (AddTableField $table $id) >> - | IDENT "Test"; table = identarg; field = identarg; id = identarg + | IDENT "Test"; table = identarg; field = identarg; id = qualidarg -> <:ast< (MemTableField $table $field $id) >> | IDENT "Test"; table = identarg; field = identarg; id = stringarg -> <:ast< (MemTableField $table $field $id) >> | IDENT "Test"; table = identarg; id = identarg -> <:ast< (MemTableField $table $id) >> + | IDENT "Test"; table = identarg; id = qualidarg + -> <:ast< (MemTableField $table $id) >> | IDENT "Test"; table = identarg; id = stringarg -> <:ast< (MemTableField $table $id) >> - | IDENT "Remove"; table = identarg; field = identarg; id = identarg -> + | IDENT "Test"; table = identarg + -> <:ast< (MemTableField $table) >> + | IDENT "Remove"; table = identarg; field = identarg; id = qualidarg -> <:ast< (RemoveTableField $table $field $id) >> | IDENT "Remove"; table = identarg; field = identarg; id = stringarg -> <:ast< (RemoveTableField $table $field $id) >> - | IDENT "Remove"; table = identarg; id = identarg -> + | IDENT "Remove"; table = identarg; id = qualidarg -> <:ast< (RemoveTableField $table $id) >> | IDENT "Remove"; table = identarg; id = stringarg -> <:ast< (RemoveTableField $table $id) >> ] ] ; option_value: - [ [ id = identarg -> id + [ [ id = qualidarg -> id | n = numarg -> n | s = stringarg -> s ] ] ; diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 1af83f722..a3d6d86cf 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -98,15 +98,12 @@ let used_of = global_vars_and_consts (****************************************************************************) (* Tools for printing of Cases *) -let encode_inductive id = +let encode_inductive ref = let (indsp,_ as ind) = - try - match kind_of_term (global_reference CCI id) with + match kind_of_term (constr_of_reference Evd.empty (Global.env()) ref)with | IsMutInd (indsp,args) -> (indsp,args) | _ -> errorlabstrm "indsp_of_id" - [< 'sTR ((string_of_id id)^" is not an inductive type") >] - with Not_found -> - error ("Cannot find reference "^(string_of_id id)) + [< 'sTR ((Global.string_of_global ref)^" is not an inductive type") >] in let mis = Global.lookup_mind_specif ind in let constr_lengths = Array.map List.length (mis_recarg mis) in @@ -134,7 +131,7 @@ module PrintingCasesMake = functor (Test : sig val test : int array -> bool val error_message : string - val member_message : identifier -> bool -> string + val member_message : global_reference -> bool -> string val field : string val title : string end) -> @@ -159,10 +156,10 @@ module PrintingCasesIf = let title = "Types leading to pretty-printing of Cases using a `if' form: " let member_message id = function | true -> - "Cases on elements of " ^ (string_of_id id) + "Cases on elements of " ^ (Global.string_of_global id) ^ " are printed using a `if' form" | false -> - "Cases on elements of " ^ (string_of_id id) + "Cases on elements of " ^ (Global.string_of_global id) ^ " are not printed using `if' form" end) @@ -175,10 +172,10 @@ module PrintingCasesLet = "Types leading to a pretty-printing of Cases using a `let' form:" let member_message id = function | true -> - "Cases on elements of " ^ (string_of_id id) + "Cases on elements of " ^ (Global.string_of_global id) ^ " are printed using a `let' form" | false -> - "Cases on elements of " ^ (string_of_id id) + "Cases on elements of " ^ (Global.string_of_global id) ^ " are not printed using a `let' form" end) @@ -199,7 +196,7 @@ let force_wildcard () = !wildcard_value let _ = declare_async_bool_option - { optasyncname = "the forced wildcard option"; + { optasyncname = "forced wildcard"; optasynckey = SecondaryTable ("Printing","Wildcard"); optasyncread = force_wildcard; optasyncwrite = (fun v -> wildcard_value := v) } @@ -209,7 +206,7 @@ let synthetize_type () = !synth_type_value let _ = declare_async_bool_option - { optasyncname = "the synthesisablity"; + { optasyncname = "synthesizability"; optasynckey = SecondaryTable ("Printing","Synth"); optasyncread = synthetize_type; optasyncwrite = (fun v -> synth_type_value := v) } diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 201896d90..bdf448afe 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -484,6 +484,12 @@ 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 _ = add "IMPLICIT_ARGS_ON" (function @@ -515,69 +521,12 @@ let coercion_of_qualid loc qid = [< Printer.pr_global ref; 'sTR" is not a coercion" >]; coe -let _ = - add "PRINTING_COERCIONS_ON" - (function - | [] -> (fun () -> Termast.print_coercions := true) - | l -> - let ql = - List.map - (function - | VARG_QUALID qid -> qid - | _ -> bad_vernac_args "PRINTING_COERCIONS_ON") l in - (fun () -> - List.iter - (fun qid -> - Classops.set_coercion_visibility true - (coercion_of_qualid dummy_loc qid)) - ql)) - -let _ = - add "PRINTING_COERCIONS_OFF" - (function - | [] -> (fun () -> Termast.print_coercions := false) - | l -> - let ql = - List.map - (function - | VARG_QUALID qid -> qid - | _ -> bad_vernac_args "PRINTING_COERCIONS_OFF") l in - (fun () -> - List.iter - (fun qid -> - Classops.set_coercion_visibility false - (coercion_of_qualid dummy_loc qid)) - ql)) +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 _ = - add "TEST_PRINTING_COERCIONS" - (function - | [] -> - (fun () -> - if !(Termast.print_coercions) = true then - message "Printing of coercions is set" - else - message "Printing of coercions is unset") - | l -> - let ql = - List.map - (function - | VARG_QUALID qid -> qid - | _ -> bad_vernac_args "TEST_PRINTING_COERCIONS") l in - (fun () -> - List.iter - (fun qid -> - let coe = coercion_of_qualid dummy_loc qid in - if Classops.is_coercion_visible coe then - message - ("Printing of coercion "^(Nametab.string_of_qualid qid)^ - " is set") - else - message - ("Printing of coercion "^(Nametab.string_of_qualid qid)^ - " is unset")) - ql)) - let number_list = List.map (function VARG_NUMBER n -> n | _ -> bad_vernac_args "Number list") @@ -838,7 +787,7 @@ let _ = | _ -> bad_vernac_args "PrintSec") let _ = declare_async_bool_option - {optasyncname = "Silent"; + {optasyncname = "silent"; optasynckey = (PrimaryTable "Silent"); optasyncread = is_silent; optasyncwrite = make_silent } @@ -1498,6 +1447,20 @@ let _ = let _ = add "SetTableField" (function + (* Hook for Printing Coercions *) + | (VARG_IDENTIFIER t) :: (VARG_IDENTIFIER f) :: l + when t = id_of_string "Printing" && f = id_of_string "Coercion" -> + let ql = + List.map + (function + | VARG_QUALID qid -> qid + | _ -> bad_vernac_args "PRINTING_COERCIONS_ON") l in + (fun () -> + List.iter + (fun qid -> + Classops.set_coercion_visibility true + (coercion_of_qualid dummy_loc qid)) + ql) | [(VARG_IDENTIFIER t);(VARG_IDENTIFIER f);arg] -> (fun () -> let key = @@ -1541,12 +1504,12 @@ let _ = let _ = add "AddTableField" (function - | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_IDENTIFIER v] -> + | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_QUALID v] -> (fun () -> let key = SecondaryTable (string_of_id t,string_of_id f) in try - (get_ident_table key)#add v + (get_ident_table key)#add (locate_qualid dummy_loc v) with Not_found -> error_undeclared_key key) | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_STRING s] -> @@ -1557,11 +1520,11 @@ let _ = (get_string_table key)#add s with Not_found -> error_undeclared_key key) - | [VARG_IDENTIFIER t; VARG_IDENTIFIER v] -> + | [VARG_IDENTIFIER t; VARG_QUALID v] -> (fun () -> let key = PrimaryTable (string_of_id t) in try - (get_ident_table key)#add v + (get_ident_table key)#add (locate_qualid dummy_loc v) with Not_found -> error_undeclared_key key) | [VARG_IDENTIFIER t; VARG_STRING s] -> @@ -1576,12 +1539,26 @@ let _ = let _ = add "RemoveTableField" (function - | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_IDENTIFIER v] -> + (* Hook for Printing Coercions *) + | (VARG_IDENTIFIER t) :: (VARG_IDENTIFIER f) :: l + when t = id_of_string "Printing" && f = id_of_string "Coercion" -> + let ql = + List.map + (function + | VARG_QUALID qid -> qid + | _ -> bad_vernac_args "PRINTING_COERCIONS_OFF") l in + (fun () -> + List.iter + (fun qid -> + Classops.set_coercion_visibility false + (coercion_of_qualid dummy_loc qid)) + ql) + | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_QUALID v] -> (fun () -> let key = SecondaryTable (string_of_id t,string_of_id f) in try - (get_ident_table key)#remove v + (get_ident_table key)#remove (locate_qualid dummy_loc v) with Not_found -> error_undeclared_key key) | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_STRING v] -> @@ -1592,11 +1569,11 @@ let _ = (get_string_table key)#remove v with Not_found -> error_undeclared_key key) - | [VARG_IDENTIFIER t; VARG_IDENTIFIER v] -> + | [VARG_IDENTIFIER t; VARG_QUALID v] -> (fun () -> let key = PrimaryTable (string_of_id t) in try - (get_ident_table key)#remove v + (get_ident_table key)#remove (locate_qualid dummy_loc v) with Not_found -> error_undeclared_key key) | [VARG_IDENTIFIER t; VARG_STRING v] -> @@ -1611,12 +1588,33 @@ let _ = let _ = add "MemTableField" (function - | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_IDENTIFIER v] -> + (* Hook for Printing Coercions *) + | (VARG_IDENTIFIER t) :: (VARG_IDENTIFIER f) :: l + when t = id_of_string "Printing" && f = id_of_string "Coercion" -> + let ql = + List.map + (function + | VARG_QUALID qid -> qid + | _ -> bad_vernac_args "TEST_PRINTING_COERCIONS") l in + (fun () -> + List.iter + (fun qid -> + let coe = coercion_of_qualid dummy_loc qid in + if Classops.is_coercion_visible coe then + message + ("Printing of coercion "^(Nametab.string_of_qualid qid)^ + " is set") + else + message + ("Printing of coercion "^(Nametab.string_of_qualid qid)^ + " is unset")) + ql) + | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_QUALID v] -> (fun () -> let key = SecondaryTable (string_of_id t,string_of_id f) in try - (get_ident_table key)#mem v + (get_ident_table key)#mem (locate_qualid dummy_loc v) with Not_found -> error_undeclared_key key) | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_STRING v] -> @@ -1627,13 +1625,26 @@ let _ = (get_string_table key)#mem v with Not_found -> error_undeclared_key key) - | [VARG_IDENTIFIER t; VARG_IDENTIFIER v] -> + | [VARG_IDENTIFIER t; VARG_QUALID v] -> (fun () -> let key = PrimaryTable (string_of_id t) in try - (get_ident_table key)#mem v + (get_ident_table key)#mem (locate_qualid dummy_loc v) with Not_found -> error_undeclared_key key) + | [VARG_IDENTIFIER t; VARG_IDENTIFIER v] -> + (fun () -> + let key = SecondaryTable (string_of_id t, string_of_id v) in + try + (get_ident_table key)#print + with not_found -> + try + (get_string_table key)#print + with not_found -> + try + print_option_value key + with Not_found -> + error_undeclared_key key) | [VARG_IDENTIFIER t; VARG_STRING v] -> (fun () -> let key = PrimaryTable (string_of_id t) in @@ -1641,6 +1652,19 @@ let _ = (get_string_table key)#mem v with Not_found -> error_undeclared_key key) + | [VARG_IDENTIFIER t] -> + (fun () -> + let key = PrimaryTable (string_of_id t) in + try + (get_ident_table key)#print + with not_found -> + try + (get_string_table key)#print + with not_found -> + try + print_option_value key + with Not_found -> + error_undeclared_key key) | _ -> bad_vernac_args "TableField") let _ = -- cgit v1.2.3