From d7f3ff62899afb162cb2825af91de72fe6d8dc85 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 29 Oct 2008 12:41:38 +0000
Subject: [PATCH] Enforcing the disjoint invariant between metasenvs.

---
 .../tactics/paramodulation/founif.ml          | 43 +++++++++++++++++--
 1 file changed, 39 insertions(+), 4 deletions(-)

diff --git a/helm/software/components/tactics/paramodulation/founif.ml b/helm/software/components/tactics/paramodulation/founif.ml
index 2a9de5ffa..87550f76a 100644
--- 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
 ;;
 
-- 
2.39.2