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