From: Enrico Tassi Date: Wed, 28 Oct 2009 12:32:41 +0000 (+0000) Subject: auto navigates a real tree, not a flattened one X-Git-Tag: make_still_working~3248 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8264a2dce28f3a4b170d4e61e3ff87629ca29479;p=helm.git auto navigates a real tree, not a flattened one --- diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml index e68f02d2a..61e9ff015 100644 --- a/helm/software/components/ng_tactics/nAuto.ml +++ b/helm/software/components/ng_tactics/nAuto.ml @@ -15,6 +15,7 @@ open Printf let debug = ref false let debug_print s = if !debug then prerr_endline (Lazy.force s) else () +let debug_do f = if !debug then f () else () open Continuationals.Stack open NTacStatus @@ -1015,37 +1016,45 @@ type cache_examination_result = ] type sort = T | P -type goal = int * int * sort (* goal, depth, sort *) +type goal = int * sort (* goal, depth, sort *) type fail = goal * cic_term type candidate = int * Ast.term (* unique candidate number, candidate *) -type op = +type 'a op = (* goal has to be proved *) | D of goal (* goal has to be cached as a success obtained using candidate as the first * step *) - | S of goal * cic_term * candidate (* int was minsize *) -type 'a elem = - (* menv, subst, size, operations done (only S), operations to do, - * failures to cache if any op fails *) - (#tac_status as 'a) * int * op list * op list * fail list + | S of goal * (#tac_status as 'a) + (* * cic_term * candidate (* int was minsize *) *) -type 'a auto_status = - (* list of computations that may lead to the solution: all op list will - * end with the same (S(g,_)) *) - 'a elem list * th_cache - -type 'a auto_result = - | Gaveup - | Proved of (#tac_status as 'a) * 'a auto_status (* alt. proofs *) +let pp_goal (g,_) = string_of_int g +let pp_item = function + | D g -> "D" ^ pp_goal g + | S (g,_) -> "S" ^ pp_goal g type flags = { do_types : bool; (* solve goals in Type *) maxwidth : int; maxsize : int; + maxdepth : int; timeout : float; } +type 'a tree_status = #tac_status as 'a * int * int +type 'a tree_item = 'a op + +type 'a and_pos = + (AndOrTree.andT, 'a tree_status, 'a tree_item) AndOrTree.position +type 'a or_pos = + (AndOrTree.orT, 'a tree_status, 'a tree_item) AndOrTree.position + +type 'a auto_status = 'a and_pos * th_cache + +type 'a auto_result = + | Gaveup + | Proved of (#tac_status as 'a) * 'a auto_status option (* alt. proofs *) + let close_failures _ c = c;; let prunable _ _ _ = false;; let cache_examine cache gty = `Notfound;; @@ -1058,7 +1067,7 @@ let only _ _ _ = true;; let candidate_no = ref 0;; let sort_new_elems l = - List.sort (fun (_,_,l1) (_,_,l2) -> List.length l1 - List.length l2) l + List.sort (fun (_,_,_,l1) (_,_,_,l2) -> List.length l1 - List.length l2) l ;; let try_candidate status t g = @@ -1139,13 +1148,13 @@ let equational_and_applicative_case in let elems = (* XXX calculate the sort *) - List.map (fun c,s,gl -> c,s,List.map (fun i -> i,depth-1,P) gl) elems + List.map (fun c,s,gl -> c,1,s,List.map (fun i -> i,P) gl) elems in let elems = sort_new_elems elems in elems, cache ;; -let calculate_goal_ty (goalno,_,_) status = +let calculate_goal_ty (goalno,_) status = try Some (get_goalty status goalno) with Error _ -> None ;; @@ -1160,14 +1169,6 @@ let d_goals l = let prop_only l = List.filter (function (_,_,P) -> true | _ -> false) l ;; -let remove_s_from_fl (id,_,_) (fl : fail list) = - let rec aux = function - | [] -> [] - | ((id1,_,_),_)::tl when id = id1 -> tl - | hd::tl -> hd :: aux tl - in - aux fl -;; let rec guess_name name ctx = if name = "_" then guess_name "auto" ctx else @@ -1190,7 +1191,7 @@ let intro_case status gno gty depth cache name = (* pp_th status cache; *) incr candidate_no; (* XXX calculate the sort *) - [(!candidate_no,Ast.Implicit `JustOne),status,[open_goal,depth,P]], + [(!candidate_no,Ast.Implicit `JustOne),0,status,[open_goal,P]], cache ;; @@ -1202,128 +1203,186 @@ let do_something signature flags s gno depth gty cache = equational_and_applicative_case signature flags s gno depth gty cache ;; -let auto_main flags signature elems cache = - let rec aux (elems, cache : 'a auto_status) = -(* processa le hint dell'utente *) -(* let cache, elems = filter_prune_hint cache elems in *) - match elems with -(* USER HINT - | (m, s, size, don, todo, fl)::orlist when !hint <> None -> - debug_print (lazy "skip"); - (match !hint with - | Some i when condition_for_hint i todo -> - aux tables flags cache orlist - | _ -> - hint := None; - aux tables flags cache elems) -*) - | [] -> - debug_print (lazy "gave up"); - Gaveup - | (s, _, _, [],_)::orlist -> - debug_print (lazy "success"); - Proved (s, (orlist, cache)) - | (s, size, don, (D (_,_,T))::todo, fl)::orlist - when not flags.do_types -> - debug_print (lazy "skip goal in Type"); - aux ((s, size, don, todo, fl)::orlist, cache) - | (s, size, don, (S(g, key, c) as op)::todo, fl)::orlist -> - let cache, orlist, fl, sibling_pruned = - add_to_cache_and_del_from_orlist_if_green_cut - g s cache key todo orlist fl size - in - let fl = remove_s_from_fl g fl in - let don = if sibling_pruned then don else op::don in - let s = NTactics.unfocus_tac s in - aux ((s, size, don, todo, fl)::orlist, cache) - | (s, size, don, todo, fl)::orlist - when List.length(prop_only (d_goals todo)) > flags.maxwidth -> - debug_print (lazy ("FAIL: WIDTH: " ^ - String.concat ", " - (List.map (fun (x,_,_) -> string_of_int x) (d_goals todo)))); - aux (orlist, cache) - | (s, size, don, todo, fl)::orlist when size > flags.maxsize -> - debug_print (lazy ("FAIL: SIZE: "^string_of_int size ^ - " > " ^ string_of_int flags.maxsize ^ ": " ^ - String.concat ", " - (List.map (fun (x,_,_) -> string_of_int x) (d_goals todo)))); - aux (orlist, cache) - | _ when Unix.gettimeofday () > flags.timeout -> - debug_print (lazy ("FAIL: TIMEOUT")); - Gaveup - | (s, size, don, (D (gno,depth,_ as g))::todo, fl)::orlist -> - debug_print (lazy "attack goal"); - match calculate_goal_ty g s with +module T = ZipTree +module Z = AndOrTree + +let show pos = + debug_print (lazy("generating a.dot")); + debug_do (fun () -> + let oc = open_out "/tmp/a.dot" in + let fmt = Format.formatter_of_out_channel oc in + GraphvizPp.Dot.header fmt; + Z.dump pp_item pos fmt; + GraphvizPp.Dot.trailer fmt; + 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"))) +;; + +let rightmost_bro pred = + let rec fst pos = + match Z.right pos with + | None -> None + | Some pos -> + if pred pos then Some pos else fst pos + in + fst +;; + +let is_not_S pos = + match Z.getO pos with + | S _ -> false + | D _ -> true +;; + +let rec next_choice_point (pos : 'a and_pos) : 'a or_pos option = + let rec giveup_right_giveup_up_backtrack_left (pos : 'a and_pos) = + match Z.upA pos with + | None -> None + | Some alts -> + match rightmost_bro is_not_S alts with + | None -> + let upalts = Z.upO alts in + let upalts = Z.inject T.Nil upalts in + backtrack_left_giveup_right_giveup_up upalts + | Some _ as x -> x + and backtrack_left_giveup_right_giveup_up (pos : 'a and_pos) = + let pos = Z.inject T.Nil pos in + let pos = match Z.getA pos with s,D g | s, S (g,_) -> Z.setA s (D g) pos in + match Z.left pos with + | None -> giveup_right_giveup_up_backtrack_left pos + | Some (pos as left_bro) -> + match Z.downA pos with + | Z.Unexplored -> assert false (* we explore left2right *) + | Z.Alternatives alts -> + match rightmost_bro is_not_S alts with + | None -> backtrack_left_giveup_right_giveup_up left_bro + | Some _ as x -> x + in + backtrack_left_giveup_right_giveup_up pos +;; + +let auto_main flags signature (pos : 'a and_pos) cache = + let solved g depth size s pos = + Z.inject (T.Node(`Or,[D g,T.Node(`And(s,depth,size),[])])) pos + in + let failed pos = + Z.inject (T.Node(`Or,[])) pos + in + + let rec next ~unfocus (pos : 'a and_pos) cache = + (* USER HINT *) + match Z.downA pos with + | Z.Unexplored -> attack pos cache (Z.getA pos) + | Z.Alternatives pos -> nextO ~unfocus pos cache + + and nextO ~unfocus (pos : 'a or_pos) cache = + match Z.getO pos with + | S _ -> assert false (* XXX set to Nil when backtracking *) + | D g -> + match Z.downO pos with + | Z.Solution (s,_,_) -> move_solution_up ~unfocus s pos cache + | Z.Todo pos -> next ~unfocus:true pos cache + + and next_choice (pos : 'a and_pos) cache = + match next_choice_point pos with + | None -> Gaveup + | Some pos -> nextO ~unfocus:true pos cache + + and move_solution_up + ~unfocus (status : #tac_status as 'a) (pos : 'a or_pos) cache + = + let pos = (* mark as solved *) + match Z.getO pos with + | S _ -> assert false (* XXX *) + | D g -> Z.setO (S (g,status)) pos + in + let pos = Z.upO pos in + match Z.getA pos with + | (_, size, depth), S (g,_) + (* S if already solved and then solved again because of a backtrack *) + | (_, size, depth), D g -> + let newg = S (g,status) in(* TODO: cache success g *) + let status = if unfocus then NTactics.unfocus_tac status else status in + let news = status,size,depth in + let pos = Z.setA news newg pos in + match Z.right pos with + | Some pos -> next ~unfocus:true pos cache | None -> - debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno)); - aux ((s,size,don,todo, fl)::orlist, cache) - | Some gty -> - let s, gty = apply_subst s (ctx_of gty) gty in - debug_print (lazy ("EXAMINE: "^ ppterm s gty)); - match cache_examine cache gty with - | `Failed_in d when d >= depth -> - debug_print (lazy ("FAIL: DEPTH (cache): "^string_of_int gno)); - let cache = close_failures fl cache in - aux (orlist, cache) - | `UnderInspection -> - debug_print (lazy ("FAIL: LOOP: " ^ string_of_int gno)); - let cache = close_failures fl cache in - aux (orlist,cache) - | `Succeded t -> - debug_print (lazy ("SUCCESS: CACHE HIT: " ^ string_of_int gno)); - let s = put_in_subst s g t gty in - aux ((s, size, don,todo, fl)::orlist, cache) - | `Notfound - | `Failed_in _ when depth > 0 -> - ( (* more depth or is the first time we see the goal *) - if prunable s gty todo then - (debug_print (lazy( "FAIL: LOOP: one father is equal")); - let cache = close_failures fl cache in - aux (orlist,cache)) - else - let cache = cache_add_underinspection cache gty depth in - debug_print (lazy ("INSPECTING: " ^ - string_of_int gno ^ "("^ string_of_int size ^ "): "^ - ppterm s gty)); - (* elems are possible computations for proving gty *) - let elems, cache = - do_something signature flags s gno depth gty cache + match Z.upA pos with + | None -> Proved (status, Some (pos,cache)) + | Some pos -> move_solution_up ~unfocus:true status pos cache + + and attack pos cache and_item = + 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")); + Gaveup + | (s, depth, width), D (_, T as g) when not flags.do_types -> + debug_print (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"); + next_choice (failed pos) cache + | (_,_,size), D _ when size > flags.maxsize -> + debug_print (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)); + 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)); + match cache_examine cache gty with + | `Failed_in d when d <= depth -> + debug_print (lazy ("fail depth (c): "^string_of_int gno)); + next_choice (failed pos) cache + | `UnderInspection -> + debug_print (lazy ("fail loop: " ^ string_of_int gno)); + next_choice (failed pos) cache + | `Succeded t -> + debug_print (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")); + next_choice (failed pos) cache) + else + let cache = cache_add_underinspection cache gty depth in + debug_print (lazy ("INSPECTING: " ^ + string_of_int gno ^ "("^ string_of_int size ^ ") ")); + (* pos are possible computations for proving gty *) + let subgoals, cache = + do_something signature flags s gno depth gty cache + in + if subgoals = [] then (* this goal has failed *) + next_choice (failed pos) cache + else + let size_gl l = List.length + (List.filter (function (_,P) -> true | _ -> false) l) + in + let subtrees = + List.map (fun (_cand,depth_incr,s,gl) -> + D(gno,P), + ZipTree.Node ( + `And (s,depth+depth_incr,size+size_gl gl), + List.map (fun g -> D g,ZipTree.Nil) gl)) + subgoals in - if elems = [] then - (* this goal has failed *) - let cache = close_failures ((g,gty)::fl) cache in - aux (orlist, cache) - else - let size_gl l = List.length - (List.filter (function (_,_,P) -> true | _ -> false) l) - in - let elems = - let inj_gl gl = List.map (fun g -> D g) gl in - let rec map = function - | [] -> assert false - | (cand,s,gl)::[] -> - let todo = - inj_gl gl @ (S(g,gty,cand))::todo - in - (* we are the last in OR, we fail on g and - * also on all failures implied by g *) - (s, size + size_gl gl, don, todo, (g,gty)::fl) - :: orlist - | (cand,s,gl)::tl -> - let todo = - inj_gl gl @ (S(g,gty,cand))::todo - in - (s, size + size_gl gl, don, todo, []) :: map tl - in - map elems - in - aux (elems, cache)) - | _ -> - debug_print (lazy ("FAIL: DEPTH: " ^ string_of_int gno)); - let cache = close_failures fl cache in - aux (orlist, cache) + next ~unfocus:true + (Z.inject (ZipTree.Node (`Or,subtrees)) pos) cache in - (aux (elems, cache) : 'a auto_result) + (next ~unfocus:true pos cache : 'a auto_result) ;; let int name l def = @@ -1348,12 +1407,13 @@ let auto_tac ~params:(_univ,flags) status = let size = int "size" flags 10 in let width = int "width" flags (3+List.length goals) in (* XXX fix sort *) - let goals depth = List.map (fun i -> D(i,depth,P)) goals in - let elems depth = [status,0,[],goals depth,[]] in + let goals = List.map (fun i -> D(i,P), ZipTree.Nil) goals in + let elems = Z.start (ZipTree.Node (`And(status,0,0),goals)) in let signature = () in let flags = { maxwidth = width; maxsize = size; + maxdepth = depth; timeout = Unix.gettimeofday() +. 3000.; do_types = false; } in @@ -1361,9 +1421,10 @@ let auto_tac ~params:(_univ,flags) status = if x > y then raise (Error (lazy "auto gave up", None)) else let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in - match auto_main flags signature (elems x) cache with + let flags = { flags with maxdepth = x } in + match auto_main flags signature elems cache with | Gaveup -> up_to (x+1) y - | Proved (s, (_orlist, _cache)) -> + | Proved (s, _) -> HLog.debug ("proved at depth " ^ string_of_int x); let stack = match s#stack with