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