let pp_goal_set msg goals names =
let active_goals, passive_goals = goals in
let pp_goal_set msg goals names =
let active_goals, passive_goals = goals in
;;
let check_if_goal_is_subsumed bag ((_,ctx,_) as env) table (goalproof,menv,ty) =
;;
let check_if_goal_is_subsumed bag ((_,ctx,_) as env) table (goalproof,menv,ty) =
(Printf.sprintf "\n%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)"
iterno (size_of_active active) (size_of_passive passive)
(Printf.sprintf "\n%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)"
iterno (size_of_active active) (size_of_passive passive)
if s_iterno < saturation_steps then
let current, passive = select env goals passive in
(* SIMPLIFICATION OF CURRENT *)
if s_iterno < saturation_steps then
let current, passive = select env goals passive in
(* SIMPLIFICATION OF CURRENT *)
let metasenv,j = CicMkImplicit.mk_implicit_type metasenv [] context in
(i,context,Cic.Meta(j,irl))::metasenv
in
let metasenv,j = CicMkImplicit.mk_implicit_type metasenv [] context in
(i,context,Cic.Meta(j,irl))::metasenv
in
- if proof_menv = [] then prerr_endline "+++++++++++++++VUOTA"
- else prerr_endline (CicMetaSubst.ppmetasenv [] proof_menv);
+ if proof_menv = [] then debug_print (lazy "+++++++++++++++VUOTA")
+ else debug_print (lazy (CicMetaSubst.ppmetasenv [] proof_menv));
let proof, goalno = status in
let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
let eq_uri = eq_of_goal type_of_goal in
let names = Utils.names_of_context context in
let proof, goalno = status in
let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
let eq_uri = eq_of_goal type_of_goal in
let names = Utils.names_of_context context in
let goal_proof,goal_ty,real_menv,_ =
(* prerr_endline ("parte la refine per: " ^ (CicPp.pp goal_proof names)); *)
try
let goal_proof,goal_ty,real_menv,_ =
(* prerr_endline ("parte la refine per: " ^ (CicPp.pp goal_proof names)); *)
try
| CicUnification.AssertFailure s -> assert false
(* fail "Maybe the local context of metas in the goal was not an IRL" s *)
in
| CicUnification.AssertFailure s -> assert false
(* fail "Maybe the local context of metas in the goal was not an IRL" s *)
in
let final_subst =
(goalno,(context,goal_proof,type_of_goal))::subst_side_effects
in
let final_subst =
(goalno,(context,goal_proof,type_of_goal))::subst_side_effects
in
let env = metasenv,context,CicUniv.empty_ugraph in
let cleaned_goal = Utils.remove_local_context type_of_goal in
let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
let env = metasenv,context,CicUniv.empty_ugraph in
let cleaned_goal = Utils.remove_local_context type_of_goal in
let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
active (list_of_passive passive) in
let _,goal = simplify_goal bag env goal table in
let (_,_,ty) = goal in
active (list_of_passive passive) in
let _,goal = simplify_goal bag env goal table in
let (_,_,ty) = goal in
let subsumed = find_all_subsumed bag env (snd table) goal in
let subsumed_or_id =
match (check_if_goal_is_identity env goal) with
let subsumed = find_all_subsumed bag env (snd table) goal in
let subsumed_or_id =
match (check_if_goal_is_identity env goal) with
let metasenv' = List.filter (fun (i,_,_)->i<>goalno) metasenv in
let goal = [], metasenv', cleaned_goal in
let env = metasenv,context,CicUniv.empty_ugraph in
let metasenv' = List.filter (fun (i,_,_)->i<>goalno) metasenv in
let goal = [], metasenv', cleaned_goal in
let env = metasenv,context,CicUniv.empty_ugraph in
- prerr_endline ">>>>>> ACTIVES >>>>>>>>";
- List.iter (fun e -> prerr_endline (Equality.string_of_equality ~env e))
+ debug_print (lazy ">>>>>> ACTIVES >>>>>>>>");
+ List.iter (fun e -> debug_print (lazy (Equality.string_of_equality ~env e)))