src/Pure/ML/ml_lex.ML
author wenzelm
Sat, 09 Aug 2008 22:43:59 +0200
changeset 27817 78cae5cca09e
parent 27799 52f07d5292cd
child 29606 fedb8be05f24
permissions -rw-r--r--
renamed ML_Lex.val_of to content_of;
wenzelm@24579
     1
(*  Title:      Pure/ML/ml_lex.ML
wenzelm@24579
     2
    ID:         $Id$
wenzelm@24579
     3
    Author:     Makarius
wenzelm@24579
     4
wenzelm@24579
     5
Lexical syntax for SML.
wenzelm@24579
     6
*)
wenzelm@24579
     7
wenzelm@24579
     8
signature ML_LEX =
wenzelm@24579
     9
sig
wenzelm@24579
    10
  datatype token_kind =
wenzelm@24596
    11
    Keyword | Ident | LongIdent | TypeVar | Word | Int | Real | Char | String |
wenzelm@24579
    12
    Space | Comment | Error of string | EOF
wenzelm@24579
    13
  eqtype token
wenzelm@27732
    14
  val stopper: token Scan.stopper
wenzelm@24596
    15
  val is_regular: token -> bool
wenzelm@24596
    16
  val is_improper: token -> bool
wenzelm@24596
    17
  val pos_of: token -> string
wenzelm@24579
    18
  val kind_of: token -> token_kind
wenzelm@27817
    19
  val content_of: token -> string
wenzelm@24579
    20
  val keywords: string list
wenzelm@24596
    21
  val source: (Symbol.symbol, 'a) Source.source ->
wenzelm@27772
    22
    (token, (SymbolPos.T, Position.T * (Symbol.symbol, 'a) Source.source)
wenzelm@27772
    23
      Source.source) Source.source
wenzelm@24579
    24
end;
wenzelm@24579
    25
wenzelm@24579
    26
structure ML_Lex: ML_LEX =
wenzelm@24579
    27
struct
wenzelm@24579
    28
wenzelm@24579
    29
(** tokens **)
wenzelm@24579
    30
wenzelm@24579
    31
(* datatype token *)
wenzelm@24579
    32
wenzelm@24579
    33
datatype token_kind =
wenzelm@24596
    34
  Keyword | Ident | LongIdent | TypeVar | Word | Int | Real | Char | String |
wenzelm@24579
    35
  Space | Comment | Error of string | EOF;
wenzelm@24579
    36
wenzelm@27772
    37
datatype token = Token of Position.range * (token_kind * string);
wenzelm@27772
    38
wenzelm@27772
    39
wenzelm@27772
    40
(* position *)
wenzelm@27772
    41
wenzelm@27772
    42
fun position_of (Token ((pos, _), _)) = pos;
wenzelm@27772
    43
fun end_position_of (Token ((_, pos), _)) = pos;
wenzelm@27772
    44
wenzelm@27772
    45
val pos_of = Position.str_of o position_of;
wenzelm@24579
    46
wenzelm@24579
    47
wenzelm@24596
    48
(* control tokens *)
wenzelm@24579
    49
wenzelm@27772
    50
fun mk_eof pos = Token ((pos, Position.none), (EOF, ""));
wenzelm@27772
    51
val eof = mk_eof Position.none;
wenzelm@24579
    52
wenzelm@24579
    53
fun is_eof (Token (_, (EOF, _))) = true
wenzelm@24579
    54
  | is_eof _ = false;
wenzelm@24579
    55
wenzelm@27772
    56
val stopper =
wenzelm@27772
    57
  Scan.stopper (fn [] => eof | toks => mk_eof (end_position_of (List.last toks))) is_eof;
wenzelm@24579
    58
wenzelm@24579
    59
wenzelm@27772
    60
(* token content *)
wenzelm@27772
    61
wenzelm@27817
    62
fun content_of (Token (_, (_, x))) = x;
wenzelm@27817
    63
fun token_leq (tok, tok') = content_of tok <= content_of tok';
wenzelm@27772
    64
wenzelm@27772
    65
fun kind_of (Token (_, (k, _))) = k;
wenzelm@27772
    66
wenzelm@24596
    67
fun is_regular (Token (_, (Error _, _))) = false
wenzelm@24596
    68
  | is_regular (Token (_, (EOF, _))) = false
wenzelm@24596
    69
  | is_regular _ = true;
wenzelm@24596
    70
wenzelm@24596
    71
fun is_improper (Token (_, (Space, _))) = true
wenzelm@24596
    72
  | is_improper (Token (_, (Comment, _))) = true
wenzelm@24596
    73
  | is_improper _ = false;
wenzelm@24596
    74
wenzelm@24596
    75
wenzelm@24579
    76
wenzelm@24579
    77
(** scanners **)
wenzelm@24579
    78
wenzelm@27772
    79
open BasicSymbolPos;
wenzelm@24579
    80
wenzelm@27772
    81
fun !!! msg = SymbolPos.!!! ("SML lexical error: " ^ msg);
wenzelm@24579
    82
wenzelm@24579
    83
wenzelm@27772
    84
(* blanks *)
wenzelm@24579
    85
wenzelm@27772
    86
val scan_blank = Scan.one (Symbol.is_ascii_blank o symbol);
wenzelm@27772
    87
val scan_blanks1 = Scan.repeat1 scan_blank;
wenzelm@24579
    88
wenzelm@24579
    89
wenzelm@24579
    90
(* keywords *)
wenzelm@24579
    91
wenzelm@24579
    92
val keywords = ["#", "(", ")", ",", "->", "...", ":", ":>", ";", "=",
wenzelm@24579
    93
  "=>", "[", "]", "_", "{", "|", "}", "abstype", "and", "andalso", "as",
wenzelm@24579
    94
  "case", "datatype", "do", "else", "end", "eqtype", "exception", "fn",
wenzelm@24579
    95
  "fun", "functor", "handle", "if", "in", "include", "infix", "infixr",
wenzelm@24579
    96
  "let", "local", "nonfix", "of", "op", "open", "orelse", "raise", "rec",
wenzelm@24579
    97
  "sharing", "sig", "signature", "struct", "structure", "then", "type",
wenzelm@24579
    98
  "val", "where", "while", "with", "withtype"];
wenzelm@24579
    99
wenzelm@27772
   100
val lex = Scan.make_lexicon (map explode keywords);
wenzelm@27772
   101
fun scan_keyword x = Scan.literal lex x;
wenzelm@24579
   102
wenzelm@24579
   103
wenzelm@24579
   104
(* identifiers *)
wenzelm@24579
   105
wenzelm@24596
   106
local
wenzelm@24596
   107
wenzelm@24579
   108
val scan_letdigs =
wenzelm@27772
   109
  Scan.many ((Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf Symbol.is_ascii_quasi) o symbol);
wenzelm@24579
   110
wenzelm@27772
   111
val scan_alphanumeric = Scan.one (Symbol.is_ascii_letter o symbol) -- scan_letdigs >> op ::;
wenzelm@24579
   112
wenzelm@27772
   113
val scan_symbolic = Scan.many1 (member (op =) (explode "!#$%&*+-/:<=>?@\\^`|~") o symbol);
wenzelm@24579
   114
wenzelm@24596
   115
in
wenzelm@24596
   116
wenzelm@24579
   117
val scan_ident = scan_alphanumeric || scan_symbolic;
wenzelm@24579
   118
wenzelm@24579
   119
val scan_longident =
wenzelm@27772
   120
  (Scan.repeat1 (scan_alphanumeric @@@ $$$ ".") >> flat) @@@ (scan_ident || $$$ "=");
wenzelm@24579
   121
wenzelm@27772
   122
val scan_typevar = $$$ "'" @@@ scan_letdigs;
wenzelm@24579
   123
wenzelm@24596
   124
end;
wenzelm@24579
   125
wenzelm@24579
   126
wenzelm@24579
   127
(* numerals *)
wenzelm@24579
   128
wenzelm@24596
   129
local
wenzelm@24596
   130
wenzelm@27772
   131
val scan_dec = Scan.many1 (Symbol.is_ascii_digit o symbol);
wenzelm@27772
   132
val scan_hex = Scan.many1 (Symbol.is_ascii_hex o symbol);
wenzelm@27772
   133
val scan_sign = Scan.optional ($$$ "~") [];
wenzelm@27772
   134
val scan_decint = scan_sign @@@ scan_dec;
wenzelm@24579
   135
wenzelm@24596
   136
in
wenzelm@24596
   137
wenzelm@27772
   138
val scan_word =
wenzelm@27772
   139
  $$$ "0" @@@ $$$ "w" @@@ $$$ "x" @@@ scan_hex ||
wenzelm@27772
   140
  $$$ "0" @@@ $$$ "w" @@@ scan_dec;
wenzelm@24579
   141
wenzelm@27772
   142
val scan_int = scan_sign @@@ ($$$ "0" @@@ $$$ "x" @@@ scan_hex || scan_dec);
wenzelm@24579
   143
wenzelm@27772
   144
val scan_exp = ($$$ "E" || $$$ "e") @@@ scan_decint;
wenzelm@24579
   145
wenzelm@24579
   146
val scan_real =
wenzelm@27772
   147
  scan_decint @@@ $$$ "." @@@ scan_dec @@@ Scan.optional scan_exp [] ||
wenzelm@27772
   148
  scan_decint @@@ scan_exp;
wenzelm@24579
   149
wenzelm@24596
   150
end;
wenzelm@24596
   151
wenzelm@24579
   152
wenzelm@24579
   153
(* chars and strings *)
wenzelm@24579
   154
wenzelm@24596
   155
local
wenzelm@24596
   156
wenzelm@24596
   157
val scan_escape =
wenzelm@27772
   158
  Scan.one (member (op =) (explode "\"\\abtnvfr") o symbol) >> single ||
wenzelm@27772
   159
  $$$ "^" @@@ (Scan.one (fn (s, _) => ord "@" <= ord s andalso ord s <= ord "_") >> single) ||
wenzelm@27772
   160
  Scan.one (Symbol.is_ascii_digit o symbol) --
wenzelm@27772
   161
    Scan.one (Symbol.is_ascii_digit o symbol) --
wenzelm@27772
   162
    Scan.one (Symbol.is_ascii_digit o symbol) >> (fn ((a, b), c) => [a, b, c]);
wenzelm@24596
   163
wenzelm@24596
   164
val scan_str =
wenzelm@27772
   165
  Scan.one (fn (s, _) => Symbol.is_printable s andalso s <> "\"" andalso s <> "\\") >> single ||
wenzelm@27772
   166
  $$$ "\\" @@@ !!! "bad escape character in string" scan_escape;
wenzelm@24596
   167
wenzelm@27772
   168
val scan_gap = $$$ "\\" @@@ scan_blanks1 @@@ $$$ "\\";
wenzelm@27772
   169
val scan_gaps = Scan.repeat scan_gap >> flat;
wenzelm@24579
   170
wenzelm@24596
   171
in
wenzelm@24579
   172
wenzelm@24579
   173
val scan_char =
wenzelm@27772
   174
  $$$ "#" @@@ $$$ "\"" @@@ scan_gaps @@@ scan_str @@@ scan_gaps @@@ $$$ "\"";
wenzelm@24579
   175
wenzelm@24579
   176
val scan_string =
wenzelm@27772
   177
  $$$ "\"" @@@ !!! "missing quote at end of string"
wenzelm@27772
   178
    ((Scan.repeat (scan_gap || scan_str) >> flat) @@@ $$$ "\"");
wenzelm@24596
   179
wenzelm@24596
   180
end;
wenzelm@24579
   181
wenzelm@24579
   182
wenzelm@24596
   183
(* token source *)
wenzelm@24579
   184
wenzelm@24579
   185
local
wenzelm@24579
   186
wenzelm@27799
   187
fun token k ss = Token (SymbolPos.range ss, (k, SymbolPos.implode ss));
wenzelm@24579
   188
wenzelm@27772
   189
val scan = !!! "bad input"
wenzelm@27772
   190
 (scan_char >> token Char ||
wenzelm@27772
   191
  scan_string >> token String ||
wenzelm@27772
   192
  scan_blanks1 >> token Space ||
wenzelm@27772
   193
  SymbolPos.scan_comment !!! >> token Comment ||
wenzelm@27772
   194
  Scan.max token_leq
wenzelm@27772
   195
   (scan_keyword >> token Keyword)
wenzelm@27772
   196
   (scan_word >> token Word ||
wenzelm@27772
   197
    scan_real >> token Real ||
wenzelm@27772
   198
    scan_int >> token Int ||
wenzelm@27772
   199
    scan_longident >> token LongIdent ||
wenzelm@27772
   200
    scan_ident >> token Ident ||
wenzelm@27772
   201
    scan_typevar >> token TypeVar));
wenzelm@27772
   202
wenzelm@27772
   203
fun recover msg =
wenzelm@27772
   204
  Scan.many (((not o Symbol.is_blank) andf Symbol.is_regular) o symbol)
wenzelm@27772
   205
  >> (fn cs => [token (Error msg) cs]);
wenzelm@24579
   206
wenzelm@24579
   207
in
wenzelm@24579
   208
wenzelm@24596
   209
fun source src =
wenzelm@27772
   210
  SymbolPos.source (Position.line 1) src
wenzelm@27772
   211
  |> Source.source SymbolPos.stopper (Scan.bulk scan) (SOME (false, recover));
wenzelm@24579
   212
wenzelm@24579
   213
end;
wenzelm@24579
   214
wenzelm@24596
   215
end;
wenzelm@24579
   216