X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Findexing.ml;h=4e222fd6ad6caf4795eb42d138c5964bb07b32cd;hb=e6b28085c97ae7b9bd3f3262b105f6b84f42b047;hp=f15a0cee61a16c3cfb5630ae0c4163bdb95ab01e;hpb=22d39afadb3027477e4a42c315ec10518cbf47ed;p=helm.git

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index f15a0cee6..4e222fd6a 100644
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -1,4 +1,7 @@
 
+let debug_print = Utils.debug_print;;
+
+
 type retrieval_mode = Matching | Unification;;
 
 
@@ -116,6 +119,8 @@ let get_candidates mode tree term =
     Discrimination_tree.PosEqSet.elements s
   in
 (*   print_candidates mode term res; *)
+(*   print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
+(*   print_newline (); *)
   let t2 = Unix.gettimeofday () in
   indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
   res
@@ -140,51 +145,64 @@ let rec find_matches metasenv context ugraph lift_amount term =
   let module HL = HelmLibraryObjects in
   let cmp = !Utils.compare_terms in
   let names = Utils.names_of_context context in
+  let termty, ugraph =
+    CicTypeChecker.type_of_aux' metasenv context term ugraph
+  in
   function
     | [] -> None
     | candidate::tl ->
         let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
-        let do_match c other eq_URI =
-          let subst', metasenv', ugraph' =
-            let t1 = Unix.gettimeofday () in
-            try
-              let r = 
-                Inference.matching (metasenv @ metas) context
-                  term (S.lift lift_amount c) ugraph in
-              let t2 = Unix.gettimeofday () in
-              match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
-              r
-            with e ->
-              let t2 = Unix.gettimeofday () in
-              match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
-              raise e
-          in
+        if not (fst (CicReduction.are_convertible
+                       ~metasenv context termty ty ugraph)) then (
+          debug_print (
+            Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found"
+              (CicPp.pp termty names) (CicPp.pp ty names));
+          find_matches metasenv context ugraph lift_amount term tl
+        ) else
+          let do_match c other eq_URI =
+            let subst', metasenv', ugraph' =
+              let t1 = Unix.gettimeofday () in
+              try
+                let r =
+                  Inference.matching (metasenv @ metas) context
+                    term (S.lift lift_amount c) ugraph in
+                let t2 = Unix.gettimeofday () in
+                match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
+                r
+              with Inference.MatchingFailure as e ->
+                let t2 = Unix.gettimeofday () in
+                match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
+                raise e
+            in
             Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
                   (candidate, eq_URI))
-        in
-        let c, other, eq_URI =
-          if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI
-          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
-        else
-          let res = try do_match c other eq_URI with e -> None in
-          match res with
-          | 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
-              if order = U.Gt then
-                res
-              else
-                find_matches metasenv context ugraph lift_amount term tl
-          | None ->
+          in
+          let c, other, eq_URI =
+            if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI
+            else right, left, HL.Logic.eq_ind_r_URI
+          in
+          if o <> U.Incomparable then
+            try
+              do_match c other eq_URI
+            with Inference.MatchingFailure ->
               find_matches metasenv context ugraph lift_amount term tl
+          else
+            let res =
+              try do_match c other eq_URI
+              with Inference.MatchingFailure -> None
+            in
+            match res with
+            | 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
+                if order = U.Gt then
+                  res
+                else
+                  find_matches metasenv context ugraph lift_amount term tl
+            | None ->
+                find_matches metasenv context ugraph lift_amount term tl
 ;;
 
 
@@ -197,58 +215,78 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
   let module HL = HelmLibraryObjects in
   let cmp = !Utils.compare_terms in
   let names = Utils.names_of_context context in
+  let termty, ugraph =
+    CicTypeChecker.type_of_aux' metasenv context term ugraph
+  in
   function
     | [] -> []
     | candidate::tl ->
         let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
-        let do_match c other eq_URI =
-          let subst', metasenv', ugraph' =
-            let t1 = Unix.gettimeofday () in
-            try
-              let r = 
-                unif_fun (metasenv @ metas) context
-                  term (S.lift lift_amount c) ugraph in
-              let t2 = Unix.gettimeofday () in
-              match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
-              r
-            with e ->
-              let t2 = Unix.gettimeofday () in
-              match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
-              raise e
+        if not (fst (CicReduction.are_convertible
+                       ~metasenv context termty ty ugraph)) then (
+          debug_print (
+            Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found"
+              (CicPp.pp termty names) (CicPp.pp ty names));
+          find_all_matches ~unif_fun metasenv context ugraph
+            lift_amount term tl
+        ) else
+          let do_match c other eq_URI =
+            let subst', metasenv', ugraph' =
+              let t1 = Unix.gettimeofday () in
+              try
+                let r = 
+                  unif_fun (metasenv @ metas) context
+                    term (S.lift lift_amount c) ugraph in
+                let t2 = Unix.gettimeofday () in
+                match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
+                r
+              with
+              | Inference.MatchingFailure
+              | CicUnification.UnificationFailure _
+              | CicUnification.Uncertain _ as e ->
+                let t2 = Unix.gettimeofday () in
+                match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
+                raise e
+            in
+            (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
+             (candidate, eq_URI))
           in
-          (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
-           (candidate, eq_URI))
-        in
-        let c, other, eq_URI =
-          if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI
-          else right, left, HL.Logic.eq_ind_r_URI
-        in
-        if o <> U.Incomparable then
-          try
-            let res = do_match c other eq_URI in
-            res::(find_all_matches ~unif_fun metasenv context ugraph
-                    lift_amount term tl)
-          with e ->
-            find_all_matches ~unif_fun metasenv context ugraph
-              lift_amount term tl
-        else
-          try
-            let res = do_match c other eq_URI in
-            match res with
-            | _, 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
-                if order <> U.Lt && order <> U.Le then
-                  res::(find_all_matches ~unif_fun metasenv context ugraph
-                          lift_amount term tl)
-                else
-                  find_all_matches ~unif_fun metasenv context ugraph
-                    lift_amount term tl
-          with e ->
-            find_all_matches ~unif_fun metasenv context ugraph
-              lift_amount term tl
+          let c, other, eq_URI =
+            if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI
+            else right, left, HL.Logic.eq_ind_r_URI
+          in
+          if o <> U.Incomparable then
+            try
+              let res = do_match c other eq_URI in
+              res::(find_all_matches ~unif_fun metasenv context ugraph
+                      lift_amount term tl)
+            with
+            | Inference.MatchingFailure
+            | CicUnification.UnificationFailure _
+            | CicUnification.Uncertain _ ->
+              find_all_matches ~unif_fun metasenv context ugraph
+                lift_amount term tl
+          else
+            try
+              let res = do_match c other eq_URI in
+              match res with
+              | _, 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
+                  if order <> U.Lt && order <> U.Le then
+                    res::(find_all_matches ~unif_fun metasenv context ugraph
+                            lift_amount term tl)
+                  else
+                    find_all_matches ~unif_fun metasenv context ugraph
+                      lift_amount term tl
+            with
+            | Inference.MatchingFailure
+            | CicUnification.UnificationFailure _
+            | CicUnification.Uncertain _ ->
+                find_all_matches ~unif_fun metasenv context ugraph
+                  lift_amount term tl
 ;;
 
 
@@ -288,13 +326,13 @@ let subsumption env table target =
           let t2 = Unix.gettimeofday () in
           match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
           r
-        with e ->
+        with Inference.MatchingFailure as e ->
           let t2 = Unix.gettimeofday () in
           match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
           raise e
       in
       samesubst subst subst'
-    with e ->
+    with Inference.MatchingFailure ->
       false
   in
   let r = List.exists (ok right) leftr in