summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/bigint.ml392
-rw-r--r--lib/bigint.mli45
-rw-r--r--lib/bignat.ml116
-rw-r--r--lib/bignat.mli37
-rw-r--r--lib/bstack.ml2
-rw-r--r--lib/bstack.mli2
-rw-r--r--lib/dyn.ml2
-rw-r--r--lib/dyn.mli2
-rw-r--r--lib/edit.ml24
-rw-r--r--lib/edit.mli9
-rw-r--r--lib/explore.ml20
-rw-r--r--lib/explore.mli2
-rw-r--r--lib/gmap.ml28
-rw-r--r--lib/gmap.mli2
-rw-r--r--lib/gmapl.ml2
-rw-r--r--lib/gmapl.mli2
-rw-r--r--lib/gset.ml2
-rw-r--r--lib/gset.mli2
-rw-r--r--lib/hashcons.ml2
-rw-r--r--lib/hashcons.mli2
-rw-r--r--lib/heap.ml2
-rw-r--r--lib/heap.mli2
-rw-r--r--lib/options.ml46
-rw-r--r--lib/options.mli20
-rw-r--r--lib/pp.ml411
-rw-r--r--lib/pp.mli2
-rw-r--r--lib/pp_control.ml2
-rw-r--r--lib/pp_control.mli2
-rw-r--r--lib/predicate.ml2
-rw-r--r--lib/predicate.mli2
-rw-r--r--lib/profile.ml10
-rw-r--r--lib/profile.mli2
-rw-r--r--lib/rtree.ml6
-rw-r--r--lib/rtree.mli5
-rw-r--r--lib/stamps.ml2
-rw-r--r--lib/stamps.mli2
-rw-r--r--lib/system.ml97
-rw-r--r--lib/system.mli18
-rw-r--r--lib/tlm.ml2
-rw-r--r--lib/tlm.mli2
-rw-r--r--lib/util.ml60
-rw-r--r--lib/util.mli30
42 files changed, 715 insertions, 307 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. *)
diff --git a/lib/dyn.ml b/lib/dyn.ml
index 63f00365..94979835 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -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..0d934922 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 7740 2005-12-26 20:07:21Z herbelin $ *)
open Util
@@ -23,8 +23,6 @@ let debug = ref false
let print_emacs = ref false
-let emacs_str s = if !print_emacs then s else ""
-
let term_quality = ref false
let xml_export = ref false
@@ -33,22 +31,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 +60,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)
@@ -105,3 +94,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..1a5444a4 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 7740 2005-12-26 20:07:21Z herbelin $ i*)
(* Global options of the system. *)
@@ -17,7 +17,6 @@ val batch_mode : bool ref
val debug : bool ref
val print_emacs : bool ref
-val emacs_str : string -> string
val term_quality : bool ref
@@ -27,15 +26,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 +39,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 +57,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
+
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 25ab9ce8..e7ba9869 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -6,7 +6,7 @@
(* * 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 7751 2005-12-28 12:58:53Z herbelin $ *)
open Pp_control
@@ -122,17 +122,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 +183,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
diff --git a/lib/pp.mli b/lib/pp.mli
index 417ea107..88deb6d2 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -6,7 +6,7 @@
(* * 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 5920 2004-07-16 20:01:26Z herbelin $ i*)
(*i*)
open Pp_control
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
index 1697c309..0f481516 100644
--- a/lib/stamps.ml
+++ b/lib/stamps.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: stamps.ml,v 1.2.16.1 2004/07/16 19:30:31 herbelin Exp $ *)
+(* $Id: stamps.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
let new_stamp =
let stamp_ctr = ref 0 in
diff --git a/lib/stamps.mli b/lib/stamps.mli
index 36f238b9..6fa3077f 100644
--- a/lib/stamps.mli
+++ b/lib/stamps.mli
@@ -6,7 +6,7 @@
(* * 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*)
+(*i $Id: stamps.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
(* Time stamps. *)
diff --git a/lib/system.ml b/lib/system.ml
index 9bbcc308..fb3cf7b5 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 7603 2005-11-23 17:21:53Z barras $ *)
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,9 +42,7 @@ 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)
| '~' ->
let n = expand_atom s (i+1) in
let v =
@@ -52,44 +50,16 @@ let rec expand_macros b s i =
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 glob 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
-
(* All subdirectories, recursively *)
let exists_dir dir =
@@ -214,6 +184,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..ea463732 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 7603 2005-11-23 17:21:53Z barras $ 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,8 +16,6 @@
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
@@ -48,6 +46,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 +66,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
-
-
diff --git a/lib/tlm.ml b/lib/tlm.ml
index 23021be4..2939e91a 100644
--- a/lib/tlm.ml
+++ b/lib/tlm.ml
@@ -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..2e6e1279 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 8672 2006-03-29 21:06:33Z 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
@@ -251,6 +250,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 =
@@ -362,12 +368,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 +385,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 *)
@@ -596,6 +606,20 @@ 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')
+
(* Matrices *)
let matrix_transpose mat =
@@ -693,6 +717,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
diff --git a/lib/util.mli b/lib/util.mli
index 19f05ea4..f77aa6b4 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 8672 2006-03-29 21:06:33Z 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
@@ -109,6 +106,8 @@ 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
@@ -130,8 +129,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. *)
@@ -170,6 +169,7 @@ 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
(*s Matrices *)
@@ -223,6 +223,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