(Inference.string_of_equality e))
res));
print_endline "|";
-;;
+;;
+
+
+let indexing_retrieval_time = ref 0.;;
let empty_table () =
and in_index = Path_indexing.in_index;;
let get_candidates mode trie term =
- let s =
- match mode with
- | Matching -> Path_indexing.retrieve_generalizations trie term
- | Unification -> Path_indexing.retrieve_unifiables trie term
+ let t1 = Unix.gettimeofday () in
+ let res =
+ let s =
+ match mode with
+ | Matching -> Path_indexing.retrieve_generalizations trie term
+ | Unification -> Path_indexing.retrieve_unifiables trie term
+(* Path_indexing.retrieve_all trie term *)
+ in
+ Path_indexing.PosEqSet.elements s
in
- Path_indexing.PosEqSet.elements s
+(* print_candidates mode term res; *)
+ let t2 = Unix.gettimeofday () in
+ indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
+ res
;;
;;
*)
+let match_unif_time_ok = ref 0.;;
+let match_unif_time_no = ref 0.;;
+
let rec find_matches metasenv context ugraph lift_amount term =
let module C = Cic in
let pos, (proof, (ty, left, right, o), metas, args) = candidate in
let do_match c other eq_URI =
let subst', metasenv', ugraph' =
- Inference.matching (metasenv @ metas) context
- term (S.lift lift_amount c) ugraph
+ let t1 = Unix.gettimeofday () in
+ try
+ let r =
+ Inference.matching (metasenv @ metas) context
+ term (S.lift lift_amount c) ugraph in
+ let t2 = Unix.gettimeofday () in
+ match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
+ r
+ with e ->
+ let t2 = Unix.gettimeofday () in
+ match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
+ raise e
in
- Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
- (candidate, eq_URI))
+ Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
+ (candidate, eq_URI))
in
let c, other, eq_URI =
if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI
let pos, (proof, (ty, left, right, o), metas, args) = candidate in
let do_match c other eq_URI =
let subst', metasenv', ugraph' =
- unif_fun (metasenv @ metas) context
- term (S.lift lift_amount c) ugraph
+ let t1 = Unix.gettimeofday () in
+ try
+ let r =
+ unif_fun (metasenv @ metas) context
+ term (S.lift lift_amount c) ugraph in
+ let t2 = Unix.gettimeofday () in
+ match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
+ r
+ with e ->
+ let t2 = Unix.gettimeofday () in
+ match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
+ raise e
in
(C.Rel (1 + lift_amount), subst', metasenv', ugraph',
(candidate, eq_URI))
try
let other = if pos = Utils.Left then r else l in
let subst', menv', ug' =
- Inference.matching metasenv context what other ugraph in
+ let t1 = Unix.gettimeofday () in
+ try
+ let r =
+ Inference.matching metasenv context what other ugraph in
+ let t2 = Unix.gettimeofday () in
+ match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
+ r
+ with e ->
+ let t2 = Unix.gettimeofday () in
+ match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
+ raise e
+ in
samesubst subst subst'
with e ->
false