From: Enrico Tassi Date: Wed, 28 Oct 2009 13:24:55 +0000 (+0000) Subject: better logging and immediate pruning of new goals when X-Git-Tag: make_still_working~3247 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=114922e4226970a259c71d415307d5268add7d65;p=helm.git better logging and immediate pruning of new goals when - length(goals) > maxwidth - depth = maxdepth and goals <> [] --- diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml index 61e9ff015..525e1bfb6 100644 --- a/helm/software/components/ng_tactics/nAuto.ml +++ b/helm/software/components/ng_tactics/nAuto.ml @@ -14,7 +14,8 @@ open Printf let debug = ref false -let debug_print s = if !debug then prerr_endline (Lazy.force s) else () +let debug_print ?(depth=0) s = + if !debug then prerr_endline (String.make depth '\t'^Lazy.force s) else () let debug_do f = if !debug then f () else () open Continuationals.Stack @@ -1070,17 +1071,21 @@ let sort_new_elems l = List.sort (fun (_,_,_,l1) (_,_,_,l2) -> List.length l1 - List.length l2) l ;; -let try_candidate status t g = +let try_candidate flags depth status t g = try - debug_print (lazy (" try " ^ CicNotationPp.pp_term t)); + debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t)); let status = NTactics.focus_tac [g] status in let status = NTactics.apply_tac ("",0,t) status in let open_goals = head_goals status#stack in - debug_print - (lazy (" success: "^String.concat " "(List.map string_of_int open_goals))); - incr candidate_no; - Some ((!candidate_no,t),status,open_goals) - with Error (msg,exn) -> debug_print (lazy " failed"); None + debug_print ~depth + (lazy ("success: "^String.concat " "(List.map string_of_int open_goals))); + if List.length open_goals > flags.maxwidth || + (depth = flags.maxdepth && open_goals <> []) then + (debug_print ~depth (lazy "pruned immediately"); None) + else + (incr candidate_no; + Some ((!candidate_no,t),status,open_goals)) + with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None ;; let rec mk_irl n = function @@ -1106,13 +1111,14 @@ let get_candidates status cache_th signature gty = List.map (function NCic.Const r -> Ast.NRef r | _ -> assert false) cands ;; -let applicative_case signature status flags g gty cache = +let applicative_case depth signature status flags g gty cache = let candidates = get_candidates status cache signature gty in - debug_print (lazy ("candidates: " ^ string_of_int (List.length candidates))); + debug_print ~depth + (lazy ("candidates: " ^ string_of_int (List.length candidates))); let elems = List.fold_left (fun elems cand -> - match try_candidate status cand g with + match try_candidate flags depth status cand g with | None -> elems | Some x -> x::elems) [] candidates @@ -1130,7 +1136,7 @@ let equational_and_applicative_case signature status flags g gty cache in let more_elems = - applicative_case + applicative_case depth signature status flags g gty cache in elems@more_elems @@ -1141,7 +1147,7 @@ let equational_and_applicative_case smart_applicative_case dbd tables depth s fake_proof goalno gty m context signature universe cache flags | None -> *) - applicative_case + applicative_case depth signature status flags g gty cache in elems @@ -1188,7 +1194,6 @@ let intro_case status gno gty depth cache name = let status, keys = keys_of_term status t in let cache = List.fold_left (add_to_th t) cache keys in debug_print (lazy (" intro: "^ string_of_int open_goal)); -(* pp_th status cache; *) incr candidate_no; (* XXX calculate the sort *) [(!candidate_no,Ast.Implicit `JustOne),0,status,[open_goal,P]], @@ -1217,7 +1222,7 @@ let show pos = Format.fprintf fmt "@?"; close_out oc; ignore(Sys.command ("dot -Tpng /tmp/a.dot > /tmp/a.png")); - ignore(Sys.command ("gnome-open /tmp/a.png"))) + ignore(Sys.command ("eog /tmp/a.png"))) ;; let rightmost_bro pred = @@ -1279,7 +1284,7 @@ let auto_main flags signature (pos : 'a and_pos) cache = and nextO ~unfocus (pos : 'a or_pos) cache = match Z.getO pos with - | S _ -> assert false (* XXX set to Nil when backtracking *) + | S _ -> assert false (* XXX set to Nil when backtrack *) | D g -> match Z.downO pos with | Z.Solution (s,_,_) -> move_solution_up ~unfocus s pos cache @@ -1315,51 +1320,52 @@ let auto_main flags signature (pos : 'a and_pos) cache = | Some pos -> move_solution_up ~unfocus:true status pos cache and attack pos cache and_item = - show pos; + (* show pos; *) match and_item with | _, S _ -> assert false (* next would close the proof or give a D *) - | _ when Unix.gettimeofday () > flags.timeout -> - debug_print (lazy ("fail timeout")); + | (_, depth, _),_ when Unix.gettimeofday () > flags.timeout -> + debug_print ~depth (lazy ("fail timeout")); Gaveup | (s, depth, width), D (_, T as g) when not flags.do_types -> - debug_print (lazy "skip goal in Type"); + debug_print ~depth (lazy "skip goal in Type"); next ~unfocus:true (solved g depth width s pos) cache | (_,depth,_), D _ when depth > flags.maxdepth -> - debug_print (lazy "fail depth"); + debug_print ~depth (lazy "fail depth"); next_choice (failed pos) cache - | (_,_,size), D _ when size > flags.maxsize -> - debug_print (lazy "fail size"); + | (_,depth,size), D _ when size > flags.maxsize -> + debug_print ~depth (lazy "fail size"); next_choice (failed pos) cache | (s,depth,size), D (gno,_ as g) -> (* assert unexplored *) assert (Z.eject pos = ZipTree.Nil); match calculate_goal_ty g s with | None -> - debug_print (lazy ("success side effect: " ^ string_of_int gno)); + debug_print + ~depth (lazy ("success side effect: " ^ string_of_int gno)); next ~unfocus:false (solved g depth size s pos) cache | Some gty -> let s, gty = apply_subst s (ctx_of gty) gty in - debug_print (lazy ("EXAMINE: "^ ppterm s gty)); + debug_print ~depth (lazy ("EXAMINE: "^ ppterm s gty)); match cache_examine cache gty with | `Failed_in d when d <= depth -> - debug_print (lazy ("fail depth (c): "^string_of_int gno)); + debug_print ~depth(lazy("fail depth (c): "^string_of_int gno)); next_choice (failed pos) cache | `UnderInspection -> - debug_print (lazy ("fail loop: " ^ string_of_int gno)); + debug_print ~depth (lazy("fail loop: "^string_of_int gno)); next_choice (failed pos) cache | `Succeded t -> - debug_print (lazy ("success (c): " ^ string_of_int gno)); + debug_print ~depth (lazy("success (c): "^string_of_int gno)); let s = put_in_subst s g t gty in next ~unfocus:true (solved g depth size s pos) cache | `Notfound | `Failed_in _ -> (* more depth or is the first time we see the goal *) if prunable s gty () then - (debug_print (lazy( "fail one father is equal")); + (debug_print ~depth (lazy( "fail one father is equal")); next_choice (failed pos) cache) else let cache = cache_add_underinspection cache gty depth in - debug_print (lazy ("INSPECTING: " ^ + debug_print ~depth (lazy ("INSPECTING: " ^ string_of_int gno ^ "("^ string_of_int size ^ ") ")); (* pos are possible computations for proving gty *) let subgoals, cache =