diff options
Diffstat (limited to 'printing/genprint.ml')
| -rw-r--r-- | printing/genprint.ml | 133 |
1 files changed, 121 insertions, 12 deletions
diff --git a/printing/genprint.ml b/printing/genprint.ml index 0ec35e07..1bb7838a 100644 --- a/printing/genprint.ml +++ b/printing/genprint.ml @@ -1,31 +1,128 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp open Genarg +open Geninterp -type ('raw, 'glb, 'top) printer = { - raw : 'raw -> std_ppcmds; - glb : 'glb -> std_ppcmds; - top : 'top -> std_ppcmds; +(* We register printers at two levels: + - generic arguments for general printers + - generic values for printing ltac values *) + +(* Printing generic values *) + +type 'a with_level = + { default_already_surrounded : Notation_term.tolerability; + default_ensure_surrounded : Notation_term.tolerability; + printer : 'a } + +type printer_result = +| PrinterBasic of (unit -> Pp.t) +| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level + +type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t + +type top_printer_result = +| TopPrinterBasic of (unit -> Pp.t) +| TopPrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t) +| TopPrinterNeedsContextAndLevel of printer_fun_with_level with_level + +type 'a printer = 'a -> printer_result + +type 'a top_printer = 'a -> top_printer_result + +module ValMap = ValTMap (struct type 'a t = 'a -> top_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 + | TopPrinterBasic pr2 -> + TopPrinterBasic (fun () -> pr_pair (pr1 ()) (pr2 ())) + | TopPrinterNeedsContext pr2 -> + TopPrinterNeedsContext (fun env sigma -> + pr_pair (pr1 ()) (pr2 env sigma)) + | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + TopPrinterNeedsContext (fun env sigma -> + pr_pair (pr1 ()) (printer env sigma default_ensure_surrounded)) + +let combine_needs pr_pair pr1 = function + | TopPrinterBasic pr2 -> + TopPrinterNeedsContext (fun env sigma -> pr_pair (pr1 env sigma) (pr2 ())) + | TopPrinterNeedsContext pr2 -> + TopPrinterNeedsContext (fun env sigma -> + pr_pair (pr1 env sigma) (pr2 env sigma)) + | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + TopPrinterNeedsContext (fun env sigma -> + pr_pair (pr1 env sigma) (printer env sigma default_ensure_surrounded)) + +let combine pr_pair pr1 v2 = + match pr1 with + | TopPrinterBasic pr1 -> + combine_dont_needs pr_pair pr1 (generic_val_print v2) + | TopPrinterNeedsContext pr1 -> + combine_needs pr_pair pr1 (generic_val_print v2) + | TopPrinterNeedsContextAndLevel { 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 + | [] -> TopPrinterBasic mt + | a::l -> + List.fold_left (combine pr_cons) (generic_val_print a) l) + +let _ = + register_val_print0 Val.typ_opt + (function + | None -> TopPrinterBasic 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_result; + glb : 'glb -> printer_result; + top : 'top -> top_printer_result; } module PrintObj = struct - type ('raw, 'glb, 'top) obj = ('raw, 'glb, 'top) printer + type ('raw, 'glb, 'top) obj = ('raw, 'glb, 'top) genprinter let name = "printer" let default wit = match wit with | ExtraArg tag -> let name = ArgT.repr tag in let printer = { - raw = (fun _ -> str "<genarg:" ++ str name ++ str ">"); - glb = (fun _ -> str "<genarg:" ++ str name ++ str ">"); - top = (fun _ -> str "<genarg:" ++ str name ++ str ">"); + raw = (fun _ -> PrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">")); + glb = (fun _ -> PrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">")); + top = (fun _ -> TopPrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">")); } in Some printer | _ -> assert false @@ -35,6 +132,18 @@ module Print = Register (PrintObj) let register_print0 wit raw glb top = let printer = { raw; glb; top; } in + 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 + 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 |