summaryrefslogtreecommitdiff
path: root/tactics/tacinterp.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /tactics/tacinterp.ml
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'tactics/tacinterp.ml')
-rw-r--r--tactics/tacinterp.ml1181
1 files changed, 664 insertions, 517 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 37b3cbcb..f4547930 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tacinterp.ml 10135 2007-09-21 14:28:12Z herbelin $ *)
+(* $Id: tacinterp.ml 11166 2008-06-22 13:23:35Z herbelin $ *)
open Constrintern
open Closure
@@ -59,6 +59,8 @@ let error_syntactic_metavariables_not_allowed loc =
(loc,"out_ident",
str "Syntactic metavariables allowed only in quotations")
+let error_global_not_found_loc (loc,qid) = error_global_not_found_loc loc qid
+
let skip_metaid = function
| AI x -> x
| MetaId (loc,_) -> error_syntactic_metavariables_not_allowed loc
@@ -82,7 +84,7 @@ type value =
| VConstr of constr (* includes idents known to be bound and references *)
| VConstr_context of constr
| VList of value list
- | VRec of value ref
+ | VRec of (identifier*value) list ref * glob_tactic_expr
let locate_tactic_call loc = function
| VTactic (_,t) -> VTactic (loc,t)
@@ -101,8 +103,11 @@ let catch_error loc tac g =
(* Signature for interpretation: val_interp and interpretation functions *)
type interp_sign =
- { lfun : (identifier * value) list;
- debug : debug_info }
+ { lfun : (identifier * value) list;
+ avoid_ids : identifier list; (* ids inherited from the call context
+ (needed to get fresh ids) *)
+ debug : debug_info;
+ last_loc : loc }
let check_is_value = function
| VRTactic _ -> (* These are goals produced by Match *)
@@ -199,7 +204,7 @@ let add_primitive_tactic s tac =
atomic_mactab := Idmap.add id tac !atomic_mactab
let _ =
- let nocl = {onhyps=Some[];onconcl=true; concl_occs=[]} in
+ let nocl = {onhyps=Some[];concl_occs=all_occurrences_expr} in
List.iter
(fun (s,t) -> add_primitive_tactic s (TacAtom(dloc,t)))
[ "red", TacReduce(Red false,nocl);
@@ -212,10 +217,14 @@ let _ =
"cofix", TacCofix None;
"trivial", TacTrivial ([],None);
"auto", TacAuto(None,[],None);
- "left", TacLeft NoBindings;
- "right", TacRight NoBindings;
- "split", TacSplit(false,NoBindings);
- "constructor", TacAnyConstructor None;
+ "left", TacLeft(false,NoBindings);
+ "eleft", TacLeft(true,NoBindings);
+ "right", TacRight(false,NoBindings);
+ "eright", TacRight(true,NoBindings);
+ "split", TacSplit(false,false,NoBindings);
+ "esplit", TacSplit(true,false,NoBindings);
+ "constructor", TacAnyConstructor (false,None);
+ "econstructor", TacAnyConstructor (true,None);
"reflexivity", TacReflexivity;
"symmetry", TacSymmetry nocl
];
@@ -227,10 +236,9 @@ let _ =
]
let lookup_atomic id = Idmap.find id !atomic_mactab
-let is_atomic id = Idmap.mem id !atomic_mactab
let is_atomic_kn kn =
let (_,_,l) = repr_kn kn in
- is_atomic (id_of_label l)
+ Idmap.mem (id_of_label l) !atomic_mactab
(* Summary and Object declaration *)
let mactab = ref Gmap.empty
@@ -288,7 +296,7 @@ type glob_sign = {
type interp_genarg_type =
(glob_sign -> raw_generic_argument -> glob_generic_argument) *
(interp_sign -> goal sigma -> glob_generic_argument ->
- closed_generic_argument) *
+ typed_generic_argument) *
(substitution -> glob_generic_argument -> glob_generic_argument)
let extragenargtab =
@@ -305,7 +313,6 @@ let lookup_genarg_subst id = let (_,_,f) = lookup_genarg id in f
(* Dynamically check that an argument is a tactic, possibly unboxing VRec *)
let coerce_to_tactic loc id = function
- | VRec v -> !v
| VTactic _ | VFun _ | VRTactic _ as a -> a
| _ -> user_err_loc
(loc, "", str "variable " ++ pr_id id ++ str " should be bound to a tactic")
@@ -373,52 +380,105 @@ let intern_or_var ist = function
| ArgVar locid -> ArgVar (intern_hyp ist locid)
| ArgArg _ as x -> x
+let loc_of_by_notation f = function
+ | AN c -> f c
+ | ByNotation (loc,s) -> loc
+
+let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef"
+
+let intern_inductive_or_by_notation = function
+ | AN r -> Nametab.inductive_of_reference r
+ | ByNotation (loc,ntn) ->
+ destIndRef (Notation.interp_notation_as_global_reference loc
+ (function IndRef ind -> true | _ -> false) ntn)
+
let intern_inductive ist = function
- | Ident (loc,id) when find_var id ist -> ArgVar (loc,id)
- | r -> ArgArg (Nametab.global_inductive r)
+ | AN (Ident (loc,id)) when find_var id ist -> ArgVar (loc,id)
+ | r -> ArgArg (intern_inductive_or_by_notation r)
let intern_global_reference ist = function
| Ident (loc,id) when find_var id ist -> ArgVar (loc,id)
| r ->
- let loc,qid = qualid_of_reference r in
- try ArgArg (loc,locate_global qid)
- with _ ->
- error_global_not_found_loc loc qid
+ let loc,_ as lqid = qualid_of_reference r in
+ try ArgArg (loc,locate_global_with_alias lqid)
+ with Not_found ->
+ error_global_not_found_loc lqid
-let intern_tac_ref ist = function
- | Ident (loc,id) when find_ltacvar id ist -> ArgVar (loc,id)
+let intern_ltac_variable ist = function
| Ident (loc,id) ->
- ArgArg (loc,
- try find_recvar id ist
- with Not_found -> locate_tactic (make_short_qualid id))
- | r ->
- let (loc,qid) = qualid_of_reference r in
- ArgArg (loc,locate_tactic qid)
-
-let intern_tactic_reference ist r =
- try intern_tac_ref ist r
- with Not_found ->
- let (loc,qid) = qualid_of_reference r in
- error_global_not_found_loc loc qid
+ if find_ltacvar id ist then
+ (* A local variable of any type *)
+ ArgVar (loc,id)
+ else
+ (* A recursive variable *)
+ ArgArg (loc,find_recvar id ist)
+ | _ ->
+ raise Not_found
let intern_constr_reference strict ist = function
| Ident (_,id) when (not strict & find_hyp id ist) or find_ctxvar id ist ->
RVar (dloc,id), None
| r ->
- let loc,qid = qualid_of_reference r in
- RRef (loc,locate_global qid), if strict then None else Some (CRef r)
-
-let intern_reference strict ist r =
- (try Reference (intern_tac_ref ist r)
- with Not_found ->
- (try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
- with Not_found ->
- (match r with
- | Ident (loc,id) when is_atomic id -> Tacexp (lookup_atomic id)
- | Ident (loc,id) when not strict -> IntroPattern (IntroIdentifier id)
- | _ ->
- let (loc,qid) = qualid_of_reference r in
- error_global_not_found_loc loc qid)))
+ let loc,_ as lqid = qualid_of_reference r in
+ RRef (loc,locate_global_with_alias lqid), if strict then None else Some (CRef r)
+
+(* Internalize an isolated reference in position of tactic *)
+
+let intern_isolated_global_tactic_reference r =
+ let (loc,qid) = qualid_of_reference r in
+ try TacCall (loc,ArgArg (loc,locate_tactic qid),[])
+ with Not_found ->
+ match r with
+ | Ident (_,id) -> Tacexp (lookup_atomic id)
+ | _ -> raise Not_found
+
+let intern_isolated_tactic_reference ist r =
+ (* An ltac reference *)
+ try Reference (intern_ltac_variable ist r)
+ with Not_found ->
+ (* A global tactic *)
+ try intern_isolated_global_tactic_reference r
+ with Not_found ->
+ (* Tolerance for compatibility, allow not to use "constr:" *)
+ try ConstrMayEval (ConstrTerm (intern_constr_reference true ist r))
+ with Not_found ->
+ (* Reference not found *)
+ error_global_not_found_loc (qualid_of_reference r)
+
+(* Internalize an applied tactic reference *)
+
+let intern_applied_global_tactic_reference r =
+ let (loc,qid) = qualid_of_reference r in
+ ArgArg (loc,locate_tactic qid)
+
+let intern_applied_tactic_reference ist r =
+ (* An ltac reference *)
+ try intern_ltac_variable ist r
+ with Not_found ->
+ (* A global tactic *)
+ try intern_applied_global_tactic_reference r
+ with Not_found ->
+ (* Reference not found *)
+ error_global_not_found_loc (qualid_of_reference r)
+
+(* Intern a reference parsed in a non-tactic entry *)
+
+let intern_non_tactic_reference strict ist r =
+ (* An ltac reference *)
+ try Reference (intern_ltac_variable ist r)
+ with Not_found ->
+ (* A constr reference *)
+ try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
+ with Not_found ->
+ (* Tolerance for compatibility, allow not to use "ltac:" *)
+ try intern_isolated_global_tactic_reference r
+ with Not_found ->
+ (* By convention, use IntroIdentifier for unbound ident, when not in a def *)
+ match r with
+ | Ident (_,id) when not strict -> IntroPattern (IntroIdentifier id)
+ | _ ->
+ (* Reference not found *)
+ error_global_not_found_loc (qualid_of_reference r)
let intern_message_token ist = function
| (MsgString _ | MsgInt _ as x) -> x
@@ -431,7 +491,7 @@ let rec intern_intro_pattern lf ist = function
IntroOrAndPattern (intern_case_intro_pattern lf ist l)
| IntroIdentifier id ->
IntroIdentifier (intern_ident lf ist id)
- | IntroWildcard | IntroAnonymous as x -> x
+ | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _ as x -> x
and intern_case_intro_pattern lf ist =
List.map (List.map (intern_intro_pattern lf ist))
@@ -478,53 +538,64 @@ let intern_clause_pattern ist (l,occl) =
(* TODO: catch ltac vars *)
let intern_induction_arg ist = function
- | ElimOnConstr c -> ElimOnConstr (intern_constr ist c)
+ | ElimOnConstr c -> ElimOnConstr (intern_constr_with_bindings ist c)
| ElimOnAnonHyp n as x -> x
| ElimOnIdent (loc,id) ->
if !strict_check then
(* If in a defined tactic, no intros-until *)
- ElimOnConstr (intern_constr ist (CRef (Ident (dloc,id))))
+ ElimOnConstr (intern_constr ist (CRef (Ident (dloc,id))),NoBindings)
else
ElimOnIdent (loc,id)
+let evaluable_of_global_reference = function
+ | ConstRef c -> EvalConstRef c
+ | VarRef c -> EvalVarRef c
+ | r -> error_not_evaluable (pr_global r)
+
+let short_name = function
+ | AN (Ident (loc,id)) when not !strict_check -> Some (loc,id)
+ | _ -> None
+
+let interp_global_reference r =
+ let lqid = qualid_of_reference r in
+ try locate_global_with_alias lqid
+ with Not_found ->
+ match r with
+ | Ident (loc,id) when not !strict_check -> VarRef id
+ | _ -> error_global_not_found_loc lqid
+
+let intern_evaluable_reference_or_by_notation = function
+ | AN r -> evaluable_of_global_reference (interp_global_reference r)
+ | ByNotation (loc,ntn) ->
+ evaluable_of_global_reference
+ (Notation.interp_notation_as_global_reference loc
+ (function ConstRef _ | VarRef _ -> true | _ -> false) ntn)
+
(* Globalizes a reduction expression *)
let intern_evaluable ist = function
- | Ident (loc,id) when find_ltacvar id ist -> ArgVar (loc,id)
- | Ident (_,id) when
+ | AN (Ident (loc,id)) when find_ltacvar id ist -> ArgVar (loc,id)
+ | AN (Ident (_,id)) when
(not !strict_check & find_hyp id ist) or find_ctxvar id ist ->
ArgArg (EvalVarRef id, None)
| r ->
- let loc,qid = qualid_of_reference r in
- try
- let e = match locate_global qid with
- | ConstRef c -> EvalConstRef c
- | VarRef c -> EvalVarRef c
- | _ -> error_not_evaluable (pr_reference r) in
- let short_name = match r with
- | Ident (loc,id) when not !strict_check -> Some (loc,id)
- | _ -> None in
- ArgArg (e,short_name)
- with
- | Not_found ->
- match r with
- | Ident (loc,id) when not !strict_check ->
- ArgArg (EvalVarRef id, Some (loc,id))
- | _ -> error_global_not_found_loc loc qid
+ let e = intern_evaluable_reference_or_by_notation r in
+ let na = short_name r in
+ ArgArg (e,na)
let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid)
let intern_flag ist red =
{ red with rConst = List.map (intern_evaluable ist) red.rConst }
-let intern_constr_occurrence ist (l,c) = (l,intern_constr ist c)
+let intern_constr_with_occurrences ist (l,c) = (l,intern_constr ist c)
let intern_red_expr ist = function
| Unfold l -> Unfold (List.map (intern_unfold ist) l)
| Fold l -> Fold (List.map (intern_constr ist) l)
| Cbv f -> Cbv (intern_flag ist f)
| Lazy f -> Lazy (intern_flag ist f)
- | Pattern l -> Pattern (List.map (intern_constr_occurrence ist) l)
- | Simpl o -> Simpl (option_map (intern_constr_occurrence ist) o)
+ | Pattern l -> Pattern (List.map (intern_constr_with_occurrences ist) l)
+ | Simpl o -> Simpl (Option.map (intern_constr_with_occurrences ist) o)
| (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r ) -> r
@@ -533,27 +604,27 @@ let intern_inversion_strength lf ist = function
NonDepInversion (k,List.map (intern_hyp_or_metaid ist) idl,
intern_intro_pattern lf ist ids)
| DepInversion (k,copt,ids) ->
- DepInversion (k, option_map (intern_constr ist) copt,
+ DepInversion (k, Option.map (intern_constr ist) copt,
intern_intro_pattern lf ist ids)
| InversionUsing (c,idl) ->
InversionUsing (intern_constr ist c, List.map (intern_hyp_or_metaid ist) idl)
(* Interprets an hypothesis name *)
-let intern_hyp_location ist ((occs,id),hl) =
- ((List.map (intern_or_var ist) occs,intern_hyp ist (skip_metaid id)), hl)
+let intern_hyp_location ist (((b,occs),id),hl) =
+ (((b,List.map (intern_or_var ist) occs),intern_hyp ist (skip_metaid id)), hl)
-let interp_constrpattern_gen sigma env ltacvar c =
- let c = intern_gen false ~allow_soapp:true ~ltacvars:(ltacvar,[])
+let interp_constrpattern_gen sigma env ?(as_type=false) ltacvar c =
+ let c = intern_gen as_type ~allow_patvar:true ~ltacvars:(ltacvar,[])
sigma env c in
pattern_of_rawconstr c
(* Reads a pattern *)
-let intern_pattern sigma env lfun = function
+let intern_pattern sigma env ?(as_type=false) lfun = function
| Subterm (ido,pc) ->
let (metas,pat) = interp_constrpattern_gen sigma env lfun pc in
ido, metas, Subterm (ido,pat)
| Term pc ->
- let (metas,pat) = interp_constrpattern_gen sigma env lfun pc in
+ let (metas,pat) = interp_constrpattern_gen sigma env ~as_type lfun pc in
None, metas, Term pat
let intern_constr_may_eval ist = function
@@ -584,30 +655,16 @@ let extern_request ch req gl la =
(* Reads the hypotheses of a Match Context rule *)
let rec intern_match_context_hyps sigma env lfun = function
| (Hyp ((_,na) as locna,mp))::tl ->
- let ido, metas1, pat = intern_pattern sigma env lfun mp in
+ let ido, metas1, pat = intern_pattern sigma env ~as_type:true lfun mp in
let lfun, metas2, hyps = intern_match_context_hyps sigma env lfun tl in
- let lfun' = name_cons na (option_cons ido lfun) in
+ let lfun' = name_cons na (Option.List.cons ido lfun) in
lfun', metas1@metas2, Hyp (locna,pat)::hyps
| [] -> lfun, [], []
(* Utilities *)
-let rec filter_some = function
- | None :: l -> filter_some l
- | Some a :: l -> a :: filter_some l
- | [] -> []
-
-let extract_names lrc =
- List.fold_right
- (fun ((loc,name),_) l ->
- if List.mem name l then
- user_err_loc
- (loc, "intern_tactic", str "This variable is bound several times");
- name::l)
- lrc []
-
let extract_let_names lrc =
List.fold_right
- (fun ((loc,name),_,_) l ->
+ (fun ((loc,name),_) l ->
if List.mem name l then
user_err_loc
(loc, "glob_tactic", str "This variable is bound several times");
@@ -615,10 +672,10 @@ let extract_let_names lrc =
lrc []
let clause_app f = function
- { onhyps=None; onconcl=b;concl_occs=nl } ->
- { onhyps=None; onconcl=b; concl_occs=nl }
- | { onhyps=Some l; onconcl=b;concl_occs=nl } ->
- { onhyps=Some(List.map f l); onconcl=b;concl_occs=nl}
+ { onhyps=None; concl_occs=nl } ->
+ { onhyps=None; concl_occs=nl }
+ | { onhyps=Some l; concl_occs=nl } ->
+ { onhyps=Some(List.map f l); concl_occs=nl}
(* Globalizes tactics : raw_tactic_expr -> glob_tactic_expr *)
let rec intern_atomic lf ist x =
@@ -628,70 +685,70 @@ let rec intern_atomic lf ist x =
TacIntroPattern (List.map (intern_intro_pattern lf ist) l)
| TacIntrosUntil hyp -> TacIntrosUntil (intern_quantified_hypothesis ist hyp)
| TacIntroMove (ido,ido') ->
- TacIntroMove (option_map (intern_ident lf ist) ido,
- option_map (intern_hyp ist) ido')
+ TacIntroMove (Option.map (intern_ident lf ist) ido,
+ Option.map (intern_hyp ist) ido')
| TacAssumption -> TacAssumption
| TacExact c -> TacExact (intern_constr ist c)
| TacExactNoCheck c -> TacExactNoCheck (intern_constr ist c)
| TacVmCastNoCheck c -> TacVmCastNoCheck (intern_constr ist c)
- | TacApply cb -> TacApply (intern_constr_with_bindings ist cb)
- | TacElim (cb,cbo) ->
- TacElim (intern_constr_with_bindings ist cb,
- option_map (intern_constr_with_bindings ist) cbo)
+ | TacApply (a,ev,cb) -> TacApply (a,ev,intern_constr_with_bindings ist cb)
+ | TacElim (ev,cb,cbo) ->
+ TacElim (ev,intern_constr_with_bindings ist cb,
+ Option.map (intern_constr_with_bindings ist) cbo)
| TacElimType c -> TacElimType (intern_type ist c)
- | TacCase cb -> TacCase (intern_constr_with_bindings ist cb)
+ | TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings ist cb)
| TacCaseType c -> TacCaseType (intern_type ist c)
- | TacFix (idopt,n) -> TacFix (option_map (intern_ident lf ist) idopt,n)
- | TacMutualFix (id,n,l) ->
+ | TacFix (idopt,n) -> TacFix (Option.map (intern_ident lf ist) idopt,n)
+ | TacMutualFix (b,id,n,l) ->
let f (id,n,c) = (intern_ident lf ist id,n,intern_type ist c) in
- TacMutualFix (intern_ident lf ist id, n, List.map f l)
- | TacCofix idopt -> TacCofix (option_map (intern_ident lf ist) idopt)
- | TacMutualCofix (id,l) ->
+ TacMutualFix (b,intern_ident lf ist id, n, List.map f l)
+ | TacCofix idopt -> TacCofix (Option.map (intern_ident lf ist) idopt)
+ | TacMutualCofix (b,id,l) ->
let f (id,c) = (intern_ident lf ist id,intern_type ist c) in
- TacMutualCofix (intern_ident lf ist id, List.map f l)
+ TacMutualCofix (b,intern_ident lf ist id, List.map f l)
| TacCut c -> TacCut (intern_type ist c)
| TacAssert (otac,ipat,c) ->
- TacAssert (option_map (intern_tactic ist) otac,
+ TacAssert (Option.map (intern_tactic ist) otac,
intern_intro_pattern lf ist ipat,
intern_constr_gen (otac<>None) ist c)
- | TacGeneralize cl -> TacGeneralize (List.map (intern_constr ist) cl)
+ | TacGeneralize cl ->
+ TacGeneralize (List.map (fun (c,na) ->
+ intern_constr_with_occurrences ist c,
+ intern_name lf ist na) cl)
| TacGeneralizeDep c -> TacGeneralizeDep (intern_constr ist c)
- | TacLetTac (na,c,cls) ->
+ | TacLetTac (na,c,cls,b) ->
let na = intern_name lf ist na in
TacLetTac (na,intern_constr ist c,
- (clause_app (intern_hyp_location ist) cls))
-(* | TacInstantiate (n,c,idh) ->
- TacInstantiate (n,intern_constr ist c,
- (match idh with
- ConclLocation () -> ConclLocation ()
- | HypLocation (id,hloc) ->
- HypLocation(intern_hyp_or_metaid ist id,hloc)))
-*)
+ (clause_app (intern_hyp_location ist) cls),b)
(* Automation tactics *)
| TacTrivial (lems,l) -> TacTrivial (List.map (intern_constr ist) lems,l)
| TacAuto (n,lems,l) ->
- TacAuto (option_map (intern_or_var ist) n,
+ TacAuto (Option.map (intern_or_var ist) n,
List.map (intern_constr ist) lems,l)
| TacAutoTDB n -> TacAutoTDB n
| TacDestructHyp (b,id) -> TacDestructHyp(b,intern_hyp ist id)
| TacDestructConcl -> TacDestructConcl
| TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2)
- | TacDAuto (n,p) -> TacDAuto (option_map (intern_or_var ist) n,p)
+ | TacDAuto (n,p,lems) ->
+ TacDAuto (Option.map (intern_or_var ist) n,p,
+ List.map (intern_constr ist) lems)
(* Derived basic tactics *)
| TacSimpleInduction h ->
TacSimpleInduction (intern_quantified_hypothesis ist h)
- | TacNewInduction (lc,cbo,ids) ->
- TacNewInduction (List.map (intern_induction_arg ist) lc,
- option_map (intern_constr_with_bindings ist) cbo,
- (intern_intro_pattern lf ist ids))
+ | TacNewInduction (ev,lc,cbo,ids,cls) ->
+ TacNewInduction (ev,List.map (intern_induction_arg ist) lc,
+ Option.map (intern_constr_with_bindings ist) cbo,
+ intern_intro_pattern lf ist ids,
+ Option.map (clause_app (intern_hyp_location ist)) cls)
| TacSimpleDestruct h ->
TacSimpleDestruct (intern_quantified_hypothesis ist h)
- | TacNewDestruct (c,cbo,ids) ->
- TacNewDestruct (List.map (intern_induction_arg ist) c,
- option_map (intern_constr_with_bindings ist) cbo,
- (intern_intro_pattern lf ist ids))
+ | TacNewDestruct (ev,c,cbo,ids,cls) ->
+ TacNewDestruct (ev,List.map (intern_induction_arg ist) c,
+ Option.map (intern_constr_with_bindings ist) cbo,
+ intern_intro_pattern lf ist ids,
+ Option.map (clause_app (intern_hyp_location ist)) cls)
| TacDoubleInduction (h1,h2) ->
let h1 = intern_quantified_hypothesis ist h1 in
let h2 = intern_quantified_hypothesis ist h2 in
@@ -708,21 +765,28 @@ let rec intern_atomic lf ist x =
| TacClearBody l -> TacClearBody (List.map (intern_hyp_or_metaid ist) l)
| TacMove (dep,id1,id2) ->
TacMove (dep,intern_hyp_or_metaid ist id1,intern_hyp_or_metaid ist id2)
- | TacRename (id1,id2) -> TacRename (intern_hyp_or_metaid ist id1, intern_hyp_or_metaid ist id2)
-
+ | TacRename l ->
+ TacRename (List.map (fun (id1,id2) ->
+ intern_hyp_or_metaid ist id1,
+ intern_hyp_or_metaid ist id2) l)
+ | TacRevert l -> TacRevert (List.map (intern_hyp_or_metaid ist) l)
+
(* Constructors *)
- | TacLeft bl -> TacLeft (intern_bindings ist bl)
- | TacRight bl -> TacRight (intern_bindings ist bl)
- | TacSplit (b,bl) -> TacSplit (b,intern_bindings ist bl)
- | TacAnyConstructor t -> TacAnyConstructor (option_map (intern_tactic ist) t)
- | TacConstructor (n,bl) -> TacConstructor (n, intern_bindings ist bl)
+ | TacLeft (ev,bl) -> TacLeft (ev,intern_bindings ist bl)
+ | TacRight (ev,bl) -> TacRight (ev,intern_bindings ist bl)
+ | TacSplit (ev,b,bl) -> TacSplit (ev,b,intern_bindings ist bl)
+ | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (intern_tactic ist) t)
+ | TacConstructor (ev,n,bl) -> TacConstructor (ev,n,intern_bindings ist bl)
(* Conversion *)
| TacReduce (r,cl) ->
TacReduce (intern_red_expr ist r, clause_app (intern_hyp_location ist) cl)
| TacChange (occl,c,cl) ->
- TacChange (option_map (intern_constr_occurrence ist) occl,
- (if occl = None then intern_type ist c else intern_constr ist c),
+ TacChange (Option.map (intern_constr_with_occurrences ist) occl,
+ (if occl = None & (cl.onhyps = None or cl.onhyps = Some []) &
+ (cl.concl_occs = all_occurrences_expr or
+ cl.concl_occs = no_occurrences_expr)
+ then intern_type ist c else intern_constr ist c),
clause_app (intern_hyp_location ist) cl)
(* Equivalence relations *)
@@ -732,9 +796,12 @@ let rec intern_atomic lf ist x =
| TacTransitivity c -> TacTransitivity (intern_constr ist c)
(* Equality and inversion *)
- | TacRewrite (b,c,cl) ->
- TacRewrite (b,intern_constr_with_bindings ist c,
- clause_app (intern_hyp_location ist) cl)
+ | TacRewrite (ev,l,cl,by) ->
+ TacRewrite
+ (ev,
+ List.map (fun (b,m,c) -> (b,m,intern_constr_with_bindings ist c)) l,
+ clause_app (intern_hyp_location ist) cl,
+ Option.map (intern_tactic ist) by)
| TacInversion (inv,hyp) ->
TacInversion (intern_inversion_strength lf ist inv,
intern_quantified_hypothesis ist hyp)
@@ -756,19 +823,12 @@ and intern_tactic_seq ist = function
let t = intern_atomic lf ist t in
!lf, TacAtom (adjust_loc loc, t)
| TacFun tacfun -> ist.ltacvars, TacFun (intern_tactic_fun ist tacfun)
- | TacLetRecIn (lrc,u) ->
- let names = extract_names lrc in
+ | TacLetIn (isrec,l,u) ->
let (l1,l2) = ist.ltacvars in
- let ist = { ist with ltacvars = (names@l1,l2) } in
- let lrc = List.map (fun (n,b) -> (n,intern_tactic_fun ist b)) lrc in
- ist.ltacvars, TacLetRecIn (lrc,intern_tactic ist u)
- | TacLetIn (l,u) ->
- let l = List.map
- (fun (n,c,b) ->
- (n,option_map (intern_tactic ist) c, intern_tacarg !strict_check ist b)) l in
- let (l1,l2) = ist.ltacvars in
- let ist' = { ist with ltacvars = ((extract_let_names l)@l1,l2) } in
- ist.ltacvars, TacLetIn (l,intern_tactic ist' u)
+ let ist' = { ist with ltacvars = (extract_let_names l @ l1, l2) } in
+ let l = List.map (fun (n,b) ->
+ (n,intern_tacarg !strict_check (if isrec then ist' else ist) b)) l in
+ ist.ltacvars, TacLetIn (isrec,l,intern_tactic ist' u)
| TacMatchContext (lz,lr,lmr) ->
ist.ltacvars, TacMatchContext(lz,lr, intern_match_rule ist lmr)
| TacMatch (lz,c,lmr) ->
@@ -778,15 +838,21 @@ and intern_tactic_seq ist = function
ist.ltacvars, TacFail (intern_or_var ist n,intern_message ist l)
| TacProgress tac -> ist.ltacvars, TacProgress (intern_tactic ist tac)
| TacAbstract (tac,s) -> ist.ltacvars, TacAbstract (intern_tactic ist tac,s)
- | TacThen (t1,t2) ->
+ | TacThen (t1,[||],t2,[||]) ->
let lfun', t1 = intern_tactic_seq ist t1 in
let lfun'', t2 = intern_tactic_seq { ist with ltacvars = lfun' } t2 in
- lfun'', TacThen (t1,t2)
+ lfun'', TacThen (t1,[||],t2,[||])
+ | TacThen (t1,tf,t2,tl) ->
+ let lfun', t1 = intern_tactic_seq ist t1 in
+ let ist' = { ist with ltacvars = lfun' } in
+ (* Que faire en cas de (tac complexe avec Match et Thens; tac2) ?? *)
+ lfun', TacThen (t1,Array.map (intern_tactic ist') tf,intern_tactic ist' t2,
+ Array.map (intern_tactic ist') tl)
| TacThens (t,tl) ->
let lfun', t = intern_tactic_seq ist t in
+ let ist' = { ist with ltacvars = lfun' } in
(* Que faire en cas de (tac complexe avec Match et Thens; tac2) ?? *)
- lfun',
- TacThens (t, List.map (intern_tactic { ist with ltacvars = lfun' }) tl)
+ lfun', TacThens (t, List.map (intern_tactic ist') tl)
| TacDo (n,tac) ->
ist.ltacvars, TacDo (intern_or_var ist n,intern_tactic ist tac)
| TacTry tac -> ist.ltacvars, TacTry (intern_tactic ist tac)
@@ -801,25 +867,28 @@ and intern_tactic_seq ist = function
and intern_tactic_fun ist (var,body) =
let (l1,l2) = ist.ltacvars in
- let lfun' = List.rev_append (filter_some var) l1 in
+ let lfun' = List.rev_append (Option.List.flatten var) l1 in
(var,intern_tactic { ist with ltacvars = (lfun',l2) } body)
and intern_tacarg strict ist = function
| TacVoid -> TacVoid
- | Reference r -> intern_reference strict ist r
+ | Reference r -> intern_non_tactic_reference strict ist r
| IntroPattern ipat ->
let lf = ref([],[]) in (*How to know what names the intropattern binds?*)
IntroPattern (intern_intro_pattern lf ist ipat)
| Integer n -> Integer n
| ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c)
- | MetaIdArg (loc,s) ->
+ | MetaIdArg (loc,istac,s) ->
(* $id can occur in Grammar tactic... *)
let id = id_of_string s in
- if find_ltacvar id ist then Reference (ArgVar (adjust_loc loc,id))
+ if find_ltacvar id ist then
+ if istac then Reference (ArgVar (adjust_loc loc,id))
+ else ConstrMayEval (ConstrTerm (RVar (adjust_loc loc,id), None))
else error_syntactic_metavariables_not_allowed loc
+ | TacCall (loc,f,[]) -> intern_isolated_tactic_reference ist f
| TacCall (loc,f,l) ->
TacCall (loc,
- intern_tactic_reference ist f,
+ intern_applied_tactic_reference ist f,
List.map (intern_tacarg !strict_check ist) l)
| TacExternal (loc,com,req,la) ->
TacExternal (loc,com,req,List.map (intern_tacarg !strict_check ist) la)
@@ -840,7 +909,7 @@ and intern_match_rule ist = function
let lfun',metas1,hyps = intern_match_context_hyps sigma env lfun rl in
let ido,metas2,pat = intern_pattern sigma env lfun mp in
let metas = list_uniquize (metas1@metas2) in
- let ist' = { ist with ltacvars = (metas@(option_cons ido lfun'),l2) } 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)
| [] -> []
@@ -1026,10 +1095,23 @@ let set_debug pos = debug := pos
(* Gives the state of debug *)
let get_debug () = !debug
+let debugging_step ist pp =
+ match ist.debug with
+ | DebugOn lev ->
+ safe_msgnl (str "Level " ++ int lev ++ str": " ++ pp () ++ fnl())
+ | _ -> ()
+
+let debugging_exception_step ist signal_anomaly e pp =
+ let explain_exc =
+ if signal_anomaly then explain_logic_error
+ else explain_logic_error_no_anomaly in
+ debugging_step ist (fun () ->
+ pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ !explain_exc e)
+
let error_ltac_variable loc id env v s =
user_err_loc (loc, "", str "Ltac variable " ++ pr_id id ++
str " is bound to" ++ spc () ++ pr_value env v ++ spc () ++
- str "which cannot be coerced to " ++ str s)
+ strbrk "which cannot be coerced to " ++ str s)
exception CannotCoerceTo of string
@@ -1043,22 +1125,25 @@ let interp_ltac_var coerce ist env locid =
with Not_found -> anomaly "Detected as ltac var at interning time"
(* Interprets an identifier which must be fresh *)
-let coerce_to_ident env = function
+let coerce_to_ident fresh env = function
| VIntroPattern (IntroIdentifier id) -> id
- | VConstr c when isVar c & not (is_variable env (destVar c)) ->
- (* This happens e.g. in definitions like "Tac H = clear H; intro H" *)
+ | VConstr c when isVar c & not (fresh & is_variable env (destVar c)) ->
+ (* We need it fresh for intro e.g. in "Tac H = clear H; intro H" *)
destVar c
| v -> raise (CannotCoerceTo "a fresh identifier")
-let interp_ident ist gl id =
+let interp_ident_gen fresh ist gl id =
let env = pf_env gl in
- try try_interp_ltac_var (coerce_to_ident env) ist (Some env) (dloc,id)
+ try try_interp_ltac_var (coerce_to_ident fresh env) ist (Some env) (dloc,id)
with Not_found -> id
+let interp_ident = interp_ident_gen false
+let interp_fresh_ident = interp_ident_gen true
+
(* Interprets an optional identifier which must be fresh *)
-let interp_name ist gl = function
+let interp_fresh_name ist gl = function
| Anonymous -> Anonymous
- | Name id -> Name (interp_ident ist gl id)
+ | Name id -> Name (interp_fresh_ident ist gl id)
let coerce_to_intro_pattern env = function
| VIntroPattern ipat -> ipat
@@ -1086,7 +1171,8 @@ let coerce_to_int = function
let interp_int ist locid =
try try_interp_ltac_var coerce_to_int ist None locid
- with Not_found -> user_err_loc(fst locid,"interp_int",str "Unbound variable")
+ with Not_found -> user_err_loc(fst locid,"interp_int",
+ str "Unbound variable" ++ pr_id (snd locid))
let interp_int_or_var ist = function
| ArgVar locid -> interp_int ist locid
@@ -1196,13 +1282,15 @@ let interp_evaluable ist env = function
interp_ltac_var (coerce_to_evaluable_ref env) ist (Some env) locid
(* Interprets an hypothesis name *)
+let interp_occurrences ist (b,occs) =
+ (b,interp_int_or_var_list ist occs)
+
let interp_hyp_location ist gl ((occs,id),hl) =
- ((interp_int_or_var_list ist occs,interp_hyp ist gl id),hl)
+ ((interp_occurrences ist occs,interp_hyp ist gl id),hl)
-let interp_clause ist gl { onhyps=ol; onconcl=b; concl_occs=occs } =
- { onhyps=option_map(List.map (interp_hyp_location ist gl)) ol;
- onconcl=b;
- concl_occs=interp_int_or_var_list ist occs }
+let interp_clause ist gl { onhyps=ol; concl_occs=occs } =
+ { onhyps=Option.map(List.map (interp_hyp_location ist gl)) ol;
+ concl_occs=interp_occurrences ist occs }
(* Interpretation of constructions *)
@@ -1220,12 +1308,12 @@ let rec constr_list_aux env = function
let constr_list ist env = constr_list_aux env ist.lfun
-(*Extract the identifier list from lfun: join all branches (what to do else?)*)
+(* Extract the identifier list from lfun: join all branches (what to do else?)*)
let rec intropattern_ids = function
| IntroIdentifier id -> [id]
| IntroOrAndPattern ll ->
List.flatten (List.map intropattern_ids (List.flatten ll))
- | IntroWildcard | IntroAnonymous -> []
+ | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _ -> []
let rec extract_ids ids = function
| (id,VIntroPattern ipat)::tl when not (List.mem id ids) ->
@@ -1237,13 +1325,16 @@ let default_fresh_id = id_of_string "H"
let interp_fresh_id ist gl l =
let ids = map_succeed (function ArgVar(_,id) -> id | _ -> failwith "") l in
- let avoid = extract_ids ids ist.lfun in
+ let avoid = (extract_ids ids ist.lfun) @ ist.avoid_ids in
let id =
if l = [] then default_fresh_id
else
- id_of_string (String.concat "" (List.map (function
- | ArgArg s -> s
- | ArgVar (_,id) -> string_of_id (interp_ident ist gl id)) l)) in
+ let s =
+ String.concat "" (List.map (function
+ | ArgArg s -> s
+ | ArgVar (_,id) -> string_of_id (interp_ident ist gl id)) l) in
+ let s = if Lexer.is_keyword s then s^"0" else s in
+ id_of_string s in
Tactics.fresh_id avoid id gl
(* To retype a list of key*constr with undefined key *)
@@ -1270,7 +1361,7 @@ let solvable_by_tactic env evi (ev,args) src =
begin
try
by (tclCOMPLETE tac);
- let _,(const,_,_) = cook_proof () in
+ let _,(const,_,_) = cook_proof ignore in
delete_current_proof (); const.const_entry_body
with e when Logic.catchable_exception e ->
delete_current_proof();
@@ -1278,20 +1369,20 @@ let solvable_by_tactic env evi (ev,args) src =
end
| _ -> raise Exit
-let solve_remaining_evars env initial_sigma evars c =
- let isevars = ref evars in
+let solve_remaining_evars env initial_sigma evd c =
+ let evdref = ref (Typeclasses.resolve_typeclasses ~fail:true env evd) in
let rec proc_rec c =
- match kind_of_term (Reductionops.whd_evar (evars_of !isevars) c) with
+ match kind_of_term (Reductionops.whd_evar (evars_of !evdref) c) with
| Evar (ev,args as k) when not (Evd.mem initial_sigma ev) ->
- let (loc,src) = evar_source ev !isevars in
- let sigma = evars_of !isevars in
+ let (loc,src) = evar_source ev !evdref in
+ let sigma = evars_of !evdref in
+ let evi = Evd.find sigma ev in
(try
- let evi = Evd.find sigma ev in
let c = solvable_by_tactic env evi k src in
- isevars := Evd.evar_define ev c !isevars;
+ evdref := Evd.evar_define ev c !evdref;
c
with Exit ->
- Pretype_errors.error_unsolvable_implicit loc env sigma src)
+ Pretype_errors.error_unsolvable_implicit loc env sigma evi src None)
| _ -> map_constr proc_rec c
in
proc_rec c
@@ -1318,8 +1409,8 @@ let interp_econstr kind ist sigma env cc =
(* Interprets an open constr *)
let interp_open_constr ccl ist sigma env cc =
- let isevars,c = interp_gen (OfType ccl) ist sigma env cc in
- (evars_of isevars,c)
+ let evd,c = interp_gen (OfType ccl) ist sigma env cc in
+ (evars_of evd,c)
let interp_constr = interp_econstr (OfType None)
@@ -1341,32 +1432,82 @@ let pf_interp_constr ist gl =
let constr_list_of_VList env = function
| VList l -> List.map (constr_of_value env) l
| _ -> raise Not_found
-
+
+let pf_interp_constr_in_compound_list inj_fun dest_fun interp_fun ist gl l =
+ let env = pf_env gl in
+ let try_expand_ltac_var x =
+ try match dest_fun x with
+ | RVar (_,id), _ ->
+ List.map inj_fun (constr_list_of_VList env (List.assoc id ist.lfun))
+ | _ ->
+ raise Not_found
+ with Not_found ->
+ (*all of dest_fun, List.assoc, constr_list_of_VList may raise Not_found*)
+ [interp_fun ist gl x] in
+ List.flatten (List.map try_expand_ltac_var l)
+
+let pf_interp_constr_list =
+ pf_interp_constr_in_compound_list (fun x -> x) (fun x -> x)
+ (fun ist gl -> interp_constr ist (project gl) (pf_env gl))
+
+(*
let pf_interp_constr_list_as_list ist gl (c,_ as x) =
match c with
| RVar (_,id) ->
(try constr_list_of_VList (pf_env gl) (List.assoc id ist.lfun)
- with Not_found -> [interp_constr ist (project gl) (pf_env gl) x])
+ with Not_found -> [])
| _ -> [interp_constr ist (project gl) (pf_env gl) x]
let pf_interp_constr_list ist gl l =
List.flatten (List.map (pf_interp_constr_list_as_list ist gl) l)
+*)
+
+let inj_open c = (Evd.empty,c)
+
+let pf_interp_open_constr_list =
+ pf_interp_constr_in_compound_list inj_open (fun x -> x)
+ (fun ist gl -> interp_open_constr None ist (project gl) (pf_env gl))
+
+(*
+let pf_interp_open_constr_list_as_list ist gl (c,_ as x) =
+ match c with
+ | RVar (_,id) ->
+ (try List.map inj_open
+ (constr_list_of_VList (pf_env gl) (List.assoc id ist.lfun))
+ with Not_found ->
+ [interp_open_constr None ist (project gl) (pf_env gl) x])
+ | _ ->
+ [interp_open_constr None ist (project gl) (pf_env gl) x]
+
+let pf_interp_open_constr_list ist gl l =
+ List.flatten (List.map (pf_interp_open_constr_list_as_list ist gl) l)
+*)
(* Interprets a type expression *)
let pf_interp_type ist gl =
interp_type ist (project gl) (pf_env gl)
(* Interprets a reduction expression *)
-let interp_unfold ist env (l,qid) =
- (interp_int_or_var_list ist l,interp_evaluable ist env qid)
+let interp_unfold ist env (occs,qid) =
+ (interp_occurrences ist occs,interp_evaluable ist env qid)
let interp_flag ist env red =
{ red with rConst = List.map (interp_evaluable ist env) red.rConst }
-let interp_pattern ist sigma env (l,c) =
- (interp_int_or_var_list ist l, interp_constr ist sigma env c)
+let interp_pattern ist sigma env (occs,c) =
+ (interp_occurrences ist occs, interp_constr ist sigma env c)
+
+let pf_interp_constr_with_occurrences ist gl =
+ interp_pattern ist (project gl) (pf_env gl)
-let pf_interp_pattern ist gl = interp_pattern ist (project gl) (pf_env gl)
+let pf_interp_constr_with_occurrences_and_name_as_list =
+ pf_interp_constr_in_compound_list
+ (fun c -> ((all_occurrences_expr,c),Anonymous))
+ (function ((occs,c),Anonymous) when occs = all_occurrences_expr -> c
+ | _ -> raise Not_found)
+ (fun ist gl (occ_c,na) ->
+ (interp_pattern ist (project gl) (pf_env gl) occ_c,
+ interp_fresh_name ist gl na))
let interp_red_expr ist sigma env = function
| Unfold l -> Unfold (List.map (interp_unfold ist env) l)
@@ -1374,7 +1515,7 @@ let interp_red_expr ist sigma env = function
| Cbv f -> Cbv (interp_flag ist env f)
| Lazy f -> Lazy (interp_flag ist env f)
| Pattern l -> Pattern (List.map (interp_pattern ist sigma env) l)
- | Simpl o -> Simpl (option_map (interp_pattern ist sigma env) o)
+ | Simpl o -> Simpl (Option.map (interp_pattern ist sigma env) o)
| (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r
let pf_interp_red_expr ist gl = interp_red_expr ist (project gl) (pf_env gl)
@@ -1396,34 +1537,18 @@ let interp_may_eval f ist gl = function
| ConstrTerm c ->
try
f ist gl c
- with e ->
- begin
- match ist.debug with
- DebugOn lev ->
- safe_msgnl (str "Level " ++ int lev ++
- str ": interpretation of term " ++
- Printer.pr_rawconstr_env (pf_env gl) (fst c) ++
- str " raised an exception" ++
- fnl() ++
- !Tactic_debug.explain_logic_error_no_anomaly e)
- | _ -> ()
- end;
- raise e
+ with e ->
+ debugging_exception_step ist false e (fun () ->
+ str"interpretation of term " ++ pr_rawconstr_env (pf_env gl) (fst c));
+ raise e
(* Interprets a constr expression possibly to first evaluate *)
let interp_constr_may_eval ist gl c =
let csr =
try
interp_may_eval pf_interp_constr ist gl c
- with e ->
- begin match ist.debug with
- DebugOn lev ->
- safe_msgnl (str "Level " ++ int lev ++
- str ": evaluation of term raised an exception" ++
- fnl() ++
- !Tactic_debug.explain_logic_error_no_anomaly e)
- | _ -> ()
- end;
+ with e ->
+ debugging_exception_step ist false e (fun () -> str"evaluation of term");
raise e
in
begin
@@ -1431,6 +1556,12 @@ let interp_constr_may_eval ist gl c =
csr
end
+let inj_may_eval = function
+ | ConstrTerm c -> ConstrTerm (inj_open c)
+ | ConstrEval (r,c) -> ConstrEval (Tactics.inj_red_expr r,inj_open c)
+ | ConstrContext (id,c) -> ConstrContext (id,inj_open c)
+ | ConstrTypeOf c -> ConstrTypeOf (inj_open c)
+
let message_of_value = function
| VVoid -> str "()"
| VInteger n -> int n
@@ -1456,7 +1587,7 @@ let rec interp_message_nl ist = function
let rec interp_intro_pattern ist gl = function
| IntroOrAndPattern l -> IntroOrAndPattern (interp_case_intro_pattern ist gl l)
| IntroIdentifier id -> interp_intro_pattern_var ist (pf_env gl) id
- | IntroWildcard | IntroAnonymous as x -> x
+ | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _ as x -> x
and interp_case_intro_pattern ist gl =
List.map (List.map (interp_intro_pattern ist gl))
@@ -1472,8 +1603,7 @@ let interp_quantified_hypothesis ist = function
| AnonHyp n -> AnonHyp n
| NamedHyp id ->
try try_interp_ltac_var coerce_to_quantified_hypothesis ist None(dloc,id)
- with Not_found | Stdpp.Exc_located (_, UserError _) | UserError _
- -> NamedHyp id
+ with Not_found -> NamedHyp id
let interp_binding_name ist = function
| AnonHyp n -> AnonHyp n
@@ -1482,8 +1612,7 @@ let interp_binding_name ist = function
(* user has to use other names for variables if these ones clash with *)
(* a name intented to be used as a (non-variable) identifier *)
try try_interp_ltac_var coerce_to_quantified_hypothesis ist None(dloc,id)
- with Not_found | Stdpp.Exc_located (_, UserError _) | UserError _
- -> NamedHyp id
+ with Not_found -> NamedHyp id
(* Quantified named or numbered hypothesis or hypothesis in context *)
(* (as in Inversion) *)
@@ -1502,25 +1631,29 @@ let interp_declared_or_quantified_hypothesis ist gl = function
(coerce_to_decl_or_quant_hyp env) ist (Some env) (dloc,id)
with Not_found -> NamedHyp id
-let interp_induction_arg ist gl = function
- | ElimOnConstr c -> ElimOnConstr (pf_interp_constr ist gl c)
- | ElimOnAnonHyp n as x -> x
- | ElimOnIdent (loc,id) ->
- if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id)
- else ElimOnConstr
- (pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id)))))
-
let interp_binding ist gl (loc,b,c) =
- (loc,interp_binding_name ist b,pf_interp_constr ist gl c)
+ (loc,interp_binding_name ist b,pf_interp_open_constr false ist gl c)
let interp_bindings ist gl = function
| NoBindings -> NoBindings
-| ImplicitBindings l -> ImplicitBindings (pf_interp_constr_list ist gl l)
+| ImplicitBindings l -> ImplicitBindings (pf_interp_open_constr_list ist gl l)
| ExplicitBindings l -> ExplicitBindings (List.map (interp_binding ist gl) l)
let interp_constr_with_bindings ist gl (c,bl) =
(pf_interp_constr ist gl c, interp_bindings ist gl bl)
+let interp_open_constr_with_bindings ist gl (c,bl) =
+ (pf_interp_open_constr false ist gl c, interp_bindings ist gl bl)
+
+let interp_induction_arg ist gl = function
+ | ElimOnConstr c -> ElimOnConstr (interp_constr_with_bindings ist gl c)
+ | ElimOnAnonHyp n as x -> x
+ | ElimOnIdent (loc,id) ->
+ if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id)
+ else ElimOnConstr
+ (pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id)))),
+ NoBindings)
+
let mk_constr_value ist gl c = VConstr (pf_interp_constr ist gl c)
let mk_hyp_value ist gl c = VConstr (mkVar (interp_hyp ist gl c))
let mk_int_or_var_value ist c = VInteger (interp_int_or_var ist c)
@@ -1531,15 +1664,13 @@ let rec val_interp ist gl (tac:glob_tactic_expr) =
let value_interp ist = match tac with
(* Immediate evaluation *)
| TacFun (it,body) -> VFun (ist.lfun,it,body)
- | TacLetRecIn (lrc,u) -> letrec_interp ist gl lrc u
- | TacLetIn (l,u) ->
- let addlfun = interp_letin ist gl l in
- val_interp { ist with lfun=addlfun@ist.lfun } gl u
+ | TacLetIn (true,l,u) -> interp_letrec ist gl l u
+ | TacLetIn (false,l,u) -> interp_letin ist gl l u
| TacMatchContext (lz,lr,lmr) -> interp_match_context ist gl lz lr lmr
| TacMatch (lz,c,lmr) -> interp_match ist gl lz c lmr
| TacArg a -> interp_tacarg ist gl a
(* Delayed evaluation *)
- | t -> VTactic (dloc,eval_tactic ist t)
+ | t -> VTactic (ist.last_loc,eval_tactic ist t)
in check_for_interrupt ();
match ist.debug with
@@ -1549,18 +1680,28 @@ let rec val_interp ist gl (tac:glob_tactic_expr) =
and eval_tactic ist = function
| TacAtom (loc,t) -> fun gl -> catch_error loc (interp_atomic ist gl t) gl
- | TacFun _ | TacLetRecIn _ | TacLetIn _ -> assert false
+ | TacFun _ | TacLetIn _ -> assert false
| TacMatchContext _ | TacMatch _ -> assert false
| TacId s -> tclIDTAC_MESSAGE (interp_message_nl ist s)
| TacFail (n,s) -> tclFAIL (interp_int_or_var ist n) (interp_message ist s)
| TacProgress tac -> tclPROGRESS (interp_tactic ist tac)
- | TacAbstract (tac,s) -> Tactics.tclABSTRACT s (interp_tactic ist tac)
- | TacThen (t1,t2) -> tclTHEN (interp_tactic ist t1) (interp_tactic ist t2)
- | TacThens (t,tl) ->
- tclTHENS (interp_tactic ist t) (List.map (interp_tactic ist) tl)
+ | TacAbstract (tac,ido) ->
+ fun gl -> Tactics.tclABSTRACT
+ (Option.map (interp_ident ist gl) ido) (interp_tactic ist tac) gl
+ | TacThen (t1,tf,t,tl) ->
+ tclTHENS3PARTS (interp_tactic ist t1)
+ (Array.map (interp_tactic ist) tf) (interp_tactic ist t) (Array.map (interp_tactic ist) tl)
+ | TacThens (t1,tl) -> tclTHENS (interp_tactic ist t1) (List.map (interp_tactic ist) tl)
| TacDo (n,tac) -> tclDO (interp_int_or_var ist n) (interp_tactic ist tac)
| TacTry tac -> tclTRY (interp_tactic ist tac)
- | TacInfo tac -> tclINFO (interp_tactic ist tac)
+ | TacInfo tac ->
+ let t = (interp_tactic ist tac) in
+ tclINFO
+ begin
+ match tac with
+ TacAtom (_,_) -> t
+ | _ -> abstract_tactic_expr (TacArg (Tacexp tac)) t
+ end
| TacRepeat tac -> tclREPEAT (interp_tactic ist tac)
| TacOrelse (tac1,tac2) ->
tclORELSE (interp_tactic ist tac1) (interp_tactic ist tac2)
@@ -1569,13 +1710,21 @@ and eval_tactic ist = function
| TacComplete tac -> tclCOMPLETE (interp_tactic ist tac)
| TacArg a -> assert false
+and force_vrec ist gl = function
+ | VRec (lfun,body) -> val_interp {ist with lfun = !lfun} gl body
+ | v -> v
+
and interp_ltac_reference isapplied mustbetac ist gl = function
| ArgVar (loc,id) ->
let v = List.assoc id ist.lfun in
+ let v = force_vrec ist gl v in
if mustbetac then coerce_to_tactic loc id v else v
| ArgArg (loc,r) ->
- let v = val_interp {lfun=[];debug=ist.debug} gl (lookup r) in
- if isapplied then v else locate_tactic_call loc v
+ let ids = extract_ids [] ist.lfun in
+ let ist =
+ { lfun=[]; debug=ist.debug; avoid_ids=ids;
+ last_loc = if isapplied then ist.last_loc else loc } in
+ val_interp ist gl (lookup r)
and interp_tacarg ist gl = function
| TacVoid -> VVoid
@@ -1583,7 +1732,7 @@ and interp_tacarg ist gl = function
| Integer n -> VInteger n
| IntroPattern ipat -> VIntroPattern (interp_intro_pattern ist gl ipat)
| ConstrMayEval c -> VConstr (interp_constr_may_eval ist gl c)
- | MetaIdArg (loc,id) -> assert false
+ | MetaIdArg (loc,_,id) -> assert false
| TacCall (loc,r,[]) -> interp_ltac_reference false true ist gl r
| TacCall (loc,f,l) ->
let fv = interp_ltac_reference true true ist gl f
@@ -1620,32 +1769,15 @@ and interp_app ist gl fv largs loc =
let (newlfun,lvar,lval)=head_with_value (var,largs) in
if lvar=[] then
let v =
- let res =
- try
- val_interp { ist with lfun=newlfun@olfun } gl body
- with e ->
- begin match ist.debug with
- DebugOn lev ->
- safe_msgnl
- (str "Level " ++ int lev ++
- str ": evaluation raises an exception" ++
- fnl() ++
- !Tactic_debug.explain_logic_error_no_anomaly e)
- | _ -> ()
- end;
- raise e
- in
- (match ist.debug with
- DebugOn lev ->
- safe_msgnl (str "Level " ++ int lev ++
- str ": evaluation returns" ++ fnl() ++
- pr_value (Some (pf_env gl)) res)
- | _ -> ());
- res
- in
-
- if lval=[] then locate_tactic_call loc v
- else interp_app ist gl v lval loc
+ try
+ let lloc = if lval=[] then loc else ist.last_loc in
+ val_interp { ist with lfun=newlfun@olfun; last_loc=lloc } gl body
+ with e ->
+ debugging_exception_step ist false e (fun () -> str "evaluation");
+ raise e in
+ debugging_step ist (fun () ->
+ str "evaluation returns" ++ fnl() ++ pr_value (Some (pf_env gl)) v);
+ if lval=[] then v else interp_app ist gl v lval loc
else
VFun(newlfun@olfun,lvar,body)
| _ ->
@@ -1674,47 +1806,20 @@ and eval_with_fail ist is_lazy goal tac =
| FailError (lvl,s) ->
raise (FailError (lvl - 1, s))
-(* Interprets recursive expressions *)
-and letrec_interp ist gl lrc u =
- let lref = Array.to_list (Array.make (List.length lrc) (ref VVoid)) in
- let lenv =
- List.fold_right2 (fun ((loc,name),_) vref l -> (name,VRec vref)::l)
- lrc lref [] in
- let lve = List.map (fun ((loc,name),(var,body)) ->
- (name,VFun(lenv@ist.lfun,var,body))) lrc in
- begin
- List.iter2 (fun vref (_,ve) -> vref:=ve) lref lve;
- val_interp { ist with lfun=lve@ist.lfun } gl u
- end
+(* Interprets the clauses of a recursive LetIn *)
+and interp_letrec ist gl llc u =
+ let lref = ref ist.lfun in
+ let lve = list_map_left (fun ((_,id),b) -> (id,VRec (lref,TacArg b))) llc in
+ lref := lve@ist.lfun;
+ let ist = { ist with lfun = lve@ist.lfun } in
+ val_interp ist gl u
(* Interprets the clauses of a LetIn *)
-and interp_letin ist gl = function
- | [] -> []
- | ((loc,id),None,t)::tl ->
- let v = interp_tacarg ist gl t in
- check_is_value v;
- (id,v):: (interp_letin ist gl tl)
- | ((loc,id),Some com,tce)::tl ->
- let env = pf_env gl in
- let typ = constr_of_value env (val_interp ist gl com)
- and v = interp_tacarg ist gl tce in
- let csr =
- try
- constr_of_value env v
- with Not_found ->
- try
- let t = tactic_of_value v in
- let ndc = Environ.named_context_val env in
- start_proof id (Local,Proof Lemma) ndc typ (fun _ _ -> ());
- by t;
- let (_,({const_entry_body = pft},_,_)) = cook_proof () in
- delete_proof (dloc,id);
- pft
- with | NotTactic ->
- delete_proof (dloc,id);
- errorlabstrm "Tacinterp.interp_letin"
- (str "Term or fully applied tactic expected in Let")
- in (id,VConstr (mkCast (csr,DEFAULTcast, typ)))::(interp_letin ist gl tl)
+and interp_letin ist gl llc u =
+ let lve = list_map_left (fun ((_,id),body) ->
+ let v = interp_tacarg ist gl body in check_is_value v; (id,v)) llc in
+ let ist = { ist with lfun = lve@ist.lfun } in
+ val_interp ist gl u
(* Interprets the Match Context expressions *)
and interp_match_context ist g lz lr lmr =
@@ -1761,7 +1866,7 @@ and interp_match_context ist g lz lr lmr =
errorlabstrm "Tacinterp.apply_match_context"
(v 0 (str "No matching clauses for match goal" ++
(if ist.debug=DebugOff then
- fnl() ++ str "(use \"Debug On\" for more info)"
+ fnl() ++ str "(use \"Set Ltac Debug\" for more info)"
else mt())))
end in
let env = pf_env g in
@@ -1811,7 +1916,8 @@ and interp_genarg ist gl x =
in_gen wit_intro_pattern
(interp_intro_pattern ist gl (out_gen globwit_intro_pattern x))
| IdentArgType ->
- in_gen wit_ident (interp_ident ist gl (out_gen globwit_ident x))
+ in_gen wit_ident
+ (interp_fresh_ident ist gl (out_gen globwit_ident x))
| VarArgType ->
in_gen wit_var (interp_hyp ist gl (out_gen globwit_var x))
| RefArgType ->
@@ -1892,34 +1998,25 @@ and interp_match ist g lz constr lmr =
(try eval_with_fail ist lz g t
with e when is_match_catchable e -> apply_match ist csr [])
| (Pat ([],Term c,mt))::tl ->
- (try let lm =
- (try matches c csr with
- e ->
- (match ist.debug with
- DebugOn lev ->
- safe_msgnl (str "Level " ++ int lev ++
- str ": matching with pattern" ++ fnl() ++
- Printer.pr_constr_pattern_env (pf_env g) c ++ fnl() ++
- str "raised the exception" ++ fnl() ++
- !Tactic_debug.explain_logic_error_no_anomaly e)
- | _ -> ()); raise e) in
- (try let lm = List.map (fun (id,c) -> (id,VConstr c)) lm in
- eval_with_fail { ist with lfun=lm@ist.lfun } lz g mt
+ (try
+ let lm =
+ try matches c csr
+ with e ->
+ debugging_exception_step ist false e (fun () ->
+ str "matching with pattern" ++ fnl () ++
+ pr_constr_pattern_env (pf_env g) c);
+ raise e in
+ try
+ let lm = List.map (fun (id,c) -> (id,VConstr c)) lm in
+ eval_with_fail { ist with lfun=lm@ist.lfun } lz g mt
with e ->
- (match ist.debug with
- DebugOn lev ->
- safe_msgnl (str "rule body for pattern" ++ fnl() ++
- Printer.pr_constr_pattern_env (pf_env g) c ++ fnl() ++
- str "raised the exception" ++ fnl() ++
- !Tactic_debug.explain_logic_error_no_anomaly e)
- | _ -> ()); raise e)
+ debugging_exception_step ist false e (fun () ->
+ str "rule body for pattern" ++
+ pr_constr_pattern_env (pf_env g) c);
+ raise e
with e when is_match_catchable e ->
- (match ist.debug with
- DebugOn lev ->
- safe_msgnl (str "Level " ++ int lev ++
- str ":switching to the next rule");
- | DebugOff -> ());
- apply_match ist csr tl)
+ debugging_step ist (fun () -> str "switching to the next rule");
+ apply_match ist csr tl)
| (Pat ([],Subterm (id,c),mt))::tl ->
(try apply_match_subterm ist 0 (id,c) csr mt
@@ -1928,49 +2025,33 @@ and interp_match ist g lz constr lmr =
errorlabstrm "Tacinterp.apply_match" (str
"No matching clauses for match") in
let csr =
- try interp_ltac_constr ist g constr with
- e -> (match ist.debug with
- DebugOn lev ->
- safe_msgnl (str "Level " ++ int lev ++
- str ": evaluation of the matched expression raised " ++
- str "the exception" ++ fnl() ++
- !Tactic_debug.explain_logic_error e)
- | _ -> ()); raise e in
+ try interp_ltac_constr ist g constr with e ->
+ 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 res =
- try apply_match ist csr ilr with
- e ->
- begin match ist.debug with
- DebugOn lev ->
- safe_msgnl (str "Level " ++ int lev ++
- str ": match expression failed with error" ++ fnl() ++
- !Tactic_debug.explain_logic_error e)
- | _ -> ()
- end;
- raise e in
- (if ist.debug <> DebugOff then
- safe_msgnl (str "match expression returns " ++
- pr_value (Some (pf_env g)) res));
- res
+ try apply_match ist csr ilr with e ->
+ debugging_exception_step ist true e (fun () -> str "match expression");
+ raise e in
+ debugging_step ist (fun () ->
+ str "match expression returns " ++ pr_value (Some (pf_env g)) res);
+ res
(* Interprets tactic expressions : returns a "constr" *)
and interp_ltac_constr ist gl e =
let result =
- try (val_interp ist gl e) with Not_found ->
- begin match ist.debug with
- DebugOn lev ->
- safe_msgnl (str "Level " ++ int lev ++
- str ": evaluation failed for" ++ fnl() ++
- Pptactic.pr_glob_tactic (pf_env gl) e)
- | _ -> ()
- end;
+ try val_interp ist gl e with Not_found ->
+ debugging_step ist (fun () ->
+ str "evaluation failed for" ++ fnl() ++
+ Pptactic.pr_glob_tactic (pf_env gl) e);
raise Not_found in
- try let cresult = constr_of_value (pf_env gl) result in
- (if !debug <> DebugOff then
- safe_msgnl (Pptactic.pr_glob_tactic (pf_env gl) e ++ fnl() ++
- str " has value " ++ fnl() ++ print_constr_env (pf_env gl) cresult);
- cresult)
-
+ try
+ let cresult = constr_of_value (pf_env gl) result in
+ debugging_step ist (fun () ->
+ Pptactic.pr_glob_tactic (pf_env gl) e ++ fnl() ++
+ str " has value " ++ fnl() ++ print_constr_env (pf_env gl) cresult);
+ cresult
with Not_found ->
errorlabstrm ""
(str "Must evaluate to a term" ++ fnl() ++
@@ -2016,72 +2097,72 @@ and interp_atomic ist gl = function
| TacIntrosUntil hyp ->
h_intros_until (interp_quantified_hypothesis ist hyp)
| TacIntroMove (ido,ido') ->
- h_intro_move (option_map (interp_ident ist gl) ido)
- (option_map (interp_hyp ist gl) ido')
+ h_intro_move (Option.map (interp_fresh_ident ist gl) ido)
+ (Option.map (interp_hyp ist gl) ido')
| TacAssumption -> h_assumption
| TacExact c -> h_exact (pf_interp_casted_constr ist gl c)
| TacExactNoCheck c -> h_exact_no_check (pf_interp_constr ist gl c)
| TacVmCastNoCheck c -> h_vm_cast_no_check (pf_interp_constr ist gl c)
- | TacApply cb -> h_apply (interp_constr_with_bindings ist gl cb)
- | TacElim (cb,cbo) ->
- h_elim (interp_constr_with_bindings ist gl cb)
- (option_map (interp_constr_with_bindings ist gl) cbo)
+ | TacApply (a,ev,cb) -> h_apply a ev (interp_constr_with_bindings ist gl cb)
+ | TacElim (ev,cb,cbo) ->
+ h_elim ev (interp_constr_with_bindings ist gl cb)
+ (Option.map (interp_constr_with_bindings ist gl) cbo)
| TacElimType c -> h_elim_type (pf_interp_type ist gl c)
- | TacCase cb -> h_case (interp_constr_with_bindings ist gl cb)
+ | TacCase (ev,cb) -> h_case ev (interp_constr_with_bindings ist gl cb)
| TacCaseType c -> h_case_type (pf_interp_type ist gl c)
- | TacFix (idopt,n) -> h_fix (option_map (interp_ident ist gl) idopt) n
- | TacMutualFix (id,n,l) ->
- let f (id,n,c) = (interp_ident ist gl id,n,pf_interp_type ist gl c) in
- h_mutual_fix (interp_ident ist gl id) n (List.map f l)
- | TacCofix idopt -> h_cofix (option_map (interp_ident ist gl) idopt)
- | TacMutualCofix (id,l) ->
- let f (id,c) = (interp_ident ist gl id,pf_interp_type ist gl c) in
- h_mutual_cofix (interp_ident ist gl id) (List.map f l)
+ | TacFix (idopt,n) -> h_fix (Option.map (interp_fresh_ident ist gl) idopt) n
+ | TacMutualFix (b,id,n,l) ->
+ let f (id,n,c) = (interp_fresh_ident ist gl id,n,pf_interp_type ist gl c)
+ in h_mutual_fix b (interp_fresh_ident ist gl id) n (List.map f l)
+ | TacCofix idopt -> h_cofix (Option.map (interp_fresh_ident ist gl) idopt)
+ | TacMutualCofix (b,id,l) ->
+ let f (id,c) = (interp_fresh_ident ist gl id,pf_interp_type ist gl c) in
+ h_mutual_cofix b (interp_fresh_ident ist gl id) (List.map f l)
| TacCut c -> h_cut (pf_interp_type ist gl c)
| TacAssert (t,ipat,c) ->
let c = (if t=None then pf_interp_constr else pf_interp_type) ist gl c in
- abstract_tactic (TacAssert (t,ipat,c))
- (Tactics.forward (option_map (interp_tactic ist) t)
+ abstract_tactic (TacAssert (t,ipat,inj_open c))
+ (Tactics.forward (Option.map (interp_tactic ist) t)
(interp_intro_pattern ist gl ipat) c)
- | TacGeneralize cl -> h_generalize (pf_interp_constr_list ist gl cl)
+ | TacGeneralize cl ->
+ h_generalize_gen
+ (pf_interp_constr_with_occurrences_and_name_as_list ist gl cl)
| TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c)
- | TacLetTac (na,c,clp) ->
+ | TacLetTac (na,c,clp,b) ->
let clp = interp_clause ist gl clp in
- h_let_tac (interp_name ist gl na) (pf_interp_constr ist gl c) clp
-(* | TacInstantiate (n,c,idh) -> h_instantiate n (fst c)
- (* pf_interp_constr ist gl c *)
- (match idh with
- ConclLocation () -> ConclLocation ()
- | HypLocation (id,hloc) ->
- HypLocation(interp_hyp ist gl id,hloc))
-*)
+ h_let_tac b (interp_fresh_name ist gl na) (pf_interp_constr ist gl c) clp
+
(* Automation tactics *)
| TacTrivial (lems,l) ->
Auto.h_trivial (pf_interp_constr_list ist gl lems)
- (option_map (List.map (interp_hint_base ist)) l)
+ (Option.map (List.map (interp_hint_base ist)) l)
| TacAuto (n,lems,l) ->
- Auto.h_auto (option_map (interp_int_or_var ist) n)
+ Auto.h_auto (Option.map (interp_int_or_var ist) n)
(pf_interp_constr_list ist gl lems)
- (option_map (List.map (interp_hint_base ist)) l)
+ (Option.map (List.map (interp_hint_base ist)) l)
| TacAutoTDB n -> Dhyp.h_auto_tdb n
| TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (interp_hyp ist gl id)
| TacDestructConcl -> Dhyp.h_destructConcl
| TacSuperAuto (n,l,b1,b2) -> Auto.h_superauto n l b1 b2
- | TacDAuto (n,p) -> Auto.h_dauto (option_map (interp_int_or_var ist) n,p)
+ | TacDAuto (n,p,lems) ->
+ Auto.h_dauto (Option.map (interp_int_or_var ist) n,p)
+ (pf_interp_constr_list ist gl lems)
(* Derived basic tactics *)
| TacSimpleInduction h ->
h_simple_induction (interp_quantified_hypothesis ist h)
- | TacNewInduction (lc,cbo,ids) ->
- h_new_induction (List.map (interp_induction_arg ist gl) lc)
- (option_map (interp_constr_with_bindings ist gl) cbo)
+ | TacNewInduction (ev,lc,cbo,ids,cls) ->
+ h_new_induction ev (List.map (interp_induction_arg ist gl) lc)
+ (Option.map (interp_constr_with_bindings ist gl) cbo)
(interp_intro_pattern ist gl ids)
+ (Option.map (interp_clause ist gl) cls)
| TacSimpleDestruct h ->
h_simple_destruct (interp_quantified_hypothesis ist h)
- | TacNewDestruct (c,cbo,ids) ->
- h_new_destruct (List.map (interp_induction_arg ist gl) c)
- (option_map (interp_constr_with_bindings ist gl) cbo)
+ | TacNewDestruct (ev,c,cbo,ids,cls) ->
+ h_new_destruct ev (List.map (interp_induction_arg ist gl) c)
+ (Option.map (interp_constr_with_bindings ist gl) cbo)
(interp_intro_pattern ist gl ids)
+ (Option.map (interp_clause ist gl) cls)
| TacDoubleInduction (h1,h2) ->
let h1 = interp_quantified_hypothesis ist h1 in
let h2 = interp_quantified_hypothesis ist h2 in
@@ -2100,25 +2181,31 @@ and interp_atomic ist gl = function
| TacClearBody l -> h_clear_body (interp_hyp_list ist gl l)
| TacMove (dep,id1,id2) ->
h_move dep (interp_hyp ist gl id1) (interp_hyp ist gl id2)
- | TacRename (id1,id2) ->
- h_rename (interp_hyp ist gl id1) (interp_ident ist gl (snd id2))
+ | TacRename l ->
+ h_rename (List.map (fun (id1,id2) ->
+ interp_hyp ist gl id1,
+ interp_fresh_ident ist gl (snd id2)) l)
+ | TacRevert l -> h_revert (interp_hyp_list ist gl l)
(* Constructors *)
- | TacLeft bl -> h_left (interp_bindings ist gl bl)
- | TacRight bl -> h_right (interp_bindings ist gl bl)
- | TacSplit (_,bl) -> h_split (interp_bindings ist gl bl)
- | TacAnyConstructor t ->
- abstract_tactic (TacAnyConstructor t)
- (Tactics.any_constructor (option_map (interp_tactic ist) t))
- | TacConstructor (n,bl) ->
- h_constructor (skip_metaid n) (interp_bindings ist gl bl)
+ | TacLeft (ev,bl) -> h_left ev (interp_bindings ist gl bl)
+ | TacRight (ev,bl) -> h_right ev (interp_bindings ist gl bl)
+ | TacSplit (ev,_,bl) -> h_split ev (interp_bindings ist gl bl)
+ | TacAnyConstructor (ev,t) ->
+ abstract_tactic (TacAnyConstructor (ev,t))
+ (Tactics.any_constructor ev (Option.map (interp_tactic ist) t))
+ | TacConstructor (ev,n,bl) ->
+ h_constructor ev (skip_metaid n) (interp_bindings ist gl bl)
(* Conversion *)
| TacReduce (r,cl) ->
h_reduce (pf_interp_red_expr ist gl r) (interp_clause ist gl cl)
| TacChange (occl,c,cl) ->
- h_change (option_map (pf_interp_pattern ist gl) occl)
- (if occl = None then pf_interp_type ist gl c
+ h_change (Option.map (pf_interp_constr_with_occurrences ist gl) occl)
+ (if occl = None & (cl.onhyps = None or cl.onhyps = Some []) &
+ (cl.concl_occs = all_occurrences_expr or
+ cl.concl_occs = no_occurrences_expr)
+ then pf_interp_type ist gl c
else pf_interp_constr ist gl c)
(interp_clause ist gl cl)
@@ -2128,12 +2215,13 @@ and interp_atomic ist gl = function
| TacTransitivity c -> h_transitivity (pf_interp_constr ist gl c)
(* Equality and inversion *)
- | TacRewrite (b,c,cl) ->
- Equality.general_multi_rewrite b
- (interp_constr_with_bindings ist gl c)
+ | TacRewrite (ev,l,cl,by) ->
+ Equality.general_multi_multi_rewrite ev
+ (List.map (fun (b,m,c) -> (b,m,interp_constr_with_bindings ist gl c)) l)
(interp_clause ist gl cl)
+ (Option.map (interp_tactic ist) by)
| TacInversion (DepInversion (k,c,ids),hyp) ->
- Inv.dinv k (option_map (pf_interp_constr ist gl) c)
+ Inv.dinv k (Option.map (pf_interp_constr ist gl) c)
(interp_intro_pattern ist gl ids)
(interp_declared_or_quantified_hypothesis ist gl hyp)
| TacInversion (NonDepInversion (k,idl,ids),hyp) ->
@@ -2165,7 +2253,8 @@ and interp_atomic ist gl = function
(interp_intro_pattern ist gl (out_gen globwit_intro_pattern x))
| IdentArgType ->
VIntroPattern
- (IntroIdentifier (interp_ident ist gl (out_gen globwit_ident x)))
+ (IntroIdentifier
+ (interp_fresh_ident ist gl (out_gen globwit_ident x)))
| VarArgType ->
mk_hyp_value ist gl (out_gen globwit_var x)
| RefArgType ->
@@ -2181,7 +2270,7 @@ and interp_atomic ist gl = function
| ExtraArgType s when tactic_genarg_level s <> None ->
(* Special treatment of tactic arguments *)
val_interp ist gl
- (out_gen (globwit_tactic (out_some (tactic_genarg_level s))) x)
+ (out_gen (globwit_tactic (Option.get (tactic_genarg_level s))) x)
| List0ArgType ConstrArgType ->
let wit = wit_list0 globwit_constr in
VList (List.map (mk_constr_value ist gl) (out_gen wit x))
@@ -2226,18 +2315,21 @@ let make_empty_glob_sign () =
gsigma = Evd.empty; genv = Global.env() }
(* Initial call for interpretation *)
-let interp_tac_gen lfun debug t gl =
- interp_tactic { lfun=lfun; debug=debug }
+let interp_tac_gen lfun avoid_ids debug t gl =
+ interp_tactic { lfun=lfun; avoid_ids=avoid_ids; debug=debug; last_loc=dloc }
(intern_tactic {
ltacvars = (List.map fst lfun, []); ltacrecvars = [];
gsigma = project gl; genv = pf_env gl } t) gl
-let eval_tactic t gls = interp_tactic { lfun=[]; debug=get_debug() } t gls
+let eval_tactic t gls =
+ interp_tactic { lfun=[]; avoid_ids=[]; debug=get_debug(); last_loc=dloc }
+ t gls
-let interp t = interp_tac_gen [] (get_debug()) t
+let interp t = interp_tac_gen [] [] (get_debug()) t
let eval_ltac_constr gl t =
- interp_ltac_constr { lfun=[]; debug=get_debug() } gl
+ interp_ltac_constr
+ { lfun=[]; avoid_ids=[]; debug=get_debug(); last_loc=dloc } gl
(intern_tactic (make_empty_glob_sign ()) t )
(* Hides interpretation for pretty-print *)
@@ -2276,7 +2368,7 @@ let subst_raw_with_bindings subst (c,bl) =
(subst_rawconstr subst c, subst_bindings subst bl)
let subst_induction_arg subst = function
- | ElimOnConstr c -> ElimOnConstr (subst_rawconstr subst c)
+ | ElimOnConstr c -> ElimOnConstr (subst_raw_with_bindings subst c)
| ElimOnAnonHyp n as x -> x
| ElimOnIdent id as x -> x
@@ -2317,15 +2409,15 @@ let subst_unfold subst (l,e) =
let subst_flag subst red =
{ red with rConst = List.map (subst_evaluable subst) red.rConst }
-let subst_constr_occurrence subst (l,c) = (l,subst_rawconstr subst c)
+let subst_constr_with_occurrences subst (l,c) = (l,subst_rawconstr subst c)
let subst_redexp subst = function
| Unfold l -> Unfold (List.map (subst_unfold subst) l)
| Fold l -> Fold (List.map (subst_rawconstr subst) l)
| Cbv f -> Cbv (subst_flag subst f)
| Lazy f -> Lazy (subst_flag subst f)
- | Pattern l -> Pattern (List.map (subst_constr_occurrence subst) l)
- | Simpl o -> Simpl (option_map (subst_constr_occurrence subst) o)
+ | Pattern l -> Pattern (List.map (subst_constr_with_occurrences subst) l)
+ | Simpl o -> Simpl (Option.map (subst_constr_with_occurrences subst) o)
| (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r
let subst_raw_may_eval subst = function
@@ -2351,27 +2443,27 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
| TacExact c -> TacExact (subst_rawconstr subst c)
| TacExactNoCheck c -> TacExactNoCheck (subst_rawconstr subst c)
| TacVmCastNoCheck c -> TacVmCastNoCheck (subst_rawconstr subst c)
- | TacApply cb -> TacApply (subst_raw_with_bindings subst cb)
- | TacElim (cb,cbo) ->
- TacElim (subst_raw_with_bindings subst cb,
- option_map (subst_raw_with_bindings subst) cbo)
+ | TacApply (a,ev,cb) -> TacApply (a,ev,subst_raw_with_bindings subst cb)
+ | TacElim (ev,cb,cbo) ->
+ TacElim (ev,subst_raw_with_bindings subst cb,
+ Option.map (subst_raw_with_bindings subst) cbo)
| TacElimType c -> TacElimType (subst_rawconstr subst c)
- | TacCase cb -> TacCase (subst_raw_with_bindings subst cb)
+ | TacCase (ev,cb) -> TacCase (ev,subst_raw_with_bindings subst cb)
| TacCaseType c -> TacCaseType (subst_rawconstr subst c)
| TacFix (idopt,n) as x -> x
- | TacMutualFix (id,n,l) ->
- TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_rawconstr subst c)) l)
+ | TacMutualFix (b,id,n,l) ->
+ TacMutualFix(b,id,n,List.map (fun (id,n,c) -> (id,n,subst_rawconstr subst c)) l)
| TacCofix idopt as x -> x
- | TacMutualCofix (id,l) ->
- TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_rawconstr subst c)) l)
+ | TacMutualCofix (b,id,l) ->
+ TacMutualCofix (b,id, List.map (fun (id,c) -> (id,subst_rawconstr subst c)) l)
| TacCut c -> TacCut (subst_rawconstr subst c)
| TacAssert (b,na,c) ->
- TacAssert (option_map (subst_tactic subst) b,na,subst_rawconstr subst c)
- | TacGeneralize cl -> TacGeneralize (List.map (subst_rawconstr subst) cl)
+ TacAssert (Option.map (subst_tactic subst) b,na,subst_rawconstr subst c)
+ | TacGeneralize cl ->
+ TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl)
| TacGeneralizeDep c -> TacGeneralizeDep (subst_rawconstr subst c)
- | TacLetTac (id,c,clp) -> TacLetTac (id,subst_rawconstr subst c,clp)
-(*| TacInstantiate (n,c,ido) -> TacInstantiate (n,subst_rawconstr subst c,ido)
-*)
+ | TacLetTac (id,c,clp,b) -> TacLetTac (id,subst_rawconstr subst c,clp,b)
+
(* Automation tactics *)
| TacTrivial (lems,l) -> TacTrivial (List.map (subst_rawconstr subst) lems,l)
| TacAuto (n,lems,l) -> TacAuto (n,List.map (subst_rawconstr subst) lems,l)
@@ -2379,17 +2471,17 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
| TacDestructHyp (b,id) -> TacDestructHyp(b,id)
| TacDestructConcl -> TacDestructConcl
| TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2)
- | TacDAuto (n,p) -> TacDAuto (n,p)
+ | TacDAuto (n,p,lems) -> TacDAuto (n,p,List.map (subst_rawconstr subst) lems)
(* Derived basic tactics *)
| TacSimpleInduction h as x -> x
- | TacNewInduction (lc,cbo,ids) -> (* Pierre C. est-ce correct? *)
- TacNewInduction (List.map (subst_induction_arg subst) lc,
- option_map (subst_raw_with_bindings subst) cbo, ids)
+ | TacNewInduction (ev,lc,cbo,ids,cls) ->
+ TacNewInduction (ev,List.map (subst_induction_arg subst) lc,
+ Option.map (subst_raw_with_bindings subst) cbo, ids, cls)
| TacSimpleDestruct h as x -> x
- | TacNewDestruct (c,cbo,ids) ->
- TacNewDestruct (List.map (subst_induction_arg subst) c, (* Julien F. est-ce correct? *)
- option_map (subst_raw_with_bindings subst) cbo, ids)
+ | TacNewDestruct (ev,c,cbo,ids,cls) ->
+ TacNewDestruct (ev,List.map (subst_induction_arg subst) c,
+ Option.map (subst_raw_with_bindings subst) cbo, ids, cls)
| TacDoubleInduction (h1,h2) as x -> x
| TacDecomposeAnd c -> TacDecomposeAnd (subst_rawconstr subst c)
| TacDecomposeOr c -> TacDecomposeOr (subst_rawconstr subst c)
@@ -2403,19 +2495,20 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
| TacClear _ as x -> x
| TacClearBody l as x -> x
| TacMove (dep,id1,id2) as x -> x
- | TacRename (id1,id2) as x -> x
+ | TacRename l as x -> x
+ | TacRevert _ as x -> x
(* Constructors *)
- | TacLeft bl -> TacLeft (subst_bindings subst bl)
- | TacRight bl -> TacRight (subst_bindings subst bl)
- | TacSplit (b,bl) -> TacSplit (b,subst_bindings subst bl)
- | TacAnyConstructor t -> TacAnyConstructor (option_map (subst_tactic subst) t)
- | TacConstructor (n,bl) -> TacConstructor (n, subst_bindings subst bl)
+ | TacLeft (ev,bl) -> TacLeft (ev,subst_bindings subst bl)
+ | TacRight (ev,bl) -> TacRight (ev,subst_bindings subst bl)
+ | TacSplit (ev,b,bl) -> TacSplit (ev,b,subst_bindings subst bl)
+ | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (subst_tactic subst) t)
+ | TacConstructor (ev,n,bl) -> TacConstructor (ev,n,subst_bindings subst bl)
(* Conversion *)
| TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl)
| TacChange (occl,c,cl) ->
- TacChange (option_map (subst_constr_occurrence subst) occl,
+ TacChange (Option.map (subst_constr_with_occurrences subst) occl,
subst_rawconstr subst c, cl)
(* Equivalence relations *)
@@ -2423,9 +2516,13 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
| TacTransitivity c -> TacTransitivity (subst_rawconstr subst c)
(* Equality and inversion *)
- | TacRewrite (b,c,cl) -> TacRewrite (b, subst_raw_with_bindings subst c,cl)
+ | TacRewrite (ev,l,cl,by) ->
+ TacRewrite (ev,
+ List.map (fun (b,m,c) ->
+ b,m,subst_raw_with_bindings subst c) l,
+ cl,Option.map (subst_tactic subst) by)
| TacInversion (DepInversion (k,c,l),hyp) ->
- TacInversion (DepInversion (k,option_map (subst_rawconstr subst) c,l),hyp)
+ TacInversion (DepInversion (k,Option.map (subst_rawconstr subst) c,l),hyp)
| TacInversion (NonDepInversion _,_) as x -> x
| TacInversion (InversionUsing (c,cl),hyp) ->
TacInversion (InversionUsing (subst_rawconstr subst c,cl),hyp)
@@ -2440,12 +2537,9 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
and subst_tactic subst (t:glob_tactic_expr) = match t with
| TacAtom (_loc,t) -> TacAtom (dloc, subst_atomic subst t)
| TacFun tacfun -> TacFun (subst_tactic_fun subst tacfun)
- | TacLetRecIn (lrc,u) ->
- let lrc = List.map (fun (n,b) -> (n,subst_tactic_fun subst b)) lrc in
- TacLetRecIn (lrc,(subst_tactic subst u:glob_tactic_expr))
- | TacLetIn (l,u) ->
- let l = List.map (fun (n,c,b) -> (n,option_map (subst_tactic subst) c,subst_tacarg subst b)) l in
- TacLetIn (l,subst_tactic subst u)
+ | TacLetIn (r,l,u) ->
+ let l = List.map (fun (n,b) -> (n,subst_tacarg subst b)) l in
+ TacLetIn (r,l,subst_tactic subst u)
| TacMatchContext (lz,lr,lmr) ->
TacMatchContext(lz,lr, subst_match_rule subst lmr)
| TacMatch (lz,c,lmr) ->
@@ -2453,8 +2547,9 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
| TacId _ | TacFail _ as x -> x
| TacProgress tac -> TacProgress (subst_tactic subst tac:glob_tactic_expr)
| TacAbstract (tac,s) -> TacAbstract (subst_tactic subst tac,s)
- | TacThen (t1,t2) ->
- TacThen (subst_tactic subst t1,subst_tactic subst t2)
+ | TacThen (t1,tf,t2,tl) ->
+ TacThen (subst_tactic subst t1,Array.map (subst_tactic subst) tf,
+ subst_tactic subst t2,Array.map (subst_tactic subst) tl)
| TacThens (t,tl) ->
TacThens (subst_tactic subst t, List.map (subst_tactic subst) tl)
| TacDo (n,tac) -> TacDo (n,subst_tactic subst tac)
@@ -2473,7 +2568,7 @@ and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body)
and subst_tacarg subst = function
| Reference r -> Reference (subst_reference subst r)
| ConstrMayEval c -> ConstrMayEval (subst_raw_may_eval subst c)
- | MetaIdArg (_loc,_) -> assert false
+ | MetaIdArg (_loc,_,_) -> assert false
| TacCall (_loc,f,l) ->
TacCall (_loc, subst_reference subst f, List.map (subst_tacarg subst) l)
| TacExternal (_loc,com,req,la) ->
@@ -2558,27 +2653,46 @@ let bad_tactic_args s =
(* Declaration of the TAC-DEFINITION object *)
let add (kn,td) = mactab := Gmap.add kn td !mactab
+type tacdef_kind = | NewTac of identifier
+ | UpdateTac of ltac_constant
+
let load_md i ((sp,kn),defs) =
let dp,_ = repr_path sp in
let mp,dir,_ = repr_kn kn in
List.iter (fun (id,t) ->
- let sp = Libnames.make_path dp id in
- let kn = Names.make_kn mp dir (label_of_id id) in
- Nametab.push_tactic (Until i) sp kn;
- add (kn,t)) defs
-
+ match id with
+ NewTac id ->
+ let sp = Libnames.make_path dp id in
+ let kn = Names.make_kn mp dir (label_of_id id) in
+ Nametab.push_tactic (Until i) sp kn;
+ add (kn,t)
+ | UpdateTac kn ->
+ mactab := Gmap.remove kn !mactab;
+ add (kn,t)) defs
+
let open_md i((sp,kn),defs) =
let dp,_ = repr_path sp in
let mp,dir,_ = repr_kn kn in
List.iter (fun (id,t) ->
- let sp = Libnames.make_path dp id in
- let kn = Names.make_kn mp dir (label_of_id id) in
- Nametab.push_tactic (Exactly i) sp kn) defs
+ match id with
+ NewTac id ->
+ let sp = Libnames.make_path dp id in
+ let kn = Names.make_kn mp dir (label_of_id id) in
+ Nametab.push_tactic (Exactly i) sp kn
+ | UpdateTac kn ->
+ let (path, id) = decode_kn kn in
+ let sp = Libnames.make_path path id in
+ Nametab.push_tactic (Exactly i) sp kn) defs
let cache_md x = load_md 1 x
+let subst_kind subst id =
+ match id with
+ | NewTac _ -> id
+ | UpdateTac kn -> UpdateTac (Mod_subst.subst_kn subst kn)
+
let subst_md (_,subst,defs) =
- List.map (fun (id,t) -> (id,subst_tactic subst t)) defs
+ List.map (fun (id,t) -> (subst_kind subst id,subst_tactic subst t)) defs
let (inMD,outMD) =
declare_object {(default_object "TAC-DEFINITION") with
@@ -2600,28 +2714,61 @@ let print_ltac id =
errorlabstrm "print_ltac"
(pr_qualid id ++ spc() ++ str "is not a user defined tactic")
+open Libnames
+
(* Adds a definition for tactics in the table *)
-let make_absolute_name (loc,id) =
- let kn = Lib.make_kn id in
- if Gmap.mem kn !mactab or is_atomic_kn kn then
+let make_absolute_name ident repl =
+ let loc = loc_of_reference ident in
+ try
+ let id, kn =
+ if repl then None, Nametab.locate_tactic (snd (qualid_of_reference ident))
+ else let id = Pcoq.coerce_global_to_id ident in
+ Some id, Lib.make_kn id
+ in
+ if Gmap.mem kn !mactab then
+ if repl then id, kn
+ else
+ user_err_loc (loc,"Tacinterp.add_tacdef",
+ str "There is already an Ltac named " ++ pr_reference ident)
+ else if is_atomic_kn kn then
+ user_err_loc (loc,"Tacinterp.add_tacdef",
+ str "Reserved Ltac name " ++ pr_reference ident)
+ else id, kn
+ with Not_found ->
user_err_loc (loc,"Tacinterp.add_tacdef",
- str "There is already an Ltac named " ++ pr_id id);
- kn
-
+ str "There is no Ltac named " ++ pr_reference ident)
+
+let rec filter_map f l =
+ let rec aux acc = function
+ [] -> acc
+ | hd :: tl ->
+ match f hd with
+ Some x -> aux (x :: acc) tl
+ | None -> aux acc tl
+ in aux [] l
+
let add_tacdef isrec tacl =
-(* let isrec = if !Options.p1 then isrec else true in*)
- let rfun = List.map (fun ((loc,id as locid),_) -> (id,make_absolute_name locid)) tacl in
+ let rfun = List.map (fun (ident, b, _) -> make_absolute_name ident b) tacl in
let ist =
- {(make_empty_glob_sign()) with ltacrecvars = if isrec then rfun else []} in
+ {(make_empty_glob_sign()) with ltacrecvars =
+ if isrec then filter_map
+ (function (Some id, qid) -> Some (id, qid) | (None, _) -> None) rfun
+ else []} in
let gtacl =
- List.map (fun ((_,id),def) ->
- (id,Options.with_option strict_check (intern_tactic ist) def))
- tacl in
+ List.map2 (fun (_,b,def) (id, qid) ->
+ let k = if b then UpdateTac qid else NewTac (Option.get id) in
+ let t = Flags.with_option strict_check (intern_tactic ist) def in
+ (k, t))
+ tacl rfun in
let id0 = fst (List.hd rfun) in
- let _ = Lib.add_leaf id0 (inMD gtacl) in
+ let _ = match id0 with Some id0 -> ignore(Lib.add_leaf id0 (inMD gtacl))
+ | _ -> Lib.add_anonymous_leaf (inMD gtacl) in
List.iter
- (fun (id,_) -> Options.if_verbose msgnl (pr_id id ++ str " is defined"))
- rfun
+ (fun (id,b,_) ->
+ Flags.if_verbose msgnl (Libnames.pr_reference id ++
+ (if b then str " is redefined"
+ else str " is defined")))
+ tacl
(***************************************************************************)
(* Other entry points *)
@@ -2629,13 +2776,13 @@ let add_tacdef isrec tacl =
let glob_tactic x = intern_tactic (make_empty_glob_sign ()) x
let glob_tactic_env l env x =
- Options.with_option strict_check
+ Flags.with_option strict_check
(intern_tactic
{ ltacvars = (l,[]); ltacrecvars = []; gsigma = Evd.empty; genv = env })
x
let interp_redexp env sigma r =
- let ist = { lfun=[]; debug=get_debug () } in
+ let ist = { lfun=[]; avoid_ids=[]; debug=get_debug (); last_loc=dloc } in
let gist = {(make_empty_glob_sign ()) with genv = env; gsigma = sigma } in
interp_red_expr ist sigma env (intern_red_expr gist r)
@@ -2645,10 +2792,10 @@ let interp_redexp env sigma r =
let _ = Auto.set_extern_interp
(fun l ->
let l = List.map (fun (id,c) -> (id,VConstr c)) l in
- interp_tactic {lfun=l;debug=get_debug()})
+ interp_tactic {lfun=l;avoid_ids=[];debug=get_debug(); last_loc=dloc})
let _ = Auto.set_extern_intern_tac
(fun l ->
- Options.with_option strict_check
+ Flags.with_option strict_check
(intern_tactic {(make_empty_glob_sign()) with ltacvars=(l,[])}))
let _ = Auto.set_extern_subst_tactic subst_tactic
let _ = Dhyp.set_extern_interp eval_tactic
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-02 14:11:07 +0000