blob: 5a1da2fd7db48b939c4de289a61dcb24d50544f8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Pp
open Util
open Genarg
type printer = {
raw : Obj.t -> std_ppcmds;
glb : Obj.t -> std_ppcmds;
top : Obj.t -> std_ppcmds;
}
let default_printer name = (); fun _ -> str "<genarg:" ++ str name ++ str ">"
let default_printer name =
let pr = default_printer name in
{ raw = pr; glb = pr; top = pr; }
let (arg0_printer_map : printer String.Map.t ref) = ref String.Map.empty
let get_printer0 name =
try String.Map.find name !arg0_printer_map
with Not_found -> default_printer name
let obj_printer t = match t with
| ExtraArgType s -> get_printer0 s
| _ -> assert false
let raw_print arg = Obj.magic (obj_printer (unquote (rawwit arg))).raw
let glb_print arg = Obj.magic (obj_printer (unquote (rawwit arg))).glb
let top_print arg = Obj.magic (obj_printer (unquote (rawwit arg))).top
let generic_raw_print v =
(obj_printer (genarg_tag v)).raw (Unsafe.prj v)
let generic_glb_print v =
(obj_printer (genarg_tag v)).glb (Unsafe.prj v)
let generic_top_print v =
(obj_printer (genarg_tag v)).top (Unsafe.prj v)
let register_print0 arg rpr gpr tpr = match unquote (rawwit arg) with
| ExtraArgType s ->
if String.Map.mem s !arg0_printer_map then
Errors.anomaly (str "interp0 function already registered: " ++ str s)
else
let pr = { raw = Obj.magic rpr; glb = Obj.magic gpr; top = Obj.magic tpr; } in
arg0_printer_map := String.Map.add s pr !arg0_printer_map
| _ -> assert false
|
