From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 1 Feb 2009 00:54:40 +0100 Subject: Imported Upstream version 8.2~rc2+dfsg --- lib/envars.ml | 84 ++++++++++++++++++++++++++++++++ lib/envars.mli | 15 ++++++ lib/flags.ml | 67 +++++++++++--------------- lib/flags.mli | 34 ++++++++----- lib/option.ml | 6 ++- lib/option.mli | 4 +- lib/system.ml | 45 ++++++++++++++--- lib/system.mli | 13 +++-- lib/util.ml | 150 ++++++++++++++++++++++++++++++++++++++++++--------------- lib/util.mli | 17 ++++++- 10 files changed, 326 insertions(+), 109 deletions(-) create mode 100644 lib/envars.ml create mode 100644 lib/envars.mli (limited to 'lib') diff --git a/lib/envars.ml b/lib/envars.ml new file mode 100644 index 00000000..5887adcd --- /dev/null +++ b/lib/envars.ml @@ -0,0 +1,84 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* raise Not_found + | p :: tl -> + if Sys.file_exists (Filename.concat p f) + then p + else which tl f + +let guess_camlbin () = + let path = try Sys.getenv "PATH" with _ -> raise Not_found in + let lpath = path_to_list path in + which lpath "ocamlc" + +let guess_camlp4bin () = + let path = try Sys.getenv "PATH" with _ -> raise Not_found in + let lpath = path_to_list path in + which lpath Coq_config.camlp4 + +let camlbin () = + if !Flags.camlbin_spec then !Flags.camlbin else + if !Flags.boot then Coq_config.camlbin else + try guess_camlbin () with _ -> Coq_config.camlbin + +let camllib () = + if !Flags.boot + then Coq_config.camllib + else + let camlbin = camlbin () in + let com = (Filename.concat camlbin "ocamlc") ^ " -where" in + let _,res = System.run_command (fun x -> x) (fun _ -> ()) com in + Util.strip res + +(* TODO : essayer aussi camlbin *) +let camlp4bin () = + if !Flags.camlp4bin_spec then !Flags.camlp4bin else + if !Flags.boot then Coq_config.camlp4bin else + try guess_camlp4bin () with _ -> Coq_config.camlp4bin + +let camlp4lib () = + if !Flags.boot + then Coq_config.camlp4lib + else + let camlp4bin = camlp4bin () in + let com = (Filename.concat camlp4bin Coq_config.camlp4) ^ " -where" in + let _,res = System.run_command (fun x -> x) (fun _ -> ()) com in + Util.strip res + + diff --git a/lib/envars.mli b/lib/envars.mli new file mode 100644 index 00000000..62d0cb61 --- /dev/null +++ b/lib/envars.mli @@ -0,0 +1,15 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* string +val coqbin : unit -> string + +val camlbin : unit -> string +val camlp4bin : unit -> string +val camllib : unit -> string +val camlp4lib : unit -> string diff --git a/lib/flags.ml b/lib/flags.ml index 16ae0c64..928912e6 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -6,13 +6,18 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: flags.ml 11309 2008-08-06 10:30:35Z herbelin $ i*) +(*i $Id: flags.ml 11801 2009-01-18 20:11:41Z herbelin $ i*) let with_option o f x = let old = !o in o:=true; try let r = f x in o := old; r with e -> o := old; raise e +let without_option o f x = + let old = !o in o:=false; + try let r = f x in o := old; r + with e -> o := old; raise e + let boot = ref false let batch_mode = ref false @@ -33,13 +38,10 @@ let raw_print = ref false let unicode_syntax = 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 +let beautify = ref false +let make_beautify f = beautify := f +let do_beautify () = !beautify +let beautify_file = ref false (* Silent / Verbose *) let silent = ref false @@ -47,16 +49,8 @@ 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 silently f x = with_option silent f x +let verbosely f x = without_option silent f x let if_silent f x = if !silent then f x let if_verbose f x = if not !silent then f x @@ -82,33 +76,13 @@ 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 *) +(* 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 *) +(* Flags for external tools *) let subst_command_placeholder s t = let buff = Buffer.create (String.length s + String.length t) in @@ -127,3 +101,16 @@ let browser_cmd_fmt = Sys.getenv coq_netscape_remote_var with Not_found -> Coq_config.browser + +(* Options for changing coqlib *) +let coqlib_spec = ref false +let coqlib = ref Coq_config.coqlib + +(* Options for changing camlbin (used by coqmktop) *) +let camlbin_spec = ref false +let camlbin = ref Coq_config.camlbin + +(* Options for changing camlp4bin (used by coqmktop) *) +let camlp4bin_spec = ref false +let camlp4bin = ref Coq_config.camlp4bin + diff --git a/lib/flags.mli b/lib/flags.mli index 1fcae990..c5903285 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: flags.mli 10921 2008-05-12 12:27:25Z msozeau $ i*) +(*i $Id: flags.mli 11801 2009-01-18 20:11:41Z herbelin $ i*) (* Global options of the system. *) @@ -29,16 +29,16 @@ val raw_print : bool ref val unicode_syntax : bool ref -val translate : bool ref -val make_translate : bool -> unit -val do_translate : unit -> bool -val translate_file : bool ref -val translate_syntax : bool ref +val beautify : bool ref +val make_beautify : bool -> unit +val do_beautify : unit -> bool +val beautify_file : bool ref val make_silent : bool -> unit val is_silent : unit -> bool val is_verbose : unit -> bool val silently : ('a -> 'b) -> 'a -> 'b +val verbosely : ('a -> 'b) -> 'a -> 'b val if_silent : ('a -> unit) -> 'a -> unit val if_verbose : ('a -> unit) -> 'a -> unit @@ -47,9 +47,13 @@ val if_warn : ('a -> unit) -> 'a -> unit val hash_cons_proofs : bool ref -(* Temporary activate an option ('c must be an atomic type) *) +(* Temporary activate an option (to activate option [o] on [f x y z], + use [with_option o (f x y) z]) *) val with_option : bool ref -> ('a -> 'b) -> 'a -> 'b +(* Temporary deactivate an option *) +val without_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 @@ -57,12 +61,6 @@ 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 @@ -75,3 +73,13 @@ val browser_cmd_fmt : string (* Substitute %s in the first chain by the second chain *) val subst_command_placeholder : string -> string -> string + +(* Options for specifying where coq librairies reside *) +val coqlib_spec : bool ref +val coqlib : string ref + +(* Options for specifying where OCaml binaries reside *) +val camlbin_spec : bool ref +val camlbin : string ref +val camlp4bin_spec : bool ref +val camlp4bin : string ref diff --git a/lib/option.ml b/lib/option.ml index 34749b8c..85efdd44 100644 --- a/lib/option.ml +++ b/lib/option.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: option.ml 10739 2008-04-01 14:45:20Z herbelin $ i*) +(*i $Id: option.ml 11576 2008-11-10 19:13:15Z msozeau $ i*) (** Module implementing basic combinators for OCaml option type. It tries follow closely the style of OCaml standard library. @@ -97,6 +97,10 @@ let fold_right f x a = | Some y -> f y a | _ -> a +(** [cata f a x] is [a] if [x] is [None] and [f y] if [x] is [Some y]. *) +let cata f a = function + | Some c -> f c + | None -> a (** {6 More Specific operations} ***) diff --git a/lib/option.mli b/lib/option.mli index d9c18d88..6fa89098 100644 --- a/lib/option.mli +++ b/lib/option.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: option.mli 10739 2008-04-01 14:45:20Z herbelin $ *) +(* $Id: option.mli 11576 2008-11-10 19:13:15Z msozeau $ *) (** Module implementing basic combinators for OCaml option type. It tries follow closely the style of OCaml standard library. @@ -66,6 +66,8 @@ val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option -> 'c option -> 'a (** [fold_right f x a] is [f y a] if [x] is [Some y], and [a] otherwise. *) val fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b +(** [cata e f x] is [e] if [x] is [None] and [f a] if [x] is [Some a] *) +val cata : ('a -> 'b) -> 'b -> 'a option -> 'b (** {6 More Specific Operations} ***) diff --git a/lib/system.ml b/lib/system.ml index 22eb52ee..65826c81 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: system.ml 11209 2008-07-05 10:17:49Z herbelin $ *) +(* $Id: system.ml 11801 2009-01-18 20:11:41Z herbelin $ *) open Pp open Util @@ -63,6 +63,34 @@ type load_path = physical_path list let physical_path_of_string s = s let string_of_physical_path p = p +(* Hints to partially detects if two paths refer to the same repertory *) +let rec remove_path_dot p = + let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *) + let n = String.length curdir in + if String.length p > n && String.sub p 0 n = curdir then + remove_path_dot (String.sub p n (String.length p - n)) + else + p + +let strip_path p = + let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *) + let n = String.length cwd in + if String.length p > n && String.sub p 0 n = cwd then + remove_path_dot (String.sub p n (String.length p - n)) + else + remove_path_dot p + +let canonical_path_name p = + let current = Sys.getcwd () in + try + Sys.chdir p; + let p' = Sys.getcwd () in + Sys.chdir current; + p' + with Sys_error _ -> + (* We give up to find a canonical name and just simplify it... *) + strip_path p + (* All subdirectories, recursively *) let exists_dir dir = @@ -100,7 +128,7 @@ let all_subdirs ~unix_path:root = if exists_dir root then traverse root []; List.rev !l -let where_in_path warn path filename = +let where_in_path ?(warn=true) path filename = let rec search = function | lpe :: rem -> let f = Filename.concat lpe filename in @@ -116,25 +144,26 @@ let where_in_path warn path filename = msg_warning (str filename ++ str " has been found in" ++ spc () ++ hov 0 (str "[ " ++ - hv 0 (prlist_with_sep pr_semicolon (fun (lpe,_) -> str lpe) l) + hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon()) + (fun (lpe,_) -> str lpe) l) ++ str " ];") ++ fnl () ++ str "loading " ++ str f); (lpe, f) in check_and_warn (search path) -let find_file_in_path paths filename = +let find_file_in_path ?(warn=true) paths filename = if not (Filename.is_implicit filename) then let root = Filename.dirname filename in root, filename else - try where_in_path true paths filename + try where_in_path ~warn paths filename with Not_found -> errorlabstrm "System.find_file_in_path" (hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++ str "on loadpath")) let is_in_path lpath filename = - try ignore (where_in_path false lpath filename); true + try ignore (where_in_path ~warn:false lpath filename); true with Not_found -> false let make_suffix name suffix = @@ -172,7 +201,7 @@ let raw_extern_intern magic suffix = in (extern_state,intern_state) -let extern_intern magic suffix = +let extern_intern ?(warn=true) magic suffix = let (raw_extern,raw_intern) = raw_extern_intern magic suffix in let extern_state name val_0 = try @@ -185,7 +214,7 @@ let extern_intern magic suffix = with Sys_error s -> error ("System error: " ^ s) and intern_state paths name = try - let _,filename = find_file_in_path paths (make_suffix name suffix) in + let _,filename = find_file_in_path ~warn paths (make_suffix name suffix) in let channel = raw_intern filename in let v = marshal_in channel in close_in channel; diff --git a/lib/system.mli b/lib/system.mli index eb83cbf8..ba5aa408 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: system.mli 11209 2008-07-05 10:17:49Z herbelin $ i*) +(*i $Id: system.mli 11801 2009-01-18 20:11:41Z herbelin $ i*) (*s Files and load paths. Load path entries remember the original root given by the user. For efficiency, we keep the full path (field @@ -16,11 +16,13 @@ type physical_path = string type load_path = physical_path list +val canonical_path_name : string -> string + val exclude_search_in_dirname : string -> unit val all_subdirs : unix_path:string -> (physical_path * string list) list val is_in_path : load_path -> string -> bool -val where_in_path : bool -> load_path -> string -> physical_path * string +val where_in_path : ?warn:bool -> load_path -> string -> physical_path * string val physical_path_of_string : string -> physical_path val string_of_physical_path : physical_path -> string @@ -34,7 +36,8 @@ val home : string val exists_dir : string -> bool -val find_file_in_path : load_path -> string -> physical_path * string +val find_file_in_path : + ?warn:bool -> load_path -> string -> physical_path * string (*s Generic input and output functions, parameterized by a magic number and a suffix. The intern functions raise the exception [Bad_magic_number] @@ -48,8 +51,8 @@ exception Bad_magic_number of string val raw_extern_intern : int -> string -> (string -> string * out_channel) * (string -> in_channel) -val extern_intern : - int -> string -> (string -> 'a -> unit) * (load_path -> string -> 'a) +val extern_intern : ?warn:bool -> int -> string -> + (string -> 'a -> unit) * (load_path -> string -> 'a) (*s Sending/receiving once with external executable *) diff --git a/lib/util.ml b/lib/util.ml index a19cc65b..a73a5558 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: util.ml 11350 2008-09-02 15:37:49Z barras $ *) +(* $Id: util.ml 11845 2009-01-22 18:55:08Z letouzey $ *) open Pp @@ -59,6 +59,9 @@ let is_letter c = (c >= 'a' && c <= 'z') or (c >= 'A' && c <= 'Z') let is_digit c = (c >= '0' && c <= '9') let is_ident_tail c = is_letter c or is_digit c or c = '\'' or c = '_' +let is_blank = function + | ' ' | '\r' | '\t' | '\n' -> true + | _ -> false (* Strings *) @@ -73,6 +76,21 @@ let explode s = let implode sl = String.concat "" sl +let strip s = + let n = String.length s in + let rec lstrip_rec i = + if i < n && is_blank s.[i] then + lstrip_rec (i+1) + else i + in + let rec rstrip_rec i = + if i >= 0 && is_blank s.[i] then + rstrip_rec (i-1) + else i + in + let a = lstrip_rec 0 and b = rstrip_rec (n-1) in + String.sub s a (b-a+1) + (* substring searching... *) (* gdzie = where, co = what *) @@ -83,6 +101,9 @@ let rec is_sub gdzie gl gi co cl ci = (is_sub gdzie gl (gi+1) co cl (ci+1))) let rec raw_str_index i gdzie l c co cl = + (* First adapt to ocaml 3.11 new semantics of index_from *) + if (i+cl > l) then raise Not_found; + (* Then proceed as in ocaml < 3.11 *) let i' = String.index_from gdzie i c in if (i'+cl <= l) && (is_sub gdzie l i' co cl 0) then i' else raw_str_index (i'+1) gdzie l c co cl @@ -106,19 +127,23 @@ let ordinal n = (* string parsing *) -let parse_loadpath s = +let split_string_at c s = let len = String.length s in - let rec decoupe_dirs n = + let rec split n = try - let pos = String.index_from s n '/' in - if pos = n then - invalid_arg "parse_loadpath: find an empty dir in loadpath"; + let pos = String.index_from s n c in let dir = String.sub s n (pos-n) in - dir :: (decoupe_dirs (succ pos)) + dir :: split (succ pos) with | Not_found -> [String.sub s n (len-n)] in - if len = 0 then [] else decoupe_dirs 0 + if len = 0 then [] else split 0 + +let parse_loadpath s = + let l = split_string_at '/' s in + if List.mem "" l then + invalid_arg "parse_loadpath: find an empty dir in loadpath"; + l module Stringset = Set.Make(struct type t = string let compare = compare end) @@ -239,6 +264,8 @@ let classify_unicode unicode = end | _ -> begin match unicode with + (* utf-8 CJC Symbols and Punctuation *) + | x when 0x3008 <= x & x <= 0x3020 -> UnicodeSymbol (* utf-8 Hiragana U3040-309F and Katakana U30A0-30FF *) | x when 0x3040 <= x & x <= 0x30FF -> UnicodeLetter (* utf-8 Unified CJK Ideographs U4E00-9FA5 *) @@ -304,27 +331,40 @@ let next_utf8 s i = (* Check the well-formedness of an identifier *) -let check_ident s = +let check_initial handle j n s = + match classify_unicode n with + | UnicodeLetter -> () + | _ -> + let c = String.sub s 0 j in + handle ("Invalid character '"^c^"' at beginning of identifier \""^s^"\".") + +let check_trailing handle i j n s = + match classify_unicode n with + | UnicodeLetter | UnicodeIdentPart -> () + | _ -> + let c = String.sub s i j in + handle ("Invalid character '"^c^"' in identifier \""^s^"\".") + +let check_ident_gen handle s = let i = ref 0 in if s <> ".." then try let j, n = next_utf8 s 0 in - match classify_unicode n with - | UnicodeLetter -> - i := !i + j; - begin try - while true do - let j, n = next_utf8 s !i in - match classify_unicode n with - | UnicodeLetter | UnicodeIdentPart -> i := !i + j - | _ -> error - ("invalid character "^(String.sub s !i j)^" in identifier "^s) - done - with End_of_input -> () end - | _ -> error (s^": an identifier should start with a letter") + check_initial handle j n s; + i := !i + j; + try + while true do + let j, n = next_utf8 s !i in + check_trailing handle !i j n s; + i := !i + j + done + with End_of_input -> () with - | End_of_input -> error "The empty string is not an identifier" - | UnsupportedUtf8 -> error (s^": unsupported character in utf8 sequence") - | Invalid_argument _ -> error (s^": invalid utf8 sequence") + | End_of_input -> error "The empty string is not an identifier." + | UnsupportedUtf8 -> error (s^": unsupported character in utf8 sequence.") + | Invalid_argument _ -> error (s^": invalid utf8 sequence.") + +let check_ident_soft = check_ident_gen warning +let check_ident = check_ident_gen error let lowercase_unicode s unicode = match unicode land 0x1F000 with @@ -626,6 +666,10 @@ let rec list_remove_first a = function | b::l -> b::list_remove_first a l | [] -> raise Not_found +let rec list_remove_assoc_in_triple x = function + | [] -> [] + | (y,_,_ as z)::l -> if x = y then l else z::list_remove_assoc_in_triple x l + let list_add_set x l = if List.mem x l then l else x::l let list_eq_set l1 l2 = @@ -726,13 +770,21 @@ let list_subset l1 l2 = in look l1 -let list_splitby p = - let rec splitby_loop x y = +let list_split_at p = + let rec split_at_loop x y = match y with | [] -> ([],[]) - | (a::l) -> if (p a) then (x,y) else (splitby_loop (x@[a]) l) + | (a::l) -> if (p a) then (List.rev x,y) else split_at_loop (a::x) l + in + split_at_loop [] + +let list_split_by p = + let rec split_loop = function + | [] -> ([],[]) + | (a::l) -> + let (l1,l2) = split_loop l in if (p a) then (a::l1,l2) else (l1,a::l2) in - splitby_loop [] + split_loop let rec list_split3 = function | [] -> ([], [], []) @@ -859,6 +911,20 @@ let list_cartesians op init ll = let list_combinations l = list_cartesians (fun x l -> x::l) [] l +(* Keep only those products that do not return None *) + +let rec list_cartesian_filter op l1 l2 = + list_map_append (fun x -> list_map_filter (op x) l2) l1 + +(* Keep only those products that do not return None *) + +let rec list_cartesians_filter op init ll = + List.fold_right (list_cartesian_filter op) ll [init] + +(* Drop the last element of a list *) + +let rec list_drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> hd :: list_drop_last tl + (* Arrays *) let array_exists f v = @@ -902,6 +968,10 @@ let array_for_all4 f v1 v2 v3 v4 = lv1 = Array.length v4 && allrec (pred lv1) +let array_for_all_i f i v = + let rec allrec i n = n = Array.length v || f i v.(n) && allrec (i+1) (n+1) in + allrec i 0 + let array_hd v = match Array.length v with | 0 -> failwith "array_hd" @@ -1117,15 +1187,15 @@ let array_fold_map2' f v1 v2 e = (v',!e') let array_distinct v = + let visited = Hashtbl.create 23 in try - for i=0 to Array.length v-1 do - for j=i+1 to Array.length v-1 do - if v.(i)=v.(j) then raise Exit - done - done; + Array.iter + (fun x -> + if Hashtbl.mem visited x then raise Exit + else Hashtbl.add visited x x) + v; true - with Exit -> - false + with Exit -> false let array_union_map f a acc = Array.fold_left @@ -1209,11 +1279,13 @@ let rec prlist elem l = match l with | h::t -> Stream.lapp (fun () -> elem h) (prlist elem t) (* unlike all other functions below, [prlist] works lazily. - if a strict behavior is needed, use [prlist_strict] instead. *) + if a strict behavior is needed, use [prlist_strict] instead. + evaluation is done from left to right. *) let rec prlist_strict elem l = match l with | [] -> mt () - | h::t -> (elem h)++(prlist_strict elem t) + | h::t -> + let e = elem h in let r = prlist_strict elem t in e++r (* [prlist_with_sep sep pr [a ; ... ; c]] outputs [pr a ++ sep() ++ ... ++ sep() ++ pr c] *) @@ -1275,7 +1347,7 @@ let prvect_with_sep sep elem v = let prvect elem v = prvect_with_sep mt elem v let pr_located pr (loc,x) = - if Flags.do_translate() && loc<>dummy_loc then + if Flags.do_beautify() && loc<>dummy_loc then let (b,e) = unloc loc in comment b ++ pr x ++ comment e else pr x diff --git a/lib/util.mli b/lib/util.mli index 99ad3c03..3cd934e7 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(*i $Id: util.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) +(*i $Id: util.mli 11769 2009-01-08 17:59:22Z glondu $ i*) (*i*) open Pp @@ -68,15 +68,18 @@ val pi3 : 'a * 'b * 'c -> 'c val is_letter : char -> bool val is_digit : char -> bool val is_ident_tail : char -> bool +val is_blank : char -> bool (*s Strings. *) val explode : string -> string list val implode : string list -> string +val strip : string -> string val string_index_from : string -> int -> string -> int val string_string_contains : where:string -> what:string -> bool val plural : int -> string -> string val ordinal : int -> string +val split_string_at : char -> string -> string list val parse_loadpath : string -> string list @@ -89,6 +92,7 @@ exception UnsupportedUtf8 val classify_unicode : int -> utf8_status val check_ident : string -> unit +val check_ident_soft : string -> unit val lowercase_first_char_utf8 : string -> string (*s Lists. *) @@ -137,6 +141,7 @@ val list_for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool val list_except : 'a -> 'a list -> 'a list val list_remove : 'a -> 'a list -> 'a list val list_remove_first : 'a -> 'a list -> 'a list +val list_remove_assoc_in_triple : 'a -> ('a * 'b * 'c) list -> ('a * 'b * 'c) list val list_for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool val list_sep_last : 'a list -> 'a * 'a list val list_try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b @@ -145,7 +150,8 @@ val list_uniquize : 'a list -> 'a list (* merges two sorted lists and preserves the uniqueness property: *) val list_merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list val list_subset : 'a list -> 'a list -> bool -val list_splitby : ('a -> bool) -> 'a list -> 'a list * 'a list +val list_split_at : ('a -> bool) -> 'a list -> 'a list * 'a list +val list_split_by : ('a -> bool) -> 'a list -> 'a list * 'a list val list_split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list val list_partition_by : ('a -> 'a -> bool) -> 'a list -> 'a list list val list_firstn : int -> 'a list -> 'a list @@ -155,6 +161,7 @@ val list_skipn : int -> 'a list -> 'a list val list_addn : int -> 'a -> 'a list -> 'a list val list_prefix_of : 'a list -> 'a list -> bool val list_drop_prefix : 'a list -> 'a list -> 'a list +val list_drop_last : 'a list -> 'a list (* [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *) val list_map_append : ('a -> 'b list) -> 'a list -> 'b list val list_join_map : ('a -> 'b list) -> 'a list -> 'b list @@ -175,6 +182,11 @@ val list_cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list val list_cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list (* list_combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *) val list_combinations : 'a list list -> 'a list list +(* Keep only those products that do not return None *) +val list_cartesian_filter : + ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list +val list_cartesians_filter : + ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list val list_union_map : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b @@ -187,6 +199,7 @@ val array_for_all3 : ('a -> 'b -> 'c -> bool) -> 'a array -> 'b array -> 'c array -> bool val array_for_all4 : ('a -> 'b -> 'c -> 'd -> bool) -> 'a array -> 'b array -> 'c array -> 'd array -> bool +val array_for_all_i : (int -> 'a -> bool) -> int -> 'a array -> bool val array_hd : 'a array -> 'a val array_tl : 'a array -> 'a array val array_last : 'a array -> 'a -- cgit v1.2.3