From b3e08a6954c8b6946f42f5c7e0bed7912d5ac87c Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 4 Nov 2008 15:13:34 +0000 Subject: [PATCH] Calling unification instead of matching when checking for subsumption might instantiate the goal with variables in table (while they are supposed to be disjoint). --- .../components/tactics/paramodulation/founif.ml | 7 +++++++ .../tactics/paramodulation/indexing.ml | 7 ++++--- .../tactics/paramodulation/saturation.ml | 17 ++++++++++------- .../components/tactics/paramodulation/utils.ml | 2 +- 4 files changed, 22 insertions(+), 11 deletions(-) diff --git a/helm/software/components/tactics/paramodulation/founif.ml b/helm/software/components/tactics/paramodulation/founif.ml index 87550f76a..c2df6371c 100644 --- a/helm/software/components/tactics/paramodulation/founif.ml +++ b/helm/software/components/tactics/paramodulation/founif.ml @@ -225,6 +225,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 -> diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index 8f696d6f3..77a377a88 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -367,6 +367,7 @@ let rec find_all_matches ?(unif_fun=Founif.unification) let module S = CicSubstitution in let module M = CicMetaSubst in let module HL = HelmLibraryObjects in + (* prerr_endline ("matching " ^ CicPp.ppterm term); *) let cmp = !Utils.compare_terms in let check = match termty with C.Implicit None -> false | _ -> true in function @@ -537,7 +538,7 @@ let subsumption_aux_all use_unification env table target = let what' = Subst.apply_subst subst what in let other' = Subst.apply_subst subst other in let subst', menv', ug' = - unif_fun metasenv m context what' other' ugraph + unif_fun [] menv context what' other' ugraph in (match Subst.merge_subst_if_possible subst subst' with | None -> ok_all what leftorright tl @@ -555,7 +556,7 @@ let subsumption_all x y z = ;; let unification_all x y z = - subsumption_aux_all true x y z + prerr_endline "unification_all"; subsumption_aux_all true x y z ;; let rec demodulation_aux bag ?from ?(typecheck=false) @@ -752,7 +753,7 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target = in let res = - demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left + demodulation_aux bag ~from:"from3" metasenv' context ugraph table 0 left in if Utils.debug_res then check_res res "demod result"; let newmeta, newtarget = diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index b2970d209..c8ab4e428 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -820,8 +820,8 @@ let check_if_goal_is_subsumed bag ((_,ctx,_) as env) table (goalproof,menv,ty) = Equality.mk_equality bag (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv) in -(* match Indexing.subsumption env table goal_equation with*) - match Indexing.unification env table goal_equation with + match Indexing.subsumption env table goal_equation with + (* match Indexing.unification env table goal_equation with *) | Some (subst, equality, swapped ) -> (* prerr_endline @@ -862,7 +862,8 @@ let find_all_subsumed bag maxm env table (goalproof,menv,ty) = else p in (goalproof, p, id, subst, cicmenv)) - (Indexing.unification_all env table goal_equation) + (Indexing.subsumption_all env table goal_equation) + (* (Indexing.unification_all env table goal_equation) *) | _ -> assert false ;; @@ -882,7 +883,7 @@ let check_if_goal_is_identity env = function let reflproof = Equality.Exact (Equality.refl_proof uri eq_ty left) in let m = Subst.apply_subst_metasenv s m in Some (goalproof, reflproof, 0, s,m) - with _ -> None) + with CicUnification.UnificationFailure _ -> None) | _ -> None ;; @@ -1592,7 +1593,7 @@ let all_subsumed bag maxm status active passive = let cleaned_goal = Utils.remove_local_context type_of_goal in let canonical_menv,other_menv = List.partition (fun (_,c,_) -> c = context) metasenv in - prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv)); + (* prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv)); *) let metasenv = List.map (fun (i,_,ty)-> (i,[],ty)) canonical_menv in let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in debug_print (lazy (string_of_int (List.length (fst active)))); @@ -1612,6 +1613,7 @@ let all_subsumed bag maxm status active passive = match (check_if_goal_is_identity env goal) with None -> subsumed | Some id -> id::subsumed in + debug_print (lazy "dopo subsumed"); let res = List.map (fun @@ -1623,7 +1625,8 @@ let all_subsumed bag maxm status active passive = let uri, metasenv, subst, meta_proof, term_to_prove, attrs = proof in let proof = uri, other_menv@metasenv, subst, meta_proof, term_to_prove, attrs in (subst, proof,gl)) subsumed_or_id - in res, !maxmeta + in + res, !maxmeta let given_clause @@ -1650,7 +1653,7 @@ let given_clause let cleaned_goal = Utils.remove_local_context type_of_goal in let canonical_menv,other_menv = List.partition (fun (_,c,_) -> c = context) metasenv in - prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv)); + (* prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv)); *) Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *) let canonical_menv = List.map (fun (i,_,ty)-> (i,[],ty)) canonical_menv in let metasenv' = List.filter (fun (i,_,_)->i<>goalno) canonical_menv in diff --git a/helm/software/components/tactics/paramodulation/utils.ml b/helm/software/components/tactics/paramodulation/utils.ml index 8a2722bb6..a85ccc674 100644 --- a/helm/software/components/tactics/paramodulation/utils.ml +++ b/helm/software/components/tactics/paramodulation/utils.ml @@ -25,7 +25,7 @@ (* $Id$ *) -let time = true;; +let time = false;; let debug = false;; let debug_metas = false;; let debug_res = false;; -- 2.39.2