match Pervasives.compare w1 w2 with
| 0 ->
let res = (List.length m1) - (List.length m2) in
- if res <> 0 then res else Pervasives.compare eq1 eq2
+ if res <> 0 then res else
+ Equality.compare eq1 eq2
| res -> res
end
repl proof
in
let newcicp,np,subst,cicmenv =
- cicproof,np, subst, (m @ menv)
+ cicproof,np, subst, Equality.apply_subst_metasenv subst (m @ menv)
in
Some
((newcicp,np,subst,cicmenv),
Equality.reset ();
;;
-let interactive_comparison context t1 t2 =
- let rc = ref [] in
- let module P = Printf in
- let rec aux n context t1 t2 =
-(* let names = names_of_context context in*)
- let pp t1 t2 = () (*
- P.eprintf "%s%s === %s\n" (String.make n ' ')
- (CicPp.pp t1 names) (CicPp.pp t2 names) *)
- in
- match t1,t2 with
- | _, Cic.Appl [Cic.Const(uri,_);t2] when
- UriManager.eq uri (UriManager.uri_of_string
- "cic:/Coq/Init/Logic/sym_eq.con")-> aux n context t1 t2
- | Cic.Implicit _, _ -> pp t1 t2
- | Cic.Meta (n,_), _ ->
- rc := (n,t2,context) :: !rc;
- pp (Cic.Meta(n,[])) t2
- | Cic.Rel n1, Cic.Rel n2 when n1 = n2 -> pp t1 t2
- | Cic.Appl l1,Cic.Appl l2 ->
- if List.length l1 <> List.length l2 then
- begin
- prerr_endline "ERROR: application with diff num of args";
- pp t1 t2
- end
- else
- List.iter2 (aux (n+1) context) l1 l2
- | Cic.Lambda (name,s,t1),Cic.Lambda(_,_,t2) ->
- let context = (Some (name,(Cic.Decl s)))::context in
- aux (n+1) context t1 t2
- | Cic.Const (u1,_), Cic.Const (u2,_) when UriManager.eq u1 u2 ->
- pp t1 t2
- | _,_ -> pp t1 t2
- in
- aux 0 context t1 t2;
- List.iter (fun (n,t,ctx) ->
- let names = names_of_context ctx in
- Printf.eprintf "%d := %s\n" n (CicPp.pp t names))
- (HExtlib.list_uniq (List.sort (fun (x,_,_) (y,_,_) -> x-y) !rc))
-;;
-
-
let saturate
dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status =
let module C = Cic in
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
-
- let cic_proof_new,cic_proof_new_menv =
- Equality.build_goal_proof goalproof (Equality.build_proof_term_new newproof)
+
+ (* generation of the new proof *)
+ let cic_proof_new =
+ 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)
+ 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);
+ 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 / blobdiff