src/Pure/Syntax/lexicon.ML
author wenzelm
Tue Mar 22 15:32:47 2011 +0100 (2011-03-22)
changeset 42052 34f1d2d81284
parent 42048 afd11ca8e018
child 42053 006095137a81
permissions -rw-r--r--
statespace syntax: strip positions -- type constraints are unexpected here;
wenzelm@18
     1
(*  Title:      Pure/Syntax/lexicon.ML
wenzelm@18
     2
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
clasohm@0
     3
wenzelm@4703
     4
Lexer for the inner Isabelle syntax (terms and types).
wenzelm@18
     5
*)
clasohm@0
     6
clasohm@0
     7
signature LEXICON0 =
wenzelm@4247
     8
sig
clasohm@0
     9
  val is_identifier: string -> bool
wenzelm@14679
    10
  val is_ascii_identifier: string -> bool
wenzelm@20165
    11
  val is_tid: string -> bool
wenzelm@30573
    12
  val scan_id: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
wenzelm@30573
    13
  val scan_longid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
wenzelm@30573
    14
  val scan_tid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
wenzelm@30573
    15
  val scan_nat: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
wenzelm@30573
    16
  val scan_int: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
wenzelm@40290
    17
  val scan_float: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
wenzelm@30573
    18
  val scan_hex: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
wenzelm@30573
    19
  val scan_bin: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
wenzelm@30573
    20
  val scan_var: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
wenzelm@30573
    21
  val scan_tvar: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
wenzelm@4247
    22
  val implode_xstr: string list -> string
wenzelm@4247
    23
  val explode_xstr: string -> string list
wenzelm@20313
    24
  val read_indexname: string -> indexname
wenzelm@4703
    25
  val read_var: string -> term
wenzelm@15991
    26
  val read_variable: string -> indexname option
wenzelm@550
    27
  val const: string -> term
wenzelm@550
    28
  val free: string -> term
wenzelm@550
    29
  val var: indexname -> term
wenzelm@5860
    30
  val read_nat: string -> int option
wenzelm@20313
    31
  val read_int: string -> int option
wenzelm@24630
    32
  val read_xnum: string -> {radix: int, leading_zeros: int, value: int}
nipkow@28904
    33
  val read_float: string -> {mant: int, exp: int}
wenzelm@35428
    34
  val mark_class: string -> string val unmark_class: string -> string
wenzelm@35428
    35
  val mark_type: string -> string val unmark_type: string -> string
wenzelm@35428
    36
  val mark_const: string -> string val unmark_const: string -> string
wenzelm@35428
    37
  val mark_fixed: string -> string val unmark_fixed: string -> string
wenzelm@35428
    38
  val unmark:
wenzelm@35428
    39
   {case_class: string -> 'a,
wenzelm@35428
    40
    case_type: string -> 'a,
wenzelm@35428
    41
    case_const: string -> 'a,
wenzelm@35428
    42
    case_fixed: string -> 'a,
wenzelm@35428
    43
    case_default: string -> 'a} -> string -> 'a
wenzelm@35428
    44
  val is_marked: string -> bool
wenzelm@42048
    45
  val pretty_position: Position.T -> Pretty.T
wenzelm@42046
    46
  val encode_position: Position.T -> string
wenzelm@42046
    47
  val decode_position: string -> Position.T option
wenzelm@4247
    48
end;
clasohm@0
    49
clasohm@0
    50
signature LEXICON =
wenzelm@4247
    51
sig
wenzelm@18
    52
  include LEXICON0
wenzelm@18
    53
  val is_xid: string -> bool
wenzelm@27800
    54
  datatype token_kind =
wenzelm@27887
    55
    Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy |
nipkow@28904
    56
    NumSy | FloatSy | XNumSy | StrSy | Space | Comment | EOF
wenzelm@27800
    57
  datatype token = Token of token_kind * string * Position.range
wenzelm@27806
    58
  val str_of_token: token -> string
wenzelm@27806
    59
  val pos_of_token: token -> Position.T
wenzelm@27887
    60
  val is_proper: token -> bool
wenzelm@27800
    61
  val mk_eof: Position.T -> token
wenzelm@27800
    62
  val eof: token
wenzelm@27800
    63
  val is_eof: token -> bool
wenzelm@27800
    64
  val stopper: token Scan.stopper
wenzelm@550
    65
  val idT: typ
wenzelm@3828
    66
  val longidT: typ
wenzelm@550
    67
  val varT: typ
wenzelm@550
    68
  val tidT: typ
wenzelm@550
    69
  val tvarT: typ
wenzelm@237
    70
  val terminals: string list
wenzelm@237
    71
  val is_terminal: string -> bool
wenzelm@38237
    72
  val report_token: Proof.context -> token -> unit
wenzelm@39510
    73
  val reported_token_range: Proof.context -> token -> string
wenzelm@18
    74
  val matching_tokens: token * token -> bool
wenzelm@18
    75
  val valued_token: token -> bool
wenzelm@237
    76
  val predef_term: string -> token option
wenzelm@30573
    77
  val tokenize: Scan.lexicon -> bool -> Symbol_Pos.T list -> token list
wenzelm@4247
    78
end;
clasohm@0
    79
wenzelm@14679
    80
structure Lexicon: LEXICON =
clasohm@0
    81
struct
clasohm@0
    82
wenzelm@18
    83
(** is_identifier etc. **)
wenzelm@18
    84
wenzelm@16150
    85
val is_identifier = Symbol.is_ident o Symbol.explode;
wenzelm@18
    86
wenzelm@14679
    87
fun is_ascii_identifier s =
wenzelm@14679
    88
  let val cs = Symbol.explode s
wenzelm@16150
    89
  in forall Symbol.is_ascii cs andalso Symbol.is_ident cs end;
wenzelm@14679
    90
wenzelm@18
    91
fun is_xid s =
wenzelm@4703
    92
  (case Symbol.explode s of
wenzelm@16150
    93
    "_" :: cs => Symbol.is_ident cs
wenzelm@16150
    94
  | cs => Symbol.is_ident cs);
wenzelm@18
    95
clasohm@330
    96
fun is_tid s =
wenzelm@4703
    97
  (case Symbol.explode s of
wenzelm@16150
    98
    "'" :: cs => Symbol.is_ident cs
wenzelm@18
    99
  | _ => false);
wenzelm@18
   100
clasohm@0
   101
clasohm@0
   102
wenzelm@4703
   103
(** basic scanners **)
wenzelm@4703
   104
wenzelm@30573
   105
open Basic_Symbol_Pos;
wenzelm@27773
   106
wenzelm@30573
   107
fun !!! msg = Symbol_Pos.!!! ("Inner lexical error: " ^ msg);
wenzelm@27773
   108
wenzelm@40525
   109
val scan_id =
wenzelm@40525
   110
  Scan.one (Symbol.is_letter o Symbol_Pos.symbol) :::
wenzelm@40525
   111
  Scan.many (Symbol.is_letdig o Symbol_Pos.symbol);
wenzelm@40525
   112
wenzelm@27773
   113
val scan_longid = scan_id @@@ (Scan.repeat1 ($$$ "." @@@ scan_id) >> flat);
wenzelm@27773
   114
val scan_tid = $$$ "'" @@@ scan_id;
wenzelm@4703
   115
wenzelm@40525
   116
val scan_nat = Scan.many1 (Symbol.is_digit o Symbol_Pos.symbol);
wenzelm@27773
   117
val scan_int = $$$ "-" @@@ scan_nat || scan_nat;
nipkow@28904
   118
val scan_natdot = scan_nat @@@ $$$ "." @@@ scan_nat;
nipkow@28904
   119
val scan_float = $$$ "-" @@@ scan_natdot || scan_natdot;
wenzelm@40525
   120
val scan_hex = $$$ "0" @@@ $$$ "x" @@@ Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol);
wenzelm@27773
   121
val scan_bin = $$$ "0" @@@ $$$ "b" @@@ Scan.many1 (fn (s, _) => s = "0" orelse s = "1");
wenzelm@4703
   122
wenzelm@27773
   123
val scan_id_nat = scan_id @@@ Scan.optional ($$$ "." @@@ scan_nat) [];
wenzelm@27773
   124
val scan_var = $$$ "?" @@@ scan_id_nat;
wenzelm@27773
   125
val scan_tvar = $$$ "?" @@@ $$$ "'" @@@ scan_id_nat;
wenzelm@4703
   126
wenzelm@4703
   127
wenzelm@4703
   128
wenzelm@18
   129
(** datatype token **)
clasohm@0
   130
wenzelm@27800
   131
datatype token_kind =
wenzelm@27887
   132
  Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy |
nipkow@28904
   133
  NumSy | FloatSy | XNumSy | StrSy | Space | Comment | EOF;
wenzelm@27800
   134
wenzelm@27800
   135
datatype token = Token of token_kind * string * Position.range;
wenzelm@27800
   136
wenzelm@27806
   137
fun str_of_token (Token (_, s, _)) = s;
wenzelm@27806
   138
fun pos_of_token (Token (_, _, (pos, _))) = pos;
wenzelm@27806
   139
wenzelm@27887
   140
fun is_proper (Token (Space, _, _)) = false
wenzelm@27887
   141
  | is_proper (Token (Comment, _, _)) = false
wenzelm@27887
   142
  | is_proper _ = true;
wenzelm@27887
   143
wenzelm@27800
   144
wenzelm@27800
   145
(* stopper *)
wenzelm@27800
   146
wenzelm@27800
   147
fun mk_eof pos = Token (EOF, "", (pos, Position.none));
wenzelm@27800
   148
val eof = mk_eof Position.none;
wenzelm@27800
   149
wenzelm@27800
   150
fun is_eof (Token (EOF, _, _)) = true
wenzelm@27800
   151
  | is_eof _ = false;
wenzelm@27800
   152
wenzelm@27800
   153
val stopper = Scan.stopper (K eof) is_eof;
wenzelm@27800
   154
clasohm@0
   155
wenzelm@237
   156
(* terminal arguments *)
clasohm@0
   157
wenzelm@550
   158
val idT = Type ("id", []);
wenzelm@3828
   159
val longidT = Type ("longid", []);
wenzelm@550
   160
val varT = Type ("var", []);
wenzelm@550
   161
val tidT = Type ("tid", []);
wenzelm@550
   162
val tvarT = Type ("tvar", []);
clasohm@0
   163
wenzelm@29156
   164
val terminal_kinds =
wenzelm@29156
   165
 [("id", IdentSy),
wenzelm@29156
   166
  ("longid", LongIdentSy),
wenzelm@29156
   167
  ("var", VarSy),
wenzelm@29156
   168
  ("tid", TFreeSy),
wenzelm@29156
   169
  ("tvar", TVarSy),
wenzelm@29156
   170
  ("num", NumSy),
wenzelm@29156
   171
  ("float_token", FloatSy),
wenzelm@29156
   172
  ("xnum", XNumSy),
wenzelm@29156
   173
  ("xstr", StrSy)];
wenzelm@29156
   174
wenzelm@29156
   175
val terminals = map #1 terminal_kinds;
wenzelm@20664
   176
val is_terminal = member (op =) terminals;
wenzelm@237
   177
clasohm@0
   178
wenzelm@27887
   179
(* markup *)
wenzelm@27887
   180
wenzelm@27887
   181
val token_kind_markup =
wenzelm@27887
   182
 fn Literal     => Markup.literal
wenzelm@27887
   183
  | IdentSy     => Markup.ident
wenzelm@27887
   184
  | LongIdentSy => Markup.ident
wenzelm@27887
   185
  | VarSy       => Markup.var
wenzelm@27887
   186
  | TFreeSy     => Markup.tfree
wenzelm@27887
   187
  | TVarSy      => Markup.tvar
wenzelm@29318
   188
  | NumSy       => Markup.numeral
wenzelm@29318
   189
  | FloatSy     => Markup.numeral
wenzelm@29318
   190
  | XNumSy      => Markup.numeral
wenzelm@29318
   191
  | StrSy       => Markup.inner_string
wenzelm@38474
   192
  | Space       => Markup.empty
wenzelm@27887
   193
  | Comment     => Markup.inner_comment
wenzelm@38474
   194
  | EOF         => Markup.empty;
wenzelm@27887
   195
wenzelm@38237
   196
fun report_token ctxt (Token (kind, _, (pos, _))) =
wenzelm@39507
   197
  Context_Position.report ctxt pos (token_kind_markup kind);
wenzelm@27887
   198
wenzelm@39510
   199
fun reported_token_range ctxt tok =
wenzelm@39168
   200
  if is_proper tok
wenzelm@39510
   201
  then Context_Position.reported_text ctxt (pos_of_token tok) Markup.token_range ""
wenzelm@39510
   202
  else "";
wenzelm@39168
   203
wenzelm@27887
   204
wenzelm@18
   205
(* matching_tokens *)
clasohm@0
   206
wenzelm@27800
   207
fun matching_tokens (Token (Literal, x, _), Token (Literal, y, _)) = x = y
wenzelm@27800
   208
  | matching_tokens (Token (k, _, _), Token (k', _, _)) = k = k';
clasohm@0
   209
clasohm@0
   210
wenzelm@18
   211
(* valued_token *)
clasohm@0
   212
wenzelm@27800
   213
fun valued_token (Token (Literal, _, _)) = false
wenzelm@27800
   214
  | valued_token (Token (EOF, _, _)) = false
wenzelm@27800
   215
  | valued_token _ = true;
clasohm@0
   216
clasohm@0
   217
wenzelm@18
   218
(* predef_term *)
clasohm@0
   219
wenzelm@29156
   220
fun predef_term s =
wenzelm@29156
   221
  (case AList.lookup (op =) terminal_kinds s of
wenzelm@29156
   222
    SOME sy => SOME (Token (sy, s, Position.no_range))
wenzelm@29156
   223
  | NONE => NONE);
clasohm@0
   224
clasohm@0
   225
wenzelm@4703
   226
(* xstr tokens *)
wenzelm@18
   227
wenzelm@14730
   228
val scan_chr =
wenzelm@27773
   229
  $$$ "\\" |-- $$$ "'" ||
wenzelm@40525
   230
  Scan.one
wenzelm@40525
   231
    ((fn s => s <> "\\" andalso s <> "'" andalso Symbol.is_regular s) o
wenzelm@40525
   232
      Symbol_Pos.symbol) >> single ||
wenzelm@27773
   233
  $$$ "'" --| Scan.ahead (~$$$ "'");
wenzelm@14730
   234
wenzelm@14730
   235
val scan_str =
wenzelm@27800
   236
  $$$ "'" @@@ $$$ "'" @@@ !!! "missing end of string"
wenzelm@27800
   237
    ((Scan.repeat scan_chr >> flat) @@@ $$$ "'" @@@ $$$ "'");
wenzelm@27800
   238
wenzelm@27800
   239
val scan_str_body =
wenzelm@27773
   240
  $$$ "'" |-- $$$ "'" |-- !!! "missing end of string"
wenzelm@27773
   241
    ((Scan.repeat scan_chr >> flat) --| $$$ "'" --| $$$ "'");
wenzelm@14730
   242
clasohm@0
   243
wenzelm@4703
   244
fun implode_xstr cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs));
wenzelm@18
   245
wenzelm@4703
   246
fun explode_xstr str =
wenzelm@30573
   247
  (case Scan.read Symbol_Pos.stopper scan_str_body (Symbol_Pos.explode (str, Position.none)) of
wenzelm@40525
   248
    SOME cs => map Symbol_Pos.symbol cs
wenzelm@5868
   249
  | _ => error ("Inner lexical error: literal string expected at " ^ quote str));
wenzelm@18
   250
wenzelm@18
   251
wenzelm@27806
   252
wenzelm@18
   253
(** tokenize **)
wenzelm@18
   254
wenzelm@27800
   255
fun token_leq (Token (_, s1, _), Token (_, s2, _)) = s1 <= s2;
wenzelm@30573
   256
fun token kind ss = Token (kind, Symbol_Pos.content ss, Symbol_Pos.range ss);
wenzelm@27800
   257
wenzelm@27800
   258
fun tokenize lex xids syms =
wenzelm@18
   259
  let
wenzelm@18
   260
    val scan_xid =
wenzelm@27773
   261
      if xids then $$$ "_" @@@ scan_id || scan_id
wenzelm@18
   262
      else scan_id;
wenzelm@18
   263
wenzelm@20096
   264
    val scan_num = scan_hex || scan_bin || scan_int;
wenzelm@20096
   265
wenzelm@550
   266
    val scan_val =
wenzelm@26007
   267
      scan_tvar >> token TVarSy ||
wenzelm@26007
   268
      scan_var >> token VarSy ||
wenzelm@26007
   269
      scan_tid >> token TFreeSy ||
nipkow@28904
   270
      scan_float >> token FloatSy ||
wenzelm@26007
   271
      scan_num >> token NumSy ||
wenzelm@27773
   272
      $$$ "#" @@@ scan_num >> token XNumSy ||
wenzelm@26007
   273
      scan_longid >> token LongIdentSy ||
wenzelm@26007
   274
      scan_xid >> token IdentSy;
wenzelm@18
   275
wenzelm@27800
   276
    val scan_lit = Scan.literal lex >> token Literal;
wenzelm@550
   277
wenzelm@4703
   278
    val scan_token =
wenzelm@30573
   279
      Symbol_Pos.scan_comment !!! >> token Comment ||
wenzelm@27887
   280
      Scan.max token_leq scan_lit scan_val ||
wenzelm@27887
   281
      scan_str >> token StrSy ||
wenzelm@40525
   282
      Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol) >> token Space;
wenzelm@18
   283
  in
wenzelm@27773
   284
    (case Scan.error
wenzelm@30573
   285
        (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_token)) syms of
wenzelm@27887
   286
      (toks, []) => toks
wenzelm@30573
   287
    | (_, ss) => error ("Inner lexical error at: " ^ Symbol_Pos.content ss ^
wenzelm@30573
   288
        Position.str_of (#1 (Symbol_Pos.range ss))))
wenzelm@18
   289
  end;
wenzelm@18
   290
wenzelm@18
   291
wenzelm@18
   292
wenzelm@18
   293
(** scan variables **)
wenzelm@18
   294
wenzelm@15991
   295
(* scan_indexname *)
wenzelm@15991
   296
wenzelm@15991
   297
local
wenzelm@18
   298
wenzelm@27773
   299
val scan_vname =
wenzelm@18
   300
  let
wenzelm@15991
   301
    fun nat n [] = n
wenzelm@15991
   302
      | nat n (c :: cs) = nat (n * 10 + (ord c - ord "0")) cs;
wenzelm@18
   303
wenzelm@15991
   304
    fun idxname cs ds = (implode (rev cs), nat 0 ds);
wenzelm@15991
   305
    fun chop_idx [] ds = idxname [] ds
wenzelm@15991
   306
      | chop_idx (cs as (_ :: "\\<^isub>" :: _)) ds = idxname cs ds
wenzelm@15991
   307
      | chop_idx (cs as (_ :: "\\<^isup>" :: _)) ds = idxname cs ds
wenzelm@15991
   308
      | chop_idx (c :: cs) ds =
wenzelm@15991
   309
          if Symbol.is_digit c then chop_idx cs (c :: ds)
wenzelm@15991
   310
          else idxname (c :: cs) ds;
wenzelm@18
   311
wenzelm@40525
   312
    val scan = (scan_id >> map Symbol_Pos.symbol) --
wenzelm@40525
   313
      Scan.optional ($$$ "." |-- scan_nat >> (nat 0 o map Symbol_Pos.symbol)) ~1;
wenzelm@18
   314
  in
wenzelm@27773
   315
    scan >>
wenzelm@27773
   316
      (fn (cs, ~1) => chop_idx (rev cs) []
wenzelm@27773
   317
        | (cs, i) => (implode cs, i))
wenzelm@18
   318
  end;
wenzelm@18
   319
wenzelm@15991
   320
in
wenzelm@18
   321
wenzelm@27773
   322
val scan_indexname = $$$ "'" |-- scan_vname >> (fn (x, i) => ("'" ^ x, i)) || scan_vname;
berghofe@15443
   323
wenzelm@15991
   324
end;
wenzelm@15991
   325
wenzelm@15991
   326
wenzelm@15991
   327
(* indexname *)
wenzelm@15991
   328
wenzelm@20313
   329
fun read_indexname s =
wenzelm@30573
   330
  (case Scan.read Symbol_Pos.stopper scan_indexname (Symbol_Pos.explode (s, Position.none)) of
skalberg@15531
   331
    SOME xi => xi
wenzelm@20313
   332
  | _ => error ("Lexical error in variable name: " ^ quote s));
wenzelm@18
   333
wenzelm@18
   334
wenzelm@4703
   335
(* read_var *)
wenzelm@18
   336
wenzelm@550
   337
fun const c = Const (c, dummyT);
wenzelm@550
   338
fun free x = Free (x, dummyT);
wenzelm@550
   339
fun var xi = Var (xi, dummyT);
wenzelm@550
   340
wenzelm@4703
   341
fun read_var str =
wenzelm@18
   342
  let
wenzelm@18
   343
    val scan =
wenzelm@30573
   344
      $$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof) >> var ||
wenzelm@40525
   345
      Scan.many (Symbol.is_regular o Symbol_Pos.symbol) >> (free o implode o map Symbol_Pos.symbol);
wenzelm@30573
   346
  in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none))) end;
wenzelm@15991
   347
wenzelm@15991
   348
wenzelm@15991
   349
(* read_variable *)
wenzelm@15991
   350
wenzelm@15991
   351
fun read_variable str =
wenzelm@27773
   352
  let val scan = $$$ "?" |-- scan_indexname || scan_indexname
wenzelm@30573
   353
  in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none)) end;
wenzelm@4587
   354
wenzelm@4587
   355
wenzelm@35428
   356
(* logical entities *)
wenzelm@35428
   357
wenzelm@35428
   358
fun marker s = (prefix s, unprefix s);
wenzelm@35428
   359
wenzelm@35428
   360
val (mark_class, unmark_class) = marker "\\<^class>";
wenzelm@35428
   361
val (mark_type, unmark_type) = marker "\\<^type>";
wenzelm@35428
   362
val (mark_const, unmark_const) = marker "\\<^const>";
wenzelm@35428
   363
val (mark_fixed, unmark_fixed) = marker "\\<^fixed>";
wenzelm@5260
   364
wenzelm@35428
   365
fun unmark {case_class, case_type, case_const, case_fixed, case_default} s =
wenzelm@35428
   366
  (case try unmark_class s of
wenzelm@35428
   367
    SOME c => case_class c
wenzelm@35428
   368
  | NONE =>
wenzelm@35428
   369
      (case try unmark_type s of
wenzelm@35428
   370
        SOME c => case_type c
wenzelm@35428
   371
      | NONE =>
wenzelm@35428
   372
          (case try unmark_const s of
wenzelm@35428
   373
            SOME c => case_const c
wenzelm@35428
   374
          | NONE =>
wenzelm@35428
   375
              (case try unmark_fixed s of
wenzelm@35428
   376
                SOME c => case_fixed c
wenzelm@35428
   377
              | NONE => case_default s))));
wenzelm@35262
   378
wenzelm@35428
   379
val is_marked =
wenzelm@35428
   380
  unmark {case_class = K true, case_type = K true, case_const = K true,
wenzelm@35428
   381
    case_fixed = K true, case_default = K false};
wenzelm@19002
   382
wenzelm@5260
   383
wenzelm@20313
   384
(* read numbers *)
wenzelm@20313
   385
wenzelm@20313
   386
local
wenzelm@20313
   387
wenzelm@20313
   388
fun nat cs =
wenzelm@40525
   389
  Option.map (#1 o Library.read_int o map Symbol_Pos.symbol)
wenzelm@30573
   390
    (Scan.read Symbol_Pos.stopper scan_nat cs);
wenzelm@5860
   391
wenzelm@20313
   392
in
wenzelm@20313
   393
wenzelm@30573
   394
fun read_nat s = nat (Symbol_Pos.explode (s, Position.none));
wenzelm@20313
   395
wenzelm@20313
   396
fun read_int s =
wenzelm@30573
   397
  (case Symbol_Pos.explode (s, Position.none) of
wenzelm@27773
   398
    ("-", _) :: cs => Option.map ~ (nat cs)
wenzelm@20313
   399
  | cs => nat cs);
wenzelm@20313
   400
wenzelm@20313
   401
end;
wenzelm@5860
   402
wenzelm@5860
   403
wenzelm@20096
   404
(* read_xnum: hex/bin/decimal *)
wenzelm@9326
   405
wenzelm@15991
   406
local
wenzelm@15991
   407
wenzelm@20096
   408
val ten = ord "0" + 10;
wenzelm@20096
   409
val a = ord "a";
wenzelm@20096
   410
val A = ord "A";
wenzelm@35428
   411
val _ = a > A orelse raise Fail "Bad ASCII";
wenzelm@20096
   412
wenzelm@20096
   413
fun remap_hex c =
wenzelm@20096
   414
  let val x = ord c in
wenzelm@20096
   415
    if x >= a then chr (x - a + ten)
wenzelm@20096
   416
    else if x >= A then chr (x - A + ten)
wenzelm@20096
   417
    else c
wenzelm@20096
   418
  end;
wenzelm@15991
   419
wenzelm@21781
   420
fun leading_zeros ["0"] = 0
wenzelm@21781
   421
  | leading_zeros ("0" :: cs) = 1 + leading_zeros cs
wenzelm@21781
   422
  | leading_zeros _ = 0;
wenzelm@21781
   423
wenzelm@15991
   424
in
paulson@15965
   425
wenzelm@9326
   426
fun read_xnum str =
wenzelm@9326
   427
  let
wenzelm@20096
   428
    val (sign, radix, digs) =
wenzelm@20096
   429
      (case Symbol.explode (perhaps (try (unprefix "#")) str) of
wenzelm@20096
   430
        "0" :: "x" :: cs => (1, 16, map remap_hex cs)
wenzelm@20096
   431
      | "0" :: "b" :: cs => (1, 2, cs)
wenzelm@20096
   432
      | "-" :: cs => (~1, 10, cs)
wenzelm@20096
   433
      | cs => (1, 10, cs));
wenzelm@29156
   434
  in
wenzelm@29156
   435
   {radix = radix,
wenzelm@29156
   436
    leading_zeros = leading_zeros digs,
wenzelm@29156
   437
    value = sign * #1 (Library.read_radix_int radix digs)}
wenzelm@29156
   438
  end;
wenzelm@9326
   439
wenzelm@15991
   440
end;
wenzelm@15991
   441
nipkow@28904
   442
fun read_float str =
nipkow@28904
   443
  let
nipkow@28904
   444
    val (sign, cs) =
wenzelm@29156
   445
      (case Symbol.explode str of
wenzelm@29156
   446
        "-" :: cs => (~1, cs)
wenzelm@29156
   447
      | cs => (1, cs));
wenzelm@29156
   448
    val (intpart, fracpart) =
nipkow@28904
   449
      (case take_prefix Symbol.is_digit cs of
wenzelm@29156
   450
        (intpart, "." :: fracpart) => (intpart, fracpart)
wenzelm@29156
   451
      | _ => raise Fail "read_float");
wenzelm@29156
   452
  in
wenzelm@29156
   453
   {mant = sign * #1 (Library.read_int (intpart @ fracpart)),
wenzelm@29156
   454
    exp = length fracpart}
wenzelm@42046
   455
  end;
wenzelm@42046
   456
wenzelm@42046
   457
wenzelm@42046
   458
(* positions *)
wenzelm@42046
   459
wenzelm@42048
   460
val position_dummy = "<position>";
wenzelm@42048
   461
val position_text = XML.Text position_dummy;
wenzelm@42048
   462
wenzelm@42048
   463
fun pretty_position pos =
wenzelm@42048
   464
  Pretty.markup (Position.markup pos Markup.position) [Pretty.str position_dummy];
wenzelm@42048
   465
wenzelm@42046
   466
fun encode_position pos =
wenzelm@42048
   467
  YXML.string_of (XML.Elem (Position.markup pos Markup.position, [position_text]));
wenzelm@42046
   468
wenzelm@42046
   469
fun decode_position str =
wenzelm@42046
   470
  (case YXML.parse_body str handle Fail msg => error msg of
wenzelm@42048
   471
    [XML.Elem ((name, props), [arg])] =>
wenzelm@42048
   472
      if name = Markup.positionN andalso arg = position_text
wenzelm@42048
   473
      then SOME (Position.of_properties props)
wenzelm@42046
   474
      else NONE
wenzelm@42046
   475
  | _ => NONE);
nipkow@28904
   476
clasohm@0
   477
end;