author | wenzelm |
Mon, 27 Nov 2017 11:40:41 +0100 | |
changeset 67095 | 91ffe1f8bf5c |
parent 64824 | 330ec9bc4b75 |
child 67364 | f74672cf83c6 |
permissions | -rw-r--r-- |
55497 | 1 |
/* Title: Pure/ML/ml_lex.scala |
2 |
Author: Makarius |
|
3 |
||
59109 | 4 |
Lexical syntax for Isabelle/ML and Standard ML. |
55497 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
55499 | 9 |
|
10 |
import scala.collection.mutable |
|
64824 | 11 |
import scala.util.parsing.input.Reader |
55497 | 12 |
|
13 |
||
14 |
object ML_Lex |
|
15 |
{ |
|
55505 | 16 |
/** keywords **/ |
17 |
||
18 |
val keywords: Set[String] = |
|
19 |
Set("#", "(", ")", ",", "->", "...", ":", ":>", ";", "=", "=>", |
|
20 |
"[", "]", "_", "{", "|", "}", "abstype", "and", "andalso", "as", |
|
21 |
"case", "datatype", "do", "else", "end", "eqtype", "exception", |
|
22 |
"fn", "fun", "functor", "handle", "if", "in", "include", |
|
23 |
"infix", "infixr", "let", "local", "nonfix", "of", "op", "open", |
|
24 |
"orelse", "raise", "rec", "sharing", "sig", "signature", |
|
25 |
"struct", "structure", "then", "type", "val", "where", "while", |
|
26 |
"with", "withtype") |
|
27 |
||
28 |
val keywords2: Set[String] = |
|
58933 | 29 |
Set("and", "case", "do", "else", "end", "if", "in", "let", "local", |
30 |
"of", "sig", "struct", "then", "while", "with") |
|
55505 | 31 |
|
32 |
val keywords3: Set[String] = |
|
33 |
Set("handle", "open", "raise") |
|
34 |
||
35 |
private val lexicon: Scan.Lexicon = Scan.Lexicon(keywords.toList: _*) |
|
36 |
||
37 |
||
38 |
||
55497 | 39 |
/** tokens **/ |
40 |
||
41 |
object Kind extends Enumeration |
|
42 |
{ |
|
43 |
val KEYWORD = Value("keyword") |
|
44 |
val IDENT = Value("identifier") |
|
45 |
val LONG_IDENT = Value("long identifier") |
|
46 |
val TYPE_VAR = Value("type variable") |
|
47 |
val WORD = Value("word") |
|
48 |
val INT = Value("integer") |
|
49 |
val REAL = Value("real") |
|
50 |
val CHAR = Value("character") |
|
51 |
val STRING = Value("quoted string") |
|
52 |
val SPACE = Value("white space") |
|
53 |
val COMMENT = Value("comment text") |
|
61471 | 54 |
val CONTROL = Value("control symbol antiquotation") |
55512 | 55 |
val ANTIQ = Value("antiquotation") |
56 |
val ANTIQ_START = Value("antiquotation: start") |
|
57 |
val ANTIQ_STOP = Value("antiquotation: stop") |
|
58 |
val ANTIQ_OTHER = Value("antiquotation: other") |
|
59 |
val ANTIQ_STRING = Value("antiquotation: quoted string") |
|
60 |
val ANTIQ_ALT_STRING = Value("antiquotation: back-quoted string") |
|
61 |
val ANTIQ_CARTOUCHE = Value("antiquotation: text cartouche") |
|
55497 | 62 |
val ERROR = Value("bad input") |
63 |
} |
|
64 |
||
60215 | 65 |
sealed case class Token(kind: Kind.Value, source: String) |
55500 | 66 |
{ |
55501 | 67 |
def is_keyword: Boolean = kind == Kind.KEYWORD |
55505 | 68 |
def is_delimiter: Boolean = is_keyword && !Symbol.is_ascii_identifier(source) |
63610 | 69 |
def is_space: Boolean = kind == Kind.SPACE |
70 |
def is_comment: Boolean = kind == Kind.COMMENT |
|
55500 | 71 |
} |
55497 | 72 |
|
73 |
||
74 |
||
75 |
/** parsers **/ |
|
76 |
||
55510
1585a65aad64
tuned signature -- emphasize line-oriented aspect;
wenzelm
parents:
55505
diff
changeset
|
77 |
case object ML_String extends Scan.Line_Context |
55512 | 78 |
case class Antiq(ctxt: Scan.Line_Context) extends Scan.Line_Context |
55499 | 79 |
|
55512 | 80 |
private object Parsers extends Scan.Parsers with Antiquote.Parsers |
55497 | 81 |
{ |
82 |
/* string material */ |
|
83 |
||
55500 | 84 |
private val blanks = many(character(Symbol.is_ascii_blank)) |
55497 | 85 |
private val blanks1 = many1(character(Symbol.is_ascii_blank)) |
86 |
||
55499 | 87 |
private val gap = "\\" ~ blanks1 ~ "\\" ^^ { case x ~ y ~ z => x + y + z } |
55500 | 88 |
private val gap_start = "\\" ~ blanks ~ """\z""".r ^^ { case x ~ y ~ _ => x + y } |
55499 | 89 |
|
55497 | 90 |
private val escape = |
91 |
one(character("\"\\abtnvfr".contains(_))) | |
|
92 |
"^" ~ one(character(c => '@' <= c && c <= '_')) ^^ { case x ~ y => x + y } | |
|
93 |
repeated(character(Symbol.is_ascii_digit), 3, 3) |
|
94 |
||
95 |
private val str = |
|
96 |
one(character(c => c != '"' && c != '\\' && ' ' <= c && c <= '~')) | |
|
59108
50ccc027e8a7
clarified Isabelle/ML strings (refining 72238ea2201c);
wenzelm
parents:
58933
diff
changeset
|
97 |
one(s => Symbol.is_symbolic(s) | Symbol.is_control(s)) | |
55497 | 98 |
"\\" ~ escape ^^ { case x ~ y => x + y } |
99 |
||
55499 | 100 |
|
101 |
/* ML char -- without gaps */ |
|
102 |
||
103 |
private val ml_char: Parser[Token] = |
|
104 |
"#\"" ~ str ~ "\"" ^^ { case x ~ y ~ z => Token(Kind.CHAR, x + y + z) } |
|
105 |
||
106 |
private val recover_ml_char: Parser[String] = |
|
107 |
"#\"" ~ opt(str) ^^ { case x ~ Some(y) => x + y case x ~ None => x } |
|
108 |
||
109 |
||
110 |
/* ML string */ |
|
111 |
||
112 |
private val ml_string_body: Parser[String] = |
|
113 |
rep(gap | str) ^^ (_.mkString) |
|
114 |
||
115 |
private val recover_ml_string: Parser[String] = |
|
116 |
"\"" ~ ml_string_body ^^ { case x ~ y => x + y } |
|
117 |
||
118 |
private val ml_string: Parser[Token] = |
|
119 |
"\"" ~ ml_string_body ~ "\"" ^^ { case x ~ y ~ z => Token(Kind.STRING, x + y + z) } |
|
120 |
||
55510
1585a65aad64
tuned signature -- emphasize line-oriented aspect;
wenzelm
parents:
55505
diff
changeset
|
121 |
private def ml_string_line(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] = |
55499 | 122 |
{ |
55510
1585a65aad64
tuned signature -- emphasize line-oriented aspect;
wenzelm
parents:
55505
diff
changeset
|
123 |
def result(x: String, c: Scan.Line_Context) = (Token(Kind.STRING, x), c) |
55499 | 124 |
|
125 |
ctxt match { |
|
126 |
case Scan.Finished => |
|
127 |
"\"" ~ ml_string_body ~ ("\"" | gap_start) ^^ |
|
128 |
{ case x ~ y ~ z => result(x + y + z, if (z == "\"") Scan.Finished else ML_String) } |
|
129 |
case ML_String => |
|
55500 | 130 |
blanks ~ opt_term("\\" ~ ml_string_body ~ ("\"" | gap_start)) ^^ |
55499 | 131 |
{ case x ~ Some(y ~ z ~ w) => |
132 |
result(x + y + z + w, if (w == "\"") Scan.Finished else ML_String) |
|
133 |
case x ~ None => result(x, ML_String) } |
|
134 |
case _ => failure("") |
|
135 |
} |
|
136 |
} |
|
137 |
||
138 |
||
139 |
/* ML comment */ |
|
140 |
||
141 |
private val ml_comment: Parser[Token] = |
|
142 |
comment ^^ (x => Token(Kind.COMMENT, x)) |
|
143 |
||
55510
1585a65aad64
tuned signature -- emphasize line-oriented aspect;
wenzelm
parents:
55505
diff
changeset
|
144 |
private def ml_comment_line(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] = |
1585a65aad64
tuned signature -- emphasize line-oriented aspect;
wenzelm
parents:
55505
diff
changeset
|
145 |
comment_line(ctxt) ^^ { case (x, c) => (Token(Kind.COMMENT, x), c) } |
55497 | 146 |
|
147 |
||
148 |
/* delimited token */ |
|
149 |
||
150 |
private def delimited_token: Parser[Token] = |
|
61596 | 151 |
ml_char | (ml_string | ml_comment) |
55497 | 152 |
|
55499 | 153 |
private val recover_delimited: Parser[Token] = |
59112 | 154 |
(recover_ml_char | (recover_ml_string | (recover_cartouche | recover_comment))) ^^ |
155 |
(x => Token(Kind.ERROR, x)) |
|
55497 | 156 |
|
157 |
||
158 |
private def other_token: Parser[Token] = |
|
159 |
{ |
|
160 |
/* identifiers */ |
|
161 |
||
162 |
val letdigs = many(character(Symbol.is_ascii_letdig)) |
|
163 |
||
164 |
val alphanumeric = |
|
165 |
one(character(Symbol.is_ascii_letter)) ~ letdigs ^^ { case x ~ y => x + y } |
|
166 |
||
167 |
val symbolic = many1(character("!#$%&*+-/:<=>?@\\^`|~".contains(_))) |
|
168 |
||
169 |
val ident = (alphanumeric | symbolic) ^^ (x => Token(Kind.IDENT, x)) |
|
170 |
||
171 |
val long_ident = |
|
172 |
rep1(alphanumeric ~ "." ^^ { case x ~ y => x + y }) ~ |
|
173 |
(alphanumeric | (symbolic | "=")) ^^ |
|
174 |
{ case x ~ y => Token(Kind.LONG_IDENT, x.mkString + y) } |
|
175 |
||
176 |
val type_var = "'" ~ letdigs ^^ { case x ~ y => Token(Kind.TYPE_VAR, x + y) } |
|
177 |
||
178 |
||
179 |
/* numerals */ |
|
180 |
||
181 |
val dec = many1(character(Symbol.is_ascii_digit)) |
|
182 |
val hex = many1(character(Symbol.is_ascii_hex)) |
|
183 |
val sign = opt("~") ^^ { case Some(x) => x case None => "" } |
|
184 |
val decint = sign ~ dec ^^ { case x ~ y => x + y } |
|
185 |
val exp = ("E" | "e") ~ decint ^^ { case x ~ y => x + y } |
|
186 |
||
187 |
val word = |
|
188 |
("0wx" ~ hex ^^ { case x ~ y => x + y } | "0w" ~ dec ^^ { case x ~ y => x + y }) ^^ |
|
189 |
(x => Token(Kind.WORD, x)) |
|
190 |
||
191 |
val int = |
|
192 |
sign ~ ("0x" ~ hex ^^ { case x ~ y => x + y } | dec) ^^ |
|
193 |
{ case x ~ y => Token(Kind.INT, x + y) } |
|
194 |
||
63204
921a5be54132
support rat numerals via special antiquotation syntax;
wenzelm
parents:
61596
diff
changeset
|
195 |
val rat = |
921a5be54132
support rat numerals via special antiquotation syntax;
wenzelm
parents:
61596
diff
changeset
|
196 |
decint ~ opt("/" ~ dec) ^^ { case x ~ None => x case x ~ Some(y ~ z) => x + y + z } |
921a5be54132
support rat numerals via special antiquotation syntax;
wenzelm
parents:
61596
diff
changeset
|
197 |
|
55497 | 198 |
val real = |
199 |
(decint ~ "." ~ dec ~ (opt(exp) ^^ { case Some(x) => x case None => "" }) ^^ |
|
200 |
{ case x ~ y ~ z ~ w => x + y + z + w } | |
|
201 |
decint ~ exp ^^ { case x ~ y => x + y }) ^^ (x => Token(Kind.REAL, x)) |
|
202 |
||
203 |
||
55499 | 204 |
/* main */ |
55497 | 205 |
|
206 |
val space = blanks1 ^^ (x => Token(Kind.SPACE, x)) |
|
207 |
||
208 |
val keyword = literal(lexicon) ^^ (x => Token(Kind.KEYWORD, x)) |
|
209 |
||
61471 | 210 |
val ml_control = control ^^ (x => Token(Kind.CONTROL, x)) |
63204
921a5be54132
support rat numerals via special antiquotation syntax;
wenzelm
parents:
61596
diff
changeset
|
211 |
val ml_antiq = |
921a5be54132
support rat numerals via special antiquotation syntax;
wenzelm
parents:
61596
diff
changeset
|
212 |
"@" ~ rat ^^ { case x ~ y => Token(Kind.ANTIQ, x + y) } | |
921a5be54132
support rat numerals via special antiquotation syntax;
wenzelm
parents:
61596
diff
changeset
|
213 |
antiq ^^ (x => Token(Kind.ANTIQ, x)) |
55512 | 214 |
|
55497 | 215 |
val bad = one(_ => true) ^^ (x => Token(Kind.ERROR, x)) |
216 |
||
61596 | 217 |
space | (ml_control | (recover_delimited | (ml_antiq | |
61471 | 218 |
(((word | (real | (int | (long_ident | (ident | type_var))))) ||| keyword) | bad)))) |
55497 | 219 |
} |
220 |
||
55499 | 221 |
|
55512 | 222 |
/* antiquotations (line-oriented) */ |
223 |
||
67095
91ffe1f8bf5c
proper treatment of multi-line cartouche as rudiment of antiquotation, e.g. relevant for syntax-highlighting in Isabelle/jEdit;
wenzelm
parents:
64824
diff
changeset
|
224 |
def ml_cartouche_line(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] = |
91ffe1f8bf5c
proper treatment of multi-line cartouche as rudiment of antiquotation, e.g. relevant for syntax-highlighting in Isabelle/jEdit;
wenzelm
parents:
64824
diff
changeset
|
225 |
cartouche_line(ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_CARTOUCHE, x), c) } |
91ffe1f8bf5c
proper treatment of multi-line cartouche as rudiment of antiquotation, e.g. relevant for syntax-highlighting in Isabelle/jEdit;
wenzelm
parents:
64824
diff
changeset
|
226 |
|
55512 | 227 |
def ml_antiq_start(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] = |
228 |
ctxt match { |
|
229 |
case Scan.Finished => "@{" ^^ (x => (Token(Kind.ANTIQ_START, x), Antiq(Scan.Finished))) |
|
230 |
case _ => failure("") |
|
231 |
} |
|
232 |
||
233 |
def ml_antiq_stop(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] = |
|
234 |
ctxt match { |
|
235 |
case Antiq(Scan.Finished) => "}" ^^ (x => (Token(Kind.ANTIQ_STOP, x), Scan.Finished)) |
|
236 |
case _ => failure("") |
|
237 |
} |
|
238 |
||
239 |
def ml_antiq_body(context: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] = |
|
240 |
context match { |
|
241 |
case Antiq(ctxt) => |
|
242 |
(if (ctxt == Scan.Finished) antiq_other ^^ (x => (Token(Kind.ANTIQ_OTHER, x), context)) |
|
243 |
else failure("")) | |
|
244 |
quoted_line("\"", ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_STRING, x), Antiq(c)) } | |
|
245 |
quoted_line("`", ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_ALT_STRING, x), Antiq(c)) } | |
|
246 |
cartouche_line(ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_CARTOUCHE, x), Antiq(c)) } |
|
247 |
case _ => failure("") |
|
248 |
} |
|
249 |
||
250 |
||
55499 | 251 |
/* token */ |
252 |
||
55497 | 253 |
def token: Parser[Token] = delimited_token | other_token |
55499 | 254 |
|
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
55512
diff
changeset
|
255 |
def token_line(SML: Boolean, ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] = |
55499 | 256 |
{ |
257 |
val other = (ml_char | other_token) ^^ (x => (x, Scan.Finished)) |
|
258 |
||
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
55512
diff
changeset
|
259 |
if (SML) ml_string_line(ctxt) | (ml_comment_line(ctxt) | other) |
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
55512
diff
changeset
|
260 |
else |
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
55512
diff
changeset
|
261 |
ml_string_line(ctxt) | |
61596 | 262 |
(ml_comment_line(ctxt) | |
67095
91ffe1f8bf5c
proper treatment of multi-line cartouche as rudiment of antiquotation, e.g. relevant for syntax-highlighting in Isabelle/jEdit;
wenzelm
parents:
64824
diff
changeset
|
263 |
(ml_cartouche_line(ctxt) | |
91ffe1f8bf5c
proper treatment of multi-line cartouche as rudiment of antiquotation, e.g. relevant for syntax-highlighting in Isabelle/jEdit;
wenzelm
parents:
64824
diff
changeset
|
264 |
(ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other))))) |
55499 | 265 |
} |
55497 | 266 |
} |
267 |
||
55499 | 268 |
|
269 |
/* tokenize */ |
|
270 |
||
55497 | 271 |
def tokenize(input: CharSequence): List[Token] = |
64824 | 272 |
Parsers.parseAll(Parsers.rep(Parsers.token), Scan.char_reader(input)) match { |
55497 | 273 |
case Parsers.Success(tokens, _) => tokens |
274 |
case _ => error("Unexpected failure of tokenizing input:\n" + input.toString) |
|
275 |
} |
|
55499 | 276 |
|
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
55512
diff
changeset
|
277 |
def tokenize_line(SML: Boolean, input: CharSequence, context: Scan.Line_Context) |
55510
1585a65aad64
tuned signature -- emphasize line-oriented aspect;
wenzelm
parents:
55505
diff
changeset
|
278 |
: (List[Token], Scan.Line_Context) = |
55499 | 279 |
{ |
64824 | 280 |
var in: Reader[Char] = Scan.char_reader(input) |
55499 | 281 |
val toks = new mutable.ListBuffer[Token] |
282 |
var ctxt = context |
|
283 |
while (!in.atEnd) { |
|
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
55512
diff
changeset
|
284 |
Parsers.parse(Parsers.token_line(SML, ctxt), in) match { |
60215 | 285 |
case Parsers.Success((x, c), rest) => toks += x; ctxt = c; in = rest |
55499 | 286 |
case Parsers.NoSuccess(_, rest) => |
287 |
error("Unexpected failure of tokenizing input:\n" + rest.source.toString) |
|
288 |
} |
|
289 |
} |
|
290 |
(toks.toList, ctxt) |
|
291 |
} |
|
55497 | 292 |
} |