diff options
Diffstat (limited to 'lib')
42 files changed, 854 insertions, 408 deletions
diff --git a/lib/bigint.ml b/lib/bigint.ml new file mode 100644 index 00000000..5bcceb5c --- /dev/null +++ b/lib/bigint.ml @@ -0,0 +1,392 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: bigint.ml 7305 2005-08-19 19:51:02Z letouzey $ *) + +(*i*) +open Pp +(*i*) + +(***************************************************) +(* Basic operations on (unbounded) integer numbers *) +(***************************************************) + +(* An integer is canonically represented as an array of k-digits blocs. + + 0 is represented by the empty array and -1 by the singleton [|-1|]. + The first bloc is in the range ]0;10^k[ for positive numbers. + The first bloc is in the range ]-10^k;-1[ for negative ones. + All other blocs are numbers in the range [0;10^k[. + + Negative numbers are represented using 2's complementation. For instance, + with 4-digits blocs, [-9655;6789] denotes -96543211 +*) + +(* The base is a power of 10 in order to facilitate the parsing and printing + of numbers in digital notation. + + All functions, to the exception of to_string and of_string should work + with an arbitrary base, even if not a power of 10. + + In practice, we set k=4 so that no overflow in ocaml machine words + (i.e. the interval [-2^30;2^30-1]) occur when multiplying two + numbers less than (10^k) +*) + +(* The main parameters *) + +let size = + let rec log10 n = if n < 10 then 0 else 1 + log10 (n / 10) in + (log10 max_int) / 2 + +let format_size = + (* How to parametrize a printf format *) + if size = 4 then Printf.sprintf "%04d" + else fun n -> + let rec aux j l n = + if j=size then l else aux (j+1) (string_of_int (n mod 10) :: l) (n/10) + in String.concat "" (aux 0 [] n) + +(* The base is 10^size *) +let base = + let rec exp10 = function 0 -> 1 | n -> 10 * exp10 (n-1) in exp10 size + +(* Basic numbers *) +let zero = [||] +let neg_one = [|-1|] + +(* Sign of an integer *) +let is_strictly_neg n = n<>[||] && n.(0) < 0 +let is_strictly_pos n = n<>[||] && n.(0) > 0 +let is_neg_or_zero n = n=[||] or n.(0) < 0 +let is_pos_or_zero n = n=[||] or n.(0) > 0 + +let normalize_pos n = + let k = ref 0 in + while !k < Array.length n & n.(!k) = 0 do incr k done; + Array.sub n !k (Array.length n - !k) + +let normalize_neg n = + let k = ref 1 in + while !k < Array.length n & n.(!k) = base - 1 do incr k done; + let n' = Array.sub n !k (Array.length n - !k) in + if Array.length n' = 0 then [|-1|] else (n'.(0) <- n'.(0) - base; n') + +let rec normalize n = + if Array.length n = 0 then n else + if n.(0) = -1 then normalize_neg n else normalize_pos n + +let neg m = + if m = zero then zero else + let n = Array.copy m in + let i = ref (Array.length m - 1) in + while !i > 0 & n.(!i) = 0 do decr i done; + if !i > 0 then begin + n.(!i) <- base - n.(!i); decr i; + while !i > 0 do n.(!i) <- base - 1 - n.(!i); decr i done; + n.(0) <- - n.(0) - 1; + if n.(0) < -1 then (n.(0) <- n.(0) + base; Array.append [| -1 |] n) else + if n.(0) = - base then (n.(0) <- 0; Array.append [| -1 |] n) + else normalize n + end else (n.(0) <- - n.(0); n) + +let push_carry r j = + let j = ref j in + while !j > 0 & r.(!j) < 0 do + r.(!j) <- r.(!j) + base; decr j; r.(!j) <- r.(!j) - 1 + done; + while !j > 0 & r.(!j) >= base do + r.(!j) <- r.(!j) - base; decr j; r.(!j) <- r.(!j) + 1 + done; + if r.(0) >= base then (r.(0) <- r.(0) - base; Array.append [| 1 |] r) + else if r.(0) < -base then (r.(0) <- r.(0) + 2*base; Array.append [| -2 |] r) + else if r.(0) = -base then (r.(0) <- 0; Array.append [| -1 |] r) + else normalize r + +let add_to r a j = + if a = zero then r else begin + for i = Array.length r - 1 downto j+1 do + r.(i) <- r.(i) + a.(i-j); + if r.(i) >= base then (r.(i) <- r.(i) - base; r.(i-1) <- r.(i-1) + 1) + done; + r.(j) <- r.(j) + a.(0); + push_carry r j + end + +let add n m = + let d = Array.length n - Array.length m in + if d > 0 then add_to (Array.copy n) m d else add_to (Array.copy m) n (-d) + +let sub_to r a j = + if a = zero then r else begin + for i = Array.length r - 1 downto j+1 do + r.(i) <- r.(i) - a.(i-j); + if r.(i) < 0 then (r.(i) <- r.(i) + base; r.(i-1) <- r.(i-1) - 1) + done; + r.(j) <- r.(j) - a.(0); + push_carry r j + end + +let sub n m = + let d = Array.length n - Array.length m in + if d >= 0 then sub_to (Array.copy n) m d + else let r = neg m in add_to r n (Array.length r - Array.length n) + +let rec mult m n = + if m = zero or n = zero then zero else + let l = Array.length m + Array.length n in + let r = Array.create l 0 in + for i = Array.length m - 1 downto 0 do + for j = Array.length n - 1 downto 0 do + let p = m.(i) * n.(j) + r.(i+j+1) in + let (q,s) = + if p < 0 + then (p + 1) / base - 1, (p + 1) mod base + base - 1 + else p / base, p mod base in + r.(i+j+1) <- s; + if q <> 0 then r.(i+j) <- r.(i+j) + q; + done + done; + normalize r + +let rec less_than_same_size m n i j = + i < Array.length m && + (m.(i) < n.(j) or (m.(i) = n.(j) && less_than_same_size m n (i+1) (j+1))) + +let less_than m n = + if is_strictly_neg m then + is_pos_or_zero n or Array.length m > Array.length n + or (Array.length m = Array.length n && less_than_same_size m n 0 0) + else + is_strictly_pos n && (Array.length m < Array.length n or + (Array.length m = Array.length n && less_than_same_size m n 0 0)) + +let equal m n = (m = n) + +let less_or_equal_than m n = equal m n or less_than m n + +let less_than_shift_pos k m n = + (Array.length m - k < Array.length n) + or (Array.length m - k = Array.length n && less_than_same_size m n k 0) + +let rec can_divide k m d i = + (i = Array.length d) or + (m.(k+i) > d.(i)) or + (m.(k+i) = d.(i) && can_divide k m d (i+1)) + +(* computes m - d * q * base^(|m|-k) in-place on positive numbers *) +let sub_mult m d q k = + if q <> 0 then + for i = Array.length d - 1 downto 0 do + let v = d.(i) * q in + m.(k+i) <- m.(k+i) - v mod base; + if m.(k+i) < 0 then (m.(k+i) <- m.(k+i) + base; m.(k+i-1) <- m.(k+i-1) -1); + if v >= base then m.(k+i-1) <- m.(k+i-1) - v / base; + done + +let euclid m d = + let isnegm, m = + if is_strictly_neg m then (-1),neg m else 1,Array.copy m in + let isnegd, d = if is_strictly_neg d then (-1),neg d else 1,d in + if d = zero then raise Division_by_zero; + let q,r = + if less_than m d then (zero,m) else + let ql = Array.length m - Array.length d in + let q = Array.create (ql+1) 0 in + let i = ref 0 in + while not (less_than_shift_pos !i m d) do + if m.(!i)=0 then incr i else + if can_divide !i m d 0 then begin + let v = + if Array.length d > 1 && d.(0) <> m.(!i) then + (m.(!i) * base + m.(!i+1)) / (d.(0) * base + d.(1) + 1) + else + m.(!i) / d.(0) in + q.(!i) <- q.(!i) + v; + sub_mult m d v !i + end else begin + let v = (m.(!i) * base + m.(!i+1)) / (d.(0) + 1) in + q.(!i) <- q.(!i) + v / base; + sub_mult m d (v / base) !i; + q.(!i+1) <- q.(!i+1) + v mod base; + if q.(!i+1) >= base then + (q.(!i+1) <- q.(!i+1)-base; q.(!i) <- q.(!i)+1); + sub_mult m d (v mod base) (!i+1) + end + done; + (normalize q, normalize m) in + (if isnegd * isnegm = -1 then neg q else q), + (if isnegm = -1 then neg r else r) + +(* Parsing/printing ordinary 10-based numbers *) + +let of_string s = + let isneg = String.length s > 1 & s.[0] = '-' in + let n = if isneg then 1 else 0 in + let d = ref n in + while !d < String.length s && s.[!d] = '0' do incr d done; + if !d = String.length s then zero else + let r = (String.length s - !d) mod size in + let h = String.sub s (!d) r in + if !d = String.length s - 1 && isneg && h="1" then neg_one else + let e = if h<>"" then 1 else 0 in + let l = (String.length s - !d) / size in + let a = Array.create (l + e + n) 0 in + if isneg then begin + a.(0) <- (-1); + let carry = ref 0 in + for i=l downto 1 do + let v = int_of_string (String.sub s ((i-1)*size + !d +r) size)+ !carry in + if v <> 0 then (a.(i+e)<- base - v; carry := 1) else carry := 0 + done; + if e=1 then a.(1) <- base - !carry - int_of_string h; + end + else begin + if e=1 then a.(0) <- int_of_string h; + for i=1 to l do + a.(i+e-1) <- int_of_string (String.sub s ((i-1)*size + !d + r) size) + done + end; + a + +let to_string_pos sgn n = + if Array.length n = 0 then "0" else + sgn ^ + String.concat "" + (string_of_int n.(0) :: List.map format_size (List.tl (Array.to_list n))) + +let to_string n = + if is_strictly_neg n then to_string_pos "-" (neg n) + else to_string_pos "" n + +(******************************************************************) +(* Optimized operations on (unbounded) integer numbers *) +(* integers smaller than base are represented as machine integers *) +(******************************************************************) + +type bigint = Obj.t + +let ints_of_int n = + if n >= base then [| n / base; n mod base |] + else if n <= - base then [| n / base - 1; n mod base + base |] + else if n = 0 then [| |] else [| n |] + +let big_of_int n = + if n >= base then Obj.repr [| n / base; n mod base |] + else if n <= - base then Obj.repr [| n / base - 1; n mod base + base |] + else Obj.repr n + +let big_of_ints n = + let n = normalize n in + if n = zero then Obj.repr 0 else + if Array.length n = 1 then Obj.repr n.(0) else + Obj.repr n + +let coerce_to_int = (Obj.magic : Obj.t -> int) +let coerce_to_ints = (Obj.magic : Obj.t -> int array) + +let ints_of_z n = + if Obj.is_int n then ints_of_int (coerce_to_int n) + else coerce_to_ints n + +let app_pair f (m, n) = + (f m, f n) + +let add m n = + if Obj.is_int m & Obj.is_int n + then big_of_int (coerce_to_int m + coerce_to_int n) + else big_of_ints (add (ints_of_z m) (ints_of_z n)) + +let sub m n = + if Obj.is_int m & Obj.is_int n + then big_of_int (coerce_to_int m - coerce_to_int n) + else big_of_ints (sub (ints_of_z m) (ints_of_z n)) + +let mult m n = + if Obj.is_int m & Obj.is_int n + then big_of_int (coerce_to_int m * coerce_to_int n) + else big_of_ints (mult (ints_of_z m) (ints_of_z n)) + +let euclid m n = + if Obj.is_int m & Obj.is_int n + then app_pair big_of_int + (coerce_to_int m / coerce_to_int n, coerce_to_int m mod coerce_to_int n) + else app_pair big_of_ints (euclid (ints_of_z m) (ints_of_z n)) + +let less_than m n = + if Obj.is_int m & Obj.is_int n + then coerce_to_int m < coerce_to_int n + else less_than (ints_of_z m) (ints_of_z n) + +let neg n = + if Obj.is_int n then big_of_int (- (coerce_to_int n)) + else big_of_ints (neg (ints_of_z n)) + +let of_string m = big_of_ints (of_string m) +let to_string m = to_string (ints_of_z m) + +let zero = big_of_int 0 +let one = big_of_int 1 +let sub_1 n = sub n one +let add_1 n = add n one +let two = big_of_int 2 +let neg_two = big_of_int (-2) +let mult_2 n = add n n +let is_zero n = n=zero + +let div2_with_rest n = + let (q,b) = euclid n two in + (q, b = one) + +let is_strictly_neg n = is_strictly_neg (ints_of_z n) +let is_strictly_pos n = is_strictly_pos (ints_of_z n) +let is_neg_or_zero n = is_neg_or_zero (ints_of_z n) +let is_pos_or_zero n = is_pos_or_zero (ints_of_z n) + +let pr_bigint n = str (to_string n) + +(* Testing suite *) + +let check () = + let numbers = [ + "1";"2";"99";"100";"101";"9999";"10000";"10001"; + "999999";"1000000";"1000001";"99999999";"100000000";"100000001"; + "1234";"5678";"12345678";"987654321"; + "-1";"-2";"-99";"-100";"-101";"-9999";"-10000";"-10001"; + "-999999";"-1000000";"-1000001";"-99999999";"-100000000";"-100000001"; + "-1234";"-5678";"-12345678";"-987654321";"0" + ] + in + let eucl n m = + let n' = abs_float n and m' = abs_float m in + let q' = floor (n' /. m') in let r' = n' -. m' *. q' in + (if n *. m < 0. & q' <> 0. then -. q' else q'), + (if n < 0. then -. r' else r') in + let round f = floor (abs_float f +. 0.5) *. (if f < 0. then -1. else 1.) in + let i = ref 0 in + let compare op n n' = + incr i; + let s = Printf.sprintf "%30s" (to_string n) in + let s' = Printf.sprintf "% 30.0f" (round n') in + if s <> s' then Printf.printf "%s: %s <> %s\n" op s s' in +List.iter (fun a -> List.iter (fun b -> + let n = of_string a and m = of_string b in + let n' = float_of_string a and m' = float_of_string b in + let a = add n m and a' = n' +. m' in + let s = sub n m and s' = n' -. m' in + let p = mult n m and p' = n' *. m' in + let q,r = try euclid n m with Division_by_zero -> zero,zero + and q',r' = eucl n' m' in + compare "+" a a'; + compare "-" s s'; + compare "*" p p'; + compare "/" q q'; + compare "%" r r') numbers) numbers; + Printf.printf "%i tests done\n" !i + + diff --git a/lib/bigint.mli b/lib/bigint.mli new file mode 100644 index 00000000..7a835a49 --- /dev/null +++ b/lib/bigint.mli @@ -0,0 +1,45 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: bigint.mli 6616 2005-01-21 17:18:23Z herbelin $ i*) + +(*i*) +open Pp +(*i*) + +(* Arbitrary large integer numbers *) + +type bigint + +val of_string : string -> bigint +val to_string : bigint -> string + +val zero : bigint +val one : bigint +val two : bigint + +val div2_with_rest : bigint -> bigint * bool (* true=odd; false=even *) +val add_1 : bigint -> bigint +val sub_1 : bigint -> bigint +val mult_2 : bigint -> bigint + +val add : bigint -> bigint -> bigint +val sub : bigint -> bigint -> bigint +val mult : bigint -> bigint -> bigint +val euclid : bigint -> bigint -> bigint * bigint + +val less_than : bigint -> bigint -> bool +val equal : bigint -> bigint -> bool + +val is_strictly_pos : bigint -> bool +val is_strictly_neg : bigint -> bool +val is_pos_or_zero : bigint -> bool +val is_neg_or_zero : bigint -> bool +val neg : bigint -> bigint + +val pr_bigint : bigint -> std_ppcmds diff --git a/lib/bignat.ml b/lib/bignat.ml deleted file mode 100644 index 583a027f..00000000 --- a/lib/bignat.ml +++ /dev/null @@ -1,116 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id: bignat.ml,v 1.5.6.1 2004/07/16 19:30:29 herbelin Exp $ *) - -(*i*) -open Pp -(*i*) - -(* Arbitrary big natural numbers *) - -type bignat = int array - -let digits = 8 -let base = 100000000 (* let enough room for multiplication by 2 *) -let base_div_2 = 50000000 -let base_to_string x = Printf.sprintf "%08d" x - -let of_string s = - let a = Array.create (String.length s / digits + 1) 0 in - let r = String.length s mod digits in - if r<>0 then a.(0) <- int_of_string (String.sub s 0 r); - for i = 1 to String.length s / digits do - a.(i) <- int_of_string (String.sub s ((i-1)*digits+r) digits) - done; - a - -let rec to_string s = - if s = [||] then "0" else - if s.(0) = 0 then to_string (Array.sub s 1 (Array.length s - 1)) - else - String.concat "" - ((string_of_int (s.(0))) - ::(List.tl (Array.to_list (Array.map base_to_string s)))) - -let is_nonzero a = - let b = ref false in Array.iter (fun x -> b := x <> 0 || !b) a; !b - -let zero = [|0|] -let one = [|1|] - -let is_one a = - let rec leading_zero i = i<0 || (a.(i) = 0 && leading_zero (i-1)) in - (a.(Array.length a - 1) = 1) && leading_zero (Array.length a - 2) - -let div2_with_rest n = - let len = Array.length n in - let q = Array.create len 0 in - for i = 0 to len - 2 do - q.(i) <- q.(i) + n.(i) / 2; q.(i + 1) <- base_div_2 * (n.(i) mod 2) - done; - q.(len - 1) <- q.(len - 1) + n.(len - 1) / 2; - q, (n.(len - 1) mod 2) = 1 - -let add_1 n = - let m = Array.copy n - and i = ref (Array.length n - 1) in - while !i >= 0 && m.(!i) = base-1 do - m.(!i) <- 0; decr i; - done; - if !i < 0 then begin - m.(0) <- 0; Array.concat [[| 1 |]; m] - end else begin - m.(!i) <- m.(!i) + 1; m - end - -let sub_1 n = - if is_nonzero n then - let m = Array.copy n - and i = ref (Array.length n - 1) in - while m.(!i) = 0 && !i > 0 do - m.(!i) <- base-1; decr i; - done; - m.(!i) <- m.(!i) - 1; - m - else n - -let rec mult_2 n = - let m = Array.copy n in - m.(Array.length n - 1) <- 2 * m.(Array.length n - 1); - for i = Array.length n - 2 downto 0 do - m.(i) <- 2 * m.(i); - if m.(i + 1) >= base then begin - m.(i + 1) <- m.(i + 1) - base; m.(i) <- m.(i) + 1 - end - done; - if m.(0) >= base then begin - m.(0) <- m.(0) - base; Array.concat [[| 1 |]; m] - end else - m - -let less_than m n = - let lm = ref 0 in - while !lm < Array.length m && m.(!lm) = 0 do incr lm done; - let ln = ref 0 in - while !ln < Array.length n && n.(!ln) = 0 do incr ln done; - let um = Array.length m - !lm and un = Array.length n - !ln in - let rec lt d = - d < um && (m.(!lm+d) < n.(!ln+d) || (m.(!lm+d) = n.(!ln+d) && lt (d+1))) - in - (um < un) || (um = un && lt 0) - -type bigint = POS of bignat | NEG of bignat - -let pr_bigint = function - | POS n -> str (to_string n) - | NEG n -> str "-" ++ str (to_string n) - -let bigint_to_string = function - | POS n -> to_string n - | NEG n -> "-" ^ (to_string n);; diff --git a/lib/bignat.mli b/lib/bignat.mli deleted file mode 100644 index 860bcf29..00000000 --- a/lib/bignat.mli +++ /dev/null @@ -1,37 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: bignat.mli,v 1.4.6.3 2005/01/21 17:14:11 herbelin Exp $ i*) - -(*i*) -open Pp -(*i*) - -(* Arbitrary big natural numbers *) - -type bignat - -val of_string : string -> bignat -val to_string : bignat -> string - -val is_nonzero : bignat -> bool -val zero : bignat -val one : bignat -val is_one : bignat -> bool -val div2_with_rest : bignat -> bignat * bool (* true=odd; false=even *) - -val add_1 : bignat -> bignat -val sub_1 : bignat -> bignat (* Remark: [sub_1 0]=0 *) -val mult_2 : bignat -> bignat - -val less_than : bignat -> bignat -> bool - -type bigint = POS of bignat | NEG of bignat - -val bigint_to_string : bigint -> string -val pr_bigint : bigint -> std_ppcmds diff --git a/lib/bstack.ml b/lib/bstack.ml index d4b995fb..b86dccf9 100644 --- a/lib/bstack.ml +++ b/lib/bstack.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: bstack.ml,v 1.3.2.1 2004/07/16 19:30:29 herbelin Exp $ *) +(* $Id: bstack.ml 5920 2004-07-16 20:01:26Z herbelin $ *) (* Queues of a given length *) diff --git a/lib/bstack.mli b/lib/bstack.mli index 617f7df1..f018d155 100644 --- a/lib/bstack.mli +++ b/lib/bstack.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: bstack.mli,v 1.4.2.1 2004/07/16 19:30:29 herbelin Exp $ i*) +(*i $Id: bstack.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) (* Bounded stacks. If the depth is [None], then there is no depth limit. *) @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: dyn.ml,v 1.3.16.1 2004/07/16 19:30:29 herbelin Exp $ *) +(* $Id: dyn.ml 5920 2004-07-16 20:01:26Z herbelin $ *) open Util diff --git a/lib/dyn.mli b/lib/dyn.mli index 7f46c7e6..86a1560a 100644 --- a/lib/dyn.mli +++ b/lib/dyn.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: dyn.mli,v 1.3.16.1 2004/07/16 19:30:29 herbelin Exp $ i*) +(*i $Id: dyn.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) (* Dynamics. Use with extreme care. Not for kids. *) diff --git a/lib/edit.ml b/lib/edit.ml index 5020ef5c..03420992 100644 --- a/lib/edit.ml +++ b/lib/edit.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: edit.ml,v 1.8.2.1 2004/07/16 19:30:29 herbelin Exp $ *) +(* $Id: edit.ml 6947 2005-04-20 16:18:41Z coq $ *) open Pp open Util @@ -84,6 +84,28 @@ let undo e n = errorlabstrm "Edit.undo" (str"Undo stack exhausted"); repeat n Bstack.pop bs +(* Return the depth of the focused proof of [e] stack, this is used to + put informations in coq prompt (in emacs mode). *) +let depth e = + match e.focus with + | None -> invalid_arg "Edit.depth" + | Some d -> + let (bs,_) = Hashtbl.find e.buf d in + Bstack.depth bs + +(* Undo focused proof of [e] to reach depth [n] *) +let undo_todepth e n = + match e.focus with + | None -> + if n <> 0 + then errorlabstrm "Edit.undo_todepth" (str"No proof in progress") + else () (* if there is no proof in progress, then n must be zero *) + | Some d -> + let (bs,_) = Hashtbl.find e.buf d in + if Bstack.depth bs < n then + errorlabstrm "Edit.undo_todepth" (str"Undo stack would be exhausted"); + repeat (Bstack.depth bs - n) Bstack.pop bs + let create e (d,b,c,udepth) = if Hashtbl.mem e.buf d then errorlabstrm "Edit.create" diff --git a/lib/edit.mli b/lib/edit.mli index edf0f67b..ab82c1f9 100644 --- a/lib/edit.mli +++ b/lib/edit.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: edit.mli,v 1.5.2.1 2004/07/16 19:30:29 herbelin Exp $ i*) +(*i $Id: edit.mli 6947 2005-04-20 16:18:41Z coq $ i*) (* The type of editors. * An editor is a finite map, ['a -> 'b], which knows how to apply @@ -54,3 +54,10 @@ val delete : ('a,'b,'c) t -> 'a -> unit val dom : ('a,'b,'c) t -> 'a list val clear : ('a,'b,'c) t -> unit + +(* [depth e] Returns the depth of the focused proof stack of [e], this + is used to put informations in coq prompt (in emacs mode). *) +val depth : ('a,'b,'c) t -> int + +(* [undo_todepth e n] Undoes focused proof of [e] to reach depth [n] *) +val undo_todepth : ('a,'b,'c) t -> int -> unit diff --git a/lib/explore.ml b/lib/explore.ml index 2eaabef8..7e6de0c4 100644 --- a/lib/explore.ml +++ b/lib/explore.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: explore.ml,v 1.3.16.1 2004/07/16 19:30:29 herbelin Exp $ i*) +(*i $Id: explore.ml 6066 2004-09-06 22:54:50Z barras $ i*) open Format @@ -37,6 +37,7 @@ module Make = functor(S : SearchProblem) -> struct if S.success s then s else depth_first_many (S.branching s) and depth_first_many = function | [] -> raise Not_found + | [s] -> depth_first s | s :: l -> try depth_first s with Not_found -> depth_first_many l let debug_depth_first s = @@ -44,8 +45,8 @@ module Make = functor(S : SearchProblem) -> struct pp_position p; S.pp s; if S.success s then s else explore_many 1 p (S.branching s) and explore_many i p = function - | [] -> - raise Not_found + | [] -> raise Not_found + | [s] -> explore (i::p) s | s :: l -> try explore (i::p) s with Not_found -> explore_many (succ i) p l in @@ -67,10 +68,8 @@ module Make = functor(S : SearchProblem) -> struct let breadth_first s = let rec explore q = - try - let (s, q') = pop q in enqueue q' (S.branching s) - with Empty -> - raise Not_found + let (s, q') = try pop q with Empty -> raise Not_found in + enqueue q' (S.branching s) and enqueue q = function | [] -> explore q | s :: l -> if S.success s then s else enqueue (push s q) l @@ -79,11 +78,8 @@ module Make = functor(S : SearchProblem) -> struct let debug_breadth_first s = let rec explore q = - try - let ((p,s), q') = pop q in - enqueue 1 p q' (S.branching s) - with Empty -> - raise Not_found + let ((p,s), q') = try pop q with Empty -> raise Not_found in + enqueue 1 p q' (S.branching s) and enqueue i p q = function | [] -> explore q diff --git a/lib/explore.mli b/lib/explore.mli index 1236f06b..07f95e8a 100644 --- a/lib/explore.mli +++ b/lib/explore.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: explore.mli,v 1.2.16.1 2004/07/16 19:30:29 herbelin Exp $ i*) +(*i $Id: explore.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) (*s Search strategies. *) diff --git a/lib/gmap.ml b/lib/gmap.ml index e5d41034..884305d9 100644 --- a/lib/gmap.ml +++ b/lib/gmap.ml @@ -5,10 +5,10 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: gmap.ml,v 1.3.16.1 2004/07/16 19:30:29 herbelin Exp $ *) +(* $Id: gmap.ml 7925 2006-01-24 23:20:39Z herbelin $ *) (* Maps using the generic comparison function of ocaml. Code borrowed from - the ocaml standard library. *) + the ocaml standard library (Copyright 1996, INRIA). *) type ('a,'b) t = Empty @@ -57,7 +57,7 @@ let rec add x data = function Empty -> Node(Empty, x, data, Empty, 1) - | Node(l, v, d, r, h) as t -> + | Node(l, v, d, r, h) -> let c = Pervasives.compare x v in if c = 0 then Node(l, x, data, r, h) @@ -81,17 +81,28 @@ let c = Pervasives.compare x v in c = 0 || mem x (if c < 0 then l else r) - let rec merge t1 t2 = + let rec min_binding = function + Empty -> raise Not_found + | Node(Empty, x, d, r, _) -> (x, d) + | Node(l, x, d, r, _) -> min_binding l + + let rec remove_min_binding = function + Empty -> invalid_arg "Map.remove_min_elt" + | Node(Empty, x, d, r, _) -> r + | Node(l, x, d, r, _) -> bal (remove_min_binding l) x d r + + let merge t1 t2 = match (t1, t2) with (Empty, t) -> t | (t, Empty) -> t - | (Node(l1, v1, d1, r1, h1), Node(l2, v2, d2, r2, h2)) -> - bal l1 v1 d1 (bal (merge r1 l2) v2 d2 r2) + | (_, _) -> + let (x, d) = min_binding t2 in + bal t1 x d (remove_min_binding t2) let rec remove x = function Empty -> Empty - | Node(l, v, d, r, h) as t -> + | Node(l, v, d, r, h) -> let c = Pervasives.compare x v in if c = 0 then merge l r @@ -109,6 +120,9 @@ Empty -> Empty | Node(l, v, d, r, h) -> Node(map f l, v, f d, map f r, h) + (* Maintien de fold_right par compatibilité (changé en fold_left dans + ocaml-3.09.0) *) + let rec fold f m accu = match m with Empty -> accu diff --git a/lib/gmap.mli b/lib/gmap.mli index 7415a395..79958fab 100644 --- a/lib/gmap.mli +++ b/lib/gmap.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: gmap.mli,v 1.4.16.1 2004/07/16 19:30:29 herbelin Exp $ i*) +(*i $Id: gmap.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) (* Maps using the generic comparison function of ocaml. Same interface as the module [Map] from the ocaml standard library. *) diff --git a/lib/gmapl.ml b/lib/gmapl.ml index 5eb4e110..0974909d 100644 --- a/lib/gmapl.ml +++ b/lib/gmapl.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: gmapl.ml,v 1.2.16.2 2006/01/03 20:31:16 herbelin Exp $ *) +(* $Id: gmapl.ml 7780 2006-01-03 20:33:53Z herbelin $ *) open Util diff --git a/lib/gmapl.mli b/lib/gmapl.mli index f8855ae4..db8f4358 100644 --- a/lib/gmapl.mli +++ b/lib/gmapl.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: gmapl.mli,v 1.4.16.1 2004/07/16 19:30:30 herbelin Exp $ i*) +(*i $Id: gmapl.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) (* Maps from ['a] to lists of ['b]. *) diff --git a/lib/gset.ml b/lib/gset.ml index 5ea2f82b..e90386a0 100644 --- a/lib/gset.ml +++ b/lib/gset.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: gset.ml,v 1.2.16.1 2004/07/16 19:30:30 herbelin Exp $ *) +(* $Id: gset.ml 5920 2004-07-16 20:01:26Z herbelin $ *) (* Sets using the generic comparison function of ocaml. Code borrowed from the ocaml standard library. *) diff --git a/lib/gset.mli b/lib/gset.mli index 32d798cc..0f14368f 100644 --- a/lib/gset.mli +++ b/lib/gset.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: gset.mli,v 1.3.16.1 2004/07/16 19:30:30 herbelin Exp $ i*) +(*i $Id: gset.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) (* Sets using the generic comparison function of ocaml. Same interface as the module [Set] from the ocaml standard library. *) diff --git a/lib/hashcons.ml b/lib/hashcons.ml index 5f083459..50be0ec4 100644 --- a/lib/hashcons.ml +++ b/lib/hashcons.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: hashcons.ml,v 1.3.16.1 2004/07/16 19:30:30 herbelin Exp $ *) +(* $Id: hashcons.ml 5920 2004-07-16 20:01:26Z herbelin $ *) (* Hash consing of datastructures *) diff --git a/lib/hashcons.mli b/lib/hashcons.mli index 2e32323a..f1e55ba1 100644 --- a/lib/hashcons.mli +++ b/lib/hashcons.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: hashcons.mli,v 1.5.16.1 2004/07/16 19:30:30 herbelin Exp $ i*) +(*i $Id: hashcons.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) (* Generic hash-consing. *) diff --git a/lib/heap.ml b/lib/heap.ml index f0db2943..92aa0070 100644 --- a/lib/heap.ml +++ b/lib/heap.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: heap.ml,v 1.1.2.1 2004/07/16 19:30:30 herbelin Exp $ *) +(* $Id: heap.ml 5920 2004-07-16 20:01:26Z herbelin $ *) (*s Heaps *) diff --git a/lib/heap.mli b/lib/heap.mli index 46e72728..d351edd0 100644 --- a/lib/heap.mli +++ b/lib/heap.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: heap.mli,v 1.1.2.2 2005/01/21 17:14:11 herbelin Exp $ i*) +(*i $Id: heap.mli 6621 2005-01-21 17:24:37Z herbelin $ i*) (* Heaps *) diff --git a/lib/options.ml b/lib/options.ml index b5c5efda..c46857e3 100644 --- a/lib/options.ml +++ b/lib/options.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: options.ml,v 1.27.2.1 2004/07/16 19:30:30 herbelin Exp $ *) +(* $Id: options.ml 9191 2006-09-29 15:45:42Z courtieu $ *) open Util @@ -22,8 +22,7 @@ let batch_mode = ref false let debug = ref false let print_emacs = ref false - -let emacs_str s = if !print_emacs then s else "" +let print_emacs_safechar = ref false let term_quality = ref false @@ -33,22 +32,11 @@ let dont_load_proofs = ref false let raw_print = ref false -let v7 = - let transl = array_exists ((=) "-translate") Sys.argv in - let v7 = array_exists ((=) "-v7") Sys.argv in - let v8 = array_exists ((=) "-v8") Sys.argv in - if v8 & transl then error "Options -translate and -v8 are incompatible"; - if v8 & v7 then error "Options -v7 and -v8 are incompatible"; - ref (v7 or transl) - -let v7_only = ref false - (* Translate *) let translate = ref false -let make_translate f = translate := f; v7 := f; () +let make_translate f = translate := f let do_translate () = !translate let translate_file = ref false -let translate_strict_impargs = ref true (* True only when interning from pp*new.ml *) let translate_syntax = ref false @@ -73,6 +61,8 @@ let silently f x = 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 + (* The number of printed hypothesis in a goal *) let print_hyps_limit = ref (None : int option) @@ -81,11 +71,11 @@ 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 @@ -105,3 +95,30 @@ let dump_it () = 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 "netscape -remote \"OpenURL(", ")\"" diff --git a/lib/options.mli b/lib/options.mli index 731b7da4..30d585fb 100644 --- a/lib/options.mli +++ b/lib/options.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: options.mli,v 1.25.2.1 2004/07/16 19:30:30 herbelin Exp $ i*) +(*i $Id: options.mli 9191 2006-09-29 15:45:42Z courtieu $ i*) (* Global options of the system. *) @@ -17,7 +17,7 @@ val batch_mode : bool ref val debug : bool ref val print_emacs : bool ref -val emacs_str : string -> string +val print_emacs_safechar : bool ref val term_quality : bool ref @@ -27,15 +27,11 @@ val dont_load_proofs : bool ref val raw_print : bool ref -val v7 : bool ref -val v7_only : 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 translate_strict_impargs : bool ref val make_silent : bool -> unit val is_silent : unit -> bool @@ -44,6 +40,8 @@ val silently : ('a -> 'b) -> 'a -> 'b val if_silent : ('a -> unit) -> 'a -> unit val if_verbose : ('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 @@ -60,3 +58,14 @@ 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 + @@ -6,10 +6,18 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pp.ml4,v 1.5.2.1 2004/07/16 19:30:30 herbelin Exp $ *) +(* $Id: pp.ml4 8747 2006-04-27 16:00:49Z courtieu $ *) open Pp_control +(* This should not be used outside of this file. Use + Options.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] *) +let print_emacs = ref false +let make_pp_emacs() = print_emacs:=true + (* The different kinds of blocks are: \begin{description} \item[hbox:] Horizontal block no line breaking; @@ -122,17 +130,17 @@ let int n = str (string_of_int n) let real r = str (string_of_float r) let bool b = str (string_of_bool b) +(* In new syntax only double quote char is escaped by repeating it *) let rec escape_string s = let rec escape_at s i = if i<0 then s - else if s.[i] == '\\' || s.[i] == '"' then - let s' = String.sub s 0 i^"\\"^String.sub s i (String.length s - i) in + else if s.[i] == '"' then + let s' = String.sub s 0 i^"\""^String.sub s i (String.length s - i) in escape_at s' (i-1) else escape_at s (i-1) in escape_at s (String.length s - 1) - -let qstring s = str ("\""^(escape_string s)^"\"") +let qstring s = str ("\""^escape_string s^"\"") let qs = qstring (* boxing commands *) @@ -183,7 +191,6 @@ let rec pr_com ft s = (* pretty printing functions *) let pp_dirs ft = - let maxbox = (get_gp ft).max_depth in let pp_open_box = function | Pp_hbox n -> Format.pp_open_hbox ft () | Pp_vbox n -> Format.pp_open_vbox ft n @@ -239,6 +246,17 @@ let pp_err_dirs = pp_dirs err_ft let ppcmds x = Ppdir_ppcmds x +(* Special chars for emacs, to detect warnings inside goal output *) +let emacs_warning_start_string = String.make 1 (Char.chr 254) +let emacs_warning_end_string = String.make 1 (Char.chr 255) + +let warnstart() = + if not !print_emacs then str "" else str emacs_warning_start_string + +let warnend() = + if not !print_emacs then str "" else str emacs_warning_end_string + + (* pretty printing functions WITHOUT FLUSH *) let pp_with ft strm = pp_dirs ft [< 'Ppdir_ppcmds strm >] @@ -247,10 +265,10 @@ let ppnl_with ft strm = pp_dirs ft [< 'Ppdir_ppcmds [< strm ; 'Ppcmd_force_newline >] >] let warning_with ft string = - ppnl_with ft [< str "Warning: " ; str string >] + ppnl_with ft [< warnstart() ; str "Warning: " ; str string ; warnend() >] let warn_with ft pps = - ppnl_with ft [< str "Warning: " ; pps >] + ppnl_with ft [< warnstart() ; str "Warning: " ; pps ; warnend() >] let pp_flush_with ft = Format.pp_print_flush ft @@ -264,7 +282,7 @@ let msgnl_with ft strm = pp_dirs ft [< 'Ppdir_ppcmds strm ; 'Ppdir_print_newline >] let msg_warning_with ft strm= - pp_dirs ft [< 'Ppdir_ppcmds [< str "Warning: "; strm>]; + pp_dirs ft [< 'Ppdir_ppcmds [< warnstart() ; str "Warning: "; strm ; warnend() >]; 'Ppdir_print_newline >] @@ -6,12 +6,17 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pp.mli,v 1.8.2.1 2004/07/16 19:30:30 herbelin Exp $ i*) +(*i $Id: pp.mli 8748 2006-04-27 16:01:26Z courtieu $ i*) (*i*) open Pp_control (*i*) +(* Modify pretty printing functions behavior for emacs ouput (special + chars inserted at some places). This function should called once in + module [Options], that's all. *) +val make_pp_emacs:unit -> unit + (* Pretty-printers. *) type ppcmd diff --git a/lib/pp_control.ml b/lib/pp_control.ml index 85303f74..7632d736 100644 --- a/lib/pp_control.ml +++ b/lib/pp_control.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pp_control.ml,v 1.8.2.1 2004/07/16 19:30:31 herbelin Exp $ *) +(* $Id: pp_control.ml 5920 2004-07-16 20:01:26Z herbelin $ *) (* Parameters of pretty-printing *) diff --git a/lib/pp_control.mli b/lib/pp_control.mli index 3588847d..7e25e561 100644 --- a/lib/pp_control.mli +++ b/lib/pp_control.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pp_control.mli,v 1.7.2.1 2004/07/16 19:30:31 herbelin Exp $ i*) +(*i $Id: pp_control.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) (* Parameters of pretty-printing. *) diff --git a/lib/predicate.ml b/lib/predicate.ml index 1eaa20ce..93b74463 100644 --- a/lib/predicate.ml +++ b/lib/predicate.ml @@ -10,7 +10,7 @@ (* *) (************************************************************************) -(* $Id: predicate.ml,v 1.1.14.1 2004/07/16 19:30:31 herbelin Exp $ *) +(* $Id: predicate.ml 5920 2004-07-16 20:01:26Z herbelin $ *) (* Sets over ordered types *) diff --git a/lib/predicate.mli b/lib/predicate.mli index 2dc7d85c..85596fea 100644 --- a/lib/predicate.mli +++ b/lib/predicate.mli @@ -1,5 +1,5 @@ -(*i $Id: predicate.mli,v 1.1.14.1 2005/01/21 17:14:11 herbelin Exp $ i*) +(*i $Id: predicate.mli 6621 2005-01-21 17:24:37Z herbelin $ i*) (* Module [Pred]: sets over infinite ordered types with complement. *) diff --git a/lib/profile.ml b/lib/profile.ml index f55388f8..dd7e977e 100644 --- a/lib/profile.ml +++ b/lib/profile.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: profile.ml,v 1.13.16.1 2004/07/16 19:30:31 herbelin Exp $ *) +(* $Id: profile.ml 7538 2005-11-08 17:14:52Z herbelin $ *) open Gc @@ -259,9 +259,9 @@ let time_overhead_B_C () = for i=1 to loops do try dummy_last_alloc := get_alloc (); - let r = dummy_f dummy_x in - let dw = dummy_spent_alloc () in - let dt = get_time () in + let _r = dummy_f dummy_x in + let _dw = dummy_spent_alloc () in + let _dt = get_time () in () with _ -> assert false done; @@ -328,7 +328,7 @@ let close_profile print = outside.owntime <- outside.owntime + t; ajoute_ownalloc outside dw; ajoute_totalloc outside dw; - if List.length !prof_table <> 0 then begin + if !prof_table <> [] then begin let ov_bc = time_overhead_B_C () (* B+C overhead *) in let ov_ad = time_overhead_A_D () (* A+D overhead *) in let adjust (n,e) = (n, adjust_time ov_bc ov_ad e) in diff --git a/lib/profile.mli b/lib/profile.mli index e8ce8994..0937e9e3 100644 --- a/lib/profile.mli +++ b/lib/profile.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: profile.mli,v 1.7.16.2 2005/01/21 17:14:11 herbelin Exp $ i*) +(*i $Id: profile.mli 6621 2005-01-21 17:24:37Z herbelin $ i*) (*s This program is a small time and allocation profiler for Objective Caml *) diff --git a/lib/rtree.ml b/lib/rtree.ml index 53cc372f..ab689be1 100644 --- a/lib/rtree.ml +++ b/lib/rtree.ml @@ -6,16 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: rtree.ml,v 1.2.8.1 2004/07/16 19:30:31 herbelin Exp $ i*) +(*i $Id: rtree.ml 8648 2006-03-18 15:37:14Z herbelin $ i*) (* Type of regular trees: - Param denotes tree variables (like de Bruijn indices) - - Node denotes the usual tree node, labelles with 'a + - Node denotes the usual tree node, labelled with 'a - Rec(j,v1..vn) introduces infinite tree. It denotes v(j+1) with parameters 0..n-1 replaced by Rec(0,v1..vn)..Rec(n-1,v1..vn) respectively. - Parameters n and higher denote parameters globals to the + Parameters n and higher denote parameters global to the current Rec node (as usual in de Bruijn binding system) *) type 'a t = diff --git a/lib/rtree.mli b/lib/rtree.mli index 79b57586..7be96652 100644 --- a/lib/rtree.mli +++ b/lib/rtree.mli @@ -6,10 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: rtree.mli,v 1.2.8.2 2005/01/21 16:41:52 herbelin Exp $ i*) +(*i $Id: rtree.mli 7493 2005-11-02 22:12:16Z mohring $ i*) (* Type of regular tree with nodes labelled by values of type 'a *) -type 'a t + +type 'a t (* Building trees *) (* build a recursive call *) diff --git a/lib/stamps.ml b/lib/stamps.ml deleted file mode 100644 index 1697c309..00000000 --- a/lib/stamps.ml +++ /dev/null @@ -1,28 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id: stamps.ml,v 1.2.16.1 2004/07/16 19:30:31 herbelin Exp $ *) - -let new_stamp = - let stamp_ctr = ref 0 in - fun () -> incr stamp_ctr; !stamp_ctr - -type 'a timestamped = { stamp : int; ed : 'a } - -let ts_stamp st = st.stamp -let ts_mod f st = { stamp = new_stamp(); ed = f st.ed } -let ts_it st = st.ed -let ts_mk v = { stamp = new_stamp(); ed = v} -let ts_eq st1 st2 = st1.stamp = st2.stamp - -type 'a idstamped = 'a timestamped - -let ids_mod f st = { stamp = st.stamp; ed = f st.ed} -let ids_it = ts_it -let ids_mk = ts_mk -let ids_eq = ts_eq diff --git a/lib/stamps.mli b/lib/stamps.mli deleted file mode 100644 index 36f238b9..00000000 --- a/lib/stamps.mli +++ /dev/null @@ -1,28 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: stamps.mli,v 1.3.16.1 2004/07/16 19:30:31 herbelin Exp $ i*) - -(* Time stamps. *) - -type 'a timestamped - -(* [ts_mod] gives a ['b timestamped] with a new stamp *) -val ts_mod : ('a -> 'b) -> 'a timestamped -> 'b timestamped -val ts_it : 'a timestamped -> 'a -val ts_mk : 'a -> 'a timestamped -val ts_eq : 'a timestamped -> 'a timestamped -> bool -val ts_stamp : 'a timestamped -> int - -type 'a idstamped - -(* [ids_mod] gives a ['b stamped] with the same stamp *) -val ids_mod : ('a -> 'b) -> 'a idstamped -> 'b idstamped -val ids_it : 'a idstamped -> 'a -val ids_mk : 'a -> 'a idstamped -val ids_eq : 'a idstamped -> 'a idstamped -> bool diff --git a/lib/system.ml b/lib/system.ml index 9bbcc308..c92e87f1 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: system.ml,v 1.31.8.3 2006/01/10 17:06:23 barras Exp $ *) +(* $Id: system.ml 9397 2006-11-21 21:50:54Z herbelin $ *) open Pp open Util @@ -34,7 +34,7 @@ let rec expand_atom s i = then expand_atom s (i+1) else i -let rec expand_macros b s i = +let rec expand_macros s i = let l = String.length s in if i=l then s else match s.[i] with @@ -42,53 +42,26 @@ let rec expand_macros b s i = let n = expand_atom s (i+1) in let v = safe_getenv (String.sub s (i+1) (n-i-1)) in let s = (String.sub s 0 i)^v^(String.sub s n (l-n)) in - expand_macros false s (i + String.length v) - | '/' -> - expand_macros true s (i+1) - | '~' -> + expand_macros s (i + String.length v) + | '~' when i = 0 -> let n = expand_atom s (i+1) in let v = if n=i+1 then home else (getpwnam (String.sub s (i+1) (n-i-1))).pw_dir in let s = v^(String.sub s n (l-n)) in - expand_macros false s (String.length v) - | c -> expand_macros false s (i+1) + expand_macros s (String.length v) + | c -> expand_macros s (i+1) -let glob s = expand_macros true s 0 +let expand_path_macros s = expand_macros s 0 (* Files and load path. *) type physical_path = string type load_path = physical_path list -(* 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 +let physical_path_of_string s = s +let string_of_physical_path p = p (* All subdirectories, recursively *) @@ -124,51 +97,44 @@ let all_subdirs ~unix_path:root = end ; List.rev !l -let search_in_path path filename = +let where_in_path path filename = let rec search = function | lpe :: rem -> - let f = glob (Filename.concat lpe filename) in + let f = Filename.concat lpe filename in if Sys.file_exists f then (lpe,f) else search rem | [] -> raise Not_found in search path -let where_in_path = search_in_path - -let find_file_in_path paths name = - let globname = glob name in - if not (Filename.is_implicit globname) then - let root = Filename.dirname globname in - root, globname +let find_file_in_path paths filename = + if not (Filename.is_implicit filename) then + let root = Filename.dirname filename in + root, filename else - try - search_in_path paths name + try where_in_path paths filename with Not_found -> errorlabstrm "System.find_file_in_path" - (hov 0 (str "Can't find file" ++ spc () ++ str name ++ spc () ++ + (hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++ str "on loadpath")) let is_in_path lpath filename = - try - let _ = search_in_path lpath filename in true - with - Not_found -> false + try ignore (where_in_path lpath filename); true + with Not_found -> false let make_suffix name suffix = if Filename.check_suffix name suffix then name else (name ^ suffix) -let file_readable_p na = - try access (glob na) [R_OK];true with Unix_error (_, _, _) -> false +let file_readable_p name = + try access name [R_OK];true with Unix_error (_, _, _) -> false -let open_trapping_failure open_fun name suffix = - let rname = glob (make_suffix name suffix) in - try open_fun rname with _ -> error ("Can't open " ^ rname) +let open_trapping_failure name = + try open_out_bin name with _ -> error ("Can't open " ^ name) -let try_remove f = - try Sys.remove f +let try_remove filename = + try Sys.remove filename with _ -> msgnl (str"Warning: " ++ str"Could not remove file " ++ - str f ++ str" which is corrupted!" ) + str filename ++ str" which is corrupted!" ) let marshal_out ch v = Marshal.to_channel ch v [] let marshal_in ch = @@ -179,14 +145,14 @@ exception Bad_magic_number of string let raw_extern_intern magic suffix = let extern_state name = - let (_,channel) as filec = - open_trapping_failure (fun n -> n,open_out_bin n) name suffix in + let filename = make_suffix name suffix in + let channel = open_trapping_failure filename in output_binary_int channel magic; - filec - and intern_state fname = - let channel = open_in_bin fname in + filename,channel + and intern_state filename = + let channel = open_in_bin filename in if input_binary_int channel <> magic then - raise (Bad_magic_number fname); + raise (Bad_magic_number filename); channel in (extern_state,intern_state) @@ -195,17 +161,17 @@ let extern_intern magic suffix = let (raw_extern,raw_intern) = raw_extern_intern magic suffix in let extern_state name val_0 = try - let (fname,channel) = raw_extern name in + let (filename,channel) = raw_extern name in try marshal_out channel val_0; close_out channel with e -> - begin try_remove fname; raise e end + begin try_remove filename; raise e end with Sys_error s -> error ("System error: " ^ s) and intern_state paths name = try - let _,fname = find_file_in_path paths (make_suffix name suffix) in - let channel = raw_intern fname in + let _,filename = find_file_in_path paths (make_suffix name suffix) in + let channel = raw_intern filename in let v = marshal_in channel in close_in channel; v @@ -214,6 +180,61 @@ let extern_intern magic suffix = in (extern_state,intern_state) +(* Communication through files with another executable *) + +let connect writefun readfun com = + let name = Filename.basename com in + let tmp_to = Filename.temp_file ("coq-"^name^"-in") ".xml" in + let tmp_from = Filename.temp_file ("coq-"^name^"-out") ".xml" in + let ch_to_in,ch_to_out = + try open_in tmp_to, open_out tmp_to + with Sys_error s -> error ("Cannot set connection to "^com^"("^s^")") in + let ch_from_in,ch_from_out = + try open_in tmp_from, open_out tmp_from + with Sys_error s -> + close_out ch_to_out; close_in ch_to_in; + error ("Cannot set connection from "^com^"("^s^")") in + writefun ch_to_out; + close_out ch_to_out; + let pid = + let ch_to' = Unix.descr_of_in_channel ch_to_in in + let ch_from' = Unix.descr_of_out_channel ch_from_out in + try Unix.create_process com [||] ch_to' ch_from' Unix.stdout + with Unix.Unix_error (err,_,_) -> + close_in ch_to_in; close_in ch_from_in; close_out ch_from_out; + unlink tmp_from; unlink tmp_to; + error ("Cannot execute "^com^"("^(Unix.error_message err)^")") in + close_in ch_to_in; + close_out ch_from_out; + (match snd (Unix.waitpid [] pid) with + | Unix.WEXITED 127 -> error (com^": cannot execute") + | Unix.WEXITED 0 -> () + | _ -> error (com^" exited abnormally")); + let a = readfun ch_from_in in + close_in ch_from_in; + unlink tmp_from; + unlink tmp_to; + a + +let run_command converter f c = + let result = Buffer.create 127 in + let cin,cout,cerr = Unix.open_process_full c (Unix.environment ()) in + let buff = String.make 127 ' ' in + let buffe = String.make 127 ' ' in + let n = ref 0 in + let ne = ref 0 in + + while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ; + !n+ !ne <> 0 + do + let r = converter (String.sub buff 0 !n) in + f r; + Buffer.add_string result r; + let r = converter (String.sub buffe 0 !ne) in + f r; + Buffer.add_string result r + done; + (Unix.close_process_full (cin,cout,cerr), Buffer.contents result) (* Time stamps. *) diff --git a/lib/system.mli b/lib/system.mli index dc172b70..a58308a8 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,v 1.17.16.3 2006/01/10 17:06:23 barras Exp $ i*) +(*i $Id: system.mli 9397 2006-11-21 21:50:54Z 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,16 +16,17 @@ type physical_path = string type load_path = physical_path list -val canonical_path_name : string -> physical_path - val all_subdirs : unix_path:string -> (physical_path * string list) list val is_in_path : load_path -> string -> bool val where_in_path : load_path -> string -> physical_path * string +val physical_path_of_string : string -> physical_path +val string_of_physical_path : physical_path -> string + val make_suffix : string -> string -> string val file_readable_p : string -> bool -val glob : string -> string +val expand_path_macros : string -> string val getenv_else : string -> string -> string val home : string @@ -48,6 +49,18 @@ val raw_extern_intern : int -> string -> val extern_intern : int -> string -> (string -> 'a -> unit) * (load_path -> string -> 'a) +(*s Sending/receiving once with external executable *) + +val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a + +(*s [run_command converter f com] launches command [com], and returns + the contents of stdout and stderr that have been processed with + [converter]; the processed contents of stdout and stderr is also + passed to [f] *) + +val run_command : (string -> string) -> (string -> unit) -> string -> + Unix.process_status * string + (*s Time stamps. *) type time @@ -56,5 +69,3 @@ val process_time : unit -> float * float val get_time : unit -> time val time_difference : time -> time -> float (* in seconds *) val fmt_time_difference : time -> time -> Pp.std_ppcmds - - @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tlm.ml,v 1.3.16.1 2004/07/16 19:30:31 herbelin Exp $ *) +(* $Id: tlm.ml 5920 2004-07-16 20:01:26Z herbelin $ *) type ('a,'b) t = Node of 'b Gset.t * ('a, ('a,'b) t) Gmap.t diff --git a/lib/tlm.mli b/lib/tlm.mli index a3011932..982bb5ed 100644 --- a/lib/tlm.mli +++ b/lib/tlm.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tlm.mli,v 1.5.16.1 2004/07/16 19:30:31 herbelin Exp $ i*) +(*i $Id: tlm.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) (* Tries. This module implements a data structure [('a,'b) t] mapping lists of values of type ['a] to sets (as lists) of values of type ['b]. *) diff --git a/lib/util.ml b/lib/util.ml index b5470e58..89cfd6fc 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -1,12 +1,12 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) -(* $Id: util.ml,v 1.84.2.3 2004/07/29 15:00:04 herbelin Exp $ *) +(* $Id: util.ml 9225 2006-10-09 15:59:23Z herbelin $ *) open Pp @@ -32,8 +32,9 @@ type 'a located = loc * 'a let anomaly_loc (loc,s,strm) = Stdpp.raise_with_loc loc (Anomaly (s,strm)) let user_err_loc (loc,s,strm) = Stdpp.raise_with_loc loc (UserError (s,strm)) let invalid_arg_loc (loc,s) = Stdpp.raise_with_loc loc (Invalid_argument s) -let join_loc (deb1,_ as loc1) (_,fin2 as loc2) = - if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc else (deb1,fin2) +let join_loc loc1 loc2 = + if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc + else (fst loc1, snd loc2) (* Like Exc_located, but specifies the outermost file read, the filename associated to the location of the error, and the error itself. *) @@ -98,6 +99,8 @@ let string_string_contains ~where ~what = with Not_found -> false +let plural n s = if n>1 then s^"s" else s + (* string parsing *) let parse_loadpath s = @@ -118,10 +121,6 @@ module Stringset = Set.Make(struct type t = string let compare = compare end) module Stringmap = Map.Make(struct type t = string let compare = compare end) -let stringmap_to_list m = Stringmap.fold (fun s y l -> (s,y)::l) m [] - -let stringmap_dom m = Stringmap.fold (fun s _ l -> s::l) m [] - (* Lists *) let list_add_set x l = if List.mem x l then l else x::l @@ -195,7 +194,7 @@ let list_map_i f = let list_map2_i f i l1 l2 = let rec map_i i = function | ([], []) -> [] - | ((h1::t1), (h2::t2)) -> (f i h1 h2) :: (map_i (succ i) (t1,t2)) + | ((h1::t1), (h2::t2)) -> let v = f i h1 h2 in v :: map_i (succ i) (t1,t2) | (_, _) -> invalid_arg "map2_i" in map_i i (l1,l2) @@ -203,7 +202,7 @@ let list_map2_i f i l1 l2 = let list_map3 f l1 l2 l3 = let rec map = function | ([], [], []) -> [] - | ((h1::t1), (h2::t2), (h3::t3)) -> (f h1 h2 h3) :: (map (t1,t2,t3)) + | ((h1::t1), (h2::t2), (h3::t3)) -> let v = f h1 h2 h3 in v::map (t1,t2,t3) | (_, _, _) -> invalid_arg "map3" in map (l1,l2,l3) @@ -215,6 +214,16 @@ let list_index x = in index_x 1 +let list_unique_index x = + let rec index_x n = function + | y::l -> + if x = y then + if List.mem x l then raise Not_found + else n + else index_x (succ n) l + | [] -> raise Not_found + in index_x 1 + let list_fold_left_i f = let rec it_list_f i a = function | [] -> a @@ -251,6 +260,13 @@ let list_for_all_i p = let list_except x l = List.filter (fun y -> not (x = y)) l +let list_remove = list_except (* Alias *) + +let rec list_remove_first a = function + | b::l when a = b -> l + | b::l -> b::list_remove_first a l + | [] -> raise Not_found + let list_for_all2eq f l1 l2 = try List.for_all2 f l1 l2 with Failure _ -> false let list_map_i f = @@ -279,9 +295,11 @@ let list_try_find f = in try_find_f -let rec list_uniquize = function - | [] -> [] - | h::t -> if List.mem h t then list_uniquize t else h::(list_uniquize t) +let list_uniquize l = + let rec aux acc = function + | [] -> List.rev acc + | h::t -> if List.mem h acc then aux acc t else aux (h::acc) t + in aux [] l let rec list_distinct = function | h::t -> (not (List.mem h t)) && list_distinct t @@ -347,7 +365,19 @@ let list_prefix_of prefl l = | ([], _) -> true | (_, _) -> false in - prefrec (prefl,l) + prefrec (prefl,l) + +let list_drop_prefix p l = +(* if l=p++t then return t else l *) + let rec list_drop_prefix_rec = function + | ([], tl) -> Some tl + | (_, []) -> None + | (h1::tp, h2::tl) -> + if h1 = h2 then list_drop_prefix_rec (tp,tl) else None + in + match list_drop_prefix_rec (p,l) with + | Some r -> r + | None -> l let list_map_append f l = List.flatten (List.map f l) @@ -362,12 +392,12 @@ let list_share_tails l1 l2 = let list_join_map f l = List.flatten (List.map f l) -let rec list_fold_map f e = function +let rec list_fold_map f e = function | [] -> (e,[]) - | h::t -> + | h::t -> let e',h' = f e h in let e'',t' = list_fold_map f e' t in - e'',h'::t' + e'',h'::t' (* (* tail-recursive version of the above function *) let list_fold_map f e l = @@ -379,6 +409,10 @@ let list_fold_map f e l = (e',List.rev lrev) *) +(* The same, based on fold_right, with the effect accumulated on the right *) +let list_fold_map' f l e = + List.fold_right (fun x (l,e) -> let (y,e) = f x e in (y::l,e)) l ([],e) + let list_map_assoc f = List.map (fun (x,a) -> (x,f a)) (* Arrays *) @@ -441,6 +475,17 @@ let array_last v = let array_cons e v = Array.append [|e|] v +let array_rev t = + let n=Array.length t in + if n <=0 then () + else + let tmp=ref t.(0) in + for i=0 to pred (n/2) do + tmp:=t.((pred n)-i); + t.((pred n)-i)<- t.(i); + t.(i)<- !tmp + done + let array_fold_right_i f v a = let rec fold a n = if n=0 then a @@ -596,6 +641,38 @@ let array_map_left_pair f a g b = r, s end +let pure_functional = false + +let array_fold_map' f v e = +if pure_functional then + let (l,e) = + Array.fold_right + (fun x (l,e) -> let (y,e) = f x e in (y::l,e)) + v ([],e) in + (Array.of_list l,e) +else + let e' = ref e in + let v' = Array.map (fun x -> let (y,e) = f x !e' in e' := e; y) v in + (v',!e') + +let array_fold_map2' f v1 v2 e = + let e' = ref e in + let v' = + array_map2 (fun x1 x2 -> let (y,e) = f x1 x2 !e' in e' := e; y) v1 v2 + in + (v',!e') + +let array_distinct v = + 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; + true + with Exit -> + false + (* Matrices *) let matrix_transpose mat = @@ -648,7 +725,7 @@ let out_some = function | Some x -> x | None -> failwith "out_some" -let option_app f = function +let option_map f = function | None -> None | Some x -> Some (f x) @@ -660,6 +737,10 @@ let option_fold_left2 f e a b = match (a,b) with | Some x, Some y -> f e x y | _ -> e +let option_fold_left f e a = match a with + | Some x -> f e x + | _ -> e + let option_fold_right f a e = match a with | Some x -> f x e | _ -> e @@ -693,6 +774,8 @@ let pr_str = str let pr_coma () = str "," ++ spc () let pr_semicolon () = str ";" ++ spc () let pr_bar () = str "|" ++ spc () +let pr_arg pr x = spc () ++ pr x +let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x let pr_ord n = let suff = match n mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" in @@ -734,6 +817,8 @@ let prvect_with_sep sep elem v = let n = Array.length v in if n = 0 then mt () else pr (n - 1) +let surround p = hov 1 (str"(" ++ p ++ str")") + (*s Size of ocaml values. *) module Size = struct diff --git a/lib/util.mli b/lib/util.mli index 19f05ea4..b2d8f135 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -1,12 +1,12 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) -(*i $Id: util.mli,v 1.84.2.2 2004/07/16 20:43:46 herbelin Exp $ i*) +(*i $Id: util.mli 9225 2006-10-09 15:59:23Z herbelin $ i*) (*i*) open Pp @@ -68,16 +68,13 @@ val explode : string -> string list val implode : string list -> string val string_index_from : string -> int -> string -> int val string_string_contains : where:string -> what:string -> bool +val plural : int -> string -> string val parse_loadpath : string -> string list module Stringset : Set.S with type elt = string - module Stringmap : Map.S with type key = string -val stringmap_to_list : 'a Stringmap.t -> (string * 'a) list -val stringmap_dom : 'a Stringmap.t -> string list - (*s Lists. *) val list_add_set : 'a -> 'a list -> 'a list @@ -103,12 +100,16 @@ val list_map2_i : val list_map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list val list_index : 'a -> 'a list -> int +(* [list_unique_index x l] returns [Not_found] if [x] doesn't occur exactly once *) +val list_unique_index : 'a -> 'a list -> int val list_iter_i : (int -> 'a -> unit) -> 'a list -> unit val list_fold_left_i : (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a val list_fold_right_and_left : ('a -> 'b -> 'b list -> 'a) -> 'b list -> 'a -> 'a 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_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 @@ -122,6 +123,7 @@ val list_last : 'a list -> 'a val list_lastn : int -> 'a list -> 'a list val list_skipn : int -> 'a list -> 'a list val list_prefix_of : 'a list -> 'a list -> bool +val list_drop_prefix : 'a list -> '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 (* raises [Invalid_argument] if the two lists don't have the same length *) @@ -130,8 +132,8 @@ val list_share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list val list_join_map : ('a -> 'b list) -> 'a list -> 'b list (* [list_fold_map f e_0 [l_1...l_n] = e_n,[k_1...k_n]] where [(e_i,k_i)=f e_{i-1} l_i] *) -val list_fold_map : - ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list +val list_fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list +val list_fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a val list_map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list (*s Arrays. *) @@ -147,6 +149,7 @@ val array_hd : 'a array -> 'a val array_tl : 'a array -> 'a array val array_last : 'a array -> 'a val array_cons : 'a -> 'a array -> 'a array +val array_rev : 'a array -> unit val array_fold_right_i : (int -> 'b -> 'a -> 'a) -> 'b array -> 'a -> 'a val array_fold_left_i : (int -> 'a -> 'b -> 'a) -> 'a -> 'b array -> 'a @@ -170,6 +173,10 @@ val array_map3 : val array_map_left : ('a -> 'b) -> 'a array -> 'b array val array_map_left_pair : ('a -> 'b) -> 'a array -> ('c -> 'd) -> 'c array -> 'b array * 'd array +val array_fold_map' : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c +val array_fold_map2' : + ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c +val array_distinct : 'a array -> bool (*s Matrices *) @@ -199,9 +206,10 @@ val interval : int -> int -> int list val in_some : 'a -> 'a option val out_some : 'a option -> 'a -val option_app : ('a -> 'b) -> 'a option -> 'b option +val option_map : ('a -> 'b) -> 'a option -> 'b option val option_cons : 'a option -> 'a list -> 'a list val option_fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b +val option_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b option -> 'a val option_fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option -> 'c option -> 'a val option_iter : ('a -> unit) -> 'a option -> unit @@ -223,6 +231,8 @@ val pr_coma : unit -> std_ppcmds val pr_semicolon : unit -> std_ppcmds val pr_bar : unit -> std_ppcmds val pr_ord : int -> std_ppcmds +val pr_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds +val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds @@ -231,6 +241,8 @@ val prlist_with_sep : val prvect_with_sep : (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b array -> std_ppcmds val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds +val surround : std_ppcmds -> std_ppcmds + (*s Size of an ocaml value (in words, bytes and kilobytes). *) |