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