fixed bugs in Indexing.find_matches and Saturation.apply_equality_to_goal

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

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index 497c426361cd5f3452a8d5f98b6902644b5db21e..85ee885cb969755c55bb551b85ea88d6e6a09550 100644 (file)
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -202,17 +202,18 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
 (*   let termty, ugraph = *)
 (*     CicTypeChecker.type_of_aux' metasenv context term ugraph *)
 (*   in *)
+  let check = match termty with C.Implicit None -> false | _ -> true in
   function
     | [] -> None
     | candidate::tl ->
         let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
-(*         if not (fst (CicReduction.are_convertible *)
-(*                        ~metasenv context termty ty ugraph)) then ( *)
-(* (\*           debug_print (lazy ( *\) *)
-(* (\*             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 termty tl *)
-(*         ) else *)
+        if check && not (fst (CicReduction.are_convertible
+                                ~metasenv context termty ty ugraph)) then (
+(*           debug_print (lazy ( *)
+(*             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 termty tl
+        ) else
           let do_match c (* other *) eq_URI =
             let subst', metasenv', ugraph' =
               let t1 = Unix.gettimeofday () in
@@ -425,7 +426,8 @@ let subsumption env table target =
 ;;
 
 
-let rec demodulation_aux metasenv context ugraph table lift_amount term =
+let rec demodulation_aux ?(typecheck=false)
+    metasenv context ugraph table lift_amount term =
   let module C = Cic in
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
@@ -435,8 +437,10 @@ let rec demodulation_aux metasenv context ugraph table lift_amount term =
   | C.Meta _ -> None
   | term ->
       let termty, ugraph =
-        C.Implicit None, ugraph
-(*         CicTypeChecker.type_of_aux' metasenv context term ugraph *)
+        if typecheck then
+          CicTypeChecker.type_of_aux' metasenv context term ugraph
+        else
+          C.Implicit None, ugraph
       in
       let res =
         find_matches metasenv context ugraph lift_amount term termty candidates
@@ -1087,7 +1091,9 @@ let rec demodulation_goal newmeta env table goal =
     let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
     !maxmeta, (newproof, newmetasenv, newterm)
   in  
-  let res = demodulation_aux metasenv' context ugraph table 0 term in
+  let res =
+    demodulation_aux ~typecheck:true metasenv' context ugraph table 0 term
+  in
   match res with
   | Some t ->
       let newmeta, newgoal = build_newgoal t in
@@ -1130,7 +1136,9 @@ let rec demodulation_theorem newmeta env table theorem =
     let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
     !maxmeta, (newterm, newty, newmetasenv)
   in  
-  let res = demodulation_aux metasenv' context ugraph table 0 termty in
+  let res =
+    demodulation_aux ~typecheck:true metasenv' context ugraph table 0 termty
+  in
   match res with
   | Some t ->
       let newmeta, newthm = build_newtheorem t in