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