src/Pure/ML/ml_lex.ML
author wenzelm
Mon Jun 01 23:28:05 2009 +0200 (2009-06-01)
changeset 31332 9639a6d4d714
parent 30683 e8ac1f9d9469
child 31426 5c9dbd511510
permissions -rw-r--r--
added flatten;
wenzelm@24579
     1
(*  Title:      Pure/ML/ml_lex.ML
wenzelm@24579
     2
    Author:     Makarius
wenzelm@24579
     3
wenzelm@24579
     4
Lexical syntax for SML.
wenzelm@24579
     5
*)
wenzelm@24579
     6
wenzelm@24579
     7
signature ML_LEX =
wenzelm@24579
     8
sig
wenzelm@24579
     9
  datatype token_kind =
wenzelm@24596
    10
    Keyword | Ident | LongIdent | TypeVar | Word | Int | Real | Char | String |
wenzelm@24579
    11
    Space | Comment | Error of string | EOF
wenzelm@24579
    12
  eqtype token
wenzelm@27732
    13
  val stopper: token Scan.stopper
wenzelm@24596
    14
  val is_regular: token -> bool
wenzelm@24596
    15
  val is_improper: token -> bool
wenzelm@30683
    16
  val set_range: Position.range -> token -> token
wenzelm@30636
    17
  val pos_of: token -> Position.T
wenzelm@24579
    18
  val kind_of: token -> token_kind
wenzelm@27817
    19
  val content_of: token -> string
wenzelm@30636
    20
  val text_of: token -> string
wenzelm@31332
    21
  val flatten: token list -> string
wenzelm@30614
    22
  val report_token: token -> unit
wenzelm@24579
    23
  val keywords: string list
wenzelm@24596
    24
  val source: (Symbol.symbol, 'a) Source.source ->
wenzelm@30573
    25
    (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
wenzelm@27772
    26
      Source.source) Source.source
wenzelm@30591
    27
  val tokenize: string -> token list
wenzelm@30645
    28
  val read_antiq: Symbol_Pos.T list * Position.T -> token Antiquote.antiquote list
wenzelm@24579
    29
end;
wenzelm@24579
    30
wenzelm@24579
    31
structure ML_Lex: ML_LEX =
wenzelm@24579
    32
struct
wenzelm@24579
    33
wenzelm@24579
    34
(** tokens **)
wenzelm@24579
    35
wenzelm@24579
    36
(* datatype token *)
wenzelm@24579
    37
wenzelm@24579
    38
datatype token_kind =
wenzelm@24596
    39
  Keyword | Ident | LongIdent | TypeVar | Word | Int | Real | Char | String |
wenzelm@24579
    40
  Space | Comment | Error of string | EOF;
wenzelm@24579
    41
wenzelm@27772
    42
datatype token = Token of Position.range * (token_kind * string);
wenzelm@27772
    43
wenzelm@27772
    44
wenzelm@27772
    45
(* position *)
wenzelm@27772
    46
wenzelm@30683
    47
fun set_range range (Token (_, x)) = Token (range, x);
wenzelm@30683
    48
wenzelm@30636
    49
fun pos_of (Token ((pos, _), _)) = pos;
wenzelm@30636
    50
fun end_pos_of (Token ((_, pos), _)) = pos;
wenzelm@24579
    51
wenzelm@24579
    52
wenzelm@24596
    53
(* control tokens *)
wenzelm@24579
    54
wenzelm@27772
    55
fun mk_eof pos = Token ((pos, Position.none), (EOF, ""));
wenzelm@27772
    56
val eof = mk_eof Position.none;
wenzelm@24579
    57
wenzelm@24579
    58
fun is_eof (Token (_, (EOF, _))) = true
wenzelm@24579
    59
  | is_eof _ = false;
wenzelm@24579
    60
wenzelm@27772
    61
val stopper =
wenzelm@30636
    62
  Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;
wenzelm@27772
    63
wenzelm@24579
    64
wenzelm@27772
    65
(* token content *)
wenzelm@27772
    66
wenzelm@27817
    67
fun content_of (Token (_, (_, x))) = x;
wenzelm@27817
    68
fun token_leq (tok, tok') = content_of tok <= content_of tok';
wenzelm@27772
    69
wenzelm@27772
    70
fun kind_of (Token (_, (k, _))) = k;
wenzelm@24579
    71
wenzelm@30636
    72
fun text_of tok =
wenzelm@30636
    73
  (case kind_of tok of
wenzelm@30645
    74
    Error msg => error msg
wenzelm@30636
    75
  | _ => Symbol.escape (content_of tok));
wenzelm@30636
    76
wenzelm@31332
    77
val flatten = implode o map text_of;
wenzelm@31332
    78
wenzelm@24596
    79
fun is_regular (Token (_, (Error _, _))) = false
wenzelm@24596
    80
  | is_regular (Token (_, (EOF, _))) = false
wenzelm@24596
    81
  | is_regular _ = true;
wenzelm@24596
    82
wenzelm@24596
    83
fun is_improper (Token (_, (Space, _))) = true
wenzelm@24596
    84
  | is_improper (Token (_, (Comment, _))) = true
wenzelm@24596
    85
  | is_improper _ = false;
wenzelm@24596
    86
wenzelm@24596
    87
wenzelm@30614
    88
(* markup *)
wenzelm@30614
    89
wenzelm@30645
    90
val token_kind_markup =
wenzelm@30645
    91
 fn Keyword   => Markup.ML_keyword
wenzelm@30645
    92
  | Ident     => Markup.ML_ident
wenzelm@30645
    93
  | LongIdent => Markup.ML_ident
wenzelm@30645
    94
  | TypeVar   => Markup.ML_tvar
wenzelm@30645
    95
  | Word      => Markup.ML_numeral
wenzelm@30645
    96
  | Int       => Markup.ML_numeral
wenzelm@30645
    97
  | Real      => Markup.ML_numeral
wenzelm@30645
    98
  | Char      => Markup.ML_char
wenzelm@30645
    99
  | String    => Markup.ML_string
wenzelm@30645
   100
  | Space     => Markup.none
wenzelm@30645
   101
  | Comment   => Markup.ML_comment
wenzelm@30645
   102
  | Error _   => Markup.ML_malformed
wenzelm@30645
   103
  | EOF       => Markup.none;
wenzelm@30614
   104
wenzelm@30645
   105
fun report_token (Token ((pos, _), (kind, _))) =
wenzelm@30645
   106
  Position.report (token_kind_markup kind) pos;
wenzelm@30614
   107
wenzelm@30614
   108
wenzelm@24579
   109
wenzelm@24579
   110
(** scanners **)
wenzelm@24579
   111
wenzelm@30573
   112
open Basic_Symbol_Pos;
wenzelm@24579
   113
wenzelm@30573
   114
fun !!! msg = Symbol_Pos.!!! ("SML lexical error: " ^ msg);
wenzelm@24579
   115
wenzelm@24579
   116
wenzelm@27772
   117
(* blanks *)
wenzelm@24579
   118
wenzelm@27772
   119
val scan_blank = Scan.one (Symbol.is_ascii_blank o symbol);
wenzelm@27772
   120
val scan_blanks1 = Scan.repeat1 scan_blank;
wenzelm@24579
   121
wenzelm@24579
   122
wenzelm@24579
   123
(* keywords *)
wenzelm@24579
   124
wenzelm@24579
   125
val keywords = ["#", "(", ")", ",", "->", "...", ":", ":>", ";", "=",
wenzelm@24579
   126
  "=>", "[", "]", "_", "{", "|", "}", "abstype", "and", "andalso", "as",
wenzelm@24579
   127
  "case", "datatype", "do", "else", "end", "eqtype", "exception", "fn",
wenzelm@24579
   128
  "fun", "functor", "handle", "if", "in", "include", "infix", "infixr",
wenzelm@24579
   129
  "let", "local", "nonfix", "of", "op", "open", "orelse", "raise", "rec",
wenzelm@24579
   130
  "sharing", "sig", "signature", "struct", "structure", "then", "type",
wenzelm@24579
   131
  "val", "where", "while", "with", "withtype"];
wenzelm@24579
   132
wenzelm@27772
   133
val lex = Scan.make_lexicon (map explode keywords);
wenzelm@27772
   134
fun scan_keyword x = Scan.literal lex x;
wenzelm@24579
   135
wenzelm@24579
   136
wenzelm@24579
   137
(* identifiers *)
wenzelm@24579
   138
wenzelm@24596
   139
local
wenzelm@24596
   140
wenzelm@24579
   141
val scan_letdigs =
wenzelm@27772
   142
  Scan.many ((Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf Symbol.is_ascii_quasi) o symbol);
wenzelm@24579
   143
wenzelm@27772
   144
val scan_alphanumeric = Scan.one (Symbol.is_ascii_letter o symbol) -- scan_letdigs >> op ::;
wenzelm@24579
   145
wenzelm@27772
   146
val scan_symbolic = Scan.many1 (member (op =) (explode "!#$%&*+-/:<=>?@\\^`|~") o symbol);
wenzelm@24579
   147
wenzelm@24596
   148
in
wenzelm@24596
   149
wenzelm@24579
   150
val scan_ident = scan_alphanumeric || scan_symbolic;
wenzelm@24579
   151
wenzelm@24579
   152
val scan_longident =
wenzelm@27772
   153
  (Scan.repeat1 (scan_alphanumeric @@@ $$$ ".") >> flat) @@@ (scan_ident || $$$ "=");
wenzelm@24579
   154
wenzelm@27772
   155
val scan_typevar = $$$ "'" @@@ scan_letdigs;
wenzelm@24579
   156
wenzelm@24596
   157
end;
wenzelm@24579
   158
wenzelm@24579
   159
wenzelm@24579
   160
(* numerals *)
wenzelm@24579
   161
wenzelm@24596
   162
local
wenzelm@24596
   163
wenzelm@27772
   164
val scan_dec = Scan.many1 (Symbol.is_ascii_digit o symbol);
wenzelm@27772
   165
val scan_hex = Scan.many1 (Symbol.is_ascii_hex o symbol);
wenzelm@27772
   166
val scan_sign = Scan.optional ($$$ "~") [];
wenzelm@27772
   167
val scan_decint = scan_sign @@@ scan_dec;
wenzelm@24579
   168
wenzelm@24596
   169
in
wenzelm@24596
   170
wenzelm@27772
   171
val scan_word =
wenzelm@27772
   172
  $$$ "0" @@@ $$$ "w" @@@ $$$ "x" @@@ scan_hex ||
wenzelm@27772
   173
  $$$ "0" @@@ $$$ "w" @@@ scan_dec;
wenzelm@24579
   174
wenzelm@27772
   175
val scan_int = scan_sign @@@ ($$$ "0" @@@ $$$ "x" @@@ scan_hex || scan_dec);
wenzelm@24579
   176
wenzelm@27772
   177
val scan_exp = ($$$ "E" || $$$ "e") @@@ scan_decint;
wenzelm@24579
   178
wenzelm@24579
   179
val scan_real =
wenzelm@27772
   180
  scan_decint @@@ $$$ "." @@@ scan_dec @@@ Scan.optional scan_exp [] ||
wenzelm@27772
   181
  scan_decint @@@ scan_exp;
wenzelm@24579
   182
wenzelm@24596
   183
end;
wenzelm@24596
   184
wenzelm@24579
   185
wenzelm@24579
   186
(* chars and strings *)
wenzelm@24579
   187
wenzelm@24596
   188
local
wenzelm@24596
   189
wenzelm@24596
   190
val scan_escape =
wenzelm@27772
   191
  Scan.one (member (op =) (explode "\"\\abtnvfr") o symbol) >> single ||
wenzelm@27772
   192
  $$$ "^" @@@ (Scan.one (fn (s, _) => ord "@" <= ord s andalso ord s <= ord "_") >> single) ||
wenzelm@27772
   193
  Scan.one (Symbol.is_ascii_digit o symbol) --
wenzelm@27772
   194
    Scan.one (Symbol.is_ascii_digit o symbol) --
wenzelm@27772
   195
    Scan.one (Symbol.is_ascii_digit o symbol) >> (fn ((a, b), c) => [a, b, c]);
wenzelm@24596
   196
wenzelm@24596
   197
val scan_str =
wenzelm@30600
   198
  Scan.one (fn (s, _) => Symbol.is_regular s andalso s <> "\"" andalso s <> "\\" andalso
wenzelm@30600
   199
    (not (Symbol.is_char s) orelse Symbol.is_printable s)) >> single ||
wenzelm@27772
   200
  $$$ "\\" @@@ !!! "bad escape character in string" scan_escape;
wenzelm@24596
   201
wenzelm@27772
   202
val scan_gap = $$$ "\\" @@@ scan_blanks1 @@@ $$$ "\\";
wenzelm@27772
   203
val scan_gaps = Scan.repeat scan_gap >> flat;
wenzelm@24579
   204
wenzelm@24596
   205
in
wenzelm@24579
   206
wenzelm@24579
   207
val scan_char =
wenzelm@27772
   208
  $$$ "#" @@@ $$$ "\"" @@@ scan_gaps @@@ scan_str @@@ scan_gaps @@@ $$$ "\"";
wenzelm@24579
   209
wenzelm@24579
   210
val scan_string =
wenzelm@27772
   211
  $$$ "\"" @@@ !!! "missing quote at end of string"
wenzelm@27772
   212
    ((Scan.repeat (scan_gap || scan_str) >> flat) @@@ $$$ "\"");
wenzelm@24596
   213
wenzelm@24596
   214
end;
wenzelm@24579
   215
wenzelm@24579
   216
wenzelm@30645
   217
(* scan tokens *)
wenzelm@24579
   218
wenzelm@24579
   219
local
wenzelm@24579
   220
wenzelm@30593
   221
fun token k ss = Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss));
wenzelm@24579
   222
wenzelm@30593
   223
val scan_ml =
wenzelm@27772
   224
 (scan_char >> token Char ||
wenzelm@27772
   225
  scan_string >> token String ||
wenzelm@27772
   226
  scan_blanks1 >> token Space ||
wenzelm@30573
   227
  Symbol_Pos.scan_comment !!! >> token Comment ||
wenzelm@27772
   228
  Scan.max token_leq
wenzelm@27772
   229
   (scan_keyword >> token Keyword)
wenzelm@27772
   230
   (scan_word >> token Word ||
wenzelm@27772
   231
    scan_real >> token Real ||
wenzelm@27772
   232
    scan_int >> token Int ||
wenzelm@27772
   233
    scan_longident >> token LongIdent ||
wenzelm@27772
   234
    scan_ident >> token Ident ||
wenzelm@27772
   235
    scan_typevar >> token TypeVar));
wenzelm@27772
   236
wenzelm@30645
   237
val scan_antiq = Antiquote.scan || scan_ml >> Antiquote.Text;
wenzelm@30645
   238
wenzelm@27772
   239
fun recover msg =
wenzelm@27772
   240
  Scan.many (((not o Symbol.is_blank) andf Symbol.is_regular) o symbol)
wenzelm@27772
   241
  >> (fn cs => [token (Error msg) cs]);
wenzelm@24579
   242
wenzelm@24579
   243
in
wenzelm@24579
   244
wenzelm@24596
   245
fun source src =
wenzelm@30573
   246
  Symbol_Pos.source (Position.line 1) src
wenzelm@30593
   247
  |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_ml)) (SOME (false, recover));
wenzelm@30591
   248
wenzelm@30591
   249
val tokenize = Source.of_string #> source #> Source.exhaust;
wenzelm@24579
   250
wenzelm@30645
   251
fun read_antiq (syms, pos) =
wenzelm@30645
   252
  (Source.of_list syms
wenzelm@30645
   253
    |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq))
wenzelm@30645
   254
      (SOME (false, fn msg => recover msg >> map Antiquote.Text))
wenzelm@30645
   255
    |> Source.exhaust
wenzelm@30645
   256
    |> tap (List.app (Antiquote.report report_token))
wenzelm@30645
   257
    |> tap Antiquote.check_nesting
wenzelm@30645
   258
    |> tap (List.app (fn Antiquote.Text tok => ignore (text_of tok) | _ => ())))
wenzelm@30645
   259
  handle ERROR msg =>
wenzelm@30645
   260
    cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos);
wenzelm@30645
   261
wenzelm@24579
   262
end;
wenzelm@24579
   263
wenzelm@24596
   264
end;
wenzelm@24579
   265