From d8d939cc3f78a805a3c16f715912ecd96c302592 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 29 Jun 2006 10:01:16 +0000 Subject: [PATCH] goals after a superposition step are relocated --- components/tactics/paramodulation/equality.ml | 28 ++++++- .../tactics/paramodulation/equality.mli | 6 ++ components/tactics/paramodulation/indexing.ml | 73 ++++++++++--------- .../tactics/paramodulation/indexing.mli | 12 ++- .../tactics/paramodulation/saturation.ml | 26 +++++-- 5 files changed, 93 insertions(+), 52 deletions(-) diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml index 5a8e88638..3ac57e6fe 100644 --- a/components/tactics/paramodulation/equality.ml +++ b/components/tactics/paramodulation/equality.ml @@ -46,6 +46,8 @@ and proof = and goal_proof = (rule * Utils.pos * int * Subst.substitution * Cic.term) list ;; +type goal = goal_proof * Cic.metasenv * Cic.term + (* globals *) let maxid = ref 0;; let id_to_eq = Hashtbl.create 1024;; @@ -432,7 +434,7 @@ let add_subst subst = function | Exact t -> Exact (Subst.apply_subst subst t) | Step (s,(rule, id1, (pos,id2), pred)) -> - Step (Subst.concat subst s,(rule, id1, (pos,id2), pred)) + Step (Subst.concat subst s,(rule, id1, (pos,id2), pred)) ;; let build_proof_step eq lift subst p1 p2 pos l r pred = @@ -653,7 +655,8 @@ let build_proof_term eq h lift proof = try List.assoc id h,l,r with Not_found -> aux p, l, r in let rec aux = function - | Exact term -> CicSubstitution.lift lift term + | Exact term -> + CicSubstitution.lift lift term | Step (subst,(rule, id1, (pos,id2), pred)) -> let p1,_,_ = proof_of_id aux id1 in let p2,l,r = proof_of_id aux id2 in @@ -668,7 +671,7 @@ let build_proof_term eq h lift proof = | Cic.Lambda (_,a,b) -> Cic.Lambda (varname,a,b) | _ -> assert false in - let p = build_proof_step eq lift subst p1 p2 pos l r pred in + let p = build_proof_step eq lift subst p1 p2 pos l r pred in (* let cond = (not (List.mem 302 (Utils.metas_of_term p)) || id1 = 8 || id1 = 132) in if not cond then prerr_endline ("ERROR " ^ string_of_int id1 ^ " " ^ string_of_int id2); @@ -733,7 +736,9 @@ let build_goal_proof eq l initial ty se = cic, p)) lets (letsno-1,initial) in - canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)), +(* canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)), + * *) +proof, se ;; @@ -777,6 +782,21 @@ let relocate newmeta menv to_be_relocated = let menv = Subst.apply_subst_metasenv subst menv @ newmetasenv in subst, menv, newmeta +let fix_metas_goal newmeta goal = + let (proof, menv, ty) = goal in + let to_be_relocated = + HExtlib.list_uniq (List.sort Pervasives.compare (Utils.metas_of_term ty)) + in + let subst, menv, newmeta = relocate newmeta menv to_be_relocated in + let ty = Subst.apply_subst subst ty in + let proof = + match proof with + | [] -> assert false (* is a nonsense to relocate the initial goal *) + | (r,pos,id,s,p) :: tl -> (r,pos,id,Subst.concat subst s,p) :: tl + in + newmeta+1,(proof, menv, ty) +;; + let fix_metas newmeta eq = let w, p, (ty, left, right, o), menv,_ = open_equality eq in let to_be_relocated = diff --git a/components/tactics/paramodulation/equality.mli b/components/tactics/paramodulation/equality.mli index 1182afee6..d4a94cdb5 100644 --- a/components/tactics/paramodulation/equality.mli +++ b/components/tactics/paramodulation/equality.mli @@ -33,6 +33,8 @@ and proof = and goal_proof = (rule * Utils.pos * int * Subst.substitution * Cic.term) list +type goal = goal_proof * Cic.metasenv * Cic.term + val pp_proof: (Cic.name option) list -> goal_proof -> proof -> Subst.substitution -> int -> Cic.term -> string @@ -66,11 +68,15 @@ val string_of_proof : val build_goal_proof: UriManager.uri -> goal_proof -> proof -> Cic.term-> int list -> Cic.term * Cic.term list +val build_proof_term : UriManager.uri -> (int * Cic.term) list -> int -> proof -> Cic.term val refl_proof: UriManager.uri -> Cic.term -> Cic.term -> Cic.term (** ensures that metavariables in equality are unique *) +val fix_metas_goal: int -> goal -> int * goal val fix_metas: int -> equality -> int * equality val metas_of_proof: proof -> int list +(* this should be used _only_ to apply (efficiently) this subst on the + * initial proof passed to build_goal_proof *) val add_subst : Subst.substitution -> proof -> proof exception TermIsNotAnEquality;; diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml index c74abe27d..7b545dd47 100644 --- a/components/tactics/paramodulation/indexing.ml +++ b/components/tactics/paramodulation/indexing.ml @@ -27,8 +27,6 @@ let _profiler = <:profiler<_profiler>>;; (* $Id$ *) -type goal = Equality.goal_proof * Cic.metasenv * Cic.term - module Index = Equality_indexing.DT (* discrimination tree based indexing *) (* module Index = Equality_indexing.DT (* path tree based indexing *) @@ -1048,41 +1046,48 @@ let build_newgoal context goal posu rule expansion = returns a list of new clauses inferred with a left superposition step the negative equation "target" and one of the positive equations in "table" *) -let superposition_left (metasenv, context, ugraph) table goal = +let superposition_left (metasenv, context, ugraph) table goal maxmeta = let names = Utils.names_of_context context in let proof,menv,eq,ty,l,r = open_goal goal in let c = !Utils.compare_terms l r in - if c = Utils.Incomparable then - begin - let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in - let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in - (* prerr_endline "incomparable"; - prerr_endline (string_of_int (List.length expansionsl)); - prerr_endline (string_of_int (List.length expansionsr)); - *) - List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl - @ - List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr - end - else - match c with - | Utils.Gt -> (* prerr_endline "GT"; *) - let big,small,possmall = l,r,Utils.Right in - let expansions, _ = betaexpand_term menv context ugraph table 0 big in - List.map - (build_newgoal context goal possmall Equality.SuperpositionLeft) - expansions - | Utils.Lt -> (* prerr_endline "LT"; *) - let big,small,possmall = r,l,Utils.Left in - let expansions, _ = betaexpand_term menv context ugraph table 0 big in - List.map - (build_newgoal context goal possmall Equality.SuperpositionLeft) - expansions - | Utils.Eq -> [] - | _ -> - prerr_endline - ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names); - assert false + let newgoals = + if c = Utils.Incomparable then + begin + let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in + let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in + (* prerr_endline "incomparable"; + prerr_endline (string_of_int (List.length expansionsl)); + prerr_endline (string_of_int (List.length expansionsr)); + *) + List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl + @ + List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr + end + else + match c with + | Utils.Gt -> (* prerr_endline "GT"; *) + let big,small,possmall = l,r,Utils.Right in + let expansions, _ = betaexpand_term menv context ugraph table 0 big in + List.map + (build_newgoal context goal possmall Equality.SuperpositionLeft) + expansions + | Utils.Lt -> (* prerr_endline "LT"; *) + let big,small,possmall = r,l,Utils.Left in + let expansions, _ = betaexpand_term menv context ugraph table 0 big in + List.map + (build_newgoal context goal possmall Equality.SuperpositionLeft) + expansions + | Utils.Eq -> [] + | _ -> + prerr_endline + ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names); + assert false + in + (* rinfresco le meta *) + List.fold_right + (fun g (max,acc) -> + let max,g = Equality.fix_metas_goal max g in max,g::acc) + newgoals (maxmeta,[]) ;; (** demodulation, when the target is a goal *) diff --git a/components/tactics/paramodulation/indexing.mli b/components/tactics/paramodulation/indexing.mli index 7caaa78f4..75e16ec1b 100644 --- a/components/tactics/paramodulation/indexing.mli +++ b/components/tactics/paramodulation/indexing.mli @@ -25,8 +25,6 @@ (* $Id$ *) -type goal = Equality.goal_proof * Cic.metasenv * Cic.term - module Index : sig module PosEqSet : Set.S @@ -51,11 +49,11 @@ val subsumption : Index.t -> Equality.equality -> (Subst.substitution * Equality.equality * bool) option + val superposition_left : Cic.conjecture list * Cic.context * CicUniv.universe_graph -> - Index.t -> - goal -> - goal list + Index.t -> Equality.goal -> int -> + int * Equality.goal list val superposition_right : ?subterms_only:bool -> @@ -76,8 +74,8 @@ val demodulation_equality : val demodulation_goal : Cic.metasenv * Cic.context * CicUniv.universe_graph -> Index.t -> - goal -> - bool * goal + Equality.goal -> + bool * Equality.goal val demodulation_theorem : 'a -> Cic.metasenv * Cic.context * CicUniv.universe_graph -> diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index e7ef6fa7c..26db9567c 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -913,8 +913,8 @@ let pp_goal_set msg goals names = ;; let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) = -(* let names = names_of_context ctx in +(* Printf.eprintf "check_goal_subsumed: %s\n" (CicPp.pp ty names); *) match ty with @@ -928,8 +928,10 @@ let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) = match Indexing.unification env table goal_equation with | Some (subst, equality, swapped ) -> prerr_endline - ("GOAL SUBSUMED BY: " ^ Equality.string_of_equality equality); - prerr_endline ("SUBST:" ^ Subst.ppsubst subst); + ("GOAL SUBSUMED IS: " ^ Equality.string_of_equality goal_equation ~env); + prerr_endline + ("GOAL IS SUBSUMED BY: " ^ Equality.string_of_equality equality ~env); + prerr_endline ("SUBST:" ^ Subst.ppsubst ~names subst); let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in let p = @@ -1028,8 +1030,11 @@ let infer_goal_set env active goals = let new_passive_goals = if Utils.metas_of_term t1 = [] then passive_goals else - let new' = - Indexing.superposition_left env (snd active) selected in + let newmaxmeta,new' = + Indexing.superposition_left env (snd active) selected + !maxmeta + in + maxmeta := newmaxmeta; passive_goals @ new' in selected::active_goals, new_passive_goals @@ -1073,7 +1078,8 @@ let infer_goal_set_with_current env current goals = active_goals, List.fold_left (fun acc g -> - let new' = Indexing.superposition_left env table g in + let newmaxmeta, new' = Indexing.superposition_left env table g !maxmeta in + maxmeta := newmaxmeta; acc @ new') passive_goals active_goals ;; @@ -1580,7 +1586,6 @@ let saturate prerr_endline (Equality.pp_proof names goalproof newproof subsumption_subst subsumption_id type_of_goal); - prerr_endline (CicMetaSubst.ppmetasenv [] proof_menv); prerr_endline "ENDOFPROOFS"; (* generation of the CIC proof *) let side_effects = @@ -1593,6 +1598,7 @@ let saturate Equality.build_goal_proof eq_uri goalproof initial type_of_goal side_effects in + prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); let goal_proof = Subst.apply_subst subsumption_subst goal_proof in let metas_still_open_in_proof = Utils.metas_of_term goal_proof in (*prerr_endline (CicPp.pp goal_proof names);*) @@ -1975,6 +1981,12 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status = let t = Equality.term_of_equality eq_uri e in prerr_endline (CicPp.pp t names)) eql; + prerr_endline ("\n result proofs: "); + List.iter (fun e -> + prerr_endline (let _,p,_,_,_ = Equality.open_equality e in + let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in + Subst.ppsubst s ^ "\n" ^ + CicPp.pp (Equality.build_proof_term eq_uri [] 0 p) names)) eql; if demod_table <> "" then begin let demod = -- 2.39.2