]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic/cicUtil.ml
fixed a finalization issue for connections closed twice
[helm.git] / helm / ocaml / cic / cicUtil.ml
index d3fcffd8039235c101bd850492d7a7b55c4be082..aa1ed1ba0ec745e30d169dba355703127e7c9629 100644 (file)
@@ -209,18 +209,42 @@ let rec mk_rels howmany from =
   | 0 -> []
   | _ -> (Cic.Rel (howmany + from)) :: (mk_rels (howmany-1) from)
 
+let profiling_enabled = false
+
 let profile =
- function s ->
-  let total = ref 0.0 in
-  let profile f x =
-   let before = Unix.gettimeofday () in
-   let res = f x in
-   let after = Unix.gettimeofday () in
-    total := !total +. (after -. before);
-    res
-  in
-  at_exit
-   (fun () ->
-     print_endline
-      ("!! TOTAL TIME SPENT IN " ^ s ^ ": " ^ string_of_float !total));
-  profile
+ if profiling_enabled then
+  function s ->
+   let total = ref 0.0 in
+   let profile f x =
+    let before = Unix.gettimeofday () in
+    let res = f x in
+    let after = Unix.gettimeofday () in
+     total := !total +. (after -. before);
+     res
+   in
+   at_exit
+    (fun () ->
+      print_endline
+       ("!! TOTAL TIME SPENT IN " ^ s ^ ": " ^ string_of_float !total));
+   profile
+ else
+  function _ -> fun f x -> f x
+
+let id_of_annterm =
+  function
+  | Cic.ARel (id,_,_,_)
+  | Cic.AVar (id,_,_)
+  | Cic.AMeta (id,_,_)
+  | Cic.ASort (id,_)
+  | Cic.AImplicit (id,_)
+  | Cic.ACast (id,_,_)
+  | Cic.AProd (id,_,_,_)
+  | Cic.ALambda (id,_,_,_)
+  | Cic.ALetIn (id,_,_,_)
+  | Cic.AAppl (id,_)
+  | Cic.AConst (id,_,_)
+  | Cic.AMutInd (id,_,_,_)
+  | Cic.AMutConstruct (id,_,_,_,_)
+  | Cic.AMutCase (id,_,_,_,_,_)
+  | Cic.AFix (id,_,_)
+  | Cic.ACoFix (id,_,_) -> id