many checks guarded with if Utils.debug_metas

[helm.git] / helm / software / components / tactics / paramodulation / founif.ml

diff --git a/helm/software/components/tactics/paramodulation/founif.ml b/helm/software/components/tactics/paramodulation/founif.ml
index 2a9de5ffa8c2d74440dbd2551debdf09ba499ce1..b635599515b75ba0d77fc7f6e7cbe793df66ee9a 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,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;;
@@ -190,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 ->