aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml12
-rw-r--r--tactics/auto.mli2
-rw-r--r--tactics/class_tactics.ml42
-rw-r--r--tactics/tacinterp.ml100
4 files changed, 66 insertions, 50 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 59791f011..0e4091b3c 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -268,12 +268,12 @@ let dummy_goal =
{it = make_evar empty_named_context_val mkProp;
sigma = empty}
-let make_exact_entry pri (c,cty) =
+let make_exact_entry sigma pri (c,cty) =
let cty = strip_outer_cast cty in
match kind_of_term cty with
| Prod _ -> failwith "make_exact_entry"
| _ ->
- let pat = Pattern.pattern_of_constr cty in
+ let pat = Pattern.pattern_of_constr sigma cty in
let head =
try head_of_constr_reference (fst (head_constr cty))
with _ -> failwith "make_exact_entry"
@@ -287,7 +287,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) =
| Prod _ ->
let ce = mk_clenv_from dummy_goal (c,cty) in
let c' = clenv_type (* ~reduce:false *) ce in
- let pat = Pattern.pattern_of_constr c' in
+ let pat = Pattern.pattern_of_constr sigma c' in
let hd = (try head_pattern_bound pat
with BoundPattern -> failwith "make_apply_entry") in
let nmiss = List.length (clenv_missing ce) in
@@ -317,7 +317,7 @@ let make_resolves env sigma flags pri c =
let ents =
map_succeed
(fun f -> f (c,cty))
- [make_exact_entry pri; make_apply_entry env sigma flags pri]
+ [make_exact_entry sigma pri; make_apply_entry env sigma flags pri]
in
if ents = [] then
errorlabstrm "Hint"
@@ -354,7 +354,7 @@ let make_trivial env sigma c =
let hd = head_of_constr_reference (fst (head_constr t)) in
let ce = mk_clenv_from dummy_goal (c,t) in
(Some hd, { pri=1;
- pat = Some (Pattern.pattern_of_constr (clenv_type ce));
+ pat = Some (Pattern.pattern_of_constr sigma (clenv_type ce));
code=Res_pf_THEN_trivial_fail(c,{ce with env=empty_env}) })
open Vernacexpr
@@ -1102,7 +1102,7 @@ let make_resolve_any_hyp env sigma (id,_,ty) =
let ents =
map_succeed
(fun f -> f (mkVar id,ty))
- [make_exact_entry None; make_apply_entry env sigma (true,true,false) None]
+ [make_exact_entry sigma None; make_apply_entry env sigma (true,true,false) None]
in
ents
diff --git a/tactics/auto.mli b/tactics/auto.mli
index fe59dc1e1..072e02989 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -112,7 +112,7 @@ val print_hint_db : Hint_db.t -> unit
[c] is the term given as an exact proof to solve the goal;
[ctyp] is the type of [c]. *)
-val make_exact_entry : int option -> constr * constr -> hint_entry
+val make_exact_entry : evar_map -> int option -> constr * constr -> hint_entry
(* [make_apply_entry (eapply,verbose) pri (c,cty)].
[eapply] is true if this hint will be used only with EApply;
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 6f928e096..b77425f0d 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -271,7 +271,7 @@ let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) =
if keep then let c = mkVar id in
map_succeed
(fun f -> try f (c,cty) with UserError _ -> failwith "")
- [make_exact_entry pri; make_apply_entry env sigma flags pri]
+ [make_exact_entry sigma pri; make_apply_entry env sigma flags pri]
else []
let pf_filtered_hyps gls =
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index bef556345..f031df256 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -497,15 +497,15 @@ let intern_binding_name ist x =
and if a term w/o ltac vars, check the name is indeed quantified *)
x
-let intern_constr_gen isarity {ltacvars=lfun; gsigma=sigma; genv=env} c =
+let intern_constr_gen allow_patvar isarity {ltacvars=lfun; gsigma=sigma; genv=env} c =
let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in
let c' =
- warn (Constrintern.intern_gen isarity ~ltacvars:(fst lfun,[]) sigma env) c
+ warn (Constrintern.intern_gen isarity ~allow_patvar ~ltacvars:(fst lfun,[]) sigma env) c
in
(c',if !strict_check then None else Some c)
-let intern_constr = intern_constr_gen false
-let intern_type = intern_constr_gen true
+let intern_constr = intern_constr_gen false false
+let intern_type = intern_constr_gen false true
(* Globalize bindings *)
let intern_binding ist (loc,b,c) =
@@ -604,15 +604,17 @@ let intern_hyp_location ist (((b,occs),id),hl) =
(((b,List.map (intern_or_var ist) occs),intern_hyp_or_metaid ist id), hl)
(* Reads a pattern *)
-let intern_pattern sigma env ?(as_type=false) lfun = function
+let intern_pattern ist ?(as_type=false) lfun = function
| Subterm (b,ido,pc) ->
let ltacvars = (lfun,[]) in
- let (metas,pat) = intern_constr_pattern sigma env ~ltacvars pc in
- ido, metas, Subterm (b,ido,pat)
+ let (metas,pat) = intern_constr_pattern ist.gsigma ist.genv ~ltacvars pc in
+ let c = intern_constr_gen true false ist pc in
+ ido, metas, Subterm (b,ido,(c,pat))
| Term pc ->
let ltacvars = (lfun,[]) in
- let (metas,pat) = intern_constr_pattern sigma env ~as_type ~ltacvars pc in
- None, metas, Term pat
+ let (metas,pat) = intern_constr_pattern ist.gsigma ist.genv ~as_type ~ltacvars pc in
+ let c = intern_constr_gen true false ist pc in
+ None, metas, Term (c,pat)
let intern_constr_may_eval ist = function
| ConstrEval (r,c) -> ConstrEval (intern_red_expr ist r,intern_constr ist c)
@@ -649,16 +651,16 @@ let extend_values_with_bindings (ln,lm) lfun =
lmatch@lfun@lnames
(* Reads the hypotheses of a "match goal" rule *)
-let rec intern_match_goal_hyps sigma env lfun = function
+let rec intern_match_goal_hyps ist lfun = function
| (Hyp ((_,na) as locna,mp))::tl ->
- let ido, metas1, pat = intern_pattern sigma env ~as_type:true lfun mp in
- let lfun, metas2, hyps = intern_match_goal_hyps sigma env lfun tl in
+ let ido, metas1, pat = intern_pattern ist ~as_type:true lfun mp in
+ let lfun, metas2, hyps = intern_match_goal_hyps ist lfun tl in
let lfun' = name_cons na (Option.List.cons ido lfun) in
lfun', metas1@metas2, Hyp (locna,pat)::hyps
| (Def ((_,na) as locna,mv,mp))::tl ->
- let ido, metas1, patv = intern_pattern sigma env ~as_type:false lfun mv in
- let ido', metas2, patt = intern_pattern sigma env ~as_type:true lfun mp in
- let lfun, metas3, hyps = intern_match_goal_hyps sigma env lfun tl in
+ let ido, metas1, patv = intern_pattern ist ~as_type:false lfun mv in
+ let ido', metas2, patt = intern_pattern ist ~as_type:true lfun mp in
+ let lfun, metas3, hyps = intern_match_goal_hyps ist lfun tl in
let lfun' = name_cons na (Option.List.cons ido' (Option.List.cons ido lfun)) in
lfun', metas1@metas2@metas3, Def (locna,patv,patt)::hyps
| [] -> lfun, [], []
@@ -714,7 +716,7 @@ let rec intern_atomic lf ist x =
| TacAssert (otac,ipat,c) ->
TacAssert (Option.map (intern_tactic ist) otac,
Option.map (intern_intro_pattern lf ist) ipat,
- intern_constr_gen (otac<>None) ist c)
+ intern_constr_gen false (otac<>None) ist c)
| TacGeneralize cl ->
TacGeneralize (List.map (fun (c,na) ->
intern_constr_with_occurrences ist c,
@@ -904,8 +906,8 @@ and intern_match_rule ist = function
All (intern_tactic ist tc) :: (intern_match_rule ist tl)
| (Pat (rl,mp,tc))::tl ->
let {ltacvars=(lfun,l2); gsigma=sigma; genv=env} = ist in
- let lfun',metas1,hyps = intern_match_goal_hyps sigma env lfun rl in
- let ido,metas2,pat = intern_pattern sigma env lfun mp in
+ let lfun',metas1,hyps = intern_match_goal_hyps ist lfun rl in
+ let ido,metas2,pat = intern_pattern ist lfun mp in
let metas = list_uniquize (metas1@metas2) in
let ist' = { ist with ltacvars = (metas@(Option.List.cons ido lfun'),l2) } in
Pat (hyps,pat,intern_tactic ist' tc) :: (intern_match_rule ist tl)
@@ -1312,7 +1314,7 @@ let solve_remaining_evars fail_evar use_classes env initial_sigma evd c =
(* Side-effect *)
!evdref,c
-let interp_gen kind ist fail_evar use_classes env sigma (c,ce) =
+let interp_gen kind ist expand_evar fail_evar use_classes env sigma (c,ce) =
let (ltacvars,unbndltacvars as vars),typs =
extract_ltac_vars_data ist sigma env in
let c = match ce with
@@ -1325,25 +1327,34 @@ let interp_gen kind ist fail_evar use_classes env sigma (c,ce) =
intern_gen (kind = IsType) ~ltacvars:ltacdata sigma env c in
let trace = push_trace (dloc,LtacConstrInterp (c,vars)) ist.trace in
let evd,c =
- catch_error trace (understand_ltac sigma env (typs,unbndltacvars) kind) c in
- let evd,c = solve_remaining_evars fail_evar use_classes env sigma evd c in
+ catch_error trace
+ (understand_ltac expand_evar sigma env (typs,unbndltacvars) kind) c in
+ let evd,c =
+ if expand_evar then
+ solve_remaining_evars fail_evar use_classes env sigma evd c
+ else
+ evd,c in
db_constr ist.debug env c;
(evd,c)
(* Interprets a constr; expects evars to be solved *)
let interp_constr_gen kind ist env sigma c =
- snd (interp_gen kind ist true true env sigma c)
+ snd (interp_gen kind ist true true true env sigma c)
let interp_constr = interp_constr_gen (OfType None)
let interp_type = interp_constr_gen IsType
(* Interprets an open constr *)
-let interp_open_constr_gen kind ist = interp_gen kind ist false false
+let interp_open_constr_gen kind ist = interp_gen kind ist true false false
let interp_open_constr ccl =
interp_open_constr_gen (OfType ccl)
+let interp_typed_pattern ist env sigma c =
+ let sigma, c = interp_gen (OfType None) ist false false false env sigma c in
+ pattern_of_constr sigma c
+
(* Interprets a constr expression casted by the current goal *)
let pf_interp_casted_constr ist gl c =
interp_constr_gen (OfType (Some (pf_concl gl))) ist (pf_env gl) (project gl) c
@@ -1626,13 +1637,18 @@ let give_context ctxt = function
| Some id -> [id,VConstr_context ctxt]
(* Reads a pattern by substituting vars of lfun *)
-let eval_pattern lfun c =
- let lvar = List.map (fun (id,c) -> (id,lazy(pattern_of_constr c))) lfun in
- instantiate_pattern lvar c
+let use_types = false
+
+let eval_pattern lfun ist env sigma (c,pat) =
+ if use_types then
+ interp_typed_pattern ist env sigma c
+ else
+ let lvar = List.map (fun (id,c) -> (id,lazy(pattern_of_constr Evd.empty c))) lfun in
+ instantiate_pattern lvar pat
-let read_pattern lfun = function
- | Subterm (b,ido,pc) -> Subterm (b,ido,eval_pattern lfun pc)
- | Term pc -> Term (eval_pattern lfun pc)
+let read_pattern lfun ist env sigma = function
+ | Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c)
+ | Term c -> Term (eval_pattern lfun ist env sigma c)
(* Reads the hypotheses of a Match Context rule *)
let cons_and_check_name id l =
@@ -1642,23 +1658,23 @@ let cons_and_check_name id l =
" used twice in the same pattern."))
else id::l
-let rec read_match_goal_hyps lfun lidh = function
+let rec read_match_goal_hyps lfun ist env sigma lidh = function
| (Hyp ((loc,na) as locna,mp))::tl ->
let lidh' = name_fold cons_and_check_name na lidh in
- Hyp (locna,read_pattern lfun mp)::
- (read_match_goal_hyps lfun lidh' tl)
+ Hyp (locna,read_pattern lfun ist env sigma mp)::
+ (read_match_goal_hyps lfun ist env sigma lidh' tl)
| (Def ((loc,na) as locna,mv,mp))::tl ->
let lidh' = name_fold cons_and_check_name na lidh in
- Def (locna,read_pattern lfun mv, read_pattern lfun mp)::
- (read_match_goal_hyps lfun lidh' tl)
+ Def (locna,read_pattern lfun ist env sigma mv, read_pattern lfun ist env sigma mp)::
+ (read_match_goal_hyps lfun ist env sigma lidh' tl)
| [] -> []
(* Reads the rules of a Match Context or a Match *)
-let rec read_match_rule lfun = function
- | (All tc)::tl -> (All tc)::(read_match_rule lfun tl)
+let rec read_match_rule lfun ist env sigma = function
+ | (All tc)::tl -> (All tc)::(read_match_rule lfun ist env sigma tl)
| (Pat (rl,mp,tc))::tl ->
- Pat (read_match_goal_hyps lfun [] rl, read_pattern lfun mp,tc)
- :: read_match_rule lfun tl
+ Pat (read_match_goal_hyps lfun ist env sigma [] rl, read_pattern lfun ist env sigma mp,tc)
+ :: read_match_rule lfun ist env sigma tl
| [] -> []
(* For Match Context and Match *)
@@ -1989,7 +2005,7 @@ and interp_match_goal ist goal lz lr lmr =
else mt()) ++ str"."))
end in
apply_match_goal ist env goal 0 lmr
- (read_match_rule (fst (constr_list ist env)) lmr)
+ (read_match_rule (fst (constr_list ist env)) ist env (project goal) lmr)
(* Tries to match the hypotheses in a Match Context *)
and apply_hyps_context ist env lz goal mt lctxt lgmatch mhyps hyps =
@@ -2158,7 +2174,7 @@ and interp_match ist g lz constr lmr =
debugging_exception_step ist true e
(fun () -> str "evaluation of the matched expression");
raise e in
- let ilr = read_match_rule (fst (constr_list ist (pf_env g))) lmr in
+ let ilr = read_match_rule (fst (constr_list ist (pf_env g))) ist (pf_env g) (project g) lmr in
let res =
try apply_match ist csr ilr with e ->
debugging_exception_step ist true e (fun () -> str "match expression");
@@ -2589,8 +2605,8 @@ let subst_raw_may_eval subst = function
| ConstrTerm c -> ConstrTerm (subst_rawconstr subst c)
let subst_match_pattern subst = function
- | Subterm (b,ido,pc) -> Subterm (b,ido,subst_pattern subst pc)
- | Term pc -> Term (subst_pattern subst pc)
+ | Subterm (b,ido,(c,pc)) -> Subterm (b,ido,(subst_rawconstr subst c,subst_pattern subst pc))
+ | Term (c,pc) -> Term (subst_rawconstr subst c,subst_pattern subst pc)
let rec subst_match_goal_hyps subst = function
| Hyp (locs,mp) :: tl ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 22:35:47 +0000