1 files changed, 50 insertions, 1 deletions
diff --git a/lib/Json.ml b/lib/Json.ml
index 16819e8d..b8f66c08 100644
--- a/lib/Json.ml
+++ b/lib/Json.ml
@@ -11,6 +11,8 @@
 (* *********************************************************************)
 
 open Format
+open Camlcoq
+
 
 (* Simple functions for JSON printing *)
 
@@ -32,13 +34,14 @@ 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 *)
+(* 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
@@ -58,3 +61,49 @@ let pp_jarray elem pp l =
     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