src/Pure/Syntax/lexicon.ML
author wenzelm
Fri, 15 Aug 2008 15:51:00 +0200
changeset 27887 9f3fd48cf673
parent 27806 ece79c0597fe
child 28407 f9db1da584ac
permissions -rw-r--r--
token_kind: add Space, Comment; tokenize: now includes improper tokens, cf. is_proper; added report_token;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     1
(*  Title:      Pure/Syntax/lexicon.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     3
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
     5
Lexer for the inner Isabelle syntax (terms and types).
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     6
*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
signature LEXICON0 =
4247
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
     9
sig
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
  val is_identifier: string -> bool
14679
6ed90bd68eda added is_ascii_identifier;
wenzelm
parents: 13808
diff changeset
    11
  val is_ascii_identifier: string -> bool
20165
4de20306a88a export is_tid;
wenzelm
parents: 20096
diff changeset
    12
  val is_tid: string -> bool
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
    13
  val scan_id: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
    14
  val scan_longid: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
    15
  val scan_tid: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
    16
  val scan_nat: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
    17
  val scan_int: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
    18
  val scan_hex: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
    19
  val scan_bin: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
    20
  val scan_var: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
    21
  val scan_tvar: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
4247
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
    22
  val implode_xstr: string list -> string
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
    23
  val explode_xstr: string -> string list
20313
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
    24
  val read_indexname: string -> indexname
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
    25
  val read_var: string -> term
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
    26
  val read_variable: string -> indexname option
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    27
  val const: string -> term
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    28
  val free: string -> term
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    29
  val var: indexname -> term
5860
ed11c9890852 added read_nat;
wenzelm
parents: 5513
diff changeset
    30
  val read_nat: string -> int option
20313
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
    31
  val read_int: string -> int option
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24583
diff changeset
    32
  val read_xnum: string -> {radix: int, leading_zeros: int, value: int}
19002
2fbb3d809026 added fixedN, constN;
wenzelm
parents: 18375
diff changeset
    33
  val fixedN: string
2fbb3d809026 added fixedN, constN;
wenzelm
parents: 18375
diff changeset
    34
  val constN: string
4247
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
    35
end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
signature LEXICON =
4247
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
    38
sig
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    39
  include LEXICON0
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    40
  val is_xid: string -> bool
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
    41
  datatype token_kind =
27887
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
    42
    Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy |
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
    43
    NumSy | XNumSy | StrSy | Space | Comment | EOF
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
    44
  datatype token = Token of token_kind * string * Position.range
27806
ece79c0597fe pos_of_token: Position.T;
wenzelm
parents: 27800
diff changeset
    45
  val str_of_token: token -> string
ece79c0597fe pos_of_token: Position.T;
wenzelm
parents: 27800
diff changeset
    46
  val pos_of_token: token -> Position.T
27887
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
    47
  val is_proper: token -> bool
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
    48
  val mk_eof: Position.T -> token
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
    49
  val eof: token
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
    50
  val is_eof: token -> bool
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
    51
  val stopper: token Scan.stopper
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    52
  val idT: typ
3828
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
    53
  val longidT: typ
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    54
  val varT: typ
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    55
  val tidT: typ
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    56
  val tvarT: typ
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
    57
  val terminals: string list
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
    58
  val is_terminal: string -> bool
27887
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
    59
  val report_token: token -> unit
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    60
  val matching_tokens: token * token -> bool
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    61
  val valued_token: token -> bool
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
    62
  val predef_term: string -> token option
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
    63
  val tokenize: Scan.lexicon -> bool -> SymbolPos.T list -> token list
4247
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
    64
end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
14679
6ed90bd68eda added is_ascii_identifier;
wenzelm
parents: 13808
diff changeset
    66
structure Lexicon: LEXICON =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    69
(** is_identifier etc. **)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    70
16150
c33fe18456fa moved is_ident to General/symbol.ML;
wenzelm
parents: 15991
diff changeset
    71
val is_identifier = Symbol.is_ident o Symbol.explode;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    72
14679
6ed90bd68eda added is_ascii_identifier;
wenzelm
parents: 13808
diff changeset
    73
fun is_ascii_identifier s =
6ed90bd68eda added is_ascii_identifier;
wenzelm
parents: 13808
diff changeset
    74
  let val cs = Symbol.explode s
16150
c33fe18456fa moved is_ident to General/symbol.ML;
wenzelm
parents: 15991
diff changeset
    75
  in forall Symbol.is_ascii cs andalso Symbol.is_ident cs end;
14679
6ed90bd68eda added is_ascii_identifier;
wenzelm
parents: 13808
diff changeset
    76
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    77
fun is_xid s =
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
    78
  (case Symbol.explode s of
16150
c33fe18456fa moved is_ident to General/symbol.ML;
wenzelm
parents: 15991
diff changeset
    79
    "_" :: cs => Symbol.is_ident cs
c33fe18456fa moved is_ident to General/symbol.ML;
wenzelm
parents: 15991
diff changeset
    80
  | cs => Symbol.is_ident cs);
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    81
330
2fda15dd1e0f changed the way a grammar is generated to allow the new parser to work;
clasohm
parents: 237
diff changeset
    82
fun is_tid s =
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
    83
  (case Symbol.explode s of
16150
c33fe18456fa moved is_ident to General/symbol.ML;
wenzelm
parents: 15991
diff changeset
    84
    "'" :: cs => Symbol.is_ident cs
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    85
  | _ => false);
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    86
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
    89
(** basic scanners **)
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
    90
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
    91
open BasicSymbolPos;
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
    92
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
    93
fun !!! msg = SymbolPos.!!! ("Inner lexical error: " ^ msg);
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
    94
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
    95
val scan_id = Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol);
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
    96
val scan_longid = scan_id @@@ (Scan.repeat1 ($$$ "." @@@ scan_id) >> flat);
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
    97
val scan_tid = $$$ "'" @@@ scan_id;
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
    98
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
    99
val scan_nat = Scan.many1 (Symbol.is_digit o symbol);
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   100
val scan_int = $$$ "-" @@@ scan_nat || scan_nat;
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   101
val scan_hex = $$$ "0" @@@ $$$ "x" @@@ Scan.many1 (Symbol.is_ascii_hex o symbol);
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   102
val scan_bin = $$$ "0" @@@ $$$ "b" @@@ Scan.many1 (fn (s, _) => s = "0" orelse s = "1");
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   103
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   104
val scan_id_nat = scan_id @@@ Scan.optional ($$$ "." @@@ scan_nat) [];
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   105
val scan_var = $$$ "?" @@@ scan_id_nat;
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   106
val scan_tvar = $$$ "?" @@@ $$$ "'" @@@ scan_id_nat;
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   107
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   108
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   109
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   110
(** datatype token **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   112
datatype token_kind =
27887
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   113
  Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy |
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   114
  NumSy | XNumSy | StrSy | Space | Comment | EOF;
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   115
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   116
datatype token = Token of token_kind * string * Position.range;
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   117
27806
ece79c0597fe pos_of_token: Position.T;
wenzelm
parents: 27800
diff changeset
   118
fun str_of_token (Token (_, s, _)) = s;
ece79c0597fe pos_of_token: Position.T;
wenzelm
parents: 27800
diff changeset
   119
fun pos_of_token (Token (_, _, (pos, _))) = pos;
ece79c0597fe pos_of_token: Position.T;
wenzelm
parents: 27800
diff changeset
   120
27887
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   121
fun is_proper (Token (Space, _, _)) = false
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   122
  | is_proper (Token (Comment, _, _)) = false
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   123
  | is_proper _ = true;
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   124
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   125
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   126
(* stopper *)
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   127
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   128
fun mk_eof pos = Token (EOF, "", (pos, Position.none));
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   129
val eof = mk_eof Position.none;
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   130
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   131
fun is_eof (Token (EOF, _, _)) = true
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   132
  | is_eof _ = false;
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   133
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   134
val stopper = Scan.stopper (K eof) is_eof;
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   135
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   137
(* terminal arguments *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   139
val idT = Type ("id", []);
3828
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
   140
val longidT = Type ("longid", []);
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   141
val varT = Type ("var", []);
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   142
val tidT = Type ("tid", []);
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   143
val tvarT = Type ("tvar", []);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
11697
8dd899efbd35 added "num" token;
wenzelm
parents: 9326
diff changeset
   145
val terminals = ["id", "longid", "var", "tid", "tvar", "num", "xnum", "xstr"];
20664
ffbc5a57191a member (op =);
wenzelm
parents: 20313
diff changeset
   146
val is_terminal = member (op =) terminals;
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   147
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
27887
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   149
(* markup *)
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   150
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   151
val token_kind_markup =
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   152
 fn Literal     => Markup.literal
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   153
  | IdentSy     => Markup.ident
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   154
  | LongIdentSy => Markup.ident
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   155
  | VarSy       => Markup.var
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   156
  | TFreeSy     => Markup.tfree
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   157
  | TVarSy      => Markup.tvar
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   158
  | NumSy       => Markup.num
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   159
  | XNumSy      => Markup.xnum
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   160
  | StrSy       => Markup.xstr
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   161
  | Space       => Markup.none
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   162
  | Comment     => Markup.inner_comment
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   163
  | EOF         => Markup.none;
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   164
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   165
fun report_token (Token (kind, _, (pos, _))) =
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   166
  Position.report (token_kind_markup kind) pos;
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   167
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   168
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   169
(* matching_tokens *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   171
fun matching_tokens (Token (Literal, x, _), Token (Literal, y, _)) = x = y
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   172
  | matching_tokens (Token (k, _, _), Token (k', _, _)) = k = k';
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   175
(* valued_token *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   177
fun valued_token (Token (Literal, _, _)) = false
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   178
  | valued_token (Token (EOF, _, _)) = false
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   179
  | valued_token _ = true;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   182
(* predef_term *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   184
fun predef_term "id" = SOME (Token (IdentSy, "id", Position.no_range))
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   185
  | predef_term "longid" = SOME (Token (LongIdentSy, "longid", Position.no_range))
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   186
  | predef_term "var" = SOME (Token (VarSy, "var", Position.no_range))
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   187
  | predef_term "tid" = SOME (Token (TFreeSy, "tid", Position.no_range))
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   188
  | predef_term "tvar" = SOME (Token (TVarSy, "tvar", Position.no_range))
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   189
  | predef_term "num" = SOME (Token (NumSy, "num", Position.no_range))
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   190
  | predef_term "xnum" = SOME (Token (XNumSy, "xnum", Position.no_range))
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   191
  | predef_term "xstr" = SOME (Token (StrSy, "xstr", Position.no_range))
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15443
diff changeset
   192
  | predef_term _ = NONE;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   195
(* xstr tokens *)
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   196
14730
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   197
val scan_chr =
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   198
  $$$ "\\" |-- $$$ "'" ||
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   199
  Scan.one ((fn s => s <> "\\" andalso s <> "'" andalso Symbol.is_regular s) o symbol) >> single ||
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   200
  $$$ "'" --| Scan.ahead (~$$$ "'");
14730
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   201
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   202
val scan_str =
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   203
  $$$ "'" @@@ $$$ "'" @@@ !!! "missing end of string"
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   204
    ((Scan.repeat scan_chr >> flat) @@@ $$$ "'" @@@ $$$ "'");
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   205
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   206
val scan_str_body =
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   207
  $$$ "'" |-- $$$ "'" |-- !!! "missing end of string"
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   208
    ((Scan.repeat scan_chr >> flat) --| $$$ "'" --| $$$ "'");
14730
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   209
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   211
fun implode_xstr cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs));
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   212
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   213
fun explode_xstr str =
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   214
  (case Scan.read SymbolPos.stopper scan_str_body (SymbolPos.explode (str, Position.none)) of
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   215
    SOME cs => map symbol cs
5868
0022d0a913b5 tuned usage of read;
wenzelm
parents: 5860
diff changeset
   216
  | _ => error ("Inner lexical error: literal string expected at " ^ quote str));
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   217
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   218
27806
ece79c0597fe pos_of_token: Position.T;
wenzelm
parents: 27800
diff changeset
   219
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   220
(** tokenize **)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   221
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   222
fun token_leq (Token (_, s1, _), Token (_, s2, _)) = s1 <= s2;
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   223
fun token kind ss = Token (kind, SymbolPos.content ss, SymbolPos.range ss);
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   224
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   225
fun tokenize lex xids syms =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   226
  let
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   227
    val scan_xid =
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   228
      if xids then $$$ "_" @@@ scan_id || scan_id
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   229
      else scan_id;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   230
20096
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   231
    val scan_num = scan_hex || scan_bin || scan_int;
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   232
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   233
    val scan_val =
26007
3760d3ff4cce basic scanners: produce symbol list instead of imploded string;
wenzelm
parents: 24630
diff changeset
   234
      scan_tvar >> token TVarSy ||
3760d3ff4cce basic scanners: produce symbol list instead of imploded string;
wenzelm
parents: 24630
diff changeset
   235
      scan_var >> token VarSy ||
3760d3ff4cce basic scanners: produce symbol list instead of imploded string;
wenzelm
parents: 24630
diff changeset
   236
      scan_tid >> token TFreeSy ||
3760d3ff4cce basic scanners: produce symbol list instead of imploded string;
wenzelm
parents: 24630
diff changeset
   237
      scan_num >> token NumSy ||
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   238
      $$$ "#" @@@ scan_num >> token XNumSy ||
26007
3760d3ff4cce basic scanners: produce symbol list instead of imploded string;
wenzelm
parents: 24630
diff changeset
   239
      scan_longid >> token LongIdentSy ||
3760d3ff4cce basic scanners: produce symbol list instead of imploded string;
wenzelm
parents: 24630
diff changeset
   240
      scan_xid >> token IdentSy;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   241
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   242
    val scan_lit = Scan.literal lex >> token Literal;
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   243
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   244
    val scan_token =
27887
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   245
      SymbolPos.scan_comment !!! >> token Comment ||
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   246
      Scan.max token_leq scan_lit scan_val ||
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   247
      scan_str >> token StrSy ||
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   248
      Scan.many1 (Symbol.is_blank o symbol) >> token Space;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   249
  in
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   250
    (case Scan.error
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   251
        (Scan.finite SymbolPos.stopper (Scan.repeat scan_token)) syms of
27887
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   252
      (toks, []) => toks
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   253
    | (_, ss) => error ("Inner lexical error at: " ^ SymbolPos.content ss ^
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   254
        Position.str_of (#1 (SymbolPos.range ss))))
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   255
  end;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   256
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   257
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   258
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   259
(** scan variables **)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   260
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   261
(* scan_indexname *)
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   262
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   263
local
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   264
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   265
val scan_vname =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   266
  let
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   267
    fun nat n [] = n
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   268
      | nat n (c :: cs) = nat (n * 10 + (ord c - ord "0")) cs;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   269
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   270
    fun idxname cs ds = (implode (rev cs), nat 0 ds);
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   271
    fun chop_idx [] ds = idxname [] ds
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   272
      | chop_idx (cs as (_ :: "\\<^isub>" :: _)) ds = idxname cs ds
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   273
      | chop_idx (cs as (_ :: "\\<^isup>" :: _)) ds = idxname cs ds
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   274
      | chop_idx (c :: cs) ds =
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   275
          if Symbol.is_digit c then chop_idx cs (c :: ds)
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   276
          else idxname (c :: cs) ds;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   277
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   278
    val scan = (scan_id >> map symbol) --
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   279
      Scan.optional ($$$ "." |-- scan_nat >> (nat 0 o map symbol)) ~1;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   280
  in
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   281
    scan >>
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   282
      (fn (cs, ~1) => chop_idx (rev cs) []
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   283
        | (cs, i) => (implode cs, i))
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   284
  end;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   285
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   286
in
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   287
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   288
val scan_indexname = $$$ "'" |-- scan_vname >> (fn (x, i) => ("'" ^ x, i)) || scan_vname;
15443
07f78cc82a73 indexname function now parses type variables as well; changed input
berghofe
parents: 14981
diff changeset
   289
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   290
end;
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   291
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   292
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   293
(* indexname *)
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   294
20313
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   295
fun read_indexname s =
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   296
  (case Scan.read SymbolPos.stopper scan_indexname (SymbolPos.explode (s, Position.none)) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15443
diff changeset
   297
    SOME xi => xi
20313
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   298
  | _ => error ("Lexical error in variable name: " ^ quote s));
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   299
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   300
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   301
(* read_var *)
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   302
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   303
fun const c = Const (c, dummyT);
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   304
fun free x = Free (x, dummyT);
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   305
fun var xi = Var (xi, dummyT);
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   306
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   307
fun read_var str =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   308
  let
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   309
    val scan =
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   310
      $$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one SymbolPos.is_eof) >> var ||
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   311
      Scan.many (Symbol.is_regular o symbol) >> (free o implode o map symbol);
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   312
  in the (Scan.read SymbolPos.stopper scan (SymbolPos.explode (str, Position.none))) end;
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   313
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   314
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   315
(* read_variable *)
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   316
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   317
fun read_variable str =
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   318
  let val scan = $$$ "?" |-- scan_indexname || scan_indexname
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   319
  in Scan.read SymbolPos.stopper scan (SymbolPos.explode (str, Position.none)) end;
4587
6bce9ef27d7e added read_var;
wenzelm
parents: 4247
diff changeset
   320
6bce9ef27d7e added read_var;
wenzelm
parents: 4247
diff changeset
   321
19002
2fbb3d809026 added fixedN, constN;
wenzelm
parents: 18375
diff changeset
   322
(* specific identifiers *)
5260
1835a591d3a7 binding / skolem vars;
wenzelm
parents: 5112
diff changeset
   323
19002
2fbb3d809026 added fixedN, constN;
wenzelm
parents: 18375
diff changeset
   324
val constN = "\\<^const>";
2fbb3d809026 added fixedN, constN;
wenzelm
parents: 18375
diff changeset
   325
val fixedN = "\\<^fixed>";
2fbb3d809026 added fixedN, constN;
wenzelm
parents: 18375
diff changeset
   326
5260
1835a591d3a7 binding / skolem vars;
wenzelm
parents: 5112
diff changeset
   327
20313
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   328
(* read numbers *)
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   329
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   330
local
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   331
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   332
fun nat cs =
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   333
  Option.map (#1 o Library.read_int o map symbol)
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   334
    (Scan.read SymbolPos.stopper scan_nat cs);
5860
ed11c9890852 added read_nat;
wenzelm
parents: 5513
diff changeset
   335
20313
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   336
in
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   337
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   338
fun read_nat s = nat (SymbolPos.explode (s, Position.none));
20313
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   339
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   340
fun read_int s =
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   341
  (case SymbolPos.explode (s, Position.none) of
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   342
    ("-", _) :: cs => Option.map ~ (nat cs)
20313
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   343
  | cs => nat cs);
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   344
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   345
end;
5860
ed11c9890852 added read_nat;
wenzelm
parents: 5513
diff changeset
   346
ed11c9890852 added read_nat;
wenzelm
parents: 5513
diff changeset
   347
20096
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   348
(* read_xnum: hex/bin/decimal *)
9326
1625c1f172b3 added read_xnum;
wenzelm
parents: 9289
diff changeset
   349
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   350
local
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   351
20096
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   352
val ten = ord "0" + 10;
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   353
val a = ord "a";
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   354
val A = ord "A";
23802
cd09234405b6 sys_error;
wenzelm
parents: 23784
diff changeset
   355
val _ = a > A orelse sys_error "Bad ASCII";
20096
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   356
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   357
fun remap_hex c =
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   358
  let val x = ord c in
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   359
    if x >= a then chr (x - a + ten)
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   360
    else if x >= A then chr (x - A + ten)
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   361
    else c
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   362
  end;
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   363
21781
8314ebb5364d read_xnum: return leading_zeros, radix;
wenzelm
parents: 21774
diff changeset
   364
fun leading_zeros ["0"] = 0
8314ebb5364d read_xnum: return leading_zeros, radix;
wenzelm
parents: 21774
diff changeset
   365
  | leading_zeros ("0" :: cs) = 1 + leading_zeros cs
8314ebb5364d read_xnum: return leading_zeros, radix;
wenzelm
parents: 21774
diff changeset
   366
  | leading_zeros _ = 0;
8314ebb5364d read_xnum: return leading_zeros, radix;
wenzelm
parents: 21774
diff changeset
   367
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   368
in
15965
f422f8283491 Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents: 15570
diff changeset
   369
9326
1625c1f172b3 added read_xnum;
wenzelm
parents: 9289
diff changeset
   370
fun read_xnum str =
1625c1f172b3 added read_xnum;
wenzelm
parents: 9289
diff changeset
   371
  let
20096
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   372
    val (sign, radix, digs) =
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   373
      (case Symbol.explode (perhaps (try (unprefix "#")) str) of
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   374
        "0" :: "x" :: cs => (1, 16, map remap_hex cs)
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   375
      | "0" :: "b" :: cs => (1, 2, cs)
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   376
      | "-" :: cs => (~1, 10, cs)
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   377
      | cs => (1, 10, cs));
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24583
diff changeset
   378
    val value = sign * #1 (Library.read_radix_int radix digs);
21781
8314ebb5364d read_xnum: return leading_zeros, radix;
wenzelm
parents: 21774
diff changeset
   379
  in {radix = radix, leading_zeros = leading_zeros digs, value = value} end;
9326
1625c1f172b3 added read_xnum;
wenzelm
parents: 9289
diff changeset
   380
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   381
end;
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   382
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   383
end;