From 0c268f5363ce7f72e85626b73082012b4e879d74 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 29 Oct 2017 17:57:29 +0100 Subject: Improving checks about the list separator in tactic notations. In Tactic Notation and TACTIC EXTEND, when an argument not ending with "_list_sep" was given with a separator, the separator was silently ignored. Now: - we take it into account if it is a list (i.e. ending with "_list"), as if "_list_sep" was given, since after all, the "_sep" is useless in the name. - we fail if there is a separator but it is not a "_list" or "_list_sep". --- plugins/ltac/tacentries.ml | 23 ++++++++++++++++------- 1 file changed, 16 insertions(+), 7 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 0bf6e3d15..ee84be541 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 -- cgit v1.2.3 From fb57fefa5f46ba8ad7be98cff81354389d87d402 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 30 Oct 2017 12:18:11 +0100 Subject: Exporting a few more printing functions. --- plugins/ltac/pptactic.ml | 7 ++++--- plugins/ltac/pptactic.mli | 7 ++++++- 2 files changed, 10 insertions(+), 4 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index d588c888c..2c46b7624 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -432,12 +432,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 } -> diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index d9da954fe..058b20569 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -69,11 +69,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 -- cgit v1.2.3 From 767816eece27e6bb8cba0bbf122507bd2a3b77a1 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 1 Nov 2017 22:54:24 +0100 Subject: Using a specific function to register vernac printers. --- API/API.mli | 2 ++ dev/doc/changes.md | 7 +++++++ grammar/argextend.mlp | 7 +------ plugins/funind/g_indfun.ml4 | 3 +-- plugins/ltac/g_obligations.ml4 | 4 +--- plugins/ltac/g_rewrite.ml4 | 3 +-- plugins/ltac/pptactic.ml | 4 ++++ plugins/ltac/pptactic.mli | 4 ++++ printing/genprint.ml | 6 ++++++ printing/genprint.mli | 2 ++ 10 files changed, 29 insertions(+), 13 deletions(-) (limited to 'plugins/ltac') diff --git a/API/API.mli b/API/API.mli index e20793077..608bd43cd 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4977,6 +4977,8 @@ sig val generic_top_print : Genarg.tlevel Genarg.generic_argument printer val register_print0 : ('raw, 'glb, 'top) Genarg.genarg_type -> 'raw printer -> 'glb printer -> 'top printer -> unit + val register_vernac_print0 : ('raw, 'glb, 'top) Genarg.genarg_type -> + 'raw printer -> unit end module Pputils : diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 6ade6576f..b1ebec44e 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -38,6 +38,13 @@ Some tactics and related functions now support static configurability, e.g.: - if None, tells to behave as told with the flag Keep Proof Equalities - if Some b, tells to keep proof equalities iff b is true +Declaration of printers for arguments used only in vernac command + +- It should now use "declare_extra_vernac_genarg_pprule" rather than + "declare_extra_genarg_pprule", otherwise, a failure at runtime might + happen. An alternative is to register the corresponding argument as + a value, using "Geninterp.register_val0 wit None". + ## Changes between Coq 8.6 and Coq 8.7 ### Ocaml diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp index 12b7b171b..9742a002d 100644 --- a/grammar/argextend.mlp +++ b/grammar/argextend.mlp @@ -186,12 +186,7 @@ let declare_vernac_argument loc s pr cl = value ($lid:"wit_"^s$ : Genarg.genarg_type 'a unit unit) = Genarg.create_arg $se$ >>; make_extend loc s cl wit; - <:str_item< do { - Pptactic.declare_extra_genarg_pprule $wit$ - $pr_rules$ - (fun _ _ _ _ -> CErrors.anomaly (Pp.str "vernac argument needs not globwit printer.")) - (fun _ _ _ _ -> CErrors.anomaly (Pp.str "vernac argument needs not wit printer.")) } - >> ] + <:str_item< Pptactic.declare_extra_vernac_genarg_pprule $wit$ $pr_rules$ >> ] open Pcaml diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 62ecaa552..829556a71 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -144,8 +144,7 @@ END let () = let raw_printer _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in - let printer _ _ _ _ = str "" in - Pptactic.declare_extra_genarg_pprule wit_function_rec_definition_loc raw_printer printer printer + Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer (* TASSI: n'importe quoi ! *) VERNAC COMMAND EXTEND Function diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index 1a2d89586..fea9e837b 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 c22e68323..b148d962e 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 "" 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 2c46b7624..00ce94f6c 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1180,6 +1180,10 @@ let declare_extra_genarg_pprule wit 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 diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 058b20569..b47f07a45 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 = { diff --git a/printing/genprint.ml b/printing/genprint.ml index 543b05024..b20ea0b62 100644 --- a/printing/genprint.ml +++ b/printing/genprint.ml @@ -39,6 +39,12 @@ let register_print0 wit raw glb top = let printer = { raw; glb; top; } in Print.register0 wit printer +let register_vernac_print0 wit raw = + let glb _ = CErrors.anomaly (Pp.str "vernac argument needs not globwit printer.") in + let top _ = CErrors.anomaly (Pp.str "vernac argument needs not wit printer.") in + let printer = { raw; glb; top; } in + Print.register0 wit printer + let raw_print wit v = (Print.obj wit).raw v let glb_print wit v = (Print.obj wit).glb v let top_print wit v = (Print.obj wit).top v diff --git a/printing/genprint.mli b/printing/genprint.mli index 130a89c92..76d80f3b5 100644 --- a/printing/genprint.mli +++ b/printing/genprint.mli @@ -27,3 +27,5 @@ val generic_top_print : tlevel generic_argument printer val register_print0 : ('raw, 'glb, 'top) genarg_type -> 'raw printer -> 'glb printer -> 'top printer -> unit +val register_vernac_print0 : ('raw, 'glb, 'top) genarg_type -> + 'raw printer -> unit -- cgit v1.2.3 From 565a9a1b5368c586e529fc9774e4cb4b81c6441b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 31 Oct 2017 17:18:50 +0100 Subject: Setting a system to register printers for Ltac values. The model provides three kinds of printers depending on whether the printer needs a context, and, if yes if it supports levels. In the latter case, it takes defaults levels for printing when in a surrounded context (lconstr style) and for printing when not in a surrounded context (constr style). This model preserves the 8.7 focussing semantics of "idtac" (i.e. focussing only when an env is needed) but it also shows that the semantics of "idtac", which focusses the goal depending on the type of its arguments, is a bit ad hoc to understand. See discussion at PR#6047 "https://github.com/coq/coq/pull/6047#discussion_r148278454". --- API/API.mli | 19 ++++++++- plugins/ltac/pptactic.ml | 97 ++++++++++++++++++++++++++++++++-------------- plugins/ltac/pptactic.mli | 3 ++ plugins/ltac/taccoerce.ml | 8 ++++ plugins/ltac/tacinterp.ml | 5 +++ printing/genprint.ml | 99 +++++++++++++++++++++++++++++++++++++++++++++-- printing/genprint.mli | 31 +++++++++++---- 7 files changed, 221 insertions(+), 41 deletions(-) (limited to 'plugins/ltac') diff --git a/API/API.mli b/API/API.mli index 608bd43cd..589745b61 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4973,12 +4973,23 @@ end module Genprint : sig + type printer_with_level = + { default_already_surrounded : Notation_term.tolerability; + default_ensure_surrounded : Notation_term.tolerability; + printer : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t } + type printer_result = + | PrinterBasic of (unit -> Pp.t) + | PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t) + | PrinterNeedsContextAndLevel of printer_with_level type 'a printer = 'a -> Pp.t - val generic_top_print : Genarg.tlevel Genarg.generic_argument printer + type 'a top_printer = 'a -> printer_result val register_print0 : ('raw, 'glb, 'top) Genarg.genarg_type -> - 'raw printer -> 'glb printer -> 'top printer -> unit + 'raw printer -> 'glb printer -> 'top top_printer -> unit val register_vernac_print0 : ('raw, 'glb, 'top) Genarg.genarg_type -> 'raw printer -> unit + val register_val_print0 : 'top Geninterp.Val.typ -> 'top top_printer -> unit + val generic_top_print : Genarg.tlevel Genarg.generic_argument top_printer + val generic_val_print : Geninterp.Val.t top_printer end module Pputils : @@ -4999,6 +5010,8 @@ sig val pr_name : Names.Name.t -> Pp.t [@@ocaml.deprecated "alias of API.Names.Name.print"] + val lsimpleconstr : Notation_term.tolerability + val ltop : Notation_term.tolerability val pr_id : Names.Id.t -> Pp.t val pr_or_var : ('a -> Pp.t) -> 'a Misctypes.or_var -> Pp.t val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t @@ -5031,6 +5044,7 @@ sig val pr_constr_pattern : Pattern.constr_pattern -> Pp.t val pr_glob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.t val pr_lglob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.t + val pr_econstr_n_env : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> EConstr.constr -> Pp.t val pr_econstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t val pr_constr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t val pr_lconstr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t @@ -5043,6 +5057,7 @@ sig val pr_lconstr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t val pr_constr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t + val pr_closed_glob_n_env : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Ltac_pretype.closed_glob_constr -> Pp.t val pr_closed_glob_env : Environ.env -> Evd.evar_map -> Ltac_pretype.closed_glob_constr -> Pp.t val pr_rel_context_of : Environ.env -> Evd.evar_map -> Pp.t val pr_named_context_of : Environ.env -> Evd.evar_map -> Pp.t diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 00ce94f6c..37c610e44 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 @@ -1175,8 +1181,8 @@ 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 "") x + Genprint.PrinterNeedsContext (fun env sigma -> + h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "") x) in Genprint.register_print0 wit f g h @@ -1186,76 +1192,111 @@ let declare_extra_vernac_genarg_pprule 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 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 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.lsimpleconstr; + Genprint.default_ensure_surrounded = Ppconstr.ltop; + Genprint.printer = (fun env sigma n -> f env sigma n c)} + +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 b47f07a45..5ecfaf590 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -125,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 a79a92a66..4d171ecbc 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -17,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, 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/tacinterp.ml b/plugins/ltac/tacinterp.ml index 66f124d2d..ec8777a45 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -76,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 @@ -124,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 "")) in wit let of_tacvalue v = in_gen (topwit wit_tacvalue) v diff --git a/printing/genprint.ml b/printing/genprint.ml index b20ea0b62..776a212b5 100644 --- a/printing/genprint.ml +++ b/printing/genprint.ml @@ -8,13 +8,100 @@ open Pp open Genarg +open Geninterp + +(* We register printers at two levels: + - generic arguments for general printers + - generic values for printing ltac values *) + +(* Printing generic values *) + +type printer_with_level = + { default_already_surrounded : Notation_term.tolerability; + default_ensure_surrounded : Notation_term.tolerability; + printer : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t } + +type printer_result = +| PrinterBasic of (unit -> Pp.t) +| PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t) +| PrinterNeedsContextAndLevel of printer_with_level type 'a printer = 'a -> Pp.t +type 'a top_printer = 'a -> printer_result + +module ValMap = ValTMap (struct type 'a t = 'a -> printer_result end) + +let print0_val_map = ref ValMap.empty + +let find_print_val_fun tag = + try ValMap.find tag !print0_val_map + with Not_found -> + let msg s = Pp.(str "print function not found for a value interpreted as " ++ str s ++ str ".") in + CErrors.anomaly (msg (Val.repr tag)) + +let generic_val_print v = + let Val.Dyn (tag,v) = v in + find_print_val_fun tag v + +let register_val_print0 s pr = + print0_val_map := ValMap.add s pr !print0_val_map + +let combine_dont_needs pr_pair pr1 = function + | PrinterBasic pr2 -> + PrinterBasic (fun () -> pr_pair (pr1 ()) (pr2 ())) + | PrinterNeedsContext pr2 -> + PrinterNeedsContext (fun env sigma -> + pr_pair (pr1 ()) (pr2 env sigma)) + | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + PrinterNeedsContext (fun env sigma -> + pr_pair (pr1 ()) (printer env sigma default_ensure_surrounded)) + +let combine_needs pr_pair pr1 = function + | PrinterBasic pr2 -> + PrinterNeedsContext (fun env sigma -> pr_pair (pr1 env sigma) (pr2 ())) + | PrinterNeedsContext pr2 -> + PrinterNeedsContext (fun env sigma -> + pr_pair (pr1 env sigma) (pr2 env sigma)) + | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + PrinterNeedsContext (fun env sigma -> + pr_pair (pr1 env sigma) (printer env sigma default_ensure_surrounded)) + +let combine pr_pair pr1 v2 = + match pr1 with + | PrinterBasic pr1 -> + combine_dont_needs pr_pair pr1 (generic_val_print v2) + | PrinterNeedsContext pr1 -> + combine_needs pr_pair pr1 (generic_val_print v2) + | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + combine_needs pr_pair (fun env sigma -> printer env sigma default_ensure_surrounded) + (generic_val_print v2) + +let _ = + let pr_cons a b = Pp.(a ++ spc () ++ b) in + register_val_print0 Val.typ_list + (function + | [] -> PrinterBasic mt + | a::l -> + List.fold_left (combine pr_cons) (generic_val_print a) l) + +let _ = + register_val_print0 Val.typ_opt + (function + | None -> PrinterBasic Pp.mt + | Some v -> generic_val_print v) + +let _ = + let pr_pair a b = Pp.(a ++ spc () ++ b) in + register_val_print0 Val.typ_pair + (fun (v1,v2) -> combine pr_pair (generic_val_print v1) v2) + +(* Printing generic arguments *) + type ('raw, 'glb, 'top) genprinter = { raw : 'raw printer; glb : 'glb printer; - top : 'top printer; + top : 'top -> printer_result; } module PrintObj = @@ -27,7 +114,7 @@ struct let printer = { raw = (fun _ -> str ""); glb = (fun _ -> str ""); - top = (fun _ -> str ""); + top = (fun _ -> PrinterBasic (fun () -> str "")); } in Some printer | _ -> assert false @@ -37,7 +124,13 @@ module Print = Register (PrintObj) let register_print0 wit raw glb top = let printer = { raw; glb; top; } in - Print.register0 wit printer + Print.register0 wit printer; + match val_tag (Topwit wit), wit with + | Val.Base t, ExtraArg t' when Geninterp.Val.repr t = ArgT.repr t' -> + register_val_print0 t top + | _ -> + (* An alias, thus no primitive printer attached *) + () let register_vernac_print0 wit raw = let glb _ = CErrors.anomaly (Pp.str "vernac argument needs not globwit printer.") in diff --git a/printing/genprint.mli b/printing/genprint.mli index 76d80f3b5..2da9bbc36 100644 --- a/printing/genprint.mli +++ b/printing/genprint.mli @@ -10,22 +10,37 @@ open Genarg +type printer_with_level = + { default_already_surrounded : Notation_term.tolerability; + default_ensure_surrounded : Notation_term.tolerability; + printer : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t } + +type printer_result = +| PrinterBasic of (unit -> Pp.t) +| PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t) +| PrinterNeedsContextAndLevel of printer_with_level + type 'a printer = 'a -> Pp.t -val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw -> Pp.t +type 'a top_printer = 'a -> printer_result + +val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw printer (** Printer for raw level generic arguments. *) -val glb_print : ('raw, 'glb, 'top) genarg_type -> 'glb -> Pp.t +val glb_print : ('raw, 'glb, 'top) genarg_type -> 'glb printer (** Printer for glob level generic arguments. *) -val top_print : ('raw, 'glb, 'top) genarg_type -> 'top -> Pp.t +val top_print : ('raw, 'glb, 'top) genarg_type -> 'top top_printer (** Printer for top level generic arguments. *) -val generic_raw_print : rlevel generic_argument printer -val generic_glb_print : glevel generic_argument printer -val generic_top_print : tlevel generic_argument printer - val register_print0 : ('raw, 'glb, 'top) genarg_type -> - 'raw printer -> 'glb printer -> 'top printer -> unit + 'raw printer -> 'glb printer -> ('top -> printer_result) -> unit +val register_val_print0 : 'top Geninterp.Val.typ -> + 'top top_printer -> unit val register_vernac_print0 : ('raw, 'glb, 'top) genarg_type -> 'raw printer -> unit + +val generic_raw_print : rlevel generic_argument printer +val generic_glb_print : glevel generic_argument printer +val generic_top_print : tlevel generic_argument top_printer +val generic_val_print : Geninterp.Val.t top_printer -- cgit v1.2.3 From 9c232079b996313ed1f5b63746304ccd639c8355 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 29 Oct 2017 19:22:27 +0100 Subject: Binding ltac printing functions to the system of generic printing. This concerns pr_value and message_of_value. This has a few consequences. For instance, no more ad hoc message "a term" or "a tactic", when not enough information is available for printing, one gets a generic message "a value of type foobar". But we also have more printers, satisfying e.g. request #5786. --- plugins/ltac/pptactic.ml | 4 +-- plugins/ltac/tacinterp.ml | 79 ++++++++++--------------------------------- test-suite/bugs/closed/5786.v | 29 ++++++++++++++++ test-suite/output/idtac.out | 11 ++++++ test-suite/output/idtac.v | 45 ++++++++++++++++++++++++ 5 files changed, 105 insertions(+), 63 deletions(-) create mode 100644 test-suite/bugs/closed/5786.v create mode 100644 test-suite/output/idtac.out create mode 100644 test-suite/output/idtac.v (limited to 'plugins/ltac') diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 37c610e44..e467d3e2c 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1220,8 +1220,8 @@ let pr_destruction_arg_env c = Genprint.PrinterNeedsContext (fun env sigma -> let make_constr_printer f c = Genprint.PrinterNeedsContextAndLevel { - Genprint.default_already_surrounded = Ppconstr.lsimpleconstr; - Genprint.default_ensure_surrounded = Ppconstr.ltop; + Genprint.default_already_surrounded = Ppconstr.ltop; + Genprint.default_ensure_surrounded = Ppconstr.lsimpleconstr; Genprint.printer = (fun env sigma n -> f env sigma n c)} let lift f a = Genprint.PrinterBasic (fun () -> f a) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index ec8777a45..8b90a0188 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -236,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 + 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) then - let c = out_gen (topwit wit_constr) 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_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 @@ -823,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 "") - 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) diff --git a/test-suite/bugs/closed/5786.v b/test-suite/bugs/closed/5786.v new file mode 100644 index 000000000..20301ec4f --- /dev/null +++ b/test-suite/bugs/closed/5786.v @@ -0,0 +1,29 @@ +(* Printing all kinds of Ltac generic arguments *) + +Tactic Notation "myidtac" string(v) := idtac v. +Goal True. +myidtac "foo". +Abort. + +Tactic Notation "myidtac2" ref(c) := idtac c. +Goal True. +myidtac2 True. +Abort. + +Tactic Notation "myidtac3" preident(s) := idtac s. +Goal True. +myidtac3 foo. +Abort. + +Tactic Notation "myidtac4" int_or_var(n) := idtac n. +Goal True. +myidtac4 3. +Abort. + +Tactic Notation "myidtac5" ident(id) := idtac id. +Goal True. +myidtac5 foo. +Abort. + + + diff --git a/test-suite/output/idtac.out b/test-suite/output/idtac.out new file mode 100644 index 000000000..3855f88a7 --- /dev/null +++ b/test-suite/output/idtac.out @@ -0,0 +1,11 @@ +"foo" +True +foo +3 +foo +2 +< True False Prop > +< True False Prop > +< > +< > +<< 1 2 3 >> diff --git a/test-suite/output/idtac.v b/test-suite/output/idtac.v new file mode 100644 index 000000000..ac60ea917 --- /dev/null +++ b/test-suite/output/idtac.v @@ -0,0 +1,45 @@ +(* Printing all kinds of Ltac generic arguments *) + +Tactic Notation "myidtac" string(v) := idtac v. +Goal True. +myidtac "foo". +Abort. + +Tactic Notation "myidtac2" ref(c) := idtac c. +Goal True. +myidtac2 True. +Abort. + +Tactic Notation "myidtac3" preident(s) := idtac s. +Goal True. +myidtac3 foo. +Abort. + +Tactic Notation "myidtac4" int_or_var(n) := idtac n. +Goal True. +myidtac4 3. +Abort. + +Tactic Notation "myidtac5" ident(id) := idtac id. +Goal True. +myidtac5 foo. +Abort. + +(* Checking non focussing of idtac for integers *) +Goal True/\True. split. +all:let c:=numgoals in idtac c. +Abort. + +(* Checking printing of lists and its focussing *) +Tactic Notation "myidtac6" constr_list(l) := idtac "<" l ">". +Goal True/\True. split. +all:myidtac6 True False Prop. +(* An empty list is focussing because of interp_genarg of a constr *) +(* even if it is not focussing on printing *) +all:myidtac6. +Abort. + +Tactic Notation "myidtac7" int_list(l) := idtac "<<" l ">>". +Goal True/\True. split. +all:myidtac7 1 2 3. +Abort. -- cgit v1.2.3 From d073a70d84aa6802a03d03a17d2246d607e85db1 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 30 Oct 2017 10:35:13 +0100 Subject: Ltac Debug: exporting env and sigma when needed so that term can be printed. We do it so as to preserve non-focussing semantics for non-focussing generic arguments. This assumes that the code treats them consistently, which is not enforced statically, but which is reasonable in the sense that when we need a context for printing, we have no other choice as needing a context and we needed one also at interpretation time. --- plugins/ltac/tacinterp.ml | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 8b90a0188..fd75862c6 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -908,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 @@ -926,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 -> @@ -1348,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 -- cgit v1.2.3