From c616bd4d9819e4cd3c868716cb92663b3c69e069 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 31 Oct 2017 15:38:40 +0100 Subject: Removing a redundancy in naming types (Ppconstr.precedence = tolerability). --- printing/ppconstr.ml | 1 - printing/ppconstr.mli | 9 ++++----- 2 files changed, 4 insertions(+), 6 deletions(-) (limited to 'printing') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 102c6ef6de..4d7a716319 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -738,7 +738,6 @@ let tag_var = tag Tag.variable pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t } - type precedence = Notation_term.precedence * Notation_term.parenRelation let modular_constr_pr = pr let rec fix rf x = rf (fix rf) x let pr = fix modular_constr_pr mt diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 7546c748d8..34cccfc2d0 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -86,9 +86,8 @@ val default_term_pr : term_pr Which has the same type. We can turn a modular printer into a printer by taking its fixpoint. *) -type precedence -val lsimpleconstr : precedence -val ltop : precedence +val lsimpleconstr : tolerability +val ltop : tolerability val modular_constr_pr : - ((unit->Pp.t) -> precedence -> constr_expr -> Pp.t) -> - (unit->Pp.t) -> precedence -> constr_expr -> Pp.t + ((unit->Pp.t) -> tolerability -> constr_expr -> Pp.t) -> + (unit->Pp.t) -> tolerability -> constr_expr -> Pp.t -- cgit v1.2.3 From 0df9c751f98d2f9b4423eb1bee17730cd0bf0123 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 31 Oct 2017 17:01:05 +0100 Subject: Exporting the level-parametric printer of constr and its variants. This is for eventually being reused in Ltac messages ("idtac"). --- printing/ppconstr.ml | 21 ++++++++++++++------- printing/ppconstr.mli | 1 + printing/printer.ml | 6 ++++++ printing/printer.mli | 5 +++++ 4 files changed, 26 insertions(+), 7 deletions(-) (limited to 'printing') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 4d7a716319..109a40a037 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -742,29 +742,36 @@ let tag_var = tag Tag.variable let rec fix rf x = rf (fix rf) x let pr = fix modular_constr_pr mt + let pr prec = function + (* A toplevel printer hack mimicking parsing, incidentally meaning + that we cannot use [pr] correctly anymore in a recursive loop + if the current expr is followed by other exprs which would be + interpreted as arguments *) + | { CAst.v = CAppExpl ((None,f,us),[]) } -> str "@" ++ pr_cref f us + | c -> pr prec c + let transf env c = if !Flags.beautify_file then let r = Constrintern.for_grammar (Constrintern.intern_constr env) c in Constrextern.extern_glob_constr (Termops.vars_of_env env) r else c - let pr prec c = pr prec (transf (Global.env()) c) + let pr_expr prec c = pr prec (transf (Global.env()) c) - let pr_simpleconstr = function - | { CAst.v = CAppExpl ((None,f,us),[]) } -> str "@" ++ pr_cref f us - | c -> pr lsimpleconstr c + let pr_simpleconstr = pr_expr lsimpleconstr let default_term_pr = { pr_constr_expr = pr_simpleconstr; - pr_lconstr_expr = pr ltop; + pr_lconstr_expr = pr_expr ltop; pr_constr_pattern_expr = pr_simpleconstr; - pr_lconstr_pattern_expr = pr ltop + pr_lconstr_pattern_expr = pr_expr ltop } let term_pr = ref default_term_pr let set_term_pr = (:=) term_pr + let pr_constr_expr_n n c = pr_expr n c let pr_constr_expr c = !term_pr.pr_constr_expr c let pr_lconstr_expr c = !term_pr.pr_lconstr_expr c let pr_constr_pattern_expr c = !term_pr.pr_constr_pattern_expr c @@ -774,5 +781,5 @@ let tag_var = tag Tag.variable let pr_record_body = pr_record_body_gen pr - let pr_binders = pr_undelimited_binders spc (pr ltop) + let pr_binders = pr_undelimited_binders spc (pr_expr ltop) diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 34cccfc2d0..be96cfce50 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -60,6 +60,7 @@ val pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t val pr_constr_expr : constr_expr -> Pp.t val pr_lconstr_expr : constr_expr -> Pp.t val pr_cases_pattern_expr : cases_pattern_expr -> Pp.t +val pr_constr_expr_n : tolerability -> constr_expr -> Pp.t type term_pr = { pr_constr_expr : constr_expr -> Pp.t; diff --git a/printing/printer.ml b/printing/printer.ml index 28b10c7812..c6650ea3b8 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -79,11 +79,14 @@ let _ = and only names of goal/section variables and rel names that do _not_ occur in the scope of the binder to be printed are avoided. *) +let pr_econstr_n_core goal_concl_style env sigma n t = + pr_constr_expr_n n (extern_constr goal_concl_style env sigma t) let pr_econstr_core goal_concl_style env sigma t = pr_constr_expr (extern_constr goal_concl_style env sigma t) let pr_leconstr_core goal_concl_style env sigma t = pr_lconstr_expr (extern_constr goal_concl_style env sigma t) +let pr_constr_n_env env sigma n c = pr_econstr_n_core false env sigma n (EConstr.of_constr c) let pr_lconstr_env env sigma c = pr_leconstr_core false env sigma (EConstr.of_constr c) let pr_constr_env env sigma c = pr_econstr_core false env sigma (EConstr.of_constr c) let _ = Hook.set Refine.pr_constr pr_constr_env @@ -94,6 +97,7 @@ let pr_constr_goal_style_env env sigma c = pr_econstr_core true env sigma (ECons let pr_open_lconstr_env env sigma (_,c) = pr_lconstr_env env sigma c let pr_open_constr_env env sigma (_,c) = pr_constr_env env sigma c +let pr_econstr_n_env env sigma c = pr_econstr_n_core false env sigma c let pr_leconstr_env env sigma c = pr_leconstr_core false env sigma c let pr_econstr_env env sigma c = pr_econstr_core false env sigma c @@ -166,6 +170,8 @@ let pr_glob_constr c = let (sigma, env) = get_current_context () in pr_glob_constr_env env c +let pr_closed_glob_n_env env sigma n c = + pr_constr_expr_n n (extern_closed_glob false env sigma c) let pr_closed_glob_env env sigma c = pr_constr_expr (extern_closed_glob false env sigma c) let pr_closed_glob c = diff --git a/printing/printer.mli b/printing/printer.mli index ba849bee6a..658ea6060b 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -33,6 +33,8 @@ val pr_constr_env : env -> evar_map -> constr -> Pp.t val pr_constr : constr -> Pp.t val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t +val pr_constr_n_env : env -> evar_map -> Notation_term.tolerability -> constr -> Pp.t + (** Same, but resilient to [Nametab] errors. Prints fully-qualified names when [shortest_qualid_of_global] has failed. Prints "??" in case of remaining issues (such as reference not in env). *) @@ -48,6 +50,8 @@ val pr_econstr : EConstr.t -> Pp.t val pr_leconstr_env : env -> evar_map -> EConstr.t -> Pp.t val pr_leconstr : EConstr.t -> Pp.t +val pr_econstr_n_env : env -> evar_map -> Notation_term.tolerability -> EConstr.t -> Pp.t + val pr_etype_env : env -> evar_map -> EConstr.types -> Pp.t val pr_letype_env : env -> evar_map -> EConstr.types -> Pp.t @@ -70,6 +74,7 @@ val pr_ltype : types -> Pp.t val pr_type_env : env -> evar_map -> types -> Pp.t val pr_type : types -> Pp.t +val pr_closed_glob_n_env : env -> evar_map -> Notation_term.tolerability -> closed_glob_constr -> Pp.t val pr_closed_glob_env : env -> evar_map -> closed_glob_constr -> Pp.t val pr_closed_glob : closed_glob_constr -> 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. --- printing/genprint.ml | 6 ++++++ printing/genprint.mli | 2 ++ 2 files changed, 8 insertions(+) (limited to 'printing') diff --git a/printing/genprint.ml b/printing/genprint.ml index 543b05024d..b20ea0b620 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 130a89c929..76d80f3b50 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". --- printing/genprint.ml | 99 +++++++++++++++++++++++++++++++++++++++++++++++++-- printing/genprint.mli | 31 +++++++++++----- 2 files changed, 119 insertions(+), 11 deletions(-) (limited to 'printing') diff --git a/printing/genprint.ml b/printing/genprint.ml index b20ea0b620..776a212b5c 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 76d80f3b50..2da9bbc36b 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