adbrucker
/
isabelle-hacks
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Added serializer implementation.

This commit is contained in:
Achim D. Brucker 2019-01-20 20:19:41 +00:00
parent 1be7bfd514
commit 338dcc874a
1 changed files with 71 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

74
Nano_JSON.thy
View File

@ -159,10 +159,78 @@ end
section\<open>Serializing Nano JSON\<close>
ML\<open>
signature NANO_JSON_SERIALIZER = sig
val serialize_json: Nano_Json_Type.json -> string
val serialize_json_pretty: Nano_Json_Type.json -> string
val serialize_term: term -> string
val serialize_term_pretty: term -> string
end
structure Nano_Json_Serializer : NANO_JSON_SERIALIZER = struct
open Nano_Json_Type
fun escapeJsonString s =
let fun bs c = "\\"^(Char.toString c)
fun escape #"\"" = bs #"\""
| escape #"\\" = bs #"\\"
| escape #"\b" = bs #"b"
| escape #"\f" = bs #"f"
| escape #"\n" = bs #"n"
| escape #"\r" = bs #"r"
| escape #"\t" = bs #"t"
| escape c =
let val ord = Char.ord c
in
if ord < 0x20
then let val hex = Word.toString (Word.fromInt ord)
val prfx = if ord < 0x10 then "\\u000" else "\\u00"
in
prfx^hex
end
else
Char.toString c
end
in
String.concat (map escape (String.explode s))
end
fun serialize pretty json = let
val nl = if pretty = NONE then "" else "\n"
fun indent' 0 = ""
| indent' n = " "^(indent' (n-1))
fun indent n = (case pretty of NONE => ""
| SOME n' => indent' (n+n'))
fun serialize' _ (OBJECT []) = "{}"
| serialize' _ (ARRAY []) = "[]"
| serialize' n (OBJECT pp) = "{"^nl^(indent (n+1)) ^ String.concatWith
(","^nl^(indent (n+1)))
(map (fn (key, value) =>
serialize' (n+1) (STRING key) ^ ":" ^
serialize' (n+1) value) pp) ^
nl^(indent n)^"}"
| serialize' n (ARRAY arr) = "["^nl^(indent (n+1)) ^ String.concatWith
(","^nl^(indent (n+1)))
(map (serialize' (n+1) ) arr) ^
nl^(indent n)^"]"
| serialize' _ (NUMBER (REAL n)) = String.implode (map (fn #"~" => #"-" | c => c)
(String.explode (Real.toString n)))
| serialize' _ (NUMBER (INTEGER n)) = String.implode (map (fn #"~" => #"-" | c => c)
(String.explode (Int.toString n)))
| serialize' _ (STRING s) = "\"" ^ escapeJsonString s ^ "\""
| serialize' _ (BOOL b) = Bool.toString b
| serialize' _ NULL = "null"
in
(serialize' 0 json)^nl
end
val serialize_json = serialize NONE
val serialize_json_pretty = serialize (SOME 0)
val serialize_term = (serialize NONE) o json_of_term
val serialize_term_pretty = (serialize (SOME 0)) o json_of_term
end
\<close>
section\<open>Parsing Nano JSON\<close>
end