| 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