eq_uri goalproof initial type_of_goal side_effects
context proof_menv
in
+(* Equality.draw_proof bag names goalproof newproof subsumption_id; *)
let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
let real_menv = fix_metasenv (proof_menv@metasenv) in
let real_menv,goal_proof =
let real_menv,fixed_proof = fix_proof proof_menv context false goal_proof in
(* prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); *)
*)
+ let pp_error goal_proof names error exn =
+ prerr_endline "THE PROOF DOES NOT TYPECHECK! <begin>";
+ prerr_endline (CicPp.pp goal_proof names);
+ prerr_endline "THE PROOF DOES NOT TYPECHECK!";
+ prerr_endline error;
+ prerr_endline "THE PROOF DOES NOT TYPECHECK! <end>";
+ raise exn
+ in
let goal_proof,goal_ty,real_menv,_ =
(* prerr_endline ("parte la refine per: " ^ (CicPp.pp goal_proof names)); *)
try
+ prerr_endline (CicPp.ppterm goal_proof);
CicRefine.type_of_aux' real_menv context goal_proof CicUniv.empty_ugraph
with
- | CicUtil.Meta_not_found _
- | CicRefine.RefineFailure _
- | CicRefine.Uncertain _
- | CicRefine.AssertFailure _
+ | CicRefine.RefineFailure s
+ | CicRefine.Uncertain s
+ | CicRefine.AssertFailure s as exn ->
+ pp_error goal_proof names (Lazy.force s) exn
+ | CicUtil.Meta_not_found i as exn ->
+ pp_error goal_proof names ("META NOT FOUND: "^string_of_int i) exn
| Invalid_argument "list_fold_left2" as exn ->
- prerr_endline "THE PROOF DOES NOT TYPECHECK!";
- prerr_endline (CicPp.pp goal_proof names);
- prerr_endline "THE PROOF DOES NOT TYPECHECK!";
- raise exn
+ pp_error goal_proof names "Invalid_argument: list_fold_left2" exn
in
let subst_side_effects,real_menv,_ =
try
let pump_actives context bag maxm active passive saturation_steps max_time =
reset_refs();
maxmeta := maxm;
+(*
let max_l l =
List.fold_left
(fun acc e -> let _,_,_,menv,_ = Equality.open_equality e in
List.fold_left (fun acc (i,_,_) -> max i acc) acc menv)
0 l in
- let active_l = fst active in
- let passive_l = fst passive in
- let ma = max_l active_l in
- let mp = max_l passive_l in
+*)
+(* let active_l = fst active in *)
+(* let passive_l = fst passive in *)
+(* let ma = max_l active_l in *)
+(* let mp = max_l passive_l in *)
match LibraryObjects.eq_URI () with
| None -> active, passive, !maxmeta
| Some eq_uri ->
=
reset_refs();
maxmeta := maxm;
+ let active_l = fst active in
+(*
let max_l l =
List.fold_left
(fun acc e -> let _,_,_,menv,_ = Equality.open_equality e in
List.fold_left (fun acc (i,_,_) -> max i acc) acc menv)
0 l
in
- let active_l = fst active in
let passive_l = fst passive in
let ma = max_l active_l in
let mp = max_l passive_l in
+*)
let proof, goalno = status in
let uri, metasenv, meta_proof, term_to_prove, attrs = proof in
let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in