modules profile, Coqinit et Coqtop (=main)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@194 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 378 insertions, 11 deletions

diff --git a/lib/profile.ml b/lib/profile.ml
new file mode 100644
index 000000000..3e1d04607
--- /dev/null
+++ b/lib/profile.ml
@@ -0,0 +1,311 @@
+
+(* $Id$ *)
+
+(* This program is a small time-profiler for Caml-Special-Light *)
+
+(* It requires the UNIX library *)
+
+(* Adapted from Christophe Raffalli *)
+
+(* To use it, link it with the program you want to profile (don not forget
+"-cclib -lunix -custom unix.cma" among the link options).
+
+To trace a function "f" you first need to get a key for it by using :
+
+let fkey = declare_profile "f"
+
+(the string is used to print the profile infomation). Warning: this
+function does a side effect. Choose the ident you want instead "fkey".
+
+Then if the function has one ONE argument add the following just after
+the definition of "f" or just after the declare_profile if this one
+follows the defintion of f.
+
+let f = profile fkey f
+
+If f has two arguments do the same with profile2, idem with 3 and
+4. For more than 4 arguments ... modify the function profile yourself,
+it is very easy (look the differences between profile and profile2.
+
+If you want to profile two mutually recursive functions, you had better
+to rename them :
+
+let fkey = declare_profile "f"
+let gkey = declare_profile "g"
+let f' = .... f' ... g'
+and g' = .... f' .... g'
+
+
+let f = profile fkey f'
+let g = profile gkey g'
+
+Before the program quits, you should call "print_profile ()". It
+produces a result of the following kind:
+
+f 5.32 7.10
+g 4.00 4.00
+main 0.12 9.44
+total -9.44 0.00
+
+- The first column is the name of the function.
+
+- The third column give the time (utime + stime) spend inside the function.
+
+- The second column give the time spend inside the function minus the
+time spend in other profiled functions called by it
+
+The last line can be ignored (there is a bug if the down-right digit is non
+zero)
+
+*)
+
+type profile_key = float ref * float ref
+
+let actif = ref true
+
+let tot_ptr = ref 0.0 and tot_ptr' = ref 0.0
+
+let prof_table = ref ["total",(tot_ptr,tot_ptr')]
+
+let stack = ref [tot_ptr']
+
+let ajoute ((name,(ptr1,ptr1')) as e) l =
+  try let (ptr,ptr') = List.assoc name l in
+  ptr  := !ptr  +. !ptr1;
+  ptr' := !ptr' +. !ptr1';
+  l
+  with Not_found -> e::l
+
+
+let magic = 1248
+
+let append_profile name =
+  if List.length !prof_table <> 1 then begin
+    let prof_table =
+      if name = "" then !prof_table
+      else
+	let new_prof_table =
+          try 
+            let c = open_in name in
+            if input_binary_int c <> magic 
+            then Printf.printf "Bad already existing recording file\n";
+            let old_prof_table = input_value c in
+            close_in c;
+            List.fold_right ajoute !prof_table old_prof_table
+          with Sys_error _ ->
+            (Printf.printf "Non existent or unaccessible recording file\n";
+             !prof_table)
+	in begin
+          (try
+             let c = open_out_gen 
+                       [Open_creat;Open_wronly;Open_trunc;Open_binary] 0o644 name in
+             output_binary_int c magic;
+             output_value c new_prof_table;
+             close_out c
+           with Sys_error _ -> Printf.printf "Unable to create recording file");
+            new_prof_table
+	  end
+    in
+    print_newline ();
+    Printf.printf "%-25s  %11s  %11s\n" 
+      "Function name" "Proper time" "Total time";
+    let l = Sort.list (fun (_,(_,p)) (_,(_,p')) -> !p > !p') prof_table in
+    List.iter (fun (name,(ptr,ptr')) ->
+		 Printf.printf "%-25s  %11.2f  %11.2f\n" name !ptr' !ptr) l;
+    Gc.print_stat stdout
+  end
+
+
+let recording_file = ref ""
+let set_recording s = recording_file := s
+
+let print_profile () = append_profile !recording_file
+
+let reset_profile () = 
+  List.iter (fun (name,(p,p')) -> p:=0.0; p':=0.0) !prof_table
+
+let init_profile () = 
+  tot_ptr:= 0.0; tot_ptr':=0.0; prof_table :=["total",(tot_ptr,tot_ptr')] 
+
+let declare_profile name = let ptr = ref 0.0 and ptr' = ref 0.0 in
+prof_table := (name,(ptr,ptr'))::!prof_table;(ptr,ptr')
+
+let profile (ptr,ptr') f =
+  (fun x ->
+     let (ut,st) = System.process_time () in
+     stack := ptr'::!stack;
+     try
+       let r = f x in
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       r
+     with e ->
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       raise e)
+
+
+
+let profile2 (ptr,ptr') f =
+  (fun x y ->
+     let (ut,st) = System.process_time () in
+     stack := ptr'::!stack;
+     try
+       let r = f x y in
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       r
+     with e ->
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       raise e)
+
+
+
+let profile3 (ptr,ptr') f =
+  (fun x y z ->
+     let (ut,st) = System.process_time () in
+     stack := ptr'::!stack;
+     try
+       let r = f x y z in
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       r
+     with e ->
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       raise e)
+
+
+
+let profile4 (ptr,ptr') f =
+  (fun x y z t ->
+     let (ut,st) = System.process_time () in
+     stack := ptr'::!stack;
+     try
+       let r = f x y z t in
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       r
+     with e ->
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       raise e)
+
+
+
+let profile5 (ptr,ptr') f =
+  (fun x y z t u ->
+     let (ut,st) = System.process_time () in
+     stack := ptr'::!stack;
+     try
+       let r = f x y z t u in
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       r
+     with e ->
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       raise e)
+
+
+
+let profile6 (ptr,ptr') f =
+  (fun x y z t u v ->
+     let (ut,st) = System.process_time () in
+     stack := ptr'::!stack;
+     try
+       let r = f x y z t u v in
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       r
+     with e ->
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       raise e)
+
+
+
+let profile7 (ptr,ptr') f =
+  (fun x y z t u v w ->
+     let (ut,st) = System.process_time () in
+     stack := ptr'::!stack;
+     try
+       let r = f x y z t u v w in
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       r
+     with e ->
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       raise e)
diff --git a/lib/profile.mli b/lib/profile.mli
new file mode 100644
index 000000000..893bf07b9
--- /dev/null
+++ b/lib/profile.mli
@@ -0,0 +1,29 @@
+
+(* $Id$ *)
+
+(* Profiling. *)
+
+type profile_key
+
+val actif : bool ref
+val print_profile : unit -> unit
+val reset_profile : unit -> unit
+val init_profile : unit -> unit
+val declare_profile : string -> profile_key
+val profile : profile_key -> ('a -> 'b) -> 'a -> 'b
+val profile2 : profile_key -> ('a -> 'b -> 'c) -> 'a -> 'b -> 'c
+val profile3 :
+  profile_key -> ('a -> 'b -> 'c -> 'd) -> 'a -> 'b -> 'c -> 'd
+val profile4 :
+  profile_key -> ('a -> 'b -> 'c -> 'd -> 'e) -> 'a -> 'b -> 'c -> 'd -> 'e
+val profile5 :
+  profile_key ->
+  ('a -> 'b -> 'c -> 'd -> 'e -> 'f) -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f
+val profile6 :
+  profile_key ->
+  ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g)
+    -> '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
diff --git a/lib/system.ml b/lib/system.ml
index 9da302d30..5422bc465 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -44,7 +44,14 @@ let all_subdirs dir =
 
 let radd_path dir = List.iter add_path (all_subdirs dir)
 
+let safe_getenv_def var def =
+  try 
+    Sys.getenv var
+  with Not_found ->
+    warning ("Environnement variable "^var^" not found: using '"^def^"' .");
+    def
 
+let home = (safe_getenv_def "HOME" ".")
 
 (* TODO: rétablir glob (expansion ~user et $VAR) si on le juge nécessaire *)
 let glob s = s
@@ -82,6 +89,9 @@ let is_in_path lpath filename =
 let make_suffix name suffix =
   if Filename.check_suffix name suffix then name else (name ^ suffix)
 
+let file_readable_p na =
+  try access (glob na) [R_OK];true with Unix_error (_, _, _) -> false
+
 let open_trapping_failure open_fun name suffix =
   let rname = make_suffix name suffix in
   try open_fun rname with _ -> error ("Can't open " ^ rname)
@@ -141,11 +151,22 @@ let (extern_intern :
 
 (* Time stamps. *)
 
-type time_stamp = float
-
-let get_time_stamp () = Unix.time()
-
-let compare_time_stamps t1 t2 =
-  let dt = t2 -. t1 in
-  if dt < 0.0 then -1 else if dt = 0.0 then 0 else 1
-
+type time = float * float * float
+
+let process_time () = 
+  let t = times ()  in
+  (t.tms_utime, t.tms_stime)
+
+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"(";
+     'rEAL((-.) ustop ustart); 'sTR"u";
+     'sTR",";
+     'rEAL((-.) sstop sstart); 'sTR"s";
+     'sTR")" >]
diff --git a/lib/system.mli b/lib/system.mli
index 0c4bbd228..e3fd5978c 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -8,9 +8,12 @@ val is_in_path : string list -> string -> bool
 val where_in_path : string list -> string -> string
 
 val make_suffix : string -> string -> string
+val file_readable_p : string -> bool
 
 val glob : string -> string
 
+val home : string
+
 (*s Global load path. *)
 
 val add_path : string -> unit
@@ -34,8 +37,11 @@ val extern_intern : int -> string -> (string -> 'a -> unit) * (string -> 'a)
 
 (*s Time stamps. *)
 
-type time_stamp
+type time
+
+val process_time : unit -> float * float
+val get_time : unit -> time
+val time_difference : time -> time -> float (* in seconds *)
+val fmt_time_difference : time -> time -> Pp.std_ppcmds
 
-val get_time_stamp : unit -> time_stamp
-val compare_time_stamps : time_stamp -> time_stamp -> int