aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/evar_tactics.ml3
-rw-r--r--plugins/ltac/extratactics.ml430
-rw-r--r--plugins/ltac/g_obligations.ml44
-rw-r--r--plugins/ltac/g_rewrite.ml43
-rw-r--r--plugins/ltac/pptactic.ml108
-rw-r--r--plugins/ltac/pptactic.mli14
-rw-r--r--plugins/ltac/taccoerce.ml11
-rw-r--r--plugins/ltac/taccoerce.mli11
-rw-r--r--plugins/ltac/tacentries.ml23
-rw-r--r--plugins/ltac/tacexpr.mli2
-rw-r--r--plugins/ltac/tacintern.ml23
-rw-r--r--plugins/ltac/tacinterp.ml112
-rw-r--r--plugins/ltac/tacinterp.mli8
-rw-r--r--plugins/ltac/tactic_debug.ml2
-rw-r--r--plugins/ltac/tactic_matching.ml6
-rw-r--r--plugins/ltac/tactic_matching.mli2
16 files changed, 207 insertions, 155 deletions
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index d9150a7bbd..1f628803a3 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -17,6 +17,7 @@ open Refiner
open Evd
open Locus
open Context.Named.Declaration
+open Ltac_pretype
module NamedDecl = Context.Named.Declaration
@@ -27,7 +28,7 @@ let instantiate_evar evk (ist,rawc) sigma =
let filtered = Evd.evar_filtered_env evi in
let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in
let lvar = {
- Glob_term.ltac_constrs = constrvars;
+ ltac_constrs = constrvars;
ltac_uconstrs = Names.Id.Map.empty;
ltac_idents = Names.Id.Map.empty;
ltac_genargs = ist.Geninterp.lfun;
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index a7aebf9e15..65c186a419 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -91,12 +91,12 @@ let elimOnConstrWithHoles tac with_evars c =
(fun c -> tac with_evars (Some (None,ElimOnConstr c)))
TACTIC EXTEND simplify_eq
- [ "simplify_eq" ] -> [ dEq false None ]
-| [ "simplify_eq" destruction_arg(c) ] -> [ mytclWithHoles dEq false c ]
+ [ "simplify_eq" ] -> [ dEq ~keep_proofs:None false None ]
+| [ "simplify_eq" destruction_arg(c) ] -> [ mytclWithHoles (dEq ~keep_proofs:None) false c ]
END
TACTIC EXTEND esimplify_eq
-| [ "esimplify_eq" ] -> [ dEq true None ]
-| [ "esimplify_eq" destruction_arg(c) ] -> [ mytclWithHoles dEq true c ]
+| [ "esimplify_eq" ] -> [ dEq ~keep_proofs:None true None ]
+| [ "esimplify_eq" destruction_arg(c) ] -> [ mytclWithHoles (dEq ~keep_proofs:None) true c ]
END
let discr_main c = elimOnConstrWithHoles discr_tac false c
@@ -117,31 +117,31 @@ let discrHyp id =
discr_main (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings)))
let injection_main with_evars c =
- elimOnConstrWithHoles (injClause None) with_evars c
+ elimOnConstrWithHoles (injClause None None) with_evars c
TACTIC EXTEND injection
-| [ "injection" ] -> [ injClause None false None ]
-| [ "injection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None) false c ]
+| [ "injection" ] -> [ injClause None None false None ]
+| [ "injection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None None) false c ]
END
TACTIC EXTEND einjection
-| [ "einjection" ] -> [ injClause None true None ]
-| [ "einjection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None) true c ]
+| [ "einjection" ] -> [ injClause None None true None ]
+| [ "einjection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None None) true c ]
END
TACTIC EXTEND injection_as
| [ "injection" "as" intropattern_list(ipat)] ->
- [ injClause (Some ipat) false None ]
+ [ injClause None (Some ipat) false None ]
| [ "injection" destruction_arg(c) "as" intropattern_list(ipat)] ->
- [ mytclWithHoles (injClause (Some ipat)) false c ]
+ [ mytclWithHoles (injClause None (Some ipat)) false c ]
END
TACTIC EXTEND einjection_as
| [ "einjection" "as" intropattern_list(ipat)] ->
- [ injClause (Some ipat) true None ]
+ [ injClause None (Some ipat) true None ]
| [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] ->
- [ mytclWithHoles (injClause (Some ipat)) true c ]
+ [ mytclWithHoles (injClause None (Some ipat)) true c ]
END
TACTIC EXTEND simple_injection
-| [ "simple" "injection" ] -> [ simpleInjClause false None ]
-| [ "simple" "injection" destruction_arg(c) ] -> [ mytclWithHoles simpleInjClause false c ]
+| [ "simple" "injection" ] -> [ simpleInjClause None false None ]
+| [ "simple" "injection" destruction_arg(c) ] -> [ mytclWithHoles (simpleInjClause None) false c ]
END
let injHyp id =
diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index 1a2d895868..fea9e837b1 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -155,6 +155,4 @@ let () =
| None -> mt ()
| Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic tac
in
- (* should not happen *)
- let dummy _ _ _ expr = assert false in
- Pptactic.declare_extra_genarg_pprule wit_withtac printer dummy dummy
+ Pptactic.declare_extra_vernac_genarg_pprule wit_withtac printer
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index c22e683235..b148d962ed 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -195,8 +195,7 @@ let binders = Pcoq.create_generic_entry Pcoq.utactic "binders" (Genarg.rawwit wi
let () =
let raw_printer _ _ _ l = Pp.pr_non_empty_arg Ppconstr.pr_binders l in
- let printer _ _ _ _ = Pp.str "<Unavailable printer for binders>" in
- Pptactic.declare_extra_genarg_pprule wit_binders raw_printer printer printer
+ Pptactic.declare_extra_vernac_genarg_pprule wit_binders raw_printer
open Pcoq
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index d588c888c4..e467d3e2ca 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -116,7 +116,13 @@ type 'a extra_genarg_printer =
| Val.Base t ->
begin match Val.eq t tag with
| None -> default
- | Some Refl -> Genprint.generic_top_print (in_gen (Topwit wit) x)
+ | Some Refl ->
+ let open Genprint in
+ match generic_top_print (in_gen (Topwit wit) x) with
+ | PrinterBasic pr -> pr ()
+ | PrinterNeedsContext pr -> pr (Global.env()) Evd.empty
+ | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+ printer (Global.env()) Evd.empty default_ensure_surrounded
end
| _ -> default
@@ -432,12 +438,13 @@ type 'a extra_genarg_printer =
let pr_occs = pr_with_occurrences (fun () -> str" |- *") (occs,()) in
(prlist_with_sep (fun () -> str", ") (pr_hyp_location pr_id) l ++ pr_occs)
- let pr_clauses default_is_concl pr_id = function
+ (* Some true = default is concl; Some false = default is all; None = no default *)
+ let pr_clauses has_default pr_id = function
| { onhyps=Some []; concl_occs=occs }
- when (match default_is_concl with Some true -> true | _ -> false) ->
+ when (match has_default with Some true -> true | _ -> false) ->
pr_with_occurrences mt (occs,())
| { onhyps=None; concl_occs=AllOccurrences }
- when (match default_is_concl with Some false -> true | _ -> false) -> mt ()
+ when (match has_default with Some false -> true | _ -> false) -> mt ()
| { onhyps=None; concl_occs=NoOccurrences } ->
pr_in (str " * |-")
| { onhyps=None; concl_occs=occs } ->
@@ -1174,83 +1181,122 @@ let declare_extra_genarg_pprule wit
g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x
in
let h x =
- let env = Global.env () in
- h (pr_econstr_env env Evd.empty) (pr_leconstr_env env Evd.empty) (fun _ _ -> str "<tactic>") x
+ Genprint.PrinterNeedsContext (fun env sigma ->
+ h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") x)
in
Genprint.register_print0 wit f g h
+let declare_extra_vernac_genarg_pprule wit f =
+ let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in
+ Genprint.register_vernac_print0 wit f
+
(** Registering *)
-let run_delayed c = c (Global.env ()) Evd.empty
+let pr_intro_pattern_env p = Genprint.PrinterNeedsContext (fun env sigma ->
+ let print_constr c = let (sigma, c) = c env sigma in pr_econstr_env env sigma c in
+ Miscprint.pr_intro_pattern print_constr p)
+
+let pr_red_expr_env r = Genprint.PrinterNeedsContext (fun env sigma ->
+ pr_red_expr (pr_econstr_env env sigma, pr_leconstr_env env sigma,
+ pr_evaluable_reference_env env, pr_constr_pattern_env env sigma) r)
+
+let pr_bindings_env bl = Genprint.PrinterNeedsContext (fun env sigma ->
+ let sigma, bl = bl env sigma in
+ Miscprint.pr_bindings
+ (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl)
+
+let pr_with_bindings_env bl = Genprint.PrinterNeedsContext (fun env sigma ->
+ let sigma, bl = bl env sigma in
+ pr_with_bindings
+ (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl)
+
+let pr_destruction_arg_env c = Genprint.PrinterNeedsContext (fun env sigma ->
+ let sigma, c = match c with
+ | clear_flag,ElimOnConstr g -> let sigma,c = g env sigma in sigma,(clear_flag,ElimOnConstr c)
+ | clear_flag,ElimOnAnonHyp n as x -> sigma, x
+ | clear_flag,ElimOnIdent id as x -> sigma, x in
+ pr_destruction_arg
+ (pr_econstr_env env sigma) (pr_leconstr_env env sigma) c)
+
+let make_constr_printer f c =
+ Genprint.PrinterNeedsContextAndLevel {
+ Genprint.default_already_surrounded = Ppconstr.ltop;
+ Genprint.default_ensure_surrounded = Ppconstr.lsimpleconstr;
+ Genprint.printer = (fun env sigma n -> f env sigma n c)}
-let run_delayed_destruction_arg = function (* HH: Using Evd.empty looks suspicious *)
- | clear_flag,ElimOnConstr g -> clear_flag,ElimOnConstr (snd (run_delayed g))
- | clear_flag,ElimOnAnonHyp n as x -> x
- | clear_flag,ElimOnIdent id as x -> x
+let lift f a = Genprint.PrinterBasic (fun () -> f a)
let () =
let pr_bool b = if b then str "true" else str "false" in
let pr_unit _ = str "()" in
- let pr_string s = str "\"" ++ str s ++ str "\"" in
Genprint.register_print0 wit_int_or_var
- (pr_or_var int) (pr_or_var int) int;
+ (pr_or_var int) (pr_or_var int) (lift int);
Genprint.register_print0 wit_ref
- pr_reference (pr_or_var (pr_located pr_global)) pr_global;
+ pr_reference (pr_or_var (pr_located pr_global)) (lift pr_global);
Genprint.register_print0 wit_ident
- pr_id pr_id pr_id;
+ pr_id pr_id (lift pr_id);
Genprint.register_print0 wit_var
- (pr_located pr_id) (pr_located pr_id) pr_id;
+ (pr_located pr_id) (pr_located pr_id) (lift pr_id);
Genprint.register_print0
wit_intro_pattern
(Miscprint.pr_intro_pattern pr_constr_expr)
(Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c))
- (Miscprint.pr_intro_pattern (fun c -> pr_econstr (snd (run_delayed c))));
+ pr_intro_pattern_env;
Genprint.register_print0
wit_clause_dft_concl
(pr_clauses (Some true) pr_lident)
(pr_clauses (Some true) pr_lident)
- (pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)))
+ (fun c -> Genprint.PrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)) c))
;
Genprint.register_print0
wit_constr
Ppconstr.pr_constr_expr
(fun (c, _) -> Printer.pr_glob_constr c)
- Printer.pr_econstr
+ (make_constr_printer Printer.pr_econstr_n_env)
;
Genprint.register_print0
wit_uconstr
Ppconstr.pr_constr_expr
(fun (c,_) -> Printer.pr_glob_constr c)
- Printer.pr_closed_glob
+ (make_constr_printer Printer.pr_closed_glob_n_env)
;
Genprint.register_print0
wit_open_constr
Ppconstr.pr_constr_expr
(fun (c, _) -> Printer.pr_glob_constr c)
- Printer.pr_econstr
+ (make_constr_printer Printer.pr_econstr_n_env)
;
Genprint.register_print0 wit_red_expr
(pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr))
(pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_and_constr_expr pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr))
- (pr_red_expr (pr_econstr, pr_leconstr, pr_evaluable_reference, pr_constr_pattern));
- Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis;
+ pr_red_expr_env
+ ;
+ Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis (lift pr_quantified_hypothesis);
Genprint.register_print0 wit_bindings
(Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
(Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
- (fun it -> Miscprint.pr_bindings_no_with pr_econstr pr_leconstr (snd (run_delayed it)));
+ pr_bindings_env
+ ;
Genprint.register_print0 wit_constr_with_bindings
(pr_with_bindings pr_constr_expr pr_lconstr_expr)
(pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
- (fun it -> pr_with_bindings pr_econstr pr_leconstr (snd (run_delayed it)));
+ pr_with_bindings_env
+ ;
+ Genprint.register_print0 wit_open_constr_with_bindings
+ (pr_with_bindings pr_constr_expr pr_lconstr_expr)
+ (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
+ pr_with_bindings_env
+ ;
Genprint.register_print0 Tacarg.wit_destruction_arg
(pr_destruction_arg pr_constr_expr pr_lconstr_expr)
(pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
- (fun it -> pr_destruction_arg pr_econstr pr_leconstr (run_delayed_destruction_arg it));
- Genprint.register_print0 Stdarg.wit_int int int int;
- Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool;
- Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit;
- Genprint.register_print0 Stdarg.wit_pre_ident str str str;
- Genprint.register_print0 Stdarg.wit_string pr_string pr_string pr_string
+ pr_destruction_arg_env
+ ;
+ Genprint.register_print0 Stdarg.wit_int int int (lift int);
+ Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool (lift pr_bool);
+ Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit (lift pr_unit);
+ Genprint.register_print0 Stdarg.wit_pre_ident str str (lift str);
+ Genprint.register_print0 Stdarg.wit_string qstring qstring (lift qstring)
let () =
let printer _ _ prtac = prtac (0, E) in
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index d9da954fe6..5ecfaf590c 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -46,6 +46,10 @@ val declare_extra_genarg_pprule :
'b glob_extra_genarg_printer ->
'c extra_genarg_printer -> unit
+val declare_extra_vernac_genarg_pprule :
+ ('a, 'b, 'c) genarg_type ->
+ 'a raw_extra_genarg_printer -> unit
+
type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list
type pp_tactic = {
@@ -69,11 +73,16 @@ val pr_may_eval :
val pr_and_short_name : ('a -> Pp.t) -> 'a and_short_name -> Pp.t
val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t
+val pr_evaluable_reference_env : env -> evaluable_global_reference -> Pp.t
+
+val pr_quantified_hypothesis : quantified_hypothesis -> Pp.t
+
val pr_in_clause :
('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t
-val pr_clauses : bool option ->
+val pr_clauses : (* default: *) bool option ->
('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t
+ (* Some true = default is concl; Some false = default is all; None = no default *)
val pr_raw_generic : env -> rlevel generic_argument -> Pp.t
@@ -116,3 +125,6 @@ val pr_value : tolerability -> Val.t -> Pp.t
val ltop : tolerability
+
+val make_constr_printer : (env -> Evd.evar_map -> Notation_term.tolerability -> 'a -> Pp.t) ->
+ 'a Genprint.top_printer
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 9e3a54cc86..4d171ecbc2 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -10,7 +10,6 @@ open Util
open Names
open Term
open EConstr
-open Pattern
open Misctypes
open Genarg
open Stdarg
@@ -18,15 +17,23 @@ open Geninterp
exception CannotCoerceTo of string
+let base_val_typ wit =
+ match val_tag (topwit wit) with Val.Base t -> t | _ -> CErrors.anomaly (Pp.str "Not a base val.")
+
let (wit_constr_context : (Empty.t, Empty.t, EConstr.constr) Genarg.genarg_type) =
let wit = Genarg.create_arg "constr_context" in
let () = register_val0 wit None in
+ let () = Genprint.register_val_print0 (base_val_typ wit)
+ (Pptactic.make_constr_printer Printer.pr_econstr_n_env) in
wit
(* includes idents known to be bound and references *)
-let (wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) Genarg.genarg_type) =
+let (wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_binders) Genarg.genarg_type) =
let wit = Genarg.create_arg "constr_under_binders" in
let () = register_val0 wit None in
+ let () = Genprint.register_val_print0 (base_val_typ wit)
+ (fun c ->
+ Genprint.PrinterNeedsContext (fun env sigma -> Printer.pr_constr_under_binders_env env sigma c)) in
wit
(** All the types considered here are base types *)
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 1a67f6f888..d7b253a687 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -10,7 +10,6 @@ open Util
open Names
open EConstr
open Misctypes
-open Pattern
open Genarg
open Geninterp
@@ -37,8 +36,8 @@ sig
val of_constr : constr -> t
val to_constr : t -> constr option
- val of_uconstr : Glob_term.closed_glob_constr -> t
- val to_uconstr : t -> Glob_term.closed_glob_constr option
+ val of_uconstr : Ltac_pretype.closed_glob_constr -> t
+ val to_uconstr : t -> Ltac_pretype.closed_glob_constr option
val of_int : int -> t
val to_int : t -> int option
val to_list : t -> t list option
@@ -63,9 +62,9 @@ val coerce_to_hint_base : Value.t -> string
val coerce_to_int : Value.t -> int
-val coerce_to_constr : Environ.env -> Value.t -> constr_under_binders
+val coerce_to_constr : Environ.env -> Value.t -> Ltac_pretype.constr_under_binders
-val coerce_to_uconstr : Environ.env -> Value.t -> Glob_term.closed_glob_constr
+val coerce_to_uconstr : Environ.env -> Value.t -> Ltac_pretype.closed_glob_constr
val coerce_to_closed_constr : Environ.env -> Value.t -> constr
@@ -93,4 +92,4 @@ val coerce_to_int_or_var_list : Value.t -> int or_var list
val wit_constr_context : (Empty.t, Empty.t, EConstr.constr) genarg_type
-val wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) genarg_type
+val wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_binders) genarg_type
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 0bf6e3d155..ee84be5414 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -63,28 +63,37 @@ let get_separator = function
| None -> user_err Pp.(str "Missing separator.")
| Some sep -> sep
-let rec parse_user_entry s sep =
+let check_separator ?loc = function
+| None -> ()
+| 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 (String.sub s 3 (l-8)) None in
+ let entry = parse_user_entry ?loc (String.sub s 3 (l-8)) 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 (String.sub s 3 (l-12)) None in
+ let entry = parse_user_entry ?loc (String.sub s 3 (l-12)) None in
Ulist1sep (entry, get_separator sep)
else if l > 5 && coincide s "_list" (l-5) then
- let entry = parse_user_entry (String.sub s 0 (l-5)) None in
+ let entry = parse_user_entry ?loc (String.sub s 0 (l-5)) None in
+ check_separator ?loc sep;
Ulist0 entry
else if l > 9 && coincide s "_list_sep" (l-9) then
- let entry = parse_user_entry (String.sub s 0 (l-9)) None in
+ let entry = parse_user_entry ?loc (String.sub s 0 (l-9)) None in
Ulist0sep (entry, get_separator sep)
else if l > 4 && coincide s "_opt" (l-4) then
- let entry = parse_user_entry (String.sub s 0 (l-4)) None in
+ let entry = parse_user_entry ?loc (String.sub s 0 (l-4)) 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
+ check_separator ?loc sep;
Uentryl ("tactic", n)
else
+ let _ = check_separator ?loc sep in
Uentry s
let interp_entry_name interp symb =
@@ -203,7 +212,7 @@ let register_tactic_notation_entry name entry =
let interp_prod_item = function
| TacTerm s -> TacTerm s
| TacNonTerm (loc, ((nt, sep), ido)) ->
- let symbol = parse_user_entry nt sep in
+ let symbol = parse_user_entry ?loc nt sep in
let interp s = function
| None ->
if String.Map.mem s !entry_names then String.Map.find s !entry_names
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 2c36faeff4..1639736883 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -386,7 +386,7 @@ type ltac_call_kind =
| LtacNameCall of ltac_constant
| LtacAtomCall of glob_atomic_tactic_expr
| LtacVarCall of Id.t * glob_tactic_expr
- | LtacConstrInterp of Glob_term.glob_constr * Glob_term.ltac_var_map
+ | LtacConstrInterp of Glob_term.glob_constr * Ltac_pretype.ltac_var_map
type ltac_trace = ltac_call_kind Loc.located list
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 99d7684d36..f171fd07d7 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -322,13 +322,23 @@ let intern_constr_pattern ist ~as_type ~ltacvars pc =
let dummy_pat = PRel 0
-let intern_typed_pattern ist p =
+let intern_typed_pattern ist ~as_type ~ltacvars p =
(* we cannot ensure in non strict mode that the pattern is closed *)
(* keeping a constr_expr copy is too complicated and we want anyway to *)
(* type it, so we remember the pattern as a glob_constr only *)
+ let metas,pat =
+ if !strict_check then
+ let ltacvars = {
+ Constrintern.ltac_vars = ltacvars;
+ ltac_bound = Id.Set.empty;
+ ltac_extra = ist.extra;
+ } in
+ Constrintern.intern_constr_pattern ist.genv ~as_type ~ltacvars p
+ else
+ [], dummy_pat in
let (glob,_ as c) = intern_constr_gen true false ist p in
let bound_names = Glob_ops.bound_glob_vars glob in
- (bound_names,c,dummy_pat)
+ metas,(bound_names,c,pat)
let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
let interp_ref r =
@@ -364,7 +374,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
(* We interpret similarly @ref and ref *)
interp_ref (AN r)
| Inr c ->
- Inr (intern_typed_pattern ist c))
+ Inr (snd (intern_typed_pattern ist ~as_type:false ~ltacvars:ist.ltacvars c)))
(* This seems fairly hacky, but it's the first way I've found to get proper
globalization of [unfold]. --adamc *)
@@ -529,7 +539,12 @@ let rec intern_atomic lf ist x =
then intern_type ist c else intern_constr ist c),
clause_app (intern_hyp_location ist) cl)
| TacChange (Some p,c,cl) ->
- TacChange (Some (intern_typed_pattern ist p),intern_constr ist c,
+ let { ltacvars } = ist in
+ let metas,pat = intern_typed_pattern ist ~as_type:false ~ltacvars p in
+ let fold accu x = Id.Set.add x accu in
+ let ltacvars = List.fold_left fold ltacvars metas in
+ let ist' = { ist with ltacvars } in
+ TacChange (Some pat,intern_constr ist' c,
clause_app (intern_hyp_location ist) cl)
(* Equality and inversion *)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 20f117ff4f..fd75862c6f 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -38,6 +38,7 @@ open Tacintern
open Taccoerce
open Proofview.Notations
open Context.Named.Declaration
+open Ltac_pretype
let ltac_trace_info = Tactic_debug.ltac_trace_info
@@ -75,6 +76,9 @@ let out_gen wit v =
let val_tag wit = val_tag (topwit wit)
+let base_val_typ wit =
+ match val_tag wit with Val.Base t -> t | _ -> anomaly (str "Not a base val.")
+
let pr_argument_type arg =
let Val.Dyn (tag, _) = arg in
Val.pr tag
@@ -123,6 +127,8 @@ type tacvalue =
let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) =
let wit = Genarg.create_arg "tacvalue" in
let () = register_val0 wit None in
+ let () = Genprint.register_val_print0 (base_val_typ wit)
+ (fun _ -> Genprint.PrinterBasic (fun () -> str "<tactic closure>")) in
wit
let of_tacvalue v = in_gen (topwit wit_tacvalue) v
@@ -230,24 +236,16 @@ let curr_debug ist = match TacStore.get ist.extra f_debug with
(* Displays a value *)
let pr_value env v =
let v = Value.normalize v in
- if has_type v (topwit wit_tacvalue) then str "a tactic"
- else if has_type v (topwit wit_constr_context) then
- let c = out_gen (topwit wit_constr_context) v in
- match env with
- | Some (env,sigma) -> pr_leconstr_env env sigma c
- | _ -> str "a term"
- else if has_type v (topwit wit_constr) then
- let c = out_gen (topwit wit_constr) v in
+ let pr_with_env pr =
match env with
- | Some (env,sigma) -> pr_leconstr_env env sigma c
- | _ -> str "a term"
- else if has_type v (topwit wit_constr_under_binders) then
- let c = out_gen (topwit wit_constr_under_binders) v in
- match env with
- | Some (env,sigma) -> pr_lconstr_under_binders_env env sigma c
- | _ -> str "a term"
- else
- str "a value of type" ++ spc () ++ pr_argument_type v
+ | Some (env,sigma) -> pr env sigma
+ | None -> str "a value of type" ++ spc () ++ pr_argument_type v in
+ let open Genprint in
+ match generic_val_print v with
+ | PrinterBasic pr -> pr ()
+ | PrinterNeedsContext pr -> pr_with_env pr
+ | PrinterNeedsContextAndLevel { default_already_surrounded; printer } ->
+ pr_with_env (fun env sigma -> printer env sigma default_already_surrounded)
let pr_closure env ist body =
let pp_body = Pptactic.pr_glob_tactic env body in
@@ -551,7 +549,6 @@ let interp_fresh_id ist env sigma l =
(* Extract the uconstr list from lfun *)
let extract_ltac_constr_context ist env sigma =
- let open Glob_term in
let add_uconstr id v map =
try Id.Map.add id (coerce_to_uconstr env v) map
with CannotCoerceTo _ -> map
@@ -602,10 +599,10 @@ let interp_gen kind ist pattern_mode flags env sigma c =
let { closure = constrvars ; term } =
interp_glob_closure ist env sigma ~kind:kind_for_intern ~pattern_mode c in
let vars = {
- Glob_term.ltac_constrs = constrvars.typed;
- Glob_term.ltac_uconstrs = constrvars.untyped;
- Glob_term.ltac_idents = constrvars.idents;
- Glob_term.ltac_genargs = ist.lfun;
+ ltac_constrs = constrvars.typed;
+ ltac_uconstrs = constrvars.untyped;
+ ltac_idents = constrvars.idents;
+ ltac_genargs = ist.lfun;
} in
(* Jason Gross: To avoid unnecessary modifications to tacinterp, as
suggested by Arnaud Spiwack, we run push_trace immediately. We do
@@ -818,51 +815,16 @@ let interp_constr_may_eval ist env sigma c =
end
(** TODO: should use dedicated printers *)
-let rec message_of_value v =
+let message_of_value v =
let v = Value.normalize v in
- let open Ftactic in
- if has_type v (topwit wit_tacvalue) then
- Ftactic.return (str "<tactic>")
- else if has_type v (topwit wit_constr) then
- let v = out_gen (topwit wit_constr) v in
- Ftactic.enter begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) v) end
- else if has_type v (topwit wit_constr_under_binders) then
- let c = out_gen (topwit wit_constr_under_binders) v in
- Ftactic.enter begin fun gl ->
- Ftactic.return (pr_constr_under_binders_env (pf_env gl) (project gl) c)
- end
- else if has_type v (topwit wit_unit) then
- Ftactic.return (str "()")
- else if has_type v (topwit wit_int) then
- Ftactic.return (int (out_gen (topwit wit_int) v))
- else if has_type v (topwit wit_intro_pattern) then
- let p = out_gen (topwit wit_intro_pattern) v in
- let print env sigma c =
- let (sigma, c) = c env sigma in
- pr_econstr_env env sigma c
- in
- Ftactic.enter begin fun gl ->
- Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (project gl) c) p)
- end
- else if has_type v (topwit wit_constr_context) then
- let c = out_gen (topwit wit_constr_context) v in
- Ftactic.enter begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) c) end
- else if has_type v (topwit wit_uconstr) then
- let c = out_gen (topwit wit_uconstr) v in
- Ftactic.enter begin fun gl ->
- Ftactic.return (pr_closed_glob_env (pf_env gl)
- (project gl) c)
- end
- else if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
- Ftactic.enter begin fun gl -> Ftactic.return (Id.print id) end
- else match Value.to_list v with
- | Some l ->
- Ftactic.List.map message_of_value l >>= fun l ->
- Ftactic.return (prlist_with_sep spc (fun x -> x) l)
- | None ->
- let tag = pr_argument_type v in
- Ftactic.return (str "<" ++ tag ++ str ">") (** TODO *)
+ let pr_with_env pr =
+ Ftactic.enter begin fun gl -> Ftactic.return (pr (pf_env gl) (project gl)) end in
+ let open Genprint in
+ match generic_val_print v with
+ | PrinterBasic pr -> Ftactic.return (pr ())
+ | PrinterNeedsContext pr -> pr_with_env pr
+ | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+ pr_with_env (fun env sigma -> printer env sigma default_ensure_surrounded)
let interp_message_token ist = function
| MsgString s -> Ftactic.return (str s)
@@ -946,13 +908,13 @@ let interp_in_hyp_as ist env sigma (id,ipat) =
let sigma, ipat = interp_intro_pattern_option ist env sigma ipat in
sigma,(interp_hyp ist env sigma id,ipat)
-let interp_binding_name ist sigma = function
+let interp_binding_name ist env sigma = function
| AnonHyp n -> AnonHyp n
| NamedHyp id ->
(* If a name is bound, it has to be a quantified hypothesis *)
(* user has to use other names for variables if these ones clash with *)
(* a name intented to be used as a (non-variable) identifier *)
- try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist None(Loc.tag id)
+ try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist (Some (env,sigma)) (Loc.tag id)
with Not_found -> NamedHyp id
let interp_declared_or_quantified_hypothesis ist env sigma = function
@@ -964,7 +926,7 @@ let interp_declared_or_quantified_hypothesis ist env sigma = function
let interp_binding ist env sigma (loc,(b,c)) =
let sigma, c = interp_open_constr ist env sigma c in
- sigma, (loc,(interp_binding_name ist sigma b,c))
+ sigma, (loc,(interp_binding_name ist env sigma b,c))
let interp_bindings ist env sigma = function
| NoBindings ->
@@ -1386,10 +1348,14 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
end >>= fun v ->
(* No errors happened, we propagate the trace *)
let v = append_trace trace v in
- Proofview.tclLIFT begin
- debugging_step ist
- (fun () ->
- str"evaluation returns"++fnl()++pr_value None v)
+ let call_debug env =
+ Proofview.tclLIFT (debugging_step ist (fun () -> str"evaluation returns"++fnl()++pr_value env v)) in
+ begin
+ let open Genprint in
+ match generic_val_print v with
+ | PrinterBasic _ -> call_debug None
+ | PrinterNeedsContext _ | PrinterNeedsContextAndLevel _ ->
+ Proofview.Goal.enter (fun gl -> call_debug (Some (pf_env gl,project gl)))
end <*>
if List.is_empty lval then Ftactic.return v else interp_app loc ist v lval
else
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index d0a0a81d4c..5f2723a1e3 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -44,7 +44,7 @@ val f_avoid_ids : Id.Set.t TacStore.field
val f_debug : debug_info TacStore.field
val extract_ltac_constr_values : interp_sign -> Environ.env ->
- Pattern.constr_under_binders Id.Map.t
+ Ltac_pretype.constr_under_binders Id.Map.t
(** Given an interpretation signature, extract all values which are coercible to
a [constr]. *)
@@ -57,7 +57,7 @@ val get_debug : unit -> debug_info
val type_uconstr :
?flags:Pretyping.inference_flags ->
?expected_type:Pretyping.typing_constraint ->
- Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr Tactypes.delayed_open
+ Geninterp.interp_sign -> Ltac_pretype.closed_glob_constr -> constr Tactypes.delayed_open
(** Adds an interpretation function for extra generic arguments *)
@@ -79,10 +79,10 @@ val interp_hyp : interp_sign -> Environ.env -> Evd.evar_map ->
val interp_glob_closure : interp_sign -> Environ.env -> Evd.evar_map ->
?kind:Pretyping.typing_constraint -> ?pattern_mode:bool -> glob_constr_and_expr ->
- Glob_term.closed_glob_constr
+ Ltac_pretype.closed_glob_constr
val interp_uconstr : interp_sign -> Environ.env -> Evd.evar_map ->
- glob_constr_and_expr -> Glob_term.closed_glob_constr
+ glob_constr_and_expr -> Ltac_pretype.closed_glob_constr
val interp_constr_gen : Pretyping.typing_constraint -> interp_sign ->
Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Evd.evar_map * constr
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 5394b1e116..a669692fc9 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -363,7 +363,7 @@ let explain_ltac_call_trace last trace loc =
| Tacexpr.LtacAtomCall te ->
quote (Pptactic.pr_glob_tactic (Global.env())
(Tacexpr.TacAtom (Loc.tag te)))
- | Tacexpr.LtacConstrInterp (c, { Glob_term.ltac_constrs = vars }) ->
+ | Tacexpr.LtacConstrInterp (c, { Ltac_pretype.ltac_constrs = vars }) ->
quote (Printer.pr_glob_constr_env (Global.env()) c) ++
(if not (Id.Map.is_empty vars) then
strbrk " (with " ++
diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml
index 18bb7d2dbd..89b78e5907 100644
--- a/plugins/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
@@ -22,7 +22,7 @@ module NamedDecl = Context.Named.Declaration
those of {!Matching.matching_result}), and a {!Term.constr}
substitution mapping corresponding to matched hypotheses. *)
type 'a t = {
- subst : Constr_matching.bound_ident_map * Pattern.extended_patvar_map ;
+ subst : Constr_matching.bound_ident_map * Ltac_pretype.extended_patvar_map ;
context : EConstr.constr Id.Map.t;
terms : EConstr.constr Id.Map.t;
lhs : 'a;
@@ -36,8 +36,8 @@ type 'a t = {
(** Some of the functions of {!Matching} return the substitution with a
[patvar_map] instead of an [extended_patvar_map]. [adjust] coerces
substitution of the former type to the latter. *)
-let adjust : Constr_matching.bound_ident_map * Pattern.patvar_map ->
- Constr_matching.bound_ident_map * Pattern.extended_patvar_map =
+let adjust : Constr_matching.bound_ident_map * Ltac_pretype.patvar_map ->
+ Constr_matching.bound_ident_map * Ltac_pretype.extended_patvar_map =
fun (l, lc) -> (l, Id.Map.map (fun c -> [], c) lc)
diff --git a/plugins/ltac/tactic_matching.mli b/plugins/ltac/tactic_matching.mli
index 01334d36c9..955f8105fb 100644
--- a/plugins/ltac/tactic_matching.mli
+++ b/plugins/ltac/tactic_matching.mli
@@ -18,7 +18,7 @@
those of {!Matching.matching_result}), and a {!Term.constr}
substitution mapping corresponding to matched hypotheses. *)
type 'a t = {
- subst : Constr_matching.bound_ident_map * Pattern.extended_patvar_map ;
+ subst : Constr_matching.bound_ident_map * Ltac_pretype.extended_patvar_map ;
context : EConstr.constr Names.Id.Map.t;
terms : EConstr.constr Names.Id.Map.t;
lhs : 'a;
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 23:22:56 +0000