diff options
| -rw-r--r-- | API/API.mli | 19 | ||||
| -rw-r--r-- | plugins/ltac/pptactic.ml | 97 | ||||
| -rw-r--r-- | plugins/ltac/pptactic.mli | 3 | ||||
| -rw-r--r-- | plugins/ltac/taccoerce.ml | 8 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 5 | ||||
| -rw-r--r-- | printing/genprint.ml | 99 | ||||
| -rw-r--r-- | printing/genprint.mli | 31 |
7 files changed, 221 insertions, 41 deletions
diff --git a/API/API.mli b/API/API.mli index 608bd43cd8..589745b616 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 00ce94f6c1..37c610e44b 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 "<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 @@ -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 b47f07a453..5ecfaf590c 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 a79a92a661..4d171ecbc2 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 66f124d2d1..ec8777a45c 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 "<tactic closure>")) in wit let of_tacvalue v = in_gen (topwit wit_tacvalue) v 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 "<genarg:" ++ str name ++ str ">"); glb = (fun _ -> str "<genarg:" ++ str name ++ str ">"); - top = (fun _ -> str "<genarg:" ++ str name ++ str ">"); + top = (fun _ -> PrinterBasic (fun () -> str "<genarg:" ++ str name ++ 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 |