X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnAuto.ml;h=53c87673bd165861c97ffb4e2564773ef4930725;hb=12f96bd48b460d06f9858a334ee7c52d6831712f;hp=fbb43cbb0298d3e5c40113b761256a3eeec2c029;hpb=b032b1dd4eab94d5bd43f6daf5ca5f9939ebc895;p=helm.git diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml index fbb43cbb0..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 = true -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 @@ -28,7 +30,7 @@ let auto_paramod ~params:(l,_) status goal = let status, l = List.fold_left (fun (status, l) t -> - let status, t = disambiguate status t None (ctx_of gty) in + let status, t = disambiguate status (ctx_of gty) t None in let status, ty = typeof status (ctx_of t) t in let status, t = term_of_cic_term status t (ctx_of gty) in let status, ty = term_of_cic_term status ty (ctx_of ty) in @@ -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) ;; @@ -912,20 +914,101 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goa ;; *) -module CacheElem : Set.OrderedType = - struct - type t = - | Failed_in of int * NCic.term (* depth, goal type *) - | Succeded of Cic.term * Cic.term (* proof, proof type *) - | UnderInspection of Cic.term (* avoid looping *) - let compare = Pervasives.compare - end +type th_cache = (NCic.context * InvRelDiscriminationTree.t) list -module CacheSet = Set.Make(CacheElem) -module Cache = - Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(CacheSet) +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 + 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 c ty = + let key_c = ctx_of t in + if not (List.mem_assq key_c c) then + (key_c ,InvRelDiscriminationTree.index + InvRelDiscriminationTree.empty ty t ) :: c + else + let rec replace = function + | [] -> [] + | (x, idx) :: tl when x == key_c -> + (x, InvRelDiscriminationTree.index idx ty t) :: tl + | x :: tl -> x :: replace tl + in + 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 + | [] -> Ncic_termSet.elements acc + | (_::tl) as k -> + try + let idx = List.assq k th in + let acc = Ncic_termSet.union acc + (InvRelDiscriminationTree.retrieve_unifiables idx gty) + in + aux acc tl + with Not_found -> aux acc tl + in + aux Ncic_termSet.empty c +;; type cache_examination_result = [ `Failed_in of int | `UnderInspection @@ -934,106 +1017,133 @@ 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 * NCic.term (* unique candidate number, candidate *) +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 *) *) + | L of goal * (#tac_status as 'a) -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 * Cache.t - -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;; let put_in_subst s _ _ _ = s;; -let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ _ = c, o, f, false ;; +let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;; let cache_add_underinspection c _ _ = c;; -let equational_case _ _ _ _ _ _ _ = [];; -let sort_new_elems l = l;; +let equational_case _ _ _ _ _ _ = [];; let only _ _ _ = true;; let candidate_no = ref 0;; -let try_candidate status t g = +let sort_new_elems l = + List.sort (fun (_,_,_,_,l1) (_,_,_,_,l2) -> List.length l1 - List.length l2) l +;; + +let try_candidate flags depth status t g = try - debug_print (lazy (" try " ^ - NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t - )); - let ast_for_t = - match t with - | NCic.Rel i -> assert false - | NCic.Const ref -> Ast.NRef ref - | _ -> assert false - in + debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t)); let status = NTactics.focus_tac [g] status in - let status = NTactics.apply_tac ("",0,ast_for_t) status in + let status = NTactics.apply_tac ("",0,t) status in let open_goals = head_goals status#stack in - incr candidate_no; - Some ((!candidate_no,t),status,open_goals) - with Error (msg,exn) -> debug_print msg; 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 + | [] -> [] + | _ :: tl -> NCic.Rel n :: mk_irl (n+1) tl +;; -let get_candidates status context gty = +let get_candidates status cache_th signature gty = let universe = status#auto_cache in - let _, gty = term_of_cic_term status gty (ctx_of gty) in + let context = ctx_of gty in + let _, raw_gty = term_of_cic_term status gty context in + let cands = + NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe raw_gty + in let cands = - NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe gty + List.filter (only signature context) + (NDiscriminationTree.TermSet.elements cands) in - (* XXX we have to trie for the context *) - NDiscriminationTree.TermSet.elements cands + List.map (fun t -> + let _status, t = term_of_cic_term status t context in Ast.NCic t) + (search_in_th gty cache_th) + @ + List.map (function NCic.Const r -> Ast.NRef r | _ -> assert false) cands ;; -let applicative_case signature status flags g gty cache context = - let candidates = get_candidates status context gty in - let candidates = List.filter (only signature context) candidates in - debug_print (lazy ("candidates: " ^ string_of_int (List.length candidates))); +let applicative_case depth signature status flags g gty cache = + let candidates = get_candidates status cache signature gty in + 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 context + signature flags status g depth gty cache = let elems = if false (*is_equational_case gty flags*) then let elems = equational_case - signature status flags g gty cache context + signature status flags g gty cache in let more_elems = - applicative_case - signature status flags g gty cache context + applicative_case depth + signature status flags g gty cache in elems@more_elems else @@ -1043,193 +1153,568 @@ 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 - signature status flags g gty cache context + 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 + 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 + 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 auto_main context 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 context 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")); + +let rec guess_name name ctx = + if name = "_" then guess_name "auto" ctx else + if not (List.mem_assoc name ctx) then name else + guess_name (name^"'") ctx +;; + +let intro_case status gno gty depth cache name = + let status = NTactics.focus_tac [gno] status in + let status = NTactics.intro_tac (guess_name name (ctx_of gty)) status in + let open_goals = head_goals status#stack in + assert (List.length open_goals = 1); + let open_goal = List.hd open_goals in + 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),0,0,status,[open_goal,P]], + cache +;; + +let do_something signature flags s gno depth gty cache = + let _s, raw_gty = term_of_cic_term s gty (ctx_of gty) in + match raw_gty with + | NCic.Prod (name,_,_) -> intro_case s gno gty depth cache name + | _ -> + equational_and_applicative_case signature flags s gno depth gty cache +;; + +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 -> - 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 = - equational_and_applicative_case - signature flags s gno depth gty cache context - 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 auto_tac ~params status = - let cache = Cache.empty in +let int name l def = + try int_of_string (List.assoc name l) + with Failure _ | Not_found -> def +;; + +let auto_tac ~params:(_univ,flags) status = let goals = head_goals status#stack in - let depth = 3 in (* XXX fix sort *) - let goals = List.map (fun i -> D(i,depth,P)) goals in - let elems = [status,0,[],goals,[]] in - let context = [] (* XXX big problem *) 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,P), T.Nil) goals in + let elems = Z.start (T.Node (`And(status,0,0),goals)) in let signature = () in let flags = { - maxwidth = 3; - maxsize = 10; + maxwidth = width; + maxsize = size; + maxdepth = depth; timeout = Unix.gettimeofday() +. 3000.; do_types = false; } in - match auto_main context 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 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 ~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 ~force:false] + @ + 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) = 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 ;;