src/Pure/Syntax/lexicon.ML
author wenzelm
Tue, 11 Jul 2006 14:21:08 +0200
changeset 20096 7058714024b3
parent 20091 edc96f85e069
child 20165 4de20306a88a
permissions -rw-r--r--
uniform treatment of num/xnum; read_xnum: proper handling of bin/hex;
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
4247
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
    12
  val implode_xstr: string list -> string
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
    13
  val explode_xstr: string -> string list
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
    14
  val scan_id: string list -> string * string list
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
    15
  val scan_longid: string list -> string * string list
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
    16
  val scan_var: string list -> string * string list
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
    17
  val scan_tid: string list -> string * string list
4902
8fbccead3695 added scan_tvar;
wenzelm
parents: 4703
diff changeset
    18
  val scan_tvar: string list -> string * string list
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
    19
  val scan_nat: string list -> string * string list
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
    20
  val scan_int: string list -> string * string list
20067
26bac504ef90 hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents: 19918
diff changeset
    21
  val scan_hex: string list -> string * string list
26bac504ef90 hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents: 19918
diff changeset
    22
  val scan_bin: string list -> string * string list
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    23
  val string_of_vname: indexname -> string
2583
690835a06cf2 added string_of_vname' (treats neg. index as free);
wenzelm
parents: 2363
diff changeset
    24
  val string_of_vname': indexname -> string
15443
07f78cc82a73 indexname function now parses type variables as well; changed input
berghofe
parents: 14981
diff changeset
    25
  val indexname: string -> indexname
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
    26
  val read_var: string -> term
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
    27
  val read_variable: string -> indexname option
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    28
  val const: string -> term
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    29
  val free: string -> term
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    30
  val var: indexname -> term
5860
ed11c9890852 added read_nat;
wenzelm
parents: 5513
diff changeset
    31
  val read_nat: string -> int option
15965
f422f8283491 Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents: 15570
diff changeset
    32
  val read_xnum: string -> IntInf.int
7784
228283fa5de4 read_idents;
wenzelm
parents: 7472
diff changeset
    33
  val read_idents: string -> string list
19002
2fbb3d809026 added fixedN, constN;
wenzelm
parents: 18375
diff changeset
    34
  val fixedN: string
2fbb3d809026 added fixedN, constN;
wenzelm
parents: 18375
diff changeset
    35
  val constN: string
4247
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
    36
end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
signature LEXICON =
4247
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
    39
sig
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    40
  include LEXICON0
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    41
  val is_xid: string -> bool
330
2fda15dd1e0f changed the way a grammar is generated to allow the new parser to work;
clasohm
parents: 237
diff changeset
    42
  val is_tid: string -> bool
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    43
  datatype token =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    44
    Token of string |
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    45
    IdentSy of string |
3828
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
    46
    LongIdentSy of string |
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    47
    VarSy of string |
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    48
    TFreeSy of string |
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    49
    TVarSy of string |
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    50
    NumSy of string |
11697
8dd899efbd35 added "num" token;
wenzelm
parents: 9326
diff changeset
    51
    XNumSy of string |
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    52
    StrSy of string |
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
    53
    EndToken
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    54
  val idT: typ
3828
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
    55
  val longidT: typ
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    56
  val varT: typ
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    57
  val tidT: typ
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    58
  val tvarT: typ
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
    59
  val terminals: string list
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
    60
  val is_terminal: string -> bool
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    61
  val str_of_token: token -> string
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    62
  val display_token: token -> string
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    63
  val matching_tokens: token * token -> bool
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    64
  val valued_token: token -> bool
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
    65
  val predef_term: string -> token option
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
    66
  val tokenize: Scan.lexicon -> bool -> string list -> token list
4247
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
    67
end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
14679
6ed90bd68eda added is_ascii_identifier;
wenzelm
parents: 13808
diff changeset
    69
structure Lexicon: LEXICON =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
4247
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
    72
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    73
(** is_identifier etc. **)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    74
16150
c33fe18456fa moved is_ident to General/symbol.ML;
wenzelm
parents: 15991
diff changeset
    75
val is_identifier = Symbol.is_ident o Symbol.explode;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    76
14679
6ed90bd68eda added is_ascii_identifier;
wenzelm
parents: 13808
diff changeset
    77
fun is_ascii_identifier s =
6ed90bd68eda added is_ascii_identifier;
wenzelm
parents: 13808
diff changeset
    78
  let val cs = Symbol.explode s
16150
c33fe18456fa moved is_ident to General/symbol.ML;
wenzelm
parents: 15991
diff changeset
    79
  in forall Symbol.is_ascii cs andalso Symbol.is_ident cs end;
14679
6ed90bd68eda added is_ascii_identifier;
wenzelm
parents: 13808
diff changeset
    80
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    81
fun is_xid s =
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
    82
  (case Symbol.explode s of
16150
c33fe18456fa moved is_ident to General/symbol.ML;
wenzelm
parents: 15991
diff changeset
    83
    "_" :: cs => Symbol.is_ident cs
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
330
2fda15dd1e0f changed the way a grammar is generated to allow the new parser to work;
clasohm
parents: 237
diff changeset
    86
fun is_tid s =
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
    87
  (case Symbol.explode s of
16150
c33fe18456fa moved is_ident to General/symbol.ML;
wenzelm
parents: 15991
diff changeset
    88
    "'" :: cs => Symbol.is_ident cs
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    89
  | _ => false);
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    90
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
    93
(** basic scanners **)
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
    94
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
    95
val scan_letter_letdigs = Scan.one Symbol.is_letter -- Scan.any Symbol.is_letdig >> op ::;
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
    96
val scan_digits1 = Scan.any1 Symbol.is_digit;
20067
26bac504ef90 hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents: 19918
diff changeset
    97
val scan_hex1 = Scan.any1 (Symbol.is_digit orf Symbol.is_hex_letter);
26bac504ef90 hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents: 19918
diff changeset
    98
val scan_bin1 = Scan.any1 (fn s => s = "0" orelse s = "1");
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
    99
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   100
val scan_id = scan_letter_letdigs >> implode;
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   101
val scan_longid = scan_id ^^ (Scan.repeat1 ($$ "." ^^ scan_id) >> implode);
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   102
val scan_tid = $$ "'" ^^ scan_id;
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   103
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   104
val scan_nat = scan_digits1 >> implode;
5513
3896c7894a57 Unary minus is now #- and not #~
paulson
parents: 5286
diff changeset
   105
val scan_int = $$ "-" ^^ scan_nat || scan_nat;
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   106
20091
wenzelm
parents: 20067
diff changeset
   107
val scan_hex = $$ "0" ^^ $$ "x" ^^ (scan_hex1 >> implode);
wenzelm
parents: 20067
diff changeset
   108
val scan_bin = $$ "0" ^^ $$ "b" ^^ (scan_bin1 >> implode);
20067
26bac504ef90 hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents: 19918
diff changeset
   109
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   110
val scan_id_nat = scan_id ^^ Scan.optional ($$ "." ^^ scan_nat) "";
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   111
val scan_var = $$ "?" ^^ scan_id_nat;
4902
8fbccead3695 added scan_tvar;
wenzelm
parents: 4703
diff changeset
   112
val scan_tvar = $$ "?" ^^ $$ "'" ^^ scan_id_nat;
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   113
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   114
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   115
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   116
(** string_of_vname **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
14783
e7f7ed4c06f2 string_of_vname moved to term.ML;
wenzelm
parents: 14737
diff changeset
   118
val string_of_vname = Term.string_of_vname;
e7f7ed4c06f2 string_of_vname moved to term.ML;
wenzelm
parents: 14737
diff changeset
   119
val string_of_vname' = Term.string_of_vname';
2583
690835a06cf2 added string_of_vname' (treats neg. index as free);
wenzelm
parents: 2363
diff changeset
   120
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   121
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   123
(** datatype token **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   125
datatype token =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   126
  Token of string |
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   127
  IdentSy of string |
3828
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
   128
  LongIdentSy of string |
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   129
  VarSy of string |
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   130
  TFreeSy of string |
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   131
  TVarSy of string |
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   132
  NumSy of string |
11697
8dd899efbd35 added "num" token;
wenzelm
parents: 9326
diff changeset
   133
  XNumSy of string |
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   134
  StrSy of string |
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   135
  EndToken;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   138
(* terminal arguments *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   140
val idT = Type ("id", []);
3828
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
   141
val longidT = Type ("longid", []);
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   142
val varT = Type ("var", []);
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   143
val tidT = Type ("tid", []);
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   144
val tvarT = Type ("tvar", []);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
11697
8dd899efbd35 added "num" token;
wenzelm
parents: 9326
diff changeset
   146
val terminals = ["id", "longid", "var", "tid", "tvar", "num", "xnum", "xstr"];
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   147
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   148
fun is_terminal s = s mem terminals;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   149
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   151
(* str_of_token *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   153
fun str_of_token (Token s) = s
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   154
  | str_of_token (IdentSy s) = s
3828
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
   155
  | str_of_token (LongIdentSy s) = s
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   156
  | str_of_token (VarSy s) = s
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   157
  | str_of_token (TFreeSy s) = s
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   158
  | str_of_token (TVarSy s) = s
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   159
  | str_of_token (NumSy s) = s
11697
8dd899efbd35 added "num" token;
wenzelm
parents: 9326
diff changeset
   160
  | str_of_token (XNumSy s) = s
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   161
  | str_of_token (StrSy s) = s
376
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
   162
  | str_of_token EndToken = "EOF";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   164
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   165
(* display_token *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   167
fun display_token (Token s) = quote s
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   168
  | display_token (IdentSy s) = "id(" ^ s ^ ")"
3828
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
   169
  | display_token (LongIdentSy s) = "longid(" ^ s ^ ")"
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   170
  | display_token (VarSy s) = "var(" ^ s ^ ")"
330
2fda15dd1e0f changed the way a grammar is generated to allow the new parser to work;
clasohm
parents: 237
diff changeset
   171
  | display_token (TFreeSy s) = "tid(" ^ s ^ ")"
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   172
  | display_token (TVarSy s) = "tvar(" ^ s ^ ")"
11697
8dd899efbd35 added "num" token;
wenzelm
parents: 9326
diff changeset
   173
  | display_token (NumSy s) = "num(" ^ s ^ ")"
8dd899efbd35 added "num" token;
wenzelm
parents: 9326
diff changeset
   174
  | display_token (XNumSy s) = "xnum(" ^ s ^ ")"
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   175
  | display_token (StrSy s) = "xstr(" ^ s ^ ")"
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   176
  | display_token EndToken = "";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   178
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   179
(* matching_tokens *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   181
fun matching_tokens (Token x, Token y) = (x = y)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   182
  | matching_tokens (IdentSy _, IdentSy _) = true
3828
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
   183
  | matching_tokens (LongIdentSy _, LongIdentSy _) = true
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   184
  | matching_tokens (VarSy _, VarSy _) = true
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   185
  | matching_tokens (TFreeSy _, TFreeSy _) = true
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   186
  | matching_tokens (TVarSy _, TVarSy _) = true
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   187
  | matching_tokens (NumSy _, NumSy _) = true
11697
8dd899efbd35 added "num" token;
wenzelm
parents: 9326
diff changeset
   188
  | matching_tokens (XNumSy _, XNumSy _) = true
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   189
  | matching_tokens (StrSy _, StrSy _) = true
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   190
  | matching_tokens (EndToken, EndToken) = true
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   191
  | matching_tokens _ = false;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   194
(* valued_token *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   196
fun valued_token (Token _) = false
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   197
  | valued_token (IdentSy _) = true
3828
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
   198
  | valued_token (LongIdentSy _) = true
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   199
  | valued_token (VarSy _) = true
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   200
  | valued_token (TFreeSy _) = true
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   201
  | valued_token (TVarSy _) = true
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   202
  | valued_token (NumSy _) = true
11697
8dd899efbd35 added "num" token;
wenzelm
parents: 9326
diff changeset
   203
  | valued_token (XNumSy _) = true
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   204
  | valued_token (StrSy _) = true
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   205
  | valued_token EndToken = false;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   208
(* predef_term *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15443
diff changeset
   210
fun predef_term "id" = SOME (IdentSy "id")
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15443
diff changeset
   211
  | predef_term "longid" = SOME (LongIdentSy "longid")
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15443
diff changeset
   212
  | predef_term "var" = SOME (VarSy "var")
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15443
diff changeset
   213
  | predef_term "tid" = SOME (TFreeSy "tid")
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15443
diff changeset
   214
  | predef_term "tvar" = SOME (TVarSy "tvar")
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15443
diff changeset
   215
  | predef_term "num" = SOME (NumSy "num")
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15443
diff changeset
   216
  | predef_term "xnum" = SOME (XNumSy "xnum")
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15443
diff changeset
   217
  | predef_term "xstr" = SOME (StrSy "xstr")
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15443
diff changeset
   218
  | predef_term _ = NONE;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   221
(* xstr tokens *)
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   222
14730
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   223
fun lex_err msg prfx (cs, _) =
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   224
  "Inner lexical error: " ^ msg ^ " at " ^ quote (prfx ^ Symbol.beginning 10 cs);
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   225
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   226
val scan_chr =
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   227
  $$ "\\" |-- Scan.one Symbol.not_eof ||
19305
5c16895d548b avoid polymorphic equality;
wenzelm
parents: 19002
diff changeset
   228
  Scan.one (fn s => s <> "'" andalso Symbol.not_eof s) ||
5c16895d548b avoid polymorphic equality;
wenzelm
parents: 19002
diff changeset
   229
  $$ "'" --| Scan.ahead (~$$ "'");
14730
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   230
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   231
val scan_str =
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   232
  $$ "'" |-- $$ "'" |-- !! (lex_err "missing end of string" "''")
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   233
    (Scan.repeat scan_chr --| $$ "'" --| $$ "'");
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   234
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   236
fun implode_xstr cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs));
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   237
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   238
fun explode_xstr str =
5868
0022d0a913b5 tuned usage of read;
wenzelm
parents: 5860
diff changeset
   239
  (case Scan.read Symbol.stopper scan_str (Symbol.explode str) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15443
diff changeset
   240
    SOME cs => cs
5868
0022d0a913b5 tuned usage of read;
wenzelm
parents: 5860
diff changeset
   241
  | _ => error ("Inner lexical error: literal string expected at " ^ quote str));
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   242
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   243
14730
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   244
(* nested comments *)
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   245
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   246
val scan_cmt =
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   247
  Scan.depend (fn d => $$ "(" ^^ $$ "*" >> pair (d + 1)) ||
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   248
  Scan.depend (fn 0 => Scan.fail | d => $$ "*" ^^ $$ ")" >> pair (d - 1)) ||
19305
5c16895d548b avoid polymorphic equality;
wenzelm
parents: 19002
diff changeset
   249
  Scan.lift ($$ "*" --| Scan.ahead (~$$ ")")) ||
5c16895d548b avoid polymorphic equality;
wenzelm
parents: 19002
diff changeset
   250
  Scan.lift (Scan.one (fn s => s <> "*" andalso Symbol.not_eof s));
14730
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   251
14783
e7f7ed4c06f2 string_of_vname moved to term.ML;
wenzelm
parents: 14737
diff changeset
   252
val scan_comment =
e7f7ed4c06f2 string_of_vname moved to term.ML;
wenzelm
parents: 14737
diff changeset
   253
  $$ "(" -- $$ "*" -- !! (lex_err "missing end of comment" "(*")
14730
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   254
    (Scan.pass 0 (Scan.repeat scan_cmt) -- $$ "*" -- $$ ")")
14783
e7f7ed4c06f2 string_of_vname moved to term.ML;
wenzelm
parents: 14737
diff changeset
   255
  >> K ();
14730
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   256
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   257
18
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
(** tokenize **)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   260
2363
963285471dc5 tokenize: no gets exploded char list;
wenzelm
parents: 1507
diff changeset
   261
fun tokenize lex xids chs =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   262
  let
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   263
    val scan_xid =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   264
      if xids then $$ "_" ^^ scan_id || scan_id
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   265
      else scan_id;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   266
20096
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   267
    val scan_num = scan_hex || scan_bin || scan_int;
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   268
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   269
    val scan_val =
4902
8fbccead3695 added scan_tvar;
wenzelm
parents: 4703
diff changeset
   270
      scan_tvar >> pair TVarSy ||
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   271
      scan_var >> pair VarSy ||
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   272
      scan_tid >> pair TFreeSy ||
20096
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   273
      scan_num >> pair NumSy ||
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   274
      $$ "#" ^^ scan_num >> pair XNumSy ||
3828
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
   275
      scan_longid >> pair LongIdentSy ||
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   276
      scan_xid >> pair IdentSy;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   277
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   278
    val scan_lit = Scan.literal lex >> (pair Token o implode);
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   279
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   280
    val scan_token =
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15443
diff changeset
   281
      scan_comment >> K NONE ||
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15443
diff changeset
   282
      Scan.max (op <= o pairself snd) scan_lit scan_val >> (fn (tk, s) => SOME (tk s)) ||
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15443
diff changeset
   283
      scan_str >> (SOME o StrSy o implode_xstr) ||
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15443
diff changeset
   284
      Scan.one Symbol.is_blank >> K NONE;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   285
  in
4938
c8bbbf3c59fa Symbol.stopper;
wenzelm
parents: 4921
diff changeset
   286
    (case Scan.error (Scan.finite Symbol.stopper (Scan.repeat scan_token)) chs of
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19305
diff changeset
   287
      (toks, []) => map_filter I toks @ [EndToken]
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   288
    | (_, cs) => error ("Inner lexical error at: " ^ quote (implode cs)))
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   289
  end;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   290
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   291
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   292
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   293
(** scan variables **)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   294
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   295
(* scan_indexname *)
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   296
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   297
local
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   298
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   299
fun scan_vname chrs =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   300
  let
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   301
    fun nat n [] = n
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   302
      | 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
   303
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   304
    fun idxname cs ds = (implode (rev cs), nat 0 ds);
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   305
    fun chop_idx [] ds = idxname [] ds
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   306
      | chop_idx (cs as (_ :: "\\<^isub>" :: _)) ds = idxname cs ds
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   307
      | chop_idx (cs as (_ :: "\\<^isup>" :: _)) ds = idxname cs ds
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   308
      | chop_idx (c :: cs) ds =
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   309
          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
   310
          else idxname (c :: cs) ds;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   311
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   312
    val scan =
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   313
      scan_letter_letdigs -- Scan.optional ($$ "." |-- scan_digits1 >> nat 0) ~1;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   314
  in
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   315
    (case scan chrs of
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   316
      ((cs, ~1), cs') => (chop_idx (rev cs) [], cs')
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   317
    | ((cs, i), cs') => ((implode cs, i), cs'))
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   318
  end;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   319
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   320
in
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   321
15443
07f78cc82a73 indexname function now parses type variables as well; changed input
berghofe
parents: 14981
diff changeset
   322
val scan_indexname =
07f78cc82a73 indexname function now parses type variables as well; changed input
berghofe
parents: 14981
diff changeset
   323
     $$ "'" |-- scan_vname >> (fn (x, i) => ("'" ^ x, i))
07f78cc82a73 indexname function now parses type variables as well; changed input
berghofe
parents: 14981
diff changeset
   324
  || scan_vname;
07f78cc82a73 indexname function now parses type variables as well; changed input
berghofe
parents: 14981
diff changeset
   325
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   326
end;
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   327
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   328
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   329
(* indexname *)
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   330
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   331
fun indexname cs =
15443
07f78cc82a73 indexname function now parses type variables as well; changed input
berghofe
parents: 14981
diff changeset
   332
  (case Scan.read Symbol.stopper scan_indexname (Symbol.explode cs) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15443
diff changeset
   333
    SOME xi => xi
15443
07f78cc82a73 indexname function now parses type variables as well; changed input
berghofe
parents: 14981
diff changeset
   334
  | _ => error ("Lexical error in variable name: " ^ quote cs));
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   335
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   336
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   337
(* read_var *)
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   338
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   339
fun const c = Const (c, dummyT);
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   340
fun free x = Free (x, dummyT);
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   341
fun var xi = Var (xi, dummyT);
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   342
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   343
fun read_var str =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   344
  let
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   345
    val scan =
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   346
      $$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol.is_eof) >> var ||
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   347
      Scan.any Symbol.not_eof >> (free o implode);
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   348
  in the (Scan.read Symbol.stopper scan (Symbol.explode str)) end;
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   349
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   350
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   351
(* read_variable *)
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   352
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   353
fun read_variable str =
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   354
  let val scan = $$ "?" |-- scan_indexname || scan_indexname
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   355
  in Scan.read Symbol.stopper scan (Symbol.explode str) end;
4587
6bce9ef27d7e added read_var;
wenzelm
parents: 4247
diff changeset
   356
6bce9ef27d7e added read_var;
wenzelm
parents: 4247
diff changeset
   357
19002
2fbb3d809026 added fixedN, constN;
wenzelm
parents: 18375
diff changeset
   358
(* specific identifiers *)
5260
1835a591d3a7 binding / skolem vars;
wenzelm
parents: 5112
diff changeset
   359
19002
2fbb3d809026 added fixedN, constN;
wenzelm
parents: 18375
diff changeset
   360
val constN = "\\<^const>";
2fbb3d809026 added fixedN, constN;
wenzelm
parents: 18375
diff changeset
   361
val fixedN = "\\<^fixed>";
2fbb3d809026 added fixedN, constN;
wenzelm
parents: 18375
diff changeset
   362
5260
1835a591d3a7 binding / skolem vars;
wenzelm
parents: 5112
diff changeset
   363
5860
ed11c9890852 added read_nat;
wenzelm
parents: 5513
diff changeset
   364
(* read_nat *)
ed11c9890852 added read_nat;
wenzelm
parents: 5513
diff changeset
   365
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   366
fun read_nat s =
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   367
  Option.map (#1 o Library.read_int)
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   368
    (Scan.read Symbol.stopper scan_digits1 (Symbol.explode s));
5860
ed11c9890852 added read_nat;
wenzelm
parents: 5513
diff changeset
   369
ed11c9890852 added read_nat;
wenzelm
parents: 5513
diff changeset
   370
20096
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   371
(* read_xnum: hex/bin/decimal *)
9326
1625c1f172b3 added read_xnum;
wenzelm
parents: 9289
diff changeset
   372
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   373
local
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   374
20096
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   375
val ten = ord "0" + 10;
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   376
val a = ord "a";
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   377
val A = ord "A";
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   378
val _ = assert (a > A) "Bad ASCII";
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   379
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   380
fun remap_hex c =
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   381
  let val x = ord c in
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   382
    if x >= a then chr (x - a + ten)
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   383
    else if x >= A then chr (x - A + ten)
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   384
    else c
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   385
  end;
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   386
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   387
in
15965
f422f8283491 Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents: 15570
diff changeset
   388
9326
1625c1f172b3 added read_xnum;
wenzelm
parents: 9289
diff changeset
   389
fun read_xnum str =
1625c1f172b3 added read_xnum;
wenzelm
parents: 9289
diff changeset
   390
  let
20096
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   391
    val (sign, radix, digs) =
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   392
      (case Symbol.explode (perhaps (try (unprefix "#")) str) of
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   393
        "0" :: "x" :: cs => (1, 16, map remap_hex cs)
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   394
      | "0" :: "b" :: cs => (1, 2, cs)
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   395
      | "-" :: cs => (~1, 10, cs)
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   396
      | cs => (1, 10, cs));
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   397
  in sign * #1 (Library.read_intinf radix digs) end;
9326
1625c1f172b3 added read_xnum;
wenzelm
parents: 9289
diff changeset
   398
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   399
end;
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   400
9326
1625c1f172b3 added read_xnum;
wenzelm
parents: 9289
diff changeset
   401
7784
228283fa5de4 read_idents;
wenzelm
parents: 7472
diff changeset
   402
(* read_ident(s) *)
228283fa5de4 read_idents;
wenzelm
parents: 7472
diff changeset
   403
228283fa5de4 read_idents;
wenzelm
parents: 7472
diff changeset
   404
fun read_idents str =
228283fa5de4 read_idents;
wenzelm
parents: 7472
diff changeset
   405
  let
228283fa5de4 read_idents;
wenzelm
parents: 7472
diff changeset
   406
    val blanks = Scan.any Symbol.is_blank;
228283fa5de4 read_idents;
wenzelm
parents: 7472
diff changeset
   407
    val junk = Scan.any Symbol.not_eof;
228283fa5de4 read_idents;
wenzelm
parents: 7472
diff changeset
   408
    val idents = Scan.repeat1 (blanks |-- scan_id --| blanks) -- junk;
228283fa5de4 read_idents;
wenzelm
parents: 7472
diff changeset
   409
  in
228283fa5de4 read_idents;
wenzelm
parents: 7472
diff changeset
   410
    (case Scan.read Symbol.stopper idents (Symbol.explode str) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15443
diff changeset
   411
      SOME (ids, []) => ids
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15443
diff changeset
   412
    | SOME (_, bad) => error ("Bad identifier: " ^ quote (implode bad))
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15443
diff changeset
   413
    | NONE => error ("No identifier found in: " ^ quote str))
7784
228283fa5de4 read_idents;
wenzelm
parents: 7472
diff changeset
   414
  end;
228283fa5de4 read_idents;
wenzelm
parents: 7472
diff changeset
   415
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   416
end;