1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: tacinterp.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
48
open Pretyping.Default
54
(str "bug in the debugger: " ++
55
str "an exception is raised while printing debug information")
57
let error_syntactic_metavariables_not_allowed loc =
60
str "Syntactic metavariables allowed only in quotations.")
62
let error_global_not_found_loc (loc,qid) = error_global_not_found_loc loc qid
64
let skip_metaid = function
66
| MetaId (loc,_) -> error_syntactic_metavariables_not_allowed loc
69
| LtacFun of ltac_type
73
(* Values for interpretation *)
75
| VRTactic of (goal list sigma * validation) (* For Match results *)
76
(* Not a true value *)
77
| VFun of ltac_trace * (identifier*value) list *
78
identifier option list * glob_tactic_expr
81
| VIntroPattern of intro_pattern_expr (* includes idents which are not *)
82
(* bound as in "Intro H" but which may be bound *)
83
(* later, as in "tac" in "Intro H; tac" *)
84
| VConstr of constr (* includes idents known to be bound and references *)
85
| VConstr_context of constr
87
| VRec of (identifier*value) list ref * glob_tactic_expr
91
let catch_error call_trace tac g =
92
if call_trace = [] then tac g else try tac g with
93
| LtacLocated _ as e -> raise e
94
| Stdpp.Exc_located (_,LtacLocated _) as e -> raise e
96
let (loc',c),tail = list_sep_last call_trace in
97
let loc,e' = match e with Stdpp.Exc_located(loc,e) -> loc,e | _ ->dloc,e in
99
let loc = if loc = dloc then loc' else loc in
100
raise (Stdpp.Exc_located(loc,e'))
102
raise (Stdpp.Exc_located(loc',LtacLocated((c,tail,loc),e')))
104
(* Signature for interpretation: val_interp and interpretation functions *)
106
{ lfun : (identifier * value) list;
107
avoid_ids : identifier list; (* ids inherited from the call context
108
(needed to get fresh ids) *)
112
let check_is_value = function
113
| VRTactic _ -> (* These are goals produced by Match *)
114
error "Immediate match producing tactics not allowed in local definitions."
117
(* For tactic_of_value *)
120
(* Gives the constr corresponding to a Constr_context tactic_arg *)
121
let constr_of_VConstr_context = function
122
| VConstr_context c -> c
124
errorlabstrm "constr_of_VConstr_context" (str "Not a context variable.")
126
(* Displays a value *)
127
let rec pr_value env = function
129
| VInteger n -> int n
130
| VIntroPattern ipat -> pr_intro_pattern (dloc,ipat)
131
| VConstr c | VConstr_context c ->
132
(match env with Some env -> pr_lconstr_env env c | _ -> str "a term")
133
| (VRTactic _ | VFun _ | VRec _) -> str "a tactic"
134
| VList [] -> str "an empty list"
136
str "a list (first element is " ++ pr_value env a ++ str")"
138
(* Transforms an id into a constr if possible, or fails *)
139
let constr_of_id env id =
140
construct_reference (Environ.named_context env) id
142
(* To embed tactics *)
143
let ((tactic_in : (interp_sign -> glob_tactic_expr) -> Dyn.t),
144
(tactic_out : Dyn.t -> (interp_sign -> glob_tactic_expr))) =
147
let ((value_in : value -> Dyn.t),
148
(value_out : Dyn.t -> value)) = create "value"
150
let valueIn t = TacDynamic (dummy_loc,value_in t)
151
let valueOut = function
152
| TacDynamic (_,d) ->
153
if (tag d) = "value" then
156
anomalylabstrm "valueOut" (str "Dynamic tag should be value")
158
anomalylabstrm "valueOut" (str "Not a Dynamic ast: ")
160
(* To embed constr *)
161
let constrIn t = CDynamic (dummy_loc,constr_in t)
162
let constrOut = function
164
if (Dyn.tag d) = "constr" then
167
anomalylabstrm "constrOut" (str "Dynamic tag should be constr")
169
anomalylabstrm "constrOut" (str "Not a Dynamic ast")
171
(* Globalizes the identifier *)
172
let find_reference env qid =
173
(* We first look for a variable of the current proof *)
174
match repr_qualid qid with
175
| (d,id) when repr_dirpath d = [] & List.mem id (ids_of_context env)
177
| _ -> Nametab.locate qid
179
let error_not_evaluable s =
180
errorlabstrm "evalref_of_ref"
181
(str "Cannot coerce" ++ spc () ++ s ++ spc () ++
182
str "to an evaluable reference.")
184
(* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
185
let atomic_mactab = ref Idmap.empty
186
let add_primitive_tactic s tac =
187
let id = id_of_string s in
188
atomic_mactab := Idmap.add id tac !atomic_mactab
191
let nocl = {onhyps=Some[];concl_occs=all_occurrences_expr} in
193
(fun (s,t) -> add_primitive_tactic s (TacAtom(dloc,t)))
194
[ "red", TacReduce(Red false,nocl);
195
"hnf", TacReduce(Hnf,nocl);
196
"simpl", TacReduce(Simpl None,nocl);
197
"compute", TacReduce(Cbv all_flags,nocl);
198
"intro", TacIntroMove(None,no_move);
199
"intros", TacIntroPattern [];
200
"assumption", TacAssumption;
201
"cofix", TacCofix None;
202
"trivial", TacTrivial ([],None);
203
"auto", TacAuto(None,[],None);
204
"left", TacLeft(false,NoBindings);
205
"eleft", TacLeft(true,NoBindings);
206
"right", TacRight(false,NoBindings);
207
"eright", TacRight(true,NoBindings);
208
"split", TacSplit(false,false,NoBindings);
209
"esplit", TacSplit(true,false,NoBindings);
210
"constructor", TacAnyConstructor (false,None);
211
"econstructor", TacAnyConstructor (true,None);
212
"reflexivity", TacReflexivity;
213
"symmetry", TacSymmetry nocl
216
(fun (s,t) -> add_primitive_tactic s t)
218
"fail", TacFail(ArgArg 0,[]);
219
"fresh", TacArg(TacFreshId [])
222
let lookup_atomic id = Idmap.find id !atomic_mactab
223
let is_atomic_kn kn =
224
let (_,_,l) = repr_kn kn in
225
Idmap.mem (id_of_label l) !atomic_mactab
227
(* Summary and Object declaration *)
228
let mactab = ref Gmap.empty
230
let lookup r = Gmap.find r !mactab
233
let init () = mactab := Gmap.empty in
234
let freeze () = !mactab in
235
let unfreeze fs = mactab := fs in
236
Summary.declare_summary "tactic-definition"
237
{ Summary.freeze_function = freeze;
238
Summary.unfreeze_function = unfreeze;
239
Summary.init_function = init;
240
Summary.survive_module = false;
241
Summary.survive_section = false }
243
(* Tactics table (TacExtend). *)
245
let tac_tab = Hashtbl.create 17
248
if Hashtbl.mem tac_tab s then
249
errorlabstrm ("Refiner.add_tactic: ")
250
(str ("Cannot redeclare tactic "^s^"."));
251
Hashtbl.add tac_tab s t
253
let overwriting_add_tactic s t =
254
if Hashtbl.mem tac_tab s then begin
255
Hashtbl.remove tac_tab s;
256
warning ("Overwriting definition of tactic "^s)
258
Hashtbl.add tac_tab s t
260
let lookup_tactic s =
262
Hashtbl.find tac_tab s
264
errorlabstrm "Refiner.lookup_tactic"
265
(str"The tactic " ++ str s ++ str" is not installed.")
267
let vernac_tactic (s,args) =
268
let tacfun = lookup_tactic s args in
269
abstract_extended_tactic s args tacfun
271
(* Interpretation of extra generic arguments *)
273
ltacvars : identifier list * identifier list;
274
(* ltac variables and the subset of vars introduced by Intro/Let/... *)
275
ltacrecvars : (identifier * ltac_constant) list;
276
(* ltac recursive names *)
277
gsigma : Evd.evar_map;
280
type interp_genarg_type =
281
(glob_sign -> raw_generic_argument -> glob_generic_argument) *
282
(interp_sign -> goal sigma -> glob_generic_argument ->
283
typed_generic_argument) *
284
(substitution -> glob_generic_argument -> glob_generic_argument)
287
ref (Gmap.empty : (string,interp_genarg_type) Gmap.t)
288
let add_interp_genarg id f =
289
extragenargtab := Gmap.add id f !extragenargtab
290
let lookup_genarg id =
291
try Gmap.find id !extragenargtab
292
with Not_found -> failwith ("No interpretation function found for entry "^id)
294
let lookup_genarg_glob id = let (f,_,_) = lookup_genarg id in f
295
let lookup_interp_genarg id = let (_,f,_) = lookup_genarg id in f
296
let lookup_genarg_subst id = let (_,_,f) = lookup_genarg id in f
298
let propagate_trace ist loc id = function
299
| VFun (_,lfun,it,b) ->
300
let t = if it=[] then b else TacFun (it,b) in
301
VFun ((loc,LtacVarCall (id,t))::ist.trace,lfun,it,b)
304
(* Dynamically check that an argument is a tactic *)
305
let coerce_to_tactic loc id = function
306
| VFun _ | VRTactic _ as a -> a
308
(loc, "", str "Variable " ++ pr_id id ++ str " should be bound to a tactic.")
314
(* We have identifier <| global_reference <| constr *)
316
let find_ident id sign =
317
List.mem id (fst sign.ltacvars) or
318
List.mem id (ids_of_named_context (Environ.named_context sign.genv))
320
let find_recvar qid sign = List.assoc qid sign.ltacrecvars
322
(* a "var" is a ltac var or a var introduced by an intro tactic *)
323
let find_var id sign = List.mem id (fst sign.ltacvars)
325
(* a "ctxvar" is a var introduced by an intro tactic (Intro/LetTac/...) *)
326
let find_ctxvar id sign = List.mem id (snd sign.ltacvars)
328
(* a "ltacvar" is an ltac var (Let-In/Fun/...) *)
329
let find_ltacvar id sign = find_var id sign & not (find_ctxvar id sign)
331
let find_hyp id sign =
332
List.mem id (ids_of_named_context (Environ.named_context sign.genv))
334
(* Globalize a name introduced by Intro/LetTac/... ; it is allowed to *)
335
(* be fresh in which case it is binding later on *)
336
let intern_ident l ist id =
337
(* We use identifier both for variables and new names; thus nothing to do *)
338
if not (find_ident id ist) then l:=(id::fst !l,id::snd !l);
341
let intern_name l ist = function
342
| Anonymous -> Anonymous
343
| Name id -> Name (intern_ident l ist id)
345
let vars_of_ist (lfun,_,_,env) =
346
List.fold_left (fun s id -> Idset.add id s)
347
(vars_of_env env) lfun
349
let get_current_context () =
350
try Pfedit.get_current_goal_context ()
351
with e when Logic.catchable_exception e ->
352
(Evd.empty, Global.env())
354
let strict_check = ref false
356
let adjust_loc loc = if !strict_check then dloc else loc
358
(* Globalize a name which must be bound -- actually just check it is bound *)
359
let intern_hyp ist (loc,id as locid) =
360
if not !strict_check then
362
else if find_ident id ist then
365
Pretype_errors.error_var_not_found_loc loc id
367
let intern_hyp_or_metaid ist id = intern_hyp ist (skip_metaid id)
369
let intern_or_var ist = function
370
| ArgVar locid -> ArgVar (intern_hyp ist locid)
373
let loc_of_by_notation f = function
375
| ByNotation (loc,s,_) -> loc
377
let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef"
379
let intern_inductive_or_by_notation = function
380
| AN r -> Nametab.inductive_of_reference r
381
| ByNotation (loc,ntn,sc) ->
382
destIndRef (Notation.interp_notation_as_global_reference loc
383
(function IndRef ind -> true | _ -> false) ntn sc)
385
let intern_inductive ist = function
386
| AN (Ident (loc,id)) when find_var id ist -> ArgVar (loc,id)
387
| r -> ArgArg (intern_inductive_or_by_notation r)
389
let intern_global_reference ist = function
390
| Ident (loc,id) when find_var id ist -> ArgVar (loc,id)
392
let loc,_ as lqid = qualid_of_reference r in
393
try ArgArg (loc,locate_global_with_alias lqid)
395
error_global_not_found_loc lqid
397
let intern_ltac_variable ist = function
399
if find_ltacvar id ist then
400
(* A local variable of any type *)
403
(* A recursive variable *)
404
ArgArg (loc,find_recvar id ist)
408
let intern_constr_reference strict ist = function
409
| Ident (_,id) when (not strict & find_hyp id ist) or find_ctxvar id ist ->
412
let loc,_ as lqid = qualid_of_reference r in
413
RRef (loc,locate_global_with_alias lqid), if strict then None else Some (CRef r)
415
let intern_move_location ist = function
416
| MoveAfter id -> MoveAfter (intern_hyp_or_metaid ist id)
417
| MoveBefore id -> MoveBefore (intern_hyp_or_metaid ist id)
418
| MoveToEnd toleft as x -> x
420
(* Internalize an isolated reference in position of tactic *)
422
let intern_isolated_global_tactic_reference r =
423
let (loc,qid) = qualid_of_reference r in
424
try TacCall (loc,ArgArg (loc,locate_tactic qid),[])
427
| Ident (_,id) -> Tacexp (lookup_atomic id)
428
| _ -> raise Not_found
430
let intern_isolated_tactic_reference strict ist r =
431
(* An ltac reference *)
432
try Reference (intern_ltac_variable ist r)
434
(* A global tactic *)
435
try intern_isolated_global_tactic_reference r
437
(* Tolerance for compatibility, allow not to use "constr:" *)
438
try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
440
(* Reference not found *)
441
error_global_not_found_loc (qualid_of_reference r)
443
(* Internalize an applied tactic reference *)
445
let intern_applied_global_tactic_reference r =
446
let (loc,qid) = qualid_of_reference r in
447
ArgArg (loc,locate_tactic qid)
449
let intern_applied_tactic_reference ist r =
450
(* An ltac reference *)
451
try intern_ltac_variable ist r
453
(* A global tactic *)
454
try intern_applied_global_tactic_reference r
456
(* Reference not found *)
457
error_global_not_found_loc (qualid_of_reference r)
459
(* Intern a reference parsed in a non-tactic entry *)
461
let intern_non_tactic_reference strict ist r =
462
(* An ltac reference *)
463
try Reference (intern_ltac_variable ist r)
465
(* A constr reference *)
466
try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
468
(* Tolerance for compatibility, allow not to use "ltac:" *)
469
try intern_isolated_global_tactic_reference r
471
(* By convention, use IntroIdentifier for unbound ident, when not in a def *)
473
| Ident (loc,id) when not strict -> IntroPattern (loc,IntroIdentifier id)
475
(* Reference not found *)
476
error_global_not_found_loc (qualid_of_reference r)
478
let intern_message_token ist = function
479
| (MsgString _ | MsgInt _ as x) -> x
480
| MsgIdent id -> MsgIdent (intern_hyp_or_metaid ist id)
482
let intern_message ist = List.map (intern_message_token ist)
484
let rec intern_intro_pattern lf ist = function
485
| loc, IntroOrAndPattern l ->
486
loc, IntroOrAndPattern (intern_or_and_intro_pattern lf ist l)
487
| loc, IntroIdentifier id ->
488
loc, IntroIdentifier (intern_ident lf ist id)
489
| loc, (IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _)
492
and intern_or_and_intro_pattern lf ist =
493
List.map (List.map (intern_intro_pattern lf ist))
495
let intern_quantified_hypothesis ist = function
496
| AnonHyp n -> AnonHyp n
498
(* Uncomment to disallow "intros until n" in ltac when n is not bound *)
499
NamedHyp ((*snd (intern_hyp ist (dloc,*)id(* ))*))
501
let intern_binding_name ist x =
502
(* We use identifier both for variables and binding names *)
503
(* Todo: consider the body of the lemma to which the binding refer
504
and if a term w/o ltac vars, check the name is indeed quantified *)
507
let intern_constr_gen isarity {ltacvars=lfun; gsigma=sigma; genv=env} c =
508
let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in
510
warn (Constrintern.intern_gen isarity ~ltacvars:(fst lfun,[]) sigma env) c
512
(c',if !strict_check then None else Some c)
514
let intern_constr = intern_constr_gen false
515
let intern_type = intern_constr_gen true
517
(* Globalize bindings *)
518
let intern_binding ist (loc,b,c) =
519
(loc,intern_binding_name ist b,intern_constr ist c)
521
let intern_bindings ist = function
522
| NoBindings -> NoBindings
523
| ImplicitBindings l -> ImplicitBindings (List.map (intern_constr ist) l)
524
| ExplicitBindings l -> ExplicitBindings (List.map (intern_binding ist) l)
526
let intern_constr_with_bindings ist (c,bl) =
527
(intern_constr ist c, intern_bindings ist bl)
529
let intern_clause_pattern ist (l,occl) =
530
let rec check = function
531
| (hyp,l) :: rest -> (intern_hyp ist (skip_metaid hyp),l)::(check rest)
535
(* TODO: catch ltac vars *)
536
let intern_induction_arg ist = function
537
| ElimOnConstr c -> ElimOnConstr (intern_constr_with_bindings ist c)
538
| ElimOnAnonHyp n as x -> x
539
| ElimOnIdent (loc,id) ->
540
if !strict_check then
541
(* If in a defined tactic, no intros-until *)
542
match intern_constr ist (CRef (Ident (dloc,id))) with
543
| RVar (loc,id),_ -> ElimOnIdent (loc,id)
544
| c -> ElimOnConstr (c,NoBindings)
548
let evaluable_of_global_reference = function
549
| ConstRef c -> EvalConstRef c
550
| VarRef c -> EvalVarRef c
551
| r -> error_not_evaluable (pr_global r)
553
let short_name = function
554
| AN (Ident (loc,id)) when not !strict_check -> Some (loc,id)
557
let interp_global_reference r =
558
let lqid = qualid_of_reference r in
559
try locate_global_with_alias lqid
562
| Ident (loc,id) when not !strict_check -> VarRef id
563
| _ -> error_global_not_found_loc lqid
565
let intern_evaluable_reference_or_by_notation = function
566
| AN r -> evaluable_of_global_reference (interp_global_reference r)
567
| ByNotation (loc,ntn,sc) ->
568
evaluable_of_global_reference
569
(Notation.interp_notation_as_global_reference loc
570
(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)
572
(* Globalizes a reduction expression *)
573
let intern_evaluable ist = function
574
| AN (Ident (loc,id)) when find_ltacvar id ist -> ArgVar (loc,id)
575
| AN (Ident (_,id)) when
576
(not !strict_check & find_hyp id ist) or find_ctxvar id ist ->
577
ArgArg (EvalVarRef id, None)
579
let e = intern_evaluable_reference_or_by_notation r in
580
let na = short_name r in
583
let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid)
585
let intern_flag ist red =
586
{ red with rConst = List.map (intern_evaluable ist) red.rConst }
588
let intern_constr_with_occurrences ist (l,c) = (l,intern_constr ist c)
590
let intern_red_expr ist = function
591
| Unfold l -> Unfold (List.map (intern_unfold ist) l)
592
| Fold l -> Fold (List.map (intern_constr ist) l)
593
| Cbv f -> Cbv (intern_flag ist f)
594
| Lazy f -> Lazy (intern_flag ist f)
595
| Pattern l -> Pattern (List.map (intern_constr_with_occurrences ist) l)
596
| Simpl o -> Simpl (Option.map (intern_constr_with_occurrences ist) o)
597
| (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r ) -> r
599
let intern_in_hyp_as ist lf (id,ipat) =
600
(intern_hyp_or_metaid ist id, Option.map (intern_intro_pattern lf ist) ipat)
602
let intern_hyp_list ist = List.map (intern_hyp_or_metaid ist)
604
let intern_inversion_strength lf ist = function
605
| NonDepInversion (k,idl,ids) ->
606
NonDepInversion (k,intern_hyp_list ist idl,
607
Option.map (intern_intro_pattern lf ist) ids)
608
| DepInversion (k,copt,ids) ->
609
DepInversion (k, Option.map (intern_constr ist) copt,
610
Option.map (intern_intro_pattern lf ist) ids)
611
| InversionUsing (c,idl) ->
612
InversionUsing (intern_constr ist c, intern_hyp_list ist idl)
614
(* Interprets an hypothesis name *)
615
let intern_hyp_location ist (((b,occs),id),hl) =
616
(((b,List.map (intern_or_var ist) occs),intern_hyp_or_metaid ist id), hl)
618
(* Reads a pattern *)
619
let intern_pattern sigma env ?(as_type=false) lfun = function
620
| Subterm (b,ido,pc) ->
621
let ltacvars = (lfun,[]) in
622
let (metas,pat) = intern_constr_pattern sigma env ~ltacvars pc in
623
ido, metas, Subterm (b,ido,pat)
625
let ltacvars = (lfun,[]) in
626
let (metas,pat) = intern_constr_pattern sigma env ~as_type ~ltacvars pc in
627
None, metas, Term pat
629
let intern_constr_may_eval ist = function
630
| ConstrEval (r,c) -> ConstrEval (intern_red_expr ist r,intern_constr ist c)
631
| ConstrContext (locid,c) ->
632
ConstrContext (intern_hyp ist locid,intern_constr ist c)
633
| ConstrTypeOf c -> ConstrTypeOf (intern_constr ist c)
634
| ConstrTerm c -> ConstrTerm (intern_constr ist c)
636
(* External tactics *)
637
let print_xml_term = ref (fun _ -> failwith "print_xml_term unset")
638
let declare_xml_printer f = print_xml_term := f
640
let internalise_tacarg ch = G_xml.parse_tactic_arg ch
642
let extern_tacarg ch env sigma = function
643
| VConstr c -> !print_xml_term ch env sigma c
644
| VRTactic _ | VFun _ | VVoid | VInteger _ | VConstr_context _
645
| VIntroPattern _ | VRec _ | VList _ ->
646
error "Only externing of terms is implemented."
648
let extern_request ch req gl la =
649
output_string ch "<REQUEST req=\""; output_string ch req;
650
output_string ch "\">\n";
651
List.iter (pf_apply (extern_tacarg ch) gl) la;
652
output_string ch "</REQUEST>\n"
654
(* Reads the hypotheses of a "match goal" rule *)
655
let rec intern_match_goal_hyps sigma env lfun = function
656
| (Hyp ((_,na) as locna,mp))::tl ->
657
let ido, metas1, pat = intern_pattern sigma env ~as_type:true lfun mp in
658
let lfun, metas2, hyps = intern_match_goal_hyps sigma env lfun tl in
659
let lfun' = name_cons na (Option.List.cons ido lfun) in
660
lfun', metas1@metas2, Hyp (locna,pat)::hyps
661
| (Def ((_,na) as locna,mv,mp))::tl ->
662
let ido, metas1, patv = intern_pattern sigma env ~as_type:false lfun mv in
663
let ido', metas2, patt = intern_pattern sigma env ~as_type:true lfun mp in
664
let lfun, metas3, hyps = intern_match_goal_hyps sigma env lfun tl in
665
let lfun' = name_cons na (Option.List.cons ido' (Option.List.cons ido lfun)) in
666
lfun', metas1@metas2@metas3, Def (locna,patv,patt)::hyps
670
let extract_let_names lrc =
672
(fun ((loc,name),_) l ->
673
if List.mem name l then
675
(loc, "glob_tactic", str "This variable is bound several times.");
679
let clause_app f = function
680
{ onhyps=None; concl_occs=nl } ->
681
{ onhyps=None; concl_occs=nl }
682
| { onhyps=Some l; concl_occs=nl } ->
683
{ onhyps=Some(List.map f l); concl_occs=nl}
685
(* Globalizes tactics : raw_tactic_expr -> glob_tactic_expr *)
686
let rec intern_atomic lf ist x =
687
match (x:raw_atomic_tactic_expr) with
689
| TacIntroPattern l ->
690
TacIntroPattern (List.map (intern_intro_pattern lf ist) l)
691
| TacIntrosUntil hyp -> TacIntrosUntil (intern_quantified_hypothesis ist hyp)
692
| TacIntroMove (ido,hto) ->
693
TacIntroMove (Option.map (intern_ident lf ist) ido,
694
intern_move_location ist hto)
695
| TacAssumption -> TacAssumption
696
| TacExact c -> TacExact (intern_constr ist c)
697
| TacExactNoCheck c -> TacExactNoCheck (intern_constr ist c)
698
| TacVmCastNoCheck c -> TacVmCastNoCheck (intern_constr ist c)
699
| TacApply (a,ev,cb,inhyp) ->
700
TacApply (a,ev,List.map (intern_constr_with_bindings ist) cb,
701
Option.map (intern_in_hyp_as ist lf) inhyp)
702
| TacElim (ev,cb,cbo) ->
703
TacElim (ev,intern_constr_with_bindings ist cb,
704
Option.map (intern_constr_with_bindings ist) cbo)
705
| TacElimType c -> TacElimType (intern_type ist c)
706
| TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings ist cb)
707
| TacCaseType c -> TacCaseType (intern_type ist c)
708
| TacFix (idopt,n) -> TacFix (Option.map (intern_ident lf ist) idopt,n)
709
| TacMutualFix (b,id,n,l) ->
710
let f (id,n,c) = (intern_ident lf ist id,n,intern_type ist c) in
711
TacMutualFix (b,intern_ident lf ist id, n, List.map f l)
712
| TacCofix idopt -> TacCofix (Option.map (intern_ident lf ist) idopt)
713
| TacMutualCofix (b,id,l) ->
714
let f (id,c) = (intern_ident lf ist id,intern_type ist c) in
715
TacMutualCofix (b,intern_ident lf ist id, List.map f l)
716
| TacCut c -> TacCut (intern_type ist c)
717
| TacAssert (otac,ipat,c) ->
718
TacAssert (Option.map (intern_tactic ist) otac,
719
Option.map (intern_intro_pattern lf ist) ipat,
720
intern_constr_gen (otac<>None) ist c)
721
| TacGeneralize cl ->
722
TacGeneralize (List.map (fun (c,na) ->
723
intern_constr_with_occurrences ist c,
724
intern_name lf ist na) cl)
725
| TacGeneralizeDep c -> TacGeneralizeDep (intern_constr ist c)
726
| TacLetTac (na,c,cls,b) ->
727
let na = intern_name lf ist na in
728
TacLetTac (na,intern_constr ist c,
729
(clause_app (intern_hyp_location ist) cls),b)
731
(* Automation tactics *)
732
| TacTrivial (lems,l) -> TacTrivial (List.map (intern_constr ist) lems,l)
733
| TacAuto (n,lems,l) ->
734
TacAuto (Option.map (intern_or_var ist) n,
735
List.map (intern_constr ist) lems,l)
736
| TacAutoTDB n -> TacAutoTDB n
737
| TacDestructHyp (b,id) -> TacDestructHyp(b,intern_hyp ist id)
738
| TacDestructConcl -> TacDestructConcl
739
| TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2)
740
| TacDAuto (n,p,lems) ->
741
TacDAuto (Option.map (intern_or_var ist) n,p,
742
List.map (intern_constr ist) lems)
744
(* Derived basic tactics *)
745
| TacSimpleInductionDestruct (isrec,h) ->
746
TacSimpleInductionDestruct (isrec,intern_quantified_hypothesis ist h)
747
| TacInductionDestruct (ev,isrec,l) ->
748
TacInductionDestruct (ev,isrec,List.map (fun (lc,cbo,(ipato,ipats),cls) ->
749
(List.map (intern_induction_arg ist) lc,
750
Option.map (intern_constr_with_bindings ist) cbo,
751
(Option.map (intern_intro_pattern lf ist) ipato,
752
Option.map (intern_intro_pattern lf ist) ipats),
753
Option.map (clause_app (intern_hyp_location ist)) cls)) l)
754
| TacDoubleInduction (h1,h2) ->
755
let h1 = intern_quantified_hypothesis ist h1 in
756
let h2 = intern_quantified_hypothesis ist h2 in
757
TacDoubleInduction (h1,h2)
758
| TacDecomposeAnd c -> TacDecomposeAnd (intern_constr ist c)
759
| TacDecomposeOr c -> TacDecomposeOr (intern_constr ist c)
760
| TacDecompose (l,c) -> let l = List.map (intern_inductive ist) l in
761
TacDecompose (l,intern_constr ist c)
762
| TacSpecialize (n,l) -> TacSpecialize (n,intern_constr_with_bindings ist l)
763
| TacLApply c -> TacLApply (intern_constr ist c)
765
(* Context management *)
766
| TacClear (b,l) -> TacClear (b,List.map (intern_hyp_or_metaid ist) l)
767
| TacClearBody l -> TacClearBody (List.map (intern_hyp_or_metaid ist) l)
768
| TacMove (dep,id1,id2) ->
769
TacMove (dep,intern_hyp_or_metaid ist id1,intern_move_location ist id2)
771
TacRename (List.map (fun (id1,id2) ->
772
intern_hyp_or_metaid ist id1,
773
intern_hyp_or_metaid ist id2) l)
774
| TacRevert l -> TacRevert (List.map (intern_hyp_or_metaid ist) l)
777
| TacLeft (ev,bl) -> TacLeft (ev,intern_bindings ist bl)
778
| TacRight (ev,bl) -> TacRight (ev,intern_bindings ist bl)
779
| TacSplit (ev,b,bl) -> TacSplit (ev,b,intern_bindings ist bl)
780
| TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (intern_tactic ist) t)
781
| TacConstructor (ev,n,bl) -> TacConstructor (ev,n,intern_bindings ist bl)
784
| TacReduce (r,cl) ->
785
TacReduce (intern_red_expr ist r, clause_app (intern_hyp_location ist) cl)
786
| TacChange (occl,c,cl) ->
787
TacChange (Option.map (intern_constr_with_occurrences ist) occl,
788
(if occl = None & (cl.onhyps = None or cl.onhyps = Some []) &
789
(cl.concl_occs = all_occurrences_expr or
790
cl.concl_occs = no_occurrences_expr)
791
then intern_type ist c else intern_constr ist c),
792
clause_app (intern_hyp_location ist) cl)
794
(* Equivalence relations *)
795
| TacReflexivity -> TacReflexivity
796
| TacSymmetry idopt ->
797
TacSymmetry (clause_app (intern_hyp_location ist) idopt)
798
| TacTransitivity c -> TacTransitivity (intern_constr ist c)
800
(* Equality and inversion *)
801
| TacRewrite (ev,l,cl,by) ->
804
List.map (fun (b,m,c) -> (b,m,intern_constr_with_bindings ist c)) l,
805
clause_app (intern_hyp_location ist) cl,
806
Option.map (intern_tactic ist) by)
807
| TacInversion (inv,hyp) ->
808
TacInversion (intern_inversion_strength lf ist inv,
809
intern_quantified_hypothesis ist hyp)
812
| TacExtend (loc,opn,l) ->
813
let _ = lookup_tactic opn in
814
TacExtend (adjust_loc loc,opn,List.map (intern_genarg ist) l)
815
| TacAlias (loc,s,l,(dir,body)) ->
816
let l = List.map (fun (id,a) -> (id,intern_genarg ist a)) l in
817
TacAlias (loc,s,l,(dir,body))
819
and intern_tactic ist tac = (snd (intern_tactic_seq ist tac) : glob_tactic_expr)
821
and intern_tactic_seq ist = function
823
let lf = ref ist.ltacvars in
824
let t = intern_atomic lf ist t in
825
!lf, TacAtom (adjust_loc loc, t)
826
| TacFun tacfun -> ist.ltacvars, TacFun (intern_tactic_fun ist tacfun)
827
| TacLetIn (isrec,l,u) ->
828
let (l1,l2) = ist.ltacvars in
829
let ist' = { ist with ltacvars = (extract_let_names l @ l1, l2) } in
830
let l = List.map (fun (n,b) ->
831
(n,intern_tacarg !strict_check (if isrec then ist' else ist) b)) l in
832
ist.ltacvars, TacLetIn (isrec,l,intern_tactic ist' u)
833
| TacMatchGoal (lz,lr,lmr) ->
834
ist.ltacvars, TacMatchGoal(lz,lr, intern_match_rule ist lmr)
835
| TacMatch (lz,c,lmr) ->
836
ist.ltacvars, TacMatch (lz,intern_tactic ist c,intern_match_rule ist lmr)
837
| TacId l -> ist.ltacvars, TacId (intern_message ist l)
839
ist.ltacvars, TacFail (intern_or_var ist n,intern_message ist l)
840
| TacProgress tac -> ist.ltacvars, TacProgress (intern_tactic ist tac)
841
| TacAbstract (tac,s) -> ist.ltacvars, TacAbstract (intern_tactic ist tac,s)
842
| TacThen (t1,[||],t2,[||]) ->
843
let lfun', t1 = intern_tactic_seq ist t1 in
844
let lfun'', t2 = intern_tactic_seq { ist with ltacvars = lfun' } t2 in
845
lfun'', TacThen (t1,[||],t2,[||])
846
| TacThen (t1,tf,t2,tl) ->
847
let lfun', t1 = intern_tactic_seq ist t1 in
848
let ist' = { ist with ltacvars = lfun' } in
849
(* Que faire en cas de (tac complexe avec Match et Thens; tac2) ?? *)
850
lfun', TacThen (t1,Array.map (intern_tactic ist') tf,intern_tactic ist' t2,
851
Array.map (intern_tactic ist') tl)
853
let lfun', t = intern_tactic_seq ist t in
854
let ist' = { ist with ltacvars = lfun' } in
855
(* Que faire en cas de (tac complexe avec Match et Thens; tac2) ?? *)
856
lfun', TacThens (t, List.map (intern_tactic ist') tl)
858
ist.ltacvars, TacDo (intern_or_var ist n,intern_tactic ist tac)
859
| TacTry tac -> ist.ltacvars, TacTry (intern_tactic ist tac)
860
| TacInfo tac -> ist.ltacvars, TacInfo (intern_tactic ist tac)
861
| TacRepeat tac -> ist.ltacvars, TacRepeat (intern_tactic ist tac)
862
| TacOrelse (tac1,tac2) ->
863
ist.ltacvars, TacOrelse (intern_tactic ist tac1,intern_tactic ist tac2)
864
| TacFirst l -> ist.ltacvars, TacFirst (List.map (intern_tactic ist) l)
865
| TacSolve l -> ist.ltacvars, TacSolve (List.map (intern_tactic ist) l)
866
| TacComplete tac -> ist.ltacvars, TacComplete (intern_tactic ist tac)
867
| TacArg a -> ist.ltacvars, TacArg (intern_tacarg true ist a)
869
and intern_tactic_fun ist (var,body) =
870
let (l1,l2) = ist.ltacvars in
871
let lfun' = List.rev_append (Option.List.flatten var) l1 in
872
(var,intern_tactic { ist with ltacvars = (lfun',l2) } body)
874
and intern_tacarg strict ist = function
876
| Reference r -> intern_non_tactic_reference strict ist r
877
| IntroPattern ipat ->
878
let lf = ref([],[]) in (*How to know what names the intropattern binds?*)
879
IntroPattern (intern_intro_pattern lf ist ipat)
880
| Integer n -> Integer n
881
| ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c)
882
| MetaIdArg (loc,istac,s) ->
883
(* $id can occur in Grammar tactic... *)
884
let id = id_of_string s in
885
if find_ltacvar id ist then
886
if istac then Reference (ArgVar (adjust_loc loc,id))
887
else ConstrMayEval (ConstrTerm (RVar (adjust_loc loc,id), None))
888
else error_syntactic_metavariables_not_allowed loc
889
| TacCall (loc,f,[]) -> intern_isolated_tactic_reference strict ist f
890
| TacCall (loc,f,l) ->
892
intern_applied_tactic_reference ist f,
893
List.map (intern_tacarg !strict_check ist) l)
894
| TacExternal (loc,com,req,la) ->
895
TacExternal (loc,com,req,List.map (intern_tacarg !strict_check ist) la)
896
| TacFreshId x -> TacFreshId (List.map (intern_or_var ist) x)
897
| Tacexp t -> Tacexp (intern_tactic ist t)
898
| TacDynamic(loc,t) as x ->
900
| "tactic" | "value" | "constr" -> x
901
| s -> anomaly_loc (loc, "",
902
str "Unknown dynamic: <" ++ str s ++ str ">"))
904
(* Reads the rules of a Match Context or a Match *)
905
and intern_match_rule ist = function
907
All (intern_tactic ist tc) :: (intern_match_rule ist tl)
908
| (Pat (rl,mp,tc))::tl ->
909
let {ltacvars=(lfun,l2); gsigma=sigma; genv=env} = ist in
910
let lfun',metas1,hyps = intern_match_goal_hyps sigma env lfun rl in
911
let ido,metas2,pat = intern_pattern sigma env lfun mp in
912
let metas = list_uniquize (metas1@metas2) in
913
let ist' = { ist with ltacvars = (metas@(Option.List.cons ido lfun'),l2) } in
914
Pat (hyps,pat,intern_tactic ist' tc) :: (intern_match_rule ist tl)
917
and intern_genarg ist x =
918
match genarg_tag x with
919
| BoolArgType -> in_gen globwit_bool (out_gen rawwit_bool x)
920
| IntArgType -> in_gen globwit_int (out_gen rawwit_int x)
922
in_gen globwit_int_or_var
923
(intern_or_var ist (out_gen rawwit_int_or_var x))
925
in_gen globwit_string (out_gen rawwit_string x)
927
in_gen globwit_pre_ident (out_gen rawwit_pre_ident x)
928
| IntroPatternArgType ->
929
let lf = ref ([],[]) in
930
(* how to know which names are bound by the intropattern *)
931
in_gen globwit_intro_pattern
932
(intern_intro_pattern lf ist (out_gen rawwit_intro_pattern x))
934
let lf = ref ([],[]) in
935
in_gen (globwit_ident_gen b)
936
(intern_ident lf ist (out_gen (rawwit_ident_gen b) x))
938
in_gen globwit_var (intern_hyp ist (out_gen rawwit_var x))
940
in_gen globwit_ref (intern_global_reference ist (out_gen rawwit_ref x))
942
in_gen globwit_sort (out_gen rawwit_sort x)
944
in_gen globwit_constr (intern_constr ist (out_gen rawwit_constr x))
945
| ConstrMayEvalArgType ->
946
in_gen globwit_constr_may_eval
947
(intern_constr_may_eval ist (out_gen rawwit_constr_may_eval x))
949
in_gen globwit_quant_hyp
950
(intern_quantified_hypothesis ist (out_gen rawwit_quant_hyp x))
952
in_gen globwit_red_expr (intern_red_expr ist (out_gen rawwit_red_expr x))
953
| OpenConstrArgType b ->
954
in_gen (globwit_open_constr_gen b)
955
((),intern_constr ist (snd (out_gen (rawwit_open_constr_gen b) x)))
956
| ConstrWithBindingsArgType ->
957
in_gen globwit_constr_with_bindings
958
(intern_constr_with_bindings ist (out_gen rawwit_constr_with_bindings x))
960
in_gen globwit_bindings
961
(intern_bindings ist (out_gen rawwit_bindings x))
962
| List0ArgType _ -> app_list0 (intern_genarg ist) x
963
| List1ArgType _ -> app_list1 (intern_genarg ist) x
964
| OptArgType _ -> app_opt (intern_genarg ist) x
965
| PairArgType _ -> app_pair (intern_genarg ist) (intern_genarg ist) x
967
match tactic_genarg_level s with
969
(* Special treatment of tactic arguments *)
970
in_gen (globwit_tactic n) (intern_tactic ist
971
(out_gen (rawwit_tactic n) x))
973
lookup_genarg_glob s ist x
975
(************* End globalization ************)
977
(***************************************************************************)
978
(* Evaluation/interpretation *)
980
(* Associates variables with values and gives the remaining variables and
982
let head_with_value (lvar,lval) =
983
let rec head_with_value_rec lacc = function
984
| ([],[]) -> (lacc,[],[])
985
| (vr::tvr,ve::tve) ->
987
| None -> head_with_value_rec lacc (tvr,tve)
988
| Some v -> head_with_value_rec ((v,ve)::lacc) (tvr,tve))
989
| (vr,[]) -> (lacc,vr,[])
990
| ([],ve) -> (lacc,[],ve)
992
head_with_value_rec [] (lvar,lval)
994
(* Gives a context couple if there is a context identifier *)
995
let give_context ctxt = function
997
| Some id -> [id,VConstr_context ctxt]
999
(* Reads a pattern by substituting vars of lfun *)
1000
let eval_pattern lfun c =
1001
let lvar = List.map (fun (id,c) -> (id,lazy(pattern_of_constr c))) lfun in
1002
instantiate_pattern lvar c
1004
let read_pattern lfun = function
1005
| Subterm (b,ido,pc) -> Subterm (b,ido,eval_pattern lfun pc)
1006
| Term pc -> Term (eval_pattern lfun pc)
1008
let value_of_ident id = VIntroPattern (IntroIdentifier id)
1010
let extend_values_with_bindings (ln,lm) lfun =
1011
let lnames = List.map (fun (id,id') ->(id,value_of_ident id')) ln in
1012
let lmatch = List.map (fun (id,c) -> (id,VConstr c)) lm in
1013
(* For compatibility, bound variables are visible only if no other
1014
binding of the same name exists *)
1017
(* Reads the hypotheses of a Match Context rule *)
1018
let cons_and_check_name id l =
1019
if List.mem id l then
1020
user_err_loc (dloc,"read_match_goal_hyps",
1021
strbrk ("Hypothesis pattern-matching variable "^(string_of_id id)^
1022
" used twice in the same pattern."))
1025
let rec read_match_goal_hyps lfun lidh = function
1026
| (Hyp ((loc,na) as locna,mp))::tl ->
1027
let lidh' = name_fold cons_and_check_name na lidh in
1028
Hyp (locna,read_pattern lfun mp)::
1029
(read_match_goal_hyps lfun lidh' tl)
1030
| (Def ((loc,na) as locna,mv,mp))::tl ->
1031
let lidh' = name_fold cons_and_check_name na lidh in
1032
Def (locna,read_pattern lfun mv, read_pattern lfun mp)::
1033
(read_match_goal_hyps lfun lidh' tl)
1036
(* Reads the rules of a Match Context or a Match *)
1037
let rec read_match_rule lfun = function
1038
| (All tc)::tl -> (All tc)::(read_match_rule lfun tl)
1039
| (Pat (rl,mp,tc))::tl ->
1040
Pat (read_match_goal_hyps lfun [] rl, read_pattern lfun mp,tc)
1041
:: read_match_rule lfun tl
1044
(* For Match Context and Match *)
1045
exception Not_coherent_metas
1046
exception Eval_fail of std_ppcmds
1048
let is_match_catchable = function
1049
| PatternMatchingFailure | Eval_fail _ -> true
1050
| e -> Logic.catchable_exception e
1052
(* Verifies if the matched list is coherent with respect to lcm *)
1053
(* While non-linear matching is modulo eq_constr in matches, merge of *)
1054
(* different instances of the same metavars is here modulo conversion... *)
1055
let verify_metas_coherence gl (ln1,lcm) (ln,lm) =
1056
let rec aux = function
1058
if (List.for_all (fun (a,b) -> a<>num or pf_conv_x gl b csr) lcm) then
1061
raise Not_coherent_metas
1065
(* Tries to match one hypothesis pattern with a list of hypotheses *)
1066
let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps =
1067
let get_id_couple id = function
1068
| Name idpat -> [idpat,VConstr (mkVar id)]
1069
| Anonymous -> [] in
1070
let match_pat lmatch hyp pat =
1073
let lmeta = extended_matches t hyp in
1075
let lmeta = verify_metas_coherence gl lmatch lmeta in
1076
([],lmeta,(fun () -> raise PatternMatchingFailure))
1078
| Not_coherent_metas -> raise PatternMatchingFailure);
1079
| Subterm (b,ic,t) ->
1080
let rec match_next_pattern find_next () =
1081
let (lmeta,ctxt,find_next') = find_next () in
1083
let lmeta = verify_metas_coherence gl lmatch lmeta in
1084
(give_context ctxt ic,lmeta,match_next_pattern find_next')
1086
| Not_coherent_metas -> match_next_pattern find_next' () in
1087
match_next_pattern(fun () -> match_subterm_gen b t hyp) () in
1088
let rec apply_one_mhyp_context_rec = function
1089
| (id,b,hyp as hd)::tl ->
1092
let rec match_next_pattern find_next () =
1094
let (ids, lmeta, find_next') = find_next () in
1095
(get_id_couple id hypname@ids, lmeta, hd,
1096
match_next_pattern find_next')
1098
| PatternMatchingFailure -> apply_one_mhyp_context_rec tl in
1099
match_next_pattern (fun () -> match_pat lmatch hyp pat) ()
1103
let rec match_next_pattern_in_body next_in_body () =
1105
let (ids,lmeta,next_in_body') = next_in_body() in
1106
let rec match_next_pattern_in_typ next_in_typ () =
1108
let (ids',lmeta',next_in_typ') = next_in_typ() in
1109
(get_id_couple id hypname@ids@ids', lmeta', hd,
1110
match_next_pattern_in_typ next_in_typ')
1112
| PatternMatchingFailure ->
1113
match_next_pattern_in_body next_in_body' () in
1114
match_next_pattern_in_typ
1115
(fun () -> match_pat lmeta hyp pat) ()
1116
with PatternMatchingFailure -> apply_one_mhyp_context_rec tl
1118
match_next_pattern_in_body
1119
(fun () -> match_pat lmatch body patv) ()
1120
| None -> apply_one_mhyp_context_rec tl)
1122
db_hyp_pattern_failure ist.debug env (hypname,pat);
1123
raise PatternMatchingFailure
1125
apply_one_mhyp_context_rec lhyps
1127
let constr_to_id loc = function
1128
| VConstr c when isVar c -> destVar c
1129
| _ -> invalid_arg_loc (loc, "Not an identifier")
1131
let constr_to_qid loc c =
1132
try shortest_qualid_of_global Idset.empty (global_of_constr c)
1133
with _ -> invalid_arg_loc (loc, "Not a global reference")
1135
let is_variable env id =
1136
List.mem id (ids_of_named_context (Environ.named_context env))
1138
(* Debug reference *)
1139
let debug = ref DebugOff
1141
(* Sets the debugger mode *)
1142
let set_debug pos = debug := pos
1144
(* Gives the state of debug *)
1145
let get_debug () = !debug
1147
let debugging_step ist pp =
1148
match ist.debug with
1150
safe_msgnl (str "Level " ++ int lev ++ str": " ++ pp () ++ fnl())
1153
let debugging_exception_step ist signal_anomaly e pp =
1155
if signal_anomaly then explain_logic_error
1156
else explain_logic_error_no_anomaly in
1157
debugging_step ist (fun () ->
1158
pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ !explain_exc e)
1160
let error_ltac_variable loc id env v s =
1161
user_err_loc (loc, "", str "Ltac variable " ++ pr_id id ++
1162
strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++
1163
strbrk "which cannot be coerced to " ++ str s ++ str".")
1165
exception CannotCoerceTo of string
1167
(* Raise Not_found if not in interpretation sign *)
1168
let try_interp_ltac_var coerce ist env (loc,id) =
1169
let v = List.assoc id ist.lfun in
1170
try coerce v with CannotCoerceTo s -> error_ltac_variable loc id env v s
1172
let interp_ltac_var coerce ist env locid =
1173
try try_interp_ltac_var coerce ist env locid
1174
with Not_found -> anomaly "Detected as ltac var at interning time"
1176
(* Interprets an identifier which must be fresh *)
1177
let coerce_to_ident fresh env = function
1178
| VIntroPattern (IntroIdentifier id) -> id
1179
| VConstr c when isVar c & not (fresh & is_variable env (destVar c)) ->
1180
(* We need it fresh for intro e.g. in "Tac H = clear H; intro H" *)
1182
| v -> raise (CannotCoerceTo "a fresh identifier")
1184
let interp_ident_gen fresh ist gl id =
1185
let env = pf_env gl in
1186
try try_interp_ltac_var (coerce_to_ident fresh env) ist (Some env) (dloc,id)
1187
with Not_found -> id
1189
let interp_ident = interp_ident_gen false
1190
let interp_fresh_ident = interp_ident_gen true
1192
(* Interprets an optional identifier which must be fresh *)
1193
let interp_fresh_name ist gl = function
1194
| Anonymous -> Anonymous
1195
| Name id -> Name (interp_fresh_ident ist gl id)
1197
let coerce_to_intro_pattern env = function
1198
| VIntroPattern ipat -> ipat
1199
| VConstr c when isVar c ->
1200
(* This happens e.g. in definitions like "Tac H = clear H; intro H" *)
1201
(* but also in "destruct H as (H,H')" *)
1202
IntroIdentifier (destVar c)
1203
| v -> raise (CannotCoerceTo "an introduction pattern")
1205
let interp_intro_pattern_var loc ist env id =
1206
try try_interp_ltac_var (coerce_to_intro_pattern env) ist (Some env) (loc,id)
1207
with Not_found -> IntroIdentifier id
1209
let coerce_to_hint_base = function
1210
| VIntroPattern (IntroIdentifier id) -> string_of_id id
1211
| _ -> raise (CannotCoerceTo "a hint base name")
1213
let interp_hint_base ist s =
1214
try try_interp_ltac_var coerce_to_hint_base ist None (dloc,id_of_string s)
1217
let coerce_to_int = function
1219
| v -> raise (CannotCoerceTo "an integer")
1221
let interp_int ist locid =
1222
try try_interp_ltac_var coerce_to_int ist None locid
1224
user_err_loc(fst locid,"interp_int",
1225
str "Unbound variable " ++ pr_id (snd locid) ++ str".")
1227
let interp_int_or_var ist = function
1228
| ArgVar locid -> interp_int ist locid
1231
let int_or_var_list_of_VList = function
1232
| VList l -> List.map (fun n -> ArgArg (coerce_to_int n)) l
1233
| _ -> raise Not_found
1235
let interp_int_or_var_as_list ist = function
1236
| ArgVar (_,id as locid) ->
1237
(try int_or_var_list_of_VList (List.assoc id ist.lfun)
1238
with Not_found | CannotCoerceTo _ -> [ArgArg (interp_int ist locid)])
1239
| ArgArg n as x -> [x]
1241
let interp_int_or_var_list ist l =
1242
List.flatten (List.map (interp_int_or_var_as_list ist) l)
1244
let constr_of_value env = function
1245
| VConstr csr -> csr
1246
| VIntroPattern (IntroIdentifier id) -> constr_of_id env id
1247
| _ -> raise Not_found
1249
let coerce_to_hyp env = function
1250
| VConstr c when isVar c -> destVar c
1251
| VIntroPattern (IntroIdentifier id) when is_variable env id -> id
1252
| _ -> raise (CannotCoerceTo "a variable")
1254
(* Interprets a bound variable (especially an existing hypothesis) *)
1255
let interp_hyp ist gl (loc,id as locid) =
1256
let env = pf_env gl in
1257
(* Look first in lfun for a value coercible to a variable *)
1258
try try_interp_ltac_var (coerce_to_hyp env) ist (Some env) locid
1260
(* Then look if bound in the proof context at calling time *)
1261
if is_variable env id then id
1262
else user_err_loc (loc,"eval_variable",pr_id id ++ str " not found.")
1264
let hyp_list_of_VList env = function
1265
| VList l -> List.map (coerce_to_hyp env) l
1266
| _ -> raise Not_found
1268
let interp_hyp_list_as_list ist gl (loc,id as x) =
1269
try hyp_list_of_VList (pf_env gl) (List.assoc id ist.lfun)
1270
with Not_found | CannotCoerceTo _ -> [interp_hyp ist gl x]
1272
let interp_hyp_list ist gl l =
1273
List.flatten (List.map (interp_hyp_list_as_list ist gl) l)
1275
let interp_clause_pattern ist gl (l,occl) =
1276
let rec check acc = function
1277
| (hyp,l) :: rest ->
1278
let hyp = interp_hyp ist gl hyp in
1279
if List.mem hyp acc then
1280
error ("Hypothesis "^(string_of_id hyp)^" occurs twice.");
1281
(hyp,l)::(check (hyp::acc) rest)
1283
in (l,check [] occl)
1285
let interp_move_location ist gl = function
1286
| MoveAfter id -> MoveAfter (interp_hyp ist gl id)
1287
| MoveBefore id -> MoveBefore (interp_hyp ist gl id)
1288
| MoveToEnd toleft as x -> x
1290
(* Interprets a qualified name *)
1291
let coerce_to_reference env v =
1293
| VConstr c -> global_of_constr c (* may raise Not_found *)
1294
| _ -> raise Not_found
1295
with Not_found -> raise (CannotCoerceTo "a reference")
1297
let interp_reference ist env = function
1300
interp_ltac_var (coerce_to_reference env) ist (Some env) locid
1302
let pf_interp_reference ist gl = interp_reference ist (pf_env gl)
1304
let coerce_to_inductive = function
1305
| VConstr c when isInd c -> destInd c
1306
| _ -> raise (CannotCoerceTo "an inductive type")
1308
let interp_inductive ist = function
1310
| ArgVar locid -> interp_ltac_var coerce_to_inductive ist None locid
1312
let coerce_to_evaluable_ref env v =
1313
let ev = match v with
1314
| VConstr c when isConst c -> EvalConstRef (destConst c)
1315
| VConstr c when isVar c -> EvalVarRef (destVar c)
1316
| VIntroPattern (IntroIdentifier id) when List.mem id (ids_of_context env)
1318
| _ -> raise (CannotCoerceTo "an evaluable reference")
1320
if not (Tacred.is_evaluable env ev) then
1321
raise (CannotCoerceTo "an evaluable reference")
1325
let interp_evaluable ist env = function
1326
| ArgArg (r,Some (loc,id)) ->
1327
(* Maybe [id] has been introduced by Intro-like tactics *)
1328
(try match Environ.lookup_named id env with
1329
| (_,Some _,_) -> EvalVarRef id
1330
| _ -> error_not_evaluable (pr_id id)
1333
| EvalConstRef _ -> r
1334
| _ -> Pretype_errors.error_var_not_found_loc loc id)
1335
| ArgArg (r,None) -> r
1337
interp_ltac_var (coerce_to_evaluable_ref env) ist (Some env) locid
1339
(* Interprets an hypothesis name *)
1340
let interp_occurrences ist (b,occs) =
1341
(b,interp_int_or_var_list ist occs)
1343
let interp_hyp_location ist gl ((occs,id),hl) =
1344
((interp_occurrences ist occs,interp_hyp ist gl id),hl)
1346
let interp_clause ist gl { onhyps=ol; concl_occs=occs } =
1347
{ onhyps=Option.map(List.map (interp_hyp_location ist gl)) ol;
1348
concl_occs=interp_occurrences ist occs }
1350
(* Interpretation of constructions *)
1352
(* Extract the constr list from lfun *)
1353
let rec constr_list_aux env = function
1355
let (l1,l2) = constr_list_aux env tl in
1356
(try ((id,constr_of_value env v)::l1,l2)
1358
let ido = match v with
1359
| VIntroPattern (IntroIdentifier id0) -> Some id0
1364
let constr_list ist env = constr_list_aux env ist.lfun
1366
(* Extract the identifier list from lfun: join all branches (what to do else?)*)
1367
let rec intropattern_ids (loc,pat) = match pat with
1368
| IntroIdentifier id -> [id]
1369
| IntroOrAndPattern ll ->
1370
List.flatten (List.map intropattern_ids (List.flatten ll))
1371
| IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _ -> []
1373
let rec extract_ids ids = function
1374
| (id,VIntroPattern ipat)::tl when not (List.mem id ids) ->
1375
intropattern_ids (dloc,ipat) @ extract_ids ids tl
1376
| _::tl -> extract_ids ids tl
1379
let default_fresh_id = id_of_string "H"
1381
let interp_fresh_id ist gl l =
1382
let ids = map_succeed (function ArgVar(_,id) -> id | _ -> failwith "") l in
1383
let avoid = (extract_ids ids ist.lfun) @ ist.avoid_ids in
1385
if l = [] then default_fresh_id
1388
String.concat "" (List.map (function
1390
| ArgVar (_,id) -> string_of_id (interp_ident ist gl id)) l) in
1391
let s = if Lexer.is_keyword s then s^"0" else s in
1393
Tactics.fresh_id avoid id gl
1395
(* To retype a list of key*constr with undefined key *)
1396
let retype_list sigma env lst =
1397
List.fold_right (fun (x,csr) a ->
1398
try (x,Retyping.get_judgment_of env sigma csr)::a with
1399
| Anomaly _ -> a) lst []
1401
let extract_ltac_vars_data ist sigma env =
1402
let (ltacvars,_ as vars) = constr_list ist env in
1403
vars, retype_list sigma env ltacvars
1405
let extract_ltac_vars ist sigma env =
1406
let (_,unbndltacvars),typs = extract_ltac_vars_data ist sigma env in
1409
let implicit_tactic = ref None
1411
let declare_implicit_tactic tac = implicit_tactic := Some tac
1415
let solvable_by_tactic env evi (ev,args) src =
1416
match (!implicit_tactic, src) with
1417
| Some tac, (ImplicitArg _ | QuestionMark _)
1419
Environ.named_context_of_val evi.evar_hyps =
1420
Environ.named_context env ->
1421
let id = id_of_string "H" in
1422
start_proof id (Local,Proof Lemma) evi.evar_hyps evi.evar_concl
1426
by (tclCOMPLETE tac);
1427
let _,(const,_,_,_) = cook_proof ignore in
1428
delete_current_proof (); const.const_entry_body
1429
with e when Logic.catchable_exception e ->
1430
delete_current_proof();
1435
let solve_remaining_evars env initial_sigma evd c =
1436
let evdref = ref (Typeclasses.resolve_typeclasses ~fail:true env evd) in
1437
let rec proc_rec c =
1438
match kind_of_term (Reductionops.whd_evar (evars_of !evdref) c) with
1439
| Evar (ev,args as k) when not (Evd.mem initial_sigma ev) ->
1440
let (loc,src) = evar_source ev !evdref in
1441
let sigma = evars_of !evdref in
1442
let evi = Evd.find sigma ev in
1444
let c = solvable_by_tactic env evi k src in
1445
evdref := Evd.evar_define ev c !evdref;
1448
Pretype_errors.error_unsolvable_implicit loc env sigma evi src None)
1449
| _ -> map_constr proc_rec c
1451
proc_rec (Evarutil.nf_isevar !evdref c)
1453
let interp_gen kind ist sigma env (c,ce) =
1454
let (ltacvars,unbndltacvars as vars),typs =
1455
extract_ltac_vars_data ist sigma env in
1456
let c = match ce with
1458
(* If at toplevel (ce<>None), the error can be due to an incorrect
1459
context at globalization time: we retype with the now known
1460
intros/lettac/inversion hypothesis names *)
1462
let ltacdata = (List.map fst ltacvars,unbndltacvars) in
1463
intern_gen (kind = IsType) ~ltacvars:ltacdata sigma env c in
1464
let trace = (dloc,LtacConstrInterp (c,vars))::ist.trace in
1465
catch_error trace (understand_ltac sigma env (typs,unbndltacvars) kind) c
1467
(* Interprets a constr and solve remaining evars with default tactic *)
1468
let interp_econstr kind ist sigma env cc =
1469
let evars,c = interp_gen kind ist sigma env cc in
1470
let csr = solve_remaining_evars env sigma evars c in
1471
db_constr ist.debug env csr;
1474
(* Interprets an open constr *)
1475
let interp_open_constr ccl ist sigma env cc =
1476
let evd,c = interp_gen (OfType ccl) ist sigma env cc in
1479
let interp_open_type ccl ist sigma env cc =
1480
let evd,c = interp_gen IsType ist sigma env cc in
1483
let interp_constr = interp_econstr (OfType None)
1485
let interp_type = interp_econstr IsType
1487
(* Interprets a constr expression casted by the current goal *)
1488
let pf_interp_casted_constr ist gl cc =
1489
interp_econstr (OfType (Some (pf_concl gl))) ist (project gl) (pf_env gl) cc
1491
(* Interprets an open constr expression *)
1492
let pf_interp_open_constr casted ist gl cc =
1493
let cl = if casted then Some (pf_concl gl) else None in
1494
interp_open_constr cl ist (project gl) (pf_env gl) cc
1496
(* Interprets a constr expression *)
1497
let pf_interp_constr ist gl =
1498
interp_constr ist (project gl) (pf_env gl)
1500
let constr_list_of_VList env = function
1501
| VList l -> List.map (constr_of_value env) l
1502
| _ -> raise Not_found
1504
let pf_interp_constr_in_compound_list inj_fun dest_fun interp_fun ist gl l =
1505
let env = pf_env gl in
1506
let try_expand_ltac_var x =
1507
try match dest_fun x with
1509
List.map inj_fun (constr_list_of_VList env (List.assoc id ist.lfun))
1513
(*all of dest_fun, List.assoc, constr_list_of_VList may raise Not_found*)
1514
[interp_fun ist gl x] in
1515
List.flatten (List.map try_expand_ltac_var l)
1517
let pf_interp_constr_list =
1518
pf_interp_constr_in_compound_list (fun x -> x) (fun x -> x)
1519
(fun ist gl -> interp_constr ist (project gl) (pf_env gl))
1522
let pf_interp_constr_list_as_list ist gl (c,_ as x) =
1525
(try constr_list_of_VList (pf_env gl) (List.assoc id ist.lfun)
1526
with Not_found -> [])
1527
| _ -> [interp_constr ist (project gl) (pf_env gl) x]
1529
let pf_interp_constr_list ist gl l =
1530
List.flatten (List.map (pf_interp_constr_list_as_list ist gl) l)
1533
let inj_open c = (Evd.empty,c)
1535
let pf_interp_open_constr_list =
1536
pf_interp_constr_in_compound_list inj_open (fun x -> x)
1537
(fun ist gl -> interp_open_constr None ist (project gl) (pf_env gl))
1540
let pf_interp_open_constr_list_as_list ist gl (c,_ as x) =
1543
(try List.map inj_open
1544
(constr_list_of_VList (pf_env gl) (List.assoc id ist.lfun))
1546
[interp_open_constr None ist (project gl) (pf_env gl) x])
1548
[interp_open_constr None ist (project gl) (pf_env gl) x]
1550
let pf_interp_open_constr_list ist gl l =
1551
List.flatten (List.map (pf_interp_open_constr_list_as_list ist gl) l)
1554
(* Interprets a type expression *)
1555
let pf_interp_type ist gl =
1556
interp_type ist (project gl) (pf_env gl)
1558
(* Interprets a reduction expression *)
1559
let interp_unfold ist env (occs,qid) =
1560
(interp_occurrences ist occs,interp_evaluable ist env qid)
1562
let interp_flag ist env red =
1563
{ red with rConst = List.map (interp_evaluable ist env) red.rConst }
1565
let interp_pattern ist sigma env (occs,c) =
1566
(interp_occurrences ist occs, interp_constr ist sigma env c)
1568
let pf_interp_constr_with_occurrences ist gl =
1569
interp_pattern ist (project gl) (pf_env gl)
1571
let pf_interp_constr_with_occurrences_and_name_as_list =
1572
pf_interp_constr_in_compound_list
1573
(fun c -> ((all_occurrences_expr,c),Anonymous))
1574
(function ((occs,c),Anonymous) when occs = all_occurrences_expr -> c
1575
| _ -> raise Not_found)
1576
(fun ist gl (occ_c,na) ->
1577
(interp_pattern ist (project gl) (pf_env gl) occ_c,
1578
interp_fresh_name ist gl na))
1580
let interp_red_expr ist sigma env = function
1581
| Unfold l -> Unfold (List.map (interp_unfold ist env) l)
1582
| Fold l -> Fold (List.map (interp_constr ist sigma env) l)
1583
| Cbv f -> Cbv (interp_flag ist env f)
1584
| Lazy f -> Lazy (interp_flag ist env f)
1585
| Pattern l -> Pattern (List.map (interp_pattern ist sigma env) l)
1586
| Simpl o -> Simpl (Option.map (interp_pattern ist sigma env) o)
1587
| (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r
1589
let pf_interp_red_expr ist gl = interp_red_expr ist (project gl) (pf_env gl)
1591
let interp_may_eval f ist gl = function
1592
| ConstrEval (r,c) ->
1593
let redexp = pf_interp_red_expr ist gl r in
1594
pf_reduction_of_red_expr gl redexp (f ist gl c)
1595
| ConstrContext ((loc,s),c) ->
1598
and ctxt = constr_of_VConstr_context (List.assoc s ist.lfun) in
1599
subst_meta [special_meta,ic] ctxt
1602
user_err_loc (loc, "interp_may_eval",
1603
str "Unbound context identifier" ++ pr_id s ++ str"."))
1604
| ConstrTypeOf c -> pf_type_of gl (f ist gl c)
1609
debugging_exception_step ist false e (fun () ->
1610
str"interpretation of term " ++ pr_rawconstr_env (pf_env gl) (fst c));
1613
(* Interprets a constr expression possibly to first evaluate *)
1614
let interp_constr_may_eval ist gl c =
1617
interp_may_eval pf_interp_constr ist gl c
1619
debugging_exception_step ist false e (fun () -> str"evaluation of term");
1623
db_constr ist.debug (pf_env gl) csr;
1627
let inj_may_eval = function
1628
| ConstrTerm c -> ConstrTerm (inj_open c)
1629
| ConstrEval (r,c) -> ConstrEval (Tactics.inj_red_expr r,inj_open c)
1630
| ConstrContext (id,c) -> ConstrContext (id,inj_open c)
1631
| ConstrTypeOf c -> ConstrTypeOf (inj_open c)
1633
let message_of_value = function
1635
| VInteger n -> int n
1636
| VIntroPattern ipat -> pr_intro_pattern (dloc,ipat)
1637
| VConstr_context c | VConstr c -> pr_constr c
1638
| VRec _ | VRTactic _ | VFun _ -> str "<tactic>"
1639
| VList _ -> str "<list>"
1641
let rec interp_message_token ist = function
1642
| MsgString s -> str s
1644
| MsgIdent (loc,id) ->
1646
try List.assoc id ist.lfun
1647
with Not_found -> user_err_loc (loc,"",pr_id id ++ str" not found.") in
1650
let rec interp_message_nl ist = function
1652
| l -> prlist_with_sep spc (interp_message_token ist) l ++ fnl()
1654
let interp_message ist l =
1655
(* Force evaluation of interp_message_token so that potential errors
1656
are raised now and not at printing time *)
1657
prlist (fun x -> spc () ++ x) (List.map (interp_message_token ist) l)
1659
let rec interp_intro_pattern ist gl = function
1660
| loc, IntroOrAndPattern l ->
1661
loc, IntroOrAndPattern (interp_or_and_intro_pattern ist gl l)
1662
| loc, IntroIdentifier id ->
1663
loc, interp_intro_pattern_var loc ist (pf_env gl) id
1664
| loc, (IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _)
1667
and interp_or_and_intro_pattern ist gl =
1668
List.map (List.map (interp_intro_pattern ist gl))
1670
let interp_in_hyp_as ist gl (id,ipat) =
1671
(interp_hyp ist gl id,Option.map (interp_intro_pattern ist gl) ipat)
1673
(* Quantified named or numbered hypothesis or hypothesis in context *)
1674
(* (as in Inversion) *)
1675
let coerce_to_quantified_hypothesis = function
1676
| VInteger n -> AnonHyp n
1677
| VIntroPattern (IntroIdentifier id) -> NamedHyp id
1678
| v -> raise (CannotCoerceTo "a quantified hypothesis")
1680
let interp_quantified_hypothesis ist = function
1681
| AnonHyp n -> AnonHyp n
1683
try try_interp_ltac_var coerce_to_quantified_hypothesis ist None(dloc,id)
1684
with Not_found -> NamedHyp id
1686
let interp_binding_name ist = function
1687
| AnonHyp n -> AnonHyp n
1689
(* If a name is bound, it has to be a quantified hypothesis *)
1690
(* user has to use other names for variables if these ones clash with *)
1691
(* a name intented to be used as a (non-variable) identifier *)
1692
try try_interp_ltac_var coerce_to_quantified_hypothesis ist None(dloc,id)
1693
with Not_found -> NamedHyp id
1695
(* Quantified named or numbered hypothesis or hypothesis in context *)
1696
(* (as in Inversion) *)
1697
let coerce_to_decl_or_quant_hyp env = function
1698
| VInteger n -> AnonHyp n
1700
try NamedHyp (coerce_to_hyp env v)
1701
with CannotCoerceTo _ ->
1702
raise (CannotCoerceTo "a declared or quantified hypothesis")
1704
let interp_declared_or_quantified_hypothesis ist gl = function
1705
| AnonHyp n -> AnonHyp n
1707
let env = pf_env gl in
1708
try try_interp_ltac_var
1709
(coerce_to_decl_or_quant_hyp env) ist (Some env) (dloc,id)
1710
with Not_found -> NamedHyp id
1712
let interp_binding ist gl (loc,b,c) =
1713
(loc,interp_binding_name ist b,pf_interp_open_constr false ist gl c)
1715
let interp_bindings ist gl = function
1716
| NoBindings -> NoBindings
1717
| ImplicitBindings l -> ImplicitBindings (pf_interp_open_constr_list ist gl l)
1718
| ExplicitBindings l -> ExplicitBindings (List.map (interp_binding ist gl) l)
1720
let interp_constr_with_bindings ist gl (c,bl) =
1721
(pf_interp_constr ist gl c, interp_bindings ist gl bl)
1723
let interp_open_constr_with_bindings ist gl (c,bl) =
1724
(pf_interp_open_constr false ist gl c, interp_bindings ist gl bl)
1726
let interp_induction_arg ist gl = function
1727
| ElimOnConstr c -> ElimOnConstr (interp_constr_with_bindings ist gl c)
1728
| ElimOnAnonHyp n as x -> x
1729
| ElimOnIdent (loc,id) ->
1731
match List.assoc id ist.lfun with
1732
| VInteger n -> ElimOnAnonHyp n
1733
| VIntroPattern (IntroIdentifier id) -> ElimOnIdent (loc,id)
1734
| VConstr c -> ElimOnConstr (c,NoBindings)
1735
| _ -> user_err_loc (loc,"",
1736
strbrk "Cannot coerce " ++ pr_id id ++
1737
strbrk " neither to a quantified hypothesis nor to a term.")
1739
(* Interactive mode *)
1740
if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id)
1742
(pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id)))),
1745
let mk_constr_value ist gl c = VConstr (pf_interp_constr ist gl c)
1746
let mk_hyp_value ist gl c = VConstr (mkVar (interp_hyp ist gl c))
1747
let mk_int_or_var_value ist c = VInteger (interp_int_or_var ist c)
1749
(* Interprets an l-tac expression into a value *)
1750
let rec val_interp ist gl (tac:glob_tactic_expr) =
1752
let value_interp ist = match tac with
1753
(* Immediate evaluation *)
1754
| TacFun (it,body) -> VFun (ist.trace,ist.lfun,it,body)
1755
| TacLetIn (true,l,u) -> interp_letrec ist gl l u
1756
| TacLetIn (false,l,u) -> interp_letin ist gl l u
1757
| TacMatchGoal (lz,lr,lmr) -> interp_match_goal ist gl lz lr lmr
1758
| TacMatch (lz,c,lmr) -> interp_match ist gl lz c lmr
1759
| TacArg a -> interp_tacarg ist gl a
1760
(* Delayed evaluation *)
1761
| t -> VFun (ist.trace,ist.lfun,[],t)
1763
in check_for_interrupt ();
1764
match ist.debug with
1766
debug_prompt lev gl tac (fun v -> value_interp {ist with debug=v})
1767
| _ -> value_interp ist
1769
and eval_tactic ist = function
1770
| TacAtom (loc,t) ->
1772
let box = ref None in abstract_tactic_box := box;
1773
let call = LtacAtomCall (t,box) in
1774
let tac = (* catch error in the interpretation *)
1775
catch_error ((dloc,call)::ist.trace) (interp_atomic ist gl) t in
1776
(* catch error in the evaluation *)
1777
catch_error ((loc,call)::ist.trace) tac gl
1778
| TacFun _ | TacLetIn _ -> assert false
1779
| TacMatchGoal _ | TacMatch _ -> assert false
1780
| TacId s -> tclIDTAC_MESSAGE (interp_message_nl ist s)
1781
| TacFail (n,s) -> tclFAIL (interp_int_or_var ist n) (interp_message ist s)
1782
| TacProgress tac -> tclPROGRESS (interp_tactic ist tac)
1783
| TacAbstract (tac,ido) ->
1784
fun gl -> Tactics.tclABSTRACT
1785
(Option.map (interp_ident ist gl) ido) (interp_tactic ist tac) gl
1786
| TacThen (t1,tf,t,tl) ->
1787
tclTHENS3PARTS (interp_tactic ist t1)
1788
(Array.map (interp_tactic ist) tf) (interp_tactic ist t) (Array.map (interp_tactic ist) tl)
1789
| TacThens (t1,tl) -> tclTHENS (interp_tactic ist t1) (List.map (interp_tactic ist) tl)
1790
| TacDo (n,tac) -> tclDO (interp_int_or_var ist n) (interp_tactic ist tac)
1791
| TacTry tac -> tclTRY (interp_tactic ist tac)
1793
let t = (interp_tactic ist tac) in
1798
| _ -> abstract_tactic_expr (TacArg (Tacexp tac)) t
1800
| TacRepeat tac -> tclREPEAT (interp_tactic ist tac)
1801
| TacOrelse (tac1,tac2) ->
1802
tclORELSE (interp_tactic ist tac1) (interp_tactic ist tac2)
1803
| TacFirst l -> tclFIRST (List.map (interp_tactic ist) l)
1804
| TacSolve l -> tclSOLVE (List.map (interp_tactic ist) l)
1805
| TacComplete tac -> tclCOMPLETE (interp_tactic ist tac)
1806
| TacArg a -> assert false
1808
and force_vrec ist gl = function
1809
| VRec (lfun,body) -> val_interp {ist with lfun = !lfun} gl body
1812
and interp_ltac_reference loc' mustbetac ist gl = function
1813
| ArgVar (loc,id) ->
1814
let v = List.assoc id ist.lfun in
1815
let v = force_vrec ist gl v in
1816
let v = propagate_trace ist loc id v in
1817
if mustbetac then coerce_to_tactic loc id v else v
1819
let ids = extract_ids [] ist.lfun in
1820
let loc_info = ((if loc' = dloc then loc else loc'),LtacNameCall r) in
1822
{ lfun=[]; debug=ist.debug; avoid_ids=ids;
1823
trace = loc_info::ist.trace } in
1824
val_interp ist gl (lookup r)
1826
and interp_tacarg ist gl = function
1828
| Reference r -> interp_ltac_reference dloc false ist gl r
1829
| Integer n -> VInteger n
1830
| IntroPattern ipat -> VIntroPattern (snd (interp_intro_pattern ist gl ipat))
1831
| ConstrMayEval c -> VConstr (interp_constr_may_eval ist gl c)
1832
| MetaIdArg (loc,_,id) -> assert false
1833
| TacCall (loc,r,[]) -> interp_ltac_reference loc true ist gl r
1834
| TacCall (loc,f,l) ->
1835
let fv = interp_ltac_reference loc true ist gl f
1836
and largs = List.map (interp_tacarg ist gl) l in
1837
List.iter check_is_value largs;
1838
interp_app loc ist gl fv largs
1839
| TacExternal (loc,com,req,la) ->
1840
interp_external loc ist gl com req (List.map (interp_tacarg ist gl) la)
1842
let id = interp_fresh_id ist gl l in
1843
VIntroPattern (IntroIdentifier id)
1844
| Tacexp t -> val_interp ist gl t
1845
| TacDynamic(_,t) ->
1847
if tg = "tactic" then
1848
val_interp ist gl (tactic_out t ist)
1849
else if tg = "value" then
1851
else if tg = "constr" then
1852
VConstr (constr_out t)
1854
anomaly_loc (dloc, "Tacinterp.val_interp",
1855
(str "Unknown dynamic: <" ++ str (Dyn.tag t) ++ str ">"))
1857
(* Interprets an application node *)
1858
and interp_app loc ist gl fv largs =
1860
| VFun(trace,olfun,var,body) ->
1861
let (newlfun,lvar,lval)=head_with_value (var,largs) in
1866
(val_interp { ist with lfun=newlfun@olfun; trace=trace } gl) body
1868
debugging_exception_step ist false e (fun () -> str "evaluation");
1870
debugging_step ist (fun () ->
1871
str "evaluation returns" ++ fnl() ++ pr_value (Some (pf_env gl)) v);
1872
if lval=[] then v else interp_app loc ist gl v lval
1874
VFun(trace,newlfun@olfun,lvar,body)
1876
user_err_loc (loc, "Tacinterp.interp_app",
1877
(str"Illegal tactic application."))
1879
(* Gives the tactic corresponding to the tactic value *)
1880
and tactic_of_value ist vle g =
1882
| VRTactic res -> res
1883
| VFun (trace,lfun,[],t) ->
1884
let tac = eval_tactic {ist with lfun=lfun; trace=trace} t in
1885
catch_error trace tac g
1886
| VFun _ -> error "A fully applied tactic is expected."
1887
| _ -> raise NotTactic
1889
(* Evaluation with FailError catching *)
1890
and eval_with_fail ist is_lazy goal tac =
1892
(match val_interp ist goal tac with
1893
| VFun (trace,lfun,[],t) when not is_lazy ->
1894
let tac = eval_tactic {ist with lfun=lfun; trace=trace} t in
1895
VRTactic (catch_error trace tac goal)
1898
| FailError (0,s) | Stdpp.Exc_located(_, FailError (0,s))
1899
| Stdpp.Exc_located(_,LtacLocated (_,FailError (0,s))) ->
1901
| FailError (lvl,s) -> raise (FailError (lvl - 1, s))
1902
| Stdpp.Exc_located(s,FailError (lvl,s')) ->
1903
raise (Stdpp.Exc_located(s,FailError (lvl - 1, s')))
1904
| Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) ->
1905
raise (Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl - 1, s'))))
1907
(* Interprets the clauses of a recursive LetIn *)
1908
and interp_letrec ist gl llc u =
1909
let lref = ref ist.lfun in
1910
let lve = list_map_left (fun ((_,id),b) -> (id,VRec (lref,TacArg b))) llc in
1911
lref := lve@ist.lfun;
1912
let ist = { ist with lfun = lve@ist.lfun } in
1915
(* Interprets the clauses of a LetIn *)
1916
and interp_letin ist gl llc u =
1917
let lve = list_map_left (fun ((_,id),body) ->
1918
let v = interp_tacarg ist gl body in check_is_value v; (id,v)) llc in
1919
let ist = { ist with lfun = lve@ist.lfun } in
1922
(* Interprets the Match Context expressions *)
1923
and interp_match_goal ist goal lz lr lmr =
1924
let hyps = pf_hyps goal in
1925
let hyps = if lr then List.rev hyps else hyps in
1926
let concl = pf_concl goal in
1927
let env = pf_env goal in
1928
let rec apply_goal_sub app ist (id,c) csr mt mhyps hyps =
1929
let rec match_next_pattern find_next () =
1930
let (lgoal,ctxt,find_next') = find_next () in
1931
let lctxt = give_context ctxt id in
1932
try apply_hyps_context ist env lz goal mt lctxt lgoal mhyps hyps
1933
with e when is_match_catchable e -> match_next_pattern find_next' () in
1934
match_next_pattern (fun () -> match_subterm_gen app c csr) () in
1935
let rec apply_match_goal ist env goal nrs lex lpt =
1937
if lex<>[] then db_pattern_rule ist.debug nrs (List.hd lex);
1941
db_mc_pattern_success ist.debug;
1942
try eval_with_fail ist lz goal t
1943
with e when is_match_catchable e ->
1944
apply_match_goal ist env goal (nrs+1) (List.tl lex) tl
1946
| (Pat (mhyps,mgoal,mt))::tl ->
1947
let mhyps = List.rev mhyps (* Sens naturel *) in
1951
let lmatch = extended_matches mg concl in
1952
db_matched_concl ist.debug env concl;
1953
apply_hyps_context ist env lz goal mt [] lmatch mhyps hyps
1954
with e when is_match_catchable e ->
1956
| PatternMatchingFailure -> db_matching_failure ist.debug
1957
| Eval_fail s -> db_eval_failure ist.debug s
1958
| _ -> db_logic_failure ist.debug e);
1959
apply_match_goal ist env goal (nrs+1) (List.tl lex) tl)
1960
| Subterm (b,id,mg) ->
1961
(try apply_goal_sub b ist (id,mg) concl mt mhyps hyps
1963
| PatternMatchingFailure ->
1964
apply_match_goal ist env goal (nrs+1) (List.tl lex) tl))
1966
errorlabstrm "Tacinterp.apply_match_goal"
1967
(v 0 (str "No matching clauses for match goal" ++
1968
(if ist.debug=DebugOff then
1969
fnl() ++ str "(use \"Set Ltac Debug\" for more info)"
1970
else mt()) ++ str"."))
1972
apply_match_goal ist env goal 0 lmr
1973
(read_match_rule (fst (constr_list ist env)) lmr)
1975
(* Tries to match the hypotheses in a Match Context *)
1976
and apply_hyps_context ist env lz goal mt lctxt lgmatch mhyps hyps =
1977
let rec apply_hyps_context_rec lfun lmatch lhyps_rest = function
1979
let (hypname, _, _ as hyp_pat) =
1981
| Hyp ((_,hypname),mhyp) -> hypname, None, mhyp
1982
| Def ((_,hypname),mbod,mhyp) -> hypname, Some mbod, mhyp
1984
let rec match_next_pattern find_next =
1985
let (lids,lm,hyp_match,find_next') = find_next () in
1986
db_matched_hyp ist.debug (pf_env goal) hyp_match hypname;
1988
let id_match = pi1 hyp_match in
1989
let nextlhyps = list_remove_assoc_in_triple id_match lhyps_rest in
1990
apply_hyps_context_rec (lfun@lids) lm nextlhyps tl
1991
with e when is_match_catchable e ->
1992
match_next_pattern find_next' in
1993
let init_match_pattern () =
1994
apply_one_mhyp_context ist env goal lmatch hyp_pat lhyps_rest in
1995
match_next_pattern init_match_pattern
1997
let lfun = extend_values_with_bindings lmatch (lfun@ist.lfun) in
1998
db_mc_pattern_success ist.debug;
1999
eval_with_fail {ist with lfun=lfun} lz goal mt
2001
apply_hyps_context_rec lctxt lgmatch hyps mhyps
2003
and interp_external loc ist gl com req la =
2004
let f ch = extern_request ch req gl la in
2005
let g ch = internalise_tacarg ch in
2006
interp_tacarg ist gl (System.connect f g com)
2008
(* Interprets extended tactic generic arguments *)
2009
and interp_genarg ist gl x =
2010
match genarg_tag x with
2011
| BoolArgType -> in_gen wit_bool (out_gen globwit_bool x)
2012
| IntArgType -> in_gen wit_int (out_gen globwit_int x)
2013
| IntOrVarArgType ->
2014
in_gen wit_int_or_var
2015
(ArgArg (interp_int_or_var ist (out_gen globwit_int_or_var x)))
2017
in_gen wit_string (out_gen globwit_string x)
2018
| PreIdentArgType ->
2019
in_gen wit_pre_ident (out_gen globwit_pre_ident x)
2020
| IntroPatternArgType ->
2021
in_gen wit_intro_pattern
2022
(interp_intro_pattern ist gl (out_gen globwit_intro_pattern x))
2024
in_gen (wit_ident_gen b)
2025
(interp_fresh_ident ist gl (out_gen (globwit_ident_gen b) x))
2027
in_gen wit_var (interp_hyp ist gl (out_gen globwit_var x))
2029
in_gen wit_ref (pf_interp_reference ist gl (out_gen globwit_ref x))
2033
(pf_interp_constr ist gl
2034
(RSort (dloc,out_gen globwit_sort x), None)))
2036
in_gen wit_constr (pf_interp_constr ist gl (out_gen globwit_constr x))
2037
| ConstrMayEvalArgType ->
2038
in_gen wit_constr_may_eval (interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x))
2039
| QuantHypArgType ->
2040
in_gen wit_quant_hyp
2041
(interp_declared_or_quantified_hypothesis ist gl
2042
(out_gen globwit_quant_hyp x))
2044
in_gen wit_red_expr (pf_interp_red_expr ist gl (out_gen globwit_red_expr x))
2045
| OpenConstrArgType casted ->
2046
in_gen (wit_open_constr_gen casted)
2047
(pf_interp_open_constr casted ist gl
2048
(snd (out_gen (globwit_open_constr_gen casted) x)))
2049
| ConstrWithBindingsArgType ->
2050
in_gen wit_constr_with_bindings
2051
(interp_constr_with_bindings ist gl (out_gen globwit_constr_with_bindings x))
2052
| BindingsArgType ->
2054
(interp_bindings ist gl (out_gen globwit_bindings x))
2055
| List0ArgType ConstrArgType -> interp_genarg_constr_list0 ist gl x
2056
| List1ArgType ConstrArgType -> interp_genarg_constr_list1 ist gl x
2057
| List0ArgType VarArgType -> interp_genarg_var_list0 ist gl x
2058
| List1ArgType VarArgType -> interp_genarg_var_list1 ist gl x
2059
| List0ArgType _ -> app_list0 (interp_genarg ist gl) x
2060
| List1ArgType _ -> app_list1 (interp_genarg ist gl) x
2061
| OptArgType _ -> app_opt (interp_genarg ist gl) x
2062
| PairArgType _ -> app_pair (interp_genarg ist gl) (interp_genarg ist gl) x
2064
match tactic_genarg_level s with
2066
(* Special treatment of tactic arguments *)
2067
in_gen (wit_tactic n) (out_gen (globwit_tactic n) x)
2069
lookup_interp_genarg s ist gl x
2071
and interp_genarg_constr_list0 ist gl x =
2072
let lc = out_gen (wit_list0 globwit_constr) x in
2073
let lc = pf_interp_constr_list ist gl lc in
2074
in_gen (wit_list0 wit_constr) lc
2076
and interp_genarg_constr_list1 ist gl x =
2077
let lc = out_gen (wit_list1 globwit_constr) x in
2078
let lc = pf_interp_constr_list ist gl lc in
2079
in_gen (wit_list1 wit_constr) lc
2081
and interp_genarg_var_list0 ist gl x =
2082
let lc = out_gen (wit_list0 globwit_var) x in
2083
let lc = interp_hyp_list ist gl lc in
2084
in_gen (wit_list0 wit_var) lc
2086
and interp_genarg_var_list1 ist gl x =
2087
let lc = out_gen (wit_list1 globwit_var) x in
2088
let lc = interp_hyp_list ist gl lc in
2089
in_gen (wit_list1 wit_var) lc
2091
(* Interprets the Match expressions *)
2092
and interp_match ist g lz constr lmr =
2093
let rec apply_match_subterm app ist (id,c) csr mt =
2094
let rec match_next_pattern find_next () =
2095
let (lmatch,ctxt,find_next') = find_next () in
2096
let lctxt = give_context ctxt id in
2097
let lfun = extend_values_with_bindings lmatch (lctxt@ist.lfun) in
2098
try eval_with_fail {ist with lfun=lfun} lz g mt
2099
with e when is_match_catchable e ->
2100
match_next_pattern find_next' () in
2101
match_next_pattern (fun () -> match_subterm_gen app c csr) () in
2102
let rec apply_match ist csr = function
2104
(try eval_with_fail ist lz g t
2105
with e when is_match_catchable e -> apply_match ist csr [])
2106
| (Pat ([],Term c,mt))::tl ->
2109
try extended_matches c csr
2111
debugging_exception_step ist false e (fun () ->
2112
str "matching with pattern" ++ fnl () ++
2113
pr_constr_pattern_env (pf_env g) c);
2116
let lfun = extend_values_with_bindings lmatch ist.lfun in
2117
eval_with_fail { ist with lfun=lfun } lz g mt
2119
debugging_exception_step ist false e (fun () ->
2120
str "rule body for pattern" ++
2121
pr_constr_pattern_env (pf_env g) c);
2123
with e when is_match_catchable e ->
2124
debugging_step ist (fun () -> str "switching to the next rule");
2125
apply_match ist csr tl)
2127
| (Pat ([],Subterm (b,id,c),mt))::tl ->
2128
(try apply_match_subterm b ist (id,c) csr mt
2129
with PatternMatchingFailure -> apply_match ist csr tl)
2131
errorlabstrm "Tacinterp.apply_match" (str
2132
"No matching clauses for match.") in
2134
try interp_ltac_constr ist g constr with e ->
2135
debugging_exception_step ist true e
2136
(fun () -> str "evaluation of the matched expression");
2138
let ilr = read_match_rule (fst (constr_list ist (pf_env g))) lmr in
2140
try apply_match ist csr ilr with e ->
2141
debugging_exception_step ist true e (fun () -> str "match expression");
2143
debugging_step ist (fun () ->
2144
str "match expression returns " ++ pr_value (Some (pf_env g)) res);
2147
(* Interprets tactic expressions : returns a "constr" *)
2148
and interp_ltac_constr ist gl e =
2150
try val_interp ist gl e with Not_found ->
2151
debugging_step ist (fun () ->
2152
str "evaluation failed for" ++ fnl() ++
2153
Pptactic.pr_glob_tactic (pf_env gl) e);
2156
let cresult = constr_of_value (pf_env gl) result in
2157
debugging_step ist (fun () ->
2158
Pptactic.pr_glob_tactic (pf_env gl) e ++ fnl() ++
2159
str " has value " ++ fnl() ++ print_constr_env (pf_env gl) cresult);
2163
(str "Must evaluate to a term" ++ fnl() ++
2164
str "offending expression: " ++ fnl() ++
2165
Pptactic.pr_glob_tactic (pf_env gl) e ++ fnl() ++ str "this is a " ++
2167
| VRTactic _ -> str "VRTactic"
2168
| VFun (_,il,ul,b) ->
2169
(str "VFun with body " ++ fnl() ++
2170
Pptactic.pr_glob_tactic (pf_env gl) b ++ fnl() ++
2171
str "instantiated arguments " ++ fnl() ++
2174
let (i,v) = p in str (string_of_id i) ++ str ", " ++ s)
2176
str "uninstantiated arguments " ++ fnl() ++
2180
Some id -> str (string_of_id id)
2181
| None -> str "_") ++ str ", " ++ s)
2183
| VVoid -> str "VVoid"
2184
| VInteger _ -> str "VInteger"
2185
| VConstr _ -> str "VConstr"
2186
| VIntroPattern _ -> str "VIntroPattern"
2187
| VConstr_context _ -> str "VConstrr_context"
2188
| VRec _ -> str "VRec"
2189
| VList _ -> str "VList") ++ str".")
2191
(* Interprets tactic expressions : returns a "tactic" *)
2192
and interp_tactic ist tac gl =
2193
try tactic_of_value ist (val_interp ist gl tac) gl
2194
with NotTactic -> errorlabstrm "" (str "Not a tactic.")
2196
(* Interprets a primitive tactic *)
2197
and interp_atomic ist gl = function
2199
| TacIntroPattern l ->
2200
h_intro_patterns (List.map (interp_intro_pattern ist gl) l)
2201
| TacIntrosUntil hyp ->
2202
h_intros_until (interp_quantified_hypothesis ist hyp)
2203
| TacIntroMove (ido,hto) ->
2204
h_intro_move (Option.map (interp_fresh_ident ist gl) ido)
2205
(interp_move_location ist gl hto)
2206
| TacAssumption -> h_assumption
2207
| TacExact c -> h_exact (pf_interp_casted_constr ist gl c)
2208
| TacExactNoCheck c -> h_exact_no_check (pf_interp_constr ist gl c)
2209
| TacVmCastNoCheck c -> h_vm_cast_no_check (pf_interp_constr ist gl c)
2210
| TacApply (a,ev,cb,None) ->
2211
h_apply a ev (List.map (interp_open_constr_with_bindings ist gl) cb)
2212
| TacApply (a,ev,cb,Some cl) ->
2213
h_apply_in a ev (List.map (interp_open_constr_with_bindings ist gl) cb)
2214
(interp_in_hyp_as ist gl cl)
2215
| TacElim (ev,cb,cbo) ->
2216
h_elim ev (interp_constr_with_bindings ist gl cb)
2217
(Option.map (interp_constr_with_bindings ist gl) cbo)
2218
| TacElimType c -> h_elim_type (pf_interp_type ist gl c)
2219
| TacCase (ev,cb) -> h_case ev (interp_constr_with_bindings ist gl cb)
2220
| TacCaseType c -> h_case_type (pf_interp_type ist gl c)
2221
| TacFix (idopt,n) -> h_fix (Option.map (interp_fresh_ident ist gl) idopt) n
2222
| TacMutualFix (b,id,n,l) ->
2223
let f (id,n,c) = (interp_fresh_ident ist gl id,n,pf_interp_type ist gl c)
2224
in h_mutual_fix b (interp_fresh_ident ist gl id) n (List.map f l)
2225
| TacCofix idopt -> h_cofix (Option.map (interp_fresh_ident ist gl) idopt)
2226
| TacMutualCofix (b,id,l) ->
2227
let f (id,c) = (interp_fresh_ident ist gl id,pf_interp_type ist gl c) in
2228
h_mutual_cofix b (interp_fresh_ident ist gl id) (List.map f l)
2229
| TacCut c -> h_cut (pf_interp_type ist gl c)
2230
| TacAssert (t,ipat,c) ->
2231
let c = (if t=None then interp_constr else interp_type) ist (project gl) (pf_env gl) c in
2232
abstract_tactic (TacAssert (t,ipat,inj_open c))
2233
(Tactics.forward (Option.map (interp_tactic ist) t)
2234
(Option.map (interp_intro_pattern ist gl) ipat) c)
2235
| TacGeneralize cl ->
2237
(pf_interp_constr_with_occurrences_and_name_as_list ist gl cl)
2238
| TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c)
2239
| TacLetTac (na,c,clp,b) ->
2240
let clp = interp_clause ist gl clp in
2241
h_let_tac b (interp_fresh_name ist gl na) (pf_interp_constr ist gl c) clp
2243
(* Automation tactics *)
2244
| TacTrivial (lems,l) ->
2245
Auto.h_trivial (pf_interp_constr_list ist gl lems)
2246
(Option.map (List.map (interp_hint_base ist)) l)
2247
| TacAuto (n,lems,l) ->
2248
Auto.h_auto (Option.map (interp_int_or_var ist) n)
2249
(pf_interp_constr_list ist gl lems)
2250
(Option.map (List.map (interp_hint_base ist)) l)
2251
| TacAutoTDB n -> Dhyp.h_auto_tdb n
2252
| TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (interp_hyp ist gl id)
2253
| TacDestructConcl -> Dhyp.h_destructConcl
2254
| TacSuperAuto (n,l,b1,b2) -> Auto.h_superauto n l b1 b2
2255
| TacDAuto (n,p,lems) ->
2256
Auto.h_dauto (Option.map (interp_int_or_var ist) n,p)
2257
(pf_interp_constr_list ist gl lems)
2259
(* Derived basic tactics *)
2260
| TacSimpleInductionDestruct (isrec,h) ->
2261
h_simple_induction_destruct isrec (interp_quantified_hypothesis ist h)
2262
| TacInductionDestruct (isrec,ev,l) ->
2263
h_induction_destruct ev isrec
2264
(List.map (fun (lc,cbo,(ipato,ipats),cls) ->
2265
(List.map (interp_induction_arg ist gl) lc,
2266
Option.map (interp_constr_with_bindings ist gl) cbo,
2267
(Option.map (interp_intro_pattern ist gl) ipato,
2268
Option.map (interp_intro_pattern ist gl) ipats),
2269
Option.map (interp_clause ist gl) cls)) l)
2270
| TacDoubleInduction (h1,h2) ->
2271
let h1 = interp_quantified_hypothesis ist h1 in
2272
let h2 = interp_quantified_hypothesis ist h2 in
2273
Elim.h_double_induction h1 h2
2274
| TacDecomposeAnd c -> Elim.h_decompose_and (pf_interp_constr ist gl c)
2275
| TacDecomposeOr c -> Elim.h_decompose_or (pf_interp_constr ist gl c)
2276
| TacDecompose (l,c) ->
2277
let l = List.map (interp_inductive ist) l in
2278
Elim.h_decompose l (pf_interp_constr ist gl c)
2279
| TacSpecialize (n,l) ->
2280
h_specialize n (interp_constr_with_bindings ist gl l)
2281
| TacLApply c -> h_lapply (pf_interp_constr ist gl c)
2283
(* Context management *)
2284
| TacClear (b,l) -> h_clear b (interp_hyp_list ist gl l)
2285
| TacClearBody l -> h_clear_body (interp_hyp_list ist gl l)
2286
| TacMove (dep,id1,id2) ->
2287
h_move dep (interp_hyp ist gl id1) (interp_move_location ist gl id2)
2289
h_rename (List.map (fun (id1,id2) ->
2290
interp_hyp ist gl id1,
2291
interp_fresh_ident ist gl (snd id2)) l)
2292
| TacRevert l -> h_revert (interp_hyp_list ist gl l)
2295
| TacLeft (ev,bl) -> h_left ev (interp_bindings ist gl bl)
2296
| TacRight (ev,bl) -> h_right ev (interp_bindings ist gl bl)
2297
| TacSplit (ev,_,bl) -> h_split ev (interp_bindings ist gl bl)
2298
| TacAnyConstructor (ev,t) ->
2299
abstract_tactic (TacAnyConstructor (ev,t))
2300
(Tactics.any_constructor ev (Option.map (interp_tactic ist) t))
2301
| TacConstructor (ev,n,bl) ->
2302
h_constructor ev (skip_metaid n) (interp_bindings ist gl bl)
2305
| TacReduce (r,cl) ->
2306
h_reduce (pf_interp_red_expr ist gl r) (interp_clause ist gl cl)
2307
| TacChange (occl,c,cl) ->
2308
h_change (Option.map (pf_interp_constr_with_occurrences ist gl) occl)
2309
(if occl = None & (cl.onhyps = None or cl.onhyps = Some []) &
2310
(cl.concl_occs = all_occurrences_expr or
2311
cl.concl_occs = no_occurrences_expr)
2312
then pf_interp_type ist gl c
2313
else pf_interp_constr ist gl c)
2314
(interp_clause ist gl cl)
2316
(* Equivalence relations *)
2317
| TacReflexivity -> h_reflexivity
2318
| TacSymmetry c -> h_symmetry (interp_clause ist gl c)
2319
| TacTransitivity c -> h_transitivity (pf_interp_constr ist gl c)
2321
(* Equality and inversion *)
2322
| TacRewrite (ev,l,cl,by) ->
2323
Equality.general_multi_multi_rewrite ev
2324
(List.map (fun (b,m,c) -> (b,m,interp_open_constr_with_bindings ist gl c)) l)
2325
(interp_clause ist gl cl)
2326
(Option.map (interp_tactic ist) by)
2327
| TacInversion (DepInversion (k,c,ids),hyp) ->
2328
Inv.dinv k (Option.map (pf_interp_constr ist gl) c)
2329
(Option.map (interp_intro_pattern ist gl) ids)
2330
(interp_declared_or_quantified_hypothesis ist gl hyp)
2331
| TacInversion (NonDepInversion (k,idl,ids),hyp) ->
2333
(Option.map (interp_intro_pattern ist gl) ids)
2334
(interp_hyp_list ist gl idl)
2335
(interp_declared_or_quantified_hypothesis ist gl hyp)
2336
| TacInversion (InversionUsing (c,idl),hyp) ->
2337
Leminv.lemInv_clause (interp_declared_or_quantified_hypothesis ist gl hyp)
2338
(pf_interp_constr ist gl c)
2339
(interp_hyp_list ist gl idl)
2341
(* For extensions *)
2342
| TacExtend (loc,opn,l) ->
2343
let tac = lookup_tactic opn in
2344
let args = List.map (interp_genarg ist gl) l in
2345
abstract_extended_tactic opn args (tac args)
2346
| TacAlias (loc,s,l,(_,body)) -> fun gl ->
2347
let rec f x = match genarg_tag x with
2349
VInteger (out_gen globwit_int x)
2350
| IntOrVarArgType ->
2351
mk_int_or_var_value ist (out_gen globwit_int_or_var x)
2352
| PreIdentArgType ->
2353
failwith "pre-identifiers cannot be bound"
2354
| IntroPatternArgType ->
2356
(snd (interp_intro_pattern ist gl (out_gen globwit_intro_pattern x)))
2360
(interp_fresh_ident ist gl (out_gen (globwit_ident_gen b) x)))
2362
mk_hyp_value ist gl (out_gen globwit_var x)
2364
VConstr (constr_of_global
2365
(pf_interp_reference ist gl (out_gen globwit_ref x)))
2367
VConstr (mkSort (interp_sort (out_gen globwit_sort x)))
2369
mk_constr_value ist gl (out_gen globwit_constr x)
2370
| ConstrMayEvalArgType ->
2372
(interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x))
2373
| ExtraArgType s when tactic_genarg_level s <> None ->
2374
(* Special treatment of tactic arguments *)
2376
(out_gen (globwit_tactic (Option.get (tactic_genarg_level s))) x)
2377
| List0ArgType ConstrArgType ->
2378
let wit = wit_list0 globwit_constr in
2379
VList (List.map (mk_constr_value ist gl) (out_gen wit x))
2380
| List0ArgType VarArgType ->
2381
let wit = wit_list0 globwit_var in
2382
VList (List.map (mk_hyp_value ist gl) (out_gen wit x))
2383
| List0ArgType IntArgType ->
2384
let wit = wit_list0 globwit_int in
2385
VList (List.map (fun x -> VInteger x) (out_gen wit x))
2386
| List0ArgType IntOrVarArgType ->
2387
let wit = wit_list0 globwit_int_or_var in
2388
VList (List.map (mk_int_or_var_value ist) (out_gen wit x))
2389
| List1ArgType ConstrArgType ->
2390
let wit = wit_list1 globwit_constr in
2391
VList (List.map (mk_constr_value ist gl) (out_gen wit x))
2392
| List1ArgType VarArgType ->
2393
let wit = wit_list1 globwit_var in
2394
VList (List.map (mk_hyp_value ist gl) (out_gen wit x))
2395
| List1ArgType IntArgType ->
2396
let wit = wit_list1 globwit_int in
2397
VList (List.map (fun x -> VInteger x) (out_gen wit x))
2398
| List1ArgType IntOrVarArgType ->
2399
let wit = wit_list1 globwit_int_or_var in
2400
VList (List.map (mk_int_or_var_value ist) (out_gen wit x))
2401
| StringArgType | BoolArgType
2402
| QuantHypArgType | RedExprArgType
2403
| OpenConstrArgType _ | ConstrWithBindingsArgType
2404
| ExtraArgType _ | BindingsArgType
2405
| OptArgType _ | PairArgType _
2406
| List0ArgType _ | List1ArgType _
2407
-> error "This generic type is not supported in alias."
2410
let lfun = (List.map (fun (x,c) -> (x,f c)) l)@ist.lfun in
2411
let trace = (loc,LtacNotationCall s)::ist.trace in
2412
interp_tactic { ist with lfun=lfun; trace=trace } body gl
2414
let make_empty_glob_sign () =
2415
{ ltacvars = ([],[]); ltacrecvars = [];
2416
gsigma = Evd.empty; genv = Global.env() }
2418
(* Initial call for interpretation *)
2419
let interp_tac_gen lfun avoid_ids debug t gl =
2420
interp_tactic { lfun=lfun; avoid_ids=avoid_ids; debug=debug; trace=[] }
2422
ltacvars = (List.map fst lfun, []); ltacrecvars = [];
2423
gsigma = project gl; genv = pf_env gl } t) gl
2425
let eval_tactic t gls =
2426
interp_tactic { lfun=[]; avoid_ids=[]; debug=get_debug(); trace=[] }
2429
let interp t = interp_tac_gen [] [] (get_debug()) t
2431
let eval_ltac_constr gl t =
2433
{ lfun=[]; avoid_ids=[]; debug=get_debug(); trace=[] } gl
2434
(intern_tactic (make_empty_glob_sign ()) t )
2436
(* Hides interpretation for pretty-print *)
2437
let hide_interp t ot gl =
2438
let ist = { ltacvars = ([],[]); ltacrecvars = [];
2439
gsigma = project gl; genv = pf_env gl } in
2440
let te = intern_tactic ist t in
2441
let t = eval_tactic te in
2443
| None -> abstract_tactic_expr (TacArg (Tacexp te)) t gl
2445
abstract_tactic_expr ~dflt:true (TacArg (Tacexp te)) (tclTHEN t t') gl
2447
(***************************************************************************)
2448
(* Substitution at module closing time *)
2450
let subst_quantified_hypothesis _ x = x
2452
let subst_declared_or_quantified_hypothesis _ x = x
2454
let subst_rawconstr_and_expr subst (c,e) =
2455
assert (e=None); (* e<>None only for toplevel tactics *)
2456
(Detyping.subst_rawconstr subst c,None)
2458
let subst_rawconstr = subst_rawconstr_and_expr (* shortening *)
2460
let subst_binding subst (loc,b,c) =
2461
(loc,subst_quantified_hypothesis subst b,subst_rawconstr subst c)
2463
let subst_bindings subst = function
2464
| NoBindings -> NoBindings
2465
| ImplicitBindings l -> ImplicitBindings (List.map (subst_rawconstr subst) l)
2466
| ExplicitBindings l -> ExplicitBindings (List.map (subst_binding subst) l)
2468
let subst_raw_with_bindings subst (c,bl) =
2469
(subst_rawconstr subst c, subst_bindings subst bl)
2471
let subst_induction_arg subst = function
2472
| ElimOnConstr c -> ElimOnConstr (subst_raw_with_bindings subst c)
2473
| ElimOnAnonHyp n as x -> x
2474
| ElimOnIdent id as x -> x
2476
let subst_and_short_name f (c,n) =
2477
(* assert (n=None); *)(* since tacdef are strictly globalized *)
2480
let subst_or_var f = function
2481
| ArgVar _ as x -> x
2482
| ArgArg x -> ArgArg (f x)
2484
let subst_located f (_loc,id) = (dloc,f id)
2486
let subst_reference subst =
2487
subst_or_var (subst_located (subst_kn subst))
2489
(*CSC: subst_global_reference is used "only" for RefArgType, that propagates
2490
to the syntactic non-terminals "global", used in commands such as
2491
Print. It is also used for non-evaluable references. *)
2492
let subst_global_reference subst =
2493
let subst_global ref =
2494
let ref',t' = subst_global subst ref in
2495
if not (eq_constr (constr_of_global ref') t') then
2496
ppnl (str "Warning: The reference " ++ pr_global ref ++ str " is not " ++
2497
str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++
2501
subst_or_var (subst_located subst_global)
2503
let subst_evaluable subst =
2504
let subst_eval_ref = subst_evaluable_reference subst in
2505
subst_or_var (subst_and_short_name subst_eval_ref)
2507
let subst_unfold subst (l,e) =
2508
(l,subst_evaluable subst e)
2510
let subst_flag subst red =
2511
{ red with rConst = List.map (subst_evaluable subst) red.rConst }
2513
let subst_constr_with_occurrences subst (l,c) = (l,subst_rawconstr subst c)
2515
let subst_redexp subst = function
2516
| Unfold l -> Unfold (List.map (subst_unfold subst) l)
2517
| Fold l -> Fold (List.map (subst_rawconstr subst) l)
2518
| Cbv f -> Cbv (subst_flag subst f)
2519
| Lazy f -> Lazy (subst_flag subst f)
2520
| Pattern l -> Pattern (List.map (subst_constr_with_occurrences subst) l)
2521
| Simpl o -> Simpl (Option.map (subst_constr_with_occurrences subst) o)
2522
| (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r
2524
let subst_raw_may_eval subst = function
2525
| ConstrEval (r,c) -> ConstrEval (subst_redexp subst r,subst_rawconstr subst c)
2526
| ConstrContext (locid,c) -> ConstrContext (locid,subst_rawconstr subst c)
2527
| ConstrTypeOf c -> ConstrTypeOf (subst_rawconstr subst c)
2528
| ConstrTerm c -> ConstrTerm (subst_rawconstr subst c)
2530
let subst_match_pattern subst = function
2531
| Subterm (b,ido,pc) -> Subterm (b,ido,subst_pattern subst pc)
2532
| Term pc -> Term (subst_pattern subst pc)
2534
let rec subst_match_goal_hyps subst = function
2535
| Hyp (locs,mp) :: tl ->
2536
Hyp (locs,subst_match_pattern subst mp)
2537
:: subst_match_goal_hyps subst tl
2538
| Def (locs,mv,mp) :: tl ->
2539
Def (locs,subst_match_pattern subst mv, subst_match_pattern subst mp)
2540
:: subst_match_goal_hyps subst tl
2543
let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
2545
| TacIntroPattern _ | TacIntrosUntil _ | TacIntroMove _ as x -> x
2546
| TacAssumption as x -> x
2547
| TacExact c -> TacExact (subst_rawconstr subst c)
2548
| TacExactNoCheck c -> TacExactNoCheck (subst_rawconstr subst c)
2549
| TacVmCastNoCheck c -> TacVmCastNoCheck (subst_rawconstr subst c)
2550
| TacApply (a,ev,cb,cl) ->
2551
TacApply (a,ev,List.map (subst_raw_with_bindings subst) cb,cl)
2552
| TacElim (ev,cb,cbo) ->
2553
TacElim (ev,subst_raw_with_bindings subst cb,
2554
Option.map (subst_raw_with_bindings subst) cbo)
2555
| TacElimType c -> TacElimType (subst_rawconstr subst c)
2556
| TacCase (ev,cb) -> TacCase (ev,subst_raw_with_bindings subst cb)
2557
| TacCaseType c -> TacCaseType (subst_rawconstr subst c)
2558
| TacFix (idopt,n) as x -> x
2559
| TacMutualFix (b,id,n,l) ->
2560
TacMutualFix(b,id,n,List.map (fun (id,n,c) -> (id,n,subst_rawconstr subst c)) l)
2561
| TacCofix idopt as x -> x
2562
| TacMutualCofix (b,id,l) ->
2563
TacMutualCofix (b,id, List.map (fun (id,c) -> (id,subst_rawconstr subst c)) l)
2564
| TacCut c -> TacCut (subst_rawconstr subst c)
2565
| TacAssert (b,na,c) ->
2566
TacAssert (Option.map (subst_tactic subst) b,na,subst_rawconstr subst c)
2567
| TacGeneralize cl ->
2568
TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl)
2569
| TacGeneralizeDep c -> TacGeneralizeDep (subst_rawconstr subst c)
2570
| TacLetTac (id,c,clp,b) -> TacLetTac (id,subst_rawconstr subst c,clp,b)
2572
(* Automation tactics *)
2573
| TacTrivial (lems,l) -> TacTrivial (List.map (subst_rawconstr subst) lems,l)
2574
| TacAuto (n,lems,l) -> TacAuto (n,List.map (subst_rawconstr subst) lems,l)
2575
| TacAutoTDB n -> TacAutoTDB n
2576
| TacDestructHyp (b,id) -> TacDestructHyp(b,id)
2577
| TacDestructConcl -> TacDestructConcl
2578
| TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2)
2579
| TacDAuto (n,p,lems) -> TacDAuto (n,p,List.map (subst_rawconstr subst) lems)
2581
(* Derived basic tactics *)
2582
| TacSimpleInductionDestruct (isrec,h) as x -> x
2583
| TacInductionDestruct (isrec,ev,l) ->
2584
TacInductionDestruct (isrec,ev,List.map (fun (lc,cbo,ids,cls) ->
2585
List.map (subst_induction_arg subst) lc,
2586
Option.map (subst_raw_with_bindings subst) cbo, ids, cls) l)
2587
| TacDoubleInduction (h1,h2) as x -> x
2588
| TacDecomposeAnd c -> TacDecomposeAnd (subst_rawconstr subst c)
2589
| TacDecomposeOr c -> TacDecomposeOr (subst_rawconstr subst c)
2590
| TacDecompose (l,c) ->
2591
let l = List.map (subst_or_var (subst_inductive subst)) l in
2592
TacDecompose (l,subst_rawconstr subst c)
2593
| TacSpecialize (n,l) -> TacSpecialize (n,subst_raw_with_bindings subst l)
2594
| TacLApply c -> TacLApply (subst_rawconstr subst c)
2596
(* Context management *)
2597
| TacClear _ as x -> x
2598
| TacClearBody l as x -> x
2599
| TacMove (dep,id1,id2) as x -> x
2600
| TacRename l as x -> x
2601
| TacRevert _ as x -> x
2604
| TacLeft (ev,bl) -> TacLeft (ev,subst_bindings subst bl)
2605
| TacRight (ev,bl) -> TacRight (ev,subst_bindings subst bl)
2606
| TacSplit (ev,b,bl) -> TacSplit (ev,b,subst_bindings subst bl)
2607
| TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (subst_tactic subst) t)
2608
| TacConstructor (ev,n,bl) -> TacConstructor (ev,n,subst_bindings subst bl)
2611
| TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl)
2612
| TacChange (occl,c,cl) ->
2613
TacChange (Option.map (subst_constr_with_occurrences subst) occl,
2614
subst_rawconstr subst c, cl)
2616
(* Equivalence relations *)
2617
| TacReflexivity | TacSymmetry _ as x -> x
2618
| TacTransitivity c -> TacTransitivity (subst_rawconstr subst c)
2620
(* Equality and inversion *)
2621
| TacRewrite (ev,l,cl,by) ->
2623
List.map (fun (b,m,c) ->
2624
b,m,subst_raw_with_bindings subst c) l,
2625
cl,Option.map (subst_tactic subst) by)
2626
| TacInversion (DepInversion (k,c,l),hyp) ->
2627
TacInversion (DepInversion (k,Option.map (subst_rawconstr subst) c,l),hyp)
2628
| TacInversion (NonDepInversion _,_) as x -> x
2629
| TacInversion (InversionUsing (c,cl),hyp) ->
2630
TacInversion (InversionUsing (subst_rawconstr subst c,cl),hyp)
2632
(* For extensions *)
2633
| TacExtend (_loc,opn,l) ->
2634
TacExtend (dloc,opn,List.map (subst_genarg subst) l)
2635
| TacAlias (_,s,l,(dir,body)) ->
2636
TacAlias (dloc,s,List.map (fun (id,a) -> (id,subst_genarg subst a)) l,
2637
(dir,subst_tactic subst body))
2639
and subst_tactic subst (t:glob_tactic_expr) = match t with
2640
| TacAtom (_loc,t) -> TacAtom (dloc, subst_atomic subst t)
2641
| TacFun tacfun -> TacFun (subst_tactic_fun subst tacfun)
2642
| TacLetIn (r,l,u) ->
2643
let l = List.map (fun (n,b) -> (n,subst_tacarg subst b)) l in
2644
TacLetIn (r,l,subst_tactic subst u)
2645
| TacMatchGoal (lz,lr,lmr) ->
2646
TacMatchGoal(lz,lr, subst_match_rule subst lmr)
2647
| TacMatch (lz,c,lmr) ->
2648
TacMatch (lz,subst_tactic subst c,subst_match_rule subst lmr)
2649
| TacId _ | TacFail _ as x -> x
2650
| TacProgress tac -> TacProgress (subst_tactic subst tac:glob_tactic_expr)
2651
| TacAbstract (tac,s) -> TacAbstract (subst_tactic subst tac,s)
2652
| TacThen (t1,tf,t2,tl) ->
2653
TacThen (subst_tactic subst t1,Array.map (subst_tactic subst) tf,
2654
subst_tactic subst t2,Array.map (subst_tactic subst) tl)
2655
| TacThens (t,tl) ->
2656
TacThens (subst_tactic subst t, List.map (subst_tactic subst) tl)
2657
| TacDo (n,tac) -> TacDo (n,subst_tactic subst tac)
2658
| TacTry tac -> TacTry (subst_tactic subst tac)
2659
| TacInfo tac -> TacInfo (subst_tactic subst tac)
2660
| TacRepeat tac -> TacRepeat (subst_tactic subst tac)
2661
| TacOrelse (tac1,tac2) ->
2662
TacOrelse (subst_tactic subst tac1,subst_tactic subst tac2)
2663
| TacFirst l -> TacFirst (List.map (subst_tactic subst) l)
2664
| TacSolve l -> TacSolve (List.map (subst_tactic subst) l)
2665
| TacComplete tac -> TacComplete (subst_tactic subst tac)
2666
| TacArg a -> TacArg (subst_tacarg subst a)
2668
and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body)
2670
and subst_tacarg subst = function
2671
| Reference r -> Reference (subst_reference subst r)
2672
| ConstrMayEval c -> ConstrMayEval (subst_raw_may_eval subst c)
2673
| MetaIdArg (_loc,_,_) -> assert false
2674
| TacCall (_loc,f,l) ->
2675
TacCall (_loc, subst_reference subst f, List.map (subst_tacarg subst) l)
2676
| TacExternal (_loc,com,req,la) ->
2677
TacExternal (_loc,com,req,List.map (subst_tacarg subst) la)
2678
| (TacVoid | IntroPattern _ | Integer _ | TacFreshId _) as x -> x
2679
| Tacexp t -> Tacexp (subst_tactic subst t)
2680
| TacDynamic(the_loc,t) as x ->
2682
| "tactic" | "value" -> x
2684
TacDynamic(the_loc, constr_in (subst_mps subst (constr_out t)))
2685
| s -> anomaly_loc (dloc, "Tacinterp.val_interp",
2686
str "Unknown dynamic: <" ++ str s ++ str ">"))
2688
(* Reads the rules of a Match Context or a Match *)
2689
and subst_match_rule subst = function
2691
(All (subst_tactic subst tc))::(subst_match_rule subst tl)
2692
| (Pat (rl,mp,tc))::tl ->
2693
let hyps = subst_match_goal_hyps subst rl in
2694
let pat = subst_match_pattern subst mp in
2695
Pat (hyps,pat,subst_tactic subst tc)
2696
::(subst_match_rule subst tl)
2699
and subst_genarg subst (x:glob_generic_argument) =
2700
match genarg_tag x with
2701
| BoolArgType -> in_gen globwit_bool (out_gen globwit_bool x)
2702
| IntArgType -> in_gen globwit_int (out_gen globwit_int x)
2703
| IntOrVarArgType -> in_gen globwit_int_or_var (out_gen globwit_int_or_var x)
2704
| StringArgType -> in_gen globwit_string (out_gen globwit_string x)
2705
| PreIdentArgType -> in_gen globwit_pre_ident (out_gen globwit_pre_ident x)
2706
| IntroPatternArgType ->
2707
in_gen globwit_intro_pattern (out_gen globwit_intro_pattern x)
2709
in_gen (globwit_ident_gen b) (out_gen (globwit_ident_gen b) x)
2710
| VarArgType -> in_gen globwit_var (out_gen globwit_var x)
2712
in_gen globwit_ref (subst_global_reference subst
2713
(out_gen globwit_ref x))
2715
in_gen globwit_sort (out_gen globwit_sort x)
2717
in_gen globwit_constr (subst_rawconstr subst (out_gen globwit_constr x))
2718
| ConstrMayEvalArgType ->
2719
in_gen globwit_constr_may_eval (subst_raw_may_eval subst (out_gen globwit_constr_may_eval x))
2720
| QuantHypArgType ->
2721
in_gen globwit_quant_hyp
2722
(subst_declared_or_quantified_hypothesis subst
2723
(out_gen globwit_quant_hyp x))
2725
in_gen globwit_red_expr (subst_redexp subst (out_gen globwit_red_expr x))
2726
| OpenConstrArgType b ->
2727
in_gen (globwit_open_constr_gen b)
2728
((),subst_rawconstr subst (snd (out_gen (globwit_open_constr_gen b) x)))
2729
| ConstrWithBindingsArgType ->
2730
in_gen globwit_constr_with_bindings
2731
(subst_raw_with_bindings subst (out_gen globwit_constr_with_bindings x))
2732
| BindingsArgType ->
2733
in_gen globwit_bindings
2734
(subst_bindings subst (out_gen globwit_bindings x))
2735
| List0ArgType _ -> app_list0 (subst_genarg subst) x
2736
| List1ArgType _ -> app_list1 (subst_genarg subst) x
2737
| OptArgType _ -> app_opt (subst_genarg subst) x
2738
| PairArgType _ -> app_pair (subst_genarg subst) (subst_genarg subst) x
2740
match tactic_genarg_level s with
2742
(* Special treatment of tactic arguments *)
2743
in_gen (globwit_tactic n)
2744
(subst_tactic subst (out_gen (globwit_tactic n) x))
2746
lookup_genarg_subst s subst x
2748
(***************************************************************************)
2749
(* Tactic registration *)
2751
(* For bad tactic calls *)
2752
let bad_tactic_args s =
2754
(str "Tactic " ++ str s ++ str " called with bad arguments")
2756
(* Declaration of the TAC-DEFINITION object *)
2757
let add (kn,td) = mactab := Gmap.add kn td !mactab
2758
let replace (kn,td) = mactab := Gmap.add kn td (Gmap.remove kn !mactab)
2760
type tacdef_kind = | NewTac of identifier
2761
| UpdateTac of ltac_constant
2763
let load_md i ((sp,kn),defs) =
2764
let dp,_ = repr_path sp in
2765
let mp,dir,_ = repr_kn kn in
2766
List.iter (fun (id,t) ->
2769
let sp = Libnames.make_path dp id in
2770
let kn = Names.make_kn mp dir (label_of_id id) in
2771
Nametab.push_tactic (Until i) sp kn;
2773
| UpdateTac kn -> replace (kn,t)) defs
2775
let open_md i((sp,kn),defs) =
2776
let dp,_ = repr_path sp in
2777
let mp,dir,_ = repr_kn kn in
2778
List.iter (fun (id,t) ->
2781
let sp = Libnames.make_path dp id in
2782
let kn = Names.make_kn mp dir (label_of_id id) in
2783
Nametab.push_tactic (Exactly i) sp kn
2784
| UpdateTac kn -> ()) defs
2786
let cache_md x = load_md 1 x
2788
let subst_kind subst id =
2791
| UpdateTac kn -> UpdateTac (Mod_subst.subst_kn subst kn)
2793
let subst_md (_,subst,defs) =
2794
List.map (fun (id,t) -> (subst_kind subst id,subst_tactic subst t)) defs
2797
declare_object {(default_object "TAC-DEFINITION") with
2798
cache_function = cache_md;
2799
load_function = load_md;
2800
open_function = open_md;
2801
subst_function = subst_md;
2802
classify_function = (fun (_,o) -> Substitute o);
2803
export_function = (fun x -> Some x)}
2807
let kn = Nametab.locate_tactic id in
2808
let t = lookup kn in
2809
str "Ltac" ++ spc() ++ pr_qualid id ++ str " :=" ++ spc() ++
2810
Pptactic.pr_glob_tactic (Global.env ()) t
2813
errorlabstrm "print_ltac"
2814
(pr_qualid id ++ spc() ++ str "is not a user defined tactic.")
2818
(* Adds a definition for tactics in the table *)
2819
let make_absolute_name ident repl =
2820
let loc = loc_of_reference ident in
2823
if repl then None, Nametab.locate_tactic (snd (qualid_of_reference ident))
2824
else let id = Pcoq.coerce_global_to_id ident in
2825
Some id, Lib.make_kn id
2827
if Gmap.mem kn !mactab then
2830
user_err_loc (loc,"Tacinterp.add_tacdef",
2831
str "There is already an Ltac named " ++ pr_reference ident ++ str".")
2832
else if is_atomic_kn kn then
2833
user_err_loc (loc,"Tacinterp.add_tacdef",
2834
str "Reserved Ltac name " ++ pr_reference ident ++ str".")
2837
user_err_loc (loc,"Tacinterp.add_tacdef",
2838
str "There is no Ltac named " ++ pr_reference ident ++ str".")
2840
let rec filter_map f l =
2841
let rec aux acc = function
2845
Some x -> aux (x :: acc) tl
2846
| None -> aux acc tl
2849
let add_tacdef isrec tacl =
2850
let rfun = List.map (fun (ident, b, _) -> make_absolute_name ident b) tacl in
2852
{(make_empty_glob_sign()) with ltacrecvars =
2853
if isrec then filter_map
2854
(function (Some id, qid) -> Some (id, qid) | (None, _) -> None) rfun
2857
List.map2 (fun (_,b,def) (id, qid) ->
2858
let k = if b then UpdateTac qid else NewTac (Option.get id) in
2859
let t = Flags.with_option strict_check (intern_tactic ist) def in
2862
let id0 = fst (List.hd rfun) in
2863
let _ = match id0 with Some id0 -> ignore(Lib.add_leaf id0 (inMD gtacl))
2864
| _ -> Lib.add_anonymous_leaf (inMD gtacl) in
2867
Flags.if_verbose msgnl (Libnames.pr_reference id ++
2868
(if b then str " is redefined"
2869
else str " is defined")))
2872
(***************************************************************************)
2873
(* Other entry points *)
2875
let glob_tactic x = intern_tactic (make_empty_glob_sign ()) x
2877
let glob_tactic_env l env x =
2878
Flags.with_option strict_check
2880
{ ltacvars = (l,[]); ltacrecvars = []; gsigma = Evd.empty; genv = env })
2883
let interp_redexp env sigma r =
2884
let ist = { lfun=[]; avoid_ids=[]; debug=get_debug (); trace=[] } in
2885
let gist = {(make_empty_glob_sign ()) with genv = env; gsigma = sigma } in
2886
interp_red_expr ist sigma env (intern_red_expr gist r)
2888
(***************************************************************************)
2889
(* Embed tactics in raw or glob tactic expr *)
2891
let globTacticIn t = TacArg (TacDynamic (dummy_loc,tactic_in t))
2892
let tacticIn t = globTacticIn (fun ist -> glob_tactic (t ist))
2894
let tacticOut = function
2895
| TacArg (TacDynamic (_,d)) ->
2896
if (tag d) = "tactic" then
2899
anomalylabstrm "tacticOut" (str "Dynamic tag should be tactic")
2901
anomalylabstrm "tacticOut"
2902
(str "Not a Dynamic ast: " (* ++ print_ast ast*) )
2904
(***************************************************************************)
2905
(* Backwarding recursive needs of tactic glob/interp/eval functions *)
2907
let _ = Auto.set_extern_interp
2909
let l = List.map (fun (id,c) -> (id,VConstr c)) l in
2910
interp_tactic {lfun=l;avoid_ids=[];debug=get_debug(); trace=[]})
2911
let _ = Auto.set_extern_intern_tac
2913
Flags.with_option strict_check
2914
(intern_tactic {(make_empty_glob_sign()) with ltacvars=(l,[])}))
2915
let _ = Auto.set_extern_subst_tactic subst_tactic
2916
let _ = Dhyp.set_extern_interp eval_tactic
2917
let _ = Dhyp.set_extern_intern_tac
2918
(fun t -> intern_tactic (make_empty_glob_sign()) t)
added
removed
tactics/tacinterp.ml
