removed old Makefile

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

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index b748afec7357c55270d9ec38fb6a67752be70b28..523cff88233def6f9d30ef2ca304458300386bb0 100644 (file)
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -23,12 +23,16 @@
  * http://cs.unibo.it/helm/.
  *)
 
  * 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 debug_print = Utils.debug_print;;
 
 
 type retrieval_mode = Matching | Unification;;
 

-

 let print_candidates mode term res =
   let _ =
     match mode with
 let print_candidates mode term res =
   let _ =
     match mode with


@@ -53,89 +57,36 @@ let indexing_retrieval_time = ref 0.;;
 
 let apply_subst = CicMetaSubst.apply_subst
 
 
 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
+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.

 *)
 *)

-
-
-(*
-(* 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 get_candidates mode tree term =
   let t1 = Unix.gettimeofday () in
   let res =
     let s = 
       match mode with
 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
     in

-    Discrimination_tree.PosEqSet.elements s
+    Index.PosEqSet.elements s

   in
   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
 (*   print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
 (*   print_newline (); *)
   let t2 = Unix.gettimeofday () in


@@ -153,6 +104,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
   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
 *)
 let rec find_matches metasenv context ugraph lift_amount term termty =
   let module C = Cic in


@@ -204,8 +171,8 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
             in
             match res with
             | Some (_, s, _, _, _) ->
             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 order = cmp c' other' in
                 let names = U.names_of_context context in
                 if order = U.Gt then


@@ -298,7 +265,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
   returns true if target is subsumed by some equality in table
 *)
 let subsumption env table target =
   returns true if target is subsumed by some equality in table
 *)
 let subsumption env table target =

-  let _, (ty, left, right, _), tmetas, _ = target in
+  let _, _, (ty, left, right, _), tmetas, _ = target in

   let metasenv, context, ugraph = env in
   let metasenv = metasenv @ tmetas in
   let samesubst subst subst' =
   let metasenv, context, ugraph = env in
   let metasenv = metasenv @ tmetas in
   let samesubst subst subst' =


@@ -324,14 +291,15 @@ let subsumption env table target =
   in
   let rec ok what = function
     | [] -> false, []
   in
   let rec ok what = function
     | [] -> false, []

-    | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), _, _)), _))::tl ->
+    | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m, _)), _))::tl ->

         try
           let other = if pos = Utils.Left then r else l in
           let subst', menv', ug' =
             let t1 = Unix.gettimeofday () in
             try
               let r = 
         try
           let other = if pos = Utils.Left then r else l in
           let subst', menv', ug' =
             let t1 = Unix.gettimeofday () in
             try
               let r = 

-                Inference.matching metasenv context what other ugraph in
+                Inference.matching (metasenv @ menv @ m) context what other ugraph
+             in

               let t2 = Unix.gettimeofday () in
               match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
               r
               let t2 = Unix.gettimeofday () in
               match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
               r


@@ -348,18 +316,26 @@ let subsumption env table target =
           ok what tl
   in
   let r, subst = ok right leftr in
           ok what tl
   in
   let r, subst = ok right leftr in

-  if r then
-    true, subst
-  else
-    let rightr =
-      match right with
-      | Cic.Meta _ -> []
-      | _ ->
-          let rightc = get_candidates Matching table right in
-          find_all_matches ~unif_fun:Inference.matching
-            metasenv context ugraph 0 right ty rightc
-    in
-    ok left rightr
+  let r, s =
+    if r then
+      true, subst
+    else
+      let rightr =
+       match right with
+         | Cic.Meta _ -> []
+         | _ ->
+              let rightc = get_candidates Matching table right in
+               find_all_matches ~unif_fun:Inference.matching
+                 metasenv context ugraph 0 right ty rightc
+      in
+       ok left rightr
+  in
+(*     (if r then  *)
+(*        debug_print  *)
+(*      (lazy *)
+(*         (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
+(*            (Inference.string_of_equality target) (Utils.print_subst s)))); *)
+    r, s

 ;;
 
 
 ;;
 
 


@@ -463,6 +439,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 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
   let metasenv, context, ugraph = env in
   let _, proof, (eq_ty, left, right, order), metas, args = target in
   let metasenv' = metasenv @ metas in


@@ -479,7 +456,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 =
     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 name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in
       incr demod_counter;
       let bo' =


@@ -496,8 +473,8 @@ let rec demodulation_equality newmeta env table sign target =
           incr maxmeta;
           let irl =
             CicMkImplicit.identity_relocation_list_for_metavariable context in
           incr maxmeta;
           let irl =
             CicMkImplicit.identity_relocation_list_for_metavariable context in

-          debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta));
-          print_newline ();
+(*           debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
+(*           print_newline (); *)

           C.Meta (!maxmeta, irl)
         in
           let eq_found =
           C.Meta (!maxmeta, irl)
         in
           let eq_found =


@@ -553,26 +530,47 @@ let rec demodulation_equality newmeta env table sign target =
     !maxmeta, res
   in
   let res = demodulation_aux metasenv' context ugraph table 0 left in
     !maxmeta, res
   in
   let res = demodulation_aux metasenv' context ugraph table 0 left in

-  match res with
-  | Some t ->
-      let newmeta, newtarget = build_newtarget true t in
-      if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
-        (Inference.meta_convertibility_eq target newtarget) then
-          newmeta, newtarget
-      else
-        demodulation_equality newmeta env table sign newtarget
-  | None ->
-      let res = demodulation_aux metasenv' context ugraph table 0 right in
-      match res with
-      | Some t ->
-          let newmeta, newtarget = build_newtarget false t in
-          if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
+  let newmeta, newtarget = 
+    match res with
+    | Some t ->
+       let newmeta, newtarget = build_newtarget true t in
+         if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||

             (Inference.meta_convertibility_eq target newtarget) then
             (Inference.meta_convertibility_eq target newtarget) then

-              newmeta, newtarget
-          else
-              demodulation_equality newmeta env table sign newtarget
-      | None ->
-          newmeta, target
+             newmeta, newtarget
+         else
+            demodulation_equality newmeta env table sign newtarget
+    | None ->
+       let res = demodulation_aux metasenv' context ugraph table 0 right in
+         match res with
+         | Some t ->
+             let newmeta, newtarget = build_newtarget false t in
+               if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
+                 (Inference.meta_convertibility_eq target newtarget) then
+                   newmeta, newtarget
+               else
+                 demodulation_equality newmeta env table sign newtarget
+         | None ->
+             newmeta, target
+  in
+  (* newmeta, newtarget *)
+  (* tentiamo di ridurre usando CicReduction.normalize *)
+  let w, p, (ty, left, right, o), m, a = newtarget in
+  let left' = ProofEngineReduction.simpl context left in
+  let right' = ProofEngineReduction.simpl context right in
+  let newleft =
+    if !Utils.compare_terms left' left = Utils.Lt then left' else left in
+  let newright = 
+    if !Utils.compare_terms right' right = Utils.Lt then right' else right in
+(*   if newleft != left || newright != right then ( *)
+(*     debug_print *)
+(*       (lazy *)
+(*      (Printf.sprintf "left: %s, left': %s\nright: %s, right': %s\n" *)
+(*         (CicPp.ppterm left) (CicPp.ppterm left') (CicPp.ppterm right) *)
+(*         (CicPp.ppterm right'))) *)
+(*   ); *)
+  let w' = Utils.compute_equality_weight ty newleft newright in
+  let o' = !Utils.compare_terms newleft newright in
+  newmeta, (w', p, (ty, newleft, newright, o'), m, a)

 ;;
 
 
 ;;
 
 


@@ -723,14 +721,14 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
   let maxmeta = ref newmeta in
   let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
 
   let maxmeta = ref newmeta in
   let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
 

-    debug_print (lazy "\nSUPERPOSITION LEFT\n");
+(*     debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)

 
     let time1 = Unix.gettimeofday () in
     
     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 time1 = Unix.gettimeofday () in
     
     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'' = 
       let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
       incr sup_l_counter;
       let bo'' = 


@@ -765,10 +763,10 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
         in
         match proof with
         | Inference.BasicProof _ ->
         in
         match proof with
         | Inference.BasicProof _ ->

-            debug_print (lazy "replacing a BasicProof");
+(*             debug_print (lazy "replacing a BasicProof"); *)

             pb
         | Inference.ProofGoalBlock (_, parent_proof) ->
             pb
         | Inference.ProofGoalBlock (_, parent_proof) ->

-            debug_print (lazy "replacing another ProofGoalBlock");
+(*             debug_print (lazy "replacing another ProofGoalBlock"); *)

             Inference.ProofGoalBlock (pb, parent_proof)
         | _ -> assert false
       in
             Inference.ProofGoalBlock (pb, parent_proof)
         | _ -> assert false
       in


@@ -913,7 +911,7 @@ let rec demodulation_goal newmeta env table goal =
         incr maxmeta;
         let irl =
           CicMkImplicit.identity_relocation_list_for_metavariable context in
         incr maxmeta;
         let irl =
           CicMkImplicit.identity_relocation_list_for_metavariable context in

-        debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta));
+(*         debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)

         C.Meta (!maxmeta, irl)
       in
       let eq_found =
         C.Meta (!maxmeta, irl)
       in
       let eq_found =


@@ -936,19 +934,19 @@ let rec demodulation_goal newmeta env table goal =
         in
         let rec repl = function
           | Inference.NoProof ->
         in
         let rec repl = function
           | Inference.NoProof ->

-              debug_print (lazy "replacing a NoProof");
+(*               debug_print (lazy "replacing a NoProof"); *)

               pb
           | Inference.BasicProof _ ->
               pb
           | Inference.BasicProof _ ->

-              debug_print (lazy "replacing a BasicProof");
+(*               debug_print (lazy "replacing a BasicProof"); *)

               pb
           | Inference.ProofGoalBlock (_, parent_proof) ->
               pb
           | Inference.ProofGoalBlock (_, parent_proof) ->

-              debug_print (lazy "replacing another ProofGoalBlock");
+(*               debug_print (lazy "replacing another ProofGoalBlock"); *)

               Inference.ProofGoalBlock (pb, parent_proof)
           | (Inference.SubProof (term, meta_index, p) as subproof) ->
               Inference.ProofGoalBlock (pb, parent_proof)
           | (Inference.SubProof (term, meta_index, p) as subproof) ->

-              debug_print
-                (lazy
-                   (Printf.sprintf "replacing %s"
-                      (Inference.string_of_proof subproof)));
+(*               debug_print *)
+(*                 (lazy *)
+(*                    (Printf.sprintf "replacing %s" *)
+(*                       (Inference.string_of_proof subproof))); *)

               Inference.SubProof (term, meta_index, repl p)
           | _ -> assert false
         in repl proof
               Inference.SubProof (term, meta_index, repl p)
           | _ -> assert false
         in repl proof