fixed bugs in Indexing.find_matches and Saturation.apply_equality_to_goal

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

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index 825d6b8c8b6a586225a349bb52ba5bef20505bb5..181b4e1d9a39da08039858250d290025925d1ca6 100644 (file)
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -858,13 +858,13 @@ let simplify_goal env goal ?passive (active_list, active_table) =
         let changed', goal = demodulate passive_table goal in
         (changed || changed'), goal
   in
-(*   let _ = *)
-(*     let p, _, t = goal in *)
-(*     debug_print *)
-(*       (lazy *)
-(*          (Printf.sprintf "Goal after demodulation: %s, %s" *)
-(*             (string_of_proof p) (CicPp.ppterm t))) *)
-(*   in *)
+  let _ =
+    let p, _, t = goal in
+    debug_print
+      (lazy
+         (Printf.sprintf "Goal after demodulation: %s, %s"
+            (string_of_proof p) (CicPp.ppterm t)))
+  in
   changed, goal
 ;;
 
@@ -942,6 +942,10 @@ let apply_equality_to_goal env equality goal =
   let eqterm =
     C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right] in
   let gproof, gmetas, gterm = goal in
+  debug_print
+    (lazy
+       (Printf.sprintf "APPLY EQUALITY TO GOAL: %s, %s"
+          (string_of_equality equality) (CicPp.ppterm gterm)));
   try
     let subst, metasenv', _ =
       let menv = metasenv @ metas @ gmetas in
@@ -1060,7 +1064,7 @@ let new_meta () =
 ;;
 
 
-let apply_to_goal env theorems active goal =
+let apply_to_goal env theorems ?passive active goal =
   let metasenv, context, ugraph = env in
   let proof, metas, term = goal in
   debug_print
@@ -1173,15 +1177,25 @@ let apply_to_goal env theorems active goal =
   in
   let r, s, l =
     if Inference.term_is_equality term then
-      let rec appleq = function
+      let _ = debug_print (lazy "OK, is equality!!") in
+      let rec appleq_a = function
         | [] -> false, [], []
         | (Positive, equality)::tl ->
             let ok, s, newproof = apply_equality_to_goal env equality goal in
-            if ok then true, s, [newproof, metas, term] else appleq tl
-        | _::tl -> appleq tl
+            if ok then true, s, [newproof, metas, term] else appleq_a tl
+        | _::tl -> appleq_a tl
+      in
+      let rec appleq_p = function
+        | [] -> false, [], []
+        | equality::tl ->
+            let ok, s, newproof = apply_equality_to_goal env equality goal in
+            if ok then true, s, [newproof, metas, term] else appleq_p tl
       in
       let al, _ = active in
-      appleq al
+      match passive with
+      | None -> appleq_a al
+      | Some (_, (pl, _), _) ->
+          let r, s, l = appleq_a al in if r then r, s, l else appleq_p pl
     else
       false, [], []
   in
@@ -1189,7 +1203,7 @@ let apply_to_goal env theorems active goal =
 ;;
 
 
-let apply_to_goal_conj env theorems active (depth, goals) =
+let apply_to_goal_conj env theorems ?passive active (depth, goals) =
   let rec aux = function
     | goal::tl ->
         let propagate_subst subst (proof, metas, term) =
@@ -1221,7 +1235,7 @@ let apply_to_goal_conj env theorems active (depth, goals) =
                 ProofBlock (subst @ s, u, nty, t, pe, p)
           in (repl proof, metas, term)
         in
-        let r = apply_to_goal env theorems active goal in (
+        let r = apply_to_goal env theorems ?passive active goal in (
           match r with
           | `No -> `No (depth, goals)
           | `GoOn sl (* (subst, gl) *) ->
@@ -1421,7 +1435,7 @@ let apply_to_goals env is_passive_empty theorems active goals =
 ;;
 
 
-let apply_goal_to_theorems dbd env theorems active goals =
+let apply_goal_to_theorems dbd env theorems ?passive active goals =
 (*   let theorems, _ = theorems in *)
   let context_hyp, library_thms = theorems in
   let thm_uris =
@@ -1434,7 +1448,7 @@ let apply_goal_to_theorems dbd env theorems active goals =
   let rec aux = function
     | [] -> false, (a_goals, p_goals)
     | theorem::tl ->
-        let res = apply_to_goal_conj env [theorem] active goal in
+        let res = apply_to_goal_conj env [theorem] ?passive active goal in
         match res with
         | `Ok newgoals ->
             true, ([newgoals], [])
@@ -1752,7 +1766,9 @@ let rec given_clause_fullred dbd env goals theorems passive active =
            (Printf.sprintf "\ngoals = \nactive\n%s\npassive\n%s\n"
               (print_goals (fst goals)) (print_goals (snd goals))))
     in
-    let ok, goals = apply_goal_to_theorems dbd env theorems active goals in
+    let ok, goals =
+      apply_goal_to_theorems dbd env theorems ~passive active goals
+    in
     if ok then
       let proof =
         match (fst goals) with