diff options
| -rw-r--r-- | tactics/eauto.ml4 | 40 |
1 files changed, 21 insertions, 19 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 3d98bc6e19..1d89286af1 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -184,7 +184,7 @@ and e_trivial_resolve db_list local_db gl = let e_possible_resolve db_list local_db gl = let hd = try Some (decompose_app_bound gl) with Bound -> None in - try List.map snd (e_my_find_search db_list local_db hd gl) + try List.map (fun (b, (tac, pp)) -> (tac, b, pp)) (e_my_find_search db_list local_db hd gl) with Not_found -> [] let find_first_goal gls = @@ -194,6 +194,7 @@ let find_first_goal gls = exploration functor [Explore.Make]. *) type search_state = { + priority : int; depth : int; (*r depth of search before failing *) tacres : goal list sigma; last_tactic : std_ppcmds Lazy.t; @@ -221,12 +222,12 @@ module SearchProblem = struct (* msg (str"Goal:" ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"); *) let rec aux = function | [] -> [] - | (tac,pptac) :: tacl -> + | (tac, cost, pptac) :: tacl -> try let lgls = apply_tac_list tac glls in (* let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *) (* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *) - (lgls,pptac) :: aux tacl + (lgls, cost, pptac) :: aux tacl with e when Errors.noncritical e -> let e = Errors.push e in Refiner.catch_failerror e; aux tacl @@ -236,8 +237,11 @@ module SearchProblem = struct number of remaining goals. *) let compare s s' = let d = s'.depth - s.depth in + let d' = Int.compare s.priority s'.priority in let nbgoals s = List.length (sig_it s.tacres) in - if not (Int.equal d 0) then d else nbgoals s - nbgoals s' + if not (Int.equal d' 0) then d' + else if not (Int.equal d 0) then d + else Int.compare (nbgoals s) (nbgoals s') let branching s = if Int.equal s.depth 0 then @@ -248,42 +252,39 @@ module SearchProblem = struct let nbgl = List.length (sig_it lg) in assert (nbgl > 0); let g = find_first_goal lg in + let map_assum id = (e_give_exact (mkVar id), (-1), lazy (str "exact" ++ spc () ++ pr_id id)) in let assumption_tacs = - let l = - filter_tactics s.tacres - (List.map - (fun id -> (e_give_exact (mkVar id), - lazy (str "exact" ++ spc () ++ pr_id id))) - (pf_ids_of_hyps g)) - in - List.map (fun (res,pp) -> { depth = s.depth; tacres = res; + let tacs = List.map map_assum (pf_ids_of_hyps g) in + let l = filter_tactics s.tacres tacs in + List.map (fun (res, cost, pp) -> { depth = s.depth; priority = cost; tacres = res; last_tactic = pp; dblist = s.dblist; localdb = List.tl s.localdb; prev = ps}) l in let intro_tac = + let l = filter_tactics s.tacres [Proofview.V82.of_tactic Tactics.intro, (-1), lazy (str "intro")] in List.map - (fun (lgls as res,pp) -> + (fun (lgls, cost, pp) -> let g' = first_goal lgls in let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') in let ldb = Hint_db.add_list hintl (List.hd s.localdb) in - { depth = s.depth; tacres = res; + { depth = s.depth; priority = cost; tacres = lgls; last_tactic = pp; dblist = s.dblist; localdb = ldb :: List.tl s.localdb; prev = ps }) - (filter_tactics s.tacres [Proofview.V82.of_tactic Tactics.intro,lazy (str "intro")]) + l in let rec_tacs = let l = filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g)) in List.map - (fun (lgls as res, pp) -> + (fun (lgls, cost, pp) -> let nbgl' = List.length (sig_it lgls) in if nbgl' < nbgl then - { depth = s.depth; tacres = res; last_tactic = pp; prev = ps; - dblist = s.dblist; localdb = List.tl s.localdb } + { depth = s.depth; priority = cost; tacres = lgls; last_tactic = pp; + prev = ps; dblist = s.dblist; localdb = List.tl s.localdb } else let newlocal = let hyps = pf_hyps g in @@ -294,7 +295,7 @@ module SearchProblem = struct else make_local_hint_db (pf_env gls) (project gls) ~ts:full_transparent_state true []) (List.firstn ((nbgl'-nbgl) + 1) (sig_it lgls)) in - { depth = pred s.depth; tacres = res; + { depth = pred s.depth; priority = cost; tacres = lgls; dblist = s.dblist; last_tactic = pp; prev = ps; localdb = newlocal @ List.tl s.localdb }) l @@ -363,6 +364,7 @@ let pr_info dbg s = let make_initial_state dbg n gl dblist localdb = { depth = n; + priority = 0; tacres = tclIDTAC gl; last_tactic = lazy (mt()); dblist = dblist; |