wneuper/isa: src/Pure/General/symbol.ML@9b00f09f7721

     1 (*  Title:      Pure/General/symbol.ML

     2     Author:     Markus Wenzel, TU Muenchen

     4 Generalized characters with infinitely many named symbols.

     5 *)

     7 signature SYMBOL =

     8 sig

     9   type symbol = string

    10   val STX: symbol

    11   val DEL: symbol

    12   val space: symbol

    13   val spaces: int -> string

    14   val is_char: symbol -> bool

    15   val is_utf8: symbol -> bool

    16   val is_symbolic: symbol -> bool

    17   val is_printable: symbol -> bool

    18   val eof: symbol

    19   val is_eof: symbol -> bool

    20   val not_eof: symbol -> bool

    21   val stopper: symbol Scan.stopper

    22   val sync: symbol

    23   val is_sync: symbol -> bool

    24   val is_regular: symbol -> bool

    25   val is_malformed: symbol -> bool

    26   val malformed_msg: symbol -> string

    27   val is_ascii: symbol -> bool

    28   val is_ascii_letter: symbol -> bool

    29   val is_ascii_digit: symbol -> bool

    30   val is_ascii_hex: symbol -> bool

    31   val is_ascii_quasi: symbol -> bool

    32   val is_ascii_blank: symbol -> bool

    33   val is_ascii_control: symbol -> bool

    34   val is_ascii_lower: symbol -> bool

    35   val is_ascii_upper: symbol -> bool

    36   val to_ascii_lower: symbol -> symbol

    37   val to_ascii_upper: symbol -> symbol

    38   val is_raw: symbol -> bool

    39   val decode_raw: symbol -> string

    40   val encode_raw: string -> string

    41   datatype sym =

    42     Char of string | UTF8 of string | Sym of string | Ctrl of string | Raw of string |

    43     Malformed of string | EOF

    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: (string, 'a) Source.source -> (symbol, (string, 'a) Source.source) Source.source

    58   val explode: string -> symbol list

    59   val esc: symbol -> string

    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   val output: string -> Output.output * int

    67 end;

    69 structure Symbol: SYMBOL =

    70 struct

    72 (** type symbol **)

    74 (*Symbols, which are considered the smallest entities of any Isabelle

    75   string, may be of the following form:

    77     (1) ASCII symbols: a

    78     (2) regular symbols: \<ident>

    79     (3) control symbols: \<^ident>

    80     (4) raw control symbols: \<^raw:...>, where "..." may be any printable

    81         character (excluding ".", ">"), or \<^raw000>

    83   Output is subject to the print_mode variable (default: verbatim),

    84   actual interpretation in display is up to front-end tools.

    85 *)

    87 type symbol = string;

    89 val STX = chr 2;

    90 val DEL = chr 127;

    92 val space = chr 32;

    94 local

    95   val small_spaces = Vector.tabulate (65, fn i => Library.replicate_string i space);

    96 in

    97   fun spaces k =

    98     if k < 64 then Vector.sub (small_spaces, k)

    99     else Library.replicate_string (k div 64) (Vector.sub (small_spaces, 64)) ^

   100       Vector.sub (small_spaces, k mod 64);

   101 end;

   103 fun is_char s = size s = 1;

   105 fun is_utf8 s = size s > 0 andalso forall_string (fn c => ord c >= 128) s;

   107 fun is_symbolic s =

   108   String.isPrefix "\\<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\\<^" s);

   110 fun is_printable s =

   111   if is_char s then ord space <= ord s andalso ord s <= ord "~"

   112   else is_utf8 s orelse is_symbolic s;

   115 (* input source control *)

   117 val eof = "";

   118 fun is_eof s = s = eof;

   119 fun not_eof s = s <> eof;

   120 val stopper = Scan.stopper (K eof) is_eof;

   122 val sync = "\\<^sync>";

   123 fun is_sync s = s = sync;

   125 fun is_regular s = not_eof s andalso s <> sync;

   127 fun is_malformed s = String.isPrefix "\\<" s andalso not (String.isSuffix ">" s);

   128 fun malformed_msg s = "Malformed symbolic character: " ^ quote s;

   131 (* ASCII symbols *)

   133 fun is_ascii s = is_char s andalso ord s < 128;

   135 fun is_ascii_letter s =

   136   is_char s andalso

   137    (ord "A" <= ord s andalso ord s <= ord "Z" orelse

   138     ord "a" <= ord s andalso ord s <= ord "z");

   140 fun is_ascii_digit s =

   141   is_char s andalso ord "0" <= ord s andalso ord s <= ord "9";

   143 fun is_ascii_hex s =

   144   is_char s andalso

   145    (ord "0" <= ord s andalso ord s <= ord "9" orelse

   146     ord "A" <= ord s andalso ord s <= ord "F" orelse

   147     ord "a" <= ord s andalso ord s <= ord "f");

   149 fun is_ascii_quasi "_" = true

   150   | is_ascii_quasi "'" = true

   151   | is_ascii_quasi _ = false;

   153 val is_ascii_blank =

   154   fn " " => true | "\t" => true | "\n" => true | "\^K" => true | "\f" => true | "\^M" => true

   155     | _ => false;

   157 fun is_ascii_control s = is_char s andalso ord s < 32 andalso not (is_ascii_blank s);

   159 fun is_ascii_lower s = is_char s andalso (ord "a" <= ord s andalso ord s <= ord "z");

   160 fun is_ascii_upper s = is_char s andalso (ord "A" <= ord s andalso ord s <= ord "Z");

   162 fun to_ascii_lower s = if is_ascii_upper s then chr (ord s + ord "a" - ord "A") else s;

   163 fun to_ascii_upper s = if is_ascii_lower s then chr (ord s + ord "A" - ord "a") else s;

   166 (* encode_raw *)

   168 fun raw_chr c =

   169   ord space <= ord c andalso ord c <= ord "~" andalso c <> "." andalso c <> ">"

   170   orelse ord c >= 128;

   172 fun encode_raw "" = ""

   173   | encode_raw str =

   174       let

   175         val raw0 = enclose "\\<^raw:" ">";

   176         val raw1 = raw0 o implode;

   177         val raw2 = enclose "\\<^raw" ">" o string_of_int o ord;

   179         fun encode cs = enc (take_prefix raw_chr cs)

   180         and enc ([], []) = []

   181           | enc (cs, []) = [raw1 cs]

   182           | enc ([], d :: ds) = raw2 d :: encode ds

   183           | enc (cs, d :: ds) = raw1 cs :: raw2 d :: encode ds;

   184       in

   185         if exists_string (not o raw_chr) str then implode (encode (raw_explode str))

   186         else raw0 str

   187       end;

   190 (* diagnostics *)

   192 fun beginning n cs =

   193   let

   194     val drop_blanks = #1 o take_suffix is_ascii_blank;

   195     val all_cs = drop_blanks cs;

   196     val dots = if length all_cs > n then " ..." else "";

   197   in

   198     (drop_blanks (take n all_cs)

   199       |> map (fn c => if is_ascii_blank c then space else c)

   200       |> implode) ^ dots

   201   end;

   204 (* decode_raw *)

   206 fun is_raw s =

   207   String.isPrefix "\\<^raw" s andalso String.isSuffix ">" s;

   209 fun decode_raw s =

   210   if not (is_raw s) then error (malformed_msg s)

   211   else if String.isPrefix "\\<^raw:" s then String.substring (s, 7, size s - 8)

   212   else chr (#1 (Library.read_int (raw_explode (String.substring (s, 6, size s - 7)))));

   215 (* symbol variants *)

   217 datatype sym =

   218   Char of string | UTF8 of string | Sym of string | Ctrl of string | Raw of string |

   219   Malformed of string | EOF;

   221 fun decode s =

   222   if s = "" then EOF

   223   else if is_char s then Char s

   224   else if is_utf8 s then UTF8 s

   225   else if is_raw s then Raw (decode_raw s)

   226   else if is_malformed s then Malformed s

   227   else if String.isPrefix "\\<^" s then Ctrl (String.substring (s, 3, size s - 4))

   228   else Sym (String.substring (s, 2, size s - 3));

   231 (* standard symbol kinds *)

   233 datatype kind = Letter | Digit | Quasi | Blank | Other;

   235 local

   236   val symbol_kinds = Symtab.make

   237    [("\\<A>", Letter),

   238     ("\\<B>", Letter),

   239     ("\\<C>", Letter),

   240     ("\\<D>", Letter),

   241     ("\\<E>", Letter),

   242     ("\\<F>", Letter),

   243     ("\\<G>", Letter),

   244     ("\\<H>", Letter),

   245     ("\\<I>", Letter),

   246     ("\\<J>", Letter),

   247     ("\\<K>", Letter),

   248     ("\\<L>", Letter),

   249     ("\\<M>", Letter),

   250     ("\\<N>", Letter),

   251     ("\\<O>", Letter),

   252     ("\\<P>", Letter),

   253     ("\\<Q>", Letter),

   254     ("\\<R>", Letter),

   255     ("\\<S>", Letter),

   256     ("\\<T>", Letter),

   257     ("\\<U>", Letter),

   258     ("\\<V>", Letter),

   259     ("\\<W>", Letter),

   260     ("\\<X>", Letter),

   261     ("\\<Y>", Letter),

   262     ("\\<Z>", Letter),

   263     ("\\<a>", Letter),

   264     ("\\<b>", Letter),

   265     ("\\<c>", Letter),

   266     ("\\<d>", Letter),

   267     ("\\<e>", Letter),

   268     ("\\<f>", Letter),

   269     ("\\<g>", Letter),

   270     ("\\<h>", Letter),

   271     ("\\<i>", Letter),

   272     ("\\<j>", Letter),

   273     ("\\<k>", Letter),

   274     ("\\<l>", Letter),

   275     ("\\<m>", Letter),

   276     ("\\<n>", Letter),

   277     ("\\<o>", Letter),

   278     ("\\<p>", Letter),

   279     ("\\<q>", Letter),

   280     ("\\<r>", Letter),

   281     ("\\<s>", Letter),

   282     ("\\<t>", Letter),

   283     ("\\<u>", Letter),

   284     ("\\<v>", Letter),

   285     ("\\<w>", Letter),

   286     ("\\<x>", Letter),

   287     ("\\<y>", Letter),

   288     ("\\<z>", Letter),

   289     ("\\<AA>", Letter),

   290     ("\\<BB>", Letter),

   291     ("\\<CC>", Letter),

   292     ("\\<DD>", Letter),

   293     ("\\<EE>", Letter),

   294     ("\\<FF>", Letter),

   295     ("\\<GG>", Letter),

   296     ("\\<HH>", Letter),

   297     ("\\<II>", Letter),

   298     ("\\<JJ>", Letter),

   299     ("\\<KK>", Letter),

   300     ("\\<LL>", Letter),

   301     ("\\<MM>", Letter),

   302     ("\\<NN>", Letter),

   303     ("\\<OO>", Letter),

   304     ("\\<PP>", Letter),

   305     ("\\<QQ>", Letter),

   306     ("\\<RR>", Letter),

   307     ("\\<SS>", Letter),

   308     ("\\<TT>", Letter),

   309     ("\\<UU>", Letter),

   310     ("\\<VV>", Letter),

   311     ("\\<WW>", Letter),

   312     ("\\<XX>", Letter),

   313     ("\\<YY>", Letter),

   314     ("\\<ZZ>", Letter),

   315     ("\\<aa>", Letter),

   316     ("\\<bb>", Letter),

   317     ("\\<cc>", Letter),

   318     ("\\<dd>", Letter),

   319     ("\\<ee>", Letter),

   320     ("\\<ff>", Letter),

   321     ("\\<gg>", Letter),

   322     ("\\<hh>", Letter),

   323     ("\\<ii>", Letter),

   324     ("\\<jj>", Letter),

   325     ("\\<kk>", Letter),

   326     ("\\<ll>", Letter),

   327     ("\\<mm>", Letter),

   328     ("\\<nn>", Letter),

   329     ("\\<oo>", Letter),

   330     ("\\<pp>", Letter),

   331     ("\\<qq>", Letter),

   332     ("\\<rr>", Letter),

   333     ("\\<ss>", Letter),

   334     ("\\<tt>", Letter),

   335     ("\\<uu>", Letter),

   336     ("\\<vv>", Letter),

   337     ("\\<ww>", Letter),

   338     ("\\<xx>", Letter),

   339     ("\\<yy>", Letter),

   340     ("\\<zz>", Letter),

   341     ("\\<alpha>", Letter),

   342     ("\\<beta>", Letter),

   343     ("\\<gamma>", Letter),

   344     ("\\<delta>", Letter),

   345     ("\\<epsilon>", Letter),

   346     ("\\<zeta>", Letter),

   347     ("\\<eta>", Letter),

   348     ("\\<theta>", Letter),

   349     ("\\<iota>", Letter),

   350     ("\\<kappa>", Letter),

   351     ("\\<lambda>", Other),      (*sic!*)

   352     ("\\<mu>", Letter),

   353     ("\\<nu>", Letter),

   354     ("\\<xi>", Letter),

   355     ("\\<pi>", Letter),

   356     ("\\<rho>", Letter),

   357     ("\\<sigma>", Letter),

   358     ("\\<tau>", Letter),

   359     ("\\<upsilon>", Letter),

   360     ("\\<phi>", Letter),

   361     ("\\<chi>", Letter),

   362     ("\\<psi>", Letter),

   363     ("\\<omega>", Letter),

   364     ("\\<Gamma>", Letter),

   365     ("\\<Delta>", Letter),

   366     ("\\<Theta>", Letter),

   367     ("\\<Lambda>", Letter),

   368     ("\\<Xi>", Letter),

   369     ("\\<Pi>", Letter),

   370     ("\\<Sigma>", Letter),

   371     ("\\<Upsilon>", Letter),

   372     ("\\<Phi>", Letter),

   373     ("\\<Psi>", Letter),

   374     ("\\<Omega>", Letter),

   375     ("\\<^isub>", Letter),

   376     ("\\<^isup>", Letter),

   377     ("\\<spacespace>", Blank)];

   378 in

   379   fun kind s =

   380     if is_ascii_letter s then Letter

   381     else if is_ascii_digit s then Digit

   382     else if is_ascii_quasi s then Quasi

   383     else if is_ascii_blank s then Blank

   384     else if is_char s then Other

   385     else the_default Other (Symtab.lookup symbol_kinds s);

   386 end;

   388 fun is_letter s = kind s = Letter;

   389 fun is_digit s = kind s = Digit;

   390 fun is_quasi s = kind s = Quasi;

   391 fun is_blank s = kind s = Blank;

   393 fun is_quasi_letter s = let val k = kind s in k = Letter orelse k = Quasi end;

   394 fun is_letdig s = let val k = kind s in k = Letter orelse k = Digit orelse k = Quasi end;

   396 fun is_ident [] = false

   397   | is_ident (c :: cs) = is_letter c andalso forall is_letdig cs;

   401 (** symbol input **)

   403 (* scanning through symbols *)

   405 fun scanner msg scan chs =

   406   let

   407     fun message (cs, NONE) = (fn () => msg ^ ": " ^ quote (beginning 10 cs))

   408       | message (cs, SOME msg') = (fn () => msg ^ ", " ^ msg' () ^ ": " ^ quote (beginning 10 cs));

   409     val fin_scan = Scan.error (Scan.finite stopper (!! message scan));

   410   in

   411     (case fin_scan chs of

   412       (result, []) => result

   413     | (_, rest) => error (message (rest, NONE) ()))

   414   end;

   416 val scan_id = Scan.one is_letter ^^ (Scan.many is_letdig >> implode);

   419 (* source *)

   421 local

   423 fun is_plain s = is_ascii s andalso s <> "\^M" andalso s <> "\\";

   425 fun is_utf8_trailer s = is_char s andalso 128 <= ord s andalso ord s < 192;

   427 fun implode_pseudo_utf8 (cs as ["\192", c]) =

   428       if ord c < 160 then chr (ord c - 128) else implode cs

   429   | implode_pseudo_utf8 cs = implode cs;

   431 val scan_encoded_newline =

   432   $$ "\^M" -- $$ "\n" >> K "\n" ||

   433   $$ "\^M" >> K "\n" ||

   434   Scan.this_string "\\<^newline>" >> K "\n";

   436 val scan_raw =

   437   Scan.this_string "raw:" ^^ (Scan.many raw_chr >> implode) ||

   438   Scan.this_string "raw" ^^ (Scan.many1 is_ascii_digit >> implode);

   440 val scan_total =

   441   Scan.one is_plain ||

   442   Scan.one is_utf8 ::: Scan.many is_utf8_trailer >> implode_pseudo_utf8 ||

   443   scan_encoded_newline ||

   444   ($$ "\\" ^^ $$ "<" ^^ (($$ "^" ^^ (scan_raw || scan_id) || scan_id) ^^ $$ ">")) ||

   445   Scan.this_string "\\<^" ||

   446   Scan.this_string "\\<" ||

   447   Scan.one not_eof;

   449 in

   451 fun source src = Source.source stopper (Scan.bulk scan_total) NONE src;

   453 end;

   456 (* explode *)

   458 local

   460 fun no_explode [] = true

   461   | no_explode ("\\" :: "<" :: _) = false

   462   | no_explode ("\^M" :: _) = false

   463   | no_explode (c :: cs) = is_ascii c andalso no_explode cs;

   465 in

   467 fun sym_explode str =

   468   let val chs = raw_explode str in

   469     if no_explode chs then chs

   470     else Source.exhaust (source (Source.of_list chs))

   471   end;

   473 end;

   476 (* escape *)

   478 val esc = fn s =>

   479   if is_char s then s

   480   else if is_utf8 s then translate_string (fn c => "\\" ^ string_of_int (ord c)) s

   481   else "\\" ^ s;

   483 val escape = implode o map esc o sym_explode;

   486 (* blanks *)

   488 fun strip_blanks s =

   489   sym_explode s

   490   |> take_prefix is_blank |> #2

   491   |> take_suffix is_blank |> #1

   492   |> implode;

   495 (* bump string -- treat as base 26 or base 1 numbers *)

   497 fun symbolic_end (_ :: "\\<^isub>" :: _) = true

   498   | symbolic_end (_ :: "\\<^isup>" :: _) = true

   499   | symbolic_end (s :: _) = is_symbolic s

   500   | symbolic_end [] = false;

   502 fun bump_init str =

   503   if symbolic_end (rev (sym_explode str)) then str ^ "'"

   504   else str ^ "a";

   506 fun bump_string str =

   507   let

   508     fun bump [] = ["a"]

   509       | bump ("z" :: ss) = "a" :: bump ss

   510       | bump (s :: ss) =

   511           if is_char s andalso ord "a" <= ord s andalso ord s < ord "z"

   512           then chr (ord s + 1) :: ss

   513           else "a" :: s :: ss;

   515     val (ss, qs) = apfst rev (take_suffix is_quasi (sym_explode str));

   516     val ss' = if symbolic_end ss then "'" :: ss else bump ss;

   517   in implode (rev ss' @ qs) end;

   521 (** symbol output **)

   523 (* length *)

   525 fun sym_len s =

   526   if not (is_printable s) then (0: int)

   527   else if String.isPrefix "\\<long" s then 2

   528   else if String.isPrefix "\\<Long" s then 2

   529   else if s = "\\<spacespace>" then 2

   530   else 1;

   532 fun sym_length ss = fold (fn s => fn n => sym_len s + n) ss 0;

   535 (* print mode *)

   537 val xsymbolsN = "xsymbols";

   539 fun output s = (s, sym_length (sym_explode s));

   542 (*final declarations of this structure!*)

   543 val explode = sym_explode;

   544 val length = sym_length;

   546 end;

author	wenzelm
	Sat, 23 Jul 2011 16:37:17 +0200
changeset 44818	9b00f09f7721
parent 44716	d89353d17f54
child 48721	c638127b4653
permissions	-rw-r--r--