json.ur 15 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339
  1. con json a = {ToJson : a -> string,
  2. FromJson : string -> a * string}
  3. fun mkJson [a] (x : {ToJson : a -> string,
  4. FromJson : string -> a * string}) = x
  5. fun skipSpaces s =
  6. let
  7. val len = String.length s
  8. fun skip i =
  9. if i >= len then
  10. ""
  11. else
  12. let
  13. val ch = String.sub s i
  14. in
  15. if Char.isSpace ch then
  16. skip (i+1)
  17. else
  18. String.substring s {Start = i, Len = len-i}
  19. end
  20. in
  21. skip 0
  22. end
  23. fun toJson [a] (j : json a) : a -> string = j.ToJson
  24. fun fromJson' [a] (j : json a) : string -> a * string = j.FromJson
  25. fun fromJson [a] (j : json a) (s : string) : a =
  26. let
  27. val (v, s') = j.FromJson (skipSpaces s)
  28. in
  29. if String.all Char.isSpace s' then
  30. v
  31. else
  32. error <xml>Extra content at end of JSON record: {[s']}</xml>
  33. end
  34. fun escape s =
  35. let
  36. val len = String.length s
  37. fun esc i =
  38. if i >= len then
  39. "\""
  40. else
  41. let
  42. val ch = String.sub s i
  43. in
  44. (if ch = #"\"" || ch = #"\\" then
  45. "\\" ^ String.str ch
  46. else
  47. String.str ch) ^ esc (i+1)
  48. end
  49. in
  50. "\"" ^ esc 0
  51. end
  52. fun unescape s =
  53. let
  54. val len = String.length s
  55. fun findEnd i =
  56. if i >= len then
  57. error <xml>JSON unescape: string ends before quote: {[s]}</xml>
  58. else
  59. let
  60. val ch = String.sub s i
  61. in
  62. case ch of
  63. #"\"" => i
  64. | #"\\" =>
  65. if i+1 >= len then
  66. error <xml>JSON unescape: Bad escape sequence: {[s]}</xml>
  67. else
  68. findEnd (i+2)
  69. | _ => findEnd (i+1)
  70. end
  71. val last = findEnd 1
  72. fun unesc i =
  73. if i >= last then
  74. ""
  75. else
  76. let
  77. val ch = String.sub s i
  78. in
  79. case ch of
  80. #"\\" =>
  81. if i+1 >= len then
  82. error <xml>JSON unescape: Bad escape sequence: {[s]}</xml>
  83. else
  84. String.str (String.sub s (i+1)) ^ unesc (i+2)
  85. | _ => String.str ch ^ unesc (i+1)
  86. end
  87. in
  88. if len = 0 || String.sub s 0 <> #"\"" then
  89. error <xml>JSON unescape: String doesn't start with double quote: {[s]}</xml>
  90. else
  91. (unesc 1, String.substring s {Start = last+1, Len = len-last-1})
  92. end
  93. val json_string = {ToJson = escape,
  94. FromJson = unescape}
  95. fun numIn [a] (_ : read a) s : a * string =
  96. let
  97. val len = String.length s
  98. fun findEnd i =
  99. if i >= len then
  100. i
  101. else
  102. let
  103. val ch = String.sub s i
  104. in
  105. if Char.isDigit ch || ch = #"-" || ch = #"." || ch = #"E" || ch = #"e" then
  106. findEnd (i+1)
  107. else
  108. i
  109. end
  110. val last = findEnd 0
  111. in
  112. (readError (String.substring s {Start = 0, Len = last}), String.substring s {Start = last, Len = len-last})
  113. end
  114. fun json_num [a] (_ : show a) (_ : read a) : json a = {ToJson = show,
  115. FromJson = numIn}
  116. val json_int = json_num
  117. val json_float = json_num
  118. val json_bool = {ToJson = fn b => if b then "true" else "false",
  119. FromJson = fn s => if String.isPrefix {Full = s, Prefix = "true"} then
  120. (True, String.substring s {Start = 4, Len = String.length s - 4})
  121. else if String.isPrefix {Full = s, Prefix = "false"} then
  122. (False, String.substring s {Start = 5, Len = String.length s - 5})
  123. else
  124. error <xml>JSON: bad boolean string: {[s]}</xml>}
  125. fun json_option [a] (j : json a) : json (option a) =
  126. {ToJson = fn v => case v of
  127. None => "null"
  128. | Some v => j.ToJson v,
  129. FromJson = fn s => if String.isPrefix {Full = s, Prefix = "null"} then
  130. (None, String.substring s {Start = 4, Len = String.length s - 4})
  131. else
  132. let
  133. val (v, s') = j.FromJson s
  134. in
  135. (Some v, s')
  136. end}
  137. fun json_list [a] (j : json a) : json (list a) =
  138. let
  139. fun toJ' (ls : list a) : string =
  140. case ls of
  141. [] => ""
  142. | x :: ls => "," ^ toJson j x ^ toJ' ls
  143. fun toJ (x : list a) : string =
  144. case x of
  145. [] => "[]"
  146. | x :: [] => "[" ^ toJson j x ^ "]"
  147. | x :: ls => "[" ^ toJson j x ^ toJ' ls ^ "]"
  148. fun fromJ (s : string) : list a * string =
  149. let
  150. fun fromJ' (s : string) : list a * string =
  151. if String.length s = 0 then
  152. error <xml>JSON list doesn't end with ']'</xml>
  153. else
  154. let
  155. val ch = String.sub s 0
  156. in
  157. case ch of
  158. #"]" => ([], String.substring s {Start = 1, Len = String.length s - 1})
  159. | _ =>
  160. let
  161. val (x, s') = j.FromJson s
  162. val s' = skipSpaces s'
  163. val s' = if String.length s' = 0 then
  164. error <xml>JSON list doesn't end with ']'</xml>
  165. else if String.sub s' 0 = #"," then
  166. skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1})
  167. else
  168. s'
  169. val (ls, s'') = fromJ' s'
  170. in
  171. (x :: ls, s'')
  172. end
  173. end
  174. in
  175. if String.length s = 0 || String.sub s 0 <> #"[" then
  176. error <xml>JSON list doesn't start with '[': {[s]}</xml>
  177. else
  178. fromJ' (skipSpaces (String.substring s {Start = 1, Len = String.length s - 1}))
  179. end
  180. in
  181. {ToJson = toJ,
  182. FromJson = fromJ}
  183. end
  184. fun json_record [ts ::: {Type}] (fl : folder ts) (jss : $(map json ts)) (names : $(map (fn _ => string) ts)) : json $ts =
  185. {ToJson = fn r => "{" ^ @foldR3 [json] [fn _ => string] [ident] [fn _ => string]
  186. (fn [nm ::_] [t ::_] [r ::_] [[nm] ~ r] (j : json t) name v acc =>
  187. escape name ^ ":" ^ j.ToJson v ^ (case acc of
  188. "" => ""
  189. | _ => "," ^ acc))
  190. "" fl jss names r ^ "}",
  191. FromJson = fn s =>
  192. let
  193. fun fromJ s (r : $(map option ts)) : $(map option ts) * string =
  194. if String.length s = 0 then
  195. error <xml>JSON object doesn't end in brace</xml>
  196. else if String.sub s 0 = #"}" then
  197. (r, String.substring s {Start = 1, Len = String.length s - 1})
  198. else let
  199. val (name, s') = unescape s
  200. val s' = skipSpaces s'
  201. val s' = if String.length s' = 0 || String.sub s' 0 <> #":" then
  202. error <xml>No colon after JSON object field name</xml>
  203. else
  204. skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1})
  205. val (r, s') = @foldR2 [json] [fn _ => string] [fn ts => $(map option ts) -> $(map option ts) * string]
  206. (fn [nm ::_] [t ::_] [r ::_] [[nm] ~ r] (j : json t) name' acc r =>
  207. if name = name' then
  208. let
  209. val (v, s') = j.FromJson s'
  210. in
  211. (r -- nm ++ {nm = Some v}, s')
  212. end
  213. else
  214. let
  215. val (r', s') = acc (r -- nm)
  216. in
  217. (r' ++ {nm = r.nm}, s')
  218. end)
  219. (fn _ => error <xml>Unknown JSON object field name {[name]}</xml>)
  220. fl jss names r
  221. val s' = skipSpaces s'
  222. val s' = if String.length s' <> 0 && String.sub s' 0 = #"," then
  223. skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1})
  224. else
  225. s'
  226. in
  227. fromJ s' r
  228. end
  229. in
  230. if String.length s = 0 || String.sub s 0 <> #"{" then
  231. error <xml>JSON record doesn't begin with brace</xml>
  232. else
  233. let
  234. val (r, s') = fromJ (skipSpaces (String.substring s {Start = 1, Len = String.length s - 1}))
  235. (@map0 [option] (fn [t ::_] => None) fl)
  236. in
  237. (@map2 [option] [fn _ => string] [ident] (fn [t] (v : option t) name =>
  238. case v of
  239. None => error <xml>Missing JSON object field {[name]}</xml>
  240. | Some v => v) fl r names, s')
  241. end
  242. end}
  243. fun json_variant [ts ::: {Type}] (fl : folder ts) (jss : $(map json ts)) (names : $(map (fn _ => string) ts)) : json (variant ts) =
  244. {ToJson = fn r => let val jnames = @map2 [json] [fn _ => string] [fn x => json x * string]
  245. (fn [t] (j : json t) (name : string) => (j, name)) fl jss names
  246. in @Variant.destrR [ident] [fn x => json x * string]
  247. (fn [p ::_] (v : p) (j : json p, name : string) =>
  248. "{" ^ escape name ^ ":" ^ j.ToJson v ^ "}") fl r jnames
  249. end,
  250. FromJson = fn s =>
  251. if String.length s = 0 || String.sub s 0 <> #"{" then
  252. error <xml>JSON variant doesn't begin with brace</xml>
  253. else
  254. let
  255. val (name, s') = unescape (skipSpaces (String.suffix s 1))
  256. val s' = skipSpaces s'
  257. val s' = if String.length s' = 0 || String.sub s' 0 <> #":" then
  258. error <xml>No colon after JSON object field name</xml>
  259. else
  260. skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1})
  261. val (r, s') = (@foldR2 [json] [fn _ => string]
  262. [fn ts => ts' :: {Type} -> [ts ~ ts'] => variant (ts ++ ts') * string]
  263. (fn [nm ::_] [t ::_] [rest ::_] [[nm] ~ rest] (j : json t) name'
  264. (acc : ts' :: {Type} -> [rest ~ ts'] => variant (rest ++ ts') * string) [fwd ::_] [[nm = t] ++ rest ~ fwd] =>
  265. if name = name'
  266. then
  267. let val (v, s') = j.FromJson s'
  268. in (make [nm] v, s')
  269. end
  270. else acc [fwd ++ [nm = t]]
  271. )
  272. (fn [fwd ::_] [[] ~ fwd] => error <xml>Unknown JSON object variant name {[name]}</xml>)
  273. fl jss names) [[]] !
  274. val s' = skipSpaces s'
  275. val s' = if String.length s' <> 0 && String.sub s' 0 = #"," then
  276. skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1})
  277. else
  278. s'
  279. in
  280. if String.length s' = 0 then
  281. error <xml>JSON object doesn't end in brace</xml>
  282. else if String.sub s' 0 = #"}" then
  283. (r, String.substring s' {Start = 1, Len = String.length s' - 1})
  284. else error <xml>Junk after JSON value in object</xml>
  285. end
  286. }
  287. val json_unit : json unit = json_record {} {}
  288. functor Recursive (M : sig
  289. con t :: Type -> Type
  290. val json_t : a ::: Type -> json a -> json (t a)
  291. end) = struct
  292. open M
  293. datatype r = Rec of t r
  294. fun rTo (Rec x) = (json_t {ToJson = rTo,
  295. FromJson = fn _ => error <xml>Tried to FromJson in ToJson!</xml>}).ToJson x
  296. fun rFrom s =
  297. let
  298. val (x, s') = (json_t {ToJson = fn _ => error <xml>Tried to ToJson in FromJson!</xml>,
  299. FromJson = rFrom}).FromJson s
  300. in
  301. (Rec x, s')
  302. end
  303. val json_r = {ToJson = rTo, FromJson = rFrom}
  304. end