fixed demodulation bug

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index 5eb89650b706dfba2fa9198087b990d2e66989b1..c4b0a842f26c163c513dfc25089736a860f872ea 100644 (file)
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -106,14 +106,19 @@ let meta_convertibility_eq eq1 eq2 =
     try
       let table = meta_convertibility_aux [] left left' in
 (*       print_table table "before"; *)
-      let table = meta_convertibility_aux table right right' in
+      let _ = meta_convertibility_aux table right right' in
 (*       print_table table "after"; *)
       true
     with NotMetaConvertible ->
 (*       Printf.printf "NotMetaConvertible:\n%s = %s\n%s = %s\n\n" *)
 (*         (CicPp.ppterm left) (CicPp.ppterm right) *)
 (*         (CicPp.ppterm left') (CicPp.ppterm right'); *)
-      false
+      try
+        let table = meta_convertibility_aux [] left right' in
+        let _ = meta_convertibility_aux table right left' in
+        true
+      with NotMetaConvertible ->
+        false
 ;;
 
 
@@ -379,26 +384,25 @@ let beta_expand ?(metas_ok=true) ?(match_only=false)
               CicUnification.fo_unif metasenv context
                 (S.lift lift_amount what) term ugraph
             in
-            (*           Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *)
-            (*             (CicPp.ppterm (S.lift lift_amount what)); *)
-            (*           Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *)
-            (*           Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *)
+(*           Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *)
+(*             (CicPp.ppterm (S.lift lift_amount what)); *)
+(*           Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *)
+(*           Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *)
             (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *)
-            let term' = CicMetaSubst.apply_subst subst' term in (
-              if match_only && not (meta_convertibility term term') then (
-(*                 Printf.printf "term e term' sono diversi!:\n%s\n%s\n\n" *)
-(*                   (CicPp.ppterm term) (CicPp.ppterm term'); *)
+            if match_only then
+              let term' = CicMetaSubst.apply_subst subst' term in
+              if not (meta_convertibility term term') then (
+(*                 let names = names_of_context context in *)
+(*                 Printf.printf "\nterm e term' sono diversi!:\n%s\n%s\n\n" *)
+(*                   (CicPp.pp term names) (CicPp.pp term' names); *)
                 res, lifted_term
               )
               else
-(*                 let _ = *)
-(*                   if match_only then *)
-(*                     Printf.printf "OK, trovato match con %s\n" *)
-(*                       (CicPp.ppterm term) *)
-(*                 in *)
                 ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
                  lifted_term)
-            )
+            else
+              ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
+               lifted_term)
           with _ ->
             res, lifted_term
     in
@@ -732,19 +736,27 @@ let demodulation newmeta (metasenv, context, ugraph) target source =
     let rec demodulate newmeta step metasenv target =
       let proof, (eq_ty, left, right), metas, args = target in
       let is_left, what, other, eq_URI = get_params step in
+
+      let env = metasenv, context, ugraph in
+      let names = names_of_context context in
 (*       Printf.printf *)
-(*         "demodulate\ntarget: %s = %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
-(*         (CicPp.ppterm left) (CicPp.ppterm right) (CicPp.ppterm what) *)
-(*         (CicPp.ppterm other) (string_of_bool is_left); *)
+(*         "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
+(*         (string_of_equality ~env target) (CicPp.pp what names) *)
+(*         (CicPp.pp other names) (string_of_bool is_left); *)
 (*       Printf.printf "step: %d\n" step; *)
 (*       print_newline (); *)
+
       let ok (t, s, m, ug) =
         nonrec_kbo (M.apply_subst s what) (M.apply_subst s other) = Gt
       in
       let res =
-        List.filter ok
-          (beta_expand ~metas_ok:false ~match_only:true
-             what ty left context (metasenv @ metas) ugraph)
+        let r = (beta_expand ~metas_ok:false ~match_only:true
+                   what ty (if is_left then left else right)
+                   context (metasenv @ metas) ugraph) 
+        in
+(*         print_endline "res:"; *)
+(*         List.iter (fun (t, s, m, ug) -> print_endline (CicPp.pp t names)) r; *)
+        List.filter ok r
       in
       match res with
       | [] ->
@@ -778,12 +790,10 @@ let demodulation newmeta (metasenv, context, ugraph) target source =
             fix_metas newmeta
               (newproof, (eq_ty, left, right), newmetasenv, newargs)
           in
-          let _, (_, left, right), _, _ = newtarget
-          and _, (_, oldleft, oldright), _, _ = target in
 (*           Printf.printf *)
-(*             "demodulate, newtarget: %s = %s\ntarget was: %s = %s\n" *)
-(*             (CicPp.ppterm left) (CicPp.ppterm right) *)
-(*             (CicPp.ppterm oldleft) (CicPp.ppterm oldright); *)
+(*             "demodulate, newtarget: %s\ntarget was: %s\n" *)
+(*             (string_of_equality ~env newtarget) *)
+(*             (string_of_equality ~env target); *)
 (*           print_newline (); *)
           demodulate newmeta step metasenv newtarget
     in