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
~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);
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
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"))
;;
projects / helm.git / commitdiff