aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/eauto.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/eauto.ml4')
-rw-r--r--tactics/eauto.ml475
1 files changed, 42 insertions, 33 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 20a7448dc..2241fb821 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -28,33 +28,41 @@ open Misctypes
open Locus
open Locusops
open Hints
+open Proofview.Notations
DECLARE PLUGIN "eauto"
let eauto_unif_flags = auto_flags_of_state full_transparent_state
-let e_give_exact ?(flags=eauto_unif_flags) c gl =
- let t1 = (pf_unsafe_type_of gl c) and t2 = pf_concl gl in
+let e_give_exact ?(flags=eauto_unif_flags) c =
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
+ let t1 = Tacmach.New.pf_unsafe_type_of gl c in
+ let t2 = Tacmach.New.pf_concl gl in
if occur_existential t1 || occur_existential t2 then
- tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl
- else Proofview.V82.of_tactic (exact_check c) gl
+ Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (Proofview.V82.tactic (exact_no_check c))
+ else exact_check c
+ end }
let assumption id = e_give_exact (mkVar id)
-let e_assumption gl =
- tclFIRST (List.map assumption (pf_ids_of_hyps gl)) gl
+let e_assumption =
+ Proofview.Goal.enter { enter = begin fun gl ->
+ Tacticals.New.tclFIRST (List.map assumption (Tacmach.New.pf_ids_of_hyps gl))
+ end }
TACTIC EXTEND eassumption
-| [ "eassumption" ] -> [ Proofview.V82.tactic e_assumption ]
+| [ "eassumption" ] -> [ e_assumption ]
END
TACTIC EXTEND eexact
-| [ "eexact" constr(c) ] -> [ Proofview.V82.tactic (e_give_exact c) ]
+| [ "eexact" constr(c) ] -> [ e_give_exact c ]
END
-let registered_e_assumption gl =
- tclFIRST (List.map (fun id gl -> e_give_exact (mkVar id) gl)
- (pf_ids_of_hyps gl)) gl
+let registered_e_assumption =
+ Proofview.Goal.enter { enter = begin fun gl ->
+ Tacticals.New.tclFIRST (List.map (fun id -> e_give_exact (mkVar id))
+ (Tacmach.New.pf_ids_of_hyps gl))
+ end }
(************************************************************************)
(* PROLOG tactic *)
@@ -83,7 +91,7 @@ let one_step l gl =
[Proofview.V82.of_tactic Tactics.intro]
@ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) (List.map mkVar (pf_ids_of_hyps gl)))
@ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) l)
- @ (List.map assumption (pf_ids_of_hyps gl))
+ @ (List.map (fun c -> Proofview.V82.of_tactic (assumption c)) (pf_ids_of_hyps gl))
let rec prolog l n gl =
if n <= 0 then error "prolog - failure";
@@ -119,15 +127,14 @@ open Unification
let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l)
let unify_e_resolve poly flags (c,clenv) =
- Proofview.Goal.nf_enter begin
- fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let clenv', c = connect_hint_clenv poly c clenv gl in
Proofview.V82.tactic
(fun gls ->
let clenv' = clenv_unique_resolver ~flags clenv' gls in
tclTHEN (Refiner.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
(Proofview.V82.of_tactic (Tactics.Simple.eapply c)) gls)
- end
+ end }
let hintmap_of hdc concl =
match hdc with
@@ -143,19 +150,21 @@ let e_exact poly flags (c,clenv) =
if poly then Clenv.refresh_undefined_univs clenv
else clenv, Univ.empty_level_subst
in e_give_exact (* ~flags *) (Vars.subst_univs_level_constr subst c)
-
-let rec e_trivial_fail_db db_list local_db goal =
+
+let rec e_trivial_fail_db db_list local_db =
+ let next = Proofview.Goal.nf_enter { enter = begin fun gl ->
+ let d = Tacmach.New.pf_last_hyp gl in
+ let hintl = make_resolve_hyp (Tacmach.New.pf_env gl) (Tacmach.New.project gl) d in
+ e_trivial_fail_db db_list (Hint_db.add_list (Tacmach.New.pf_env gl) (Tacmach.New.project gl) hintl local_db)
+ end } in
+ Proofview.Goal.enter { enter = begin fun gl ->
let tacl =
registered_e_assumption ::
- (tclTHEN (Proofview.V82.of_tactic 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
- (Hint_db.add_list (pf_env g') (project g') hintl local_db) g'))) ::
- (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) )
+ (Tacticals.New.tclTHEN Tactics.intro next) ::
+ (List.map fst (e_trivial_resolve db_list local_db (Tacmach.New.pf_nf_concl gl)))
in
- tclFIRST (List.map tclCOMPLETE tacl) goal
+ Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl)
+ end }
and e_my_find_search db_list local_db hdc concl =
let hint_of_db = hintmap_of hdc concl in
@@ -174,14 +183,14 @@ and e_my_find_search db_list local_db hdc concl =
let tac = function
| Res_pf (term,cl) -> unify_resolve poly st (term,cl)
| ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl)
- | Give_exact (c,cl) -> Proofview.V82.tactic (e_exact poly st (c,cl))
+ | Give_exact (c,cl) -> e_exact poly st (c,cl)
| Res_pf_THEN_trivial_fail (term,cl) ->
- Proofview.V82.tactic (tclTHEN (Proofview.V82.of_tactic (unify_e_resolve poly st (term,cl)))
- (e_trivial_fail_db db_list local_db))
+ Tacticals.New.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
- let tac = Proofview.V82.of_tactic (run_hint t tac) in
+ let tac = run_hint t tac in
(tac, lazy (pr_hint t)))
in
List.map tac_of_hint hintl
@@ -234,7 +243,7 @@ module SearchProblem = struct
| [] -> []
| (tac, cost, pptac) :: tacl ->
try
- let lgls = apply_tac_list tac glls in
+ let lgls = apply_tac_list (Proofview.V82.of_tactic 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, cost, pptac) :: aux tacl
@@ -272,7 +281,7 @@ module SearchProblem = struct
prev = ps; local_lemmas = s.local_lemmas}) l
in
let intro_tac =
- let l = filter_tactics s.tacres [Proofview.V82.of_tactic Tactics.intro, (-1), lazy (str "intro")] in
+ let l = filter_tactics s.tacres [Tactics.intro, (-1), lazy (str "intro")] in
List.map
(fun (lgls, cost, pp) ->
let g' = first_goal lgls in
@@ -567,7 +576,7 @@ let unfold_head env (ids, csts) c =
in aux c
let autounfold_one db cl =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let concl = Proofview.Goal.concl gl in
let st =
@@ -586,7 +595,7 @@ let autounfold_one db cl =
| 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
+ end }
(* Cset.fold (fun cst -> cons (all_occurrences, EvalConstRef cst)) csts *)
(* (Id.Set.fold (fun id -> cons (all_occurrences, EvalVarRef id)) ids [])) db) *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 18:45:47 +0000