From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 29 Apr 2009 10:47:55 +0000 (+0000)
Subject: many checks guarded with if Utils.debug_metas
X-Git-Tag: make_still_working~4036
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b8934a9598d747662139c74c751b8223bcc19d03;p=helm.git

many checks guarded with if Utils.debug_metas
---

diff --git a/helm/software/components/tactics/paramodulation/founif.ml b/helm/software/components/tactics/paramodulation/founif.ml
index c2df6371c..b63559951 100644
--- a/helm/software/components/tactics/paramodulation/founif.ml
+++ b/helm/software/components/tactics/paramodulation/founif.ml
@@ -206,9 +206,10 @@ let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
   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
+  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;;
diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 97e45522d..99f66f1d1 100644
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -145,7 +145,7 @@ let not_unit_eq ctx eq =
   List.exists 
     (fun (_,_,ty) ->
        try 
-	 let s,_ = CicTypeChecker.type_of_aux' metas ctx ty CicUniv.empty_ugraph
+	 let s,_ = CicTypeChecker.type_of_aux' metas ctx ty CicUniv.oblivion_ugraph
 	 in s = Cic.Sort(Cic.Prop)
        with _ -> 
 	 prerr_endline ("ERROR typing " ^ CicPp.ppterm ty); assert false) metas
@@ -313,7 +313,8 @@ let rec find_matches bag metasenv context ugraph lift_amount term termty =
               Founif.matching 
                 metasenv metas context term (S.lift lift_amount c) ugraph
             in
-	    check_metasenv "founif :" metasenv';
+            if Utils.debug_metas then
+    	      check_metasenv "founif :" metasenv';
             Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
           in
           let c, other =
@@ -517,7 +518,8 @@ let subsumption_aux_all use_unification env table target =
   let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
   let _, context, ugraph = env in
   let metasenv = tmetas in
-  check_for_duplicates metasenv "subsumption_aux_all";
+  if Utils.debug_metas then
+    check_for_duplicates metasenv "subsumption_aux_all";
   let predicate, unif_fun = 
     if use_unification then
       Unification, Founif.unification
@@ -576,12 +578,13 @@ let rec demodulation_aux bag ?from ?(typecheck=false)
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
-  check_for_duplicates metasenv "in input a demodulation aux";
+  if Utils.debug_metas then
+    check_for_duplicates metasenv "in input a demodulation aux";
   let candidates = 
     get_candidates 
       ~env:(metasenv,context,ugraph) (* Unification *) Matching table term 
-  in let candidates = List.filter (fun _,x -> not (not_unit_eq context x)) candidates 
-  in
+  in 
+(*   let candidates = List.filter (fun _,x -> not (not_unit_eq context x)) candidates in *)
   let res =
     match term with
       | C.Meta _ -> None
@@ -899,8 +902,8 @@ let rec betaexpand_term
   | C.Meta (i, l) -> res, lifted_term
   | term ->
       let termty, ugraph =
-(*        C.Implicit None, ugraph *)
-         CicTypeChecker.type_of_aux' metasenv context term ugraph 
+       C.Implicit None, ugraph
+(*          CicTypeChecker.type_of_aux' metasenv context term ugraph  *)
       in
       let candidates = get_candidates Unification table term in
       (* List.iter (fun (_,e) -> debug_print (lazy (Equality.string_of_equality e))) candidates; *)
diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 8f4e54851..7ee7d6b16 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -820,7 +820,8 @@ let find_all_subsumed bag env table (goalproof,menv,ty) =
 	  (fun (subst, equality, swapped) (bag,acc) ->
 	     let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
              let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
-             Indexing.check_for_duplicates cicmenv "from subsumption";
+             if Utils.debug_metas then
+               Indexing.check_for_duplicates cicmenv "from subsumption";
              let bag, p =
 	       if swapped then
                  Equality.symmetric bag eq_ty l id uri m