From b8934a9598d747662139c74c751b8223bcc19d03 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 29 Apr 2009 10:47:55 +0000 Subject: [PATCH] many checks guarded with if Utils.debug_metas --- .../tactics/paramodulation/founif.ml | 7 ++++--- .../tactics/paramodulation/indexing.ml | 19 +++++++++++-------- .../tactics/paramodulation/saturation.ml | 3 ++- 3 files changed, 17 insertions(+), 12 deletions(-) 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 -- 2.39.2