From b78de5584633b864248519d9f7cd9f86a0005c24 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 28 Oct 2011 08:40:50 +0000 Subject: [PATCH] New management of the resulting substitution in deep eq. We reduced several time the goal vs the active table, possibly resulting in a clash of names generating cyclic substitutions. --- .../components/ng_paramodulation/nCicProof.ml | 99 +++++-------------- .../ng_paramodulation/superposition.ml | 50 +++++++--- 2 files changed, 60 insertions(+), 89 deletions(-) diff --git a/matita/components/ng_paramodulation/nCicProof.ml b/matita/components/ng_paramodulation/nCicProof.ml index 3f30a85c3..60f2cbafc 100644 --- a/matita/components/ng_paramodulation/nCicProof.ml +++ b/matita/components/ng_paramodulation/nCicProof.ml @@ -64,7 +64,6 @@ let debug c _ = c;; extract t ;; - let mk_predicate status hole_type amount ft p1 vl = let rec aux t p = match p with @@ -79,10 +78,10 @@ let debug c _ = c;; end) in let module Pp = Pp.Pp(NCicBlob) in - prerr_endline ("term: " ^ Pp.pp_foterm ft); - prerr_endline ("path: " ^ String.concat "," + (* prerr_endline ("term: " ^ Pp.pp_foterm ft); + prerr_endline ("path: " ^ String.concat "," (List.map string_of_int p1)); - prerr_endline ("leading to: " ^ Pp.pp_foterm t); + prerr_endline ("leading to: " ^ Pp.pp_foterm t); *) assert false | Terms.Node l -> let l = @@ -202,6 +201,11 @@ let debug c _ = c;; let module Pp = Pp.Pp(NCicBlob) in let module Subst = FoSubst in + let compose subst1 subst2 = + let s1 = List.map (fun (x,t) -> (x, Subst.apply_subst subst2 t)) subst1 in + let s2 = List.filter (fun (m,_) -> not (List.mem_assoc m s1)) subst2 + in s1 @ s2 + in let position i l = let rec aux = function | [] -> assert false @@ -238,24 +242,7 @@ let debug c _ = c;; let lit = Subst.apply_subst subst lit in extract status 0 [] lit in (* composition of all subst acting on goal *) - let res_subst = - let rec rsaux ongoal acc = - function - | [] -> acc (* is the final subst for refl *) - | id::tl when ongoal -> - let lit,vl,proof = get_literal id in - (match proof with - | Terms.Exact _ -> rsaux ongoal acc tl - | Terms.Step (_, _, _, _, _, s) -> - rsaux ongoal (s@acc) tl) - | id::tl -> - (* subst is the the substitution for refl *) - rsaux (id=mp) subst tl - in - let r = rsaux false [] steps in - (* prerr_endline ("res substitution: " ^ Pp.pp_substitution r); - prerr_endline ("\n" ^ "subst: " ^ Pp.pp_substitution subst); *) - r + let res_subst = subst in let rec aux ongoal seen = function | [] -> NCic.Rel 1 @@ -268,16 +255,17 @@ let debug c _ = c;; let refl = if demod then NCic.Implicit `Term else mk_refl eq_ty in - (* prerr_endline ("Reached m point, id=" ^ (string_of_int id)); + (* prerr_endline ("Reached m point, id=" ^ (string_of_int id)); (NCic.LetIn ("clause_" ^ string_of_int id, eq_ty, refl, aux true ((id,([],lit))::seen) (id::tl))) *) - NCicSubstitution.subst status + let res = NCicSubstitution.subst status ~avoid_beta_redexes:true ~no_implicit:false refl (aux true ((id,([],lit))::seen) (id::tl)) + in res else match proof with | Terms.Exact _ when tl=[] -> - (* prerr_endline ("Exact (tl=[]) for " ^ (string_of_int id));*) + (* prerr_endline ("Exact (tl=[]) for " ^ (string_of_int id)); *) aux ongoal seen tl | Terms.Step _ when tl=[] -> assert false | Terms.Exact ft -> @@ -288,21 +276,27 @@ let debug c _ = c;; close_with_lambdas vl (extract status amount vl ft), aux ongoal ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl) - *) - NCicSubstitution.subst status + *) + let res = NCicSubstitution.subst status ~avoid_beta_redexes:true ~no_implicit:false (close_with_lambdas vl (extract status amount vl ft)) (aux ongoal ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl) + in res | Terms.Step (_, id1, id2, dir, pos, subst) -> + (* prerr_endline (if ongoal then "on goal" else "not on goal"); + prerr_endline (Pp.pp_substitution subst); *) + (* let subst = if ongoal then res_subst else subst in *) let id, id1,(lit,vl,proof) = if ongoal then let lit,vl,proof = get_literal id1 in - id1,id,(Subst.apply_subst res_subst lit, - Subst.filter res_subst vl, proof) + id1,id,(Subst.apply_subst res_subst lit, + Subst.filter res_subst vl, proof) else id,id1,(lit,vl,proof) in (* free variables remaining in the goal should not be abstracted: we do not want to prove a generalization *) + (* prerr_endline ("variables = " ^ String.concat "," + (List.map string_of_int vl)); *) let vl = if ongoal then [] else vl in let proof_of_id id = let vars = List.rev (vars_of id seen) in @@ -314,37 +308,6 @@ let debug c _ = c;; in let p_id1 = proof_of_id id1 in let p_id2 = proof_of_id id2 in -(* - let morphism, l, r = - let p = - if (ongoal=true) = (dir=Terms.Left2Right) then - p_id2 - else sym p_id2 in - let id1_ty = ty_of id1 seen in - let id2_ty,l,r = - match ty_of id2 seen with - | Terms.Node [ _; t; l; r ] -> - extract status amount vl (Subst.apply_subst subst t), - extract status amount vl (Subst.apply_subst subst l), - extract status amount vl (Subst.apply_subst subst r) - | _ -> assert false - in - (*prerr_endline "mk_predicate :"; - if ongoal then prerr_endline "ongoal=true" - else prerr_endline "ongoal=false"; - prerr_endline ("id=" ^ string_of_int id); - prerr_endline ("id1=" ^ string_of_int id1); - prerr_endline ("id2=" ^ string_of_int id2); - prerr_endline ("Positions :" ^ - (String.concat ", " - (List.map string_of_int pos)));*) - mk_morphism - p amount (Subst.apply_subst subst id1_ty) pos vl, - l,r - in - let rewrite_step = iff1 morphism p_id1 - in -*) let pred, hole_type, l, r = let id1_ty = ty_of id1 seen in let id2_ty,l,r = @@ -355,19 +318,9 @@ let debug c _ = c;; extract status amount vl (Subst.apply_subst subst r) | _ -> assert false in - (* - prerr_endline "mk_predicate :"; - if ongoal then prerr_endline "ongoal=true" - else prerr_endline "ongoal=false"; - prerr_endline ("id=" ^ string_of_int id); - prerr_endline ("id1=" ^ string_of_int id1 - ^": " ^ Pp.pp_foterm id1_ty); - prerr_endline ("id2=" ^ string_of_int id2 - ^ ": " ^ NCicPp.ppterm [][][] id2_ty); - prerr_endline ("Positions :" ^ - (String.concat ", " - (List.map string_of_int pos)));*) - mk_predicate status + (* let _ = prerr_endline ("body = " ^(Pp.pp_foterm id1_ty)) + in *) + mk_predicate status id2_ty amount (Subst.apply_subst subst id1_ty) pos vl, id2_ty, l,r diff --git a/matita/components/ng_paramodulation/superposition.ml b/matita/components/ng_paramodulation/superposition.ml index cdb34969f..50b31317a 100644 --- a/matita/components/ng_paramodulation/superposition.ml +++ b/matita/components/ng_paramodulation/superposition.ml @@ -374,12 +374,17 @@ module Superposition (B : Orderings.Blob) = bag, maxvar, res ;; - let rewrite_eq ~unify l r ty vl table = + (* rewrite_eq check if in table there an equation matching l=r; + used in subsumption and deep_eq. In deep_eq, we need to match + several times times w.r.t. the same table, hence we should refresh + the retrieved clauses, to avoid clashes of variables *) + + let rewrite_eq ~refresh ~unify maxvar l r ty vl table = let retrieve = if unify then IDX.DT.retrieve_unifiables else IDX.DT.retrieve_generalizations in let lcands = retrieve table l in let rcands = retrieve table r in - let f b c = + let f b c = let id, dir, l, r, vl = match c with | (d, (id,Terms.Equation (l,r,ty,_),vl,_))-> id, d, l, r, vl @@ -398,8 +403,12 @@ module Superposition (B : Orderings.Blob) = | [] -> None | (id2,dir,c,vl1)::tl -> try + let c,maxvar = if refresh then + let maxvar,_,r = Utils.relocate maxvar vl1 [] in + Subst.apply_subst r c,maxvar + else c,maxvar in let subst = Unif.unification (* (vl@vl1) *) locked_vars c t in - Some (id2, dir, subst) + Some (id2, dir, subst, maxvar) with FoUnif.UnificationFailure _ -> aux tl in aux (cands1 @ cands2) @@ -409,9 +418,9 @@ module Superposition (B : Orderings.Blob) = match lit with | Terms.Predicate _ -> assert false | Terms.Equation (l,r,ty,_) -> - match rewrite_eq ~unify l r ty vl table with + match rewrite_eq ~refresh:false ~unify maxvar l r ty vl table with | None -> None - | Some (id2, dir, subst) -> + | Some (id2, dir, subst, maxvar) -> let id_t = Terms.Node [ Terms.Leaf B.eqP; ty; r; r ] in build_new_clause bag maxvar (fun _ -> true) Terms.Superposition id_t subst id id2 [2] dir @@ -423,38 +432,46 @@ module Superposition (B : Orderings.Blob) = (* id refers to a clause proving contextl l = contextr r *) let rec deep_eq ~unify l r ty pos contextl contextr table acc = + (* let _ = prerr_endline ("pos = " ^ String.concat "," + (List.map string_of_int pos)) in *) match acc with | None -> None | Some(bag,maxvar,(id,lit,vl,p),subst) -> (* prerr_endline ("input subst = "^Pp.pp_substitution subst); *) + (* prerr_endline ("l prima =" ^ Pp.pp_foterm l); *) + (* prerr_endline ("r prima =" ^ Pp.pp_foterm r); *) let l = Subst.apply_subst subst l in let r = Subst.apply_subst subst r in + (* prerr_endline ("l dopo =" ^ Pp.pp_foterm l); *) + (* prerr_endline ("r dopo =" ^ Pp.pp_foterm r); *) try let subst1 = Unif.unification (* vl *) [] l r in let lit = match lit with Terms.Predicate _ -> assert false | Terms.Equation (l,r,ty,o) -> - Terms.Equation (FoSubst.apply_subst subst1 l, - FoSubst.apply_subst subst1 r, ty, o) + let l = Subst.apply_subst subst1 l in + let r = Subst.apply_subst subst1 r in + Terms.Equation (l, r, ty, o) in Some(bag,maxvar,(id,lit,vl,p),Subst.concat subst1 subst) with FoUnif.UnificationFailure _ -> - match rewrite_eq ~unify l r ty vl table with - | Some (id2, dir, subst1) -> + match rewrite_eq ~refresh:true ~unify maxvar l r ty vl table with + | Some (id2, dir, subst1, maxvar) -> (* prerr_endline ("subst1 = "^Pp.pp_substitution subst1); - prerr_endline ("old subst = "^Pp.pp_substitution subst);*) + prerr_endline ("old subst = "^Pp.pp_substitution subst); *) let newsubst = Subst.concat subst1 subst in let id_t = FoSubst.apply_subst newsubst (Terms.Node[Terms.Leaf B.eqP;ty;contextl r;contextr r]) in - (match + (match build_new_clause_reloc bag maxvar (fun _ -> true) Terms.Superposition id_t - subst1 id id2 (pos@[2]) dir - with + subst1 id id2 (pos@[2]) dir + with | Some ((bag, maxvar), c), r -> - (* prerr_endline ("r = "^Pp.pp_substitution r); *) + (* prerr_endline ("creo "^ Pp.pp_unit_clause c); *) + (* prerr_endline ("r = "^Pp.pp_substitution r); *) let newsubst = Subst.flat (Subst.concat r subst) in Some(bag,maxvar,c,newsubst) @@ -645,7 +662,7 @@ module Superposition (B : Orderings.Blob) = let bag, clause = if no_demod then bag, clause else demodulate bag clause table in - let _ = debug (lazy ("demodulated goal : " + let _ = debug(lazy ("demodulated goal : " ^ Pp.pp_unit_clause clause)) in if List.exists (are_alpha_eq clause) g_actives then None @@ -668,12 +685,13 @@ module Superposition (B : Orderings.Blob) = | None -> Some (bag,clause) | Some (bag,maxvar,cl,subst) -> debug (lazy "Goal subsumed"); + debug (lazy ("subst in superpos: " ^ Pp.pp_substitution subst)); raise (Success (bag,maxvar,cl,subst)) (* match is_subsumed ~unify:true bag maxvar clause table with | None -> Some (bag, clause) | Some ((bag,maxvar),c) -> - prerr_endline "Goal subsumed"; + debug (lazy "Goal subsumed"); raise (Success (bag,maxvar,c)) *) ;; -- 2.39.2