* http://cs.unibo.it/helm/.
*)
+module Index = Equality_indexing.DT (* discrimination tree based indexing *)
+(*
+module Index = Equality_indexing.DT (* path tree based indexing *)
+*)
+
let debug_print = Utils.debug_print;;
type retrieval_mode = Matching | Unification;;
-
let print_candidates mode term res =
let _ =
match mode with
let apply_subst = CicMetaSubst.apply_subst
-
-
-(*
-(* NO INDEXING *)
-let init_index () = ()
-
-let empty_table () = []
-
-let index table equality =
- let _, _, (_, l, r, ordering), _, _ = equality in
- match ordering with
- | Utils.Gt -> (Utils.Left, equality)::table
- | Utils.Lt -> (Utils.Right, equality)::table
- | _ -> (Utils.Left, equality)::(Utils.Right, equality)::table
-;;
-
-let remove_index table equality =
- List.filter (fun (p, e) -> e != equality) table
-;;
-
-let in_index table equality =
- List.exists (fun (p, e) -> e == equality) table
-;;
-
-let get_candidates mode table term = table
-*)
-
-
-(*
-(* PATH INDEXING *)
-let init_index () = ()
-
-let empty_table () =
- Path_indexing.PSTrie.empty
-;;
-
-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
-(* print_candidates mode term res; *)
- let t2 = Unix.gettimeofday () in
- indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
- res
-;;
-*)
-
-
-(* DISCRIMINATION TREES *)
-let init_index () =
- Hashtbl.clear Discrimination_tree.arities;
-;;
-
-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 index = Index.index
+let remove_index = Index.remove_index
+let in_index = Index.in_index
+let empty = Index.empty
+let init_index = Index.init_index
(* returns a list of all the equalities in the tree that are in relation
"mode" with the given term, where mode can be either Matching or
let res =
let s =
match mode with
- | Matching -> Discrimination_tree.retrieve_generalizations tree term
- | Unification -> Discrimination_tree.retrieve_unifiables tree term
+ | Matching -> Index.retrieve_generalizations tree term
+ | Unification -> Index.retrieve_unifiables tree term
in
- Discrimination_tree.PosEqSet.elements s
+ Index.PosEqSet.elements s
in
(* print_candidates mode term res; *)
(* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
in
match res with
| Some (_, s, _, _, _) ->
- let c' = apply_subst s c
- and other' = apply_subst s other in
+ let c' = apply_subst s c in
+ let other' = U.guarded_simpl context (apply_subst s other) in
let order = cmp c' other' in
let names = U.names_of_context context in
if order = U.Gt then
let module S = CicSubstitution in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
+ let module U = Utils in
let metasenv, context, ugraph = env in
let _, proof, (eq_ty, left, right, order), metas, args = target in
let metasenv' = metasenv @ metas in
in
let what, other = if pos = Utils.Left then what, other else other, what in
let newterm, newproof =
- let bo = apply_subst subst (S.subst other t) in
+ let bo = U.guarded_simpl context (apply_subst subst (S.subst other t)) in
let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in
incr demod_counter;
let bo' =
let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
let what, other = if pos = Utils.Left then what, other else other, what in
let newgoal, newproof =
- let bo' = apply_subst s (S.subst other bo) in
+ let bo' = U.guarded_simpl context (apply_subst s (S.subst other bo)) in
let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
incr sup_l_counter;
let bo'' =