* http://cs.unibo.it/helm/.
*)
+module OrderedPosEquality = struct
+ type t = Utils.pos * Inference.equality
+ let compare = Pervasives.compare
+ end
+
+module PosEqSet = Set.Make(OrderedPosEquality);;
+
+module DT = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet);;
+
let debug_print = Utils.debug_print;;
let apply_subst = CicMetaSubst.apply_subst
-
-
(*
(* NO INDEXING *)
let init_index () = ()
;;
let index = Path_indexing.index
-and remove_index = Path_indexing.remove_index
-and in_index = Path_indexing.in_index;;
+let remove_index tree equality =
+ let _, _, (_, l, r, ordering), _, _ = equality in
+ match ordering with
+ | Utils.Gt -> DT.remove_index tree l equality
+ | Utils.Lt -> DT.remove_index tree r equality
+ | _ ->
+ DT.remove_index (DT.remove_index tree r equality) l equality
+
+
+let in_index = Path_indexing.in_index;;
let get_candidates mode trie term =
let t1 = Unix.gettimeofday () in
;;
*)
-
(* DISCRIMINATION TREES *)
let init_index () =
- Hashtbl.clear Discrimination_tree.arities;
+ Hashtbl.clear DT.arities;
;;
let empty_table () =
- Discrimination_tree.DiscriminationTree.empty
+ DT.empty
;;
-let index = Discrimination_tree.index
-and remove_index = Discrimination_tree.remove_index
-and in_index = Discrimination_tree.in_index;;
+let remove_index tree equality =
+ let _, _, (_, l, r, ordering), _, _ = equality in
+ match ordering with
+ | Utils.Gt -> DT.remove_index tree l (Utils.Left, equality)
+ | Utils.Lt -> DT.remove_index tree r (Utils.Right, equality)
+ | _ ->
+ let tree = DT.remove_index tree r (Utils.Right, equality) in
+ DT.remove_index tree l (Utils.Left, equality)
+
+let index tree equality =
+ let _, _, (_, l, r, ordering), _, _ = equality in
+ match ordering with
+ | Utils.Gt -> DT.index tree l (Utils.Left, equality)
+ | Utils.Lt -> DT.index tree r (Utils.Right, equality)
+ | _ ->
+ let tree = DT.index tree r (Utils.Right, equality) in
+ DT.index tree l (Utils.Left, equality)
+
+
+let in_index tree equality =
+ let _, _, (_, l, r, ordering), _, _ = equality in
+ let meta_convertibility (pos,equality') =
+ Inference.meta_convertibility_eq equality equality'
+ in
+ DT.in_index tree l meta_convertibility || DT.in_index tree r meta_convertibility
+
(* 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 -> DT.retrieve_generalizations tree term
+ | Unification -> DT.retrieve_unifiables tree term
in
- Discrimination_tree.PosEqSet.elements s
+ 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'' =