X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Ffounif.ml;h=b635599515b75ba0d77fc7f6e7cbe793df66ee9a;hb=b8934a9598d747662139c74c751b8223bcc19d03;hp=ac80099b06b3602b3905330949f37cbd37896994;hpb=5ca3189127b10847b4986330482f34157661bbcf;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/founif.ml b/helm/software/components/tactics/paramodulation/founif.ml
index ac80099b0..b63559951 100644
--- a/helm/software/components/tactics/paramodulation/founif.ml
+++ b/helm/software/components/tactics/paramodulation/founif.ml
@@ -106,9 +106,7 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph =
     | C.Meta (i, l), t -> (
         try
           let _, _, ty = CicUtil.lookup_meta i menv in
-          assert (not (Subst.is_in_subst i subst));
           let subst = Subst.buildsubst i context t ty subst in
-          let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *)
           subst, menv
         with CicUtil.Meta_not_found m ->
           let names = names_of_context context in
@@ -143,11 +141,41 @@ let profiler2 = HExtlib.profile "P/Inference.unif_simple[flatten_fast]"
 let profiler3 = HExtlib.profile "P/Inference.unif_simple[resolve_meta]"
 let profiler4 = HExtlib.profile "P/Inference.unif_simple[filter]"
 
+let check_for_duplicates metas msg =
+  let rec aux = function
+    | [] -> true
+    | (m,_,_)::tl -> 
+	not (List.exists (fun (i, _, _) -> i = m) tl) && aux tl in
+  let b = aux metas in
+  if not b then  
+    begin 
+      prerr_endline ("DUPLICATI ---- " ^ msg);
+      prerr_endline (CicMetaSubst.ppmetasenv [] metas);
+      assert false
+    end
+  else b
+;;
+
+let check_metasenv msg menv =
+  List.iter
+    (fun (i,ctx,ty) -> 
+       try ignore(CicTypeChecker.type_of_aux' menv ctx ty 
+		  CicUniv.empty_ugraph)
+       with 
+	 | CicUtil.Meta_not_found _ -> 
+	     prerr_endline (msg ^ CicMetaSubst.ppmetasenv [] menv);
+	     assert false
+	 | _ -> ()
+    ) menv
+;;
+
 let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
-  let metasenv = 
-    HExtlib.list_uniq (List.sort Pervasives.compare (metasenv1 @ metasenv2)) 
-    (* metasenv1 @ metasenv2 *)
-  in
+  let metasenv = metasenv1@metasenv2 in
+  if Utils.debug_metas then
+    begin
+      ignore(check_for_duplicates metasenv "unification_aux");
+      check_metasenv "unification_aux" metasenv;
+    end;
   let subst, menv, ug =
     if not (is_simple_term t1) || not (is_simple_term t2) then (
       debug_print
@@ -175,7 +203,13 @@ let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
   in
   let flatten subst = profiler.HExtlib.profile flatten subst in
   let subst = flatten subst in *)
-    subst, menv, ug
+  if Utils.debug_metas then
+    ignore(check_for_duplicates menv "unification_aux prima di apply_subst");
+  let menv = Subst.apply_subst_metasenv subst menv in
+  if Utils.debug_metas then
+    (let _ = check_for_duplicates menv "unif_aux after" in
+    check_metasenv "unification_aux after 1" menv);
+  subst, menv, ug
 ;;
 
 exception MatchingFailure;;
@@ -192,6 +226,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 ->