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