Discrimination and trie removed.

[helm.git] / helm / ocaml / paramodulation / indexing.ml

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index cb20afd812b9ab54567ca32e3ae0d574d259f955..8c41375565652266966189d1d068d7b3bba437c2 100644 (file)
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -23,6 +23,15 @@
  * 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;;
 
 
@@ -53,8 +62,6 @@ let indexing_retrieval_time = ref 0.;;
 
 let apply_subst = CicMetaSubst.apply_subst
 
-
-
 (*
 (* NO INDEXING *)
 let init_index () = ()
@@ -90,8 +97,16 @@ let empty_table () =
 ;;
 
 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
@@ -111,19 +126,41 @@ let get_candidates mode trie term =
 ;;
 *)
 
-
 (* 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
@@ -143,10 +180,10 @@ 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
+      | 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); *)
@@ -233,8 +270,8 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
             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
@@ -501,6 +538,7 @@ let rec demodulation_equality newmeta env table sign target =
   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
@@ -517,7 +555,7 @@ let rec demodulation_equality newmeta env table sign target =
     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' =
@@ -789,7 +827,7 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
     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'' =