X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Findexing.ml;h=5c08d906d07bb5b6f94b9d5793dc7533ac347e87;hb=31afc64440b7da53bb79e6f1524d47bf0fb56aaf;hp=85821097df286ed60d3e14c3e7f600ca709d449e;hpb=acf29bdbdcdc6ad8c2d9d27e8a47500981b605cd;p=helm.git

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index 85821097d..5c08d906d 100644
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -10,34 +10,35 @@ let head_of_term = function
 ;;
 
 
-let index table (sign, eq) =
+let index table eq =
   let _, (_, l, r, ordering), _, _ = eq in
   let hl = head_of_term l in
   let hr = head_of_term r in
   let index x pos = 
     let x_entry = try Hashtbl.find table x with Not_found -> [] in
-    Hashtbl.replace table x ((pos, sign, eq)::x_entry)
+    Hashtbl.replace table x ((pos, eq)::x_entry)
   in
-(*   (match ordering with *)
-(*    | Utils.Gt ->  *)
-(*        index hl Left *)
-(*    | Utils.Lt ->  *)
-(*        index hr Right *)
-(*    | _ -> index hl Left; *)
-(*        index hr Right); *)
-  index hl Left;
-  index hr Right;
+  let _ = 
+    match ordering with
+    | Utils.Gt ->
+        index hl Left
+    | Utils.Lt ->
+        index hr Right
+    | _ -> index hl Left; index hr Right
+  in
+(*   index hl Left; *)
+(*   index hr Right; *)
   table
 ;;
 
 
-let remove_index table (sign, eq) =
+let remove_index table eq =
   let _, (_, l, r, ordering), _, _ = eq in
   let hl = head_of_term l
   and hr = head_of_term r in
   let remove_index x pos =
     let x_entry = try Hashtbl.find table x with Not_found -> [] in
-    let newentry = List.filter (fun e -> e <> (pos, sign, eq)) x_entry in
+    let newentry = List.filter (fun e -> e <> (pos, eq)) x_entry in
     Hashtbl.replace table x newentry
   in
   remove_index hl Left;
@@ -46,26 +47,38 @@ let remove_index table (sign, eq) =
 ;;
 
 
-let rec find_matches metasenv context ugraph lift_amount term =
+let rec find_matches unif_fun metasenv context ugraph lift_amount term =
   let module C = Cic in
   let module U = Utils in
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
   let cmp = !Utils.compare_terms in
+  let names = Utils.names_of_context context in
+  Printf.printf "CHIAMO find_matches (%s) su: %s\n"
+    (if unif_fun == Inference.matching then "MATCHING"
+     else if unif_fun == CicUnification.fo_unif then "UNIFICATION"
+     else "??????????")
+    (CicPp.pp term names);
   function
     | [] -> None
-    | (_, U.Negative, _)::tl ->
-        find_matches metasenv context ugraph lift_amount term tl
-    | (pos, U.Positive, (_, (_, _, _, o), _, _))::tl
-        when (pos = Left && o = U.Lt) || (pos = Right && o = U.Gt) ->
-        find_matches metasenv context ugraph lift_amount term tl
-    | (pos, U.Positive, (proof, (ty, left, right, o), metas, args))::tl ->
+    | (pos, (proof, (ty, left, right, o), metas, args))::tl ->
         let do_match c other eq_URI =
+          Printf.printf "provo con %s: %s, %s\n\n"
+            (if unif_fun == Inference.matching then "MATCHING"
+             else if unif_fun == CicUnification.fo_unif then "UNIFICATION"
+             else "??????????")
+            (CicPp.pp term names)
+            (CicPp.pp (S.lift lift_amount c) names);
           let subst', metasenv', ugraph' =
-            Inference.matching (metasenv @ metas) context term
-              (S.lift lift_amount c) ugraph
+(*             Inference.matching (metasenv @ metas) context term *)
+(*               (S.lift lift_amount c) ugraph *)
+            unif_fun (metasenv @ metas) context
+              term (S.lift lift_amount c) ugraph
           in
+(*           let names = U.names_of_context context in *)
+          Printf.printf "MATCH FOUND: %s, %s\n"
+            (CicPp.pp term names) (CicPp.pp (S.lift lift_amount c) names);
           Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
                 (proof, ty, c, other, eq_URI))
         in
@@ -74,19 +87,38 @@ let rec find_matches metasenv context ugraph lift_amount term =
           else right, left, HL.Logic.eq_ind_r_URI
         in
         if o <> U.Incomparable then
-          try do_match c other eq_URI
-          with e -> find_matches metasenv context ugraph lift_amount term tl
+          try
+            print_endline "SONO QUI!";
+            let res = do_match c other eq_URI in
+            print_endline "RITORNO RES";
+            res
+          with e ->
+            Printf.printf "ERRORE!: %s\n" (Printexc.to_string e);
+            find_matches unif_fun metasenv context ugraph lift_amount term tl
         else
-          let res = try do_match c other eq_URI with e -> None in
+          let res =
+            try
+              let res = do_match c other eq_URI in
+              print_endline "RITORNO RES 2";
+              res
+            with e -> None in
           match res with
-          | Some (_, s, _, _, _) -> 
-              if cmp (M.apply_subst s left) (M.apply_subst s right) =
-                (if pos = Left then U.Gt else U.Lt) then
-                  res
+          | Some (_, s, _, _, _) ->
+              let c' = M.apply_subst s c
+              and other' = M.apply_subst s other in
+              let order = cmp c' other' in
+              let names = U.names_of_context context in
+              Printf.printf "c': %s\nother': %s\norder: %s\n\n"
+                (CicPp.pp c' names) (CicPp.pp other' names)
+                (U.string_of_comparison order);
+(*               if cmp (M.apply_subst s c) (M.apply_subst s other) = U.Gt then *)
+              if order = U.Gt then
+                res
               else
-                find_matches metasenv context ugraph lift_amount term tl
+                find_matches unif_fun metasenv context ugraph
+                  lift_amount term tl
           | None ->
-              find_matches metasenv context ugraph lift_amount term tl
+              find_matches unif_fun metasenv context ugraph lift_amount term tl
 ;;
 
 
@@ -101,7 +133,8 @@ let rec demodulate_term metasenv context ugraph table lift_amount term =
   | C.Meta _ -> None
   | term ->
       let res =
-        find_matches metasenv context ugraph lift_amount term candidates
+        find_matches Inference.matching metasenv context ugraph
+          lift_amount term candidates
       in
       if res <> None then
         res
@@ -148,8 +181,8 @@ let rec demodulate_term metasenv context ugraph table lift_amount term =
                   Some (C.Prod (nn, s', (S.lift 1 t)), subst, menv, ug, info)
             )
         | t ->
-            Printf.printf "Ne` Appl ne` Prod: %s\n"
-              (CicPp.pp t (Utils.names_of_context context));
+(*             Printf.printf "Ne` Appl ne` Prod: %s\n" *)
+(*               (CicPp.pp t (Utils.names_of_context context)); *)
             None
 ;;
 
@@ -159,9 +192,10 @@ let rec demodulate newmeta env table target =
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
+  print_endline "\n\ndemodulate";
   let metasenv, context, ugraph = env in
   let proof, (eq_ty, left, right, order), metas, args = target in
-  let metasenv = metasenv @ metas in
+  let metasenv' = metasenv @ metas in
   let build_newtarget is_left
       (t, subst, menv, ug, (proof', ty, what, other, eq_URI)) = 
     let newterm, newproof =
@@ -169,7 +203,7 @@ let rec demodulate newmeta env table target =
       let bo'' =
         C.Appl ([C.MutInd (HL.Logic.eq_URI, 0, []);
                  S.lift 1 eq_ty] @
-                  if is_left then [bo; S.lift 1 right] else [S.lift 1 left; bo])
+                 if is_left then [bo; S.lift 1 right] else [S.lift 1 left; bo])
       in
       let t' = C.Lambda (C.Anonymous, ty, bo'') in
       bo,
@@ -192,20 +226,20 @@ let rec demodulate newmeta env table target =
     in
     newmeta, newtarget
   in
-  let res = demodulate_term metasenv context ugraph table 0 left in
+  let res = demodulate_term 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 then
+      if Inference.is_identity (metasenv', context, ugraph) newtarget then
         newmeta, newtarget
       else
         demodulate newmeta env table newtarget
   | None ->
-      let res = demodulate_term metasenv context ugraph table 0 right in
+      let res = demodulate_term 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 then
+          if Inference.is_identity (metasenv', context, ugraph) newtarget then
             newmeta, newtarget
           else
             demodulate newmeta env table newtarget
@@ -277,11 +311,17 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term =
   match term with
   | C.Meta _ -> res, lifted_term
   | _ ->
+(*       let names = Utils.names_of_context context in *)
+(*       Printf.printf "CHIAMO find_matches su: %s\n" (CicPp.pp term names); *)
       match
-        find_matches metasenv context ugraph lift_amount term candidates
+        find_matches CicUnification.fo_unif metasenv context ugraph
+          lift_amount term candidates
       with
       | None -> res, lifted_term
-      | Some r -> r::res, lifted_term
+      | Some r ->
+(*           let _, _, _, _, (_, _, what, _, _) = r in *)
+(*           Printf.printf "OK, aggiungo a res: %s\n" (CicPp.pp what names); *)
+          r::res, lifted_term
 ;;
 
 
@@ -292,10 +332,20 @@ let superposition_left (metasenv, context, ugraph) table target =
   let module HL = HelmLibraryObjects in
   let module CR = CicReduction in
   let module U = Utils in
+  print_endline "\n\nsuperposition_left";
   let proof, (eq_ty, left, right, ordering), _, _ = target in
   let expansions, _ =
     let term = if ordering = U.Gt then left else right in
-    betaexpand_term metasenv context ugraph table 0 term
+    let res = 
+      betaexpand_term metasenv context ugraph table 0 term in
+(*     let names = U.names_of_context context in *)
+(*     Printf.printf "\n\nsuperposition_left: %s\n%s\n" *)
+(*       (CicPp.pp term names) *)
+(*       (String.concat "\n" *)
+(*          (List.map *)
+(*             (fun (_, _, _, _, (_, _, what, _, _)) -> CicPp.pp what names) *)
+(*             (fst res))); *)
+    res
   in
   let build_new (bo, s, m, ug, (proof', ty, what, other, eq_URI)) =
     let newgoal, newproof =
@@ -332,12 +382,14 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
   let module HL = HelmLibraryObjects in
   let module CR = CicReduction in
   let module U = Utils in
+  print_endline "\n\nsuperposition_right";
   let eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
+  let metasenv' = metasenv @ newmetas in
   let maxmeta = ref newmeta in
   let res1, res2 =
     match ordering with
-    | U.Gt -> fst (betaexpand_term metasenv context ugraph table 0 left), []
-    | U.Lt -> [], fst (betaexpand_term metasenv context ugraph table 0 right)
+    | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
+    | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
     | _ ->
         let res l r =
           List.filter
@@ -345,7 +397,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
                let subst = M.apply_subst subst in
                let o = !Utils.compare_terms (subst l) (subst r) in
                o <> U.Lt && o <> U.Le)
-            (fst (betaexpand_term metasenv context ugraph table 0 l))
+            (fst (betaexpand_term metasenv' context ugraph table 0 l))
         in
         (res left right), (res right left)
   in