blob: b8f66c085816c2bc15ecf105ef06081b1055abd3 (
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
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *)
(* *)
(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *)
(* is distributed under the terms of the INRIA Non-Commercial *)
(* License Agreement. *)
(* *)
(* *********************************************************************)
open Format
open Camlcoq
(* Simple functions for JSON printing *)
(* Print a string as json string *)
let pp_jstring oc s =
fprintf oc "\"%s\"" s
(* Print a bool as json bool *)
let pp_jbool oc = fprintf oc "%B"
(* Print an int as json int *)
let pp_jint oc = fprintf oc "%d"
(* Print an int32 as json int *)
let pp_jint32 oc = fprintf oc "%ld"
(* Print optional value *)
let pp_jopt pp_elem oc = function
| None -> output_string oc "null"
| Some i -> pp_elem oc i
(* Print opening and closing curly braces for json dictionaries *)
let pp_jobject_start pp =
fprintf pp "@[<v 1>{"
let pp_jobject_end pp =
fprintf pp "@;<0 -1>}@]"
(* Print a member of a json dictionary *)
let pp_jmember ?(first=false) pp name pp_mem mem =
let sep = if first then "" else "," in
fprintf pp "%s@ \"%s\": %a" sep name pp_mem mem
(* Print singleton object *)
let pp_jsingle_object pp name pp_mem mem =
pp_jobject_start pp;
pp_jmember ~first:true pp name pp_mem mem;
pp_jobject_end pp
(* Print a list as json array *)
let pp_jarray elem pp l =
match l with
| [] -> fprintf pp "[]";
| hd::tail ->
fprintf pp "@[<v 1>[";
fprintf pp "%a" elem hd;
List.iter (fun l -> fprintf pp ",@ %a" elem l) tail;
fprintf pp "@;<0 -1>]@]"
(* Helper functions for printing coq integer and floats *)
let pp_int pp i =
fprintf pp "%ld" (camlint_of_coqint i)
let pp_int64 pp i =
fprintf pp "%Ld" (camlint64_of_coqint i)
let pp_float32 pp f =
fprintf pp "%ld" (camlint_of_coqint (Floats.Float32.to_bits f))
let pp_float64 pp f =
fprintf pp "%Ld" (camlint64_of_coqint (Floats.Float.to_bits f))
let pp_z pp z =
fprintf pp "%s" (Z.to_string z)
(* Helper functions for printing assembler constructs *)
let pp_atom pp a =
pp_jstring pp (extern_atom a)
let pp_atom_constant pp a =
pp_jsingle_object pp "Atom" pp_atom a
let pp_int_constant pp i =
pp_jsingle_object pp "Integer" pp_int i
let pp_float64_constant pp f =
pp_jsingle_object pp "Float" pp_float64 f
let pp_float32_constant pp f =
pp_jsingle_object pp "Float" pp_float32 f
let id = ref 0
let next_id () =
let tmp = !id in
incr id;
tmp
let reset_id () =
id := 0
let pp_id_const pp () =
let i = next_id () in
pp_jsingle_object pp "Integer" (fun pp i -> fprintf pp "%d" i) i
|
