aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-10-31 17:18:50 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-11-02 11:36:41 +0100
commit565a9a1b5368c586e529fc9774e4cb4b81c6441b (patch)
tree054160a2e7eb5842f8b5e6b7c20fa016b8ae1817 /printing
parentb0e9d691d6c48fb09b20bb9d98626143eb8b92df (diff)
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".
Diffstat (limited to 'printing')
-rw-r--r--printing/genprint.ml99
-rw-r--r--printing/genprint.mli31
2 files changed, 119 insertions, 11 deletions
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 "<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 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