X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Findexing.ml;h=2d9076ad5fd1e389d5d94f5fce3230d9b972d862;hb=803959f90ae806a62746efe7f557ecd4b70c16ee;hp=1d2d6a9048a12361851620fdf7bd461e47755ac9;hpb=6b38b8f5c675570ca5a70e917cf77c783ef2d092;p=helm.git

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index 1d2d6a904..2d9076ad5 100644
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -23,12 +23,18 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
+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
@@ -53,89 +59,36 @@ let indexing_retrieval_time = ref 0.;;
 
 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
-;;
+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
+   Unification.
+
+   Format of the return value: list of tuples in the form:
+   (position - Left or Right - of the term that matched the given one in this
+     equality,
+    equality found)
+   
+   Note that if equality is "left = right", if the ordering is left > right,
+   the position will always be Left, and if the ordering is left < right,
+   position will be Right.
 *)
-
-
-(* 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 get_candidates mode tree term =
   let t1 = Unix.gettimeofday () in
   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_candidates mode term res; *)
 (*   print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
 (*   print_newline (); *)
   let t2 = Unix.gettimeofday () in
@@ -153,6 +106,22 @@ let match_unif_time_no = ref 0.;;
   termty can be Implicit if it is not needed. The result (one of the sides of
   the equality, actually) should be not greater (wrt the term ordering) than
   term
+
+  Format of the return value:
+
+  (term to substitute, [Cic.Rel 1 properly lifted - see the various
+                        build_newtarget functions inside the various
+                        demodulation_* functions]
+   substitution used for the matching,
+   metasenv,
+   ugraph, [substitution, metasenv and ugraph have the same meaning as those
+   returned by CicUnification.fo_unif]
+   (equality where the matching term was found, [i.e. the equality to use as
+                                                rewrite rule]
+    uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
+         the equality: this is used to build the proof term, again see one of
+         the build_newtarget functions]
+   ))
 *)
 let rec find_matches metasenv context ugraph lift_amount term termty =
   let module C = Cic in
@@ -204,8 +173,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
@@ -472,6 +441,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
@@ -488,7 +458,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' =
@@ -760,7 +730,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'' =