From bc532ce9c59e1644e02e6c0663855164c2400a40 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 5 Apr 2006 12:07:51 +0000 Subject: [PATCH] the tactic now returns as open goals the open metas in the proof subsumption is now used correctly in given_clause_fullred --- components/tactics/paramodulation/indexing.ml | 31 ++-- .../tactics/paramodulation/indexing.mli | 2 +- .../tactics/paramodulation/inference.ml | 6 +- .../tactics/paramodulation/inference.mli | 1 + .../tactics/paramodulation/saturation.ml | 134 ++++++++++++------ .../tactics/paramodulation/saturation.mli | 2 +- 6 files changed, 114 insertions(+), 62 deletions(-) diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml index e6a2463c0..873cc5698 100644 --- a/components/tactics/paramodulation/indexing.ml +++ b/components/tactics/paramodulation/indexing.ml @@ -407,7 +407,13 @@ let find_all_matches (* returns true if target is subsumed by some equality in table *) -let subsumption env table target = +let subsumption env table target = + (* + let print_res l = + prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug, + ((pos,equation),_)) -> Inference.string_of_equality equation)l)) + in + *) let _, _, (ty, left, right, _), tmetas = target in let metasenv, context, ugraph = env in let metasenv = tmetas in @@ -434,16 +440,18 @@ let subsumption env table target = find_all_matches ~unif_fun:Inference.matching metasenv context ugraph 0 left ty leftc in +(* print_res leftr;*) let rec ok what = function - | [] -> false, [] - | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m)), _))::tl -> + | [] -> None + | (_, subst, menv, ug, ((pos,equation),_))::tl -> + let _, _, (_, l, r, o), m = equation in try let other = if pos = Utils.Left then r else l in let subst', menv', ug' = let t1 = Unix.gettimeofday () in try let r = - Inference.matching metasenv menv context what other ugraph + Inference.matching metasenv m context what other ugraph in let t2 = Unix.gettimeofday () in match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1); @@ -455,15 +463,13 @@ let subsumption env table target = in (match merge_if_possible subst subst' with | None -> ok what tl - | Some s -> true, s) + | Some s -> Some (s, equation)) with Inference.MatchingFailure -> ok what tl in - let r, subst = ok right leftr in - let r, s = - if r then - true, subst - else + match ok right leftr with + | Some _ as res -> res + | None -> let rightr = match right with | Cic.Meta _ -> [] @@ -472,14 +478,13 @@ let subsumption env table target = find_all_matches ~unif_fun:Inference.matching metasenv context ugraph 0 right ty rightc in +(* print_res rightr;*) ok left rightr - in (* (if r then *) (* debug_print *) (* (lazy *) (* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *) (* (Inference.string_of_equality target) (Utils.print_subst s)))); *) - r, s ;; let rec demodulation_aux ?from ?(typecheck=false) @@ -709,6 +714,8 @@ let rec demodulation_equality ?from newmeta env table sign target = prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what)); prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other)); prerr_endline ("+++++++++++++subst: " ^ (Inference.ppsubst subst)); + prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv [] + newmenv)); raise exc; else () in diff --git a/components/tactics/paramodulation/indexing.mli b/components/tactics/paramodulation/indexing.mli index d10d7e6d8..5af20df5c 100644 --- a/components/tactics/paramodulation/indexing.mli +++ b/components/tactics/paramodulation/indexing.mli @@ -49,7 +49,7 @@ val subsumption : Cic.metasenv * Cic.context * CicUniv.universe_graph -> Index.t -> Inference.equality -> - bool * Inference.substitution + (Inference.substitution * Inference.equality) option val superposition_left : int -> Cic.conjecture list * Cic.context * CicUniv.universe_graph -> diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml index 547a23559..a3894fd84 100644 --- a/components/tactics/paramodulation/inference.ml +++ b/components/tactics/paramodulation/inference.ml @@ -541,11 +541,11 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph = subst, menv with CicUtil.Meta_not_found m -> let names = names_of_context context in - debug_print - (lazy + (*debug_print + (lazy*) prerr_endline (Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m (CicPp.pp t1 names) (CicPp.pp t2 names) - (print_metasenv menv) (print_metasenv metasenv))); + (print_metasenv menv) (print_metasenv metasenv)); assert false ) | _, C.Meta _ -> unif subst menv t s diff --git a/components/tactics/paramodulation/inference.mli b/components/tactics/paramodulation/inference.mli index 107e3b819..b08054ca4 100644 --- a/components/tactics/paramodulation/inference.mli +++ b/components/tactics/paramodulation/inference.mli @@ -142,4 +142,5 @@ val metas_of_proof: proof -> int list val fix_metas: int -> equality -> int * equality val apply_subst: substitution -> Cic.term -> Cic.term +val apply_subst_metasenv: substitution -> Cic.metasenv -> Cic.metasenv val ppsubst: substitution -> string diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index 07c6c6012..e88a061a3 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -87,7 +87,7 @@ let test eq = false type result = | ParamodulationFailure - | ParamodulationSuccess of Inference.proof option * environment + | ParamodulationSuccess of (Inference.proof * Cic.metasenv) option ;; type goal = proof * Cic.metasenv * Cic.term;; @@ -650,17 +650,20 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = else match passive_table with | None -> - if fst (Indexing.subsumption env active_table c) then - None - else + if Indexing.subsumption env active_table c = None then res + else + None | Some passive_table -> if Indexing.in_index passive_table c then None else - let r1, _ = Indexing.subsumption env active_table c in - if r1 then None else - let r2, _ = Indexing.subsumption env passive_table c in - if r2 then None else res + if Indexing.subsumption env active_table c = None then + if Indexing.subsumption env passive_table c = None then + res + else + None + else + None ;; type fs_time_info_t = { @@ -736,10 +739,10 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = let subs = match passive_table with | None -> - (fun e -> not (fst (Indexing.subsumption env active_table e))) + (fun e -> (Indexing.subsumption env active_table e = None)) | Some passive_table -> - (fun e -> not ((fst (Indexing.subsumption env active_table e)) || - (fst (Indexing.subsumption env passive_table e)))) + (fun e -> ((Indexing.subsumption env active_table e = None) && + (Indexing.subsumption env passive_table e = None))) in (* let t1 = Unix.gettimeofday () in *) (* let t2 = Unix.gettimeofday () in *) @@ -782,8 +785,11 @@ let rec simplify_goal env goal ?passive (active_list, active_table) = let changed', goal = demodulate passive_table goal in (changed || changed'), goal in - changed, if not changed then goal - else snd (simplify_goal env goal ?passive (active_list, active_table)) + changed, + if not changed then + goal + else + snd (simplify_goal env goal ?passive (active_list, active_table)) ;; @@ -976,9 +982,12 @@ let make_theorems theorems = let activate_goal (active, passive) = - match passive with - | goal_conj::tl -> true, (goal_conj::active, tl) - | [] -> false, (active, passive) + if active = [] then + match passive with + | goal_conj::tl -> true, (goal_conj::active, tl) + | [] -> false, (active, passive) + else + true, (active,passive) ;; @@ -1741,6 +1750,31 @@ and given_clause_aux dbd env goals theorems passive active = ;; *) +let check_if_goal_is_subsumed env (proof,menv,ty) table = + match ty with + | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] + when UriManager.eq uri (LibraryObjects.eq_URI ()) -> + (let goal_equation = 0,proof,(eq_ty,left,right,Eq),menv in + match Indexing.subsumption env table goal_equation with + | Some (subst, (_,p,_,m)) -> + let p = Inference.apply_subst subst (Inference.build_proof_term p) in + let newp = + let rec repl = function + | Inference.ProofGoalBlock (_, gp) -> + Inference.ProofGoalBlock (Inference.BasicProof ([],p), gp) + | Inference.NoProof -> Inference.BasicProof ([],p) + | Inference.BasicProof _ -> Inference.BasicProof ([],p) + | Inference.SubProof (t, i, p2) -> + Inference.SubProof (t, i, repl p2) + | _ -> assert false + in + repl proof + in + Some (newp,Inference.apply_subst_metasenv subst m @ menv) + | None -> None) + | _ -> None +;; + let counter = ref 0 (** given-clause algorithm with full reduction strategy *) @@ -1790,22 +1824,13 @@ let rec given_clause_fullred dbd env goals theorems passive active = | _ -> assert false in repl proof - in true, Some newp - | (_, [proof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]])::_-> - (* here we check if the goal is subsumed by an active *) - let ok, subst = - (* the first m is unused *) - Indexing.subsumption (m,context,CicUniv.empty_ugraph) - (snd active) - (0,proof,(eq_ty,left,right,Eq),m) - in - if ok then - begin - prerr_endline "The goal is subsumed by an active"; - false, None - end - else - ok, None + in true, Some (newp,m) + | (_, [proof,m,ty])::_ -> + (match check_if_goal_is_subsumed env (proof,m,ty) (snd active) with + | None -> false,None + | Some (newproof,m) -> + prerr_endline "Proof found by subsumption!"; + true, Some (newproof,m)) | _ -> false, None in if ok then @@ -1844,7 +1869,7 @@ let rec given_clause_fullred dbd env goals theorems passive active = (let x,y,_ = passive in (fst x)@(fst y)))) in prerr_endline s; prerr_endline sp; *) - ParamodulationSuccess (proof, env)) + ParamodulationSuccess (proof)) else given_clause_fullred_aux dbd env goals theorems passive active else @@ -1974,7 +1999,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active = (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign) (string_of_equality ~env current))); let _, proof, _, m = current in - ParamodulationSuccess (Some proof, env) + ParamodulationSuccess (Some (proof, m)) ) else ( debug_print (lazy "\n================================================"); @@ -2094,10 +2119,10 @@ end prova *) | true, goal -> let proof = match goal with - | Some goal -> let _, proof, _, _ = goal in Some proof + | Some goal -> let _, proof, _, env = goal in Some (proof,env) | None -> None in - ParamodulationSuccess (proof, env) + ParamodulationSuccess proof ) ;; @@ -2269,7 +2294,7 @@ let main dbd full term metasenv ugraph = match res with | ParamodulationFailure -> Printf.printf "NO proof found! :-(\n\n" - | ParamodulationSuccess (Some proof, env) -> + | ParamodulationSuccess (Some (proof, env)) -> let proof = Inference.build_proof_term proof in Printf.printf "OK, found a proof!\n"; (* REMEMBER: we have to instantiate meta_proof, we should use @@ -2300,7 +2325,7 @@ let main dbd full term metasenv ugraph = in () - | ParamodulationSuccess (None, env) -> + | ParamodulationSuccess None -> Printf.printf "Success, but no proof?!?\n\n" in if Utils.time then @@ -2362,6 +2387,7 @@ let saturate let module C = Cic in reset_refs (); Indexing.init_index (); + counter := 0; maxdepth := depth; maxwidth := width; (* CicUnification.unif_ty := false;*) @@ -2439,9 +2465,30 @@ let saturate (res, finish -. start) in match res with - | ParamodulationSuccess (Some proof, _) -> + | ParamodulationSuccess (Some (proof, proof_menv)) -> debug_print (lazy "OK, found a proof!"); let proof = Inference.build_proof_term proof in + let equality_for_replace i t1 = + match t1 with + | C.Meta (n, _) -> n = i + | _ -> false + in + let proof_menv, what, with_what = + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context + in + List.fold_left + (fun (acc1,acc2,acc3) (i,_,ty) -> + (i,context,ty)::acc1, + (Cic.Meta(i,[]))::acc2, + (Cic.Meta(i,irl)) ::acc3) + ([],[],[]) proof_menv + in + let proof = ProofEngineReduction.replace_lifting + ~equality:(=) + ~what ~with_what + ~where:proof + in (* prerr_endline (CicPp.ppterm proof); *) let names = names_of_context context in let newmetasenv = @@ -2451,6 +2498,7 @@ let saturate in List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv in + let newmetasenv = newmetasenv@proof_menv in let newstatus = try let ty, ug = @@ -2465,11 +2513,6 @@ let saturate (string_of_bool (fst (CicReduction.are_convertible context type_of_goal ty ug))))); - let equality_for_replace i t1 = - match t1 with - | C.Meta (n, _) -> n = i - | _ -> false - in let real_proof = ProofEngineReduction.replace ~equality:equality_for_replace @@ -2484,7 +2527,8 @@ let saturate (print_metasenv newmetasenv) (CicPp.pp real_proof [](* names *)) (CicPp.pp term_to_prove names))); - ((uri, newmetasenv, real_proof, term_to_prove), []) + ((uri, newmetasenv, real_proof, term_to_prove), + List.map (fun (i,_,_) -> i) proof_menv) with CicTypeChecker.TypeCheckerFailure _ -> debug_print (lazy "THE PROOF DOESN'T TYPECHECK!!!"); debug_print (lazy (CicPp.pp proof names)); diff --git a/components/tactics/paramodulation/saturation.mli b/components/tactics/paramodulation/saturation.mli index 17fbb8cfd..95f258124 100644 --- a/components/tactics/paramodulation/saturation.mli +++ b/components/tactics/paramodulation/saturation.mli @@ -33,7 +33,7 @@ val saturate : ?width:int -> ProofEngineTypes.proof * ProofEngineTypes.goal -> (UriManager.uri option * Cic.conjecture list * Cic.term * Cic.term) * - 'a list + ProofEngineTypes.goal list val weight_age_ratio : int ref val weight_age_counter: int ref -- 2.39.2