diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 69 | ||||
| -rw-r--r-- | tactics/auto.mli | 2 | ||||
| -rw-r--r-- | tactics/eauto.ml4 | 67 |
3 files changed, 107 insertions, 31 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 816bd61ca0..2c327b71ba 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -591,11 +591,17 @@ let auto_unif_flags = { (* Try unification with the precompiled clause, then use registered Apply *) +let unify_resolve_nodelta (c,clenv) gls = + let clenv' = connect_clenv gls clenv in + let _ = clenv_unique_resolver false ~flags:auto_unif_flags clenv' gls in + h_simplest_apply c gls + let unify_resolve flags (c,clenv) gls = let clenv' = connect_clenv gls clenv in let _ = clenv_unique_resolver false ~flags clenv' gls in h_apply true false (c,NoBindings) gls + (* builds a hint database from a constr signature *) (* typically used with (lid, ltyp) = pf_hyps_types <some goal> *) @@ -648,33 +654,54 @@ let rec trivial_fail_db mod_delta db_list local_db gl = (List.map tclCOMPLETE (trivial_resolve mod_delta db_list local_db (pf_concl gl)))) gl -and my_find_search mod_delta db_list local_db hdc concl = - let flags = - if mod_delta then {auto_unif_flags with use_metas_eagerly = true} - else auto_unif_flags +and my_find_search_nodelta db_list local_db hdc concl = + let tacl = + if occur_existential concl then + list_map_append + (fun (st, db) -> (Hint_db.map_all hdc db)) + (local_db::db_list) + else + list_map_append (fun (_, db) -> + Hint_db.map_auto (hdc,concl) db) + (local_db::db_list) in + List.map + (fun {pri=b; pat=p; code=t} -> + (b, + match t with + | Res_pf (term,cl) -> unify_resolve_nodelta (term,cl) + | ERes_pf (_,c) -> (fun gl -> error "eres_pf") + | Give_exact c -> exact_check c + | Res_pf_THEN_trivial_fail (term,cl) -> + tclTHEN + (unify_resolve_nodelta (term,cl)) + (trivial_fail_db false db_list local_db) + | Unfold_nth c -> unfold_in_concl [[],c] + | Extern tacast -> + conclPattern concl (Option.get p) tacast)) + tacl + +and my_find_search mod_delta = + if mod_delta then my_find_search_delta + else my_find_search_nodelta + +and my_find_search_delta db_list local_db hdc concl = + let flags = {auto_unif_flags with use_metas_eagerly = true} in let tacl = if occur_existential concl then list_map_append (fun (st, db) -> - let st = - if mod_delta then - {flags with modulo_delta = st} - else flags - in + let st = {flags with modulo_delta = st} in List.map (fun x -> (st,x)) (Hint_db.map_all hdc db)) (local_db::db_list) else list_map_append (fun ((ids, csts as st), db) -> let st, l = - if not mod_delta then - flags, Hint_db.map_auto (hdc,concl) db - else - let l = - if (Idpred.is_empty ids && Cpred.is_empty csts) - then Hint_db.map_auto (hdc,concl) db - else Hint_db.map_all hdc db - in {flags with modulo_delta = st}, l + let l = + if (Idpred.is_empty ids && Cpred.is_empty csts) + then Hint_db.map_auto (hdc,concl) db + else Hint_db.map_all hdc db + in {flags with modulo_delta = st}, l in List.map (fun x -> (st,x)) l) (local_db::db_list) in @@ -682,18 +709,18 @@ and my_find_search mod_delta db_list local_db hdc concl = (fun (st, {pri=b; pat=p; code=t}) -> (b, match t with - | Res_pf (term,cl) -> unify_resolve st (term,cl) + | Res_pf (term,cl) -> unify_resolve st (term,cl) | ERes_pf (_,c) -> (fun gl -> error "eres_pf") | Give_exact c -> exact_check c | Res_pf_THEN_trivial_fail (term,cl) -> tclTHEN (unify_resolve st (term,cl)) - (trivial_fail_db mod_delta db_list local_db) + (trivial_fail_db true db_list local_db) | Unfold_nth c -> unfold_in_concl [[],c] | Extern tacast -> conclPattern concl (Option.get p) tacast)) - tacl - + tacl + and trivial_resolve mod_delta db_list local_db cl = try let hdconstr = List.hd (head_constr_bound cl []) in diff --git a/tactics/auto.mli b/tactics/auto.mli index 7853235be0..5b151162c4 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -141,6 +141,8 @@ val default_search_depth : int ref val auto_unif_flags : Unification.unify_flags (* Try unification with the precompiled clause, then use registered Apply *) +val unify_resolve_nodelta : (constr * clausenv) -> tactic + val unify_resolve : Unification.unify_flags -> (constr * clausenv) -> tactic (* [ConclPattern concl pat tacast]: diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 3894dfd1f7..e6172d3df1 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -91,25 +91,72 @@ open Unification (* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *) (***************************************************************************) +(* no delta yet *) + let unify_e_resolve flags (c,clenv) gls = let clenv' = connect_clenv gls clenv in let _ = clenv_unique_resolver false ~flags clenv' gls in h_simplest_eapply c gls -let rec e_trivial_fail_db db_list local_db goal = +let unify_e_resolve_nodelta (c,clenv) gls = + let clenv' = connect_clenv gls clenv in + let _ = clenv_unique_resolver false clenv' gls in + h_simplest_eapply c gls + +let rec e_trivial_fail_db mod_delta db_list local_db goal = let tacl = registered_e_assumption :: (tclTHEN Tactics.intro (function g'-> let d = pf_last_hyp g' in let hintl = make_resolve_hyp (pf_env g') (project g') d in - (e_trivial_fail_db db_list + (e_trivial_fail_db mod_delta db_list (add_hint_list hintl local_db) g'))) :: - (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) ) + (List.map fst (e_trivial_resolve mod_delta db_list local_db (pf_concl goal)) ) in tclFIRST (List.map tclCOMPLETE tacl) goal -and e_my_find_search db_list local_db hdc concl = +and e_my_find_search mod_delta = + if mod_delta then e_my_find_search_delta + else e_my_find_search_nodelta + +and e_my_find_search_nodelta db_list local_db hdc concl = + let hdc = head_of_constr_reference hdc in + let hintl = + if occur_existential concl then + list_map_append (fun (st, db) -> Hint_db.map_all hdc db) (local_db::db_list) + else + list_map_append (fun (st, db) -> + Hint_db.map_auto (hdc,concl) db) (local_db::db_list) + in + let tac_of_hint = + fun {pri=b; pat = p; code=t} -> + (b, + let tac = + match t with + | Res_pf (term,cl) -> unify_resolve_nodelta (term,cl) + | ERes_pf (term,cl) -> unify_e_resolve_nodelta (term,cl) + | Give_exact (c) -> e_give_exact_constr c + | Res_pf_THEN_trivial_fail (term,cl) -> + tclTHEN (unify_e_resolve_nodelta (term,cl)) + (e_trivial_fail_db false db_list local_db) + | Unfold_nth c -> unfold_in_concl [[],c] + | Extern tacast -> conclPattern concl + (Option.get p) tacast + in + (tac,fmt_autotactic t)) + (*i + fun gls -> pPNL (fmt_autotactic t); Format.print_flush (); + try tac gls + with e when Logic.catchable_exception(e) -> + (Format.print_string "Fail\n"; + Format.print_flush (); + raise e) + i*) + in + List.map tac_of_hint hintl + +and e_my_find_search_delta db_list local_db hdc concl = let hdc = head_of_constr_reference hdc in let hintl = if occur_existential concl then @@ -131,7 +178,7 @@ and e_my_find_search db_list local_db hdc concl = | Give_exact (c) -> e_give_exact_constr c | Res_pf_THEN_trivial_fail (term,cl) -> tclTHEN (unify_e_resolve st (term,cl)) - (e_trivial_fail_db db_list local_db) + (e_trivial_fail_db true db_list local_db) | Unfold_nth c -> unfold_in_concl [[],c] | Extern tacast -> conclPattern concl (Option.get p) tacast @@ -148,16 +195,16 @@ and e_my_find_search db_list local_db hdc concl = in List.map tac_of_hint hintl -and e_trivial_resolve db_list local_db gl = +and e_trivial_resolve mod_delta db_list local_db gl = try Auto.priority - (e_my_find_search db_list local_db + (e_my_find_search mod_delta db_list local_db (List.hd (head_constr_bound gl [])) gl) with Bound | Not_found -> [] -let e_possible_resolve db_list local_db gl = +let e_possible_resolve mod_delta db_list local_db gl = try List.map snd - (e_my_find_search db_list local_db + (e_my_find_search mod_delta db_list local_db (List.hd (head_constr_bound gl [])) gl) with Bound | Not_found -> [] @@ -248,7 +295,7 @@ module SearchProblem = struct in let rec_tacs = let l = - filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g)) + filter_tactics s.tacres (e_possible_resolve false s.dblist (List.hd s.localdb) (pf_concl g)) in List.map (fun ((lgls,_) as res, pp) -> |