From a59b644de4234fb7fe3fce28284979091f257130 Mon Sep 17 00:00:00 2001 From: aspiwack Date: Thu, 6 Dec 2007 17:36:14 +0000 Subject: Plus de combinateurs sont passés de Util à Option. Le module Options devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7 --- lib/flags.ml | 128 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ lib/flags.mli | 74 ++++++++++++++++++++++++++++++++ lib/option.ml | 27 ++++++++++++ lib/option.mli | 17 +++++++- lib/options.ml | 128 -------------------------------------------------------- lib/options.mli | 74 -------------------------------- lib/pp.ml4 | 6 +-- lib/util.ml | 8 ---- lib/util.mli | 2 - 9 files changed, 248 insertions(+), 216 deletions(-) create mode 100644 lib/flags.ml create mode 100644 lib/flags.mli delete mode 100644 lib/options.ml delete mode 100644 lib/options.mli (limited to 'lib') diff --git a/lib/flags.ml b/lib/flags.ml new file mode 100644 index 0000000000..12b2ed0370 --- /dev/null +++ b/lib/flags.ml @@ -0,0 +1,128 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* o := old; raise e + +let boot = ref false + +let batch_mode = ref false + +let debug = ref false + +let print_emacs = ref false +let print_emacs_safechar = ref false + +let term_quality = ref false + +let xml_export = ref false + +let dont_load_proofs = ref false + +let raw_print = ref false + +(* Translate *) +let translate = ref false +let make_translate f = translate := f +let do_translate () = !translate +let translate_file = ref false + +(* True only when interning from pp*new.ml *) +let translate_syntax = ref false + +(* Silent / Verbose *) +let silent = ref false +let make_silent flag = silent := flag; () +let is_silent () = !silent +let is_verbose () = not !silent + +let silently f x = + let oldsilent = !silent in + try + silent := true; + let rslt = f x in + silent := oldsilent; + rslt + with e -> begin + silent := oldsilent; raise e + end + +let if_silent f x = if !silent then f x +let if_verbose f x = if not !silent then f x + +let hash_cons_proofs = ref true + +let warn = ref true +let make_warn flag = warn := flag; () +let if_warn f x = if !warn then f x + +(* The number of printed hypothesis in a goal *) + +let print_hyps_limit = ref (None : int option) +let set_print_hyps_limit n = print_hyps_limit := n +let print_hyps_limit () = !print_hyps_limit + +(* A list of the areas of the system where "unsafe" operation + * has been requested *) + +let unsafe_set = ref Stringset.empty +let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set +let is_unsafe s = Stringset.mem s !unsafe_set + +(* Dump of globalization (to be used by coqdoc) *) + +let dump = ref false +let dump_file = ref "" +let dump_into_file f = dump := true; dump_file := f + +let dump_buffer = Buffer.create 8192 + +let dump_string = Buffer.add_string dump_buffer + +let dump_it () = + if !dump then begin + let mode = [Open_wronly; Open_append; Open_creat] in + let c = open_out_gen mode 0o666 !dump_file in + output_string c (Buffer.contents dump_buffer); + close_out c + end + +let _ = at_exit dump_it + +(* Flags.for the virtual machine *) + +let boxed_definitions = ref true +let set_boxed_definitions b = boxed_definitions := b +let boxed_definitions _ = !boxed_definitions + +(* Flags.for external tools *) + +let browser_cmd_fmt = + try + let coq_netscape_remote_var = "COQREMOTEBROWSER" in + let coq_netscape_remote = Sys.getenv coq_netscape_remote_var in + let i = Util.string_index_from coq_netscape_remote 0 "%s" in + let pre = String.sub coq_netscape_remote 0 i in + let post = String.sub coq_netscape_remote (i + 2) + (String.length coq_netscape_remote - (i + 2)) in + if Util.string_string_contains ~where:post ~what:"%s" then + error ("The environment variable \"" ^ + coq_netscape_remote_var ^ + "\" must contain exactly one placeholder \"%s\".") + else pre,post + with + Not_found -> + if Sys.os_type = "Win32" + then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE ", "" + else "firefox -remote \"OpenURL(", ")\"" diff --git a/lib/flags.mli b/lib/flags.mli new file mode 100644 index 0000000000..248b59b0df --- /dev/null +++ b/lib/flags.mli @@ -0,0 +1,74 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit +val do_translate : unit -> bool +val translate_file : bool ref +val translate_syntax : bool ref + +val make_silent : bool -> unit +val is_silent : unit -> bool +val is_verbose : unit -> bool +val silently : ('a -> 'b) -> 'a -> 'b +val if_silent : ('a -> unit) -> 'a -> unit +val if_verbose : ('a -> unit) -> 'a -> unit + +val make_warn : bool -> unit +val if_warn : ('a -> unit) -> 'a -> unit + +val hash_cons_proofs : bool ref + +(* Temporary activate an option ('c must be an atomic type) *) +val with_option : bool ref -> ('a -> 'b) -> 'a -> 'b + +(* If [None], no limit *) +val set_print_hyps_limit : int option -> unit +val print_hyps_limit : unit -> int option + +val add_unsafe : string -> unit +val is_unsafe : string -> bool + +(* Dump of globalization (to be used by coqdoc) *) + +val dump : bool ref +val dump_into_file : string -> unit +val dump_string : string -> unit + +(* Options for the virtual machine *) + +val set_boxed_definitions : bool -> unit +val boxed_definitions : unit -> bool + +(* Options for external tools *) + +(* Returns head and tail of printf string format *) +(* ocaml doesn't allow not applied formats *) +val browser_cmd_fmt : string * string + diff --git a/lib/option.ml b/lib/option.ml index 0ed36b0026..436358b555 100644 --- a/lib/option.ml +++ b/lib/option.ml @@ -32,6 +32,14 @@ let get = function (** [make x] returns [Some x]. *) let make x = Some x +(** [init b x] returns [Some x] if [b] is [true] and [None] otherwise. *) +let init b x = + if b then + Some x + else + None + + (** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *) let flatten = function | Some (Some y) -> Some y @@ -120,3 +128,22 @@ let lift2 f x y = match x,y with | Some z, Some w -> Some (f z w) | _,_ -> None + + + +(** {6 Operations with Lists} *) + +module List = + struct + (** [List.cons x l] equals [y::l] if [x] is [Some y] and [l] otherwise. *) + let cons x l = + match x with + | Some y -> y::l + | _ -> l + + (** [List.flatten l] is the list of all the [y]s such that [l] contains + [Some y] (in the same order). *) + let rec flatten = function + | x::l -> cons x (flatten l) + | [] -> [] +end diff --git a/lib/option.mli b/lib/option.mli index f98c45ee72..8e768d8af2 100644 --- a/lib/option.mli +++ b/lib/option.mli @@ -28,6 +28,9 @@ val get : 'a option -> 'a (** [make x] returns [Some x]. *) val make : 'a -> 'a option +(** [init b x] returns [Some x] if [b] is [true] and [None] otherwise. *) +val init : bool -> 'a -> 'a option + (** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *) val flatten : 'a option option -> 'a option @@ -64,7 +67,7 @@ val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option -> 'c option -> 'a val fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b -(** {6 More Specific operations} ***) +(** {6 More Specific Operations} ***) (** [default f x a] is [f y] if [x] is [Some y] and [a] otherwise. *) val default : ('a -> 'b) -> 'a option -> 'b -> 'b @@ -83,3 +86,15 @@ val lift_left : ('a -> 'b -> 'c) -> 'a option -> 'b -> 'c option (** [lift2 f x y] is [Some (f z w)] if [x] equals [Some z] and [y] equals [Some w]. It is [None] otherwise. *) val lift2 : ('a -> 'b -> 'c) -> 'a option -> 'b option -> 'c option + + +(** {6 Operations with Lists} *) + +module List : sig + (** [List.cons x l] equals [y::l] if [x] is [Some y] and [l] otherwise. *) + val cons : 'a option -> 'a list -> 'a list + + (** [List.flatten l] is the list of all the [y]s such that [l] contains + [Some y] (in the same order). *) + val flatten : 'a option list -> 'a list +end diff --git a/lib/options.ml b/lib/options.ml deleted file mode 100644 index 5890695678..0000000000 --- a/lib/options.ml +++ /dev/null @@ -1,128 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* o := old; raise e - -let boot = ref false - -let batch_mode = ref false - -let debug = ref false - -let print_emacs = ref false -let print_emacs_safechar = ref false - -let term_quality = ref false - -let xml_export = ref false - -let dont_load_proofs = ref false - -let raw_print = ref false - -(* Translate *) -let translate = ref false -let make_translate f = translate := f -let do_translate () = !translate -let translate_file = ref false - -(* True only when interning from pp*new.ml *) -let translate_syntax = ref false - -(* Silent / Verbose *) -let silent = ref false -let make_silent flag = silent := flag; () -let is_silent () = !silent -let is_verbose () = not !silent - -let silently f x = - let oldsilent = !silent in - try - silent := true; - let rslt = f x in - silent := oldsilent; - rslt - with e -> begin - silent := oldsilent; raise e - end - -let if_silent f x = if !silent then f x -let if_verbose f x = if not !silent then f x - -let hash_cons_proofs = ref true - -let warn = ref true -let make_warn flag = warn := flag; () -let if_warn f x = if !warn then f x - -(* The number of printed hypothesis in a goal *) - -let print_hyps_limit = ref (None : int option) -let set_print_hyps_limit n = print_hyps_limit := n -let print_hyps_limit () = !print_hyps_limit - -(* A list of the areas of the system where "unsafe" operation - * has been requested *) - -let unsafe_set = ref Stringset.empty -let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set -let is_unsafe s = Stringset.mem s !unsafe_set - -(* Dump of globalization (to be used by coqdoc) *) - -let dump = ref false -let dump_file = ref "" -let dump_into_file f = dump := true; dump_file := f - -let dump_buffer = Buffer.create 8192 - -let dump_string = Buffer.add_string dump_buffer - -let dump_it () = - if !dump then begin - let mode = [Open_wronly; Open_append; Open_creat] in - let c = open_out_gen mode 0o666 !dump_file in - output_string c (Buffer.contents dump_buffer); - close_out c - end - -let _ = at_exit dump_it - -(* Options for the virtual machine *) - -let boxed_definitions = ref true -let set_boxed_definitions b = boxed_definitions := b -let boxed_definitions _ = !boxed_definitions - -(* Options for external tools *) - -let browser_cmd_fmt = - try - let coq_netscape_remote_var = "COQREMOTEBROWSER" in - let coq_netscape_remote = Sys.getenv coq_netscape_remote_var in - let i = Util.string_index_from coq_netscape_remote 0 "%s" in - let pre = String.sub coq_netscape_remote 0 i in - let post = String.sub coq_netscape_remote (i + 2) - (String.length coq_netscape_remote - (i + 2)) in - if Util.string_string_contains ~where:post ~what:"%s" then - error ("The environment variable \"" ^ - coq_netscape_remote_var ^ - "\" must contain exactly one placeholder \"%s\".") - else pre,post - with - Not_found -> - if Sys.os_type = "Win32" - then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE ", "" - else "firefox -remote \"OpenURL(", ")\"" diff --git a/lib/options.mli b/lib/options.mli deleted file mode 100644 index 73962735da..0000000000 --- a/lib/options.mli +++ /dev/null @@ -1,74 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit -val do_translate : unit -> bool -val translate_file : bool ref -val translate_syntax : bool ref - -val make_silent : bool -> unit -val is_silent : unit -> bool -val is_verbose : unit -> bool -val silently : ('a -> 'b) -> 'a -> 'b -val if_silent : ('a -> unit) -> 'a -> unit -val if_verbose : ('a -> unit) -> 'a -> unit - -val make_warn : bool -> unit -val if_warn : ('a -> unit) -> 'a -> unit - -val hash_cons_proofs : bool ref - -(* Temporary activate an option ('c must be an atomic type) *) -val with_option : bool ref -> ('a -> 'b) -> 'a -> 'b - -(* If [None], no limit *) -val set_print_hyps_limit : int option -> unit -val print_hyps_limit : unit -> int option - -val add_unsafe : string -> unit -val is_unsafe : string -> bool - -(* Dump of globalization (to be used by coqdoc) *) - -val dump : bool ref -val dump_into_file : string -> unit -val dump_string : string -> unit - -(* Options for the virtual machine *) - -val set_boxed_definitions : bool -> unit -val boxed_definitions : unit -> bool - -(* Options for external tools *) - -(* Returns head and tail of printf string format *) -(* ocaml doesn't allow not applied formats *) -val browser_cmd_fmt : string * string - diff --git a/lib/pp.ml4 b/lib/pp.ml4 index 415a3002ab..067c527002 100644 --- a/lib/pp.ml4 +++ b/lib/pp.ml4 @@ -11,10 +11,10 @@ open Pp_control (* This should not be used outside of this file. Use - Options.print_emacs instead. This one is updated when reading + Flags.print_emacs instead. This one is updated when reading command line options. This was the only way to make [Pp] depend on - an option without creating a circularity: [Options] -> [Util] -> - [Pp] -> [Options] *) + an option without creating a circularity: [Flags. -> [Util] -> + [Pp] -> [Flags. *) let print_emacs = ref false let make_pp_emacs() = print_emacs:=true let make_pp_nonemacs() = print_emacs:=false diff --git a/lib/util.ml b/lib/util.ml index b61cd88ff6..99a203d52f 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -788,19 +788,11 @@ let interval n m = in interval_n ([],m) -let option_cons a l = match a with - | Some x -> x::l - | None -> l - let option_compare f a b = match (a,b) with | None, None -> true | Some a', Some b' -> f a' b' | _ -> failwith "option_compare" -let rec filter_some = function - | [] -> [] - | None::l -> filter_some l - | Some a::l -> a :: filter_some l let map_succeed f = let rec map_f = function diff --git a/lib/util.mli b/lib/util.mli index 71262bb4cd..331363f0ae 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -223,9 +223,7 @@ val intmap_inv : 'a Intmap.t -> 'a -> int list val interval : int -> int -> int list -val option_cons : 'a option -> 'a list -> 'a list val option_compare : ('a -> 'b -> bool) -> 'a option -> 'b option -> bool -val filter_some : 'a option list -> 'a list (* In [map_succeed f l] an element [a] is removed if [f a] raises *) (* [Failure _] otherwise behaves as [List.map f l] *) -- cgit v1.2.3