X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=6e792201964824db331fce7d3fc7813bac10be2a;hb=b109559ac6795075508fd5c231a1bf2a3223031a;hp=514cd049e686e5b882af3368c6f4bbdd386daea3;hpb=61a2faa2694907757dd617175e0144705e79d65a;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index 514cd049e..6e7922019 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/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 = @@ -1351,20 +1353,28 @@ let build_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! "; + prerr_endline (CicPp.pp goal_proof names); + prerr_endline "THE PROOF DOES NOT TYPECHECK!"; + prerr_endline error; + prerr_endline "THE PROOF DOES NOT TYPECHECK! "; + raise exn + in let goal_proof,goal_ty,real_menv,_ = (* prerr_endline ("parte la refine per: " ^ (CicPp.pp goal_proof names)); *) try + debug_print (lazy (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 @@ -1376,7 +1386,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 @@ -1385,7 +1395,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 = @@ -1531,15 +1541,17 @@ let build_proof 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 -> @@ -1557,12 +1569,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 @@ -1570,7 +1582,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 @@ -1591,18 +1603,20 @@ let given_clause = 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 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 @@ -1610,10 +1624,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 ????? *)