src/Pure/General/symbol.ML
author wenzelm
Thu Apr 03 18:42:36 2008 +0200 (2008-04-03)
changeset 26538 d65504ffb47d
parent 26524 63953bec4c98
child 26632 90c0b075c0d3
permissions -rw-r--r--
replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
     1 (*  Title:      Pure/General/symbol.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Generalized characters with infinitely many named symbols.
     6 *)
     7 
     8 signature SYMBOL =
     9 sig
    10   type symbol
    11   val SOH: symbol
    12   val STX: symbol
    13   val ENQ: symbol
    14   val ACK: symbol
    15   val DEL: symbol
    16   val space: symbol
    17   val spaces: int -> string
    18   val is_char: symbol -> bool
    19   val is_symbolic: symbol -> bool
    20   val is_printable: symbol -> bool
    21   val eof: symbol
    22   val is_eof: symbol -> bool
    23   val stopper: symbol * (symbol -> bool)
    24   val sync: symbol
    25   val is_sync: symbol -> bool
    26   val malformed: symbol
    27   val end_malformed: symbol
    28   val separate_chars: string -> string
    29   val is_regular: symbol -> bool
    30   val is_ascii: symbol -> bool
    31   val is_ascii_letter: symbol -> bool
    32   val is_ascii_digit: symbol -> bool
    33   val is_ascii_hex: symbol -> bool
    34   val is_ascii_quasi: symbol -> bool
    35   val is_ascii_blank: symbol -> bool
    36   val is_ascii_lower: symbol -> bool
    37   val is_ascii_upper: symbol -> bool
    38   val to_ascii_lower: symbol -> symbol
    39   val to_ascii_upper: symbol -> symbol
    40   val is_raw: symbol -> bool
    41   val decode_raw: symbol -> string
    42   val encode_raw: string -> string
    43   datatype sym = Char of string | Sym of string | Ctrl of string | Raw of string
    44   val decode: symbol -> sym
    45   datatype kind = Letter | Digit | Quasi | Blank | Other
    46   val kind: symbol -> kind
    47   val is_letter: symbol -> bool
    48   val is_digit: symbol -> bool
    49   val is_quasi: symbol -> bool
    50   val is_blank: symbol -> bool
    51   val is_quasi_letter: symbol -> bool
    52   val is_letdig: symbol -> bool
    53   val is_ident: symbol list -> bool
    54   val beginning: int -> symbol list -> string
    55   val scanner: string -> (string list -> 'a * string list) -> symbol list -> 'a
    56   val scan_id: string list -> string * string list
    57   val source: bool -> (string, 'a) Source.source ->
    58     (symbol, (string, 'a) Source.source) Source.source
    59   val explode: string -> symbol list
    60   val escape: string -> string
    61   val strip_blanks: string -> string
    62   val bump_init: string -> string
    63   val bump_string: string -> string
    64   val length: symbol list -> int
    65   val xsymbolsN: string
    66 end;
    67 
    68 structure Symbol: SYMBOL =
    69 struct
    70 
    71 (** type symbol **)
    72 
    73 (*Symbols, which are considered the smallest entities of any Isabelle
    74   string, may be of the following form:
    75 
    76     (1) ASCII symbols: a
    77     (2) regular symbols: \<ident>
    78     (3) control symbols: \<^ident>
    79     (4) raw control symbols: \<^raw:...>, where "..." may be any printable
    80         character (excluding ".", ">"), or \<^raw000>
    81 
    82   Output is subject to the print_mode variable (default: verbatim),
    83   actual interpretation in display is up to front-end tools.
    84 *)
    85 
    86 type symbol = string;
    87 
    88 val SOH = chr 1;
    89 val STX = chr 2;
    90 val ENQ = chr 5;
    91 val ACK = chr 6;
    92 val DEL = chr 127;
    93 
    94 val space = chr 32;
    95 
    96 local
    97   val small_spaces = Vector.tabulate (65, fn i => Library.replicate_string i space);
    98 in
    99   fun spaces k =
   100     if k < 64 then Vector.sub (small_spaces, k)
   101     else Library.replicate_string (k div 64) (Vector.sub (small_spaces, 64)) ^
   102       Vector.sub (small_spaces, k mod 64);
   103 end;
   104 
   105 fun is_char s = size s = 1;
   106 
   107 fun is_symbolic s =
   108   String.isPrefix "\\<" s andalso not (String.isPrefix "\\<^" s);
   109 
   110 fun is_printable s =
   111   if is_char s then ord space <= ord s andalso ord s <= ord "~"
   112   else not (String.isPrefix "\\<^" s);
   113 
   114 
   115 (* input source control *)
   116 
   117 val eof = "";
   118 fun is_eof s = s = eof;
   119 fun not_eof s = s <> eof;
   120 val stopper = (eof, is_eof);
   121 
   122 val sync = "\\<^sync>";
   123 fun is_sync s = s = sync;
   124 
   125 val malformed = "[[";
   126 val end_malformed = "]]";
   127 
   128 val separate_chars = explode #> space_implode space;
   129 fun malformed_msg s = "Malformed symbolic character: " ^ quote (separate_chars s);
   130 
   131 fun is_regular s =
   132   not_eof s andalso s <> sync andalso s <> malformed andalso s <> end_malformed;
   133 
   134 
   135 (* ascii symbols *)
   136 
   137 fun is_ascii s = is_char s andalso ord s < 128;
   138 
   139 fun is_ascii_letter s =
   140   is_char s andalso
   141    (ord "A" <= ord s andalso ord s <= ord "Z" orelse
   142     ord "a" <= ord s andalso ord s <= ord "z");
   143 
   144 fun is_ascii_digit s =
   145   is_char s andalso ord "0" <= ord s andalso ord s <= ord "9";
   146 
   147 fun is_ascii_hex s =
   148   is_char s andalso
   149    (ord "0" <= ord s andalso ord s <= ord "9" orelse
   150     ord "A" <= ord s andalso ord s <= ord "F" orelse
   151     ord "a" <= ord s andalso ord s <= ord "f");
   152 
   153 fun is_ascii_quasi "_" = true
   154   | is_ascii_quasi "'" = true
   155   | is_ascii_quasi _ = false;
   156 
   157 val is_ascii_blank =
   158   fn " " => true | "\t" => true | "\n" => true | "\^K" => true | "\^L" => true | "\^M" => true
   159     | _ => false;
   160 
   161 fun is_ascii_lower s = is_char s andalso (ord "a" <= ord s andalso ord s <= ord "z");
   162 fun is_ascii_upper s = is_char s andalso (ord "A" <= ord s andalso ord s <= ord "Z");
   163 
   164 fun to_ascii_lower s = if is_ascii_upper s then chr (ord s + ord "a" - ord "A") else s;
   165 fun to_ascii_upper s = if is_ascii_lower s then chr (ord s + ord "A" - ord "a") else s;
   166 
   167 
   168 (* encode_raw *)
   169 
   170 fun raw_chr c =
   171   ord space <= ord c andalso ord c <= ord "~" andalso c <> "." andalso c <> ">"
   172   orelse ord c >= 128;
   173 
   174 fun encode_raw str =
   175   let
   176     val raw0 = enclose "\\<^raw:" ">";
   177     val raw1 = raw0 o implode;
   178     val raw2 = enclose "\\<^raw" ">" o string_of_int o ord;
   179 
   180     fun encode cs = enc (Library.take_prefix raw_chr cs)
   181     and enc ([], []) = []
   182       | enc (cs, []) = [raw1 cs]
   183       | enc ([], d :: ds) = raw2 d :: encode ds
   184       | enc (cs, d :: ds) = raw1 cs :: raw2 d :: encode ds;
   185   in
   186     if exists_string (not o raw_chr) str then implode (encode (explode str))
   187     else raw0 str
   188   end;
   189 
   190 
   191 (* diagnostics *)
   192 
   193 fun beginning n cs =
   194   let
   195     val drop_blanks = #1 o Library.take_suffix is_ascii_blank;
   196     val all_cs = drop_blanks cs;
   197     val dots = if length all_cs > n then " ..." else "";
   198   in
   199     (drop_blanks (Library.take (n, all_cs))
   200       |> map (fn c => if is_ascii_blank c then space else c)
   201       |> implode) ^ dots
   202   end;
   203 
   204 
   205 (* decode_raw *)
   206 
   207 fun is_raw s =
   208   String.isPrefix "\\<^raw" s andalso String.isSuffix ">" s;
   209 
   210 fun decode_raw s =
   211   if not (is_raw s) then error (malformed_msg s)
   212   else if String.isPrefix "\\<^raw:" s then String.substring (s, 7, size s - 8)
   213   else chr (#1 (Library.read_int (explode (String.substring (s, 6, size s - 7)))));
   214 
   215 
   216 (* symbol variants *)
   217 
   218 datatype sym = Char of string | Sym of string | Ctrl of string | Raw of string;
   219 
   220 fun decode s =
   221   if is_char s then Char s
   222   else if is_raw s then Raw (decode_raw s)
   223   else if String.isPrefix "\\<^" s then Ctrl (String.substring (s, 3, size s - 4))
   224   else if String.isPrefix "\\<" s then Sym (String.substring (s, 2, size s - 3))
   225   else error (malformed_msg s);
   226 
   227 
   228 (* standard symbol kinds *)
   229 
   230 datatype kind = Letter | Digit | Quasi | Blank | Other;
   231 
   232 local
   233   val symbol_kinds = Symtab.make
   234    [("\\<A>", Letter),
   235     ("\\<B>", Letter),
   236     ("\\<C>", Letter),
   237     ("\\<D>", Letter),
   238     ("\\<E>", Letter),
   239     ("\\<F>", Letter),
   240     ("\\<G>", Letter),
   241     ("\\<H>", Letter),
   242     ("\\<I>", Letter),
   243     ("\\<J>", Letter),
   244     ("\\<K>", Letter),
   245     ("\\<L>", Letter),
   246     ("\\<M>", Letter),
   247     ("\\<N>", Letter),
   248     ("\\<O>", Letter),
   249     ("\\<P>", Letter),
   250     ("\\<Q>", Letter),
   251     ("\\<R>", Letter),
   252     ("\\<S>", Letter),
   253     ("\\<T>", Letter),
   254     ("\\<U>", Letter),
   255     ("\\<V>", Letter),
   256     ("\\<W>", Letter),
   257     ("\\<X>", Letter),
   258     ("\\<Y>", Letter),
   259     ("\\<Z>", Letter),
   260     ("\\<a>", Letter),
   261     ("\\<b>", Letter),
   262     ("\\<c>", Letter),
   263     ("\\<d>", Letter),
   264     ("\\<e>", Letter),
   265     ("\\<f>", Letter),
   266     ("\\<g>", Letter),
   267     ("\\<h>", Letter),
   268     ("\\<i>", Letter),
   269     ("\\<j>", Letter),
   270     ("\\<k>", Letter),
   271     ("\\<l>", Letter),
   272     ("\\<m>", Letter),
   273     ("\\<n>", Letter),
   274     ("\\<o>", Letter),
   275     ("\\<p>", Letter),
   276     ("\\<q>", Letter),
   277     ("\\<r>", Letter),
   278     ("\\<s>", Letter),
   279     ("\\<t>", Letter),
   280     ("\\<u>", Letter),
   281     ("\\<v>", Letter),
   282     ("\\<w>", Letter),
   283     ("\\<x>", Letter),
   284     ("\\<y>", Letter),
   285     ("\\<z>", Letter),
   286     ("\\<AA>", Letter),
   287     ("\\<BB>", Letter),
   288     ("\\<CC>", Letter),
   289     ("\\<DD>", Letter),
   290     ("\\<EE>", Letter),
   291     ("\\<FF>", Letter),
   292     ("\\<GG>", Letter),
   293     ("\\<HH>", Letter),
   294     ("\\<II>", Letter),
   295     ("\\<JJ>", Letter),
   296     ("\\<KK>", Letter),
   297     ("\\<LL>", Letter),
   298     ("\\<MM>", Letter),
   299     ("\\<NN>", Letter),
   300     ("\\<OO>", Letter),
   301     ("\\<PP>", Letter),
   302     ("\\<QQ>", Letter),
   303     ("\\<RR>", Letter),
   304     ("\\<SS>", Letter),
   305     ("\\<TT>", Letter),
   306     ("\\<UU>", Letter),
   307     ("\\<VV>", Letter),
   308     ("\\<WW>", Letter),
   309     ("\\<XX>", Letter),
   310     ("\\<YY>", Letter),
   311     ("\\<ZZ>", Letter),
   312     ("\\<aa>", Letter),
   313     ("\\<bb>", Letter),
   314     ("\\<cc>", Letter),
   315     ("\\<dd>", Letter),
   316     ("\\<ee>", Letter),
   317     ("\\<ff>", Letter),
   318     ("\\<gg>", Letter),
   319     ("\\<hh>", Letter),
   320     ("\\<ii>", Letter),
   321     ("\\<jj>", Letter),
   322     ("\\<kk>", Letter),
   323     ("\\<ll>", Letter),
   324     ("\\<mm>", Letter),
   325     ("\\<nn>", Letter),
   326     ("\\<oo>", Letter),
   327     ("\\<pp>", Letter),
   328     ("\\<qq>", Letter),
   329     ("\\<rr>", Letter),
   330     ("\\<ss>", Letter),
   331     ("\\<tt>", Letter),
   332     ("\\<uu>", Letter),
   333     ("\\<vv>", Letter),
   334     ("\\<ww>", Letter),
   335     ("\\<xx>", Letter),
   336     ("\\<yy>", Letter),
   337     ("\\<zz>", Letter),
   338     ("\\<alpha>", Letter),
   339     ("\\<beta>", Letter),
   340     ("\\<gamma>", Letter),
   341     ("\\<delta>", Letter),
   342     ("\\<epsilon>", Letter),
   343     ("\\<zeta>", Letter),
   344     ("\\<eta>", Letter),
   345     ("\\<theta>", Letter),
   346     ("\\<iota>", Letter),
   347     ("\\<kappa>", Letter),
   348     ("\\<lambda>", Other),      (*sic!*)
   349     ("\\<mu>", Letter),
   350     ("\\<nu>", Letter),
   351     ("\\<xi>", Letter),
   352     ("\\<pi>", Letter),
   353     ("\\<rho>", Letter),
   354     ("\\<sigma>", Letter),
   355     ("\\<tau>", Letter),
   356     ("\\<upsilon>", Letter),
   357     ("\\<phi>", Letter),
   358     ("\\<chi>", Letter),
   359     ("\\<psi>", Letter),
   360     ("\\<omega>", Letter),
   361     ("\\<Gamma>", Letter),
   362     ("\\<Delta>", Letter),
   363     ("\\<Theta>", Letter),
   364     ("\\<Lambda>", Letter),
   365     ("\\<Xi>", Letter),
   366     ("\\<Pi>", Letter),
   367     ("\\<Sigma>", Letter),
   368     ("\\<Upsilon>", Letter),
   369     ("\\<Phi>", Letter),
   370     ("\\<Psi>", Letter),
   371     ("\\<Omega>", Letter),
   372     ("\\<^isub>", Letter),
   373     ("\\<^isup>", Letter),
   374     ("\\<spacespace>", Blank)];
   375 in
   376   fun kind s =
   377     if is_ascii_letter s then Letter
   378     else if is_ascii_digit s then Digit
   379     else if is_ascii_quasi s then Quasi
   380     else if is_ascii_blank s then Blank
   381     else if is_char s then Other
   382     else the_default Other (Symtab.lookup symbol_kinds s);
   383 end;
   384 
   385 fun is_letter s = kind s = Letter;
   386 fun is_digit s = kind s = Digit;
   387 fun is_quasi s = kind s = Quasi;
   388 fun is_blank s = kind s = Blank;
   389 
   390 fun is_quasi_letter s = let val k = kind s in k = Letter orelse k = Quasi end;
   391 fun is_letdig s = let val k = kind s in k = Letter orelse k = Digit orelse k = Quasi end;
   392 
   393 fun is_ident [] = false
   394   | is_ident (c :: cs) = is_letter c andalso forall is_letdig cs;
   395 
   396 
   397 
   398 (** symbol input **)
   399 
   400 (* scanning through symbols *)
   401 
   402 fun scanner msg scan chs =
   403   let
   404     fun message (cs, NONE) = msg ^ ": " ^ quote (beginning 10 cs)
   405       | message (cs, SOME msg') = msg ^ ", " ^ msg' ^ ": " ^ quote (beginning 10 cs);
   406     val fin_scan = Scan.error (Scan.finite stopper (!! message scan));
   407   in
   408     (case fin_scan chs of
   409       (result, []) => result
   410     | (_, rest) => error (message (rest, NONE)))
   411   end;
   412 
   413 val scan_id = Scan.one is_letter ^^ (Scan.many is_letdig >> implode);
   414 
   415 
   416 (* source *)
   417 
   418 local
   419 
   420 fun is_plain s = s <> "\^M" andalso s <> "\\" andalso not_eof s;
   421 
   422 val scan_encoded_newline =
   423   $$ "\^M" -- $$ "\n" >> K "\n" ||
   424   $$ "\^M" >> K "\n" ||
   425   $$ "\\" -- Scan.optional ($$ "\\") "" -- Scan.this_string "<^newline>" >> K "\n";
   426 
   427 val scan_raw =
   428   Scan.this_string "raw:" ^^ (Scan.many raw_chr >> implode) ||
   429   Scan.this_string "raw" ^^ (Scan.many1 is_ascii_digit >> implode);
   430 
   431 val scan =
   432   Scan.one is_plain ||
   433   scan_encoded_newline ||
   434   (($$ "\\" --| Scan.optional ($$ "\\") "") ^^ $$ "<" ^^
   435     !! (fn (cs, _) => malformed_msg (beginning 10 ("\\" :: "<" :: cs)))
   436       (($$ "^" ^^ (scan_raw || scan_id) || scan_id) ^^ $$ ">")) ||
   437   Scan.one not_eof;
   438 
   439 val recover =
   440   Scan.many (fn s => not (is_blank s) andalso s <> "\"" andalso s <> "`" andalso not_eof s)
   441     >> (fn ss => malformed :: ss @ [end_malformed]);
   442 
   443 in
   444 
   445 fun source do_recover src =
   446   Source.source stopper (Scan.bulk scan)
   447     (if do_recover then SOME (false, K recover) else NONE) src;
   448 
   449 end;
   450 
   451 
   452 (* explode *)
   453 
   454 local
   455 
   456 fun no_explode [] = true
   457   | no_explode ("\\" :: "<" :: _) = false
   458   | no_explode ("\^M" :: _) = false
   459   | no_explode (_ :: cs) = no_explode cs;
   460 
   461 in
   462 
   463 fun sym_explode str =
   464   let val chs = explode str in
   465     if no_explode chs then chs
   466     else Source.exhaust (source false (Source.of_list chs))
   467   end;
   468 
   469 end;
   470 
   471 
   472 (* escape *)
   473 
   474 val escape = implode o map (fn s => if is_char s then s else "\\" ^ s) o sym_explode;
   475 
   476 
   477 (* blanks *)
   478 
   479 fun strip_blanks s =
   480   sym_explode s
   481   |> Library.take_prefix is_blank |> #2
   482   |> Library.take_suffix is_blank |> #1
   483   |> implode;
   484 
   485 
   486 (* bump string -- treat as base 26 or base 1 numbers *)
   487 
   488 fun symbolic_end (_ :: "\\<^isub>" :: _) = true
   489   | symbolic_end (_ :: "\\<^isup>" :: _) = true
   490   | symbolic_end (s :: _) = is_symbolic s
   491   | symbolic_end [] = false;
   492 
   493 fun bump_init str =
   494   if symbolic_end (rev (sym_explode str)) then str ^ "'"
   495   else str ^ "a";
   496 
   497 fun bump_string str =
   498   let
   499     fun bump [] = ["a"]
   500       | bump ("z" :: ss) = "a" :: bump ss
   501       | bump (s :: ss) =
   502           if is_char s andalso ord "a" <= ord s andalso ord s < ord "z"
   503           then chr (ord s + 1) :: ss
   504           else "a" :: s :: ss;
   505 
   506     val (ss, qs) = apfst rev (Library.take_suffix is_quasi (sym_explode str));
   507     val ss' = if symbolic_end ss then "'" :: ss else bump ss;
   508   in implode (rev ss' @ qs) end;
   509 
   510 
   511 
   512 (** xsymbols **)
   513 
   514 val xsymbolsN = "xsymbols";
   515 
   516 fun sym_len s =
   517   if not (is_printable s) then (0: int)
   518   else if String.isPrefix "\\<long" s then 2
   519   else if String.isPrefix "\\<Long" s then 2
   520   else if s = "\\<spacespace>" then 2
   521   else 1;
   522 
   523 fun sym_length ss = fold (fn s => fn n => sym_len s + n) ss 0;
   524 
   525 (*final declarations of this structure!*)
   526 val length = sym_length;
   527 val explode = sym_explode;
   528 
   529 end;