5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
|
10 import scala.util.parsing.combinator.lexical.Scanners |
|
11 import scala.util.parsing.input.CharArrayReader.EofCh |
10 import scala.util.parsing.json.{JSONObject, JSONArray} |
12 import scala.util.parsing.json.{JSONObject, JSONArray} |
|
13 |
11 |
14 |
12 object JSON |
15 object JSON |
13 { |
16 { |
14 type T = Any |
17 type T = Any |
15 type S = String |
18 type S = String |
|
19 |
|
20 |
|
21 /* lexer */ |
|
22 |
|
23 object Kind extends Enumeration |
|
24 { |
|
25 val KEYWORD, STRING, NUMBER, ERROR = Value |
|
26 } |
|
27 |
|
28 sealed case class Token(kind: Kind.Value, text: String) |
|
29 { |
|
30 def is_keyword: Boolean = kind == Kind.KEYWORD |
|
31 def is_string: Boolean = kind == Kind.STRING |
|
32 def is_number: Boolean = kind == Kind.NUMBER |
|
33 def is_error: Boolean = kind == Kind.ERROR |
|
34 } |
|
35 |
|
36 object Lexer extends Scanners with Scan.Parsers |
|
37 { |
|
38 override type Elem = Char |
|
39 type Token = JSON.Token |
|
40 |
|
41 def errorToken(msg: String): Token = Token(Kind.ERROR, msg) |
|
42 |
|
43 override val whiteSpace = """\s+""".r |
|
44 def whitespace: Parser[Any] = many(character(Symbol.is_ascii_blank(_))) |
|
45 |
|
46 val letter: Parser[String] = one(character(Symbol.is_ascii_letter(_))) |
|
47 val letters1: Parser[String] = many1(character(Symbol.is_ascii_letter(_))) |
|
48 |
|
49 def digits: Parser[String] = many(character(Symbol.is_ascii_digit(_))) |
|
50 def digits1: Parser[String] = many1(character(Symbol.is_ascii_digit(_))) |
|
51 |
|
52 |
|
53 /* keyword */ |
|
54 |
|
55 def keyword: Parser[Token] = |
|
56 elem("keyword", "{}[],:".contains(_)) ^^ (c => Token(Kind.KEYWORD, c.toString)) | |
|
57 letters1 ^^ (s => |
|
58 if (s == "true" || s == "false" || s == "null") Token(Kind.KEYWORD, s) |
|
59 else errorToken("Bad keyword: " + quote(s))) |
|
60 |
|
61 |
|
62 /* string */ |
|
63 |
|
64 def string: Parser[Token] = |
|
65 '\"' ~> rep(string_body) <~ '\"' ^^ (cs => Token(Kind.STRING, cs.mkString)) |
|
66 |
|
67 def string_body: Parser[Char] = |
|
68 elem("", c => c != '\"' && c != '\\' && c != EofCh) | '\\' ~> string_escape |
|
69 |
|
70 def string_escape: Parser[Char] = |
|
71 elem("", "\"\\/".contains(_)) | |
|
72 elem("", "bfnrt".contains(_)) ^^ |
|
73 { case 'b' => '\b' case 'f' => '\f' case 'n' => '\n' case 'r' => '\r' case 't' => '\t' } | |
|
74 'u' ~> repeated(character("0123456789abcdefABCDEF".contains(_)), 4, 4) ^^ |
|
75 (s => Integer.parseInt(s, 16).toChar) |
|
76 |
|
77 def string_failure: Parser[Token] = '\"' ~> failure("Unterminated string") |
|
78 |
|
79 |
|
80 /* number */ |
|
81 |
|
82 def number: Parser[Token] = |
|
83 opt("-" <~ whitespace) ~ number_body ~ opt(letter) ^^ { |
|
84 case a ~ b ~ None => Token(Kind.NUMBER, a.getOrElse("") + b) |
|
85 case a ~ b ~ Some(c) => |
|
86 errorToken("Invalid number format: " + quote(a.getOrElse("") + b + c)) |
|
87 } |
|
88 |
|
89 def number_body: Parser[String] = |
|
90 (zero | positive) ~ opt(number_fract) ~ opt(number_exp) ^^ |
|
91 { case a ~ b ~ c => a + b.getOrElse("") + c.getOrElse("") } |
|
92 |
|
93 def number_fract: Parser[String] = "." ~ digits1 ^^ { case a ~ b => a + b } |
|
94 |
|
95 def number_exp: Parser[String] = |
|
96 one(character("eE".contains(_))) ~ maybe(character("-+".contains(_))) ~ digits1 ^^ |
|
97 { case a ~ b ~ c => a + b + c } |
|
98 |
|
99 def zero = one(character(c => c == '0')) |
|
100 def nonzero = one(character(c => c != '0' && Symbol.is_ascii_digit(c))) |
|
101 def positive: Parser[String] = nonzero ~ digits ^^ { case a ~ b => a + b } |
|
102 |
|
103 |
|
104 /* token */ |
|
105 |
|
106 def token: Parser[Token] = |
|
107 keyword | (string | (string_failure | (number | failure("Illegal character")))) |
|
108 } |
16 |
109 |
17 |
110 |
18 /* standard format */ |
111 /* standard format */ |
19 |
112 |
20 def parse(s: S): T = Format.unapply(s) getOrElse error("Malformed JSON") |
113 def parse(s: S): T = Format.unapply(s) getOrElse error("Malformed JSON") |