src/Pure/Isar/outer_lex.ML
author haftmann
Fri Nov 10 07:44:47 2006 +0100 (2006-11-10)
changeset 21286 b5e7b80caa6a
parent 20982 fade54fde622
child 21858 05f57309170c
permissions -rw-r--r--
introduces canonical AList functions for loop_tacs
     1 (*  Title:      Pure/Isar/outer_lex.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Outer lexical syntax for Isabelle/Isar.
     6 *)
     7 
     8 signature OUTER_LEX =
     9 sig
    10   datatype token_kind =
    11     Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
    12     Nat | String | AltString | Verbatim | Space | Comment | Sync | Malformed | EOF
    13   eqtype token
    14   val str_of_kind: token_kind -> string
    15   val stopper: token * (token -> bool)
    16   val not_sync: token -> bool
    17   val not_eof: token -> bool
    18   val position_of: token -> Position.T
    19   val pos_of: token -> string
    20   val is_kind: token_kind -> token -> bool
    21   val keyword_with: (string -> bool) -> token -> bool
    22   val ident_with: (string -> bool) -> token -> bool
    23   val name_of: token -> string
    24   val is_proper: token -> bool
    25   val is_semicolon: token -> bool
    26   val is_comment: token -> bool
    27   val is_begin_ignore: token -> bool
    28   val is_end_ignore: token -> bool
    29   val is_blank: token -> bool
    30   val is_newline: token -> bool
    31   val unparse: token -> string
    32   val val_of: token -> string
    33   val is_sid: string -> bool
    34   val !!! : string -> (Position.T * 'a -> 'b) -> Position.T * 'a -> 'b
    35   val incr_line: ('a -> 'b * 'c) -> Position.T * 'a -> 'b * (Position.T * 'c)
    36   val keep_line: ('a -> 'b * 'c) -> Position.T * 'a -> 'b * (Position.T * 'c)
    37   val scan_blank: Position.T * Symbol.symbol list
    38     -> Symbol.symbol * (Position.T * Symbol.symbol list)
    39   val scan_string: Position.T * Symbol.symbol list -> string * (Position.T * Symbol.symbol list)
    40   val scan: (Scan.lexicon * Scan.lexicon) ->
    41     Position.T * Symbol.symbol list -> token * (Position.T * Symbol.symbol list)
    42   val source: bool -> (unit -> (Scan.lexicon * Scan.lexicon)) ->
    43     Position.T -> (Symbol.symbol, 'a) Source.source ->
    44     (token, Position.T * (Symbol.symbol, 'a) Source.source) Source.source
    45   val source_proper: (token, 'a) Source.source ->
    46     (token, (token, 'a) Source.source) Source.source
    47   val make_lexicon: string list -> Scan.lexicon
    48 end;
    49 
    50 structure OuterLex: OUTER_LEX =
    51 struct
    52 
    53 
    54 (** tokens **)
    55 
    56 (* datatype token *)
    57 
    58 datatype token_kind =
    59   Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
    60   Nat | String | AltString | Verbatim | Space | Comment | Sync | Malformed | EOF;
    61 
    62 datatype token = Token of Position.T * (token_kind * string);
    63 
    64 val str_of_kind =
    65  fn Command => "command"
    66   | Keyword => "keyword"
    67   | Ident => "identifier"
    68   | LongIdent => "long identifier"
    69   | SymIdent => "symbolic identifier"
    70   | Var => "schematic variable"
    71   | TypeIdent => "type variable"
    72   | TypeVar => "schematic type variable"
    73   | Nat => "number"
    74   | String => "string"
    75   | AltString => "back-quoted string"
    76   | Verbatim => "verbatim text"
    77   | Space => "white space"
    78   | Comment => "comment text"
    79   | Sync => "sync marker"
    80   | Malformed => "bad input"
    81   | EOF => "end-of-file";
    82 
    83 
    84 (* control tokens *)
    85 
    86 fun not_sync (Token (_, (Sync, _))) = false
    87   | not_sync _ = true;
    88 
    89 val malformed = Token (Position.none, (Malformed, ""));
    90 fun malformed_of xs = Token (Position.none, (Malformed, implode xs));
    91 
    92 
    93 (* eof token *)
    94 
    95 val eof = Token (Position.none, (EOF, ""));
    96 
    97 fun is_eof (Token (_, (EOF, _))) = true
    98   | is_eof _ = false;
    99 
   100 val stopper = (eof, is_eof);
   101 val not_eof = not o is_eof;
   102 
   103 
   104 (* get position *)
   105 
   106 fun position_of (Token (pos, _)) = pos;
   107 val pos_of = Position.str_of o position_of;
   108 
   109 
   110 (* kind of token *)
   111 
   112 fun is_kind k (Token (_, (k', _))) = k = k';
   113 
   114 fun keyword_with pred (Token (_, (Keyword, x))) = pred x
   115   | keyword_with _ _ = false;
   116 
   117 fun ident_with pred (Token (_, (Ident, x))) = pred x
   118   | ident_with _ _ = false;
   119 
   120 fun is_proper (Token (_, (Space, _))) = false
   121   | is_proper (Token (_, (Comment, _))) = false
   122   | is_proper _ = true;
   123 
   124 fun is_semicolon (Token (_, (Keyword, ";"))) = true
   125   | is_semicolon _ = false;
   126 
   127 fun is_comment (Token (_, (Comment, _))) = true
   128   | is_comment _ = false;
   129 
   130 fun is_begin_ignore (Token (_, (Comment, "<"))) = true
   131   | is_begin_ignore _ = false;
   132 
   133 fun is_end_ignore (Token (_, (Comment, ">"))) = true
   134   | is_end_ignore _ = false;
   135 
   136 
   137 (* blanks and newlines -- space tokens obey lines *)
   138 
   139 fun is_blank (Token (_, (Space, s))) = not (String.isSuffix "\n" s)
   140   | is_blank _ = false;
   141 
   142 fun is_newline (Token (_, (Space, s))) = String.isSuffix "\n" s
   143   | is_newline _ = false;
   144 
   145 
   146 (* token content *)
   147 
   148 fun name_of (tok as Token (_, (k, x))) =
   149   if is_semicolon tok then "terminator"
   150   else if x = "" then str_of_kind k
   151   else str_of_kind k ^ " " ^ quote x;
   152 
   153 fun escape q =
   154   implode o map (fn s => if s = q orelse s = "\\" then "\\" ^ s else s) o Symbol.explode;
   155 
   156 fun unparse (Token (_, (kind, x))) =
   157   (case kind of
   158     String => x |> quote o escape "\""
   159   | AltString => x |> enclose "`" "`" o escape "`"
   160   | Verbatim => x |> enclose "{*" "*}"
   161   | Comment => x |> enclose "(*" "*)"
   162   | _ => x);
   163 
   164 fun val_of (Token (_, (_, x))) = x;
   165 
   166 fun token_leq (Token (_, (_, x)), Token (_, (_, x'))) = x <= x';
   167 
   168 
   169 
   170 (** scanners **)
   171 
   172 fun change_prompt scan = Scan.prompt "# " scan;
   173 
   174 
   175 (* diagnostics *)
   176 
   177 fun lex_err msg ((pos, cs), _) = "Outer lexical error" ^ Position.str_of pos ^ ": " ^ msg cs;
   178 fun !!! msg scan = Scan.!! (lex_err (K msg)) scan;
   179 
   180 
   181 (* line numbering *)
   182 
   183 fun incr_line scan = Scan.depend (fn pos => scan >> pair (Position.inc pos));
   184 val keep_line = Scan.lift;
   185 
   186 val scan_blank =
   187   incr_line ($$ "\n") ||
   188   keep_line (Scan.one Symbol.is_blank);
   189 
   190 
   191 (* scan symbolic idents *)
   192 
   193 val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
   194 
   195 val scan_symid =
   196   Scan.any1 is_sym_char >> implode ||
   197   Scan.one Symbol.is_symbolic;
   198 
   199 fun is_symid str =
   200   (case try Symbol.explode str of
   201     SOME [s] => Symbol.is_symbolic s orelse is_sym_char s
   202   | SOME ss => forall is_sym_char ss
   203   | _ => false);
   204 
   205 fun is_sid "begin" = false
   206   | is_sid ":" = true
   207   | is_sid s = is_symid s orelse Syntax.is_identifier s;
   208 
   209 
   210 (* scan strings *)
   211 
   212 local
   213 
   214 fun scan_str q =
   215   scan_blank ||
   216   keep_line ($$ "\\") |-- !!! "bad escape character in string"
   217       (scan_blank || keep_line ($$ q || $$ "\\")) ||
   218   keep_line (Scan.one (fn s => s <> q andalso s <> "\\" andalso
   219     Symbol.not_sync s andalso Symbol.not_eof s));
   220 
   221 fun scan_strs q =
   222   keep_line ($$ q) |--
   223     !!! "missing quote at end of string"
   224       (change_prompt ((Scan.repeat (scan_str q) >> implode) --| keep_line ($$ q)));
   225 
   226 in
   227 
   228 val scan_string = scan_strs "\"";
   229 val scan_alt_string = scan_strs "`";
   230 
   231 end;
   232 
   233 
   234 (* scan verbatim text *)
   235 
   236 val scan_verb =
   237   scan_blank ||
   238   keep_line ($$ "*" --| Scan.ahead (~$$ "}")) ||
   239   keep_line (Scan.one (fn s => s <> "*" andalso Symbol.not_sync s andalso Symbol.not_eof s));
   240 
   241 val scan_verbatim =
   242   keep_line ($$ "{" -- $$ "*") |--
   243     !!! "missing end of verbatim text"
   244       (change_prompt ((Scan.repeat scan_verb >> implode) --| keep_line ($$ "*" -- $$ "}")));
   245 
   246 
   247 (* scan space *)
   248 
   249 fun is_space s = Symbol.is_blank s andalso s <> "\n";
   250 
   251 val scan_space =
   252   (keep_line (Scan.any1 is_space) -- Scan.optional (incr_line ($$ "\n")) "" ||
   253     keep_line (Scan.any is_space) -- incr_line ($$ "\n")) >> (fn (cs, c) => implode cs ^ c);
   254 
   255 
   256 (* scan nested comments *)
   257 
   258 val scan_cmt =
   259   Scan.lift scan_blank ||
   260   Scan.depend (fn d => keep_line ($$ "(" ^^ $$ "*") >> pair (d + 1)) ||
   261   Scan.depend (fn 0 => Scan.fail | d => keep_line ($$ "*" ^^ $$ ")") >> pair (d - 1)) ||
   262   Scan.lift (keep_line ($$ "*" --| Scan.ahead (~$$ ")"))) ||
   263   Scan.lift (keep_line (Scan.one (fn s =>
   264     s <> "*" andalso Symbol.not_sync s andalso Symbol.not_eof s)));
   265 
   266 val scan_comment =
   267   keep_line ($$ "(" -- $$ "*") |--
   268     !!! "missing end of comment"
   269       (change_prompt
   270         (Scan.pass 0 (Scan.repeat scan_cmt >> implode) --| keep_line ($$ "*" -- $$ ")")));
   271 
   272 
   273 (* scan token *)
   274 
   275 fun scan (lex1, lex2) =
   276   let
   277     val scanner = Scan.state :-- (fn pos =>
   278       let
   279         fun token k x = Token (pos, (k, x));
   280         fun sync _ = token Sync Symbol.sync;
   281       in
   282         scan_string >> token String ||
   283         scan_alt_string >> token AltString ||
   284         scan_verbatim >> token Verbatim ||
   285         scan_space >> token Space ||
   286         scan_comment >> token Comment ||
   287         keep_line (Scan.one Symbol.is_sync >> sync) ||
   288         keep_line (Scan.max token_leq
   289           (Scan.max token_leq
   290             (Scan.literal lex1 >> (token Keyword o implode))
   291             (Scan.literal lex2 >> (token Command o implode)))
   292           (Syntax.scan_longid >> token LongIdent ||
   293             Syntax.scan_id >> token Ident ||
   294             Syntax.scan_var >> token Var ||
   295             Syntax.scan_tid >> token TypeIdent ||
   296             Syntax.scan_tvar >> token TypeVar ||
   297             Syntax.scan_nat >> token Nat ||
   298             scan_symid >> token SymIdent))
   299       end) >> #2;
   300   in !! (lex_err (fn cs => "bad input " ^ quote (Symbol.beginning 10 cs))) scanner end;
   301 
   302 
   303 (* token sources *)
   304 
   305 val is_junk = (not o Symbol.is_blank) andf Symbol.not_sync andf Symbol.not_eof;
   306 fun recover xs = (keep_line (Scan.any is_junk) >> (fn ts => [malformed_of ts])) xs;
   307 
   308 fun source do_recover get_lex pos src =
   309   Source.source' pos Symbol.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
   310     (if do_recover then SOME recover else NONE) src;
   311 
   312 fun source_proper src = src |> Source.filter is_proper;
   313 
   314 
   315 (* lexicons *)
   316 
   317 val make_lexicon = Scan.make_lexicon o map Symbol.explode;
   318 
   319 end;