X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=9739f1ccf44ac84767adc0ea018210d601e3d75f;hb=b0a6c05decc9f0e731f70cfc5ae5350ae4046b79;hp=30561bf07b5df933fecb0da1e3efef1be1539207;hpb=a8b7ed9527a68e33dea2458452147b84cfca7ef6;p=helm.git diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index 30561bf07..9739f1ccf 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -31,6 +31,7 @@ let connect_to_auto = true;; +let debug_print = Utils.debug_print;; (* profiling statistics... *) let infer_time = ref 0.;; @@ -801,13 +802,13 @@ let print_goals goals = let pp_goal_set msg goals names = let active_goals, passive_goals = goals in - prerr_endline ("////" ^ msg); - prerr_endline ("ACTIVE G: " ^ + debug_print (lazy ("////" ^ msg)); + debug_print (lazy ("ACTIVE G: " ^ (String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names) - active_goals))); - prerr_endline ("PASSIVE G: " ^ + active_goals)))); + debug_print (lazy ("PASSIVE G: " ^ (String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names) - passive_goals))) + passive_goals)))) ;; let check_if_goal_is_subsumed bag ((_,ctx,_) as env) table (goalproof,menv,ty) = @@ -990,21 +991,21 @@ let pp_goals label goals context = let names = Utils.names_of_context context in List.iter (fun _,_,g -> - prerr_endline - (Printf.sprintf "Current goal: %s = %s\n" label (CicPp.pp g names))) + debug_print (lazy + (Printf.sprintf "Current goal: %s = %s\n" label (CicPp.pp g names)))) (fst goals); List.iter (fun _,_,g -> - prerr_endline - (Printf.sprintf "PASSIVE goal: %s = %s\n" label (CicPp.pp g names))) + debug_print (lazy + (Printf.sprintf "PASSIVE goal: %s = %s\n" label (CicPp.pp g names)))) (snd goals); ;; let print_status iterno goals active passive = - prerr_endline + debug_print (lazy (Printf.sprintf "\n%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)" iterno (size_of_active active) (size_of_passive passive) - (size_of_goal_set_a goals) (size_of_goal_set_p goals)) + (size_of_goal_set_a goals) (size_of_goal_set_p goals))) ;; (** given-clause algorithm with full reduction strategy: NEW implementation *) @@ -1055,9 +1056,9 @@ let given_clause in match check_if_goals_set_is_solved bag env active goals with | Some p -> - prerr_endline + debug_print (lazy (Printf.sprintf "\nFound a proof in: %f\n" - (Unix.gettimeofday() -. initial_time)); + (Unix.gettimeofday() -. initial_time))); ParamodulationSuccess (p,active,passive) | None -> (* SELECTION *) @@ -1083,9 +1084,9 @@ let given_clause if s_iterno < saturation_steps then let current, passive = select env goals passive in (* SIMPLIFICATION OF CURRENT *) - prerr_endline + debug_print (lazy ("Selected : " ^ - Equality.string_of_equality ~env current); + Equality.string_of_equality ~env current)); forward_simplify bag eq_uri env current active, passive else None, passive @@ -1255,7 +1256,7 @@ let fix_proof metasenv context all_implicits p = try let _ = CicUtil.lookup_meta i metasenv in metasenv with CicUtil.Meta_not_found _ -> - prerr_endline ("not found: "^(string_of_int i)); + debug_print (lazy ("not found: "^(string_of_int i))); let metasenv,j = CicMkImplicit.mk_implicit_type metasenv [] context in (i,context,Cic.Meta(j,irl))::metasenv in @@ -1316,17 +1317,17 @@ let build_proof bag status goalproof newproof subsumption_id subsumption_subst proof_menv = - 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, meta_proof, term_to_prove, attrs = proof 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 - prerr_endline "Proof:"; - prerr_endline + debug_print (lazy "Proof:"); + debug_print (lazy (Equality.pp_proof bag names goalproof newproof subsumption_subst - subsumption_id type_of_goal); + subsumption_id type_of_goal)); (* prerr_endline ("max weight: " ^ (string_of_int (Equality.max_weight goalproof newproof))); @@ -1338,11 +1339,12 @@ let build_proof (ProofEngineHelpers.compare_metasenvs ~newmetasenv:metasenv ~oldmetasenv:proof_menv) in let goal_proof, side_effects_t = - let initial = (* Equality.add_subst subsumption_subst*) newproof in + let initial = Equality.add_subst subsumption_subst newproof in Equality.build_goal_proof bag 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 = @@ -1359,20 +1361,33 @@ let build_proof prerr_endline "THE PROOF DOES NOT TYPECHECK! "; raise exn in + let old_insert_coercions = !CicRefine.insert_coercions 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 + debug_print (lazy (CicPp.ppterm goal_proof)); + CicRefine.insert_coercions := false; + let res = + CicRefine.type_of_aux' + real_menv context goal_proof CicUniv.empty_ugraph + in + CicRefine.insert_coercions := old_insert_coercions; + res with | CicRefine.RefineFailure s | CicRefine.Uncertain s | CicRefine.AssertFailure s as exn -> + CicRefine.insert_coercions := old_insert_coercions; pp_error goal_proof names (Lazy.force s) exn | CicUtil.Meta_not_found i as exn -> + CicRefine.insert_coercions := old_insert_coercions; pp_error goal_proof names ("META NOT FOUND: "^string_of_int i) exn | Invalid_argument "list_fold_left2" as exn -> + CicRefine.insert_coercions := old_insert_coercions; pp_error goal_proof names "Invalid_argument: list_fold_left2" exn + | exn -> + CicRefine.insert_coercions := old_insert_coercions; + raise exn in let subst_side_effects,real_menv,_ = try @@ -1384,7 +1399,7 @@ let build_proof | CicUnification.AssertFailure s -> assert false (* fail "Maybe the local context of metas in the goal was not an IRL" s *) in - prerr_endline "+++++++++++++ FINE UNIF"; + Utils.debug_print (lazy "+++++++++++++ FINE UNIF"); let final_subst = (goalno,(context,goal_proof,type_of_goal))::subst_side_effects in @@ -1393,7 +1408,7 @@ let build_proof *) let proof, real_metasenv = ProofEngineHelpers.subst_meta_and_metasenv_in_proof - proof goalno (CicMetaSubst.apply_subst final_subst) + proof goalno final_subst (List.filter (fun i,_,_ -> i<>goalno ) real_menv) in let open_goals = @@ -1567,12 +1582,12 @@ let pump_actives context bag maxm active passive saturation_steps max_time = let all_subsumed bag maxm status active passive = maxmeta := maxm; let proof, goalno = status in - let uri, metasenv, meta_proof, term_to_prove, attrs = proof 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 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 - prerr_endline (string_of_int (List.length (fst active))); + debug_print (lazy (string_of_int (List.length (fst active)))); (* we simplify using both actives passives *) let table = List.fold_left @@ -1580,7 +1595,7 @@ let all_subsumed bag maxm status active passive = active (list_of_passive passive) in let _,goal = simplify_goal bag env goal table in let (_,_,ty) = goal in - prerr_endline (CicPp.ppterm ty); + debug_print (lazy (CicPp.ppterm ty)); let subsumed = find_all_subsumed bag env (snd table) goal in let subsumed_or_id = match (check_if_goal_is_identity env goal) with @@ -1614,7 +1629,7 @@ let given_clause let mp = max_l passive_l in *) let proof, goalno = status in - let uri, metasenv, meta_proof, term_to_prove, attrs = proof 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 cleaned_goal = Utils.remove_local_context type_of_goal in @@ -1622,10 +1637,10 @@ let given_clause 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))) active_l; - prerr_endline ">>>>>>>>>>>>>>"; + debug_print (lazy ">>>>>>>>>>>>>>"); let goals = make_goal_set goal in match (* given_caluse non prende in input maxm ????? *)