aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorglondu2009-09-17 15:58:14 +0000
committerglondu2009-09-17 15:58:14 +0000
commit61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch)
tree961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /lib
parent6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff)
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
-rw-r--r--lib/bigint.ml26
-rw-r--r--lib/bstack.ml6
-rw-r--r--lib/compat.ml48
-rw-r--r--lib/dnet.ml58
-rw-r--r--lib/dnet.mli18
-rw-r--r--lib/dyn.ml2
-rw-r--r--lib/edit.ml16
-rw-r--r--lib/envars.ml50
-rw-r--r--lib/explore.ml18
-rw-r--r--lib/explore.mli8
-rw-r--r--lib/flags.ml4
-rw-r--r--lib/gmapl.ml2
-rw-r--r--lib/hashcons.ml6
-rw-r--r--lib/heap.ml54
-rw-r--r--lib/heap.mli20
-rw-r--r--lib/lib.mllib12
-rw-r--r--lib/option.ml28
-rw-r--r--lib/option.mli14
-rw-r--r--lib/pp.ml422
-rw-r--r--lib/pp.mli2
-rw-r--r--lib/pp_control.ml14
-rw-r--r--lib/pp_control.mli4
-rw-r--r--lib/predicate.ml2
-rw-r--r--lib/profile.ml54
-rw-r--r--lib/profile.mli6
-rw-r--r--lib/refutpat.ml42
-rw-r--r--lib/rtree.ml12
-rw-r--r--lib/rtree.mli4
-rw-r--r--lib/system.ml60
-rw-r--r--lib/system.mli8
-rw-r--r--lib/tlm.ml26
-rw-r--r--lib/util.ml340
-rw-r--r--lib/util.mli20
33 files changed, 463 insertions, 463 deletions
diff --git a/lib/bigint.ml b/lib/bigint.ml
index 3b974652b9..f505bbe14e 100644
--- a/lib/bigint.ml
+++ b/lib/bigint.ml
@@ -19,8 +19,8 @@ open Pp
(* 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.
+ 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,
@@ -78,7 +78,7 @@ let normalize_neg n =
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 Array.length n = 0 then n else
if n.(0) = -1 then normalize_neg n else normalize_pos n
let neg m =
@@ -192,7 +192,7 @@ let euclid m d =
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 =
+ 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
@@ -200,7 +200,7 @@ let euclid m d =
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 =
+ 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
@@ -232,11 +232,11 @@ let of_string s =
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 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);
+ 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
@@ -296,7 +296,7 @@ let app_pair f (m, n) =
(f m, f n)
let add m n =
- if Obj.is_int m & Obj.is_int 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))
@@ -311,8 +311,8 @@ let mult m 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
+ 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))
@@ -360,12 +360,12 @@ let pow =
let (quo,rem) = div2_with_rest m in
pow_aux
((* [if m mod 2 = 1]*)
- if rem then
+ if rem then
mult n odd_rest
else
odd_rest )
(* quo = [m/2] *)
- (mult n n) quo
+ (mult n n) quo
in
pow_aux one
@@ -393,7 +393,7 @@ let check () =
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 ->
+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
diff --git a/lib/bstack.ml b/lib/bstack.ml
index b4232ebcf0..4191ccdb15 100644
--- a/lib/bstack.ml
+++ b/lib/bstack.ml
@@ -47,10 +47,10 @@ let push bs e =
incr_size bs;
bs.depth <- bs.depth + 1;
bs.stack.(bs.pos) <- e
-
+
let pop bs =
if bs.size > 1 then begin
- bs.size <- bs.size - 1;
+ bs.size <- bs.size - 1;
bs.depth <- bs.depth - 1;
let oldpos = bs.pos in
decr_pos bs;
@@ -61,7 +61,7 @@ let pop bs =
let top bs =
if bs.size >= 1 then bs.stack.(bs.pos)
else error "Nothing on the stack"
-
+
let app_push bs f =
if bs.size = 0 then error "Nothing on the stack"
else push bs (f (bs.stack.(bs.pos)))
diff --git a/lib/compat.ml4 b/lib/compat.ml4
index 481b9f8d46..7566624b80 100644
--- a/lib/compat.ml4
+++ b/lib/compat.ml4
@@ -12,8 +12,8 @@
IFDEF OCAML309 THEN DEFINE OCAML308 END
-IFDEF CAMLP5 THEN
-module M = struct
+IFDEF CAMLP5 THEN
+module M = struct
type loc = Stdpp.location
let dummy_loc = Stdpp.dummy_loc
let make_loc = Stdpp.make_loc
@@ -39,11 +39,11 @@ let unloc (b,e) =
loc
let join_loc loc1 loc2 =
if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc
- else (fst loc1, snd loc2)
+ else (fst loc1, snd loc2)
type token = Token.t
type lexer = Token.lexer
end
-ELSE
+ELSE
module M = struct
type loc = int * int
let dummy_loc = (0,0)
diff --git a/lib/dnet.ml b/lib/dnet.ml
index b5a7bb7283..0236cdab3a 100644
--- a/lib/dnet.ml
+++ b/lib/dnet.ml
@@ -10,8 +10,8 @@
(* Generic dnet implementation over non-recursive types *)
-module type Datatype =
-sig
+module type Datatype =
+sig
type 'a t
val map : ('a -> 'b) -> 'a t -> 'b t
val map2 : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
@@ -44,11 +44,11 @@ sig
val map : (ident -> ident) -> (unit structure -> unit structure) -> t -> t
end
-module Make =
- functor (T:Datatype) ->
- functor (Ident:Set.OrderedType) ->
+module Make =
+ functor (T:Datatype) ->
+ functor (Ident:Set.OrderedType) ->
functor (Meta:Set.OrderedType) ->
-struct
+struct
type ident = Ident.t
type meta = Meta.t
@@ -58,7 +58,7 @@ struct
| Meta of meta
type 'a structure = 'a T.t
-
+
module Idset = Set.Make(Ident)
module Mmap = Map.Make(Meta)
module Tmap = Map.Make(struct type t = unit structure
@@ -70,7 +70,7 @@ struct
(* we store identifiers at the leaf of the dnet *)
- type node =
+ type node =
| Node of t structure
| Terminal of t structure * idset
@@ -85,7 +85,7 @@ struct
(* given a node of the net and a word, returns the subnet with the
same head as the word (with the rest of the nodes) *)
- let split l (w:'a structure) : node * node Tmap.t =
+ let split l (w:'a structure) : node * node Tmap.t =
let elt : node = Tmap.find (head w) l in
(elt, Tmap.remove (head w) l)
@@ -101,24 +101,24 @@ struct
Nodes ((Tmap.add (head w) new_node tl), m)
with Not_found ->
let new_content = T.map (fun p -> add empty p id) w in
- let new_node =
+ let new_node =
if T.terminal w then
Terminal (new_content, Idset.singleton id)
else Node new_content in
Nodes ((Tmap.add (head w) new_node t), m) )
- | Meta i ->
- let m =
+ | Meta i ->
+ let m =
try Mmap.add i (Idset.add id (Mmap.find i m)) m
with Not_found -> Mmap.add i (Idset.singleton id) m in
Nodes (t, m)
let add t w id = add t w id
-
+
let rec find_all (Nodes (t,m)) : idset =
Idset.union
(Mmap.fold (fun _ -> Idset.union) m Idset.empty)
(Tmap.fold
- ( fun _ n acc ->
+ ( fun _ n acc ->
let s2 = match n with
| Terminal (_,is) -> is
| Node e -> T.choose find_all e in
@@ -137,44 +137,44 @@ struct
| (Some s, _ | _, Some s) -> s
| _ -> raise Not_found
- let fold_pattern ?(complete=true) f acc pat dn =
+ let fold_pattern ?(complete=true) f acc pat dn =
let deferred = ref [] in
let leafs,metas = ref None, ref None in
- let leaf s = leafs := match !leafs with
+ let leaf s = leafs := match !leafs with
| None -> Some s
| Some s' -> Some (fast_inter s s') in
let meta s = metas := match !metas with
| None -> Some s
| Some s' -> Some (Idset.union s s') in
let defer c = deferred := c::!deferred in
- let rec fp_rec (p:term_pattern) (Nodes(t,m) as dn:t) =
+ let rec fp_rec (p:term_pattern) (Nodes(t,m) as dn:t) =
Mmap.iter (fun _ -> meta) m; (* TODO: gérer patterns nonlin ici *)
match p with
| Meta m -> defer (m,dn)
- | Term w ->
+ | Term w ->
try match select t w with
| Terminal (_,is) -> leaf is
- | Node e ->
+ | Node e ->
if complete then T.fold2 (fun _ -> fp_rec) () w e else
- if T.fold2
+ if T.fold2
(fun b p dn -> match p with
| Term _ -> fp_rec p dn; false
| Meta _ -> b
) true w e
then T.choose (T.choose fp_rec w) e
- with Not_found ->
+ with Not_found ->
if Mmap.is_empty m then raise Not_found else ()
in try
fp_rec pat dn;
- (try Some (option_any2 Idset.union !leafs !metas) with Not_found -> None),
+ (try Some (option_any2 Idset.union !leafs !metas) with Not_found -> None),
List.fold_left (fun acc (m,dn) -> f m dn acc) acc !deferred
with Not_found | Empty -> None,acc
(* intersection of two dnets. keep only the common pairs *)
let rec inter (t1:t) (t2:t) : t =
let inter_map f (Nodes (t1,m1):t) (Nodes (t2,m2):t) : t =
- Nodes
- (Tmap.fold
+ Nodes
+ (Tmap.fold
( fun k e acc ->
try Tmap.add k (f e (Tmap.find k t2)) acc
with Not_found -> acc
@@ -193,8 +193,8 @@ struct
) t1 t2
let rec union (t1:t) (t2:t) : t =
- let union_map f (Nodes (t1,m1):t) (Nodes (t2,m2):t) : t =
- Nodes
+ let union_map f (Nodes (t1,m1):t) (Nodes (t2,m2):t) : t =
+ Nodes
(Tmap.fold
( fun k e acc ->
try Tmap.add k (f e (Tmap.find k acc)) acc
@@ -211,12 +211,12 @@ struct
| Terminal (e1,s1), Terminal (_,s2) -> Terminal (e1,Idset.union s1 s2)
| Node e1, Node e2 -> Node (T.map2 union e1 e2)
| _ -> assert false
- ) t1 t2
-
+ ) t1 t2
+
let find_match (p:term_pattern) (t:t) : idset =
let metas = ref Mmap.empty in
let (mset,lset) = fold_pattern ~complete:false
- (fun m t acc ->
+ (fun m t acc ->
(* Printf.printf "eval pat %d\n" (Obj.magic m:int);*)
Some (option_any2 fast_inter acc
(Some(let t = try inter t (Mmap.find m !metas) with Not_found -> t in
diff --git a/lib/dnet.mli b/lib/dnet.mli
index a01bbb0e2e..b2f2714720 100644
--- a/lib/dnet.mli
+++ b/lib/dnet.mli
@@ -33,7 +33,7 @@
symmetric, see term_dnet.ml).
The complexity of the search is (almost) the depth of the term.
-
+
To use it, you have to provide a module (Datatype) with the datatype
parametrized on the recursive argument. example:
@@ -70,13 +70,13 @@ end
module type S =
sig
type t
-
+
(* provided identifier type *)
type ident
(* provided metavariable type *)
type meta
-
+
(* provided parametrized datastructure *)
type 'a structure
@@ -92,13 +92,13 @@ sig
type term_pattern = 'a structure pattern as 'a
val empty : t
-
+
(* [add t w i] adds a new association (w,i) in t. *)
val add : t -> term_pattern -> ident -> t
-
+
(* [find_all t] returns all identifiers contained in t. *)
val find_all : t -> Idset.t
-
+
(* [fold_pattern f acc p dn] folds f on each meta of p, passing the
meta and the sub-dnet under it. The result includes:
- Some set if identifiers were gathered on the leafs of the term
@@ -118,10 +118,10 @@ sig
(* apply a function on each identifier and node of terms in a dnet *)
val map : (ident -> ident) -> (unit structure -> unit structure) -> t -> t
end
-
+
module Make :
- functor (T:Datatype) ->
- functor (Ident:Set.OrderedType) ->
+ functor (T:Datatype) ->
+ functor (Ident:Set.OrderedType) ->
functor (Meta:Set.OrderedType) ->
S with type ident = Ident.t
and type meta = Meta.t
diff --git a/lib/dyn.ml b/lib/dyn.ml
index 1e3aa294d7..d2bd458a7d 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -17,7 +17,7 @@ type t = string * Obj.t
let dyntab = ref ([] : string list)
let create s =
- if List.mem s !dyntab then
+ if List.mem s !dyntab then
anomaly ("Dyn.create: already declared dynamic " ^ s);
dyntab := s :: !dyntab;
((fun v -> (s,Obj.repr v)),
diff --git a/lib/edit.ml b/lib/edit.ml
index e6f2907ecc..fd870a21ba 100644
--- a/lib/edit.ml
+++ b/lib/edit.ml
@@ -16,7 +16,7 @@ type ('a,'b,'c) t = {
mutable last_focused_stk : 'a list;
buf : ('a, 'b Bstack.t * 'c) Hashtbl.t }
-let empty () = {
+let empty () = {
focus = None;
last_focused_stk = [];
buf = Hashtbl.create 17 }
@@ -38,7 +38,7 @@ let unfocus e =
e.last_focused_stk <- foc::(list_except foc e.last_focused_stk);
e.focus <- None
end
-
+
let last_focused e =
match e.last_focused_stk with
| [] -> None
@@ -48,7 +48,7 @@ let restore_last_focus e =
match e.last_focused_stk with
| [] -> ()
| f::_ -> focus e f
-
+
let focusedp e =
match e.focus with
| None -> false
@@ -96,8 +96,8 @@ let depth e =
(* Undo focused proof of [e] to reach depth [n] *)
let undo_todepth e n =
match e.focus with
- | None ->
- if n <> 0
+ | 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 ->
@@ -109,7 +109,7 @@ let undo_todepth e n =
let create e (d,b,c,usize) =
if Hashtbl.mem e.buf d then
- errorlabstrm "Edit.create"
+ errorlabstrm "Edit.create"
(str"Already editing something of that name");
let bs = Bstack.create usize b in
Hashtbl.add e.buf d (bs,c)
@@ -123,11 +123,11 @@ let delete e d =
| Some d' -> if d = d' then (e.focus <- None ; (restore_last_focus e))
| None -> ()
-let dom e =
+let dom e =
let l = ref [] in
Hashtbl.iter (fun x _ -> l := x :: !l) e.buf;
!l
-
+
let clear e =
e.focus <- None;
e.last_focused_stk <- [];
diff --git a/lib/envars.ml b/lib/envars.ml
index d700ffe160..2e680ad057 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -9,77 +9,77 @@
(* This file gathers environment variables needed by Coq to run (such
as coqlib) *)
-let coqbin () =
+let coqbin () =
if !Flags.boot || Coq_config.local
then Filename.concat Coq_config.coqsrc "bin"
else System.canonical_path_name (Filename.dirname Sys.executable_name)
-let guess_coqlib () =
+let guess_coqlib () =
let file = "states/initial.coq" in
- if Sys.file_exists (Filename.concat Coq_config.coqlib file)
+ if Sys.file_exists (Filename.concat Coq_config.coqlib file)
then Coq_config.coqlib
- else
+ else
let coqbin = System.canonical_path_name (Filename.dirname Sys.executable_name) in
let prefix = Filename.dirname coqbin in
- let rpath = if Coq_config.local then [] else
+ let rpath = if Coq_config.local then [] else
(if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) in
let coqlib = List.fold_left Filename.concat prefix rpath in
if Sys.file_exists (Filename.concat coqlib file) then coqlib else
Util.error "cannot guess a path for Coq libraries; please use -coqlib option"
-
-let coqlib () =
+
+let coqlib () =
if !Flags.coqlib_spec then !Flags.coqlib else
(if !Flags.boot then Coq_config.coqsrc else guess_coqlib ())
let path_to_list p =
let sep = if Sys.os_type = "Win32" then ';' else ':' in
- Util.split_string_at sep p
+ Util.split_string_at sep p
let rec which l f =
match l with
| [] -> raise Not_found
- | p :: tl ->
- if Sys.file_exists (Filename.concat p f)
- then p
+ | p :: tl ->
+ if Sys.file_exists (Filename.concat p f)
+ then p
else which tl f
-
-let guess_camlbin () =
- let path = try Sys.getenv "PATH" with _ -> raise Not_found in
+
+let guess_camlbin () =
+ let path = try Sys.getenv "PATH" with _ -> raise Not_found in
let lpath = path_to_list path in
which lpath "ocamlc"
-let guess_camlp4bin () =
- let path = try Sys.getenv "PATH" with _ -> raise Not_found in
+let guess_camlp4bin () =
+ let path = try Sys.getenv "PATH" with _ -> raise Not_found in
let lpath = path_to_list path in
which lpath Coq_config.camlp4
-let camlbin () =
+let camlbin () =
if !Flags.camlbin_spec then !Flags.camlbin else
if !Flags.boot then Coq_config.camlbin else
try guess_camlbin () with _ -> Coq_config.camlbin
-let camllib () =
+let camllib () =
if !Flags.boot
then Coq_config.camllib
- else
- let camlbin = camlbin () in
+ else
+ let camlbin = camlbin () in
let com = (Filename.concat camlbin "ocamlc") ^ " -where" in
let _,res = System.run_command (fun x -> x) (fun _ -> ()) com in
Util.strip res
(* TODO : essayer aussi camlbin *)
-let camlp4bin () =
+let camlp4bin () =
if !Flags.camlp4bin_spec then !Flags.camlp4bin else
if !Flags.boot then Coq_config.camlp4bin else
try guess_camlp4bin () with _ -> Coq_config.camlp4bin
-let camlp4lib () =
+let camlp4lib () =
if !Flags.boot
then Coq_config.camlp4lib
- else
- let camlp4bin = camlp4bin () in
+ else
+ let camlp4bin = camlp4bin () in
let com = (Filename.concat camlp4bin Coq_config.camlp4) ^ " -where" in
let _,res = System.run_command (fun x -> x) (fun _ -> ()) com in
Util.strip res
-
+
diff --git a/lib/explore.ml b/lib/explore.ml
index 51ff79e32b..7604950998 100644
--- a/lib/explore.ml
+++ b/lib/explore.ml
@@ -23,7 +23,7 @@ module Make = functor(S : SearchProblem) -> struct
type position = int list
- let pp_position p =
+ let pp_position p =
let rec pp_rec = function
| [] -> ()
| [i] -> printf "%d" i
@@ -33,21 +33,21 @@ module Make = functor(S : SearchProblem) -> struct
(*s Depth first search. *)
- let rec depth_first s =
+ let rec depth_first s =
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 =
+ let debug_depth_first s =
let rec explore p s =
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
| [s] -> explore (i::p) s
- | s :: l ->
+ | s :: l ->
try explore (i::p) s with Not_found -> explore_many (succ i) p l
in
explore [1] s
@@ -66,7 +66,7 @@ module Make = functor(S : SearchProblem) -> struct
| h, x::t -> x, (h,t)
| h, [] -> match List.rev h with x::t -> x, ([],t) | [] -> raise Empty
- let breadth_first s =
+ let breadth_first s =
let rec explore q =
let (s, q') = try pop q with Empty -> raise Not_found in
enqueue q' (S.branching s)
@@ -76,15 +76,15 @@ module Make = functor(S : SearchProblem) -> struct
in
enqueue empty [s]
- let debug_breadth_first s =
+ let debug_breadth_first s =
let rec explore q =
- let ((p,s), q') = try pop q with Empty -> raise Not_found in
+ 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
| s :: l ->
- let ps = i::p in
+ let ps = i::p in
pp_position ps; S.pp s;
if S.success s then s else enqueue (succ i) p (push (ps,s) q) l
in
diff --git a/lib/explore.mli b/lib/explore.mli
index 907e2f2569..e29f27955a 100644
--- a/lib/explore.mli
+++ b/lib/explore.mli
@@ -12,12 +12,12 @@
(*s A search problem implements the following signature [SearchProblem].
[state] is the type of states of the search tree.
- [branching] is the branching function; if [branching s] returns an
+ [branching] is the branching function; if [branching s] returns an
empty list, then search from [s] is aborted; successors of [s] are
recursively searched in the order they appear in the list.
- [success] determines whether a given state is a success.
+ [success] determines whether a given state is a success.
- [pp] is a pretty-printer for states used in debugging versions of the
+ [pp] is a pretty-printer for states used in debugging versions of the
search functions. *)
module type SearchProblem = sig
@@ -33,7 +33,7 @@ module type SearchProblem = sig
end
(*s Functor [Make] returns some search functions given a search problem.
- Search functions raise [Not_found] if no success is found.
+ Search functions raise [Not_found] if no success is found.
States are always visited in the order they appear in the
output of [branching] (whatever the search method is).
Debugging versions of the search functions print the position of the
diff --git a/lib/flags.ml b/lib/flags.ml
index dac88a4733..1bf393fd08 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -80,8 +80,8 @@ let is_unsafe s = Stringset.mem s !unsafe_set
let boxed_definitions = ref true
let set_boxed_definitions b = boxed_definitions := b
-let boxed_definitions _ = !boxed_definitions
-
+let boxed_definitions _ = !boxed_definitions
+
(* Flags for external tools *)
let subst_command_placeholder s t =
diff --git a/lib/gmapl.ml b/lib/gmapl.ml
index 8fc2daf96a..cec10d6444 100644
--- a/lib/gmapl.ml
+++ b/lib/gmapl.ml
@@ -32,4 +32,4 @@ let remove x y m =
let l = Gmap.find x m in
Gmap.add x (if List.mem y l then list_subtract l [y] else l) m
-
+
diff --git a/lib/hashcons.ml b/lib/hashcons.ml
index c7cd145424..921a4ed563 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -19,7 +19,7 @@
* the hash-consing functions u provides.
* [equal] is a comparison function. It is allowed to use physical equality
* on the sub-terms hash-consed by the hash_sub function.
- * [hash] is the hash function given to the Hashtbl.Make function
+ * [hash] is the hash function given to the Hashtbl.Make function
*
* Note that this module type coerces to the argument of Hashtbl.Make.
*)
@@ -106,7 +106,7 @@ let recursive_loop_hcons h u =
let rec hrec visited x =
if List.memq x visited then x
else hc (hrec (x::visited),u) x
- in
+ in
hrec []
(* For 2 mutually recursive types *)
@@ -164,7 +164,7 @@ let comp_obj o1 o2 =
else false
else o1=o2
-let hash_obj hrec o =
+let hash_obj hrec o =
begin
if tuple_p o then
let n = Obj.size o in
diff --git a/lib/heap.ml b/lib/heap.ml
index 47718bf3e7..7ddb4a7205 100644
--- a/lib/heap.ml
+++ b/lib/heap.ml
@@ -16,35 +16,35 @@ module type Ordered = sig
end
module type S =sig
-
+
(* Type of functional heaps *)
type t
(* Type of elements *)
type elt
-
+
(* The empty heap *)
val empty : t
-
+
(* [add x h] returns a new heap containing the elements of [h], plus [x];
complexity $O(log(n))$ *)
val add : elt -> t -> t
-
+
(* [maximum h] returns the maximum element of [h]; raises [EmptyHeap]
when [h] is empty; complexity $O(1)$ *)
val maximum : t -> elt
-
+
(* [remove h] returns a new heap containing the elements of [h], except
- the maximum of [h]; raises [EmptyHeap] when [h] is empty;
- complexity $O(log(n))$ *)
+ the maximum of [h]; raises [EmptyHeap] when [h] is empty;
+ complexity $O(log(n))$ *)
val remove : t -> t
-
+
(* usual iterators and combinators; elements are presented in
arbitrary order *)
val iter : (elt -> unit) -> t -> unit
-
+
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
-
+
end
exception EmptyHeap
@@ -54,9 +54,9 @@ exception EmptyHeap
module Functional(X : Ordered) = struct
(* Heaps are encoded as complete binary trees, i.e., binary trees
- which are full expect, may be, on the bottom level where it is filled
- from the left.
- These trees also enjoy the heap property, namely the value of any node
+ which are full expect, may be, on the bottom level where it is filled
+ from the left.
+ These trees also enjoy the heap property, namely the value of any node
is greater or equal than those of its left and right subtrees.
There are 4 kinds of complete binary trees, denoted by 4 constructors:
@@ -68,7 +68,7 @@ module Functional(X : Ordered) = struct
and [PFP] for a partial tree with a full left subtree and a partial
right subtree. *)
- type t =
+ type t =
| Empty
| FFF of t * X.t * t (* full (full, full) *)
| PPF of t * X.t * t (* partial (partial, full) *)
@@ -78,7 +78,7 @@ module Functional(X : Ordered) = struct
type elt = X.t
let empty = Empty
-
+
(* smart constructors for insertion *)
let p_f l x r = match l with
| Empty | FFF _ -> PFF (l, x, r)
@@ -89,7 +89,7 @@ module Functional(X : Ordered) = struct
| r -> PFP (l, x, r)
let rec add x = function
- | Empty ->
+ | Empty ->
FFF (Empty, x, Empty)
(* insertion to the left *)
| FFF (l, y, r) | PPF (l, y, r) ->
@@ -113,9 +113,9 @@ module Functional(X : Ordered) = struct
| r -> PFP (l, x, r)
let rec remove = function
- | Empty ->
+ | Empty ->
raise EmptyHeap
- | FFF (Empty, _, Empty) ->
+ | FFF (Empty, _, Empty) ->
Empty
| PFF (l, _, Empty) ->
l
@@ -124,30 +124,30 @@ module Functional(X : Ordered) = struct
let xl = maximum l in
let xr = maximum r in
let l' = remove l in
- if X.compare xl xr >= 0 then
- p_f l' xl r
- else
+ if X.compare xl xr >= 0 then
+ p_f l' xl r
+ else
p_f l' xr (add xl (remove r))
(* remove on the right *)
| FFF (l, x, r) | PFP (l, x, r) ->
let xl = maximum l in
let xr = maximum r in
let r' = remove r in
- if X.compare xl xr > 0 then
+ if X.compare xl xr > 0 then
pf_ (add xr (remove l)) xl r'
- else
+ else
pf_ l xr r'
let rec iter f = function
- | Empty ->
+ | Empty ->
()
- | FFF (l, x, r) | PPF (l, x, r) | PFF (l, x, r) | PFP (l, x, r) ->
+ | FFF (l, x, r) | PPF (l, x, r) | PFF (l, x, r) | PFP (l, x, r) ->
iter f l; f x; iter f r
let rec fold f h x0 = match h with
- | Empty ->
+ | Empty ->
x0
- | FFF (l, x, r) | PPF (l, x, r) | PFF (l, x, r) | PFP (l, x, r) ->
+ | FFF (l, x, r) | PPF (l, x, r) | PFF (l, x, r) | PFP (l, x, r) ->
fold f l (fold f r (f x x0))
end
diff --git a/lib/heap.mli b/lib/heap.mli
index 0bef2edb22..777e356de7 100644
--- a/lib/heap.mli
+++ b/lib/heap.mli
@@ -16,35 +16,35 @@ module type Ordered = sig
end
module type S =sig
-
+
(* Type of functional heaps *)
type t
(* Type of elements *)
type elt
-
+
(* The empty heap *)
val empty : t
-
+
(* [add x h] returns a new heap containing the elements of [h], plus [x];
complexity $O(log(n))$ *)
val add : elt -> t -> t
-
+
(* [maximum h] returns the maximum element of [h]; raises [EmptyHeap]
when [h] is empty; complexity $O(1)$ *)
val maximum : t -> elt
-
+
(* [remove h] returns a new heap containing the elements of [h], except
- the maximum of [h]; raises [EmptyHeap] when [h] is empty;
- complexity $O(log(n))$ *)
+ the maximum of [h]; raises [EmptyHeap] when [h] is empty;
+ complexity $O(log(n))$ *)
val remove : t -> t
-
+
(* usual iterators and combinators; elements are presented in
arbitrary order *)
val iter : (elt -> unit) -> t -> unit
-
+
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
-
+
end
exception EmptyHeap
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 1f203ec8d9..2321abd1b0 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -4,17 +4,17 @@ Compat
Flags
Util
Bigint
-Hashcons
+Hashcons
Dyn
System
-Envars
-Bstack
+Envars
+Bstack
Edit
-Gset
+Gset
Gmap
-Tlm
+Tlm
Gmapl
-Profile
+Profile
Explore
Predicate
Rtree
diff --git a/lib/option.ml b/lib/option.ml
index 3d98034256..2a530b89bd 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -20,7 +20,7 @@
let has_some = function
| None -> false
| _ -> true
-
+
exception IsNone
(** [get x] returns [y] where [x] is [Some y]. It raises IsNone
@@ -34,11 +34,11 @@ let make x = Some x
(** [init b x] returns [Some x] if [b] is [true] and [None] otherwise. *)
let init b x =
- if b then
+ if b then
Some x
else
None
-
+
(** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *)
let flatten = function
@@ -48,7 +48,7 @@ let flatten = function
(** {6 "Iterators"} ***)
-(** [iter f x] executes [f y] if [x] equals [Some y]. It does nothing
+(** [iter f x] executes [f y] if [x] equals [Some y]. It does nothing
otherwise. *)
let iter f = function
| Some y -> f y
@@ -60,7 +60,7 @@ exception Heterogeneous
(** [iter2 f x y] executes [f z w] if [x] equals [Some z] and [y] equals
[Some w]. It does nothing if both [x] and [y] are [None]. And raises
[Heterogeneous] otherwise. *)
-let iter2 f x y =
+let iter2 f x y =
match x,y with
| Some z, Some w -> f z w
| None,None -> ()
@@ -92,7 +92,7 @@ let fold_left2 f a x y =
| _ -> raise Heterogeneous
(** [fold_right f x a] is [f y a] if [x] is [Some y], and [a] otherwise. *)
-let fold_right f x a =
+let fold_right f x a =
match x with
| Some y -> f y a
| _ -> a
@@ -112,20 +112,20 @@ let default a = function
(** [lift f x] is the same as [map f x]. *)
let lift = map
-(** [lift_right f a x] is [Some (f a y)] if [x] is [Some y], and
+(** [lift_right f a x] is [Some (f a y)] if [x] is [Some y], and
[None] otherwise. *)
let lift_right f a = function
| Some y -> Some (f a y)
| _ -> None
-(** [lift_left f x a] is [Some (f y a)] if [x] is [Some y], and
+(** [lift_left f x a] is [Some (f y a)] if [x] is [Some y], and
[None] otherwise. *)
let lift_left f x a =
match x with
| Some y -> Some (f y a)
| _ -> None
-(** [lift2 f x y] is [Some (f z w)] if [x] equals [Some z] and [y] equals
+(** [lift2 f x y] is [Some (f z w)] if [x] equals [Some z] and [y] equals
[Some w]. It is [None] otherwise. *)
let lift2 f x y =
match x,y with
@@ -137,18 +137,18 @@ let lift2 f x y =
(** {6 Operations with Lists} *)
module List =
- struct
+ struct
(** [List.cons x l] equals [y::l] if [x] is [Some y] and [l] otherwise. *)
let cons x l =
match x with
| Some y -> y::l
| _ -> l
-
+
(** [List.flatten l] is the list of all the [y]s such that [l] contains
[Some y] (in the same order). *)
let rec flatten = function
| x::l -> cons x (flatten l)
- | [] -> []
+ | [] -> []
end
@@ -157,8 +157,8 @@ end
module Misc =
struct
- (** [Misc.compare f x y] lifts the equality predicate [f] to
- option types. That is, if both [x] and [y] are [None] then
+ (** [Misc.compare f x y] lifts the equality predicate [f] to
+ option types. That is, if both [x] and [y] are [None] then
it returns [true], if they are bothe [Some _] then
[f] is called. Otherwise it returns [false]. *)
let compare f x y =
diff --git a/lib/option.mli b/lib/option.mli
index 04f3ca37d0..8002a7ea29 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -18,7 +18,7 @@
(** [has_some x] is [true] if [x] is of the form [Some y] and [false]
otherwise. *)
val has_some : 'a option -> bool
-
+
exception IsNone
(** [get x] returns [y] where [x] is [Some y]. It raises IsNone
@@ -37,7 +37,7 @@ val flatten : 'a option option -> 'a option
(** {6 "Iterators"} ***)
-(** [iter f x] executes [f y] if [x] equals [Some y]. It does nothing
+(** [iter f x] executes [f y] if [x] equals [Some y]. It does nothing
otherwise. *)
val iter : ('a -> unit) -> 'a option -> unit
@@ -77,15 +77,15 @@ val default : 'a -> 'a option -> 'a
(** [lift] is the same as {!map}. *)
val lift : ('a -> 'b) -> 'a option -> 'b option
-(** [lift_right f a x] is [Some (f a y)] if [x] is [Some y], and
+(** [lift_right f a x] is [Some (f a y)] if [x] is [Some y], and
[None] otherwise. *)
val lift_right : ('a -> 'b -> 'c) -> 'a -> 'b option -> 'c option
-(** [lift_left f x a] is [Some (f y a)] if [x] is [Some y], and
+(** [lift_left f x a] is [Some (f y a)] if [x] is [Some y], and
[None] otherwise. *)
val lift_left : ('a -> 'b -> 'c) -> 'a option -> 'b -> 'c option
-(** [lift2 f x y] is [Some (f z w)] if [x] equals [Some z] and [y] equals
+(** [lift2 f x y] is [Some (f z w)] if [x] equals [Some z] and [y] equals
[Some w]. It is [None] otherwise. *)
val lift2 : ('a -> 'b -> 'c) -> 'a option -> 'b option -> 'c option
@@ -105,8 +105,8 @@ end
(** {6 Miscelaneous Primitives} *)
module Misc : sig
- (** [Misc.compare f x y] lifts the equality predicate [f] to
- option types. That is, if both [x] and [y] are [None] then
+ (** [Misc.compare f x y] lifts the equality predicate [f] to
+ option types. That is, if both [x] and [y] are [None] then
it returns [true], if they are bothe [Some _] then
[f] is called. Otherwise it returns [false]. *)
val compare : ('a -> 'a -> bool) -> 'a option -> 'a option -> bool
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 20a97810e7..b0948b0f40 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -19,7 +19,7 @@ let print_emacs = ref false
let make_pp_emacs() = print_emacs:=true
let make_pp_nonemacs() = print_emacs:=false
-(* The different kinds of blocks are:
+(* The different kinds of blocks are:
\begin{description}
\item[hbox:] Horizontal block no line breaking;
\item[vbox:] Vertical block each break leads to a new line;
@@ -31,9 +31,9 @@ let make_pp_nonemacs() = print_emacs:=false
(except if no mark yet on the reste of the line)
\end{description}
*)
-
+
let comments = ref []
-
+
let rec split_com comacc acc pos = function
[] -> comments := List.rev acc; comacc
| ((b,e),c as com)::coms ->
@@ -132,7 +132,7 @@ let real r = str (string_of_float r)
let bool b = str (string_of_bool b)
let strbrk s =
let rec aux p n =
- if n < String.length s then
+ if n < String.length s then
if s.[n] = ' ' then
if p=n then [< spc (); aux (n+1) (n+1) >]
else [< str (String.sub s p (n-p)); spc (); aux (n+1) (n+1) >]
@@ -224,13 +224,13 @@ let rec pr_com ft s =
| None -> ()
(* pretty printing functions *)
-let pp_dirs ft =
+let pp_dirs ft =
let pp_open_box = function
| Pp_hbox n -> Format.pp_open_hbox ft ()
| Pp_vbox n -> Format.pp_open_vbox ft n
| Pp_hvbox n -> Format.pp_open_hvbox ft n
| Pp_hovbox n -> Format.pp_open_hovbox ft n
- | Pp_tbox -> Format.pp_open_tbox ft ()
+ | Pp_tbox -> Format.pp_open_tbox ft ()
in
let rec pp_cmd = function
| Ppcmd_print(n,s) ->
@@ -264,12 +264,12 @@ let pp_dirs ft =
| Ppdir_ppcmds cmdstream -> Stream.iter pp_cmd cmdstream
| Ppdir_print_newline ->
com_brk ft; Format.pp_print_newline ft ()
- | Ppdir_print_flush -> Format.pp_print_flush ft ()
+ | Ppdir_print_flush -> Format.pp_print_flush ft ()
in
fun dirstream ->
- try
+ try
Stream.iter pp_dir dirstream; com_brk ft
- with
+ with
| e -> Format.pp_print_flush ft () ; raise e
@@ -284,10 +284,10 @@ let ppcmds x = Ppdir_ppcmds x
let emacs_warning_start_string = String.make 1 (Char.chr 254)
let emacs_warning_end_string = String.make 1 (Char.chr 255)
-let warnstart() =
+let warnstart() =
if not !print_emacs then mt() else str emacs_warning_start_string
-let warnend() =
+let warnend() =
if not !print_emacs then mt() else str emacs_warning_end_string
let warnbody strm =
diff --git a/lib/pp.mli b/lib/pp.mli
index ab2804a53f..66d9bfa674 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -85,7 +85,7 @@ val warning_with : Format.formatter -> string -> unit
val warn_with : Format.formatter -> std_ppcmds -> unit
val pp_flush_with : Format.formatter -> unit -> unit
-val set_warning_function : (Format.formatter -> std_ppcmds -> unit) -> unit
+val set_warning_function : (Format.formatter -> std_ppcmds -> unit) -> unit
(*s Pretty-printing functions \emph{with flush}. *)
diff --git a/lib/pp_control.ml b/lib/pp_control.ml
index 7617d5ca42..ecc546491d 100644
--- a/lib/pp_control.ml
+++ b/lib/pp_control.ml
@@ -18,7 +18,7 @@ type pp_global_params = {
(* Default parameters of pretty-printing *)
-let dflt_gp = {
+let dflt_gp = {
margin = 78;
max_indent = 50;
max_depth = 50;
@@ -26,7 +26,7 @@ let dflt_gp = {
(* A deeper pretty-printer to print proof scripts *)
-let deep_gp = {
+let deep_gp = {
margin = 78;
max_indent = 50;
max_depth = 10000;
@@ -35,13 +35,13 @@ let deep_gp = {
(* set_gp : Format.formatter -> pp_global_params -> unit
* set the parameters of a formatter *)
-let set_gp ft gp =
+let set_gp ft gp =
Format.pp_set_margin ft gp.margin ;
Format.pp_set_max_indent ft gp.max_indent ;
Format.pp_set_max_boxes ft gp.max_depth ;
Format.pp_set_ellipsis_text ft gp.ellipsis
-let set_dflt_gp ft = set_gp ft dflt_gp
+let set_dflt_gp ft = set_gp ft dflt_gp
let get_gp ft =
{ margin = Format.pp_get_margin ft ();
@@ -56,7 +56,7 @@ type 'a pp_formatter_params = {
fp_output : out_channel ;
fp_output_function : string -> int -> int -> unit ;
fp_flush_function : unit -> unit }
-
+
(* Output functions for stdout and stderr *)
let std_fp = {
@@ -69,7 +69,7 @@ let err_fp = {
fp_output_function = output stderr;
fp_flush_function = (fun () -> flush stderr) }
-(* with_fp : 'a pp_formatter_params -> Format.formatter
+(* with_fp : 'a pp_formatter_params -> Format.formatter
* returns of formatter for given formatter functions *)
let with_fp fp =
@@ -83,7 +83,7 @@ let with_output_to ch =
let ft = with_fp { fp_output = ch ;
fp_output_function = (output ch) ;
fp_flush_function = (fun () -> flush ch) } in
- set_gp ft deep_gp;
+ set_gp ft deep_gp;
ft
let std_ft = ref Format.std_formatter
diff --git a/lib/pp_control.mli b/lib/pp_control.mli
index b43584f344..5c481b89af 100644
--- a/lib/pp_control.mli
+++ b/lib/pp_control.mli
@@ -10,7 +10,7 @@
(* Parameters of pretty-printing. *)
-type pp_global_params = {
+type pp_global_params = {
margin : int;
max_indent : int;
max_depth : int;
@@ -25,7 +25,7 @@ val get_gp : Format.formatter -> pp_global_params
(*s Output functions of pretty-printing. *)
-type 'a pp_formatter_params = {
+type 'a pp_formatter_params = {
fp_output : out_channel;
fp_output_function : string -> int -> int -> unit;
fp_flush_function : unit -> unit }
diff --git a/lib/predicate.ml b/lib/predicate.ml
index b2e40d3cf1..af66c0f28d 100644
--- a/lib/predicate.ml
+++ b/lib/predicate.ml
@@ -44,7 +44,7 @@ module type S =
module Make(Ord: OrderedType) =
struct
module EltSet = Set.Make(Ord)
-
+
(* when bool is false, the denoted set is the complement of
the given set *)
type elt = Ord.t
diff --git a/lib/profile.ml b/lib/profile.ml
index 80ae6b4b45..fdea309b8c 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -113,12 +113,12 @@ let ajoute_to_list ((name,n) as e) l =
with Not_found -> e::l
let magic = 1249
-
+
let merge_profile filename (curr_table, curr_outside, curr_total as new_data) =
let (old_table, old_outside, old_total) =
- try
+ try
let c = open_in filename in
- if input_binary_int c <> magic
+ if input_binary_int c <> magic
then Printf.printf "Incompatible recording file: %s\n" filename;
let old_data = input_value c in
close_in c;
@@ -134,7 +134,7 @@ let merge_profile filename (curr_table, curr_outside, curr_total as new_data) =
begin
(try
let c =
- open_out_gen
+ open_out_gen
[Open_creat;Open_wronly;Open_trunc;Open_binary] 0o644 filename in
output_binary_int c magic;
output_value c updated_data;
@@ -186,7 +186,7 @@ overheadA| ...
real 2' | ...
---------- end 2nd f2
overheadC| ...
- ---------- [2'w2] 2nd call to get_time for 2nd f2
+ ---------- [2'w2] 2nd call to get_time for 2nd f2
overheadD| ...
---------- end profile for f2
real 1 | ...
@@ -242,7 +242,7 @@ let time_overhead_A_D () =
ajoute_totalloc p (e.totalloc-.totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
- if not (p==e) then
+ if not (p==e) then
(match !dummy_stack with [] -> assert false | _::s -> stack := s);
dummy_last_alloc := get_alloc ()
done;
@@ -279,7 +279,7 @@ let compute_alloc lo = lo /. (float_of_int word_length)
let format_profile (table, outside, total) =
print_newline ();
- Printf.printf
+ Printf.printf
"%-23s %9s %9s %10s %10s %10s\n"
"Function name" "Own time" "Tot. time" "Own alloc" "Tot. alloc" "Calls ";
let l = Sort.list (fun (_,{tottime=p}) (_,{tottime=p'}) -> p > p') table in
@@ -293,7 +293,7 @@ let format_profile (table, outside, total) =
e.owncount e.intcount)
l;
Printf.printf "%-23s %9.2f %9.2f %10.0f %10.0f %6d\n"
- "others"
+ "others"
(float_of_time outside.owntime) (float_of_time outside.tottime)
(compute_alloc outside.ownalloc)
(compute_alloc outside.totalloc)
@@ -305,7 +305,7 @@ let format_profile (table, outside, total) =
(compute_alloc total.ownalloc)
(compute_alloc total.totalloc);
Printf.printf
- "Time in seconds and allocation in words (1 word = %d bytes)\n"
+ "Time in seconds and allocation in words (1 word = %d bytes)\n"
word_length
let recording_file = ref ""
@@ -319,7 +319,7 @@ let adjust_time ov_bc ov_ad e =
tottime = e.tottime - int_of_float (abcd_all +. bc_imm);
owntime = e.owntime - int_of_float (ad_imm +. bc_imm) }
-let close_profile print =
+let close_profile print =
let dw = spent_alloc () in
let t = get_time () in
match !stack with
@@ -390,7 +390,7 @@ let profile1 e f a =
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
- if not (p==e) then
+ if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
r
@@ -404,7 +404,7 @@ let profile1 e f a =
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
- if not (p==e) then
+ if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
raise exn
@@ -432,7 +432,7 @@ let profile2 e f a b =
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
- if not (p==e) then
+ if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
r
@@ -446,7 +446,7 @@ let profile2 e f a b =
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
- if not (p==e) then
+ if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
raise exn
@@ -474,7 +474,7 @@ let profile3 e f a b c =
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
- if not (p==e) then
+ if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
r
@@ -488,7 +488,7 @@ let profile3 e f a b c =
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
- if not (p==e) then
+ if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
raise exn
@@ -516,7 +516,7 @@ let profile4 e f a b c d =
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
- if not (p==e) then
+ if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
r
@@ -530,7 +530,7 @@ let profile4 e f a b c d =
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
- if not (p==e) then
+ if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
raise exn
@@ -558,7 +558,7 @@ let profile5 e f a b c d g =
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
- if not (p==e) then
+ if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
r
@@ -572,7 +572,7 @@ let profile5 e f a b c d g =
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
- if not (p==e) then
+ if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
raise exn
@@ -600,7 +600,7 @@ let profile6 e f a b c d g h =
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
- if not (p==e) then
+ if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
r
@@ -614,7 +614,7 @@ let profile6 e f a b c d g h =
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
- if not (p==e) then
+ if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
raise exn
@@ -642,7 +642,7 @@ let profile7 e f a b c d g h i =
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
- if not (p==e) then
+ if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
r
@@ -656,7 +656,7 @@ let profile7 e f a b c d g h i =
ajoute_totalloc p (e.totalloc -. totalloc0);
p.intcount <- p.intcount + e.intcount - intcount0 + 1;
p.immcount <- p.immcount + 1;
- if not (p==e) then
+ if not (p==e) then
(match !stack with [] -> assert false | _::s -> stack := s);
last_alloc := get_alloc ();
raise exn
@@ -695,9 +695,9 @@ let obj_stats a =
(!c, !s + !b, !m)
module H = Hashtbl.Make(
- struct
- type t = Obj.t
- let equal = (==)
+ struct
+ type t = Obj.t
+ let equal = (==)
let hash o = Hashtbl.hash (magic o : int)
end)
diff --git a/lib/profile.mli b/lib/profile.mli
index ab2af23985..3647756f71 100644
--- a/lib/profile.mli
+++ b/lib/profile.mli
@@ -49,7 +49,7 @@ let g = profile gkey g';;
Before the program quits, you should call "print_profile ();;". It
produces a result of the following kind:
-Function name Own time Total time Own alloc Tot. alloc Calls
+Function name Own time Total time Own alloc Tot. alloc Calls
f 0.28 0.47 116 116 5 4
h 0.19 0.19 0 0 4 0
g 0.00 0.00 0 0 0 0
@@ -65,7 +65,7 @@ Est. overhead/total 0.00 0.47 2752 3260
the number of calls to profiled functions inside the scope of the
current function
-Remarks:
+Remarks:
- If a function has a polymorphic type, you need to supply it with at
least one argument as in "let f a = profile1 fkey f a;;" (instead of
@@ -103,7 +103,7 @@ val profile6 :
-> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g
val profile7 :
profile_key ->
- ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h)
+ ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h)
-> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h
diff --git a/lib/refutpat.ml4 b/lib/refutpat.ml4
index f2575def43..7c6801a8b9 100644
--- a/lib/refutpat.ml4
+++ b/lib/refutpat.ml4
@@ -15,7 +15,7 @@ open Pcaml
This small camlp4 extension creates a "let*" variant of the "let"
syntax that allow the use of a non-exhaustive pattern. The typical
usage is:
-
+
let* x::l = foo in ...
when foo is already known to be non-empty. This way, no warnings by ocamlc.
diff --git a/lib/rtree.ml b/lib/rtree.ml
index 4832fe58df..ad4d313385 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -53,7 +53,7 @@ let rec subst_rtree_rec depth sub = function
let subst_rtree sub t = subst_rtree_rec 0 [|sub|] t
-(* To avoid looping, we must check that every body introduces a node
+(* To avoid looping, we must check that every body introduces a node
or a parameter *)
let rec expand = function
| Rec(j,defs) ->
@@ -81,17 +81,17 @@ the last one should be accepted
*)
(* Tree destructors, expanding loops when necessary *)
-let dest_param t =
+let dest_param t =
match expand t with
Param (i,j) -> (i,j)
| _ -> failwith "Rtree.dest_param"
-let dest_node t =
+let dest_node t =
match expand t with
Node (l,sons) -> (l,sons)
| _ -> failwith "Rtree.dest_node"
-let is_node t =
+let is_node t =
match expand t with
Node _ -> true
| _ -> false
@@ -104,13 +104,13 @@ let rec map f t = match t with
let rec smartmap f t = match t with
Param _ -> t
- | Node (a,sons) ->
+ | Node (a,sons) ->
let a'=f a and sons' = Util.array_smartmap (map f) sons in
if a'==a && sons'==sons then
t
else
Node (a',sons')
- | Rec(j,defs) ->
+ | Rec(j,defs) ->
let defs' = Util.array_smartmap (map f) defs in
if defs'==defs then
t
diff --git a/lib/rtree.mli b/lib/rtree.mli
index db5475b795..de5a9aa386 100644
--- a/lib/rtree.mli
+++ b/lib/rtree.mli
@@ -11,7 +11,7 @@
(* Type of regular tree with nodes labelled by values of type 'a *)
(* The implementation uses de Bruijn indices, so binding capture
is avoided by the lift operator (see example below) *)
-type 'a t
+type 'a t
(* Building trees *)
@@ -40,7 +40,7 @@ val mk_rec_calls : int -> 'a t array
val mk_rec : 'a t array -> 'a t array
(* [lift k t] increases of [k] the free parameters of [t]. Needed
- to avoid captures when a tree appears under [mk_rec] *)
+ to avoid captures when a tree appears under [mk_rec] *)
val lift : int -> 'a t -> 'a t
val is_node : 'a t -> bool
diff --git a/lib/system.ml b/lib/system.ml
index 982a607f94..4afae39188 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -15,7 +15,7 @@ open Unix
(* Expanding shell variables and home-directories *)
let safe_getenv_def var def =
- try
+ try
Sys.getenv var
with Not_found ->
warning ("Environment variable "^var^" not found: using '"^def^"' .");
@@ -38,7 +38,7 @@ let rec expand_macros s i =
let l = String.length s in
if i=l then s else
match s.[i] with
- | '$' ->
+ | '$' ->
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
@@ -64,7 +64,7 @@ let physical_path_of_string s = s
let string_of_physical_path p = p
(* Hints to partially detects if two paths refer to the same repertory *)
-let rec remove_path_dot p =
+let 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
@@ -82,7 +82,7 @@ let strip_path p =
let canonical_path_name p =
let current = Sys.getcwd () in
- try
+ try
Sys.chdir p;
let p' = Sys.getcwd () in
Sys.chdir current;
@@ -100,7 +100,7 @@ let skipped_dirnames = ref ["CVS"; "_darcs"]
let exclude_search_in_dirname f = skipped_dirnames := f :: !skipped_dirnames
-let ok_dirname f =
+let ok_dirname f =
f <> "" && f.[0] <> '.' && not (List.mem f !skipped_dirnames) &&
try ignore (check_ident f); true with _ -> false
@@ -114,7 +114,7 @@ let all_subdirs ~unix_path:root =
let f = readdir dirh in
if ok_dirname f then
let file = Filename.concat dir f in
- try
+ try
if (stat file).st_kind = S_DIR then begin
let newrel = rel@[f] in
add file newrel;
@@ -132,14 +132,14 @@ let where_in_path ?(warn=true) path filename =
let rec search = function
| lpe :: rem ->
let f = Filename.concat lpe filename in
- if Sys.file_exists f
+ if Sys.file_exists f
then (lpe,f) :: search rem
else search rem
| [] -> [] in
let rec check_and_warn l =
match l with
| [] -> raise Not_found
- | (lpe, f) :: l' ->
+ | (lpe, f) :: l' ->
if warn & l' <> [] then
msg_warning
(str filename ++ str " has been found in" ++ spc () ++
@@ -159,11 +159,11 @@ let find_file_in_path ?(warn=true) paths filename =
else
errorlabstrm "System.find_file_in_path"
(hov 0 (str "Can't find file" ++ spc () ++ str filename))
- else
+ else
try where_in_path ~warn paths filename
with Not_found ->
errorlabstrm "System.find_file_in_path"
- (hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++
+ (hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++
str "on loadpath"))
let is_in_path lpath filename =
@@ -192,40 +192,40 @@ let marshal_in ch =
exception Bad_magic_number of string
let raw_extern_intern magic suffix =
- let extern_state name =
+ let extern_state name =
let filename = make_suffix name suffix in
let channel = open_trapping_failure filename in
output_binary_int channel magic;
filename,channel
- and intern_state filename =
+ and intern_state filename =
let channel = open_in_bin filename in
if input_binary_int channel <> magic then
raise (Bad_magic_number filename);
channel
- in
+ in
(extern_state,intern_state)
let extern_intern ?(warn=true) magic suffix =
let (raw_extern,raw_intern) = raw_extern_intern magic suffix in
- let extern_state name val_0 =
+ let extern_state name val_0 =
try
let (filename,channel) = raw_extern name in
try
marshal_out channel val_0;
close_out channel
- with e ->
+ with e ->
begin try_remove filename; raise e end
with Sys_error s -> error ("System error: " ^ s)
- and intern_state paths name =
+ and intern_state paths name =
try
let _,filename = find_file_in_path ~warn paths (make_suffix name suffix) in
let channel = raw_intern filename in
let v = marshal_in channel in
- close_in channel;
+ close_in channel;
v
- with Sys_error s ->
+ with Sys_error s ->
error("System error: " ^ s)
- in
+ in
(extern_state,intern_state)
(* Communication through files with another executable *)
@@ -237,14 +237,14 @@ let connect writefun readfun com =
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 =
+ 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;
+ 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 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 [|com|] ch_to' ch_from' Unix.stdout
@@ -272,15 +272,15 @@ let run_command converter f c =
let n = ref 0 in
let ne = ref 0 in
- while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ;
+ 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
+ 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
+ let r = converter (String.sub buffe 0 !ne) in
f r;
- Buffer.add_string result r
+ Buffer.add_string result r
done;
(Unix.close_process_full (cin,cout,cerr), Buffer.contents result)
@@ -288,16 +288,16 @@ let run_command converter f c =
type time = float * float * float
-let process_time () =
+let process_time () =
let t = times () in
(t.tms_utime, t.tms_stime)
-let get_time () =
+let get_time () =
let t = times () in
(time(), t.tms_utime, t.tms_stime)
let time_difference (t1,_,_) (t2,_,_) = t2 -. t1
-
+
let fmt_time_difference (startreal,ustart,sstart) (stopreal,ustop,sstop) =
real (stopreal -. startreal) ++ str " secs " ++
str "(" ++
diff --git a/lib/system.mli b/lib/system.mli
index 7556ed9e4d..2932d7b669 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -48,22 +48,22 @@ val marshal_in : in_channel -> 'a
exception Bad_magic_number of string
-val raw_extern_intern : int -> string ->
+val raw_extern_intern : int -> string ->
(string -> string * out_channel) * (string -> in_channel)
-val extern_intern : ?warn:bool -> int -> string ->
+val extern_intern : ?warn:bool -> 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
+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 ->
+val run_command : (string -> string) -> (string -> unit) -> string ->
Unix.process_status * string
(*s Time stamps. *)
diff --git a/lib/tlm.ml b/lib/tlm.ml
index 95092a8859..1c1483ad49 100644
--- a/lib/tlm.ml
+++ b/lib/tlm.ml
@@ -23,41 +23,41 @@ let in_dom (Node (_,m)) lbl = Gmap.mem lbl m
let is_empty_node (Node(a,b)) = (Gset.elements a = []) & (Gmap.to_list b = [])
let assure_arc m lbl =
- if Gmap.mem lbl m then
+ if Gmap.mem lbl m then
m
- else
+ else
Gmap.add lbl (Node (Gset.empty,Gmap.empty)) m
let cleanse_arcs (Node (hereset,m)) =
- let l = Gmap.rng m in
+ let l = Gmap.rng m in
Node(hereset, if List.for_all is_empty_node l then Gmap.empty else m)
let rec at_path f (Node (hereset,m)) = function
- | [] ->
+ | [] ->
cleanse_arcs (Node(f hereset,m))
| h::t ->
- let m = assure_arc m h in
+ let m = assure_arc m h in
cleanse_arcs (Node(hereset,
Gmap.add h (at_path f (Gmap.find h m) t) m))
let add tm (path,v) =
at_path (fun hereset -> Gset.add v hereset) tm path
-
+
let rmv tm (path,v) =
at_path (fun hereset -> Gset.remove v hereset) tm path
-let app f tlm =
+let app f tlm =
let rec apprec pfx (Node(hereset,m)) =
- let path = List.rev pfx in
+ let path = List.rev pfx in
Gset.iter (fun v -> f(path,v)) hereset;
Gmap.iter (fun l tm -> apprec (l::pfx) tm) m
- in
+ in
apprec [] tlm
-
-let to_list tlm =
+
+let to_list tlm =
let rec torec pfx (Node(hereset,m)) =
- let path = List.rev pfx in
+ let path = List.rev pfx in
List.flatten((List.map (fun v -> (path,v)) (Gset.elements hereset))::
(List.map (fun (l,tm) -> torec (l::pfx) tm) (Gmap.to_list m)))
- in
+ in
torec [] tlm
diff --git a/lib/util.ml b/lib/util.ml
index b161b966e1..ddf44eec37 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -36,7 +36,7 @@ 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 located_fold_left f x (_,a) = f x a
+let located_fold_left f x (_,a) = f x a
let located_iter2 f (_,a) (_,b) = f a b
(* Like Exc_located, but specifies the outermost file read, the filename
@@ -73,13 +73,13 @@ let is_blank = function
(* Strings *)
-let explode s =
+let explode s =
let rec explode_rec n =
if n >= String.length s then
[]
- else
+ else
String.make 1 (String.get s n) :: explode_rec (succ n)
- in
+ in
explode_rec 0
let implode sl = String.concat "" sl
@@ -107,12 +107,12 @@ let drop_simple_quotes s =
(* gdzie = where, co = what *)
(* gdzie=gdzie(string) gl=gdzie(length) gi=gdzie(index) *)
-let rec is_sub gdzie gl gi co cl ci =
+let rec is_sub gdzie gl gi co cl ci =
(ci>=cl) ||
- ((String.unsafe_get gdzie gi = String.unsafe_get co ci) &&
+ ((String.unsafe_get gdzie gi = String.unsafe_get co ci) &&
(is_sub gdzie gl (gi+1) co cl (ci+1)))
-let rec raw_str_index i gdzie l c co cl =
+let rec raw_str_index i gdzie l c co cl =
(* First adapt to ocaml 3.11 new semantics of index_from *)
if (i+cl > l) then raise Not_found;
(* Then proceed as in ocaml < 3.11 *)
@@ -120,7 +120,7 @@ let rec raw_str_index i gdzie l c co cl =
if (i'+cl <= l) && (is_sub gdzie l i' co cl 0) then i' else
raw_str_index (i'+1) gdzie l c co cl
-let string_index_from gdzie i co =
+let string_index_from gdzie i co =
if co="" then i else
raw_str_index i gdzie (String.length gdzie)
(String.unsafe_get co 0) co (String.length co)
@@ -142,7 +142,7 @@ let ordinal n =
let split_string_at c s =
let len = String.length s in
let rec split n =
- try
+ try
let pos = String.index_from s n c in
let dir = String.sub s n (pos-n) in
dir :: split (succ pos)
@@ -231,7 +231,7 @@ let classify_unicode unicode =
begin match unicode with
(* utf-8 general punctuation U2080-2089 *)
(* Hyphens *)
- | x when 0x2010 <= x & x <= 0x2011 -> UnicodeLetter
+ | x when 0x2010 <= x & x <= 0x2011 -> UnicodeLetter
(* Dashes and other symbols *)
| x when 0x2012 <= x & x <= 0x2027 -> UnicodeSymbol
(* Per mille and per ten thousand signs *)
@@ -243,9 +243,9 @@ let classify_unicode unicode =
| x when 0x2058 <= x & x <= 0x205E -> UnicodeSymbol
(* Invisible mathematical operators *)
| x when 0x2061 <= x & x <= 0x2063 -> UnicodeSymbol
- (* utf-8 superscript U2070-207C *)
+ (* utf-8 superscript U2070-207C *)
| x when 0x2070 <= x & x <= 0x207C -> UnicodeSymbol
- (* utf-8 subscript U2080-2089 *)
+ (* utf-8 subscript U2080-2089 *)
| x when 0x2080 <= x & x <= 0x2089 -> UnicodeIdentPart
(* utf-8 letter-like U2100-214F *)
| x when 0x2100 <= x & x <= 0x214F -> UnicodeLetter
@@ -296,7 +296,7 @@ let classify_unicode unicode =
exception End_of_input
let utf8_of_unicode n =
- if n < 128 then
+ if n < 128 then
String.make 1 (Char.chr n)
else if n < 2048 then
let s = String.make 2 (Char.chr (128 + n mod 64)) in
@@ -306,18 +306,18 @@ let utf8_of_unicode n =
end
else if n < 65536 then
let s = String.make 3 (Char.chr (128 + n mod 64)) in
- begin
+ begin
s.[1] <- Char.chr (128 + (n / 64) mod 64);
- s.[0] <- Char.chr (224 + n / 4096);
+ s.[0] <- Char.chr (224 + n / 4096);
s
end
else
let s = String.make 4 (Char.chr (128 + n mod 64)) in
- begin
+ begin
s.[2] <- Char.chr (128 + (n / 64) mod 64);
s.[1] <- Char.chr (128 + (n / 4096) mod 64);
s.[0] <- Char.chr (240 + n / 262144);
- s
+ s
end
let next_utf8 s i =
@@ -370,7 +370,7 @@ let check_ident_gen handle s =
i := !i + j
done
with End_of_input -> ()
- with
+ with
| End_of_input -> error "The empty string is not an identifier."
| UnsupportedUtf8 -> error (s^": unsupported character in utf8 sequence.")
| Invalid_argument _ -> error (s^": invalid utf8 sequence.")
@@ -411,18 +411,18 @@ let lowercase_unicode s unicode =
| 0x038C -> 0x03CC
| x when 0x038E <= x & x <= 0x038F -> x + 63
| x when 0x0390 <= x & x <= 0x03AB & x <> 0x03A2 -> x + 32
- (* utf-8 Greek lowercase letters U03B0-03CE *)
+ (* utf-8 Greek lowercase letters U03B0-03CE *)
| x when 0x03AC <= x & x <= 0x03CE -> x
| x when 0x03CF <= x & x <= 0x03FF ->
warning ("Unable to decide which lowercase letter to map to "^s); x
(* utf-8 Cyrillic letters U0400-0481 *)
| x when 0x0400 <= x & x <= 0x040F -> x + 80
| x when 0x0410 <= x & x <= 0x042F -> x + 32
- | x when 0x0430 <= x & x <= 0x045F -> x
+ | x when 0x0430 <= x & x <= 0x045F -> x
| x when 0x0460 <= x & x <= 0x0481 ->
if x mod 2 = 1 then x else x + 1
(* utf-8 Cyrillic letters U048A-U4F9 (Warning: 04CF) *)
- | x when 0x048A <= x & x <= 0x04F9 & x <> 0x04CF ->
+ | x when 0x048A <= x & x <= 0x04F9 & x <> 0x04CF ->
if x mod 2 = 1 then x else x + 1
(* utf-8 Cyrillic supplement letters U0500-U050F *)
| x when 0x0500 <= x & x <= 0x050F ->
@@ -510,41 +510,41 @@ let rec list_compare cmp l1 l2 =
| 0 -> list_compare cmp l1 l2
| c -> c)
-let list_intersect l1 l2 =
+let list_intersect l1 l2 =
List.filter (fun x -> List.mem x l2) l1
-let list_union l1 l2 =
+let list_union l1 l2 =
let rec urec = function
| [] -> l2
| a::l -> if List.mem a l2 then urec l else a::urec l
- in
+ in
urec l1
-let list_unionq l1 l2 =
+let list_unionq l1 l2 =
let rec urec = function
| [] -> l2
| a::l -> if List.memq a l2 then urec l else a::urec l
- in
+ in
urec l1
let list_subtract l1 l2 =
if l2 = [] then l1 else List.filter (fun x -> not (List.mem x l2)) l1
-let list_subtractq l1 l2 =
+let list_subtractq l1 l2 =
if l2 = [] then l1 else List.filter (fun x -> not (List.memq x l2)) l1
-let list_chop n l =
+let list_chop n l =
let rec chop_aux acc = function
| (0, l2) -> (List.rev acc, l2)
| (n, (h::t)) -> chop_aux (h::acc) (pred n, t)
| (_, []) -> failwith "list_chop"
- in
+ in
chop_aux [] (n,l)
-let list_tabulate f len =
+let list_tabulate f len =
let rec tabrec n =
if n = len then [] else (f n)::(tabrec (n+1))
- in
+ in
tabrec 0
let rec list_make n v =
@@ -552,41 +552,41 @@ let rec list_make n v =
else if n < 0 then invalid_arg "list_make"
else v::list_make (n-1) v
-let list_assign l n e =
+let list_assign l n e =
let rec assrec stk = function
| ((h::t), 0) -> List.rev_append stk (e::t)
| ((h::t), n) -> assrec (h::stk) (t, n-1)
| ([], _) -> failwith "list_assign"
- in
+ in
assrec [] (l,n)
let rec list_smartmap f l = match l with
[] -> l
- | h::tl ->
+ | h::tl ->
let h' = f h and tl' = list_smartmap f tl in
if h'==h && tl'==tl then l
else h'::tl'
let list_map_left f = (* ensures the order in case of side-effects *)
let rec map_rec = function
- | [] -> []
+ | [] -> []
| x::l -> let v = f x in v :: map_rec l
- in
+ in
map_rec
-let list_map_i f =
+let list_map_i f =
let rec map_i_rec i = function
- | [] -> []
+ | [] -> []
| x::l -> let v = f i x in v :: map_i_rec (i+1) l
- in
+ in
map_i_rec
-let list_map2_i f i l1 l2 =
+let list_map2_i f i l1 l2 =
let rec map_i i = function
| ([], []) -> []
| ((h1::t1), (h2::t2)) -> let v = f i h1 h2 in v :: map_i (succ i) (t1,t2)
| (_, _) -> invalid_arg "map2_i"
- in
+ in
map_i i (l1,l2)
let list_map3 f l1 l2 l3 =
@@ -594,7 +594,7 @@ let list_map3 f l1 l2 l3 =
| ([], [], []) -> []
| ((h1::t1), (h2::t2), (h3::t3)) -> let v = f h1 h2 h3 in v::map (t1,t2,t3)
| (_, _, _) -> invalid_arg "map3"
- in
+ in
map (l1,l2,l3)
let list_map4 f l1 l2 l3 l4 =
@@ -602,41 +602,41 @@ let list_map4 f l1 l2 l3 l4 =
| ([], [], [], []) -> []
| ((h1::t1), (h2::t2), (h3::t3), (h4::t4)) -> let v = f h1 h2 h3 h4 in v::map (t1,t2,t3,t4)
| (_, _, _, _) -> invalid_arg "map4"
- in
+ in
map (l1,l2,l3,l4)
-let list_index x =
+let list_index x =
let rec index_x n = function
| y::l -> if x = y then n else index_x (succ n) l
| [] -> raise Not_found
- in
+ in
index_x 1
-let list_index0 x l = list_index x l - 1
+let list_index0 x l = list_index x l - 1
-let list_unique_index x =
+let list_unique_index x =
let rec index_x n = function
- | y::l ->
- if x = y then
+ | y::l ->
+ if x = y then
if List.mem x l then raise Not_found
- else n
+ else n
else index_x (succ n) l
- | [] -> raise Not_found
+ | [] -> raise Not_found
in index_x 1
let list_fold_right_i f i l =
let rec it_list_f i l a = match l with
| [] -> a
| b::l -> f (i-1) b (it_list_f (i-1) l a)
- in
+ in
it_list_f (List.length l + i) l
-let list_fold_left_i f =
+let list_fold_left_i f =
let rec it_list_f i a = function
- | [] -> a
+ | [] -> a
| b::l -> it_list_f (i+1) (f i a b) l
- in
- it_list_f
+ in
+ it_list_f
let rec list_fold_left3 f accu l1 l2 l3 =
match (l1, l2, l3) with
@@ -667,16 +667,16 @@ let list_iter3 f l1 l2 l3 =
| ([], [], []) -> ()
| ((h1::t1), (h2::t2), (h3::t3)) -> f h1 h2 h3; iter (t1,t2,t3)
| (_, _, _) -> invalid_arg "map3"
- in
+ in
iter (l1,l2,l3)
let list_iter_i f l = list_fold_left_i (fun i _ x -> f i x) 0 () l
-let list_for_all_i p =
+let list_for_all_i p =
let rec for_all_p i = function
- | [] -> true
+ | [] -> true
| a::l -> p i a && for_all_p (i+1) l
- in
+ in
for_all_p
let list_except x l = List.filter (fun y -> not (x = y)) l
@@ -714,18 +714,18 @@ let rec list_sep_last = function
| hd::[] -> (hd,[])
| hd::tl -> let (l,tl) = list_sep_last tl in (l,hd::tl)
-let list_try_find_i f =
+let list_try_find_i f =
let rec try_find_f n = function
| [] -> failwith "try_find_i"
| h::t -> try f n h with Failure _ -> try_find_f (n+1) t
- in
+ in
try_find_f
-let list_try_find f =
+let list_try_find f =
let rec try_find_f = function
| [] -> failwith "try_find"
| h::t -> try f h with Failure _ -> try_find_f t
- in
+ in
try_find_f
let list_uniquize l =
@@ -739,12 +739,12 @@ let list_uniquize l =
| [] -> List.rev acc
in aux [] l
-let rec list_distinct l =
+let rec list_distinct l =
let visited = Hashtbl.create 23 in
let rec loop = function
| h::t ->
if Hashtbl.mem visited h then false
- else
+ else
begin
Hashtbl.add visited h h;
loop t
@@ -757,10 +757,10 @@ let rec list_merge_uniq cmp l1 l2 =
| [], l2 -> l2
| l1, [] -> l1
| h1 :: t1, h2 :: t2 ->
- let c = cmp h1 h2 in
- if c = 0
+ let c = cmp h1 h2 in
+ if c = 0
then h1 :: list_merge_uniq cmp t1 t2
- else if c <= 0
+ else if c <= 0
then h1 :: list_merge_uniq cmp t1 l2
else h2 :: list_merge_uniq cmp l1 t2
@@ -789,13 +789,13 @@ let list_subset l1 l2 =
let rec look = function
| [] -> true
| x::ll -> try Hashtbl.find t2 x; look ll with Not_found -> false
- in
+ in
look l1
-(* [list_split_at i l] splits [l] into two lists [(l1,l2)] such that [l1++l2=l]
+(* [list_split_at i l] splits [l] into two lists [(l1,l2)] such that [l1++l2=l]
and [l1] has length [i].
It raises [Failure] when [i] is negative or greater than the length of [l] *)
-let list_split_at index l =
+let list_split_at index l =
let rec aux i acc = function
tl when i = index -> (List.rev acc), tl
| hd :: tl -> aux (succ i) (hd :: acc) tl
@@ -805,12 +805,12 @@ let list_split_at index l =
(* [list_split_when p l] splits [l] into two lists [(l1,a::l2)] such that
[l1++(a::l2)=l], [p a=true] and [p b = false] for every element [b] of [l1].
If there is no such [a], then it returns [(l,[])] instead *)
-let list_split_when p =
- let rec split_when_loop x y =
- match y with
+let list_split_when p =
+ let rec split_when_loop x y =
+ match y with
| [] -> ([],[])
| (a::l) -> if (p a) then (List.rev x,y) else split_when_loop (a::x) l
- in
+ in
split_when_loop []
let rec list_split3 = function
@@ -831,7 +831,7 @@ let list_firstn n l =
| (0, l) -> List.rev acc
| (n, (h::t)) -> aux (h::acc) (pred n, t)
| _ -> failwith "firstn"
- in
+ in
aux [] (n,l)
let rec list_last = function
@@ -846,20 +846,20 @@ let list_lastn n l =
in
if len < n then failwith "lastn" else aux len l
-let rec list_skipn n l = match n,l with
- | 0, _ -> l
+let rec list_skipn n l = match n,l with
+ | 0, _ -> l
| _, [] -> failwith "list_fromn"
| n, _::l -> list_skipn (pred n) l
-let rec list_addn n x l =
+let rec list_addn n x l =
if n = 0 then l else x :: (list_addn (pred n) x l)
-let list_prefix_of prefl l =
+let list_prefix_of prefl l =
let rec prefrec = function
| (h1::t1, h2::t2) -> h1 = h2 && prefrec (t1,t2)
| ([], _) -> true
| (_, _) -> false
- in
+ in
prefrec (prefl,l)
let list_drop_prefix p l =
@@ -867,7 +867,7 @@ let list_drop_prefix p l =
let rec list_drop_prefix_rec = function
| ([], tl) -> Some tl
| (_, []) -> None
- | (h1::tp, h2::tl) ->
+ | (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
@@ -883,7 +883,7 @@ let list_share_tails l1 l2 =
let rec shr_rev acc = function
| ((x1::l1), (x2::l2)) when x1 == x2 -> shr_rev (x1::acc) (l1,l2)
| (l1,l2) -> (List.rev l1, List.rev l2, acc)
- in
+ in
shr_rev [] (List.rev l1, List.rev l2)
let rec list_fold_map f e = function
@@ -894,10 +894,10 @@ let rec list_fold_map f e = function
e'',h'::t'
(* (* tail-recursive version of the above function *)
-let list_fold_map f e l =
- let g (e,b') h =
+let list_fold_map f e l =
+ let g (e,b') h =
let (e',h') = f e h in
- (e',h'::b')
+ (e',h'::b')
in
let (e',lrev) = List.fold_left g (e,[]) l in
(e',List.rev lrev)
@@ -921,17 +921,17 @@ let list_union_map f l acc =
acc
l
-(* A generic cartesian product: for any operator (**),
- [list_cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]],
+(* A generic cartesian product: for any operator (**),
+ [list_cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]],
and so on if there are more elements in the lists. *)
-let rec list_cartesian op l1 l2 =
+let rec list_cartesian op l1 l2 =
list_map_append (fun x -> List.map (op x) l2) l1
-(* [list_cartesians] is an n-ary cartesian product: it iterates
+(* [list_cartesians] is an n-ary cartesian product: it iterates
[list_cartesian] over a list of lists. *)
-let list_cartesians op init ll =
+let list_cartesians op init ll =
List.fold_right (list_cartesian op) ll [init]
(* list_combinations [[a;b];[c;d]] gives [[a;c];[a;d];[b;c];[b;d]] *)
@@ -940,12 +940,12 @@ let list_combinations l = list_cartesians (fun x l -> x::l) [] l
(* Keep only those products that do not return None *)
-let rec list_cartesian_filter op l1 l2 =
+let rec list_cartesian_filter op l1 l2 =
list_map_append (fun x -> list_map_filter (op x) l2) l1
(* Keep only those products that do not return None *)
-let rec list_cartesians_filter op init ll =
+let rec list_cartesians_filter op init ll =
List.fold_right (list_cartesian_filter op) ll [init]
(* Drop the last element of a list *)
@@ -961,61 +961,61 @@ let array_compare item_cmp v1 v2 =
-1 -> 0
| i ->
let c' = item_cmp v1.(i) v2.(i) in
- if c'<>0 then c'
+ if c'<>0 then c'
else cmp (i-1) in
cmp (Array.length v1 - 1)
-let array_exists f v =
+let array_exists f v =
let rec exrec = function
| -1 -> false
| n -> (f v.(n)) || (exrec (n-1))
- in
- exrec ((Array.length v)-1)
+ in
+ exrec ((Array.length v)-1)
-let array_for_all f v =
+let array_for_all f v =
let rec allrec = function
| -1 -> true
| n -> (f v.(n)) && (allrec (n-1))
- in
- allrec ((Array.length v)-1)
+ in
+ allrec ((Array.length v)-1)
let array_for_all2 f v1 v2 =
let rec allrec = function
| -1 -> true
| n -> (f v1.(n) v2.(n)) && (allrec (n-1))
- in
+ in
let lv1 = Array.length v1 in
- lv1 = Array.length v2 && allrec (pred lv1)
+ lv1 = Array.length v2 && allrec (pred lv1)
let array_for_all3 f v1 v2 v3 =
let rec allrec = function
| -1 -> true
| n -> (f v1.(n) v2.(n) v3.(n)) && (allrec (n-1))
- in
+ in
let lv1 = Array.length v1 in
- lv1 = Array.length v2 && lv1 = Array.length v3 && allrec (pred lv1)
+ lv1 = Array.length v2 && lv1 = Array.length v3 && allrec (pred lv1)
let array_for_all4 f v1 v2 v3 v4 =
let rec allrec = function
| -1 -> true
| n -> (f v1.(n) v2.(n) v3.(n) v4.(n)) && (allrec (n-1))
- in
+ in
let lv1 = Array.length v1 in
lv1 = Array.length v2 &&
lv1 = Array.length v3 &&
lv1 = Array.length v4 &&
- allrec (pred lv1)
+ allrec (pred lv1)
-let array_for_all_i f i v =
- let rec allrec i n = n = Array.length v || f i v.(n) && allrec (i+1) (n+1) in
+let array_for_all_i f i v =
+ let rec allrec i n = n = Array.length v || f i v.(n) && allrec (i+1) (n+1) in
allrec i 0
-let array_hd v =
+let array_hd v =
match Array.length v with
| 0 -> failwith "array_hd"
| _ -> v.(0)
-let array_tl v =
+let array_tl v =
match Array.length v with
| 0 -> failwith "array_tl"
| n -> Array.sub v 1 (pred n)
@@ -1027,12 +1027,12 @@ let array_last v =
let array_cons e v = Array.append [|e|] v
-let array_rev t =
+let array_rev t =
let n=Array.length t in
- if n <=0 then ()
+ if n <=0 then ()
else
let tmp=ref t.(0) in
- for i=0 to pred (n/2) do
+ for i=0 to pred (n/2) do
tmp:=t.((pred n)-i);
t.((pred n)-i)<- t.(i);
t.(i)<- !tmp
@@ -1063,7 +1063,7 @@ let array_fold_right2 f v1 v2 a =
let array_fold_left2 f a v1 v2 =
let lv1 = Array.length v1 in
- let rec fold a n =
+ let rec fold a n =
if n >= lv1 then a else fold (f a v1.(n) v2.(n)) (succ n)
in
if Array.length v2 <> lv1 then invalid_arg "array_fold_left2";
@@ -1071,25 +1071,25 @@ let array_fold_left2 f a v1 v2 =
let array_fold_left2_i f a v1 v2 =
let lv1 = Array.length v1 in
- let rec fold a n =
+ let rec fold a n =
if n >= lv1 then a else fold (f n a v1.(n) v2.(n)) (succ n)
in
if Array.length v2 <> lv1 then invalid_arg "array_fold_left2";
fold a 0
-let array_fold_left_from n f a v =
+let array_fold_left_from n f a v =
let rec fold a n =
if n >= Array.length v then a else fold (f a v.(n)) (succ n)
- in
+ in
fold a n
-let array_fold_right_from n f v a =
+let array_fold_right_from n f v a =
let rec fold n =
if n >= Array.length v then a else f v.(n) (fold (succ n))
- in
+ in
fold n
-let array_app_tl v l =
+let array_app_tl v l =
if Array.length v = 0 then invalid_arg "array_app_tl";
array_fold_right_from 1 (fun e l -> e::l) v l
@@ -1109,9 +1109,9 @@ exception Local of int
(* If none of the elements is changed by f we return ar itself.
The for loop looks for the first such an element.
- If found it is temporarily stored in a ref and the new array is produced,
+ If found it is temporarily stored in a ref and the new array is produced,
but f is not re-applied to elements that are already checked *)
-let array_smartmap f ar =
+let array_smartmap f ar =
let ar_size = Array.length ar in
let aux = ref None in
try
@@ -1125,10 +1125,10 @@ let array_smartmap f ar =
done;
ar
with
- Local i ->
- let copy j =
- if j<i then ar.(j)
- else if j=i then
+ Local i ->
+ let copy j =
+ if j<i then ar.(j)
+ else if j=i then
match !aux with Some a' -> a' | None -> failwith "Error"
else f (ar.(j))
in
@@ -1136,8 +1136,8 @@ let array_smartmap f ar =
let array_map2 f v1 v2 =
if Array.length v1 <> Array.length v2 then invalid_arg "array_map2";
- if Array.length v1 == 0 then
- [| |]
+ if Array.length v1 == 0 then
+ [| |]
else begin
let res = Array.create (Array.length v1) (f v1.(0) v2.(0)) in
for i = 1 to pred (Array.length v1) do
@@ -1148,8 +1148,8 @@ let array_map2 f v1 v2 =
let array_map2_i f v1 v2 =
if Array.length v1 <> Array.length v2 then invalid_arg "array_map2";
- if Array.length v1 == 0 then
- [| |]
+ if Array.length v1 == 0 then
+ [| |]
else begin
let res = Array.create (Array.length v1) (f 0 v1.(0) v2.(0)) in
for i = 1 to pred (Array.length v1) do
@@ -1161,8 +1161,8 @@ let array_map2_i f v1 v2 =
let array_map3 f v1 v2 v3 =
if Array.length v1 <> Array.length v2 ||
Array.length v1 <> Array.length v3 then invalid_arg "array_map3";
- if Array.length v1 == 0 then
- [| |]
+ if Array.length v1 == 0 then
+ [| |]
else begin
let res = Array.create (Array.length v1) (f v1.(0) v2.(0) v3.(0)) in
for i = 1 to pred (Array.length v1) do
@@ -1203,7 +1203,7 @@ let pure_functional = false
let array_fold_map' f v e =
if pure_functional then
let (l,e) =
- Array.fold_right
+ 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)
@@ -1219,8 +1219,8 @@ let array_fold_map f e v =
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
+ let v' =
+ array_map2 (fun x1 x2 -> let (y,e) = f x1 x2 !e' in e' := e; y) v1 v2
in
(v',!e')
@@ -1253,10 +1253,10 @@ let identity x = x
let compose f g x = f (g x)
-let iterate f =
+let iterate f =
let rec iterate_f n x =
if n <= 0 then x else iterate_f (pred n) (f x)
- in
+ in
iterate_f
let repeat n f x =
@@ -1265,7 +1265,7 @@ let repeat n f x =
let iterate_for a b f x =
let rec iterate i v = if i > b then v else iterate (succ i) (f i v) in
iterate a x
-
+
(* Misc *)
type ('a,'b) union = Inl of 'a | Inr of 'b
@@ -1281,22 +1281,22 @@ let intmap_to_list m = Intmap.fold (fun n v l -> (n,v)::l) m []
let intmap_inv m b = Intmap.fold (fun n v l -> if v = b then n::l else l) m []
-let interval n m =
+let interval n m =
let rec interval_n (l,m) =
if n > m then l else interval_n (m::l,pred m)
- in
+ in
interval_n ([],m)
-let map_succeed f =
- let rec map_f = function
+let map_succeed f =
+ let rec map_f = function
| [] -> []
| h::t -> try (let x = f h in x :: map_f t) with Failure _ -> map_f t
- in
- map_f
+ in
+ map_f
(* Pretty-printing *)
-
+
let pr_spc = spc
let pr_fnl = fnl
let pr_int = int
@@ -1312,7 +1312,7 @@ let nth n = str (ordinal n)
(* [prlist pr [a ; ... ; c]] outputs [pr a ++ ... ++ pr c] *)
-let rec prlist elem l = match l with
+let rec prlist elem l = match l with
| [] -> mt ()
| h::t -> Stream.lapp (fun () -> elem h) (prlist elem t)
@@ -1320,7 +1320,7 @@ let rec prlist elem l = match l with
if a strict behavior is needed, use [prlist_strict] instead.
evaluation is done from left to right. *)
-let rec prlist_strict elem l = match l with
+let rec prlist_strict elem l = match l with
| [] -> mt ()
| h::t ->
let e = elem h in let r = prlist_strict elem t in e++r
@@ -1344,7 +1344,7 @@ let rec pr_sequence elem = function
let e = elem h and r = pr_sequence elem t in
if e = mt () then r else e ++ spc () ++ r
-(* [pr_enum pr [a ; b ; ... ; c]] outputs
+(* [pr_enum pr [a ; b ; ... ; c]] outputs
[pr a ++ str "," ++ pr b ++ str "," ++ ... ++ str "and" ++ pr c] *)
let pr_enum pr l =
@@ -1355,11 +1355,11 @@ let pr_enum pr l =
let pr_vertical_list pr = function
| [] -> str "none" ++ fnl ()
| l -> fnl () ++ str " " ++ hov 0 (prlist_with_sep pr_fnl pr l) ++ fnl ()
-
+
let prvecti elem v =
let n = Array.length v in
let rec pr i =
- if i = 0 then
+ if i = 0 then
elem 0 v.(0)
else
let r = pr (i-1) and e = elem i v.(i) in r ++ e
@@ -1371,10 +1371,10 @@ let prvecti elem v =
let prvect_with_sep sep elem v =
let rec pr n =
- if n = 0 then
+ if n = 0 then
elem v.(0)
- else
- let r = pr (n-1) and s = sep() and e = elem v.(n) in
+ else
+ let r = pr (n-1) and s = sep() and e = elem v.(n) in
r ++ s ++ e
in
let n = Array.length v in
@@ -1428,34 +1428,34 @@ let memon_eq eq n f =
(*s Size of ocaml values. *)
module Size = struct
-
+
open Obj
(*s Pointers already visited are stored in a hash-table, where
comparisons are done using physical equality. *)
module H = Hashtbl.Make(
- struct
- type t = Obj.t
- let equal = (==)
+ struct
+ type t = Obj.t
+ let equal = (==)
let hash o = Hashtbl.hash (magic o : int)
end)
-
+
let node_table = (H.create 257 : unit H.t)
-
+
let in_table o = try H.find node_table o; true with Not_found -> false
-
+
let add_in_table o = H.add node_table o ()
-
+
let reset_table () = H.clear node_table
-
+
(*s Objects are traversed recursively, as soon as their tags are less than
[no_scan_tag]. [count] records the numbers of words already visited. *)
let size_of_double = size (repr 1.0)
-
+
let count = ref 0
-
+
let rec traverse t =
if not (in_table t) then begin
add_in_table t;
@@ -1465,20 +1465,20 @@ module Size = struct
if tag < no_scan_tag then begin
count := !count + 1 + n;
for i = 0 to n - 1 do
- let f = field t i in
+ let f = field t i in
if is_block f then traverse f
done
end else if tag = string_tag then
- count := !count + 1 + n
+ count := !count + 1 + n
else if tag = double_tag then
count := !count + size_of_double
else if tag = double_array_tag then
- count := !count + 1 + size_of_double * n
+ count := !count + 1 + size_of_double * n
else
incr count
end
end
-
+
(*s Sizes of objects in words and in bytes. The size in bytes is computed
system-independently according to [Sys.word_size]. *)
@@ -1511,6 +1511,6 @@ let heap_size_kb () = (heap_size () + 1023) / 1024
(*s interruption *)
let interrupt = ref false
-let check_for_interrupt () =
+let check_for_interrupt () =
if !interrupt then begin interrupt := false; raise Sys.Break end
diff --git a/lib/util.mli b/lib/util.mli
index 5e32a1b0ea..4579982bcf 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -128,7 +128,7 @@ val list_map_filter : ('a -> 'b option) -> 'a list -> 'b list
val list_smartmap : ('a -> 'a) -> 'a list -> 'a list
val list_map_left : ('a -> 'b) -> 'a list -> 'b list
val list_map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
-val list_map2_i :
+val list_map2_i :
(int -> 'a -> 'b -> 'c) -> int -> 'a list -> 'b list -> 'c list
val list_map3 :
('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
@@ -139,7 +139,7 @@ val list_filter_i :
(* [list_index] returns the 1st index of an element in a list (counting from 1) *)
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_unique_index : 'a -> 'a list -> int
(* [list_index0] behaves as [list_index] except that it starts counting at 0 *)
val list_index0 : 'a -> 'a list -> int
val list_iter3 : ('a -> 'b -> 'c -> unit) -> 'a list -> 'b list -> 'c list -> unit
@@ -169,7 +169,7 @@ val list_partition_by : ('a -> 'a -> bool) -> 'a list -> 'a list list
val list_firstn : int -> 'a list -> 'a list
val list_last : 'a list -> 'a
val list_lastn : int -> 'a list -> 'a list
-val list_skipn : int -> 'a list -> 'a list
+val list_skipn : int -> 'a list -> 'a list
val list_addn : int -> 'a -> 'a list -> 'a list
val list_prefix_of : 'a list -> 'a list -> bool
(* [list_drop_prefix p l] returns [t] if [l=p++t] else return [l] *)
@@ -186,11 +186,11 @@ val list_share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a 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
-(* A generic cartesian product: for any operator (**),
- [list_cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]],
+(* A generic cartesian product: for any operator (**),
+ [list_cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]],
and so on if there are more elements in the lists. *)
val list_cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
-(* [list_cartesians] is an n-ary cartesian product: it iterates
+(* [list_cartesians] is an n-ary cartesian product: it iterates
[list_cartesian] over a list of lists. *)
val list_cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
(* list_combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *)
@@ -219,14 +219,14 @@ 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 :
+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
val array_fold_right2 :
('a -> 'b -> 'c -> 'c) -> 'a array -> 'b array -> 'c -> 'c
-val array_fold_left2 :
+val array_fold_left2 :
('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a
-val array_fold_left2_i :
+val array_fold_left2_i :
(int -> 'a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a
val array_fold_left_from : int -> ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a
val array_fold_right_from : int -> ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
@@ -237,7 +237,7 @@ val array_chop : int -> 'a array -> 'a array * 'a array
val array_smartmap : ('a -> 'a) -> 'a array -> 'a array
val array_map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
val array_map2_i : (int -> 'a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
-val array_map3 :
+val array_map3 :
('a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array
val array_map_left : ('a -> 'b) -> 'a array -> 'b array
val array_map_left_pair : ('a -> 'b) -> 'a array -> ('c -> 'd) -> 'c array ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:45:00 +0000