From: Enrico Tassi Date: Thu, 4 May 2006 10:55:15 +0000 (+0000) Subject: new pp function for proofs X-Git-Tag: make_still_working~7387 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2b4dcaef8f1bef33eeb27e760a1fe518a58edc8a;p=helm.git new pp function for proofs --- diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml index 7ad20206a..6c0b24327 100644 --- a/helm/software/components/tactics/paramodulation/equality.ml +++ b/helm/software/components/tactics/paramodulation/equality.ml @@ -555,7 +555,6 @@ let build_proof_step subst p1 p2 pos l r pred = -> let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in let uri_trans = LibraryObjects.trans_eq_URI ~eq in - let uri_sym = LibraryObjects.sym_eq_URI ~eq in let pred_of t = CicSubstitution.subst t lhs in let pred_of_what = pred_of what in let pred_of_other = pred_of other in @@ -563,27 +562,31 @@ let build_proof_step subst p1 p2 pos l r pred = * ==================================== * inject p2: P(what) = P(other) *) - let inject ty lhs what other p2 = + let rec inject ty lhs what other p2 = + match p2 with + | Cic.Appl ((Cic.Const(uri_trans,ens))::tl) + when LibraryObjects.is_trans_eq_URI uri_trans -> + let ty,l,m,r,plm,pmr = open_trans ens tl in + mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l) + (inject ty lhs m r pmr) (inject ty lhs l m plm) + | _ -> let liftedty = CicSubstitution.lift 1 ty in let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in let refl_eq_part = Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other] in - mk_eq_ind (Utils.eq_ind_r_URI ()) ty other + (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other (Cic.Lambda (Cic.Name "foo",ty, (Cic.Appl - [Cic.MutInd(eq,0,[]);liftedty;lhs;lifted_pred_of_other]))) - refl_eq_part what p2 + [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs]))) + refl_eq_part what p2) in mk_trans uri_trans ty pred_of_other pred_of_what rhs - (mk_sym uri_sym ty pred_of_what pred_of_other - (inject ty lhs what other p2) - ) p1 + (inject ty lhs what other p2) p1 | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed lhs -> let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in let uri_trans = LibraryObjects.trans_eq_URI ~eq in - let uri_sym = LibraryObjects.sym_eq_URI ~eq in let pred_of t = CicSubstitution.subst t lhs in let pred_of_what = pred_of what in let pred_of_other = pred_of other in @@ -591,27 +594,33 @@ let build_proof_step subst p1 p2 pos l r pred = * ==================================== * inject p2: P(what) = P(other) *) - let inject ty lhs what other p2 = - let liftedty = CicSubstitution.lift 1 ty in - let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in - let refl_eq_part = - Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other] - in - mk_eq_ind (Utils.eq_ind_URI ()) ty other - (Cic.Lambda (Cic.Name "foo",ty, - (Cic.Appl - [Cic.MutInd(eq,0,[]);liftedty;lhs;lifted_pred_of_other]))) - refl_eq_part what p2 + let rec inject ty lhs what other p2 = + match p2 with + | Cic.Appl ((Cic.Const(uri_trans,ens))::tl) + when LibraryObjects.is_trans_eq_URI uri_trans -> + let ty,l,m,r,plm,pmr = open_trans ens tl in + mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r) + (inject ty lhs m l plm) + (inject ty lhs r m pmr) + | _ -> + let liftedty = CicSubstitution.lift 1 ty in + let lifted_pred_of_other = + CicSubstitution.lift 1 (pred_of other) in + let refl_eq_part = + Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other] + in + mk_eq_ind (Utils.eq_ind_URI ()) ty other + (Cic.Lambda (Cic.Name "foo",ty, + (Cic.Appl + [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs]))) + refl_eq_part what p2 in mk_trans uri_trans ty pred_of_other pred_of_what rhs - (mk_sym uri_sym ty pred_of_other pred_of_what - (inject ty lhs what other p2) - ) p1 + (inject ty lhs what other p2) p1 | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed rhs -> let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in let uri_trans = LibraryObjects.trans_eq_URI ~eq in - let uri_sym = LibraryObjects.sym_eq_URI ~eq in let pred_of t = CicSubstitution.subst t rhs in let pred_of_what = pred_of what in let pred_of_other = pred_of other in @@ -619,26 +628,32 @@ let build_proof_step subst p1 p2 pos l r pred = * ==================================== * inject p2: P(what) = P(other) *) - let inject ty lhs what other p2 = + let rec inject ty lhs what other p2 = + match p2 with + | Cic.Appl ((Cic.Const(uri_trans,ens))::tl) + when LibraryObjects.is_trans_eq_URI uri_trans -> + let ty,l,m,r,plm,pmr = open_trans ens tl in + mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l) + (inject ty lhs m r pmr) + (inject ty lhs l m plm) + | _ -> let liftedty = CicSubstitution.lift 1 ty in let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in let refl_eq_part = Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other] in - mk_eq_ind (Utils.eq_ind_r_URI ()) ty other + (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other (Cic.Lambda (Cic.Name "foo",ty, (Cic.Appl - [Cic.MutInd(eq,0,[]);liftedty;lhs;lifted_pred_of_other]))) - refl_eq_part what p2 + [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs]))) + refl_eq_part what p2) in - mk_trans uri_trans ty lhs pred_of_what pred_of_other p1 - (mk_sym uri_sym ty pred_of_what pred_of_other - (inject ty rhs other what p2)) + mk_trans uri_trans ty lhs pred_of_what pred_of_other + p1 (inject ty rhs other what p2) | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed rhs -> let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in let uri_trans = LibraryObjects.trans_eq_URI ~eq in - let uri_sym = LibraryObjects.sym_eq_URI ~eq in let pred_of t = CicSubstitution.subst t rhs in let pred_of_what = pred_of what in let pred_of_other = pred_of other in @@ -646,7 +661,15 @@ let build_proof_step subst p1 p2 pos l r pred = * ==================================== * inject p2: P(what) = P(other) *) - let inject ty lhs what other p2 = + let rec inject ty lhs what other p2 = + match p2 with + | Cic.Appl ((Cic.Const(uri_trans,ens))::tl) + when LibraryObjects.is_trans_eq_URI uri_trans -> + let ty,l,m,r,plm,pmr = open_trans ens tl in + (mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r) + (inject ty lhs m l plm) + (inject ty lhs r m pmr)) + | _ -> let liftedty = CicSubstitution.lift 1 ty in let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in let refl_eq_part = @@ -655,12 +678,11 @@ let build_proof_step subst p1 p2 pos l r pred = mk_eq_ind (Utils.eq_ind_URI ()) ty other (Cic.Lambda (Cic.Name "foo",ty, (Cic.Appl - [Cic.MutInd(eq,0,[]);liftedty;lhs;lifted_pred_of_other]))) + [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs]))) refl_eq_part what p2 in - mk_trans uri_trans ty lhs pred_of_what pred_of_other p1 - (mk_sym uri_sym ty pred_of_other pred_of_what - (inject ty rhs other what p2)) + 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 -> @@ -678,6 +700,37 @@ let build_proof_term_new proof = build_proof_step subst p1 p2 pos l r pred in aux proof +;; + +let wfo goalproof = + let rec aux acc id = + let p,_,_ = proof_of_id id in + match p with + | Exact _ -> id :: acc + | Step (_,(_,id1, (_,id2), _)) -> + let acc = if not (List.mem id1 acc) then aux acc id1 else acc in + 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 string_of_id names id = + try + let (_,(p,_),(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in + match p with + | Exact t -> + Printf.sprintf "%d = %s: %s = %s" id + (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names) + | Step (_,(step,id1, (_,id2), _) ) -> + Printf.sprintf "%5d: %s %4d %4d %s = %s" id + (if step = SuperpositionRight then "SupR" else "Demo") + id1 id2 (CicPp.pp l names) (CicPp.pp r names) + with + Not_found -> assert false + +let pp_proof names goalproof = + String.concat "\n" (List.map (string_of_id names) (wfo goalproof)) let build_goal_proof l initial = let proof = diff --git a/helm/software/components/tactics/paramodulation/equality.mli b/helm/software/components/tactics/paramodulation/equality.mli index 4d48f22aa..ea0cefd55 100644 --- a/helm/software/components/tactics/paramodulation/equality.mli +++ b/helm/software/components/tactics/paramodulation/equality.mli @@ -45,7 +45,8 @@ and old_proof = | SubProof of Cic.term * int * old_proof and goal_proof = (Utils.pos * int * substitution * Cic.term) list - + +val pp_proof: (Cic.name option) list -> goal_proof -> string val empty_subst : substitution val apply_subst : substitution -> Cic.term -> Cic.term diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index 4423661b0..f1cec900f 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -1540,14 +1540,16 @@ let saturate (* 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 "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 "NEWPROOFCIC"; - prerr_endline (CicPp.pp cic_proof_new names); + (* 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); *) (* generation of proof metasenv *) let newmetasenv = @@ -1605,8 +1607,8 @@ let saturate cic_proof_new, newmetasenv_new, newmetasenv_new,new_ty, newug (* THE OLD PROOF: cic_proof,newmetasenv,proof_menv,oldty,oldug *) in - prerr_endline "FINAL PROOF"; - prerr_endline (CicPp.pp cic_proof names); +(* prerr_endline "FINAL PROOF";*) +(* prerr_endline (CicPp.pp cic_proof names);*) prerr_endline "ENDOFPROOFS"; (* debug_print