1/* Title: Pure/General/json.scala 2 Author: Makarius 3 4Support for JSON: https://www.json.org/. 5 6See also http://seriot.ch/parsing_json.php "Parsing JSON is a Minefield". 7*/ 8 9package isabelle 10 11 12import scala.util.parsing.combinator.Parsers 13import scala.util.parsing.combinator.lexical.Scanners 14import scala.util.parsing.input.CharArrayReader.EofCh 15 16 17object JSON 18{ 19 type T = Any 20 type S = String 21 22 object Object 23 { 24 type Entry = (String, JSON.T) 25 26 type T = Map[String, JSON.T] 27 val empty: Object.T = Map.empty 28 29 def apply(entries: Entry*): Object.T = Map(entries:_*) 30 31 def unapply(obj: T): Option[Object.T] = 32 obj match { 33 case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) => 34 Some(m.asInstanceOf[Object.T]) 35 case _ => None 36 } 37 } 38 39 40 /* lexer */ 41 42 object Kind extends Enumeration 43 { 44 val KEYWORD, STRING, NUMBER, ERROR = Value 45 } 46 47 sealed case class Token(kind: Kind.Value, text: String) 48 { 49 def is_keyword: Boolean = kind == Kind.KEYWORD 50 def is_keyword(name: String): Boolean = kind == Kind.KEYWORD && text == name 51 def is_string: Boolean = kind == Kind.STRING 52 def is_number: Boolean = kind == Kind.NUMBER 53 def is_error: Boolean = kind == Kind.ERROR 54 } 55 56 object Lexer extends Scanners with Scan.Parsers 57 { 58 override type Elem = Char 59 type Token = JSON.Token 60 61 def errorToken(msg: String): Token = Token(Kind.ERROR, msg) 62 63 val white_space: String = " \t\n\r" 64 override val whiteSpace = ("[" + white_space + "]+").r 65 def whitespace: Parser[Any] = many(character(white_space.contains(_))) 66 67 val letter: Parser[String] = one(character(Symbol.is_ascii_letter(_))) 68 val letters1: Parser[String] = many1(character(Symbol.is_ascii_letter(_))) 69 70 def digits: Parser[String] = many(character(Symbol.is_ascii_digit(_))) 71 def digits1: Parser[String] = many1(character(Symbol.is_ascii_digit(_))) 72 73 74 /* keyword */ 75 76 def keyword: Parser[Token] = 77 (letters1 | one(character("{}[],:".contains(_)))) ^^ (s => Token(Kind.KEYWORD, s)) 78 79 80 /* string */ 81 82 def string: Parser[Token] = 83 '\"' ~> rep(string_body) <~ '\"' ^^ (cs => Token(Kind.STRING, cs.mkString)) 84 85 def string_body: Parser[Char] = 86 elem("", c => c > '\u001f' && c != '\"' && c != '\\' && c != EofCh) | '\\' ~> string_escape 87 88 def string_escape: Parser[Char] = 89 elem("", "\"\\/".contains(_)) | 90 elem("", "bfnrt".contains(_)) ^^ 91 { case 'b' => '\b' case 'f' => '\f' case 'n' => '\n' case 'r' => '\r' case 't' => '\t' } | 92 'u' ~> repeated(character("0123456789abcdefABCDEF".contains(_)), 4, 4) ^^ 93 (s => Integer.parseInt(s, 16).toChar) 94 95 def string_failure: Parser[Token] = '\"' ~> failure("Unterminated string") 96 97 98 /* number */ 99 100 def number: Parser[Token] = 101 opt("-") ~ number_body ~ opt(letter) ^^ { 102 case a ~ b ~ None => Token(Kind.NUMBER, a.getOrElse("") + b) 103 case a ~ b ~ Some(c) => 104 errorToken("Invalid number format: " + quote(a.getOrElse("") + b + c)) 105 } 106 107 def number_body: Parser[String] = 108 (zero | positive) ~ opt(number_fract) ~ opt(number_exp) ^^ 109 { case a ~ b ~ c => a + b.getOrElse("") + c.getOrElse("") } 110 111 def number_fract: Parser[String] = "." ~ digits1 ^^ { case a ~ b => a + b } 112 113 def number_exp: Parser[String] = 114 one(character("eE".contains(_))) ~ maybe(character("-+".contains(_))) ~ digits1 ^^ 115 { case a ~ b ~ c => a + b + c } 116 117 def zero = one(character(c => c == '0')) 118 def nonzero = one(character(c => c != '0' && Symbol.is_ascii_digit(c))) 119 def positive: Parser[String] = nonzero ~ digits ^^ { case a ~ b => a + b } 120 121 122 /* token */ 123 124 def token: Parser[Token] = 125 keyword | (string | (string_failure | (number | failure("Illegal character")))) 126 } 127 128 129 /* parser */ 130 131 trait Parser extends Parsers 132 { 133 type Elem = Token 134 135 def $$$(name: String): Parser[Token] = elem(name, _.is_keyword(name)) 136 def string: Parser[String] = elem("string", _.is_string) ^^ (_.text) 137 def number: Parser[Double] = elem("number", _.is_number) ^^ (tok => tok.text.toDouble) 138 139 def json_object: Parser[Object.T] = 140 $$$("{") ~> 141 repsep(string ~ ($$$(":") ~> json_value) ^^ { case a ~ b => (a, b) }, $$$(",")) <~ 142 $$$("}") ^^ (_.toMap) 143 144 def json_array: Parser[List[T]] = 145 $$$("[") ~> repsep(json_value, $$$(",")) <~ $$$("]") 146 147 def json_value: Parser[T] = 148 json_object | (json_array | (number | (string | 149 ($$$("true") ^^^ true | ($$$("false") ^^^ false | ($$$("null") ^^^ null)))))) 150 151 def parse(input: CharSequence, strict: Boolean): T = 152 { 153 val scanner = new Lexer.Scanner(Scan.char_reader(input)) 154 phrase(if (strict) json_object | json_array else json_value)(scanner) match { 155 case Success(json, _) => json 156 case NoSuccess(_, next) => error("Malformed JSON input at " + next.pos) 157 } 158 } 159 } 160 161 object Parser extends Parser 162 163 164 /* standard format */ 165 166 def parse(s: S, strict: Boolean = true): T = Parser.parse(s, strict) 167 168 object Format 169 { 170 def unapply(s: S): Option[T] = 171 try { Some(parse(s, strict = false)) } 172 catch { case ERROR(_) => None } 173 174 def apply(json: T): S = 175 { 176 val result = new StringBuilder 177 178 def string(s: String) 179 { 180 result += '"' 181 result ++= 182 s.iterator.map { 183 case '"' => "\\\"" 184 case '\\' => "\\\\" 185 case '\b' => "\\b" 186 case '\f' => "\\f" 187 case '\n' => "\\n" 188 case '\r' => "\\r" 189 case '\t' => "\\t" 190 case c => 191 if (c <= '\u001f' || c >= '\u007f' && c <= '\u009f') "\\u%04x".format(c.toInt) 192 else c 193 }.mkString 194 result += '"' 195 } 196 197 def array(list: List[T]) 198 { 199 result += '[' 200 Library.separate(None, list.map(Some(_))).foreach({ 201 case None => result += ',' 202 case Some(x) => json_format(x) 203 }) 204 result += ']' 205 } 206 207 def object_(obj: Object.T) 208 { 209 result += '{' 210 Library.separate(None, obj.toList.map(Some(_))).foreach({ 211 case None => result += ',' 212 case Some((x, y)) => 213 string(x) 214 result += ':' 215 json_format(y) 216 }) 217 result += '}' 218 } 219 220 def json_format(x: T) 221 { 222 x match { 223 case null => result ++= "null" 224 case _: Int | _: Long | _: Boolean => result ++= x.toString 225 case n: Double => 226 val i = n.toLong 227 result ++= (if (i.toDouble == n) i.toString else n.toString) 228 case s: String => string(s) 229 case Object(m) => object_(m) 230 case list: List[T] => array(list) 231 case _ => error("Bad JSON value: " + x.toString) 232 } 233 } 234 235 json_format(json) 236 result.toString 237 } 238 } 239 240 241 /* typed values */ 242 243 object Value 244 { 245 object UUID 246 { 247 def unapply(json: T): Option[java.util.UUID] = 248 json match { 249 case x: java.lang.String => 250 try { Some(java.util.UUID.fromString(x)) } 251 catch { case _: IllegalArgumentException => None } 252 case _ => None 253 } 254 } 255 256 object String { 257 def unapply(json: T): Option[java.lang.String] = 258 json match { 259 case x: java.lang.String => Some(x) 260 case _ => None 261 } 262 } 263 264 object Double { 265 def unapply(json: T): Option[scala.Double] = 266 json match { 267 case x: scala.Double => Some(x) 268 case x: scala.Long => Some(x.toDouble) 269 case x: scala.Int => Some(x.toDouble) 270 case _ => None 271 } 272 } 273 274 object Long { 275 def unapply(json: T): Option[scala.Long] = 276 json match { 277 case x: scala.Double if x.toLong.toDouble == x => Some(x.toLong) 278 case x: scala.Long => Some(x) 279 case x: scala.Int => Some(x.toLong) 280 case _ => None 281 } 282 } 283 284 object Int { 285 def unapply(json: T): Option[scala.Int] = 286 json match { 287 case x: scala.Double if x.toInt.toDouble == x => Some(x.toInt) 288 case x: scala.Long if x.toInt.toLong == x => Some(x.toInt) 289 case x: scala.Int => Some(x) 290 case _ => None 291 } 292 } 293 294 object Boolean { 295 def unapply(json: T): Option[scala.Boolean] = 296 json match { 297 case x: scala.Boolean => Some(x) 298 case _ => None 299 } 300 } 301 302 object List 303 { 304 def unapply[A](json: T, unapply: T => Option[A]): Option[List[A]] = 305 json match { 306 case xs: List[T] => 307 val ys = xs.map(unapply) 308 if (ys.forall(_.isDefined)) Some(ys.map(_.get)) else None 309 case _ => None 310 } 311 } 312 } 313 314 315 /* object values */ 316 317 def optional(entry: (String, Option[T])): Object.T = 318 entry match { 319 case (name, Some(x)) => Object(name -> x) 320 case (_, None) => Object.empty 321 } 322 323 def value(obj: T, name: String): Option[T] = 324 obj match { 325 case Object(m) => m.get(name) 326 case _ => None 327 } 328 329 def value[A](obj: T, name: String, unapply: T => Option[A]): Option[A] = 330 for { 331 json <- value(obj, name) 332 x <- unapply(json) 333 } yield x 334 335 def array(obj: T, name: String): Option[List[T]] = 336 value(obj, name) match { 337 case Some(a: List[T]) => Some(a) 338 case _ => None 339 } 340 341 def value_default[A](obj: T, name: String, unapply: T => Option[A], default: => A): Option[A] = 342 value(obj, name) match { 343 case None => Some(default) 344 case Some(json) => unapply(json) 345 } 346 347 def uuid(obj: T, name: String): Option[UUID] = 348 value(obj, name, Value.UUID.unapply) 349 350 def string(obj: T, name: String): Option[String] = 351 value(obj, name, Value.String.unapply) 352 def string_default(obj: T, name: String, default: => String = ""): Option[String] = 353 value_default(obj, name, Value.String.unapply, default) 354 355 def double(obj: T, name: String): Option[Double] = 356 value(obj, name, Value.Double.unapply) 357 def double_default(obj: T, name: String, default: => Double = 0.0): Option[Double] = 358 value_default(obj, name, Value.Double.unapply, default) 359 360 def long(obj: T, name: String): Option[Long] = 361 value(obj, name, Value.Long.unapply) 362 def long_default(obj: T, name: String, default: => Long = 0): Option[Long] = 363 value_default(obj, name, Value.Long.unapply, default) 364 365 def int(obj: T, name: String): Option[Int] = 366 value(obj, name, Value.Int.unapply) 367 def int_default(obj: T, name: String, default: => Int = 0): Option[Int] = 368 value_default(obj, name, Value.Int.unapply, default) 369 370 def bool(obj: T, name: String): Option[Boolean] = 371 value(obj, name, Value.Boolean.unapply) 372 def bool_default(obj: T, name: String, default: => Boolean = false): Option[Boolean] = 373 value_default(obj, name, Value.Boolean.unapply, default) 374 375 def list[A](obj: T, name: String, unapply: T => Option[A]): Option[List[A]] = 376 value(obj, name, Value.List.unapply(_, unapply)) 377 def list_default[A](obj: T, name: String, unapply: T => Option[A], default: => List[A] = Nil) 378 : Option[List[A]] = value_default(obj, name, Value.List.unapply(_, unapply), default) 379} 380