diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/bigint.ml | 26 | ||||
| -rw-r--r-- | lib/bstack.ml | 6 | ||||
| -rw-r--r-- | lib/compat.ml4 | 8 | ||||
| -rw-r--r-- | lib/dnet.ml | 58 | ||||
| -rw-r--r-- | lib/dnet.mli | 18 | ||||
| -rw-r--r-- | lib/dyn.ml | 2 | ||||
| -rw-r--r-- | lib/edit.ml | 16 | ||||
| -rw-r--r-- | lib/envars.ml | 50 | ||||
| -rw-r--r-- | lib/explore.ml | 18 | ||||
| -rw-r--r-- | lib/explore.mli | 8 | ||||
| -rw-r--r-- | lib/flags.ml | 4 | ||||
| -rw-r--r-- | lib/gmapl.ml | 2 | ||||
| -rw-r--r-- | lib/hashcons.ml | 6 | ||||
| -rw-r--r-- | lib/heap.ml | 54 | ||||
| -rw-r--r-- | lib/heap.mli | 20 | ||||
| -rw-r--r-- | lib/lib.mllib | 12 | ||||
| -rw-r--r-- | lib/option.ml | 28 | ||||
| -rw-r--r-- | lib/option.mli | 14 | ||||
| -rw-r--r-- | lib/pp.ml4 | 22 | ||||
| -rw-r--r-- | lib/pp.mli | 2 | ||||
| -rw-r--r-- | lib/pp_control.ml | 14 | ||||
| -rw-r--r-- | lib/pp_control.mli | 4 | ||||
| -rw-r--r-- | lib/predicate.ml | 2 | ||||
| -rw-r--r-- | lib/profile.ml | 54 | ||||
| -rw-r--r-- | lib/profile.mli | 6 | ||||
| -rw-r--r-- | lib/refutpat.ml4 | 2 | ||||
| -rw-r--r-- | lib/rtree.ml | 12 | ||||
| -rw-r--r-- | lib/rtree.mli | 4 | ||||
| -rw-r--r-- | lib/system.ml | 60 | ||||
| -rw-r--r-- | lib/system.mli | 8 | ||||
| -rw-r--r-- | lib/tlm.ml | 26 | ||||
| -rw-r--r-- | lib/util.ml | 340 | ||||
| -rw-r--r-- | lib/util.mli | 20 |
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 -> |