X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=c9f641cb3ae72ef01a32c204311698dbdfa31208;hb=1640e695e405f800547bb1e34cb043e9afa8d10e;hp=70e6ed24e782b5d5d41656dd199567d40a5ebaa4;hpb=4ae46ae1b0353b51bc77b621077fdbcd5f2d075e;p=helm.git diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index 70e6ed24e..c9f641cb3 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -14,8 +14,8 @@ open Printf let debug = ref false let debug_print ?(depth=0) s = if !debug then prerr_endline (String.make depth '\t'^Lazy.force s) else () -(* let print= debug_print *) - let print ?(depth=0) s = +(* let print = debug_print *) +let print ?(depth=0) s = prerr_endline (String.make depth '\t'^Lazy.force s) let debug_do f = if !debug then f () else () @@ -25,37 +25,8 @@ open NTacStatus module Ast = CicNotationPt let app_counter = ref 0 -(* =================================== paramod =========================== *) -let auto_paramod ~params:(l,_) status goal = - let gty = get_goalty status goal in - let n,h,metasenv,subst,o = status#obj in - let status,t = term_of_cic_term status gty (ctx_of gty) in - let status, l = - List.fold_left - (fun (status, l) t -> - 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 - (status, (t,ty) :: l)) - (status,[]) l - in - match - NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l - with - | [] -> raise (Error (lazy "no proof found",None)) - | (pt, metasenv, subst)::_ -> - let status = status#set_obj (n,h,metasenv,subst,o) in - instantiate status goal (mk_cic_term (ctx_of gty) pt) -;; - -let auto_paramod_tac ~params status = - NTactics.distribute_tac (auto_paramod ~params) status -;; - -(*************** subsumption ****************) +(* ======================= utility functions ========================= *) module IntSet = Set.Make(struct type t = int let compare = compare end) -(* exceptions *) let get_sgoalty status g = let _,_,metasenv,subst,_ = status#obj in @@ -82,6 +53,165 @@ let menv_closure status gl = in closure IntSet.empty gl ;; +(* we call a "fact" an object whose hypothesis occur in the goal + or in types of goal-variables *) +let is_a_fact status ty = + let status, ty, _ = saturate ~delta:0 status ty in + debug_print (lazy (ppterm status ty)); + let g_metas = metas_of_term status ty in + let clos = menv_closure status g_metas in + let _,_,metasenv,_,_ = status#obj in + let menv = + List.fold_left + (fun acc (i,_) -> IntSet.add i acc) + IntSet.empty metasenv + in IntSet.equal clos menv;; + +let is_a_fact_obj s uri = + let obj = NCicEnvironment.get_checked_obj uri in + match obj with + | (_,_,[],[],NCic.Constant(_,_,Some(t),ty,_)) -> + is_a_fact s (mk_cic_term [] ty) +(* aggiungere i costruttori *) + | _ -> false + +let current_goal status = + let open_goals = head_goals status#stack in + assert (List.length open_goals = 1); + let open_goal = List.hd open_goals in + let gty = get_goalty status open_goal in + let ctx = ctx_of gty in + open_goal, ctx, gty + + +(* =============================== paramod =========================== *) +let solve fast status eq_cache goal = + let f = + if fast then NCicParamod.fast_eq_check + else NCicParamod.paramod in + let n,h,metasenv,subst,o = status#obj in + let gname, ctx, gty = List.assoc goal metasenv in + let gty = NCicUntrusted.apply_subst subst ctx gty in + let build_status (pt, _, metasenv, subst) = + try + debug_print (lazy ("refining: "^(NCicPp.ppterm ctx subst metasenv pt))); + let stamp = Unix.gettimeofday () in + let metasenv, subst, pt, pty = + NCicRefiner.typeof status + (* (status#set_coerc_db NCicCoercion.empty_db) *) + metasenv subst ctx pt None in + debug_print (lazy ("refined: "^(NCicPp.ppterm ctx subst metasenv pt))); + debug_print (lazy ("synt: "^(NCicPp.ppterm ctx subst metasenv pty))); + let metasenv, subst = + NCicUnification.unify status metasenv subst ctx gty pty + (* the previous code is much less expensive than directly refining + pt with expected type pty + in + prerr_endline ("exp: "^(NCicPp.ppterm ctx subst metasenv gty)); + NCicRefiner.typeof + (status#set_coerc_db NCicCoercion.empty_db) + metasenv subst ctx pt (Some gty) *) + in + print (lazy (Printf.sprintf "Refined in %fs" + (Unix.gettimeofday() -. stamp))); + let status = status#set_obj (n,h,metasenv,subst,o) in + let metasenv = List.filter (fun j,_ -> j <> goal) metasenv in + let subst = (goal,(gname,ctx,pt,pty)) :: subst in + Some (status#set_obj (n,h,metasenv,subst,o)) + with + NCicRefiner.RefineFailure msg + | NCicRefiner.Uncertain msg -> + debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^ + snd (Lazy.force msg))); None + | NCicRefiner.AssertFailure msg -> + debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^ + Lazy.force msg)); None + | _ -> None + in + HExtlib.filter_map build_status + (f status metasenv subst ctx eq_cache (NCic.Rel ~-1,gty)) +;; + +let fast_eq_check eq_cache status goal = + match solve true status eq_cache goal with + | [] -> raise (Error (lazy "no proof found",None)) + | s::_ -> s +;; + +let dist_fast_eq_check eq_cache s = + NTactics.distribute_tac (fast_eq_check eq_cache) s +;; + +let auto_eq_check eq_cache status = + try + let s = dist_fast_eq_check eq_cache status in + [s] + with + | Error _ -> [] +;; + +(* warning: ctx is supposed to be already instantiated w.r.t subst *) +let index_local_equations eq_cache status = + let open_goals = head_goals status#stack in + let open_goal = List.hd open_goals in + let ngty = get_goalty status open_goal in + let ctx = ctx_of ngty in + let c = ref 0 in + List.fold_left + (fun eq_cache _ -> + c:= !c+1; + let t = NCic.Rel !c in + try + let ty = NCicTypeChecker.typeof [] [] ctx t in + debug_print(lazy("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty))); + NCicParamod.forward_infer_step eq_cache t ty + with + | NCicTypeChecker.TypeCheckerFailure _ + | NCicTypeChecker.AssertFailure _ -> eq_cache) + eq_cache ctx +;; + +let fast_eq_check_tac ~params s = + let unit_eq = index_local_equations s#eq_cache s in + dist_fast_eq_check unit_eq s +;; + +let paramod eq_cache status goal = + match solve false status eq_cache goal with + | [] -> raise (Error (lazy "no proof found",None)) + | s::_ -> s +;; + +let paramod_tac ~params s = + let unit_eq = index_local_equations s#eq_cache s in + NTactics.distribute_tac (paramod unit_eq) s +;; + +(* +let fast_eq_check_tac_all ~params eq_cache status = + let g,_,_ = current_goal status in + let allstates = fast_eq_check_all status eq_cache g in + let pseudo_low_tac s _ _ = s in + let pseudo_low_tactics = + List.map pseudo_low_tac allstates + in + List.map (fun f -> NTactics.distribute_tac f status) pseudo_low_tactics +;; +*) + +(* +let demod status eq_cache goal = + let n,h,metasenv,subst,o = status#obj in + let gname, ctx, gty = List.assoc goal metasenv in + let gty = NCicUntrusted.apply_subst subst ctx gty in + +let demod_tac ~params s = + let unit_eq = index_local_equations s#eq_cache s in + dist_fast_eq_check unit_eq s +*) + +(*************** subsumption ****************) + let close_wrt_context = List.fold_left (fun ty ctx_entry -> @@ -223,16 +353,16 @@ let close status g = let elems = IntSet.elements subset in let _, ctx, ty = NCicUtils.lookup_meta g metasenv in let ty = NCicUntrusted.apply_subst subst ctx ty in - print (lazy ("Elements for " ^ (NCicPp.ppterm ctx [] metasenv ty))); - print (lazy (String.concat ", " (List.map string_of_int elems))); + debug_print (lazy ("metas in " ^ (NCicPp.ppterm ctx [] metasenv ty))); + debug_print (lazy (String.concat ", " (List.map string_of_int elems))); let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in let submenv = List.rev (NCicUntrusted.sort_metasenv subst submenv) in (* let submenv = metasenv in *) let ty = close_wrt_metasenv subst ty submenv in - print (lazy (NCicPp.ppterm ctx [] [] ty)); - ty + debug_print (lazy (NCicPp.ppterm ctx [] [] ty)); + ctx,ty ;; @@ -1101,7 +1231,50 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goa ;; *) +(****************** smart application ********************) + + +let smart_apply t unit_eq status g = + let n,h,metasenv,subst,o = status#obj in + let gname, ctx, gty = List.assoc g metasenv in + (* let ggty = mk_cic_term context gty in *) + let status, t = disambiguate status ctx t None in + let status,t = term_of_cic_term status t ctx in + let ty = NCicTypeChecker.typeof subst metasenv ctx t in + let ty,metasenv,args = NCicMetaSubst.saturate metasenv subst ctx ty 0 in + let metasenv,j,inst,_ = NCicMetaSubst.mk_meta metasenv ctx `IsTerm in + let status = status#set_obj (n,h,metasenv,subst,o) in + let pterm = if args=[] then t else NCic.Appl(t::args) in + let eq_coerc = + let uri = + NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq_coerc.con" in + let ref = NReference.reference_of_spec uri (NReference.Def(2)) in + NCic.Const ref + in + let smart = + NCic.Appl[eq_coerc;ty;NCic.Implicit `Type;pterm;inst] in + let smart = mk_cic_term ctx smart in + try + let status = instantiate status g smart in + let _,_,metasenv,subst,_ = status#obj in + let _,ctx,jty = List.assoc j metasenv in + let jty = NCicUntrusted.apply_subst subst ctx jty in + debug_print(lazy("goal " ^ (NCicPp.ppterm ctx [] [] jty))); + fast_eq_check unit_eq status j + with + | Error _ as e -> debug_print (lazy "error"); raise e + +let smart_apply_tac t s = + let unit_eq = index_local_equations s#eq_cache s in + NTactics.distribute_tac (smart_apply t unit_eq) s + +let smart_apply_auto t eq_cache = + NTactics.distribute_tac (smart_apply t eq_cache) + + (****************** types **************) + + type th_cache = (NCic.context * InvRelDiscriminationTree.t) list let keys_of_term status t = @@ -1180,11 +1353,10 @@ let pp_th status = 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 + | [] -> (* Ncic_termSet.elements *) acc | (_::tl) as k -> try let idx = List.assq k th in @@ -1199,12 +1371,19 @@ let search_in_th gty th = type flags = { do_types : bool; (* solve goals in Type *) + last : bool; (* last goal: take first solution only *) maxwidth : int; maxsize : int; maxdepth : int; timeout : float; } +type cache = + {facts : th_cache; (* positive results *) + under_inspection : th_cache; (* to prune looping *) + unit_eq : NCicParamod.state + } + type sort = T | P type goal = int * sort (* goal, depth, sort *) type fail = goal * cic_term @@ -1212,114 +1391,185 @@ type candidate = int * Ast.term (* unique candidate number, candidate *) exception Gaveup of IntSet.t (* a sublist of unprovable conjunctive atoms of the input goals *) -exception Proved of #NTacStatus.tac_status +exception Proved of NTacStatus.tac_status -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 cache_add_underinspection c _ _ = c;; -let equational_case _ _ _ _ _ _ = [];; -let only _ _ _ = true;; +(* 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 cache_add_underinspection c _ _ = c;; *) + +let init_cache ?(facts=[]) ?(under_inspection=[]) + ?(unit_eq=NCicParamod.empty_state) _ = + {facts = facts; + under_inspection = under_inspection; + unit_eq = unit_eq + } + +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 -;; +let openg_no status = List.length (head_goals status#stack) + +let sort_new_elems l = + List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l -let try_candidate flags depth status t g = +let try_candidate ?(smart=0) flags depth status eq_cache t = try - 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 ~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) + print ~depth (lazy ("------------ try " ^ CicNotationPp.pp_term t)); + let status = + if smart= 0 then NTactics.apply_tac ("",0,t) status + else if smart = 1 then smart_apply_auto ("",0,t) eq_cache status + else (* smart = 2: both *) + try NTactics.apply_tac ("",0,t) status + with Error _ -> + smart_apply_auto ("",0,t) eq_cache status in + let og_no = openg_no status in + if (* og_no > flags.maxwidth || *) + ((depth + 1) = flags.maxdepth && og_no <> 0) then + (print ~depth (lazy "pruned immediately"); None) else (incr candidate_no; - Some ((!candidate_no,t),status,open_goals)) + Some ((!candidate_no,t),status)) with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None ;; -let get_candidates status cache_th signature gty = +let get_candidates ?(smart=true) status cache signature gty = let universe = status#auto_cache in let context = ctx_of gty in + let t_ast t = + let _status, t = term_of_cic_term status t context + in Ast.NCic t in + let c_ast = function + | NCic.Const r -> Ast.NRef r | _ -> assert false in let _, raw_gty = term_of_cic_term status gty context in - let cands = - NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe raw_gty - in - let cands = - List.filter (only signature context) - (NDiscriminationTree.TermSet.elements cands) + let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables + universe raw_gty in + let local_cands = search_in_th gty cache in + let together global local = + List.map c_ast + (List.filter (only signature context) + (NDiscriminationTree.TermSet.elements global)) @ + List.map t_ast (Ncic_termSet.elements local) in + let candidates = together cands local_cands in + let smart_candidates = + if smart then + match raw_gty with + | NCic.Appl (hd::tl) -> + let weak_gty = + NCic.Appl (hd:: HExtlib.mk_list(NCic.Meta (0,(0,NCic.Irl 0))) + (List.length tl)) in + let more_cands = + NDiscriminationTree.DiscriminationTree.retrieve_unifiables + universe weak_gty in + let smart_cands = + NDiscriminationTree.TermSet.diff more_cands cands in + let cic_weak_gty = mk_cic_term context weak_gty in + let more_local_cands = search_in_th cic_weak_gty cache in + let smart_local_cands = + Ncic_termSet.diff more_local_cands local_cands in + together smart_cands smart_local_cands + | _ -> [] + else [] in - 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 + candidates, smart_candidates ;; -let applicative_case depth signature status flags g gty cache = +let applicative_case depth signature status flags gty (cache:cache) = app_counter:= !app_counter+1; - let candidates = get_candidates status cache signature gty in + let _,_,metasenv,subst,_ = status#obj in + let context = ctx_of gty in + let tcache = cache.facts in + let is_eq = + let status, t = term_of_cic_term status gty context in + NCicParamod.is_equation metasenv subst context t + in + debug_print(lazy (string_of_bool is_eq)); + let candidates, smart_candidates = + get_candidates ~smart:(not is_eq) status tcache signature gty in debug_print ~depth (lazy ("candidates: " ^ string_of_int (List.length candidates))); - let elems = + debug_print ~depth + (lazy ("smart candidates: " ^ + string_of_int (List.length smart_candidates))); +(* + let sm = 0 in + let smart_candidates = [] in *) + let sm = if is_eq then 0 else 2 in + let only_one = flags.last && (depth + 1 = flags.maxdepth) in + print (lazy ("only_one: " ^ (string_of_bool only_one))); + let elems = List.fold_left (fun elems cand -> - match try_candidate flags depth status cand g with - | None -> elems - | Some x -> x::elems) + if (only_one && (elems <> [])) then elems + else + match try_candidate (~smart:sm) + flags depth status cache.unit_eq cand with + | None -> elems + | Some x -> x::elems) [] candidates in - elems + let more_elems = + if only_one && elems <> [] then elems + else + List.fold_left + (fun elems cand -> + if (only_one && (elems <> [])) then elems + else + match try_candidate (~smart:1) + flags depth status cache.unit_eq cand with + | None -> elems + | Some x -> x::elems) + [] smart_candidates + in + elems@more_elems ;; -let equational_and_applicative_case - 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 - in - let more_elems = - applicative_case depth - signature status flags g gty cache - in - elems@more_elems - else - let elems = - (*match LibraryObjects.eq_URI () with - | Some _ -> - smart_applicative_case dbd tables depth s fake_proof goalno - gty m context signature universe cache flags - | None -> *) - applicative_case depth - signature status flags g gty cache - in - elems - in - let elems = - List.map (fun c,s,gl -> - c,1,1,s,List.map (fun i -> - let sort = - let gty = get_goalty s i in - 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 - in - i,sort) gl) elems - in - let elems = sort_new_elems elems in - elems, cache +exception Found +;; + +(* gty is supposed to be meta-closed *) +let is_subsumed depth status gty cache = + if cache=[] then false else ( + debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty))); + let n,h,metasenv,subst,obj = status#obj in + let ctx = ctx_of gty in + let _ , target = term_of_cic_term status gty ctx in + let target = NCicSubstitution.lift 1 target in + (* candidates must only be searched w.r.t the given context *) + let candidates = + try + let idx = List.assq ctx cache in + Ncic_termSet.elements + (InvRelDiscriminationTree.retrieve_generalizations idx gty) + with Not_found -> [] + in + debug_print ~depth + (lazy ("failure candidates: " ^ string_of_int (List.length candidates))); + try + List.iter + (fun t -> + let _ , source = term_of_cic_term status t ctx in + let implication = + NCic.Prod("foo",source,target) in + let metasenv,j,_,_ = + NCicMetaSubst.mk_meta + metasenv ctx ~with_type:implication `IsType in + let status = status#set_obj (n,h,metasenv,subst,obj) in + let status = status#set_stack [([1,Open j],[],[],`NoTag)] in + try + let status = NTactics.intro_tac "foo" status in + let status = + NTactics.apply_tac ("",0,Ast.NCic (NCic.Rel 1)) status + in + if (head_goals status#stack = []) then raise Found + else () + with + | Error _ -> ()) + candidates;false + with Found -> debug_print ~depth (lazy "success");true) ;; let rec guess_name name ctx = @@ -1328,22 +1578,81 @@ let rec guess_name name ctx = 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 compute the sort *) - [(!candidate_no,Ast.Implicit `JustOne),0,0,status,[open_goal,P]], - cache +let is_prod status = + let _, ctx, gty = current_goal status in + let _, raw_gty = term_of_cic_term status gty ctx in + match raw_gty with + | NCic.Prod (name,_,_) -> Some (guess_name name ctx) + | _ -> None + +let intro ~depth status facts name = + let status = NTactics.intro_tac name status in + let _, ctx, ngty = current_goal status in + let t = mk_cic_term ctx (NCic.Rel 1) in + let status, keys = keys_of_term status t in + let facts = List.fold_left (add_to_th t) facts keys in + debug_print ~depth (lazy ("intro: "^ name)); + (* unprovability is not stable w.r.t introduction *) + status, facts +;; + +let rec intros_facts ~depth status facts = + match is_prod status with + | Some(name) -> + let status,facts = + intro ~depth status facts name + in intros_facts ~depth status facts + | _ -> status, facts +;; + +let rec intros ~depth status (cache:cache) = + match is_prod status with + | Some _ -> + let status,facts = + intros_facts ~depth status cache.facts + in + (* we reindex the equation from scratch *) + let unit_eq = + index_local_equations status#eq_cache status in + (* under_inspection must be set to empty *) + status, init_cache ~facts ~unit_eq () + | _ -> status, cache +;; + +let reduce ~depth status g = + let n,h,metasenv,subst,o = status#obj in + let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in + let ty = NCicUntrusted.apply_subst subst ctx ty in + let ty' = NCicReduction.whd ~subst ctx ty in + if ty = ty' then [] + else + (debug_print ~depth + (lazy ("reduced to: "^ NCicPp.ppterm ctx subst metasenv ty')); + let metasenv = + (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv) + in + let status = status#set_obj (n,h,metasenv,subst,o) in + incr candidate_no; + [(!candidate_no,Ast.Ident("__whd",None)),status]) +;; + +let do_something signature flags status g depth gty cache = + (* whd *) + let l = reduce ~depth status g in + (* backward aplications *) + let l1 = + List.map + (fun s -> + incr candidate_no; + ((!candidate_no,Ast.Ident("__paramod",None)),s)) + (auto_eq_check cache.unit_eq status) in + let l2 = + if (l1 <> []) then [] + else applicative_case depth signature status flags gty cache + (* fast paramodulation *) + in + (* states in l1 have have an empty set of subgoals: no point to sort them *) + l1 @ (sort_new_elems (l@l2)), cache ;; let pp_goal = function @@ -1360,14 +1669,6 @@ let pp_goals status l = l) ;; -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 M = struct type t = int @@ -1434,9 +1735,10 @@ let focus_tac focus status = status#set_stack gstatus ;; -let rec auto_clusters +let rec auto_clusters ?(top=false) flags signature cache depth status : unit = debug_print ~depth (lazy "entering auto clusters"); + print (lazy ("auto cluster: " ^ (string_of_bool flags.last))); (* ignore(Unix.select [] [] [] 0.01); *) let status = clean_up_tac status in let goals = head_goals status#stack in @@ -1445,9 +1747,10 @@ let rec auto_clusters else if List.length goals < 2 then auto_main flags signature cache depth status else - debug_print ~depth (lazy ("goals = " ^ + print ~depth (lazy ("goals = " ^ String.concat "," (List.map string_of_int goals))); let classes = HExtlib.clusters (deps status) goals in + let classes = if top then List.rev classes else classes in debug_print ~depth (lazy (String.concat "\n" @@ -1455,73 +1758,99 @@ let rec auto_clusters (fun l -> ("cluster:" ^ String.concat "," (List.map string_of_int l))) classes))); - let status = + let status,b = List.fold_left - (fun status gl -> + (fun (status,b) gl -> let status = focus_tac gl status in try debug_print ~depth (lazy ("focusing on" ^ String.concat "," (List.map string_of_int gl))); - auto_main flags signature cache depth status; status - with Proved(status) -> NTactics.merge_tac status) - status classes - in raise (Proved status) + auto_main flags signature cache depth status; assert false + with + | Proved(status) -> (NTactics.merge_tac status,true) + | Gaveup _ when top -> (NTactics.merge_tac status,b) + ) + (status,false) classes + in if b then raise (Proved status) else raise (Gaveup IntSet.empty) and -(* The pair solved,init_status is used for chaching purposes. - solved is the list of goals in init_status already proved. - Initially, init_status=status and k is set to [] *) -(* let rec auto_main flags signature cache status k depth = *) +(* the goals returned upon failure are an unsatisfiable subset + of the initial head goals in the stack *) -auto_main flags signature cache depth status: unit = +auto_main flags signature (cache:cache) depth status: unit = + print (lazy ("auto enter: " ^ (string_of_bool flags.last))); debug_print ~depth (lazy "entering auto main"); (* ignore(Unix.select [] [] [] 0.01); *) let status = sort_tac (clean_up_tac status) in let goals = head_goals status#stack in match goals with | [] -> raise (Proved status) - | g::tlg -> - if depth = flags.maxdepth then raise (Gaveup IntSet.empty) - else - let status = - if tlg=[] then status - else NTactics.branch_tac status in - let gty = get_goalty status g in - let status, gty = apply_subst status (ctx_of gty) gty in - debug_print ~depth (lazy("Depth = " ^ (string_of_int depth))); - debug_print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty)); - close status g; - (* let closed = metas_of_term status gty = [] in *) + | orig::_ -> + let ng = List.length goals in + if ng > flags.maxwidth then + (print (lazy "FAIL WIDTH"); raise (Gaveup IntSet.empty)) + else let branch = ng>1 in + if depth = flags.maxdepth then raise (Gaveup IntSet.empty) + else + let status = + if branch then NTactics.branch_tac status + else status in + let status, cache = intros ~depth status cache in + let g,gctx, gty = current_goal status in + let ctx,ty = close status g in + let closegty = mk_cic_term ctx ty in + let status, gty = apply_subst status gctx gty in + debug_print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty)); + if is_subsumed depth status closegty cache.under_inspection then + (debug_print (lazy "SUBSUMED"); + raise (Gaveup IntSet.add g IntSet.empty)) + else + let do_flags = + {flags with last = flags.last && (not branch)} in let alternatives, cache = - do_something signature flags status g depth gty cache in + do_something signature do_flags status g depth gty cache in + let loop_cache = + let under_inspection = + add_to_th closegty cache.under_inspection closegty in + {cache with under_inspection = under_inspection} in let unsat = List.fold_left (* the underscore information does not need to be returned by do_something *) - (fun unsat ((_,t),_,_,status,_) -> - let depth' = - if t=(Ast.Implicit `JustOne) then depth else depth+1 in + (fun unsat ((_,t),status) -> + let depth',looping_cache = + if t=Ast.Ident("__whd",None) then depth,cache + else depth+1, loop_cache in debug_print (~depth:depth') - (lazy ("Case: " ^ CicNotationPp.pp_term t)); - try auto_clusters flags signature cache + (lazy ("Case: " ^ CicNotationPp.pp_term t)); + let flags' = + {flags with maxwidth = flags.maxwidth - ng +1} in + (* sistemare *) + let flags' = + {flags' with last = flags'.last && (not branch)} in + print (lazy ("auto last: " ^ (string_of_bool flags'.last))); + try auto_clusters flags' signature loop_cache depth' status; unsat with | Proved status -> debug_print (~depth:depth') (lazy "proved"); - if tlg=[] then raise (Proved status) - else + if branch then let status = NTactics.merge_tac status - in - (try auto_clusters flags signature cache - depth status; unsat - with Gaveup f -> - debug_print ~depth - (lazy ("Unsat1 at depth " ^ (string_of_int depth) + in + (* old cache, here *) + let flags = + {flags with maxwidth = flags.maxwidth - 1} in + try auto_clusters flags signature cache + depth status; assert false + with Gaveup f -> + debug_print ~depth + (lazy ("Unsat1 at depth " ^ (string_of_int depth) ^ ": " ^ (pp_goals status (IntSet.elements f)))); (* TODO: cache failures *) - IntSet.union f unsat) + IntSet.union f unsat + else raise (Proved status) | Gaveup f -> debug_print (~depth:depth') (lazy ("Unsat2 at depth " ^ (string_of_int depth') @@ -1531,7 +1860,7 @@ auto_main flags signature cache depth status: unit = unsat) IntSet.empty alternatives in - raise (Gaveup IntSet.add g unsat) + raise (Gaveup IntSet.add orig unsat) ;; let int name l def = @@ -1540,9 +1869,13 @@ let int name l def = ;; let auto_tac ~params:(_univ,flags) status = + let oldstatus = status in + let status = (status:> NTacStatus.tac_status) in let goals = head_goals status#stack in - let status, cache = mk_th_cache status goals in -(* pp_th status cache; *) + let status, facts = mk_th_cache status goals in + let unit_eq = index_local_equations status#eq_cache status in + let cache = init_cache ~facts ~unit_eq () in +(* pp_th status facts; *) (* NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t -> debug_print (lazy( @@ -1554,11 +1887,12 @@ let auto_tac ~params:(_univ,flags) status = *) let depth = int "depth" flags 3 in let size = int "size" flags 10 in - let width = int "width" flags (3+List.length goals) in + let width = int "width" flags 4 (* (3+List.length goals)*) in (* XXX fix sort *) let goals = List.map (fun i -> (i,P)) goals in let signature = () in let flags = { + last = true; maxwidth = width; maxsize = size; maxdepth = depth; @@ -1568,27 +1902,33 @@ let auto_tac ~params:(_univ,flags) status = let initial_time = Unix.gettimeofday() in app_counter:= 0; let rec up_to x y = - if x > y then raise (Error (lazy "auto gave up", None)) + if x > y then + (print(lazy + ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time))); + print(lazy + ("Applicative nodes:"^string_of_int !app_counter)); + 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 - try auto_clusters flags signature cache 0 status;status + try auto_clusters (~top:true) flags signature cache 0 status;assert false with | Gaveup _ -> up_to (x+1) y | Proved s -> - HLog.debug ("proved at depth " ^ string_of_int x); + print (lazy ("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 + let s = s#set_stack stack in + oldstatus#set_status s in let s = up_to depth depth in - debug_print(lazy + print(lazy ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time))); - debug_print(lazy + print(lazy ("Applicative nodes:"^string_of_int !app_counter)); s ;;