Enforcing the disjoint invariant between metasenvs.

diff --git a/helm/software/components/tactics/paramodulation/founif.ml b/helm/software/components/tactics/paramodulation/founif.ml
index 2a9de5ffa8c2d74440dbd2551debdf09ba499ce1..87550f76aa20c2eed4478e0271aa65900c118af2 100644 (file)
--- a/helm/software/components/tactics/paramodulation/founif.ml
+++ b/helm/software/components/tactics/paramodulation/founif.ml
@@ -141,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
@@ -173,6 +203,11 @@ 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 *)
+  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
+  let _ = check_for_duplicates menv "unif_aux after" in
+    check_metasenv "unification_aux after 1" menv;
     subst, menv, ug
 ;;