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