X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnAuto.ml;h=267f3b10bb1dc30c6fd604f9c86be623a5c13417;hb=b880d8ac3206602be68919dd93038e607ae08550;hp=d3409bcbeea21164c8ccc036406b6db48f449f0c;hpb=6ec8ad120e5b2dd2f054cbdf83845453a7be7bcc;p=helm.git diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml index d3409bcbe..267f3b10b 100644 --- a/helm/software/components/ng_tactics/nAuto.ml +++ b/helm/software/components/ng_tactics/nAuto.ml @@ -14,7 +14,9 @@ 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 open NTacStatus @@ -915,37 +917,50 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goa type th_cache = (NCic.context * InvRelDiscriminationTree.t) list +let keys_of_term status t = + let status, orig_ty = typeof status (ctx_of t) t in + let _, ty, _ = saturate ~delta:max_int status orig_ty in + let keys = [ty] in + let keys = + let _, ty = term_of_cic_term status ty (ctx_of ty) in + match ty with + | NCic.Const (NReference.Ref (_,NReference.Def h)) + | NCic.Appl (NCic.Const(NReference.Ref(_,NReference.Def h))::_) + when h > 0 -> + let _,ty,_= saturate status ~delta:(h-1) orig_ty in + ty::keys + | _ -> keys + in + status, keys +;; + let mk_th_cache status gl = List.fold_left (fun (status, acc) g -> let gty = get_goalty status g in let ctx = ctx_of gty in + debug_print(lazy("th cache for: "^ppterm status gty)); + debug_print(lazy("th cache in: "^ppcontext status ctx)); if List.mem_assq ctx acc then status, acc else let idx = InvRelDiscriminationTree.empty in let status,_,idx = - List.fold_left (fun (status, i, idx) _ -> - let t = mk_cic_term ctx (NCic.Rel i) in - let status, orig_ty = typeof status ctx t in - let _, ty, _ = saturate ~delta:max_int status orig_ty in - let idx = InvRelDiscriminationTree.index idx ty t in - let idx = - let _, ty = term_of_cic_term status ty (ctx_of ty) in - match ty with - | NCic.Const (NReference.Ref (_,NReference.Def h)) - | NCic.Appl (NCic.Const(NReference.Ref(_,NReference.Def h))::_) - when h > 0 -> - let _,ty,_= saturate status ~delta:(h-1) orig_ty in - InvRelDiscriminationTree.index idx ty t - | _ -> idx - in - status, i+1, idx) + List.fold_left + (fun (status, i, idx) _ -> + let t = mk_cic_term ctx (NCic.Rel i) in + debug_print(lazy("indexing: "^ppterm status t)); + let status, keys = keys_of_term status t in + let idx = + List.fold_left (fun idx k -> + InvRelDiscriminationTree.index idx k t) idx keys + in + status, i+1, idx) (status, 1, idx) ctx in status, (ctx, idx) :: acc) (status,[]) gl ;; -let add_to_th t ty c = +let add_to_th t c ty = let key_c = ctx_of t in if not (List.mem_assq key_c c) then (key_c ,InvRelDiscriminationTree.index @@ -960,6 +975,25 @@ let add_to_th t ty c = replace c ;; +let pp_idx status idx = + InvRelDiscriminationTree.iter idx + (fun k set -> + debug_print(lazy("K: " ^ NCicInverseRelIndexable.string_of_path k)); + Ncic_termSet.iter + (fun t -> debug_print(lazy("\t"^ppterm status t))) + set) +;; + +let pp_th status = + List.iter + (fun ctx, idx -> + debug_print(lazy( "-----------------------------------------------")); + debug_print(lazy( (NCicPp.ppcontext ~metasenv:[] ~subst:[] ctx))); + debug_print(lazy( "||====> ")); + pp_idx status idx) +;; + + let search_in_th gty th = let c = ctx_of gty in let rec aux acc = function @@ -975,20 +1009,6 @@ let search_in_th gty th = in aux Ncic_termSet.empty c ;; - -let pp_th status = - List.iter - (fun ctx, idx -> - prerr_endline "-----------------------------------------------"; - prerr_endline (NCicPp.ppcontext ~metasenv:[] ~subst:[] ctx); - prerr_endline "||====> "; - InvRelDiscriminationTree.iter idx - (fun k set -> - prerr_endline ("K: " ^ NCicInverseRelIndexable.string_of_path k); - Ncic_termSet.iter - (fun t -> prerr_endline ("\t"^ppterm status t)) set)) -;; - type cache_examination_result = [ `Failed_in of int | `UnderInspection @@ -997,37 +1017,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;; @@ -1040,20 +1068,24 @@ 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 = +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 @@ -1079,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 @@ -1103,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 @@ -1114,20 +1147,20 @@ 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 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 ;; @@ -1140,15 +1173,7 @@ let d_goals l = aux [] 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 + List.filter (function (_,P) -> true | _ -> false) l ;; let rec guess_name name ctx = @@ -1163,19 +1188,15 @@ let intro_case status gno gty depth cache name = let open_goals = head_goals status#stack in assert (List.length open_goals = 1); let open_goal = List.hd open_goals in - let status, cache = - let ngty = get_goalty status open_goal in - let ctx = ctx_of ngty in - let t = mk_cic_term ctx (NCic.Rel 1) in - let status, ty = typeof status ctx t in - let _status, ty, _args = saturate status ty in - status, add_to_th t ty cache - in - debug_print (lazy (" intro: "^ string_of_int open_goal)); -(* pp_th status cache; *) + let ngty = get_goalty status open_goal in + let ctx = ctx_of ngty in + let t = mk_cic_term ctx (NCic.Rel 1) in + let status, keys = keys_of_term status t in + let cache = List.fold_left (add_to_th t) cache keys in + debug_print ~depth (lazy ("intro: "^ string_of_int open_goal)); 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 ;; @@ -1187,124 +1208,185 @@ 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")); - 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 )); - 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 ("eog /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 = + (* TODO: process USER HINT is any *) + 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 backtrack *) + | 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 *) + | (_, 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 ~depth (lazy "skip goal in Type"); + next ~unfocus:true (solved g depth width s pos) cache + | (_,depth,_), D _ when depth > flags.maxdepth -> + debug_print ~depth (lazy "fail depth"); + next_choice (failed pos) cache + | (_,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 + ~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 ~depth (lazy ("EXAMINE: "^ ppterm s gty)); + match cache_examine cache gty with + | `Failed_in d when d <= depth -> + debug_print ~depth(lazy("fail depth (c): "^string_of_int gno)); + next_choice (failed pos) cache + | `UnderInspection -> + debug_print ~depth (lazy("fail loop: "^string_of_int gno)); + next_choice (failed pos) cache + | `Succeded t -> + 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 ~depth (lazy( "fail one father is equal")); + next_choice (failed pos) cache) + else + let cache = cache_add_underinspection cache gty depth in + debug_print ~depth (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 (prop_only 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 = @@ -1315,28 +1397,101 @@ let int name l def = let auto_tac ~params:(_univ,flags) status = let goals = head_goals status#stack in let status, cache = mk_th_cache status goals in +(* pp_th status cache; *) +(* + NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t -> + debug_print (lazy( + NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^ + String.concat "\n " (List.map ( + NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[]) + (NDiscriminationTree.TermSet.elements t)) + ))); +*) let depth = int "depth" flags 3 in + let size = int "size" flags 10 in + let width = int "width" flags (3+List.length goals) in (* XXX fix sort *) - let goals = List.map (fun i -> D(i,depth,P)) goals in - let elems = [status,0,[],goals,[]] 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 = 3 + List.length goals; - maxsize = 10; + maxwidth = width; + maxsize = size; + maxdepth = depth; timeout = Unix.gettimeofday() +. 3000.; do_types = false; } in - match auto_main flags signature elems cache with - | Gaveup -> raise (Error (lazy "auto gave up", None)) - | Proved (s, (_orlist, _cache)) -> - let stack = - match s#stack with - | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest - | _ -> assert false - in - s#set_stack stack + let rec up_to x y = + if x > y then raise (Error (lazy "auto gave up", None)) + else + let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in + let flags = { flags with maxdepth = x } in + match auto_main flags signature elems cache with + | Gaveup -> up_to (x+1) y + | Proved (s, _) -> + HLog.debug ("proved at depth " ^ string_of_int x); + let stack = + match s#stack with + | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest + | _ -> assert false + in + s#set_stack stack + in + up_to 2 depth ;; +let group_by_tac ~eq_predicate ~action:tactic status = + let goals = head_goals status#stack in + if List.length goals < 2 then tactic status + else + let eq_predicate = eq_predicate status in + let rec aux classes = function + | [] -> classes + | g :: tl -> + try + let c = List.find (fun c -> eq_predicate c g) classes in + let classes = List.filter ((<>) c) classes in + aux ((g::c) :: classes) tl + with Not_found -> aux ([g] :: classes) tl + in + let classes = aux [] goals in + List.iter + (fun l -> + HLog.debug ("cluster:" ^ String.concat "," (List.map string_of_int l))) + classes; + let pos_of l1 l2 = + let l2 = HExtlib.list_mapi (fun x i -> x,i+1) l2 in + List.map (fun x -> List.assoc x l2) l1 + in + NTactics.block_tac ([ NTactics.branch_tac ] + @ + HExtlib.list_concat ~sep:[NTactics.shift_tac] + (List.map (fun gl-> [NTactics.pos_tac (pos_of gl goals); tactic]) classes) + @ + [ NTactics.merge_tac ]) status +;; + +module IntSet = Set.Make(struct type t = int let compare = compare end) + +let type_dependency status gl g = + let rec closure acc = function + | [] -> acc + | x::l when IntSet.mem x acc -> closure acc l + | x::l -> + let acc = IntSet.add x acc in + let gty = get_goalty status x in + let deps = metas_of_term status gty in + closure acc (deps @ l) + in + not (IntSet.is_empty + (IntSet.inter + (closure IntSet.empty gl) + (closure IntSet.empty [g]))) +;; + +let auto_tac ~params = + group_by_tac ~eq_predicate:type_dependency ~action:(auto_tac ~params) +;; (* ========================= dispatching of auto/auto_paramod ============ *) let auto_tac ~params:(_,flags as params) =