diff options
Diffstat (limited to 'lib/Json.ml')
-rw-r--r-- | lib/Json.ml | 51 |
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 |