src/Pure/Isar/token.ML
author wenzelm
Sat Jul 23 16:37:17 2011 +0200 (2011-07-23)
changeset 43947 9b00f09f7721
parent 43773 e8ba493027a3
child 44658 5bec9c15ef29
permissions -rw-r--r--
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
     1 (*  Title:      Pure/Isar/token.ML
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 Outer token syntax for Isabelle/Isar.
     5 *)
     6 
     7 signature TOKEN =
     8 sig
     9   datatype kind =
    10     Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
    11     Nat | Float | String | AltString | Verbatim | Space | Comment | InternalValue |
    12     Error of string | Sync | EOF
    13   datatype value =
    14     Text of string | Typ of typ | Term of term | Fact of thm list |
    15     Attribute of morphism -> attribute
    16   type T
    17   val str_of_kind: kind -> string
    18   val position_of: T -> Position.T
    19   val end_position_of: T -> Position.T
    20   val pos_of: T -> string
    21   val eof: T
    22   val is_eof: T -> bool
    23   val not_eof: T -> bool
    24   val not_sync: T -> bool
    25   val stopper: T Scan.stopper
    26   val kind_of: T -> kind
    27   val is_kind: kind -> T -> bool
    28   val keyword_with: (string -> bool) -> T -> bool
    29   val ident_with: (string -> bool) -> T -> bool
    30   val is_proper: T -> bool
    31   val is_semicolon: T -> bool
    32   val is_comment: T -> bool
    33   val is_begin_ignore: T -> bool
    34   val is_end_ignore: T -> bool
    35   val is_blank: T -> bool
    36   val is_newline: T -> bool
    37   val source_of: T -> string
    38   val source_position_of: T -> Symbol_Pos.text * Position.T
    39   val content_of: T -> string
    40   val unparse: T -> string
    41   val text_of: T -> string * string
    42   val get_value: T -> value option
    43   val map_value: (value -> value) -> T -> T
    44   val mk_text: string -> T
    45   val mk_typ: typ -> T
    46   val mk_term: term -> T
    47   val mk_fact: thm list -> T
    48   val mk_attribute: (morphism -> attribute) -> T
    49   val assignable: T -> T
    50   val assign: value option -> T -> unit
    51   val closure: T -> T
    52   val ident_or_symbolic: string -> bool
    53   val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
    54   val source': {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
    55     (Symbol_Pos.T, 'a) Source.source -> (T, (Symbol_Pos.T, 'a) Source.source) Source.source
    56   val source: {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
    57     Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
    58       (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
    59   val read_antiq: Scan.lexicon -> (T list -> 'a * T list) -> Symbol_Pos.T list * Position.T -> 'a
    60 end;
    61 
    62 structure Token: TOKEN =
    63 struct
    64 
    65 (** tokens **)
    66 
    67 (* token values *)
    68 
    69 (*The value slot assigns an (optional) internal value to a token,
    70   usually as a side-effect of special scanner setup (see also
    71   args.ML).  Note that an assignable ref designates an intermediate
    72   state of internalization -- it is NOT meant to persist.*)
    73 
    74 datatype value =
    75   Text of string |
    76   Typ of typ |
    77   Term of term |
    78   Fact of thm list |
    79   Attribute of morphism -> attribute;
    80 
    81 datatype slot =
    82   Slot |
    83   Value of value option |
    84   Assignable of value option Unsynchronized.ref;
    85 
    86 
    87 (* datatype token *)
    88 
    89 datatype kind =
    90   Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
    91   Nat | Float | String | AltString | Verbatim | Space | Comment | InternalValue |
    92   Error of string | Sync | EOF;
    93 
    94 datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot;
    95 
    96 val str_of_kind =
    97  fn Command => "command"
    98   | Keyword => "keyword"
    99   | Ident => "identifier"
   100   | LongIdent => "long identifier"
   101   | SymIdent => "symbolic identifier"
   102   | Var => "schematic variable"
   103   | TypeIdent => "type variable"
   104   | TypeVar => "schematic type variable"
   105   | Nat => "natural number"
   106   | Float => "floating-point number"
   107   | String => "string"
   108   | AltString => "back-quoted string"
   109   | Verbatim => "verbatim text"
   110   | Space => "white space"
   111   | Comment => "comment text"
   112   | InternalValue => "internal value"
   113   | Error _ => "bad input"
   114   | Sync => "sync marker"
   115   | EOF => "end-of-file";
   116 
   117 
   118 (* position *)
   119 
   120 fun position_of (Token ((_, (pos, _)), _, _)) = pos;
   121 fun end_position_of (Token ((_, (_, pos)), _, _)) = pos;
   122 
   123 val pos_of = Position.str_of o position_of;
   124 
   125 
   126 (* control tokens *)
   127 
   128 fun mk_eof pos = Token (("", (pos, Position.none)), (EOF, ""), Slot);
   129 val eof = mk_eof Position.none;
   130 
   131 fun is_eof (Token (_, (EOF, _), _)) = true
   132   | is_eof _ = false;
   133 
   134 val not_eof = not o is_eof;
   135 
   136 fun not_sync (Token (_, (Sync, _), _)) = false
   137   | not_sync _ = true;
   138 
   139 val stopper =
   140   Scan.stopper (fn [] => eof | toks => mk_eof (end_position_of (List.last toks))) is_eof;
   141 
   142 
   143 (* kind of token *)
   144 
   145 fun kind_of (Token (_, (k, _), _)) = k;
   146 fun is_kind k (Token (_, (k', _), _)) = k = k';
   147 
   148 fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
   149   | keyword_with _ _ = false;
   150 
   151 fun ident_with pred (Token (_, (Ident, x), _)) = pred x
   152   | ident_with _ _ = false;
   153 
   154 fun is_proper (Token (_, (Space, _), _)) = false
   155   | is_proper (Token (_, (Comment, _), _)) = false
   156   | is_proper _ = true;
   157 
   158 fun is_semicolon (Token (_, (Keyword, ";"), _)) = true
   159   | is_semicolon _ = false;
   160 
   161 fun is_comment (Token (_, (Comment, _), _)) = true
   162   | is_comment _ = false;
   163 
   164 fun is_begin_ignore (Token (_, (Comment, "<"), _)) = true
   165   | is_begin_ignore _ = false;
   166 
   167 fun is_end_ignore (Token (_, (Comment, ">"), _)) = true
   168   | is_end_ignore _ = false;
   169 
   170 
   171 (* blanks and newlines -- space tokens obey lines *)
   172 
   173 fun is_blank (Token (_, (Space, x), _)) = not (String.isSuffix "\n" x)
   174   | is_blank _ = false;
   175 
   176 fun is_newline (Token (_, (Space, x), _)) = String.isSuffix "\n" x
   177   | is_newline _ = false;
   178 
   179 
   180 (* token content *)
   181 
   182 fun source_of (Token ((source, (pos, _)), (_, x), _)) =
   183   if YXML.detect x then x
   184   else YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source]));
   185 
   186 fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);
   187 
   188 fun content_of (Token (_, (_, x), _)) = x;
   189 
   190 
   191 (* unparse *)
   192 
   193 fun unparse (Token (_, (kind, x), _)) =
   194   (case kind of
   195     String => Symbol_Pos.quote_string_qq x
   196   | AltString => Symbol_Pos.quote_string_bq x
   197   | Verbatim => enclose "{*" "*}" x
   198   | Comment => enclose "(*" "*)" x
   199   | Sync => ""
   200   | EOF => ""
   201   | _ => x);
   202 
   203 fun text_of tok =
   204   if is_semicolon tok then ("terminator", "")
   205   else
   206     let
   207       val k = str_of_kind (kind_of tok);
   208       val s = unparse tok;
   209     in
   210       if s = "" then (k, "")
   211       else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ s, "")
   212       else (k, s)
   213     end;
   214 
   215 
   216 
   217 (** associated values **)
   218 
   219 (* access values *)
   220 
   221 fun get_value (Token (_, _, Value v)) = v
   222   | get_value _ = NONE;
   223 
   224 fun map_value f (Token (x, y, Value (SOME v))) = Token (x, y, Value (SOME (f v)))
   225   | map_value _ tok = tok;
   226 
   227 
   228 (* make values *)
   229 
   230 fun mk_value k v = Token ((k, Position.no_range), (InternalValue, k), Value (SOME v));
   231 
   232 val mk_text = mk_value "<text>" o Text;
   233 val mk_typ = mk_value "<typ>" o Typ;
   234 val mk_term = mk_value "<term>" o Term;
   235 val mk_fact = mk_value "<fact>" o Fact;
   236 val mk_attribute = mk_value "<attribute>" o Attribute;
   237 
   238 
   239 (* static binding *)
   240 
   241 (*1st stage: make empty slots assignable*)
   242 fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (Unsynchronized.ref NONE))
   243   | assignable tok = tok;
   244 
   245 (*2nd stage: assign values as side-effect of scanning*)
   246 fun assign v (Token (_, _, Assignable r)) = r := v
   247   | assign _ _ = ();
   248 
   249 (*3rd stage: static closure of final values*)
   250 fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v)
   251   | closure tok = tok;
   252 
   253 
   254 
   255 (** scanners **)
   256 
   257 open Basic_Symbol_Pos;
   258 
   259 fun !!! msg = Symbol_Pos.!!! (fn () => "Outer lexical error: " ^ msg);
   260 
   261 
   262 (* scan symbolic idents *)
   263 
   264 val is_sym_char = member (op =) (raw_explode "!#$%&*+-/<=>?@^_|~");
   265 
   266 val scan_symid =
   267   Scan.many1 (is_sym_char o Symbol_Pos.symbol) ||
   268   Scan.one (Symbol.is_symbolic o Symbol_Pos.symbol) >> single;
   269 
   270 fun is_symid str =
   271   (case try Symbol.explode str of
   272     SOME [s] => Symbol.is_symbolic s orelse is_sym_char s
   273   | SOME ss => forall is_sym_char ss
   274   | _ => false);
   275 
   276 fun ident_or_symbolic "begin" = false
   277   | ident_or_symbolic ":" = true
   278   | ident_or_symbolic "::" = true
   279   | ident_or_symbolic s = Lexicon.is_identifier s orelse is_symid s;
   280 
   281 
   282 (* scan verbatim text *)
   283 
   284 val scan_verb =
   285   $$$ "*" --| Scan.ahead (~$$$ "}") ||
   286   Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single;
   287 
   288 val scan_verbatim =
   289   (Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") -- !!! "missing end of verbatim text"
   290     (Symbol_Pos.change_prompt
   291       ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
   292 
   293 
   294 (* scan space *)
   295 
   296 fun is_space s = Symbol.is_blank s andalso s <> "\n";
   297 
   298 val scan_space =
   299   Scan.many1 (is_space o Symbol_Pos.symbol) @@@ Scan.optional ($$$ "\n") [] ||
   300   Scan.many (is_space o Symbol_Pos.symbol) @@@ $$$ "\n";
   301 
   302 
   303 (* scan comment *)
   304 
   305 val scan_comment =
   306   Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body !!! -- Symbol_Pos.scan_pos);
   307 
   308 
   309 
   310 (** token sources **)
   311 
   312 fun source_proper src = src |> Source.filter is_proper;
   313 
   314 local
   315 
   316 fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2;
   317 
   318 fun token k ss =
   319   Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.content ss), Slot);
   320 
   321 fun token_range k (pos1, (ss, pos2)) =
   322   Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.content ss), Slot);
   323 
   324 fun scan (lex1, lex2) = !!! "bad input"
   325   (Symbol_Pos.scan_string_qq >> token_range String ||
   326     Symbol_Pos.scan_string_bq >> token_range AltString ||
   327     scan_verbatim >> token_range Verbatim ||
   328     scan_comment >> token_range Comment ||
   329     scan_space >> token Space ||
   330     Scan.one (Symbol.is_sync o Symbol_Pos.symbol) >> (token Sync o single) ||
   331     (Scan.max token_leq
   332       (Scan.max token_leq
   333         (Scan.literal lex2 >> pair Command)
   334         (Scan.literal lex1 >> pair Keyword))
   335       (Lexicon.scan_longid >> pair LongIdent ||
   336         Lexicon.scan_id >> pair Ident ||
   337         Lexicon.scan_var >> pair Var ||
   338         Lexicon.scan_tid >> pair TypeIdent ||
   339         Lexicon.scan_tvar >> pair TypeVar ||
   340         Lexicon.scan_float >> pair Float ||
   341         Lexicon.scan_nat >> pair Nat ||
   342         scan_symid >> pair SymIdent) >> uncurry token));
   343 
   344 fun recover msg =
   345   Scan.many ((Symbol.is_regular andf (not o Symbol.is_blank)) o Symbol_Pos.symbol)
   346   >> (single o token (Error msg));
   347 
   348 in
   349 
   350 fun source' {do_recover} get_lex =
   351   Source.source Symbol_Pos.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
   352     (Option.map (rpair recover) do_recover);
   353 
   354 fun source do_recover get_lex pos src =
   355   Symbol_Pos.source pos src
   356   |> source' do_recover get_lex;
   357 
   358 end;
   359 
   360 
   361 (* read_antiq *)
   362 
   363 fun read_antiq lex scan (syms, pos) =
   364   let
   365     fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^
   366       "@{" ^ Symbol_Pos.content syms ^ "}");
   367 
   368     val res =
   369       Source.of_list syms
   370       |> source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
   371       |> source_proper
   372       |> Source.source stopper (Scan.error (Scan.bulk scan)) NONE
   373       |> Source.exhaust;
   374   in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
   375 
   376 end;