added some typechecks to avoid using equations with the wrong type

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index 64a96f82aefdcdb4f11a665c3316538b37519f07..be02d8c1b83eb552523a7a5425e3cb267010299c 100644 (file)
--- 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;;
 
 
@@ -142,51 +145,61 @@ 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 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 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 ->
+                find_matches metasenv context ugraph lift_amount term tl
 ;;
 
 
@@ -199,58 +212,69 @@ 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
+        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 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
+          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 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
+              let res = do_match c other eq_URI in
+              res::(find_all_matches ~unif_fun metasenv context ugraph
+                      lift_amount term tl)
             with 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
-        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
+              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
 ;;
 
 

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index db185b421b040e5a1f8cbb63677c399b43114c7e..0ff8aeb7ab84782dbfbfd7c9dd83a951fd838af6 100644 (file)
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -1084,7 +1084,8 @@ let equations_blacklist =
       "cic:/Coq/Init/Logic/f_equal.con";
       "cic:/Coq/Init/Logic/f_equal2.con";
       "cic:/Coq/Init/Logic/f_equal3.con";
-      "cic:/Coq/Init/Logic/sym_eq.con"
+      "cic:/Coq/Init/Logic/sym_eq.con";
+(*       "cic:/Coq/Logic/Eqdep/UIP_refl.con"; *)
     ]
 ;;
 

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index ec7634d94525ce35007ea475e72a959784c7b4a7..f56b8946f0e248d305c8ca2927a01c459543d5be 100644 (file)
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -5,10 +5,6 @@ open Utils;;
 (* set to false to disable paramodulation inside auto_tac *)
 let connect_to_auto = true;;
 
-let debug = true;;
-
-let debug_print = if debug then prerr_endline else ignore;;
-
 
 (* profiling statistics... *)
 let infer_time = ref 0.;;

diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index d6454f2027d4799fdf2dd49bf1ade2bdd685f24d..840b3a828a5483e4c978b2db62572b18fa9b1fed 100644 (file)
--- a/helm/ocaml/paramodulation/utils.ml
+++ b/helm/ocaml/paramodulation/utils.ml
@@ -1,3 +1,8 @@
+let debug = true;;
+
+let debug_print = if debug then prerr_endline else ignore;;
+
+
 let print_metasenv metasenv =
   String.concat "\n--------------------------\n"
     (List.map (fun (i, context, term) ->

diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/paramodulation/utils.mli
index e69caed4d6644bf46c9704b76006bcc1c8b94c43..0187f94a7bff5a429a6656186465be79ff2b24e4 100644 (file)
--- a/helm/ocaml/paramodulation/utils.mli
+++ b/helm/ocaml/paramodulation/utils.mli
@@ -41,3 +41,5 @@ type pos = Left | Right
 val string_of_pos: pos -> string
 
 val compute_equality_weight: Cic.term -> Cic.term -> Cic.term -> int
+
+val debug_print: string -> unit