X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnAuto.ml;h=53c87673bd165861c97ffb4e2564773ef4930725;hb=12f96bd48b460d06f9858a334ee7c52d6831712f;hp=c9162d0fe2080923a5f31deca1fd5ffb5ff7c626;hpb=01efa7df65c658be9b93dbefe3c2de0b8836fa5a;p=helm.git diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml index c9162d0fe..53c87673b 100644 --- a/helm/software/components/ng_tactics/nAuto.ml +++ b/helm/software/components/ng_tactics/nAuto.ml @@ -13,8 +13,10 @@ open Printf -let debug = ref false -let debug_print s = if !debug then prerr_endline (Lazy.force s) else () +let debug = ref true +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 @@ -39,7 +41,7 @@ let auto_paramod ~params:(l,_) status goal = NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l with | [] -> raise (Error (lazy "no proof found",None)) - | (pt, metasenv, subst)::_ -> + | (pt, _, metasenv, subst)::_ -> let status = status#set_obj (n,h,metasenv,subst,o) in instantiate status goal (mk_cic_term (ctx_of gty) pt) ;; @@ -1015,37 +1017,47 @@ 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 - -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 + | S of goal * (#tac_status as 'a) + (* * cic_term * candidate (* int was minsize *) *) + | L of goal * (#tac_status as 'a) -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 + | L (g,_) -> "L" ^ 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,20 +1070,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 @@ -1097,19 +1113,24 @@ 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 in elems ;; +let calculate_goal_ty (goalno,_) status = + try Some (get_goalty status goalno) + with Error _ -> None +;; let equational_and_applicative_case signature flags status g depth gty cache @@ -1121,7 +1142,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 @@ -1132,41 +1153,40 @@ 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,1,s,List.map (fun i -> + let sort = + match calculate_goal_ty (i,()) s with + | None -> assert false + | Some gty -> + let _, sort = typeof s (ctx_of gty) gty in + match term_of_cic_term s sort (ctx_of sort) with + | _, NCic.Sort NCic.Prop -> P + | _ -> (*T*)P + in + i,sort) gl) elems in let elems = sort_new_elems elems in elems, cache ;; -let calculate_goal_ty (goalno,_,_) status = - try Some (get_goalty status goalno) - with Error _ -> None -;; + let d_goals l = let rec aux acc = function | (D g)::tl -> aux (acc@[g]) tl - | (S _)::tl -> aux acc tl + | (S _|L _)::tl -> aux acc tl | [] -> acc in 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 = @@ -1186,11 +1206,10 @@ let intro_case status gno gty depth cache name = 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 (lazy (" intro: "^ string_of_int open_goal)); -(* pp_th status cache; *) + 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,0,status,[open_goal,P]], cache ;; @@ -1202,128 +1221,350 @@ 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")); +module T = ZipTree +module Z = AndOrTree + +let img_counter = ref 0 ;; +let show pos = + incr img_counter; + let file = ("/tmp/a"^string_of_int !img_counter^".dot") in + debug_print (lazy("generating " ^ file)); + debug_do (fun () -> + let oc = open_out file 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 "^file^" > "^file^".png")); + (*ignore(Sys.command ("eog "^file^".png"))*)) +;; + +let rightmost_bro pred pos = + let rec last acc pos = + let acc = if pred pos then Some pos else acc in + match Z.right pos with + | None -> acc + | Some pos -> last acc pos + in + last None pos +;; + +let leftmost_bro pred pos = + let rec fst pos = + if pred pos then Some pos else + match Z.right pos with + | None -> None + | Some pos -> fst pos + in + fst pos +;; + +let rec first_left_mark_L_as_D pred pos = + if pred pos then + Some pos + else + let pos = + match Z.getA pos with + | s,L (g,_) -> + Z.inject T.Nil (Z.setA s (D g) pos) + | _ -> pos + in + match Z.left pos with + | None -> None + | Some pos -> + first_left_mark_L_as_D pred pos +;; + +let is_oS pos = + match Z.getO pos with + | S _ -> true + | D _ | L _ -> false +;; + + +let is_aS pos = + match Z.getA pos with + | _,S _ -> true + | _,D _ | _,L _ -> false +;; + +let is_not_oS x = not (is_oS x);; +let is_not_aS x = not (is_aS x);; + +let is_oL pos = match Z.getO pos with L _ -> true | _ -> false ;; +let is_aL pos = match Z.getA pos with _,L _ -> true | _ -> false ;; + +let is_not_oL x = not (is_oL x) ;; +let is_not_aL x = not (is_aL x) ;; + +let rec forall_left pred pos = + match Z.left pos with + | None -> true + | Some pos -> if pred pos then forall_left pred pos else false +;; + + +let rec product = function + | [] -> [] + | ((g,s) :: tl) as l -> (s,List.map fst l) :: product tl +;; + +let has_no_alternatives (pos : 'a and_pos) = + match Z.getA pos with + | _, L _ -> true + | _ -> false +;; + +let rec collect_left_up (pos : 'a and_pos) = + match Z.left pos with + | Some pos -> + (match Z.getA pos with + | _, L (g,s) -> (g,s) :: collect_left_up pos + | _ -> []) + | None -> + match Z.upA pos with + | None -> [] (* root *) + | Some pos -> collect_left_up (Z.upO pos) +;; + +let compute_failed_goals (pos : 'a and_pos) = + let curr = match Z.getA pos with (s,_,_),D g -> (g,s) | _ -> assert false in + product (List.rev (curr :: collect_left_up pos) ) +;; + +let pp_failures l = + debug_print (lazy("CACHE FAILURES/UNDERINSPECTION")); + List.iter (fun (s,gl) -> + debug_print (lazy("FAIL: " ^ + String.concat " , " (List.map (fun g -> + match calculate_goal_ty g s with + | None -> + (try + let (i,_) = g in + let _,_,_,subst,_ = s#obj in + let _,cc,_,ty = NCicUtils.lookup_subst i subst in + let ty = mk_cic_term cc ty in + string_of_int i^":"^ppterm s ty + with NCicUtils.Subst_not_found _ -> "XXXX") + | Some gty -> + let s, gty = apply_subst s (ctx_of gty) gty in + string_of_int (fst g)^":"^ppterm s gty) gl)))) + l +;; + +let is_closed pos = + match Z.getA pos with + | (s,_,_),S (g,_) + | (s,_,_),D g -> + (match calculate_goal_ty g s with + | None -> true + | Some gty -> metas_of_term s gty = []) + | _, L _ -> assert false +;; + +let auto_main flags signature (pos : 'a and_pos) cache = + let solved g depth size s (pos : 'a and_pos) = + Z.inject (T.Node(`Or,[D g,T.Node(`And(s,depth,size),[])])) pos + in + let failed (pos : 'a and_pos) = + pp_failures (compute_failed_goals 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 _ | L _ -> assert false (* XXX set to Nil when backtrack *) + | D g -> + match Z.downO pos with + | Z.Solution (s,_,_) -> move_solution_up ~unfocus true s pos cache + | Z.Todo pos -> next ~unfocus:true pos cache + + and next_choice_point (pos : 'a and_pos) cache = + + let rec global_choice_point (pos : 'a and_pos) : 'a auto_result = +(* prerr_endline "global"; show pos; *) + match Z.upA pos with + | None -> Gaveup + | Some alts -> + let alts = Z.inject T.Nil alts in + let alts = + match Z.getO alts with + | S (s,g) -> Z.setO (L (s,g)) alts + | D (g) -> Z.setO (L (g,Obj.magic g)) alts + (* L (and other marks) for OR should have no arguments *) + | L _ -> assert false + in + match Z.right alts with + | None -> + let upalts = Z.upO alts in + let upalts = Z.inject T.Nil upalts in + let upalts = + match Z.getA upalts with + | s,S (a,b) -> Z.setA s (L (a,b)) upalts + | _,L _ -> assert false + | s,D (a) -> Z.setA s (L (a,Obj.magic a)) upalts + in + backtrack upalts + | Some pos -> + match Z.downO pos with + | Z.Solution (s,_,_) -> + move_solution_up ~unfocus:false true s pos cache + | Z.Todo pos -> next ~unfocus:true pos cache + + and backtrack (pos : 'a and_pos) : 'a auto_result = +(* prerr_endline "backtrack"; show pos; *) + let pos = Z.inject T.Nil pos in + let pos = + match Z.getA pos with + | s,D g | s, S (g,_) | s,L(g,_) -> Z.setA s (D g) pos + in + match first_left_mark_L_as_D is_aS pos with + | None -> global_choice_point pos + | Some pos -> + let rec local_choice_point pos = +(* prerr_endline "local"; show pos; *) + match Z.downA pos with + | Z.Unexplored -> attack pos cache (Z.getA pos) + | Z.Alternatives alts -> + match leftmost_bro is_not_oL alts with + | None -> assert false (* is not L, thus has alternatives *) + | Some pos -> + let is_D = is_not_oS pos in + match if is_D then Z.downO pos else Z.downOr pos with + | Z.Solution (s,_,_) -> assert(is_D); + move_solution_up ~unfocus:false true s pos cache + | Z.Todo pos when is_D -> attack pos cache (Z.getA pos) + | Z.Todo pos -> + match first_left_mark_L_as_D is_aS pos with + | Some pos -> local_choice_point pos + | None -> assert false + in + local_choice_point pos + in + backtrack pos + + and next_choice (pos : 'a and_pos) cache = + next_choice_point pos cache + + and move_solution_up + ~unfocus are_sons_L + (status : #tac_status as 'a) (pos : 'a or_pos) cache + = + let pos = (* mark as solved *) + match Z.getO pos with + | L _ -> assert false (* XXX *) + | S (g,_) + | D g -> + if are_sons_L then + Z.inject T.Nil (Z.setO (L (g,status)) pos) + else + Z.setO (S (g,status)) pos + in + let has_alternative_or = match Z.right pos with None -> false | _ -> true in + let pos = Z.upO pos in + let are_all_lbro_L = forall_left is_aL pos in + let has_no_alternative = + ((not has_alternative_or) && are_sons_L) || + is_closed pos + in + match Z.getA pos with + | _, L _ -> assert false + | (_, size, depth), S (g,_) + (* S if already solved and then solved again because of a backtrack *) + | (_, size, depth), D g -> + let newg = + if has_no_alternative then (L (g,status)) else (S (g,status))in + (* TODO: cache success g *) + let pos = if has_no_alternative then Z.inject T.Nil pos else pos in + 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 -> + match Z.upA pos with + | None -> Proved (status, Some (pos,cache)) + | Some pos -> + move_solution_up + ~unfocus:true (has_no_alternative && are_all_lbro_L) + status pos cache + + and attack pos cache and_item = + (* show pos; uncomment to show the tree *) + match and_item with + | _, S _ -> assert false (* next would close the proof or give a D *) + | _, L _ -> assert false (* L is a final solution *) + | (_, depth, _),_ when Unix.gettimeofday () > flags.timeout -> + debug_print ~depth (lazy ("fail timeout")); Gaveup - | (s, size, don, (D (gno,depth,_ as g))::todo, fl)::orlist -> - debug_print (lazy "attack goal"); + | (s, depth, width), D (_, T as g) when not flags.do_types -> + debug_print ~depth (lazy "skip goal in Type"); + next ~unfocus:false (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 (Z.eject pos = T.Nil); (*subtree must be unexplored *) match calculate_goal_ty g s with | None -> - debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno)); - aux ((s,size,don,todo, fl)::orlist, cache) + 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)); - 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 - 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) + 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 than before or 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 ^ ") ")); + 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,size_mult,s,gl) -> + D(gno,P), + T.Node (`And + (s,depth+depth_incr,size+size_mult*(size_gl gl)), + List.map (fun g -> D g,T.Nil) gl)) + subgoals + in + next ~unfocus:true + (Z.inject (T.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 +1589,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), T.Nil) goals in + let elems = Z.start (T.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 +1603,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 @@ -1372,10 +1615,44 @@ let auto_tac ~params:(_univ,flags) status = in s#set_stack stack in - up_to 2 depth + up_to depth depth +;; + +let rec rm_assoc n = function + | [] -> assert false + | (x,i)::tl when n=x -> i,tl + | p::tl -> let i,tl = rm_assoc n tl in i,p::tl +;; + +let merge canonicals elements n m = + let cn,canonicals = rm_assoc n canonicals in + let cm,canonicals = rm_assoc m canonicals in + let ln,elements = rm_assoc cn elements in + let lm,elements = rm_assoc cm elements in + let canonicals = + (n,cm)::(m,cm)::List.map + (fun (x,xc) as p -> + if xc = cn then (x,cm) else p) canonicals + in + let elements = (cn,ln@lm)::elements + in + canonicals,elements +;; + +let clusters f l = + let canonicals = List.map (fun x -> (x,x)) l in + let elements = List.map (fun x -> (x,[x])) l in + List.fold_left + (fun (canonicals,elements) x -> + let dep = f x in + List.fold_left + (fun (canonicals,elements) d -> + merge canonicals elements d x) + (canonicals,elements) dep) + (canonicals,elements) l ;; -let group_by_tac eq_predicate tactic status = +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 @@ -1398,7 +1675,7 @@ let group_by_tac eq_predicate tactic status = 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 ] + NTactics.block_tac ([ NTactics.branch_tac ~force:false] @ HExtlib.list_concat ~sep:[NTactics.shift_tac] (List.map (fun gl-> [NTactics.pos_tac (pos_of gl goals); tactic]) classes) @@ -1425,13 +1702,19 @@ let type_dependency status gl g = ;; let auto_tac ~params = - group_by_tac type_dependency (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) = if List.mem_assoc "paramodulation" flags then - auto_paramod_tac ~params + auto_paramod_tac ~params + else if List.mem_assoc "paramod" flags then + NnAuto.paramod_tac ~params + else if List.mem_assoc "fast_paramod" flags then + NnAuto.fast_eq_check_tac ~params + else if List.mem_assoc "slir" flags then + NnAuto.auto_tac ~params else auto_tac ~params ;;