From 86d27070abaa7844fa53ab83b8a57489cc2d7e1a Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 24 Mar 2006 16:01:08 +0000 Subject: [PATCH] New unification and new matching. --- .../tactics/paramodulation/inference.ml | 130 ++++++++++++++---- .../tactics/paramodulation/saturation.ml | 9 +- components/tactics/paramodulation/utils.ml | 2 - 3 files changed, 108 insertions(+), 33 deletions(-) diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml index 07d95ef86..f5508c8c1 100644 --- a/components/tactics/paramodulation/inference.ml +++ b/components/tactics/paramodulation/inference.ml @@ -367,17 +367,21 @@ let rec is_simple_term = function ;; -let lookup_subst meta subst = +let rec lookup_subst meta subst = match meta with | Cic.Meta (i, _) -> ( - try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t + try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst + in lookup_subst t subst with Not_found -> meta ) - | _ -> assert false + | _ -> meta ;; +let locked menv i = + List.exists (fun (j,_,_) -> i = j) menv +;; -let unification_simple metasenv context t1 t2 ugraph = +let unification_simple locked_menv metasenv context t1 t2 ugraph = let module C = Cic in let module M = CicMetaSubst in let module U = CicUnification in @@ -394,14 +398,24 @@ let unification_simple metasenv context t1 t2 ugraph = let rec unif subst menv s t = let s = match s with C.Meta _ -> lookup s subst | _ -> s and t = match t with C.Meta _ -> lookup t subst | _ -> t + in match s, t with | s, t when s = t -> subst, menv - | C.Meta (i, _), C.Meta (j, _) when i > j -> + | C.Meta (i, _), C.Meta (j, _) + when (locked locked_menv i) &&(locked locked_menv j) -> + raise + (U.UnificationFailure (lazy "Inference.unification.unif")) + | C.Meta (i, _), C.Meta (j, _) when (locked locked_menv i) -> + unif subst menv t s + | C.Meta (i, _), C.Meta (j, _) when (i > j) && not (locked locked_menv j) -> unif subst menv t s | C.Meta _, t when occurs_check subst s t -> raise (U.UnificationFailure (lazy "Inference.unification.unif")) + | C.Meta (i, l), t when (locked locked_menv i) -> + raise + (U.UnificationFailure (lazy "Inference.unification.unif")) | C.Meta (i, l), t -> ( try let _, _, ty = CicUtil.lookup_meta i menv in @@ -437,45 +451,56 @@ let unification_simple metasenv context t1 t2 ugraph = List.rev subst, menv, ugraph ;; +let profiler = HExtlib.profile "flatten" -let unification metasenv1 metasenv2 context t1 t2 ugraph = - let metasenv = metasenv1 metasenv2 in +let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph = + let metasenv = metasenv1 @ metasenv2 in let subst, menv, ug = if not (is_simple_term t1) || not (is_simple_term t2) then ( debug_print (lazy (Printf.sprintf "NOT SIMPLE TERMS: %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2))); - CicUnification.fo_unif metasenv context t1 t2 ugraph + raise (CicUnification .UnificationFailure (lazy "Inference.unification.unif")) ) else - unification_simple metasenv context t1 t2 ugraph + if b then + (* full unification *) + unification_simple [] metasenv context t1 t2 ugraph + else + (* matching: metasenv1 is locked *) + unification_simple metasenv1 metasenv context t1 t2 ugraph in if Utils.debug_res then ignore(check_disjoint_invariant subst menv "unif"); - let subst = + let flatten subst = List.map (fun (i, (context, term, ty)) -> let context = CicMetaSubst.apply_subst_context subst context in let term = CicMetaSubst.apply_subst subst term in let ty = CicMetaSubst.apply_subst subst ty in - (i, (context, term, ty))) subst in -(* - let rec fix_term = function - | (Cic.Meta (i, l) as t) -> - let t' = lookup_subst t subst in - if t <> t' then fix_term t' else t - | Cic.Appl l -> Cic.Appl (List.map fix_term l) - | t -> t + (i, (context, term, ty))) subst in - let rec fix_subst = function - | [] -> [] - | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl) - in - fix_subst subst, menv, ug *) - subst, menv, ug + let flatten subst = profiler.HExtlib.profile flatten subst in + let subst = flatten subst in + subst, menv, ug +;; + +exception MatchingFailure;; + +let matching1 metasenv1 metasenv2 context t1 t2 ugraph = + try + unification_aux false metasenv1 metasenv2 context t1 t2 ugraph + with + CicUnification .UnificationFailure _ -> + raise MatchingFailure ;; +let unification = unification_aux true +;; + + +(* let unification metasenv1 metasenv2 context t1 t2 ugraph = let (subst, metasenv, ugraph) = CicUnification.fo_unif (metasenv1@metasenv2) context t1 t2 ugraph in @@ -484,8 +509,7 @@ let unification metasenv1 metasenv2 context t1 t2 ugraph = (subst, metasenv, ugraph) ;; - -exception MatchingFailure;; +*) (* @@ -603,7 +627,8 @@ let matching metasenv context t1 t2 ugraph = it perform unification in the union metasenv, then check that the first metasenv has not changed *) -let matching metasenv1 metasenv2 context t1 t2 ugraph = + +let matching2 metasenv1 metasenv2 context t1 t2 ugraph = let subst, metasenv, ugraph = try unification metasenv1 metasenv2 context t1 t2 ugraph @@ -621,9 +646,17 @@ let matching metasenv1 metasenv2 context t1 t2 ugraph = ignore(check_disjoint_invariant subst metasenv "qua-2"); (* let us unfold subst *) if metasenv = metasenv1 then - subst, metasenv, ugraph (* everything is fine *) + let subst = + List.map + (fun (i, (context, term, ty)) -> + let context = CicMetaSubst.apply_subst_context subst context in + let term = CicMetaSubst.apply_subst subst term in + let ty = CicMetaSubst.apply_subst subst ty in + (i, (context, term, ty))) subst in + subst, metasenv, ugraph (* everything is fine *) else (* let us unfold subst *) + (* let subst = List.map (fun (i, (context, term, ty)) -> @@ -631,6 +664,7 @@ let matching metasenv1 metasenv2 context t1 t2 ugraph = let term = CicMetaSubst.apply_subst subst term in let ty = CicMetaSubst.apply_subst subst ty in (i, (context, term, ty))) subst in + *) (* let us revert Meta-Meta in subst privileging metasenv1 *) let subst, metasenv = List.fold_left @@ -646,13 +680,51 @@ let matching metasenv1 metasenv2 context t1 t2 ugraph = ((j, (c, Cic.Meta (i, lc), ty))::subst, (i,c,ty)::metasenv') |_ -> s::subst,metasenv) ([],metasenv) subst - in + in (* finally, let us chek again that metasenv = metasenv1 *) if metasenv = metasenv1 then subst, metasenv, ugraph else raise MatchingFailure ;; +(* debug +let matching metasenv1 metasenv2 context t1 t2 ugraph = + let rc1 = + try Some (matching1 metasenv1 metasenv2 context t1 t2 ugraph) + with MatchingFailure -> None + in + let rc2 = + try + Some (matching2 metasenv1 metasenv2 context t1 t2 ugraph) + with MatchingFailure -> None + in + match rc1,rc2 with + | Some (s,m,g) , None -> + prerr_endline (CicPp.ppterm t1); + prerr_endline (CicPp.ppterm t2); + prerr_endline "SOLO NOI"; + prerr_endline (CicMetaSubst.ppsubst s); + s,m,g + | None , Some _ -> + prerr_endline (CicPp.ppterm t1); + prerr_endline (CicPp.ppterm t2); + prerr_endline "SOLO LUI"; + assert false + | None, None -> raise MatchingFailure + | Some (s,m,g), Some (s',m',g') -> + let s = List.sort (fun (i,_) (j,_) -> i - j) s in + let s' = List.sort (fun (i,_) (j,_) -> i - j) s' in + if s <> s' then + begin + prerr_endline (CicMetaSubst.ppsubst s); + prerr_endline (CicMetaSubst.ppsubst s'); + prerr_endline (CicPp.ppterm t1); + prerr_endline (CicPp.ppterm t2); + end; + s,m,g +*) +let matching = matching1;; + let check_eq context msg eq = let w, proof, (eq_ty, left, right, order), metas, args = eq in if not (fst (CicReduction.are_convertible ~metasenv:metas context eq_ty diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index b3fa5f3fc..b6678683d 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -468,8 +468,12 @@ let infer env sign current (active_list, active_table) = let neg, pos = infer_positive table tl in neg, res @ pos in + let maxm, copy_of_current = Inference.fix_metas !maxmeta current in + maxmeta := maxm; let curr_table = Indexing.index Indexing.empty current in - let neg, pos = infer_positive curr_table active_list in + let neg, pos = + infer_positive curr_table ((sign,copy_of_current)::active_list) + in if Utils.debug_metas then ignore(List.map (function current -> @@ -1774,7 +1778,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active = " LOCALMAX: " ^ string_of_int !Indexing.local_max ^ " #ACTIVES: " ^ string_of_int (size_of_active active) ^ " #PASSIVES: " ^ string_of_int (size_of_passive passive)); - if (size_of_active active) mod 54 = 0 then + if (size_of_active active) mod 50 = 0 then (let s = Printf.sprintf "actives:\n%s\n" (String.concat "\n" ((List.map @@ -1828,6 +1832,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active = forward_simpl_time := !forward_simpl_time +. (time2 -. time1); match res with | None -> + (* weight_age_counter := !weight_age_counter + 1; *) given_clause_fullred dbd env goals theorems passive active | Some (sign, current) -> if (sign = Negative) && (is_identity env current) then ( diff --git a/components/tactics/paramodulation/utils.ml b/components/tactics/paramodulation/utils.ml index 8fb1d42bc..db19e87d1 100644 --- a/components/tactics/paramodulation/utils.ml +++ b/components/tactics/paramodulation/utils.ml @@ -41,8 +41,6 @@ let print_metasenv metasenv = ;; - - let print_subst ?(prefix="\n") subst = String.concat prefix (List.map -- 2.39.2