aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Json.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Json.ml')
-rw-r--r--lib/Json.ml42
1 files changed, 42 insertions, 0 deletions
diff --git a/lib/Json.ml b/lib/Json.ml
new file mode 100644
index 00000000..4aa91e95
--- /dev/null
+++ b/lib/Json.ml
@@ -0,0 +1,42 @@
+(* *********************************************************************)
+(* *)
+(* 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 Printf
+
+(* Simple functions for JSON printing *)
+
+(* Print a string as json string *)
+let p_jstring oc s = fprintf oc "\"%s\"" s
+
+(* Print a list as json array *)
+let p_jarray elem oc l =
+ match l with
+ | [] -> fprintf oc "[]"
+ | hd::tail ->
+ output_string oc "["; elem oc hd;
+ List.iter (fprintf oc ",%a" elem) tail;
+ output_string oc "]"
+
+(* Print a bool as json bool *)
+let p_jbool oc = fprintf oc "%B"
+
+(* Print a int as json int *)
+let p_jint oc = fprintf oc "%d"
+
+(* Print a member *)
+let p_jmember oc name p_mem mem =
+ fprintf oc "\n%a:%a" p_jstring name p_mem mem
+
+(* Print optional value *)
+let p_jopt p_elem oc = function
+ | None -> output_string oc "null"
+ | Some i -> p_elem oc i