-let head_of_term = function
- | Cic.Appl (hd::tl) -> hd
- | t -> t
+type retrieval_mode = Matching | Unification;;
+
+
+let print_candidates mode term res =
+ let _ =
+ match mode with
+ | Matching ->
+ Printf.printf "| candidates Matching %s\n" (CicPp.ppterm term)
+ | Unification ->
+ Printf.printf "| candidates Unification %s\n" (CicPp.ppterm term)
+ in
+ print_endline
+ (String.concat "\n"
+ (List.map
+ (fun (p, e) ->
+ Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
+ (Inference.string_of_equality e))
+ res));
+ print_endline "|";
;;
-(*
+let indexing_retrieval_time = ref 0.;;
+
+
let empty_table () =
- Hashtbl.create 10
+ Path_indexing.PSTrie.empty
;;
-
-let index table eq =
- let _, (_, l, r, ordering), _, _ = eq in
- let hl = head_of_term l in
- let hr = head_of_term r in
- let index x pos =
- let x_entry = try Hashtbl.find table x with Not_found -> [] in
- Hashtbl.replace table x ((pos, eq)::x_entry)
- in
- let _ =
- match ordering with
- | Utils.Gt ->
- index hl Utils.Left
- | Utils.Lt ->
- index hr Utils.Right
- | _ -> index hl Utils.Left; index hr Utils.Right
+let index = Path_indexing.index
+and remove_index = Path_indexing.remove_index
+and in_index = Path_indexing.in_index;;
+
+let get_candidates mode 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
-(* index hl Utils.Left; *)
-(* index hr Utils.Right; *)
- table
+(* print_candidates mode term res; *)
+ let t2 = Unix.gettimeofday () in
+ indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
+ res
;;
-let remove_index table eq =
- let _, (_, l, r, ordering), _, _ = eq in
- let hl = head_of_term l
- and hr = head_of_term r in
- let remove_index x pos =
- let x_entry = try Hashtbl.find table x with Not_found -> [] in
- let newentry = List.filter (fun e -> e <> (pos, eq)) x_entry in
- Hashtbl.replace table x newentry
- in
- remove_index hl Utils.Left;
- remove_index hr Utils.Right;
- table
+(*
+let empty_table () =
+ Discrimination_tree.DiscriminationTree.empty
;;
-*)
+let index = Discrimination_tree.index
+and remove_index = Discrimination_tree.remove_index
+and in_index = Discrimination_tree.in_index;;
-let empty_table () =
- Path_indexing.PSTrie.empty
+let get_candidates mode tree term =
+ let res =
+ let s =
+ match mode with
+ | Matching -> Discrimination_tree.retrieve_generalizations tree term
+ | Unification -> Discrimination_tree.retrieve_unifiables tree term
+ in
+ Discrimination_tree.PosEqSet.elements s
+ in
+(* print_candidates mode term res; *)
+ res
;;
+*)
+
+let match_unif_time_ok = ref 0.;;
+let match_unif_time_no = ref 0.;;
-let index = Path_indexing.index
-and remove_index = Path_indexing.remove_index;;
-
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))
;;
-type retrieval_mode = Matching | Unification;;
-
-(*
-let get_candidates mode table term =
- try Hashtbl.find table (head_of_term term) with Not_found -> []
-;;
-*)
-
-
-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
- in
- Path_indexing.PosEqSet.elements s
-;;
-
-
let subsumption env table target =
let _, (ty, tl, tr, _), tmetas, _ = target in
let metasenv, context, ugraph = env in
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
projects / helm.git / blobdiff