summaryrefslogtreecommitdiff
path: root/tactics/eauto.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/eauto.ml')
-rw-r--r--tactics/eauto.ml155
1 files changed, 79 insertions, 76 deletions
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 23ff5822..dc310c54 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -1,26 +1,29 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Pp
open CErrors
open Util
open Names
-open Nameops
open Term
open Termops
+open EConstr
open Proof_type
open Tacticals
open Tacmach
+open Evd
open Tactics
open Clenv
open Auto
open Genredexpr
-open Tacexpr
+open Tactypes
open Locus
open Locusops
open Hints
@@ -29,26 +32,27 @@ open Proofview.Notations
let eauto_unif_flags = auto_flags_of_state full_transparent_state
let e_give_exact ?(flags=eauto_unif_flags) c =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let t1 = Tacmach.New.pf_unsafe_type_of gl c in
- let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
- if occur_existential t1 || occur_existential t2 then
+ let t2 = Tacmach.New.pf_concl gl in
+ let sigma = Tacmach.New.project gl in
+ if occur_existential sigma t1 || occur_existential sigma t2 then
Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c)
else exact_check c
- end }
+ end
let assumption id = e_give_exact (mkVar id)
let e_assumption =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
Tacticals.New.tclFIRST (List.map assumption (Tacmach.New.pf_ids_of_hyps gl))
- end }
+ end
let registered_e_assumption =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
Tacticals.New.tclFIRST (List.map (fun id -> e_give_exact (mkVar id))
(Tacmach.New.pf_ids_of_hyps gl))
- end }
+ end
(************************************************************************)
(* PROLOG tactic *)
@@ -60,7 +64,7 @@ let registered_e_assumption =
let first_goal gls =
let gl = gls.Evd.it and sig_0 = gls.Evd.sigma in
- if List.is_empty gl then error "first_goal";
+ if List.is_empty gl then user_err Pp.(str "first_goal");
{ Evd.it = List.hd gl; Evd.sigma = sig_0; }
(* tactic -> tactic_list : Apply a tactic to the first goal in the list *)
@@ -71,7 +75,7 @@ let apply_tac_list tac glls =
| (g1::rest) ->
let gl = apply_sig_tac sigr tac g1 in
repackage sigr (gl@rest)
- | _ -> error "apply_tac_list"
+ | _ -> user_err Pp.(str "apply_tac_list")
let one_step l gl =
[Proofview.V82.of_tactic Tactics.intro]
@@ -80,25 +84,25 @@ let one_step l 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";
+ if n <= 0 then user_err Pp.(str "prolog - failure");
let prol = (prolog l (n-1)) in
(tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl
-let out_term = function
+let out_term env = function
| IsConstr (c, _) -> c
- | IsGlobRef gr -> fst (Universes.fresh_global_instance (Global.env ()) gr)
+ | IsGlobRef gr -> EConstr.of_constr (fst (Universes.fresh_global_instance env gr))
let prolog_tac l n =
Proofview.V82.tactic begin fun gl ->
let map c =
- let (c, sigma) = Tactics.run_delayed (pf_env gl) (project gl) c in
+ let (sigma, c) = c (pf_env gl) (project gl) in
let c = pf_apply (prepare_hint false (false,true)) gl (sigma, c) in
- out_term c
+ out_term (pf_env gl) c
in
let l = List.map map l in
try (prolog l n gl)
- with UserError ("Refiner.tclFIRST",_) ->
- errorlabstrm "Prolog.prolog" (str "Prolog failed.")
+ with UserError (Some "Refiner.tclFIRST",_) ->
+ user_err ~hdr:"Prolog.prolog" (str "Prolog failed.")
end
open Auto
@@ -110,50 +114,49 @@ open Auto
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 { enter = begin fun gl ->
+ Proofview.Goal.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 }
-
-let hintmap_of secvars hdc concl =
+ let clenv' = clenv_unique_resolver ~flags clenv' gl in
+ Proofview.tclTHEN
+ (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
+ (Tactics.Simple.eapply c)
+ end
+
+let hintmap_of sigma secvars hdc concl =
match hdc with
| None -> fun db -> Hint_db.map_none ~secvars db
| Some hdc ->
- if occur_existential concl then
- (fun db -> Hint_db.map_existential ~secvars hdc concl db)
- else (fun db -> Hint_db.map_auto ~secvars hdc concl db)
+ if occur_existential sigma concl then
+ (fun db -> Hint_db.map_existential sigma ~secvars hdc concl db)
+ else (fun db -> Hint_db.map_auto sigma ~secvars hdc concl db)
(* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
let e_exact poly flags (c,clenv) =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let clenv', c = connect_hint_clenv poly c clenv gl in
Tacticals.New.tclTHEN
(Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
(e_give_exact c)
- end }
+ end
let rec e_trivial_fail_db db_list local_db =
- let next = Proofview.Goal.nf_enter { enter = begin fun gl ->
+ let next = Proofview.Goal.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 ->
+ end in
+ Proofview.Goal.enter begin fun gl ->
let secvars = compute_secvars gl in
let tacl =
registered_e_assumption ::
(Tacticals.New.tclTHEN Tactics.intro next) ::
- (List.map fst (e_trivial_resolve db_list local_db secvars (Tacmach.New.pf_nf_concl gl)))
+ (List.map fst (e_trivial_resolve (Tacmach.New.pf_env gl) (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_concl gl)))
in
Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl)
- end }
+ end
-and e_my_find_search db_list local_db secvars hdc concl =
- let hint_of_db = hintmap_of secvars hdc concl in
+and e_my_find_search env sigma db_list local_db secvars hdc concl =
+ let hint_of_db = hintmap_of sigma secvars hdc concl in
let hintl =
List.map_append (fun db ->
let flags = auto_flags_of_state (Hint_db.transparent_state db) in
@@ -177,19 +180,19 @@ and e_my_find_search db_list local_db secvars hdc concl =
| Extern tacast -> conclPattern concl p tacast
in
let tac = run_hint t tac in
- (tac, lazy (pr_hint t)))
+ (tac, lazy (pr_hint env sigma t)))
in
List.map tac_of_hint hintl
-and e_trivial_resolve db_list local_db secvars gl =
- let hd = try Some (decompose_app_bound gl) with Bound -> None in
- try priority (e_my_find_search db_list local_db secvars hd gl)
+and e_trivial_resolve env sigma db_list local_db secvars gl =
+ let hd = try Some (decompose_app_bound sigma gl) with Bound -> None in
+ try priority (e_my_find_search env sigma db_list local_db secvars hd gl)
with Not_found -> []
-let e_possible_resolve db_list local_db secvars gl =
- let hd = try Some (decompose_app_bound gl) with Bound -> None in
+let e_possible_resolve env sigma db_list local_db secvars gl =
+ let hd = try Some (decompose_app_bound sigma gl) with Bound -> None in
try List.map (fun (b, (tac, pp)) -> (tac, b, pp))
- (e_my_find_search db_list local_db secvars hd gl)
+ (e_my_find_search env sigma db_list local_db secvars hd gl)
with Not_found -> []
let find_first_goal gls =
@@ -202,11 +205,11 @@ type search_state = {
priority : int;
depth : int; (*r depth of search before failing *)
tacres : goal list sigma;
- last_tactic : std_ppcmds Lazy.t;
+ last_tactic : Pp.t Lazy.t;
dblist : hint_db list;
localdb : hint_db list;
prev : prev_search_state;
- local_lemmas : Tacexpr.delayed_open_constr list;
+ local_lemmas : delayed_open_constr list;
}
and prev_search_state = (* for info eauto *)
@@ -260,7 +263,7 @@ module SearchProblem = struct
let g = find_first_goal lg in
let hyps = pf_ids_of_hyps g in
let secvars = secvars_of_hyps (pf_hyps g) in
- let map_assum id = (e_give_exact (mkVar id), (-1), lazy (str "exact" ++ spc () ++ pr_id id)) in
+ let map_assum id = (e_give_exact (mkVar id), (-1), lazy (str "exact" ++ spc () ++ Id.print id)) in
let assumption_tacs =
let tacs = List.map map_assum hyps in
let l = filter_tactics s.tacres tacs in
@@ -287,9 +290,9 @@ module SearchProblem = struct
in
let rec_tacs =
let l =
- let concl = Reductionops.nf_evar (project g)(pf_concl g) in
+ let concl = Reductionops.nf_evar (project g) (pf_concl g) in
filter_tactics s.tacres
- (e_possible_resolve s.dblist (List.hd s.localdb) secvars concl)
+ (e_possible_resolve (pf_env g) (project g) s.dblist (List.hd s.localdb) secvars concl)
in
List.map
(fun (lgls, cost, pp) ->
@@ -330,8 +333,7 @@ let global_info_eauto = ref false
let _ =
Goptions.declare_bool_option
- { Goptions.optsync = true;
- Goptions.optdepr = false;
+ { Goptions.optdepr = false;
Goptions.optname = "Debug Eauto";
Goptions.optkey = ["Debug";"Eauto"];
Goptions.optread = (fun () -> !global_debug_eauto);
@@ -339,8 +341,7 @@ let _ =
let _ =
Goptions.declare_bool_option
- { Goptions.optsync = true;
- Goptions.optdepr = false;
+ { Goptions.optdepr = false;
Goptions.optname = "Info Eauto";
Goptions.optkey = ["Info";"Eauto"];
Goptions.optread = (fun () -> !global_info_eauto);
@@ -403,10 +404,10 @@ let e_search_auto debug (in_depth,p) lems db_list gl =
s.tacres
with Not_found ->
pr_info_nop d;
- error "eauto: search failed"
+ user_err Pp.(str "eauto: search failed")
-(* let e_search_auto_key = Profile.declare_profile "e_search_auto" *)
-(* let e_search_auto = Profile.profile5 e_search_auto_key e_search_auto *)
+(* let e_search_auto_key = CProfile.declare_profile "e_search_auto" *)
+(* let e_search_auto = CProfile.profile5 e_search_auto_key e_search_auto *)
let eauto_with_bases ?(debug=Off) np lems db_list =
tclTRY (e_search_auto debug np lems db_list)
@@ -436,11 +437,11 @@ let cons a l = a :: l
let autounfolds db occs cls gl =
let unfolds = List.concat (List.map (fun dbname ->
let db = try searchtable_map dbname
- with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname)
+ with Not_found -> user_err ~hdr:"autounfold" (str "Unknown database " ++ str dbname)
in
let (ids, csts) = Hint_db.unfolds db in
let hyps = pf_ids_of_hyps gl in
- let ids = Idset.filter (fun id -> List.mem id hyps) ids in
+ let ids = Id.Set.filter (fun id -> List.mem id hyps) ids in
Cset.fold (fun cst -> cons (AllOccurrences, EvalConstRef cst)) csts
(Id.Set.fold (fun id -> cons (AllOccurrences, EvalVarRef id)) ids [])) db)
in Proofview.V82.of_tactic (unfold_option unfolds cls) gl
@@ -464,18 +465,19 @@ let autounfold_tac db cls =
in
autounfold dbs cls
-let unfold_head env (ids, csts) c =
+let unfold_head env sigma (ids, csts) c =
let rec aux c =
- match kind_of_term c with
+ match EConstr.kind sigma c with
| Var id when Id.Set.mem id ids ->
(match Environ.named_body id env with
- | Some b -> true, b
+ | Some b -> true, EConstr.of_constr b
| None -> false, c)
- | Const (cst,u as c) when Cset.mem cst csts ->
- true, Environ.constant_value_in env c
+ | Const (cst, u) when Cset.mem cst csts ->
+ let u = EInstance.kind sigma u in
+ true, EConstr.of_constr (Environ.constant_value_in env (cst, u))
| App (f, args) ->
(match aux f with
- | true, f' -> true, Reductionops.whd_betaiota Evd.empty (mkApp (f', args))
+ | true, f' -> true, Reductionops.whd_betaiota sigma (mkApp (f', args))
| false, _ ->
let done_, args' =
Array.fold_left_i (fun i (done_, acc) arg ->
@@ -489,7 +491,7 @@ let unfold_head env (ids, csts) c =
else false, c)
| _ ->
let done_ = ref false in
- let c' = map_constr (fun c ->
+ let c' = EConstr.map sigma (fun c ->
if !done_ then c else
let x, c' = aux c in
done_ := x; c') c
@@ -497,18 +499,19 @@ let unfold_head env (ids, csts) c =
in aux c
let autounfold_one db cl =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
+ let sigma = Tacmach.New.project gl in
let concl = Proofview.Goal.concl gl in
let st =
List.fold_left (fun (i,c) dbname ->
let db = try searchtable_map dbname
- with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname)
+ with Not_found -> user_err ~hdr:"autounfold" (str "Unknown database " ++ str dbname)
in
let (ids, csts) = Hint_db.unfolds db in
(Id.Set.union ids i, Cset.union csts c)) (Id.Set.empty, Cset.empty) db
in
- let did, c' = unfold_head env st
+ let did, c' = unfold_head env sigma st
(match cl with Some (id, _) -> Tacmach.New.pf_get_hyp_typ id gl | None -> concl)
in
if did then
@@ -516,4 +519,4 @@ 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 17:32:00 +0000