Calling unification instead of matching when checking for subsumption

might instantiate the goal with variables in table (while they are supposed
to be disjoint).

diff --git a/helm/software/components/tactics/paramodulation/founif.ml b/helm/software/components/tactics/paramodulation/founif.ml
index 87550f76aa20c2eed4478e0271aa65900c118af2..c2df6371c410fa8da7d18b9b6d296c6a1b0d8bb2 100644 (file)
--- a/helm/software/components/tactics/paramodulation/founif.ml
+++ b/helm/software/components/tactics/paramodulation/founif.ml
@@ -225,6 +225,13 @@ let matching metasenv1 metasenv2 context t1 t2 ugraph =
 ;;
 
 let unification m1 m2 c t1 t2 ug = 
+  let m1 =
+    if (m1 = m2 && m1 <> []) then assert false
+      (* (prerr_endline "eccoci 2"; []) *) else m1 in
+  (*   
+  prerr_endline (CicPp.ppterm t1);
+  prerr_endline (CicPp.ppterm t2);
+  prerr_endline "++++++++++"; *)
   try 
     unification_aux true m1 m2 c t1 t2 ug
   with exn -> 

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 8f696d6f3e330b960c0d3782c62f2d3720f46ece..77a377a88bfd67d8987bfdd4adfec094961ca468 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -367,6 +367,7 @@ let rec find_all_matches ?(unif_fun=Founif.unification)
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
+  (* prerr_endline ("matching " ^  CicPp.ppterm term); *)
   let cmp = !Utils.compare_terms in
   let check = match termty with C.Implicit None -> false | _ -> true in
   function
@@ -537,7 +538,7 @@ let subsumption_aux_all use_unification env table target =
           let what' = Subst.apply_subst subst what in
           let other' = Subst.apply_subst subst other in
           let subst', menv', ug' =
-            unif_fun metasenv m context what' other' ugraph
+            unif_fun [] menv context what' other' ugraph
           in
           (match Subst.merge_subst_if_possible subst subst' with
           | None -> ok_all what leftorright tl
@@ -555,7 +556,7 @@ let subsumption_all x y z =
 ;;
 
 let unification_all x y z = 
-  subsumption_aux_all true x y z
+  prerr_endline "unification_all"; subsumption_aux_all true x y z
 ;;
 
 let rec demodulation_aux bag ?from ?(typecheck=false) 
@@ -752,7 +753,7 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target =
   in
 
   let res = 
-    demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left 
+    demodulation_aux bag ~from:"from3" metasenv' context ugraph table 0 left 
   in
   if Utils.debug_res then check_res res "demod result";
   let newmeta, newtarget = 

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index b2970d209c39c5edbd3e2d5057b933bc4942ef42..c8ab4e428cfecdc9f9e92f672b55fdb532b00f52 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -820,8 +820,8 @@ let check_if_goal_is_subsumed bag ((_,ctx,_) as env) table (goalproof,menv,ty) =
          Equality.mk_equality bag
            (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv) 
       in
-(*      match Indexing.subsumption env table goal_equation with*)
-       match Indexing.unification env table goal_equation with 
+       match Indexing.subsumption env table goal_equation with 
+       (* match Indexing.unification env table goal_equation with *)
         | Some (subst, equality, swapped ) ->
 (*
             prerr_endline 
@@ -862,7 +862,8 @@ let find_all_subsumed bag maxm env table (goalproof,menv,ty) =
               else
                  p
              in (goalproof, p, id, subst, cicmenv))
-         (Indexing.unification_all env table goal_equation)
+          (Indexing.subsumption_all env table goal_equation)
+         (* (Indexing.unification_all env table goal_equation) *)
   | _ -> assert false
 ;;
 
@@ -882,7 +883,7 @@ let check_if_goal_is_identity env = function
       let reflproof = Equality.Exact (Equality.refl_proof uri eq_ty left) in
       let m = Subst.apply_subst_metasenv s m in
       Some (goalproof, reflproof, 0, s,m)
-    with _ -> None)
+    with CicUnification.UnificationFailure _ -> None)
   | _ -> None
 ;;                              
     
@@ -1592,7 +1593,7 @@ let all_subsumed bag maxm status active passive =
   let cleaned_goal = Utils.remove_local_context type_of_goal in
   let canonical_menv,other_menv = 
     List.partition (fun (_,c,_) -> c = context)  metasenv in
-  prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv)); 
+  (* prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv));   *)
   let metasenv = List.map (fun (i,_,ty)-> (i,[],ty)) canonical_menv in
   let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
   debug_print (lazy (string_of_int (List.length (fst active))));
@@ -1612,6 +1613,7 @@ let all_subsumed bag maxm status active passive =
     match (check_if_goal_is_identity env goal) with
        None -> subsumed
       | Some id -> id::subsumed in
+  debug_print (lazy "dopo subsumed");
   let res =
     List.map 
       (fun 
@@ -1623,7 +1625,8 @@ let all_subsumed bag maxm status active passive =
           let uri, metasenv, subst, meta_proof, term_to_prove, attrs = proof in
           let proof = uri, other_menv@metasenv, subst, meta_proof, term_to_prove, attrs in
             (subst, proof,gl)) subsumed_or_id 
-  in res, !maxmeta
+  in 
+  res, !maxmeta
 
 
 let given_clause 
@@ -1650,7 +1653,7 @@ let given_clause
   let cleaned_goal = Utils.remove_local_context type_of_goal in
   let canonical_menv,other_menv = 
     List.partition (fun (_,c,_) -> c = context)  metasenv in
-  prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv));
+  (* prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv));  *)
   Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *)
   let canonical_menv = List.map (fun (i,_,ty)-> (i,[],ty)) canonical_menv in
   let metasenv' = List.filter (fun (i,_,_)->i<>goalno) canonical_menv in

diff --git a/helm/software/components/tactics/paramodulation/utils.ml b/helm/software/components/tactics/paramodulation/utils.ml
index 8a2722bb6820a1bf3d06652c8d9101be147dabad..a85ccc674220482c782598f26d1d1d1e8e4b9394 100644 (file)
--- a/helm/software/components/tactics/paramodulation/utils.ml
+++ b/helm/software/components/tactics/paramodulation/utils.ml
@@ -25,7 +25,7 @@
 
 (* $Id$ *)
 
-let time = true;;
+let time = false;;
 let debug = false;;
 let debug_metas = false;; 
 let debug_res = false;;