diff options
Diffstat (limited to 'tactics/eauto.ml4')
-rw-r--r-- | tactics/eauto.ml4 | 94 |
1 files changed, 48 insertions, 46 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 30c5e686..27c3569d 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -125,6 +125,14 @@ let unify_e_resolve poly flags (c,clenv) gls = tclTHEN (Refiner.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) (Proofview.V82.of_tactic (Tactics.Simple.eapply (Vars.subst_univs_level_constr subst c))) gls +let hintmap_of hdc concl = + match hdc with + | None -> fun db -> Hint_db.map_none db + | Some hdc -> + if occur_existential concl then (fun db -> Hint_db.map_existential hdc concl db) + else (fun db -> Hint_db.map_auto hdc concl db) + (* FIXME: should be (Hint_db.map_eauto hdc concl db) *) + let e_exact poly flags (c,clenv) = let clenv', subst = if poly then Clenv.refresh_undefined_univs clenv @@ -145,47 +153,39 @@ let rec e_trivial_fail_db db_list local_db goal = tclFIRST (List.map tclCOMPLETE tacl) goal and e_my_find_search db_list local_db hdc concl = + let hint_of_db = hintmap_of hdc concl in let hintl = - if occur_existential concl then - List.map_append (fun db -> - let flags = auto_flags_of_state (Hint_db.transparent_state db) in - List.map (fun x -> flags, x) (Hint_db.map_existential hdc concl db) - (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)) (local_db::db_list) - else List.map_append (fun db -> let flags = auto_flags_of_state (Hint_db.transparent_state db) in - List.map (fun x -> flags, x) (Hint_db.map_auto hdc concl db)) (local_db::db_list) + List.map (fun x -> flags, x) (hint_of_db db)) (local_db::db_list) in let tac_of_hint = fun (st, {pri = b; pat = p; code = t; poly = poly}) -> (b, - let tac = - match t with - | Res_pf (term,cl) -> Proofview.V82.of_tactic (unify_resolve poly st (term,cl)) - | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl) - | Give_exact (c,cl) -> e_exact poly st (c,cl) - | Res_pf_THEN_trivial_fail (term,cl) -> - tclTHEN (unify_e_resolve poly st (term,cl)) - (e_trivial_fail_db db_list local_db) - | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl - | Extern tacast -> Proofview.V82.of_tactic (conclPattern concl p tacast) + let tac = function + | Res_pf (term,cl) -> unify_resolve poly st (term,cl) + | ERes_pf (term,cl) -> Proofview.V82.tactic (unify_e_resolve poly st (term,cl)) + | Give_exact (c,cl) -> Proofview.V82.tactic (e_exact poly st (c,cl)) + | Res_pf_THEN_trivial_fail (term,cl) -> + Proofview.V82.tactic (tclTHEN (unify_e_resolve poly st (term,cl)) + (e_trivial_fail_db db_list local_db)) + | Unfold_nth c -> Proofview.V82.tactic (reduce (Unfold [AllOccurrences,c]) onConcl) + | Extern tacast -> conclPattern concl p tacast in - (tac,lazy (pr_autotactic t))) + let tac = Proofview.V82.of_tactic (run_auto_tactic t tac) in + (tac, lazy (pr_autotactic t))) in List.map tac_of_hint hintl and e_trivial_resolve db_list local_db gl = - try - priority - (e_my_find_search db_list local_db - (decompose_app_bound gl) gl) - with Bound | Not_found -> [] + let hd = try Some (decompose_app_bound gl) with Bound -> None in + try priority (e_my_find_search db_list local_db hd gl) + with Not_found -> [] let e_possible_resolve db_list local_db gl = - try List.map snd - (e_my_find_search db_list local_db - (decompose_app_bound gl) gl) - with Bound | Not_found -> [] + let hd = try Some (decompose_app_bound gl) with Bound -> None in + 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 = try first_goal gls with UserError _ -> assert false @@ -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; @@ -566,7 +568,7 @@ let autounfold_one db cl = in if did then match cl with - | Some hyp -> change_in_hyp None (fun sigma -> sigma, c') hyp + | Some hyp -> change_in_hyp None (make_change_arg c') hyp | None -> convert_concl_no_check c' DEFAULTcast else Tacticals.New.tclFAIL 0 (str "Nothing to unfold") end |