X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicUtil.ml;h=07f39896c3050396c9e72a194c88931cfe3d7158;hb=51d82e0a8a4d4ed86d2646edb2654e565ac34a82;hp=d3fcffd8039235c101bd850492d7a7b55c4be082;hpb=f85e6f52232af229b80a8447492cfae80f95d832;p=helm.git diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml index d3fcffd80..07f39896c 100644 --- a/helm/ocaml/cic/cicUtil.ml +++ b/helm/ocaml/cic/cicUtil.ml @@ -209,18 +209,43 @@ let rec mk_rels howmany from = | 0 -> [] | _ -> (Cic.Rel (howmany + from)) :: (mk_rels (howmany-1) from) +let profiling_enabled = false + +type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b } 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 = profile } + else + function _ -> { profile = 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