src/Pure/Isar/outer_lex.ML
author wenzelm
Thu Aug 07 13:45:05 2008 +0200 (2008-08-07 ago)
changeset 27769 ad50c38ef842
parent 27752 ea7d573e565f
child 27780 7d0910f662f7
permissions -rw-r--r--
improved position handling due to SymbolPos.T;
SymbolPos.scan_comment_body;
tuned;
wenzelm@5825
     1
(*  Title:      Pure/Isar/outer_lex.ML
wenzelm@5825
     2
    ID:         $Id$
wenzelm@5825
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@5825
     4
wenzelm@5825
     5
Outer lexical syntax for Isabelle/Isar.
wenzelm@5825
     6
*)
wenzelm@5825
     7
wenzelm@5825
     8
signature OUTER_LEX =
wenzelm@5825
     9
sig
wenzelm@5825
    10
  datatype token_kind =
wenzelm@23729
    11
    Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar | Nat |
wenzelm@23788
    12
    String | AltString | Verbatim | Space | Comment | Malformed | Error of string | Sync | EOF
aspinall@15143
    13
  eqtype token
wenzelm@5825
    14
  val str_of_kind: token_kind -> string
wenzelm@5825
    15
  val position_of: token -> Position.T
wenzelm@27752
    16
  val end_position_of: token -> Position.T
wenzelm@5825
    17
  val pos_of: token -> string
wenzelm@27733
    18
  val eof: token
wenzelm@27733
    19
  val is_eof: token -> bool
wenzelm@27733
    20
  val not_eof: token -> bool
wenzelm@27733
    21
  val not_sync: token -> bool
wenzelm@27733
    22
  val stopper: token Scan.stopper
wenzelm@23721
    23
  val kind_of: token -> token_kind
wenzelm@5825
    24
  val is_kind: token_kind -> token -> bool
wenzelm@7026
    25
  val keyword_with: (string -> bool) -> token -> bool
wenzelm@16029
    26
  val ident_with: (string -> bool) -> token -> bool
wenzelm@5825
    27
  val is_proper: token -> bool
wenzelm@9130
    28
  val is_semicolon: token -> bool
wenzelm@17069
    29
  val is_comment: token -> bool
wenzelm@8580
    30
  val is_begin_ignore: token -> bool
wenzelm@8580
    31
  val is_end_ignore: token -> bool
wenzelm@17069
    32
  val is_blank: token -> bool
wenzelm@8651
    33
  val is_newline: token -> bool
wenzelm@25642
    34
  val val_of: token -> string
wenzelm@27747
    35
  val source_of: token -> string
wenzelm@14991
    36
  val unparse: token -> string
wenzelm@23788
    37
  val text_of: token -> string * string
wenzelm@5876
    38
  val is_sid: string -> bool
wenzelm@27769
    39
  val !!! : string -> (SymbolPos.T list -> 'a) -> SymbolPos.T list -> 'a
wenzelm@27769
    40
  val scan_quoted: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
wenzelm@27769
    41
  val source_proper: (token, 'a) Source.source -> (token, (token, 'a) Source.source) Source.source
wenzelm@27769
    42
  val source: bool Option.option -> (unit -> Scan.lexicon * Scan.lexicon) ->
wenzelm@27769
    43
    Position.T -> (Symbol.symbol, 'a) Source.source -> (token,
wenzelm@27769
    44
      (SymbolPos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
wenzelm@5825
    45
end;
wenzelm@5825
    46
wenzelm@5825
    47
structure OuterLex: OUTER_LEX =
wenzelm@5825
    48
struct
wenzelm@5825
    49
wenzelm@5825
    50
(** tokens **)
wenzelm@5825
    51
wenzelm@5825
    52
(* datatype token *)
wenzelm@5825
    53
wenzelm@5825
    54
datatype token_kind =
wenzelm@23729
    55
  Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar | Nat |
wenzelm@23788
    56
  String | AltString | Verbatim | Space | Comment | Malformed | Error of string | Sync | EOF;
wenzelm@5825
    57
wenzelm@27769
    58
datatype token = Token of (string * Position.range) * (token_kind * string);
wenzelm@5825
    59
wenzelm@5825
    60
val str_of_kind =
wenzelm@7026
    61
 fn Command => "command"
wenzelm@7026
    62
  | Keyword => "keyword"
wenzelm@5825
    63
  | Ident => "identifier"
wenzelm@5825
    64
  | LongIdent => "long identifier"
wenzelm@5825
    65
  | SymIdent => "symbolic identifier"
wenzelm@5825
    66
  | Var => "schematic variable"
wenzelm@5825
    67
  | TypeIdent => "type variable"
wenzelm@5825
    68
  | TypeVar => "schematic type variable"
wenzelm@5825
    69
  | Nat => "number"
wenzelm@5825
    70
  | String => "string"
wenzelm@17164
    71
  | AltString => "back-quoted string"
wenzelm@5825
    72
  | Verbatim => "verbatim text"
wenzelm@7682
    73
  | Space => "white space"
wenzelm@7682
    74
  | Comment => "comment text"
wenzelm@23729
    75
  | Malformed => "malformed symbolic character"
wenzelm@23729
    76
  | Error _ => "bad input"
wenzelm@23788
    77
  | Sync => "sync marker"
wenzelm@5825
    78
  | EOF => "end-of-file";
wenzelm@5825
    79
wenzelm@5825
    80
wenzelm@27733
    81
(* position *)
wenzelm@5825
    82
wenzelm@27769
    83
fun position_of (Token ((_, (pos, _)), _)) = pos;
wenzelm@27769
    84
fun end_position_of (Token ((_, (_, pos)), _)) = pos;
wenzelm@27663
    85
wenzelm@5825
    86
val pos_of = Position.str_of o position_of;
wenzelm@5825
    87
wenzelm@5825
    88
wenzelm@27733
    89
(* control tokens *)
wenzelm@27733
    90
wenzelm@27769
    91
fun mk_eof pos = Token (("", (pos, Position.none)), (EOF, ""));
wenzelm@27733
    92
val eof = mk_eof Position.none;
wenzelm@27733
    93
wenzelm@27733
    94
fun is_eof (Token (_, (EOF, _))) = true
wenzelm@27733
    95
  | is_eof _ = false;
wenzelm@27733
    96
wenzelm@27733
    97
val not_eof = not o is_eof;
wenzelm@27733
    98
wenzelm@27733
    99
fun not_sync (Token (_, (Sync, _))) = false
wenzelm@27733
   100
  | not_sync _ = true;
wenzelm@27733
   101
wenzelm@27752
   102
val stopper =
wenzelm@27752
   103
  Scan.stopper (fn [] => eof | toks => mk_eof (end_position_of (List.last toks))) is_eof;
wenzelm@27733
   104
wenzelm@27733
   105
wenzelm@5825
   106
(* kind of token *)
wenzelm@5825
   107
wenzelm@23721
   108
fun kind_of (Token (_, (k, _))) = k;
wenzelm@5825
   109
fun is_kind k (Token (_, (k', _))) = k = k';
wenzelm@5825
   110
wenzelm@7026
   111
fun keyword_with pred (Token (_, (Keyword, x))) = pred x
wenzelm@7026
   112
  | keyword_with _ _ = false;
wenzelm@5825
   113
wenzelm@16029
   114
fun ident_with pred (Token (_, (Ident, x))) = pred x
wenzelm@16029
   115
  | ident_with _ _ = false;
wenzelm@16029
   116
wenzelm@7682
   117
fun is_proper (Token (_, (Space, _))) = false
wenzelm@7682
   118
  | is_proper (Token (_, (Comment, _))) = false
wenzelm@5825
   119
  | is_proper _ = true;
wenzelm@5825
   120
wenzelm@9195
   121
fun is_semicolon (Token (_, (Keyword, ";"))) = true
wenzelm@9130
   122
  | is_semicolon _ = false;
wenzelm@9130
   123
wenzelm@17069
   124
fun is_comment (Token (_, (Comment, _))) = true
wenzelm@17069
   125
  | is_comment _ = false;
wenzelm@17069
   126
wenzelm@8580
   127
fun is_begin_ignore (Token (_, (Comment, "<"))) = true
wenzelm@8580
   128
  | is_begin_ignore _ = false;
wenzelm@8580
   129
wenzelm@8580
   130
fun is_end_ignore (Token (_, (Comment, ">"))) = true
wenzelm@8580
   131
  | is_end_ignore _ = false;
wenzelm@8580
   132
wenzelm@8651
   133
wenzelm@17069
   134
(* blanks and newlines -- space tokens obey lines *)
wenzelm@8651
   135
wenzelm@23678
   136
fun is_blank (Token (_, (Space, x))) = not (String.isSuffix "\n" x)
wenzelm@17069
   137
  | is_blank _ = false;
wenzelm@17069
   138
wenzelm@23678
   139
fun is_newline (Token (_, (Space, x))) = String.isSuffix "\n" x
wenzelm@8651
   140
  | is_newline _ = false;
wenzelm@8651
   141
wenzelm@5825
   142
wenzelm@14991
   143
(* token content *)
wenzelm@9155
   144
wenzelm@25642
   145
fun val_of (Token (_, (_, x))) = x;
wenzelm@25642
   146
wenzelm@27769
   147
fun source_of (Token ((src, (pos, _)), _)) =
wenzelm@27769
   148
  YXML.string_of (XML.Elem (Markup.tokenN, Position.properties_of pos, [XML.Text src]));
wenzelm@27747
   149
wenzelm@27747
   150
wenzelm@27747
   151
(* unparse *)
wenzelm@27747
   152
wenzelm@18547
   153
fun escape q =
wenzelm@18547
   154
  implode o map (fn s => if s = q orelse s = "\\" then "\\" ^ s else s) o Symbol.explode;
wenzelm@18547
   155
wenzelm@14991
   156
fun unparse (Token (_, (kind, x))) =
wenzelm@14991
   157
  (case kind of
wenzelm@18547
   158
    String => x |> quote o escape "\""
wenzelm@18547
   159
  | AltString => x |> enclose "`" "`" o escape "`"
wenzelm@14991
   160
  | Verbatim => x |> enclose "{*" "*}"
wenzelm@14991
   161
  | Comment => x |> enclose "(*" "*)"
wenzelm@25642
   162
  | Malformed => Output.escape (translate_string Output.output x)
wenzelm@23729
   163
  | Sync => ""
wenzelm@23729
   164
  | EOF => ""
wenzelm@14991
   165
  | _ => x);
wenzelm@14991
   166
wenzelm@23788
   167
fun text_of tok =
wenzelm@23788
   168
  if is_semicolon tok then ("terminator", "")
wenzelm@23729
   169
  else
wenzelm@23788
   170
    let
wenzelm@23788
   171
      val k = str_of_kind (kind_of tok);
wenzelm@25642
   172
      val s = unparse tok
wenzelm@25642
   173
        handle ERROR _ => Symbol.separate_chars (val_of tok);
wenzelm@23788
   174
    in
wenzelm@23788
   175
      if s = "" then (k, "")
wenzelm@23788
   176
      else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ s, "")
wenzelm@23788
   177
      else (k, s)
wenzelm@23788
   178
    end;
wenzelm@23729
   179
wenzelm@5825
   180
wenzelm@5825
   181
wenzelm@5825
   182
(** scanners **)
wenzelm@5825
   183
wenzelm@27769
   184
open BasicSymbolPos;
wenzelm@5825
   185
wenzelm@27769
   186
fun !!! msg = SymbolPos.!!! ("Outer lexical error: " ^ msg);
wenzelm@5825
   187
wenzelm@27769
   188
fun change_prompt scan = Scan.prompt "# " scan;
wenzelm@5825
   189
wenzelm@5825
   190
wenzelm@5825
   191
(* scan symbolic idents *)
wenzelm@5825
   192
wenzelm@20664
   193
val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
wenzelm@5825
   194
wenzelm@8231
   195
val scan_symid =
wenzelm@27769
   196
  Scan.many1 (is_sym_char o symbol) ||
wenzelm@27769
   197
  Scan.one (Symbol.is_symbolic o symbol) >> single;
wenzelm@5825
   198
wenzelm@8231
   199
fun is_symid str =
wenzelm@8231
   200
  (case try Symbol.explode str of
skalberg@15531
   201
    SOME [s] => Symbol.is_symbolic s orelse is_sym_char s
skalberg@15531
   202
  | SOME ss => forall is_sym_char ss
wenzelm@8231
   203
  | _ => false);
wenzelm@8231
   204
wenzelm@20982
   205
fun is_sid "begin" = false
wenzelm@20982
   206
  | is_sid ":" = true
wenzelm@22873
   207
  | is_sid "::" = true
wenzelm@20982
   208
  | is_sid s = is_symid s orelse Syntax.is_identifier s;
wenzelm@5825
   209
wenzelm@5825
   210
wenzelm@5825
   211
(* scan strings *)
wenzelm@5825
   212
wenzelm@17164
   213
local
wenzelm@17164
   214
wenzelm@25579
   215
val char_code =
wenzelm@27769
   216
  Scan.one (Symbol.is_ascii_digit o symbol) --
wenzelm@27769
   217
  Scan.one (Symbol.is_ascii_digit o symbol) --
wenzelm@27769
   218
  Scan.one (Symbol.is_ascii_digit o symbol) :|--
wenzelm@27769
   219
  (fn (((a, pos), (b, _)), (c, _)) =>
wenzelm@25579
   220
    let val (n, _) = Library.read_int [a, b, c]
wenzelm@27769
   221
    in if n <= 255 then Scan.succeed [(chr n, pos)] else Scan.fail end);
wenzelm@25579
   222
wenzelm@17164
   223
fun scan_str q =
wenzelm@27769
   224
  $$$ "\\" |-- !!! "bad escape character in string" ($$$ q || $$$ "\\" || char_code) ||
wenzelm@27769
   225
  Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single;
wenzelm@5825
   226
wenzelm@17164
   227
fun scan_strs q =
wenzelm@27769
   228
  $$$ q |-- !!! "missing quote at end of string"
wenzelm@27769
   229
    (change_prompt (Scan.repeat (scan_str q) --| $$$ q)) >> flat;
wenzelm@17164
   230
wenzelm@17164
   231
in
wenzelm@17164
   232
wenzelm@17164
   233
val scan_string = scan_strs "\"";
wenzelm@17164
   234
val scan_alt_string = scan_strs "`";
wenzelm@17164
   235
wenzelm@27769
   236
val scan_quoted = Scan.trace (scan_string || scan_alt_string) >> #2;
wenzelm@27752
   237
wenzelm@17164
   238
end;
wenzelm@5825
   239
wenzelm@5825
   240
wenzelm@5825
   241
(* scan verbatim text *)
wenzelm@5825
   242
wenzelm@5825
   243
val scan_verb =
wenzelm@27769
   244
  $$$ "*" --| Scan.ahead (~$$$ "}") ||
wenzelm@27769
   245
  Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single;
wenzelm@5825
   246
wenzelm@5825
   247
val scan_verbatim =
wenzelm@27769
   248
  $$$ "{" |-- $$$ "*" |-- !!! "missing end of verbatim text"
wenzelm@27769
   249
    (change_prompt (Scan.repeat scan_verb --| $$$ "*" --| $$$ "}")) >> flat;
wenzelm@5825
   250
wenzelm@5825
   251
wenzelm@5825
   252
(* scan space *)
wenzelm@5825
   253
wenzelm@19305
   254
fun is_space s = Symbol.is_blank s andalso s <> "\n";
wenzelm@5825
   255
wenzelm@5825
   256
val scan_space =
wenzelm@27769
   257
  Scan.many1 (is_space o symbol) @@@ Scan.optional ($$$ "\n") [] ||
wenzelm@27769
   258
  Scan.many (is_space o symbol) @@@ $$$ "\n";
wenzelm@5825
   259
wenzelm@5825
   260
wenzelm@5825
   261
(* scan nested comments *)
wenzelm@5825
   262
wenzelm@5825
   263
val scan_cmt =
wenzelm@27769
   264
  Scan.depend (fn d => $$$ "(" @@@ $$$ "*" >> pair (d + 1)) ||
wenzelm@27769
   265
  Scan.depend (fn 0 => Scan.fail | d => $$$ "*" @@@ $$$ ")" >> pair (d - 1)) ||
wenzelm@27769
   266
  Scan.lift ($$$ "*" --| Scan.ahead (~$$$ ")")) ||
wenzelm@27769
   267
  Scan.lift (Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single);
wenzelm@5825
   268
wenzelm@5825
   269
val scan_comment =
wenzelm@27769
   270
  $$$ "(" |-- $$$ "*" |-- !!! "missing end of comment"
wenzelm@27769
   271
    (change_prompt (Scan.pass 0 (Scan.repeat scan_cmt >> flat) --| $$$ "*" --| $$$ ")"));
wenzelm@5825
   272
wenzelm@5825
   273
wenzelm@23678
   274
(* scan malformed symbols *)
wenzelm@23678
   275
wenzelm@23678
   276
val scan_malformed =
wenzelm@27769
   277
  $$$ Symbol.malformed |--
wenzelm@27769
   278
    change_prompt (Scan.many (Symbol.is_regular o symbol))
wenzelm@27769
   279
  --| Scan.option ($$$ Symbol.end_malformed);
wenzelm@27752
   280
wenzelm@27752
   281
wenzelm@27663
   282
wenzelm@27769
   283
(** token sources **)
wenzelm@5825
   284
wenzelm@27769
   285
fun source_proper src = src |> Source.filter is_proper;
wenzelm@5825
   286
wenzelm@23678
   287
local
wenzelm@23678
   288
wenzelm@27769
   289
fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2;
wenzelm@27769
   290
fun token (k, ss) = Token (SymbolPos.implode ss, (k, implode (map symbol ss)));
wenzelm@23678
   291
wenzelm@27769
   292
fun scan (lex1, lex2) = !!! "bad input"
wenzelm@27769
   293
  (scan_string >> pair String ||
wenzelm@27769
   294
    scan_alt_string >> pair AltString ||
wenzelm@27769
   295
    scan_verbatim >> pair Verbatim ||
wenzelm@27769
   296
    SymbolPos.scan_comment_body !!! >> pair Comment ||
wenzelm@27769
   297
    scan_space >> pair Space ||
wenzelm@27769
   298
    scan_malformed >> pair Malformed ||
wenzelm@27769
   299
    Scan.one (Symbol.is_sync o symbol) >> (fn s => (Sync, [s])) ||
wenzelm@27769
   300
    ((Scan.max token_leq
wenzelm@27769
   301
      (Scan.max token_leq
wenzelm@27769
   302
        (Scan.literal lex2 >> pair Command)
wenzelm@27769
   303
        (Scan.literal lex1 >> pair Keyword))
wenzelm@27769
   304
      (Syntax.scan_longid >> pair LongIdent ||
wenzelm@27769
   305
        Syntax.scan_id >> pair Ident ||
wenzelm@27769
   306
        Syntax.scan_var >> pair Var ||
wenzelm@27769
   307
        Syntax.scan_tid >> pair TypeIdent ||
wenzelm@27769
   308
        Syntax.scan_tvar >> pair TypeVar ||
wenzelm@27769
   309
        Syntax.scan_nat >> pair Nat ||
wenzelm@27769
   310
        scan_symid >> pair SymIdent)))) >> token;
wenzelm@27769
   311
wenzelm@27769
   312
fun recover msg =
wenzelm@27769
   313
  Scan.many ((Symbol.is_regular andf (not o Symbol.is_blank)) o symbol)
wenzelm@27769
   314
  >> (fn ss => [token (Error msg, ss)]);
wenzelm@23678
   315
wenzelm@23678
   316
in
wenzelm@5825
   317
wenzelm@5825
   318
fun source do_recover get_lex pos src =
wenzelm@27769
   319
  SymbolPos.source pos src
wenzelm@27769
   320
  |> Source.source SymbolPos.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
wenzelm@27769
   321
    (Option.map (rpair recover) do_recover);
wenzelm@23678
   322
wenzelm@23678
   323
end;
wenzelm@5825
   324
wenzelm@5825
   325
end;