From 1a65db059b643422fc8eded4f4e03b512071515b Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 5 May 2006 14:56:30 +0000 Subject: [PATCH] New version of deep_subsumption --- components/tactics/paramodulation/equality.ml | 26 ++++++- .../tactics/paramodulation/equality.mli | 2 +- .../tactics/paramodulation/saturation.ml | 76 +++++++++++-------- 3 files changed, 67 insertions(+), 37 deletions(-) diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml index c4aaa1ca4..5248a6a92 100644 --- a/components/tactics/paramodulation/equality.ml +++ b/components/tactics/paramodulation/equality.ml @@ -355,6 +355,17 @@ let string_of_proof_new ?(names=[]) p gp = gp) ;; +let rec depend eq id = + let (_,(p,_),(_,_,_,_),_,ideq) = open_equality eq in + if id = ideq then true else + match p with + Exact _ -> false + | Step (_,(_,id1,(_,id2),_)) -> + let eq1 = Hashtbl.find id_to_eq id1 in + let eq2 = Hashtbl.find id_to_eq id2 in + depend eq1 id || depend eq1 id2 +;; + let ppsubst = ppsubst ~names:[] (* returns an explicit named subst and a list of arguments for sym_eq_URI *) @@ -537,6 +548,7 @@ let build_proof_step subst p1 p2 pos l r pred = CicSubstitution.subst (Cic.Rel 1) t in match body,pos with +(* |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Left -> let third = CicSubstitution.subst (Cic.Implicit None) third in let uri_trans = LibraryObjects.trans_eq_URI ~eq in @@ -689,6 +701,7 @@ let build_proof_step subst p1 p2 pos l r pred = in mk_trans uri_trans ty lhs pred_of_what pred_of_other p1 (inject ty rhs other what p2) +*) | _, Utils.Left -> mk_eq_ind (Utils.eq_ind_URI ()) ty what pred p1 other p2 | _, Utils.Right -> @@ -708,7 +721,7 @@ let build_proof_term_new proof = aux proof ;; -let wfo goalproof = +let wfo goalproof proof = let rec aux acc id = let p,_,_ = proof_of_id id in match p with @@ -718,7 +731,12 @@ let wfo goalproof = let acc = if not (List.mem id2 acc) then aux acc id2 else acc in id :: acc in - List.fold_left (fun acc (_,id,_,_) -> aux acc id) [] goalproof + let acc = + match proof with + | Exact _ -> [] + | Step (_,(_,id1, (_,id2), _)) -> aux (aux [] id1) id2 + in + List.fold_left (fun acc (_,id,_,_) -> aux acc id) acc goalproof ;; let string_of_id names id = @@ -735,8 +753,8 @@ let string_of_id names id = with Not_found -> assert false -let pp_proof names goalproof = - String.concat "\n" (List.map (string_of_id names) (wfo goalproof)) ^ +let pp_proof names goalproof proof = + String.concat "\n" (List.map (string_of_id names) (wfo goalproof proof)) ^ "\ngoal is demodulated with " ^ (String.concat " " ((List.map (fun (_,i,_,_) -> string_of_int i) goalproof))) diff --git a/components/tactics/paramodulation/equality.mli b/components/tactics/paramodulation/equality.mli index 2d7e48e5c..1a2a3a280 100644 --- a/components/tactics/paramodulation/equality.mli +++ b/components/tactics/paramodulation/equality.mli @@ -46,7 +46,7 @@ and old_proof = and goal_proof = (Utils.pos * int * substitution * Cic.term) list -val pp_proof: (Cic.name option) list -> goal_proof -> string +val pp_proof: (Cic.name option) list -> goal_proof -> new_proof -> string val empty_subst : substitution val apply_subst : substitution -> Cic.term -> Cic.term diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index 1cb6d3514..6b1b65e27 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -358,7 +358,7 @@ let check_for_deep_subsumption env active_table eq = let _,_,(eq_ty, left, right, order),metas,id = Equality.open_equality eq in if id = 14242 then assert false; - let check deep l r = + let check_subsumed deep l r = let eqtmp = Equality.mk_tmp_equality(0,(eq_ty,l,r,Utils.Incomparable),metas)in match Indexing.subsumption env active_table eqtmp with @@ -370,18 +370,24 @@ let check_for_deep_subsumption env active_table eq = Equality.string_of_equality ~env eq' ^ "\n\n"); true in - let rec aux b = function - | Cic.Rel n, Cic.Rel m -> if n = m then true else false - | ((Cic.Appl l) as left),((Cic.Appl l') as right) -> - check b left right || - (try - List.for_all2 (fun t t' -> aux true (t,t')) (List.tl l) (List.tl l') - with Invalid_argument _ -> false) - | (Cic.Meta _),_ - | _,(Cic.Meta _) -> false - | _ -> false + let rec aux b (ok_so_far, subsumption_used) t1 t2 = + match t1,t2 with + | t1, t2 when not ok_so_far -> ok_so_far, subsumption_used + | t1, t2 when subsumption_used -> t1 = t2, subsumption_used + | Cic.Appl (h1::l),Cic.Appl (h2::l') when h1 = h2 -> + let rc = check_subsumed b t1 t1 in + if rc then + true, true + else + (try + List.fold_left2 + (fun (ok_so_far, subsumption_used) t t' -> + aux true (ok_so_far, subsumption_used) t t') + (ok_so_far, subsumption_used) l l' + with Invalid_argument _ -> false,subsumption_used) + | _ -> false, subsumption_used in - aux false (left,right) + fst (aux false (true,false) left right) ;; (* @@ -618,21 +624,21 @@ let simplify_goals env goals ?passive active = (** simplifies active usign new *) let backward_simplify_active env new_pos new_table min_weight active = let active_list, active_table = active in - let active_list, newa = + let active_list, newa, pruned = List.fold_right - (fun equality (res, newn) -> - let ew, _, _, _,_ = Equality.open_equality equality in + (fun equality (res, newn,pruned) -> + let ew, _, _, _,id = Equality.open_equality equality in if ew < min_weight then - equality::res, newn + equality::res, newn,pruned else match forward_simplify env (Utils.Positive, equality) (new_pos, new_table) with - | None -> res, newn + | None -> res, newn, id::pruned | Some e -> if Equality.compare equality e = 0 then - e::res, newn + e::res, newn, pruned else - res, e::newn) - active_list ([], []) + res, e::newn, pruned) + active_list ([], [],[]) in let find eq1 where = List.exists (Equality.meta_convertibility_eq eq1) where @@ -891,6 +897,7 @@ let print_goals goals = ;; let check_if_goal_is_subsumed env ((cicproof,proof),menv,ty) table = + prerr_endline "check_goal_subsumed"; match ty with | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] when UriManager.eq uri (LibraryObjects.eq_URI ()) -> @@ -902,8 +909,10 @@ let check_if_goal_is_subsumed env ((cicproof,proof),menv,ty) table = | Some (subst, equality ) -> let (_,(np,p),(ty,l,r,_),m,id) = Equality.open_equality equality in + prerr_endline "1"; let p = Equality.apply_subst subst (Equality.build_proof_term_old p) in + prerr_endline "2"; let newp = let rec repl = function | Equality.ProofGoalBlock (_, gp) -> @@ -919,9 +928,12 @@ let check_if_goal_is_subsumed env ((cicproof,proof),menv,ty) table = in repl proof in + prerr_endline "3"; let newcicp,np,subst,cicmenv = - cicproof,np, subst, Equality.apply_subst_metasenv subst (m @ menv) + cicproof,np, subst, + Equality.apply_subst_metasenv subst (m @ menv) in + prerr_endline "."; Some ((newcicp,np,subst,cicmenv), (newp, Equality.apply_subst_metasenv subst m @ menv )) @@ -1119,8 +1131,8 @@ and given_clause_fullred_aux dbd env goals theorems passive active = (* weight_age_counter := !weight_age_counter + 1; *) given_clause_fullred dbd env goals theorems passive active | Some current -> - prerr_endline (Printf.sprintf "selected sipl: %s" - (Equality.string_of_equality ~env current)); +(* prerr_endline (Printf.sprintf "selected simpl: %s" + (Equality.string_of_equality ~env current));*) let t1 = Unix.gettimeofday () in let new' = infer env current active in let _ = @@ -1478,6 +1490,7 @@ let saturate let goal' = goal in let uri, metasenv, meta_proof, term_to_prove = proof in let _, context, goal = CicUtil.lookup_meta goal' metasenv in + let names = names_of_context context in let eq_indexes, equalities, maxm = find_equalities context proof in let new_meta_goal, metasenv, type_of_goal = let irl = @@ -1555,6 +1568,11 @@ let saturate (proof, proof_menv))) (* OLD *) -> prerr_endline "OK, found a proof!"; + + prerr_endline "NEWPROOF"; + (* prerr_endline (Equality.string_of_proof_new ~names newproof + * goalproof);*) + prerr_endline (Equality.pp_proof names goalproof newproof); (* generation of the old proof *) let cic_proof = Equality.build_proof_term_old proof in @@ -1607,15 +1625,10 @@ let saturate in (* pp new/old proof *) - let names = names_of_context context in (* prerr_endline "OLDPROOF";*) (* prerr_endline (Equality.string_of_proof_old proof);*) (* prerr_endline "OLDPROOFCIC";*) (* prerr_endline (CicPp.pp cic_proof names); *) - prerr_endline "NEWPROOF"; - (* prerr_endline (Equality.string_of_proof_new ~names newproof - * goalproof);*) - prerr_endline (Equality.pp_proof names goalproof); (* prerr_endline "NEWPROOFCIC";*) (* prerr_endline (CicPp.pp cic_proof_new names); *) @@ -1627,9 +1640,8 @@ let saturate in List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv in - let newmetasenv = newmetasenv@proof_menv in let newmetasenv_new = newmetasenv@newproof_menv in - + let newmetasenv = newmetasenv@proof_menv in (* check/refine/... build the new proof *) let newstatus = let cic_proof,newmetasenv,proof_menv,ty, ug = @@ -1670,8 +1682,8 @@ let saturate in if List.length newmetasenv_new <> 0 then prerr_endline - ("Some METAS are still open: " ^ CicMetaSubst.ppmetasenv - [] newmetasenv_new); + ("Some METAS are still open: "(* ^ CicMetaSubst.ppmetasenv + [] newmetasenv_new*)); cic_proof_new, newmetasenv_new, newmetasenv_new,new_ty, newug (* THE OLD PROOF: cic_proof,newmetasenv,proof_menv,oldty,oldug *) in -- 2.39.2