From: Enrico Tassi Date: Wed, 26 Apr 2006 09:59:07 +0000 (+0000) Subject: cleanup of saturate X-Git-Tag: 0.4.95@7852~1496 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d7ed0cc36dd7e4169bc8f37b5b58884a17de4a89;p=helm.git cleanup of saturate --- diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index 59b06ef29..5cc6e811e 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -1522,21 +1522,29 @@ let saturate in match res with | ParamodulationSuccess - (Some ((goalproof,newproof,subsumption_subst, newproof_menv),(proof, proof_menv))) -> + (Some + ((goalproof,newproof,subsumption_subst, newproof_menv), (* NEW *) + (proof, proof_menv))) (* OLD *) + -> prerr_endline "OK, found a proof!"; - prerr_endline (Equality.string_of_proof_old proof); + (* generation of the old proof *) let cic_proof = Equality.build_proof_term_old proof in - + + (* generation of the new proof *) let cic_proof_new,cic_proof_new_menv = - Equality.build_goal_proof goalproof (Equality.build_proof_term_new newproof) + Equality.build_goal_proof + goalproof (Equality.build_proof_term_new newproof) in let newproof_menv = Equality.apply_subst_metasenv subsumption_subst (newproof_menv @ cic_proof_new_menv) in - let cic_proof_new = Equality.apply_subst subsumption_subst cic_proof_new in + let cic_proof_new = + Equality.apply_subst subsumption_subst cic_proof_new + in + (* replacing fake mets with real ones *) let equality_for_replace i t1 = match t1 with | C.Meta (n, _) -> n = i @@ -1573,6 +1581,8 @@ let saturate ~what ~with_what ~where:cic_proof_new in + + (* pp new/old proof *) let names = names_of_context context in prerr_endline "OLDPROOF"; prerr_endline (Equality.string_of_proof_old proof); @@ -1582,6 +1592,8 @@ let saturate prerr_endline (Equality.string_of_proof_new ~names newproof goalproof); prerr_endline "NEWPROOFCIC"; prerr_endline (CicPp.pp cic_proof_new names); + + (* generation of proof metasenv *) let newmetasenv = let i1 = match new_meta_goal with @@ -1591,119 +1603,108 @@ let saturate in let newmetasenv = newmetasenv@proof_menv in let newmetasenv_new = newmetasenv@newproof_menv in + + (* check/refine/... build the new proof *) let newstatus = - try - let cic_proof,newmetasenv,proof_menv,ty, ug = - prerr_endline "type checking ... (old) "; -(* let old_ty, oldug = *) -(* CicTypeChecker.type_of_aux' newmetasenv context cic_proof ugraph *) -(* in*) - let cic_proof_new,new_ty,newmetasenv_new,newug = - try - (* - prerr_endline "refining ... (new) "; - CicRefine.type_of_aux' - newmetasenv_new context cic_proof_new ugraph*) - let ty,ug = - prerr_endline "typechecking ... (new) "; - CicTypeChecker.type_of_aux' - newmetasenv_new context cic_proof_new ugraph - in - cic_proof_new, ty, newmetasenv_new, ug - with - | CicTypeChecker.TypeCheckerFailure s -> - prerr_endline "FAILURE IN TYPECHECKING"; - prerr_endline (Lazy.force s); - assert false - | CicRefine.RefineFailure s - | CicRefine.Uncertain s - | CicRefine.AssertFailure s -> - prerr_endline "FAILURE IN REFINE"; - prerr_endline (Lazy.force s); - interactive_comparison context cic_proof_new cic_proof; - assert false - in -(* - prerr_endline "check unif ... (old vs new) "; - (try - ignore(CicUnification.fo_unif - newmetasenv_new context cic_proof_new cic_proof CicUniv.empty_ugraph) - with CicUnification.UnificationFailure _ -> - prerr_endline "WARNING, new and old proofs are not unifiable"); - prerr_endline "unif ... (new) "; - let subst, newmetasenv_new, newug = - CicUnification.fo_unif - newmetasenv_new context new_ty type_of_goal newug - in - if subst <> [] then - prerr_endline "UNIF SERVE ################################"; -*) - let subst = [] in - if List.length newmetasenv_new <> 0 then - prerr_endline - ("Some METAS are still open: " ^ CicMetaSubst.ppmetasenv - [] newmetasenv_new); - (CicMetaSubst.apply_subst subst cic_proof_new), - newmetasenv_new, - (CicMetaSubst.apply_subst_metasenv subst newmetasenv_new), - (CicMetaSubst.apply_subst subst new_ty), - newug -(* cic_proof,newmetasenv,proof_menv,oldty,oldug*) + let cic_proof,newmetasenv,proof_menv,ty, ug = + prerr_endline "type checking ... (old) "; + let _old_ty, _oldug = + try + CicTypeChecker.type_of_aux' newmetasenv context cic_proof ugraph + with + CicTypeChecker.TypeCheckerFailure s -> + prerr_endline "THE *OLD* PROOF DOESN'T TYPECHECK!!!"; + prerr_endline (Lazy.force s); + Cic.Implicit None, CicUniv.empty_ugraph in - prerr_endline "FINAL PROOF"; - prerr_endline (CicPp.pp cic_proof names); - prerr_endline "ENDOFPROOFS"; - - debug_print - (lazy - (Printf.sprintf - "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n" - (CicPp.pp type_of_goal names) (CicPp.pp ty names) - (string_of_bool - (fst (CicReduction.are_convertible - context type_of_goal ty ug))))); - let real_proof = - ProofEngineReduction.replace - ~equality:equality_for_replace - ~what:[goal'] ~with_what:[cic_proof] - ~where:meta_proof + let cic_proof_new,new_ty,newmetasenv_new,newug = + try + (* + prerr_endline "refining ... (new) "; + CicRefine.type_of_aux' + newmetasenv_new context cic_proof_new ugraph + *) + let ty,ug = + prerr_endline "typechecking ... (new) "; + CicTypeChecker.type_of_aux' + newmetasenv_new context cic_proof_new ugraph + in + cic_proof_new, ty, newmetasenv_new, ug + with + | CicTypeChecker.TypeCheckerFailure s -> + prerr_endline "THE PROOF DOESN'T TYPECHECK!!!"; + prerr_endline (Lazy.force s); + assert false + | CicRefine.RefineFailure s + | CicRefine.Uncertain s + | CicRefine.AssertFailure s -> + prerr_endline "FAILURE IN REFINE"; + prerr_endline (Lazy.force s); + interactive_comparison context cic_proof_new cic_proof; + assert false in - debug_print - (lazy - (Printf.sprintf "status:\n%s\n%s\n%s\n%s\n" - (match uri with Some uri -> UriManager.string_of_uri uri - | None -> "") - (print_metasenv newmetasenv) - (CicPp.pp real_proof [](* names *)) - (CicPp.pp term_to_prove names))); - ((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 cic_proof names)); - raise (ProofEngineTypes.Fail - (lazy "Found a proof, but it doesn't typecheck")) + if List.length newmetasenv_new <> 0 then + prerr_endline + ("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 + prerr_endline "FINAL PROOF"; + prerr_endline (CicPp.pp cic_proof names); + prerr_endline "ENDOFPROOFS"; + (* + debug_print + (lazy + (Printf.sprintf + "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n" + (CicPp.pp type_of_goal names) (CicPp.pp ty names) + (string_of_bool + (fst (CicReduction.are_convertible + context type_of_goal ty ug))))); + *) + let real_proof = + ProofEngineReduction.replace + ~equality:equality_for_replace + ~what:[goal'] ~with_what:[cic_proof] + ~where:meta_proof + in + (* + debug_print + (lazy + (Printf.sprintf "status:\n%s\n%s\n%s\n%s\n" + (match uri with Some uri -> UriManager.string_of_uri uri + | None -> "") + (print_metasenv newmetasenv) + (CicPp.pp real_proof [](* names *)) + (CicPp.pp term_to_prove names))); + *) + let open_goals = List.map (fun (i,_,_) -> i) proof_menv in + (uri, newmetasenv, real_proof, term_to_prove), open_goals in - let tall = fs_time_info.build_all in - let tdemodulate = fs_time_info.demodulate in - let tsubsumption = fs_time_info.subsumption in if Utils.time then begin + let tall = fs_time_info.build_all in + let tdemodulate = fs_time_info.demodulate in + let tsubsumption = fs_time_info.subsumption in prerr_endline ( (Printf.sprintf "\nTIME NEEDED: %.9f" time) ^ (Printf.sprintf "\ntall: %.9f" tall) ^ (Printf.sprintf "\ntdemod: %.9f" tdemodulate) ^ (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption) ^ (Printf.sprintf "\ninfer_time: %.9f" !infer_time) ^ - (Printf.sprintf "\nforward_simpl_times: %.9f" !forward_simpl_time) ^ + (Printf.sprintf "\nforward_simpl_times: %.9f" + !forward_simpl_time) ^ (Printf.sprintf "\nforward_simpl_new_times: %.9f" - !forward_simpl_new_time) ^ - (Printf.sprintf "\nbackward_simpl_times: %.9f" !backward_simpl_time) ^ + !forward_simpl_new_time) ^ + (Printf.sprintf "\nbackward_simpl_times: %.9f" + !backward_simpl_time) ^ (Printf.sprintf "\npassive_maintainance_time: %.9f" !passive_maintainance_time)) end; - newstatus - | _ -> + newstatus + | ParamodulationSuccess None -> assert false + | ParamodulationFailure -> raise (ProofEngineTypes.Fail (lazy "NO proof found")) ;;