aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extraargs.mlg2
-rw-r--r--plugins/ltac/g_auto.mlg50
-rw-r--r--plugins/ltac/g_ltac.mlg141
-rw-r--r--plugins/ltac/g_rewrite.mlg21
-rw-r--r--plugins/ltac/g_tactic.mlg19
-rw-r--r--plugins/ltac/pltac.ml6
-rw-r--r--plugins/ltac/pltac.mli4
-rw-r--r--plugins/ltac/pptactic.ml6
-rw-r--r--plugins/ltac/pptactic.mli2
-rw-r--r--plugins/ltac/rewrite.ml88
-rw-r--r--plugins/ltac/rewrite.mli2
-rw-r--r--plugins/ltac/taccoerce.ml9
-rw-r--r--plugins/ltac/tacentries.ml114
-rw-r--r--plugins/ltac/tacentries.mli3
-rw-r--r--plugins/ltac/tacintern.ml32
-rw-r--r--plugins/ltac/tacintern.mli3
-rw-r--r--plugins/ltac/tacinterp.ml25
-rw-r--r--plugins/ltac/tacinterp.mli7
18 files changed, 278 insertions, 256 deletions
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index ad4374dba3..ff4a82f864 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -41,7 +41,7 @@ let () = create_generic_quotation "ipattern" Pltac.simple_intropattern wit_simpl
let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Stdarg.wit_open_constr
let () =
let inject (loc, v) = Tacexpr.Tacexp v in
- Tacentries.create_ltac_quotation "ltac" inject (Pltac.tactic_expr, Some 5)
+ Tacentries.create_ltac_quotation "ltac" inject (Pltac.ltac_expr, Some 5)
(** Backward-compatible tactic notation entry names *)
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 44472a1995..7e8400910c 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -116,12 +116,25 @@ END
let make_depth n = snd (Eauto.make_dimension n None)
+(* deprecated in 8.13; the second int_or_var will be removed *)
+let deprecated_eauto_bfs =
+ CWarnings.create
+ ~name:"eauto_bfs" ~category:"deprecated"
+ (fun () -> Pp.str "The syntax [eauto @int_or_var @int_or_var] is deprecated. Use [bfs eauto] instead.")
+
+let deprecated_bfs tacname =
+ CWarnings.create
+ ~name:"eauto_bfs" ~category:"deprecated"
+ (fun () -> Pp.str "The syntax [" ++ Pp.str tacname ++ Pp.str "@int_or_var @int_or_var] is deprecated. No replacement yet.")
+
}
TACTIC EXTEND eauto
| [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
hintbases(db) ] ->
- { Eauto.gen_eauto (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
+ {
+ ( match n,p with Some _, Some _ -> deprecated_eauto_bfs () | _ -> () );
+ Eauto.gen_eauto (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
END
TACTIC EXTEND new_eauto
@@ -135,13 +148,17 @@ END
TACTIC EXTEND debug_eauto
| [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
hintbases(db) ] ->
- { Eauto.gen_eauto ~debug:Debug (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
+ {
+ ( match n,p with Some _, Some _ -> (deprecated_bfs "debug eauto") () | _ -> () );
+ Eauto.gen_eauto ~debug:Debug (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
END
TACTIC EXTEND info_eauto
| [ "info_eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
hintbases(db) ] ->
- { Eauto.gen_eauto ~debug:Info (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
+ {
+ ( match n,p with Some _, Some _ -> (deprecated_bfs "info_eauto") () | _ -> () );
+ Eauto.gen_eauto ~debug:Info (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
END
TACTIC EXTEND dfs_eauto
@@ -150,6 +167,12 @@ TACTIC EXTEND dfs_eauto
{ Eauto.gen_eauto (Eauto.make_dimension p None) (eval_uconstrs ist lems) db }
END
+TACTIC EXTEND bfs_eauto
+| [ "bfs" "eauto" int_or_var_opt(p) auto_using(lems)
+ hintbases(db) ] ->
+ { Eauto.gen_eauto (true, Eauto.make_depth p) (eval_uconstrs ist lems) db }
+END
+
TACTIC EXTEND autounfold
| [ "autounfold" hintbases(db) clause_dft_concl(cl) ] -> { Eauto.autounfold_tac db cl }
END
@@ -240,10 +263,21 @@ ARGUMENT EXTEND opthints
END
VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF
-| #[ locality = Attributes.locality; ] [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> {
- let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in
- let locality = if Locality.make_section_locality locality then Goptions.OptLocal else Goptions.OptGlobal in
- Hints.add_hints ~locality
- (match dbnames with None -> ["core"] | Some l -> l) entry;
+| #[ locality = Attributes.option_locality; ] [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> {
+ let open Goptions in
+ let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in
+ let () = match locality with
+ | OptGlobal ->
+ if Global.sections_are_opened () then
+ CErrors.user_err Pp.(str
+ "This command does not support the global attribute in sections.");
+ | OptExport ->
+ if Global.sections_are_opened () then
+ CErrors.user_err Pp.(str
+ "This command does not support the export attribute in sections.");
+ | OptDefault | OptLocal -> ()
+ in
+ Hints.add_hints ~locality
+ (match dbnames with None -> ["core"] | Some l -> l) entry;
}
END
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 6cf5d30a95..c2e95c45f9 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -74,22 +74,22 @@ let hint = G_proofs.hint
}
GRAMMAR EXTEND Gram
- GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg command hint
+ GLOBAL: tactic tacdef_body ltac_expr binder_tactic tactic_value command hint
tactic_mode constr_may_eval constr_eval toplevel_selector
- operconstr;
+ term;
tactic_then_last:
- [ [ "|"; lta = LIST0 (OPT tactic_expr) SEP "|" ->
+ [ [ "|"; lta = LIST0 (OPT ltac_expr) SEP "|" ->
{ Array.map (function None -> TacId [] | Some t -> t) (Array.of_list lta) }
| -> { [||] }
] ]
;
- tactic_then_gen:
- [ [ ta = tactic_expr; "|"; tg = tactic_then_gen -> { let (first,last) = tg in (ta::first, last) }
- | ta = tactic_expr; ".."; l = tactic_then_last -> { ([], Some (ta, l)) }
+ for_each_goal:
+ [ [ ta = ltac_expr; "|"; tg = for_each_goal -> { let (first,last) = tg in (ta::first, last) }
+ | ta = ltac_expr; ".."; l = tactic_then_last -> { ([], Some (ta, l)) }
| ".."; l = tactic_then_last -> { ([], Some (TacId [], l)) }
- | ta = tactic_expr -> { ([ta], None) }
- | "|"; tg = tactic_then_gen -> { let (first,last) = tg in (TacId [] :: first, last) }
+ | ta = ltac_expr -> { ([ta], None) }
+ | "|"; tg = for_each_goal -> { let (first,last) = tg in (TacId [] :: first, last) }
| -> { ([TacId []], None) }
] ]
;
@@ -97,13 +97,13 @@ GRAMMAR EXTEND Gram
for [TacExtend] *)
[ [ "[" ; l = OPT">" -> { if Option.is_empty l then true else false } ] ]
;
- tactic_expr:
+ ltac_expr:
[ "5" RIGHTA
[ te = binder_tactic -> { te } ]
| "4" LEFTA
- [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> { TacThen (ta0, ta1) }
- | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> { TacThen (ta0,ta1) }
- | ta0 = tactic_expr; ";"; l = tactic_then_locality; tg = tactic_then_gen; "]" -> {
+ [ ta0 = ltac_expr; ";"; ta1 = binder_tactic -> { TacThen (ta0, ta1) }
+ | ta0 = ltac_expr; ";"; ta1 = ltac_expr -> { TacThen (ta0,ta1) }
+ | ta0 = ltac_expr; ";"; l = tactic_then_locality; tg = for_each_goal; "]" -> {
let (first,tail) = tg in
match l , tail with
| false , Some (t,last) -> TacThen (ta0,TacExtendTac (Array.of_list first, t, last))
@@ -111,51 +111,51 @@ GRAMMAR EXTEND Gram
| false , None -> TacThen (ta0,TacDispatch first)
| true , None -> TacThens (ta0,first) } ]
| "3" RIGHTA
- [ IDENT "try"; ta = tactic_expr -> { TacTry ta }
- | IDENT "do"; n = int_or_var; ta = tactic_expr -> { TacDo (n,ta) }
- | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> { TacTimeout (n,ta) }
- | IDENT "time"; s = OPT string; ta = tactic_expr -> { TacTime (s,ta) }
- | IDENT "repeat"; ta = tactic_expr -> { TacRepeat ta }
- | IDENT "progress"; ta = tactic_expr -> { TacProgress ta }
- | IDENT "once"; ta = tactic_expr -> { TacOnce ta }
- | IDENT "exactly_once"; ta = tactic_expr -> { TacExactlyOnce ta }
- | IDENT "infoH"; ta = tactic_expr -> { TacShowHyps ta }
+ [ IDENT "try"; ta = ltac_expr -> { TacTry ta }
+ | IDENT "do"; n = int_or_var; ta = ltac_expr -> { TacDo (n,ta) }
+ | IDENT "timeout"; n = int_or_var; ta = ltac_expr -> { TacTimeout (n,ta) }
+ | IDENT "time"; s = OPT string; ta = ltac_expr -> { TacTime (s,ta) }
+ | IDENT "repeat"; ta = ltac_expr -> { TacRepeat ta }
+ | IDENT "progress"; ta = ltac_expr -> { TacProgress ta }
+ | IDENT "once"; ta = ltac_expr -> { TacOnce ta }
+ | IDENT "exactly_once"; ta = ltac_expr -> { TacExactlyOnce ta }
+ | IDENT "infoH"; ta = ltac_expr -> { TacShowHyps ta }
(*To do: put Abstract in Refiner*)
| IDENT "abstract"; tc = NEXT -> { TacAbstract (tc,None) }
| IDENT "abstract"; tc = NEXT; "using"; s = ident ->
{ TacAbstract (tc,Some s) }
- | sel = selector; ta = tactic_expr -> { TacSelect (sel, ta) } ]
+ | IDENT "only"; sel = selector; ":"; ta = ltac_expr -> { TacSelect (sel, ta) } ]
(*End of To do*)
| "2" RIGHTA
- [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> { TacOr (ta0,ta1) }
- | ta0 = tactic_expr; "+"; ta1 = tactic_expr -> { TacOr (ta0,ta1) }
- | IDENT "tryif" ; ta = tactic_expr ;
- "then" ; tat = tactic_expr ;
- "else" ; tae = tactic_expr -> { TacIfThenCatch(ta,tat,tae) }
- | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> { TacOrelse (ta0,ta1) }
- | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> { TacOrelse (ta0,ta1) } ]
+ [ ta0 = ltac_expr; "+"; ta1 = binder_tactic -> { TacOr (ta0,ta1) }
+ | ta0 = ltac_expr; "+"; ta1 = ltac_expr -> { TacOr (ta0,ta1) }
+ | IDENT "tryif" ; ta = ltac_expr ;
+ "then" ; tat = ltac_expr ;
+ "else" ; tae = ltac_expr -> { TacIfThenCatch(ta,tat,tae) }
+ | ta0 = ltac_expr; "||"; ta1 = binder_tactic -> { TacOrelse (ta0,ta1) }
+ | ta0 = ltac_expr; "||"; ta1 = ltac_expr -> { TacOrelse (ta0,ta1) } ]
| "1" RIGHTA
[ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" ->
{ TacMatchGoal (b,false,mrl) }
| b = match_key; IDENT "reverse"; IDENT "goal"; "with";
mrl = match_context_list; "end" ->
{ TacMatchGoal (b,true,mrl) }
- | b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" ->
+ | b = match_key; c = ltac_expr; "with"; mrl = match_list; "end" ->
{ TacMatch (b,c,mrl) }
- | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
+ | IDENT "first" ; "["; l = LIST0 ltac_expr SEP "|"; "]" ->
{ TacFirst l }
- | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
+ | IDENT "solve" ; "["; l = LIST0 ltac_expr SEP "|"; "]" ->
{ TacSolve l }
| IDENT "idtac"; l = LIST0 message_token -> { TacId l }
| g=failkw; n = [ n = int_or_var -> { n } | -> { fail_default_value } ];
l = LIST0 message_token -> { TacFail (g,n,l) }
| st = simple_tactic -> { st }
- | a = tactic_arg -> { TacArg(CAst.make ~loc a) }
- | r = reference; la = LIST0 tactic_arg_compat ->
+ | a = tactic_value -> { TacArg(CAst.make ~loc a) }
+ | r = reference; la = LIST0 tactic_arg ->
{ TacArg(CAst.make ~loc @@ TacCall (CAst.make ~loc (r,la))) } ]
| "0"
- [ "("; a = tactic_expr; ")" -> { a }
- | "["; ">"; tg = tactic_then_gen; "]" -> {
+ [ "("; a = ltac_expr; ")" -> { a }
+ | "["; ">"; tg = for_each_goal; "]" -> {
let (tf,tail) = tg in
begin match tail with
| Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl)
@@ -166,24 +166,24 @@ GRAMMAR EXTEND Gram
failkw:
[ [ IDENT "fail" -> { TacLocal } | IDENT "gfail" -> { TacGlobal } ] ]
;
- (* binder_tactic: level 5 of tactic_expr *)
+ (* binder_tactic: level 5 of ltac_expr *)
binder_tactic:
[ RIGHTA
- [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" ->
+ [ "fun"; it = LIST1 input_fun ; "=>"; body = ltac_expr LEVEL "5" ->
{ TacFun (it,body) }
| "let"; isrec = [IDENT "rec" -> { true } | -> { false } ];
llc = LIST1 let_clause SEP "with"; "in";
- body = tactic_expr LEVEL "5" -> { TacLetIn (isrec,llc,body) } ] ]
+ body = ltac_expr LEVEL "5" -> { TacLetIn (isrec,llc,body) } ] ]
;
(* Tactic arguments to the right of an application *)
- tactic_arg_compat:
- [ [ a = tactic_arg -> { a }
+ tactic_arg:
+ [ [ a = tactic_value -> { a }
| c = Constr.constr -> { (match c with { CAst.v = CRef (r,None) } -> Reference r | c -> ConstrMayEval (ConstrTerm c)) }
(* Unambiguous entries: tolerated w/o "ltac:" modifier *)
| "()" -> { TacGeneric (None, genarg_of_unit ()) } ] ]
;
(* Can be used as argument and at toplevel in tactic expressions. *)
- tactic_arg:
+ tactic_value:
[ [ c = constr_eval -> { ConstrMayEval c }
| IDENT "fresh"; l = LIST0 fresh_id -> { TacFreshId l }
| IDENT "type_term"; c=uconstr -> { TacPretype c }
@@ -223,20 +223,20 @@ GRAMMAR EXTEND Gram
| l = ident -> { Name.Name l } ] ]
;
let_clause:
- [ [ idr = identref; ":="; te = tactic_expr ->
+ [ [ idr = identref; ":="; te = ltac_expr ->
{ (CAst.map (fun id -> Name id) idr, arg_of_expr te) }
- | na = ["_" -> { CAst.make ~loc Anonymous } ]; ":="; te = tactic_expr ->
+ | na = ["_" -> { CAst.make ~loc Anonymous } ]; ":="; te = ltac_expr ->
{ (na, arg_of_expr te) }
- | idr = identref; args = LIST1 input_fun; ":="; te = tactic_expr ->
+ | idr = identref; args = LIST1 input_fun; ":="; te = ltac_expr ->
{ (CAst.map (fun id -> Name id) idr, arg_of_expr (TacFun(args,te))) } ] ]
;
match_pattern:
[ [ IDENT "context"; oid = OPT Constr.ident;
- "["; pc = Constr.lconstr_pattern; "]" ->
+ "["; pc = Constr.cpattern; "]" ->
{ Subterm (oid, pc) }
- | pc = Constr.lconstr_pattern -> { Term pc } ] ]
+ | pc = Constr.cpattern -> { Term pc } ] ]
;
- match_hyps:
+ match_hyp:
[ [ na = name; ":"; mp = match_pattern -> { Hyp (na, mp) }
| na = name; ":="; "["; mpv = match_pattern; "]"; ":"; mpt = match_pattern -> { Def (na, mpv, mpt) }
| na = name; ":="; mpv = match_pattern ->
@@ -250,19 +250,19 @@ GRAMMAR EXTEND Gram
] ]
;
match_context_rule:
- [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
- "=>"; te = tactic_expr -> { Pat (largs, mp, te) }
- | "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
- "]"; "=>"; te = tactic_expr -> { Pat (largs, mp, te) }
- | "_"; "=>"; te = tactic_expr -> { All te } ] ]
+ [ [ largs = LIST0 match_hyp SEP ","; "|-"; mp = match_pattern;
+ "=>"; te = ltac_expr -> { Pat (largs, mp, te) }
+ | "["; largs = LIST0 match_hyp SEP ","; "|-"; mp = match_pattern;
+ "]"; "=>"; te = ltac_expr -> { Pat (largs, mp, te) }
+ | "_"; "=>"; te = ltac_expr -> { All te } ] ]
;
match_context_list:
[ [ mrl = LIST1 match_context_rule SEP "|" -> { mrl }
| "|"; mrl = LIST1 match_context_rule SEP "|" -> { mrl } ] ]
;
match_rule:
- [ [ mp = match_pattern; "=>"; te = tactic_expr -> { Pat ([],mp,te) }
- | "_"; "=>"; te = tactic_expr -> { All te } ] ]
+ [ [ mp = match_pattern; "=>"; te = ltac_expr -> { Pat ([],mp,te) }
+ | "_"; "=>"; te = ltac_expr -> { All te } ] ]
;
match_list:
[ [ mrl = LIST1 match_rule SEP "|" -> { mrl }
@@ -282,13 +282,13 @@ GRAMMAR EXTEND Gram
(* Definitions for tactics *)
tacdef_body:
[ [ name = Constr.global; it=LIST1 input_fun;
- redef = ltac_def_kind; body = tactic_expr ->
+ redef = ltac_def_kind; body = ltac_expr ->
{ if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body))
else
let id = reference_to_id name in
Tacexpr.TacticDefinition (id, TacFun (it, body)) }
| name = Constr.global; redef = ltac_def_kind;
- body = tactic_expr ->
+ body = ltac_expr ->
{ if redef then Tacexpr.TacticRedefinition (name, body)
else
let id = reference_to_id name in
@@ -296,7 +296,7 @@ GRAMMAR EXTEND Gram
] ]
;
tactic:
- [ [ tac = tactic_expr -> { tac } ] ]
+ [ [ tac = ltac_expr -> { tac } ] ]
;
range_selector:
@@ -314,15 +314,12 @@ GRAMMAR EXTEND Gram
{ let open Goal_select in
Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l } ] ]
;
- selector_body:
+ selector:
[ [ l = range_selector_or_nth -> { l }
| test_bracket_ident; "["; id = ident; "]" -> { Goal_select.SelectId id } ] ]
;
- selector:
- [ [ IDENT "only"; sel = selector_body; ":" -> { sel } ] ]
- ;
toplevel_selector:
- [ [ sel = selector_body; ":" -> { sel }
+ [ [ sel = selector; ":" -> { sel }
| "!"; ":" -> { Goal_select.SelectAlreadyFocused }
| IDENT "all"; ":" -> { Goal_select.SelectAll } ] ]
;
@@ -332,19 +329,19 @@ GRAMMAR EXTEND Gram
;
command:
[ [ IDENT "Proof"; "with"; ta = Pltac.tactic;
- l = OPT [ "using"; l = G_vernac.section_subset_expr -> { l } ] ->
+ l = OPT [ IDENT "using"; l = G_vernac.section_subset_expr -> { l } ] ->
{ Vernacexpr.VernacProof (Some (in_tac ta), l) }
- | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr;
- ta = OPT [ "with"; ta = Pltac.tactic -> { in_tac ta } ] ->
- { Vernacexpr.VernacProof (ta,Some l) } ] ]
+ | IDENT "Proof"; IDENT "using"; l = G_vernac.section_subset_expr;
+ "with"; ta = Pltac.tactic ->
+ { Vernacexpr.VernacProof (Some (in_tac ta),Some l) } ] ]
;
hint:
[ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>";
tac = Pltac.tactic ->
{ Vernacexpr.HintsExtern (n,c, in_tac tac) } ] ]
;
- operconstr: LEVEL "0"
- [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" ->
+ term: LEVEL "0"
+ [ [ IDENT "ltac"; ":"; "("; tac = Pltac.ltac_expr; ")" ->
{ let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in
CAst.make ~loc @@ CHole (None, IntroAnonymous, Some arg) } ] ]
;
@@ -402,7 +399,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve STATE proof
{ classify_as_proofstep } -> {
let g = Option.default (Goal_select.get_default_goal_selector ()) g in
let global = match g with Goal_select.SelectAll | Goal_select.SelectList _ -> true | _ -> false in
- let t = ComTactic.I (Tacinterp.hide_interp, { Tacinterp.global; ast = t; }) in
+ let t = Tacinterp.hide_interp { Tacinterp.global; ast = t; } in
ComTactic.solve g ~info t ~with_end_tac
}
END
@@ -415,7 +412,7 @@ VERNAC { tactic_mode } EXTEND VernacSolveParallel STATE proof
VtProofStep{ proof_block_detection = pbr }
} -> {
let t, abstract = rm_abstract t in
- let t = ComTactic.I (Tacinterp.hide_interp, { Tacinterp.global = true; ast = t; }) in
+ let t = Tacinterp.hide_interp { Tacinterp.global = true; ast = t; } in
ComTactic.solve_parallel ~info t ~abstract ~with_end_tac
}
END
@@ -469,7 +466,7 @@ END
VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY
| [ "Print" "Ltac" reference(r) ] ->
- { Feedback.msg_notice (Tacintern.print_ltac r) }
+ { Feedback.msg_notice (Tacentries.print_ltac r) }
END
VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index ee94fd565a..a3f03b5bb5 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -67,12 +67,12 @@ END
{
type raw_strategy = (constr_expr, Tacexpr.raw_red_expr) strategy_ast
-type glob_strategy = (glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast
+type glob_strategy = (glob_constr_and_expr, Tacexpr.glob_red_expr) strategy_ast
let interp_strategy ist gl s =
let sigma = project gl in
- sigma, strategy_of_ast s
-let glob_strategy ist s = map_strategy (Tacintern.intern_constr ist) (fun c -> c) s
+ sigma, strategy_of_ast ist s
+let glob_strategy ist s = map_strategy (Tacintern.intern_constr ist) (Tacintern.intern_red_expr ist) s
let subst_strategy s str = str
let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>"
@@ -80,12 +80,9 @@ let pr_raw_strategy env sigma prc prlc _ (s : raw_strategy) =
let prr = Pptactic.pr_red_expr env sigma (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_qualid, prc) in
Rewrite.pr_strategy (prc env sigma) prr s
let pr_glob_strategy env sigma prc prlc _ (s : glob_strategy) =
- let prr = Pptactic.pr_red_expr env sigma
- (Ppconstr.pr_constr_expr,
- Ppconstr.pr_lconstr_expr,
- Pputils.pr_or_by_notation Libnames.pr_qualid,
- Ppconstr.pr_constr_expr)
- in
+ let prpat env sigma (_,c,_) = prc env sigma c in
+ let prcst = Pputils.pr_or_var Pptactic.(pr_and_short_name (pr_evaluable_reference_env env)) in
+ let prr = Pptactic.pr_red_expr env sigma (prc, prlc, prcst, prpat) in
Rewrite.pr_strategy (prc env sigma) prr s
}
@@ -130,15 +127,15 @@ END
{
let db_strat db = StratUnary (Topdown, StratHints (false, db))
-let cl_rewrite_clause_db db = cl_rewrite_clause_strat (strategy_of_ast (db_strat db))
+let cl_rewrite_clause_db ist db = cl_rewrite_clause_strat (strategy_of_ast ist (db_strat db))
}
TACTIC EXTEND rewrite_strat
| [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> { cl_rewrite_clause_strat s (Some id) }
| [ "rewrite_strat" rewstrategy(s) ] -> { cl_rewrite_clause_strat s None }
-| [ "rewrite_db" preident(db) "in" hyp(id) ] -> { cl_rewrite_clause_db db (Some id) }
-| [ "rewrite_db" preident(db) ] -> { cl_rewrite_clause_db db None }
+| [ "rewrite_db" preident(db) "in" hyp(id) ] -> { cl_rewrite_clause_db ist db (Some id) }
+| [ "rewrite_db" preident(db) ] -> { cl_rewrite_clause_db ist db None }
END
{
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index c186a83a5c..236de65462 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -121,8 +121,8 @@ let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
end
| _ -> ElimOnConstr clbind
-let mkNumeral n =
- Numeral (NumTok.Signed.of_int_string (string_of_int n))
+let mkNumber n =
+ Number (NumTok.Signed.of_int_string (string_of_int n))
let mkTacCase with_evar = function
| [(clear,ElimOnConstr cl),(None,None),None],None ->
@@ -130,7 +130,7 @@ let mkTacCase with_evar = function
(* Reinterpret numbers as a notation for terms *)
| [(clear,ElimOnAnonHyp n),(None,None),None],None ->
TacCase (with_evar,
- (clear,(CAst.make @@ CPrim (mkNumeral n),
+ (clear,(CAst.make @@ CPrim (mkNumber n),
NoBindings)))
(* Reinterpret ident as notations for variables in the context *)
(* because we don't know if they are quantified or not *)
@@ -291,7 +291,7 @@ GRAMMAR EXTEND Gram
;
simple_intropattern:
[ [ pat = simple_intropattern_closed;
- l = LIST0 ["%"; c = operconstr LEVEL "0" -> { c } ] ->
+ l = LIST0 ["%"; c = term LEVEL "0" -> { c } ] ->
{ let {CAst.loc=loc0;v=pat} = pat in
let f c pat =
let loc1 = Constrexpr_ops.constr_loc c in
@@ -320,7 +320,7 @@ GRAMMAR EXTEND Gram
with_bindings:
[ [ "with"; bl = bindings -> { bl } | -> { NoBindings } ] ]
;
- red_flags:
+ red_flag:
[ [ IDENT "beta" -> { [FBeta] }
| IDENT "iota" -> { [FMatch;FFix;FCofix] }
| IDENT "match" -> { [FMatch] }
@@ -337,7 +337,7 @@ GRAMMAR EXTEND Gram
] ]
;
strategy_flag:
- [ [ s = LIST1 red_flags -> { Redops.make_red_flag (List.flatten s) }
+ [ [ s = LIST1 red_flag -> { Redops.make_red_flag (List.flatten s) }
| d = delta_flag -> { all_with d }
] ]
;
@@ -450,6 +450,11 @@ GRAMMAR EXTEND Gram
;
as_or_and_ipat:
[ [ "as"; ipat = or_and_intropattern_loc -> { Some ipat }
+ | "as"; ipat = equality_intropattern ->
+ { match ipat with
+ | IntroRewrite _ -> user_err Pp.(str "Disjunctive/conjunctive pattern expected.")
+ | IntroInjection _ -> user_err Pp.(strbrk "Found an injection pattern while a disjunctive/conjunctive pattern was expected; use " ++ str "\"injection as pattern\"" ++ strbrk " instead.")
+ | _ -> assert false }
| -> { None } ] ]
;
eqn_ipat:
@@ -460,7 +465,7 @@ GRAMMAR EXTEND Gram
[ [ "as"; id = ident -> { Names.Name.Name id } | -> { Names.Name.Anonymous } ] ]
;
by_tactic:
- [ [ "by"; tac = tactic_expr LEVEL "3" -> { Some tac }
+ [ [ "by"; tac = ltac_expr LEVEL "3" -> { Some tac }
| -> { None } ] ]
;
rewriter :
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index b7b54143df..94e398fe5d 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -37,8 +37,10 @@ let clause_dft_concl =
(* Main entries for ltac *)
-let tactic_arg = Entry.create "tactic_arg"
-let tactic_expr = Entry.create "tactic_expr"
+let tactic_value = Entry.create "tactic_value"
+let tactic_arg = tactic_value
+let ltac_expr = Entry.create "ltac_expr"
+let tactic_expr = ltac_expr
let binder_tactic = Entry.create "binder_tactic"
let tactic = Entry.create "tactic"
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 8565c4b4d6..3a4a081c93 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -31,8 +31,12 @@ val simple_tactic : raw_tactic_expr Entry.t
val simple_intropattern : constr_expr intro_pattern_expr CAst.t Entry.t
val in_clause : Names.lident Locus.clause_expr Entry.t
val clause_dft_concl : Names.lident Locus.clause_expr Entry.t
+val tactic_value : raw_tactic_arg Entry.t
val tactic_arg : raw_tactic_arg Entry.t
+ [@@deprecated "Deprecated in 8.13; use 'tactic_value' instead"]
+val ltac_expr : raw_tactic_expr Entry.t
val tactic_expr : raw_tactic_expr Entry.t
+ [@@deprecated "Deprecated in 8.13; use 'ltac_expr' instead"]
val binder_tactic : raw_tactic_expr Entry.t
val tactic : raw_tactic_expr Entry.t
val tactic_eoi : raw_tactic_expr Entry.t
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index fe896f9351..edd56ee0f7 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1135,8 +1135,8 @@ let pr_goal_selector ~toplevel s =
pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env));
pr_lconstr = (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env));
pr_pattern = (fun env sigma -> pr_pat_and_constr_expr (pr_glob_constr_env env));
- pr_lpattern = (fun env sigma -> pr_pat_and_constr_expr (pr_lglob_constr_env env));
pr_constant = pr_or_var (pr_and_short_name (pr_evaluable_reference_env env));
+ pr_lpattern = (fun env sigma -> pr_pat_and_constr_expr (pr_lglob_constr_env env));
pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant);
pr_name = pr_lident;
pr_generic = Pputils.pr_glb_generic;
@@ -1334,8 +1334,8 @@ let () =
;
Genprint.register_print0
wit_constr
- (lift_env Ppconstr.pr_lconstr_expr)
- (lift_env (fun env sigma (c, _) -> pr_lglob_constr_pptac env sigma c))
+ (lift_env Ppconstr.pr_constr_expr)
+ (lift_env (fun env sigma (c, _) -> pr_glob_constr_pptac env sigma c))
(make_constr_printer Printer.pr_econstr_n_env)
;
Genprint.register_print0
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 6a9fb5c2ea..5e199dad62 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -8,7 +8,7 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-(** This module implements pretty-printers for tactic_expr syntactic
+(** This module implements pretty-printers for ltac_expr syntactic
objects and their subcomponents. *)
open Genarg
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index ff24e38577..8196ba6555 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -769,7 +769,7 @@ let get_rew_prf evars r = match r.rew_prf with
let poly_subrelation sort =
if sort then PropGlobal.subrelation else TypeGlobal.subrelation
-let resolve_subrelation env avoid car rel sort prf rel' res =
+let resolve_subrelation env car rel sort prf rel' res =
if Termops.eq_constr (fst res.rew_evars) rel rel' then res
else
let evars, app = app_poly_check env res.rew_evars (poly_subrelation sort) [|car; rel; rel'|] in
@@ -779,7 +779,7 @@ let resolve_subrelation env avoid car rel sort prf rel' res =
rew_prf = RewPrf (rel', appsub);
rew_evars = evars }
-let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) evars =
+let resolve_morphism env m args args' (b,cstr) evars =
let evars, morph_instance, proj, sigargs, m', args, args' =
let first = match (Array.findi (fun _ b -> not (Option.is_empty b)) args') with
| Some i -> i
@@ -843,18 +843,18 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
let proof = applist (proj, List.rev projargs) in
let newt = applist (m', List.rev typeargs) in
match respars with
- [ a, Some r ] -> evars, proof, substl subst a, substl subst r, oldt, fnewt newt
+ [ a, Some r ] -> evars, proof, substl subst a, substl subst r, newt
| _ -> assert(false)
-let apply_constraint env avoid car rel prf cstr res =
+let apply_constraint env car rel prf cstr res =
match snd cstr with
| None -> res
- | Some r -> resolve_subrelation env avoid car rel (fst cstr) prf r res
+ | Some r -> resolve_subrelation env car rel (fst cstr) prf r res
-let coerce env avoid cstr res =
+let coerce env cstr res =
let evars, (rel, prf) = get_rew_prf res.rew_evars res in
let res = { res with rew_evars = evars } in
- apply_constraint env avoid res.rew_car rel prf cstr res
+ apply_constraint env res.rew_car rel prf cstr res
let apply_rule unify loccs : int pure_strategy =
let (nowhere_except_in,occs) = convert_occs loccs in
@@ -863,7 +863,7 @@ let apply_rule unify loccs : int pure_strategy =
then List.mem occ occs
else not (List.mem occ occs)
in
- { strategy = fun { state = occ ; env ; unfresh ;
+ { strategy = fun { state = occ ; env ;
term1 = t ; ty1 = ty ; cstr ; evars } ->
let unif = if isEvar (goalevars evars) t then None else unify env evars t in
match unif with
@@ -874,7 +874,7 @@ let apply_rule unify loccs : int pure_strategy =
else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occ, Identity)
else
let res = { rew with rew_car = ty } in
- let res = Success (coerce env unfresh cstr res) in
+ let res = Success (coerce env cstr res) in
(occ, res)
}
@@ -968,7 +968,7 @@ let fold_match ?(force=false) env sigma c =
let unfold_match env sigma sk app =
match EConstr.kind sigma app with
- | App (f', args) when Constant.equal (fst (destConst sigma f')) sk ->
+ | App (f', args) when QConstant.equal env (fst (destConst sigma f')) sk ->
let v = Environ.constant_value_in (Global.env ()) (sk,Univ.Instance.empty)(*FIXME*) in
let v = EConstr.of_constr v in
Reductionops.whd_beta env sigma (mkApp (v, args))
@@ -1017,10 +1017,10 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
| None -> false
| Some r -> not (is_rew_cast r.rew_prf)) args'
then
- let evars', prf, car, rel, c1, c2 =
- resolve_morphism env unfresh t m args args' (prop, cstr') evars'
+ let evars', prf, car, rel, c2 =
+ resolve_morphism env m args args' (prop, cstr') evars'
in
- let res = { rew_car = ty; rew_from = c1;
+ let res = { rew_car = ty; rew_from = t;
rew_to = c2; rew_prf = RewPrf (rel, prf);
rew_evars = evars' }
in Success res
@@ -1071,7 +1071,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
let res =
match prf with
| RewPrf (rel, prf) ->
- Success (apply_constraint env unfresh res.rew_car
+ Success (apply_constraint env res.rew_car
rel prf (prop,cstr) res)
| _ -> Success res
in state, res
@@ -1094,20 +1094,6 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
| Fail | Identity -> res
in state, res
- (* if x' = None && flags.under_lambdas then *)
- (* let lam = mkLambda (n, x, b) in *)
- (* let lam', occ = aux env lam occ None in *)
- (* let res = *)
- (* match lam' with *)
- (* | None -> None *)
- (* | Some (prf, (car, rel, c1, c2)) -> *)
- (* Some (resolve_morphism env sigma t *)
- (* ~fnewt:unfold_all *)
- (* (Lazy.force coq_all) [| x ; lam |] [| None; lam' |] *)
- (* cstr evars) *)
- (* in res, occ *)
- (* else *)
-
| Prod (n, dom, codom) ->
let lam = mkLambda (n, dom, codom) in
let (evars', app), unfold =
@@ -1131,31 +1117,13 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
B. Barras' idea is to have a context of relations, of length 1, with Σ for gluing
dependent relations and using projections to get them out.
*)
- (* | Lambda (n, t, b) when flags.under_lambdas -> *)
- (* let n' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n in *)
- (* let n'' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n' in *)
- (* let n''' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n'' in *)
- (* let rel = new_cstr_evar cstr env (mkApp (Lazy.force coq_relation, [|t|])) in *)
- (* let env' = Environ.push_rel_context [(n'',None,lift 2 rel);(n'',None,lift 1 t);(n', None, t)] env in *)
- (* let b' = s env' avoid b (Typing.type_of env' (goalevars evars) (lift 2 b)) (unlift_cstr env (goalevars evars) cstr) evars in *)
- (* (match b' with *)
- (* | Some (Some r) -> *)
- (* let prf = match r.rew_prf with *)
- (* | RewPrf (rel, prf) -> *)
- (* let rel = pointwise_or_dep_relation n' t r.rew_car rel in *)
- (* let prf = mkLambda (n', t, prf) in *)
- (* RewPrf (rel, prf) *)
- (* | x -> x *)
- (* in *)
- (* Some (Some { r with *)
- (* rew_prf = prf; *)
- (* rew_car = mkProd (n, t, r.rew_car); *)
- (* rew_from = mkLambda(n, t, r.rew_from); *)
- (* rew_to = mkLambda (n, t, r.rew_to) }) *)
- (* | _ -> b') *)
| Lambda (n, t, b) when flags.under_lambdas ->
let n' = map_annot (Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env)) n in
+ let unfresh = match n'.binder_name with
+ | Anonymous -> unfresh
+ | Name id -> Id.Set.add id unfresh
+ in
let open Context.Rel.Declaration in
let env' = EConstr.push_rel (LocalAssum (n', t)) env in
let bty = Retyping.get_type_of env' (goalevars evars) b in
@@ -1196,7 +1164,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
| Success r ->
let case = mkCase (ci, lift 1 p, map_invert (lift 1) iv, mkRel 1, Array.map (lift 1) brs) in
let res = make_leibniz_proof env case ty r in
- state, Success (coerce env unfresh (prop,cstr) res)
+ state, Success (coerce env (prop,cstr) res)
| Fail | Identity ->
if Array.for_all (Int.equal 0) ci.ci_cstr_ndecls then
let evars', eqty = app_poly_sort prop env evars coq_eq [| ty |] in
@@ -1237,7 +1205,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
in
let res =
match res with
- | Success r -> Success (coerce env unfresh (prop,cstr) r)
+ | Success r -> Success (coerce env (prop,cstr) r)
| Fail | Identity -> res
in state, res
| _ -> state, Fail
@@ -1671,9 +1639,9 @@ let cl_rewrite_clause l left2right occs clause =
let cl_rewrite_clause_strat strat clause =
cl_rewrite_clause_strat false strat clause
-let apply_glob_constr c l2r occs = (); fun ({ state = () ; env = env } as input) ->
+let apply_glob_constr ist c l2r occs = (); fun ({ state = () ; env = env } as input) ->
let c sigma =
- let (sigma, c) = Pretyping.understand_tcc env sigma c in
+ let (sigma, c) = Tacinterp.interp_open_constr ist env sigma c in
(sigma, (c, NoBindings))
in
let flags = general_rewrite_unif_flags () in
@@ -1750,12 +1718,12 @@ let rec pr_strategy prc prr = function
| StratEval r -> str "eval" ++ spc () ++ prr r
| StratFold c -> str "fold" ++ spc () ++ prc c
-let rec strategy_of_ast = function
+let rec strategy_of_ast ist = function
| StratId -> Strategies.id
| StratFail -> Strategies.fail
| StratRefl -> Strategies.refl
| StratUnary (f, s) ->
- let s' = strategy_of_ast s in
+ let s' = strategy_of_ast ist s in
let f' = match f with
| Subterms -> all_subterms
| Subterm -> one_subterm
@@ -1769,13 +1737,13 @@ let rec strategy_of_ast = function
| Repeat -> Strategies.repeat
in f' s'
| StratBinary (f, s, t) ->
- let s' = strategy_of_ast s in
- let t' = strategy_of_ast t in
+ let s' = strategy_of_ast ist s in
+ let t' = strategy_of_ast ist t in
let f' = match f with
| Compose -> Strategies.seq
| Choice -> Strategies.choice
in f' s' t'
- | StratConstr (c, b) -> { strategy = apply_glob_constr (fst c) b AllOccurrences }
+ | StratConstr (c, b) -> { strategy = apply_glob_constr ist c b AllOccurrences }
| StratHints (old, id) -> if old then Strategies.old_hints id else Strategies.hints id
| StratTerms l -> { strategy =
(fun ({ state = () ; env } as input) ->
@@ -1784,7 +1752,7 @@ let rec strategy_of_ast = function
}
| StratEval r -> { strategy =
(fun ({ state = () ; env ; evars } as input) ->
- let (sigma,r_interp) = Tacinterp.interp_redexp env (goalevars evars) r in
+ let (sigma,r_interp) = Tacinterp.interp_red_expr ist env (goalevars evars) r in
(Strategies.reduce r_interp).strategy { input with
evars = (sigma,cstrevars evars) }) }
| StratFold c -> Strategies.fold_glob (fst c)
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 60a66dd861..8e0ce183c2 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -62,7 +62,7 @@ type rewrite_result =
type strategy
-val strategy_of_ast : (glob_constr_and_expr, raw_red_expr) strategy_ast -> strategy
+val strategy_of_ast : interp_sign -> (glob_constr_and_expr, glob_red_expr) strategy_ast -> strategy
val map_strategy : ('a -> 'b) -> ('c -> 'd) ->
('a, 'c) strategy_ast -> ('b, 'd) strategy_ast
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index ee28229cb7..4c1fe6417e 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -394,8 +394,13 @@ type appl =
(* Values for interpretation *)
type tacvalue =
- | VFun of appl * Tacexpr.ltac_trace * Loc.t option * Val.t Id.Map.t *
- Name.t list * Tacexpr.glob_tactic_expr
+ | VFun of
+ appl *
+ Tacexpr.ltac_trace *
+ Loc.t option * (* when executing a global Ltac function: the location where this function was called *)
+ Val.t Id.Map.t * (* closure *)
+ Name.t list * (* binders *)
+ Tacexpr.glob_tactic_expr (* body *)
| VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr
let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) =
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index d58a76fe13..29e29044f1 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -31,21 +31,9 @@ type argument = Genarg.ArgT.any Extend.user_symbol
(**********************************************************************)
(* Interpret entry names of the form "ne_constr_list" as entry keys *)
-let coincide s pat off =
- let len = String.length pat in
- let break = ref true in
- let i = ref 0 in
- while !break && !i < len do
- let c = Char.code s.[off + !i] in
- let d = Char.code pat.[!i] in
- break := Int.equal c d;
- incr i
- done;
- !break
-
let atactic n =
if n = 5 then Pcoq.Symbol.nterm Pltac.binder_tactic
- else Pcoq.Symbol.nterml Pltac.tactic_expr (string_of_int n)
+ else Pcoq.Symbol.nterml Pltac.ltac_expr (string_of_int n)
type entry_name = EntryName :
'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.Symbol.t -> entry_name
@@ -70,28 +58,37 @@ let check_separator ?loc = function
| Some _ -> user_err ?loc (str "Separator is only for arguments with suffix _list_sep.")
let rec parse_user_entry ?loc s sep =
- let l = String.length s in
- if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
- let entry = parse_user_entry ?loc (String.sub s 3 (l-8)) None in
+ let open CString in
+ let matches pre suf s =
+ String.length s > (String.length pre + String.length suf) &&
+ is_prefix pre s && is_suffix suf s
+ in
+ let basename pre suf s =
+ let plen = String.length pre in
+ String.sub s plen (String.length s - (plen + String.length suf))
+ in
+ let tactic_len = String.length "tactic" in
+ if matches "ne_" "_list" s then
+ let entry = parse_user_entry ?loc (basename "ne_" "_list" s) None in
check_separator ?loc sep;
Ulist1 entry
- else if l > 12 && coincide s "ne_" 0 &&
- coincide s "_list_sep" (l-9) then
- let entry = parse_user_entry ?loc (String.sub s 3 (l-12)) None in
+ else if matches "ne_" "_list_sep" s then
+ let entry = parse_user_entry ?loc (basename "ne_" "_list_sep" s) None in
Ulist1sep (entry, get_separator sep)
- else if l > 5 && coincide s "_list" (l-5) then
- let entry = parse_user_entry ?loc (String.sub s 0 (l-5)) None in
+ else if matches "" "_list" s then
+ let entry = parse_user_entry ?loc (basename "" "_list" s) None in
check_separator ?loc sep;
Ulist0 entry
- else if l > 9 && coincide s "_list_sep" (l-9) then
- let entry = parse_user_entry ?loc (String.sub s 0 (l-9)) None in
+ else if matches "" "_list_sep" s then
+ let entry = parse_user_entry ?loc (basename "" "_list_sep" s) None in
Ulist0sep (entry, get_separator sep)
- else if l > 4 && coincide s "_opt" (l-4) then
- let entry = parse_user_entry ?loc (String.sub s 0 (l-4)) None in
+ else if matches "" "_opt" s then
+ let entry = parse_user_entry ?loc (basename "" "_opt" s) None in
check_separator ?loc sep;
Uopt entry
- else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then
- let n = Char.code s.[6] - 48 in
+ else if String.length s = tactic_len + 1 && is_prefix "tactic" s
+ && '5' >= s.[tactic_len] && s.[tactic_len] >= '0' then
+ let n = Char.code s.[tactic_len] - Char.code '0' in
check_separator ?loc sep;
Uentryl ("tactic", n)
else
@@ -119,7 +116,7 @@ let get_tactic_entry n =
else if Int.equal n 5 then
Pltac.binder_tactic, None
else if 1<=n && n<5 then
- Pltac.tactic_expr, Some (Gramlib.Gramext.Level (string_of_int n))
+ Pltac.ltac_expr, Some (Gramlib.Gramext.Level (string_of_int n))
else
user_err Pp.(str ("Invalid Tactic Notation level: "^(string_of_int n)^"."))
@@ -159,7 +156,7 @@ let rec prod_item_of_symbol lev = function
EntryName (Rawwit wit, Pcoq.Symbol.nterm (genarg_grammar wit))
| Extend.Uentryl (s, n) ->
let ArgT.Any tag = s in
- assert (coincide (ArgT.repr tag) "tactic" 0);
+ assert (CString.is_suffix "tactic" (ArgT.repr tag));
get_tacentry n lev
(** Tactic grammar extensions *)
@@ -386,7 +383,7 @@ let add_ml_tactic_notation name ~level ?deprecation prods =
in
List.iteri iter (List.rev prods);
(* We call [extend_atomic_tactic] only for "basic tactics" (the ones
- at tactic_expr level 0) *)
+ at ltac_expr level 0) *)
if Int.equal level 0 then extend_atomic_tactic name prods
(**********************************************************************)
@@ -423,7 +420,7 @@ let create_ltac_quotation name cast (e, l) =
in
let action _ v _ _ _ loc = cast (Some loc, v) in
let gram = (level, assoc, [Pcoq.Production.make rule action]) in
- Pcoq.grammar_extend Pltac.tactic_arg {pos=None; data=[gram]}
+ Pcoq.grammar_extend Pltac.tactic_value {pos=None; data=[gram]}
(** Command *)
@@ -531,16 +528,40 @@ let print_ltacs () =
let locatable_ltac = "Ltac"
+let split_ltac_fun = function
+ | Tacexpr.TacFun (l,t) -> (l,t)
+ | t -> ([],t)
+
+let pr_ltac_fun_arg n = spc () ++ Name.print n
+
+let print_ltac_body qid tac =
+ let filter mp =
+ try Some (Nametab.shortest_qualid_of_module mp)
+ with Not_found -> None
+ in
+ let mods = List.map_filter filter tac.Tacenv.tac_redef in
+ let redefined = match mods with
+ | [] -> mt ()
+ | mods ->
+ let redef = prlist_with_sep fnl pr_qualid mods in
+ fnl () ++ str "Redefined by:" ++ fnl () ++ redef
+ in
+ let l,t = split_ltac_fun tac.Tacenv.tac_body in
+ hv 2 (
+ hov 2 (str "Ltac" ++ spc() ++ pr_qualid qid ++
+ prlist pr_ltac_fun_arg l ++ spc () ++ str ":=")
+ ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) ++ redefined
+
let () =
let open Prettyp in
- let locate qid = try Some (Tacenv.locate_tactic qid) with Not_found -> None in
- let locate_all = Tacenv.locate_extended_all_tactic in
- let shortest_qualid = Tacenv.shortest_qualid_of_tactic in
- let name kn = str "Ltac" ++ spc () ++ pr_path (Tacenv.path_of_tactic kn) in
- let print kn =
- let qid = qualid_of_path (Tacenv.path_of_tactic kn) in
- Tacintern.print_ltac qid
- in
+ let locate qid = try Some (qid, Tacenv.locate_tactic qid) with Not_found -> None in
+ let locate_all qid = List.map (fun kn -> (qid,kn)) (Tacenv.locate_extended_all_tactic qid) in
+ let shortest_qualid (qid,kn) = Tacenv.shortest_qualid_of_tactic kn in
+ let name (qid,kn) = str "Ltac" ++ spc () ++ pr_path (Tacenv.path_of_tactic kn) in
+ let print (qid,kn) =
+ let entries = Tacenv.ltac_entries () in
+ let tac = KNmap.find kn entries in
+ print_ltac_body qid tac in
let about = name in
register_locatable locatable_ltac {
locate;
@@ -554,14 +575,25 @@ let () =
let print_located_tactic qid =
Feedback.msg_notice (Prettyp.print_located_other locatable_ltac qid)
+let print_ltac id =
+ try
+ let kn = Tacenv.locate_tactic id in
+ let entries = Tacenv.ltac_entries () in
+ let tac = KNmap.find kn entries in
+ print_ltac_body id tac
+ with
+ Not_found ->
+ user_err ~hdr:"print_ltac"
+ (pr_qualid id ++ spc() ++ str "is not a user defined tactic.")
+
(** Grammar *)
let () =
let entries = [
- AnyEntry Pltac.tactic_expr;
+ AnyEntry Pltac.ltac_expr;
AnyEntry Pltac.binder_tactic;
AnyEntry Pltac.simple_tactic;
- AnyEntry Pltac.tactic_arg;
+ AnyEntry Pltac.tactic_value;
] in
register_grammars_by_name "tactic" entries
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 6ee3ce091b..fc9ab54eba 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -69,6 +69,9 @@ val print_ltacs : unit -> unit
val print_located_tactic : Libnames.qualid -> unit
(** Display the absolute name of a tactic. *)
+val print_ltac : Libnames.qualid -> Pp.t
+(** Display the definition of a tactic. *)
+
(** {5 Low-level registering of tactics} *)
type (_, 'a) ml_ty_sig =
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 9c3b05fdf1..47f1d3bf66 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -769,38 +769,6 @@ let glob_tactic_env l env x =
(intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars })
x
-let split_ltac_fun = function
- | TacFun (l,t) -> (l,t)
- | t -> ([],t)
-
-let pr_ltac_fun_arg n = spc () ++ Name.print n
-
-let print_ltac id =
- try
- let kn = Tacenv.locate_tactic id in
- let entries = Tacenv.ltac_entries () in
- let tac = KNmap.find kn entries in
- let filter mp =
- try Some (Nametab.shortest_qualid_of_module mp)
- with Not_found -> None
- in
- let mods = List.map_filter filter tac.Tacenv.tac_redef in
- let redefined = match mods with
- | [] -> mt ()
- | mods ->
- let redef = prlist_with_sep fnl pr_qualid mods in
- fnl () ++ str "Redefined by:" ++ fnl () ++ redef
- in
- let l,t = split_ltac_fun tac.Tacenv.tac_body in
- hv 2 (
- hov 2 (str "Ltac" ++ spc() ++ pr_qualid id ++
- prlist pr_ltac_fun_arg l ++ spc () ++ str ":=")
- ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) ++ redefined
- with
- Not_found ->
- user_err ~hdr:"print_ltac"
- (pr_qualid id ++ spc() ++ str "is not a user defined tactic.")
-
(** Registering *)
let lift intern = (); fun ist x -> (ist, intern ist x)
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index 22ec15566b..f779aa470c 100644
--- a/plugins/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
@@ -55,9 +55,6 @@ val intern_hyp : glob_sign -> lident -> lident
val intern_genarg : glob_sign -> raw_generic_argument -> glob_generic_argument
-(** printing *)
-val print_ltac : Libnames.qualid -> Pp.t
-
(** Reduction expressions *)
val intern_red_expr : glob_sign -> raw_red_expr -> glob_red_expr
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 12bfb4d09e..3d734d3a66 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -153,11 +153,15 @@ let add_extra_loc loc extra =
match loc with
| None -> extra
| Some loc -> TacStore.set extra f_loc loc
-let add_loc loc ist =
+let extract_loc ist = TacStore.get ist.extra f_loc
+
+let ensure_loc loc ist =
match loc with
| None -> ist
- | Some loc -> { ist with extra = TacStore.set ist.extra f_loc loc }
-let extract_loc ist = TacStore.get ist.extra f_loc
+ | Some loc ->
+ match extract_loc ist with
+ | None -> { ist with extra = TacStore.set ist.extra f_loc loc }
+ | Some _ -> ist
let print_top_val env v = Pptactic.pr_value Pptactic.ltop v
@@ -1175,7 +1179,7 @@ and eval_tactic_ist ist tac : unit Proofview.tactic = match tac with
| TacFirst l -> Tacticals.New.tclFIRST (List.map (interp_tactic ist) l)
| TacSolve l -> Tacticals.New.tclSOLVE (List.map (interp_tactic ist) l)
| TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac)
- | TacArg {CAst.loc} -> Ftactic.run (val_interp (add_loc loc ist) tac) (fun v -> tactic_of_value ist v)
+ | TacArg {CAst.loc} -> Ftactic.run (val_interp (ensure_loc loc ist) tac) (fun v -> tactic_of_value ist v)
| TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
(* For extensions *)
| TacAlias {loc; v=(s,l)} ->
@@ -1254,9 +1258,12 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
let extra = TacStore.set extra f_trace trace in
let ist = { lfun = Id.Map.empty; poly; extra } in
let appl = GlbAppl[r,[]] in
+ (* We call a global ltac reference: add a loc on its executation only if not
+ already in another global reference *)
+ let ist = ensure_loc loc ist in
Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false
- (catch_error_tac_loc (* interp *) loc false trace
- (val_interp ~appl (add_loc (* exec *) loc ist) (Tacenv.interp_ltac r)))
+ (catch_error_tac_loc (* loc for interpretation *) loc false trace
+ (val_interp ~appl ist (Tacenv.interp_ltac r)))
and interp_tacarg ist arg : Val.t Ftactic.t =
match arg with
@@ -1325,7 +1332,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
; extra = TacStore.set ist.extra f_trace []
} in
Profile_ltac.do_profile "interp_app" trace ~count_call:false
- (catch_error_tac_loc loc false trace (val_interp (add_loc loc ist) body)) >>= fun v ->
+ (catch_error_tac_loc loc false trace (val_interp (ensure_loc loc ist) body)) >>= fun v ->
Ftactic.return (name_vfun (push_appl appl largs) v)
end
begin fun (e, info) ->
@@ -1997,7 +2004,7 @@ let interp_tac_gen lfun avoid_ids debug t =
let interp t = interp_tac_gen Id.Map.empty Id.Set.empty (get_debug()) t
(* MUST be marshallable! *)
-type tactic_expr = {
+type ltac_expr = {
global: bool;
ast: Tacexpr.raw_tactic_expr;
}
@@ -2019,7 +2026,7 @@ let hide_interp {global;ast} =
hide_interp (Proofview.Goal.env gl)
end
-let hide_interp = ComTactic.register_tactic_interpreter "ltac1" hide_interp
+let ComTactic.Interpreter hide_interp = ComTactic.register_tactic_interpreter "ltac1" hide_interp
(***************************************************************************)
(** Register standard arguments *)
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index 01d7306c9d..a74f4592f7 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -77,6 +77,9 @@ val val_interp : interp_sign -> glob_tactic_expr -> (value -> unit Proofview.tac
val interp_ltac_constr : interp_sign -> glob_tactic_expr -> (constr -> unit Proofview.tactic) -> unit Proofview.tactic
(** Interprets redexp arguments *)
+val interp_red_expr : interp_sign -> Environ.env -> Evd.evar_map -> glob_red_expr -> Evd.evar_map * red_expr
+
+(** Interprets redexp arguments from a raw one *)
val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map * red_expr
(** Interprets tactic expressions *)
@@ -126,12 +129,12 @@ val interp_tac_gen : value Id.Map.t -> Id.Set.t ->
val interp : raw_tactic_expr -> unit Proofview.tactic
(** Hides interpretation for pretty-print *)
-type tactic_expr = {
+type ltac_expr = {
global: bool;
ast: Tacexpr.raw_tactic_expr;
}
-val hide_interp : tactic_expr ComTactic.tactic_interpreter
+val hide_interp : ltac_expr -> ComTactic.interpretable
(** Internals that can be useful for syntax extensions. *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 23:27:11 +0000