From 0f8a03b999acc2a16cbbffd6b19ab0e2967587cc Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 26 May 2006 11:08:29 +0000 Subject: [PATCH] 1) variables occurring only in proofs anre not relocated 2) during unification the resulting metasenv is cleaned of duplicates (duplicates can only be variables in proofs, not in left/right) --- components/tactics/paramodulation/equality.ml | 70 ++++++++++++------- components/tactics/paramodulation/indexing.ml | 2 +- .../tactics/paramodulation/inference.ml | 5 +- .../tactics/paramodulation/saturation.ml | 11 ++- 4 files changed, 57 insertions(+), 31 deletions(-) diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml index 5f847bcb5..ec311615e 100644 --- a/components/tactics/paramodulation/equality.ml +++ b/components/tactics/paramodulation/equality.ml @@ -78,18 +78,20 @@ let open_equality (_,weight,proof,(ty,l,r,o),m,id) = let string_of_equality ?env eq = match env with | None -> - let w, _, (ty, left, right, o), _ , id = open_equality eq in - Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s" + let w, _, (ty, left, right, o), m , id = open_equality eq in + Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s [%s]" id w (CicPp.ppterm ty) (CicPp.ppterm left) (Utils.string_of_comparison o) (CicPp.ppterm right) + (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) | Some (_, context, _) -> let names = Utils.names_of_context context in - let w, _, (ty, left, right, o), _ , id = open_equality eq in - Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s" + let w, _, (ty, left, right, o), m , id = open_equality eq in + Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s [%s]" id w (CicPp.pp ty names) (CicPp.pp left names) (Utils.string_of_comparison o) (CicPp.pp right names) + (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) ;; let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) = @@ -479,15 +481,17 @@ let wfo goalproof proof = let string_of_id names id = try - let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in + let (_,p,(_,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in match p with | Exact t -> - Printf.sprintf "%d = %s: %s = %s" id + Printf.sprintf "%d = %s: %s = %s [%s]" id (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names) + (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) | Step (_,(step,id1, (_,id2), _) ) -> - Printf.sprintf "%6d: %s %6d %6d %s = %s" id + Printf.sprintf "%6d: %s %6d %6d %s = %s [%s]" id (if step = SuperpositionRight then "SupR" else "Demo") id1 id2 (CicPp.pp l names) (CicPp.pp r names) + (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) with Not_found -> assert false @@ -545,9 +549,17 @@ let build_proof_term h lift proof = let rec aux = function | Exact term -> CicSubstitution.lift lift term | Step (subst,(_, id1, (pos,id2), pred)) -> + if Subst.is_in_subst 302 subst then + prerr_endline ("TROVATA in " ^ string_of_int id1 ^ " " ^ string_of_int id2); + let p1,_,_ = proof_of_id aux id1 in let p2,l,r = proof_of_id aux id2 in - build_proof_step lift subst p1 p2 pos l r pred + let p = build_proof_step 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); + assert cond;*) + p in aux proof ;; @@ -575,7 +587,10 @@ let build_goal_proof l initial ty se = let rec aux se current_proof = function | [] -> current_proof,se | (pos,id,subst,pred)::tl -> - let p,l,r = proof_of_id id in + if Subst.is_in_subst 302 subst then + prerr_endline ("TROVATA in " ^ string_of_int id ); + + let p,l,r = proof_of_id id in let p = build_proof_term h letsno p in let pos = if pos = Utils.Left then Utils.Right else Utils.Left in let proof = @@ -597,7 +612,7 @@ let build_goal_proof l initial ty se = cic, p)) lets (letsno-1,initial) in - canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)), se + (*canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty))*)proof, se ;; let refl_proof ty term = @@ -612,26 +627,29 @@ let metas_of_proof p = Utils.metas_of_term p ;; -let relocate newmeta menv = - let subst, metasenv, newmeta = +let relocate newmeta menv to_be_relocated = + let subst, newmetasenv, newmeta = List.fold_right - (fun (i, context, ty) (subst, menv, maxmeta) -> - let irl = [] (* - CicMkImplicit.identity_relocation_list_for_metavariable context *) - in - let newsubst = Subst.buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in - let newmeta = maxmeta, context, ty in - newsubst, newmeta::menv, maxmeta+1) - menv (Subst.empty_subst, [], newmeta+1) + (fun i (subst, metasenv, maxmeta) -> + let _,context,ty = CicUtil.lookup_meta i menv in + let irl = [] in + let newmeta = Cic.Meta(maxmeta,irl) in + let newsubst = Subst.buildsubst i context newmeta ty subst in + newsubst, (maxmeta,context,ty)::metasenv, maxmeta+1) + to_be_relocated (Subst.empty_subst, [], newmeta+1) in - let metasenv = Subst.apply_subst_metasenv subst metasenv in - let subst = Subst.flatten_subst subst in - subst, metasenv, newmeta + let menv = Subst.apply_subst_metasenv subst menv @ newmetasenv in + subst, menv, newmeta let fix_metas newmeta eq = let w, p, (ty, left, right, o), menv,_ = open_equality eq in - let subst, metasenv, newmeta = relocate newmeta menv in + let to_be_relocated = + HExtlib.list_uniq + (List.sort Pervasives.compare + (Utils.metas_of_term left @ Utils.metas_of_term right)) + in + let subst, metasenv, newmeta = relocate newmeta menv to_be_relocated in let ty = Subst.apply_subst subst ty in let left = Subst.apply_subst subst left in let right = Subst.apply_subst subst right in @@ -641,8 +659,8 @@ let fix_metas newmeta eq = Step (Subst.concat s subst,(r,id1,(pos,id2), pred)) in let p = fix_proof p in - let eq = mk_equality (w, p, (ty, left, right, o), metasenv) in - newmeta+1, eq + let eq' = mk_equality (w, p, (ty, left, right, o), metasenv) in + newmeta+1, eq' exception NotMetaConvertible;; diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml index a2e6eda07..dd2d0a422 100644 --- a/components/tactics/paramodulation/indexing.ml +++ b/components/tactics/paramodulation/indexing.ml @@ -1057,7 +1057,7 @@ let superposition_left (metasenv, context, ugraph) table goal = (** demodulation, when the target is a goal *) let rec demodulation_goal env table goal = let goalproof,menv,_,_,left,right = open_goal goal in - let metasenv, context, ugraph = env in + let _, context, ugraph = env in (* let term = Utils.guarded_simpl (~debug:true) context term in*) let do_right () = let resright = demodulation_aux menv context ugraph table 0 right in diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml index ab27f8a31..36e9f99a6 100644 --- a/components/tactics/paramodulation/inference.ml +++ b/components/tactics/paramodulation/inference.ml @@ -139,7 +139,10 @@ let profiler3 = HExtlib.profile "P/Inference.unif_simple[resolve_meta]" let profiler4 = HExtlib.profile "P/Inference.unif_simple[filter]" let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph = - let metasenv = metasenv1 @ metasenv2 in + let metasenv = + HExtlib.list_uniq (List.sort Pervasives.compare (metasenv1 @ metasenv2)) + (*metasenv1 @ metasenv2*) + in let subst, menv, ug = if not (is_simple_term t1) || not (is_simple_term t2) then ( debug_print diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index 445eccdbc..e12b1f8a7 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -1692,7 +1692,7 @@ let saturate let eq_indexes, equalities, maxm = find_equalities context proof in let ugraph = CicUniv.empty_ugraph in let env = (metasenv, context, ugraph) in - let goal = [], metasenv, type_of_goal in + let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, type_of_goal in let res, time = let t1 = Unix.gettimeofday () in let lib_eq_uris, library_equalities, maxm = @@ -1760,6 +1760,7 @@ let saturate (goalproof,newproof,subsumption_subst, proof_menv) -> prerr_endline "OK, found a proof!"; prerr_endline (Equality.pp_proof names goalproof newproof); + prerr_endline (CicMetaSubst.ppmetasenv [] proof_menv); prerr_endline "ENDOFPROOFS"; (* generation of the CIC proof *) let side_effects = @@ -1771,7 +1772,7 @@ let saturate let initial = newproof in Equality.build_goal_proof goalproof initial type_of_goal side_effects in -prerr_endline (CicPp.pp goal_proof names); +(*prerr_endline (CicPp.pp goal_proof names);*) let goal_proof = Subst.apply_subst subsumption_subst goal_proof in let side_effects_t = List.map (Subst.apply_subst subsumption_subst) side_effects_t @@ -1790,6 +1791,8 @@ prerr_endline (CicPp.pp goal_proof names); (Cic.Meta(i,irl)) ::acc3,Some (Cic.Meta(i,irl))) ([],[],[],None) proof_menv in +prerr_endline ("RIMPIAZZATO CON " ^ match free_meta with None -> "?" | Some m -> CicPp.ppterm m); + let replace where = ProofEngineReduction.replace_lifting ~equality:(=) ~what ~with_what ~where @@ -1803,6 +1806,7 @@ prerr_endline (CicPp.pp goal_proof names); (ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv:goal_proof_menv) in +prerr_endline ("freemetas: " ^ String.concat "," (List.map string_of_int free_metas) ); (* check/refine/... build the new proof *) let replaced_goal = ProofEngineReduction.replace @@ -1827,6 +1831,7 @@ prerr_endline (CicPp.pp goal_proof names); let final_subst = (goalno,(context,goal_proof,type_of_goal))::subst_side_effects in +prerr_endline ("MENVreal_menv: " ^ CicMetaSubst.ppmetasenv [] real_menv); let _ = try CicTypeChecker.type_of_aux' real_menv context goal_proof @@ -1837,7 +1842,7 @@ prerr_endline (CicPp.pp goal_proof names); | CicTypeChecker.AssertFailure _ | Invalid_argument "list_fold_left2" as exn -> prerr_endline "THE PROOF DOES NOT TYPECHECK!"; - prerr_endline (CicPp.pp goal_proof names); +(* prerr_endline (CicPp.pp goal_proof names); *) raise exn in let proof, real_metasenv = -- 2.39.2