From d7f3ff62899afb162cb2825af91de72fe6d8dc85 Mon Sep 17 00:00:00 2001 From: Andrea Asperti 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