(*  Title:      Pure/General/symbol.ML

     Author:     Markus Wenzel, TU Muenchen

 Generalized characters with infinitely many named symbols.

 *)

 signature SYMBOL =

 sig

   type symbol

   val SOH: symbol

   val STX: symbol

   val ENQ: symbol

   val ACK: symbol

   val DEL: symbol

   val space: symbol

   val spaces: int -> string

   val is_char: symbol -> bool

   val is_symbolic: symbol -> bool

   val is_printable: symbol -> bool

   val is_utf8_trailer: symbol -> bool

   val name_of: symbol -> string

   val eof: symbol

   val is_eof: symbol -> bool

   val not_eof: symbol -> bool

   val stopper: symbol Scan.stopper

   val sync: symbol

   val is_sync: symbol -> bool

   val malformed: symbol

   val end_malformed: symbol

   val separate_chars: string -> string

   val is_regular: symbol -> bool

   val is_ascii: symbol -> bool

   val is_ascii_letter: symbol -> bool

   val is_ascii_digit: symbol -> bool

   val is_ascii_hex: symbol -> bool

   val is_ascii_quasi: symbol -> bool

   val is_ascii_blank: symbol -> bool

   val is_ascii_lower: symbol -> bool

   val is_ascii_upper: symbol -> bool

   val to_ascii_lower: symbol -> symbol

   val to_ascii_upper: symbol -> symbol

   val is_raw: symbol -> bool

   val decode_raw: symbol -> string

   val encode_raw: string -> string

   datatype sym = Char of string | Sym of string | Ctrl of string | Raw of string

   val decode: symbol -> sym

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

   val kind: symbol -> kind

   val is_letter: symbol -> bool

   val is_digit: symbol -> bool

   val is_quasi: symbol -> bool

   val is_blank: symbol -> bool

   val is_quasi_letter: symbol -> bool

   val is_letdig: symbol -> bool

   val is_ident: symbol list -> bool

   val beginning: int -> symbol list -> string

   val scanner: string -> (string list -> 'a * string list) -> symbol list -> 'a

   val scan_id: string list -> string * string list

   val source: {do_recover: bool} -> (string, 'a) Source.source ->

     (symbol, (string, 'a) Source.source) Source.source

   val explode: string -> symbol list

   val escape: string -> string

   val strip_blanks: string -> string

   val bump_init: string -> string

   val bump_string: string -> string

   val length: symbol list -> int

   val xsymbolsN: string

   val output: string -> output * int

 end;

 structure Symbol: SYMBOL =

 struct

 (** type symbol **)

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

   string, may be of the following form:

     (1) ASCII symbols: a

     (2) regular symbols: \<ident>

     (3) control symbols: \<^ident>

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

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

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

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

 *)

 type symbol = string;

 val SOH = chr 1;

 val STX = chr 2;

 val ENQ = chr 5;

 val ACK = chr 6;

 val DEL = chr 127;

 val space = chr 32;

 local

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

 in

   fun spaces k =

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

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

       Vector.sub (small_spaces, k mod 64);

 end;

 fun is_char s = size s = 1;

 fun is_symbolic s =

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

 fun is_printable s =

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

   else not (String.isPrefix "\\<^" s);

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

 (* input source control *)

 val eof = "";

 fun is_eof s = s = eof;

 fun not_eof s = s <> eof;

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

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

 fun is_sync s = s = sync;

 val malformed = "[[";

 val end_malformed = "]]";

 val separate_chars = explode #> space_implode space;

 fun malformed_msg s = "Malformed symbolic character: " ^ quote (separate_chars s);

 fun is_regular s =

   not_eof s andalso s <> sync andalso s <> malformed andalso s <> end_malformed;

 fun name_of s = if is_symbolic s

   then (unsuffix ">" o unprefix "\\<") s

   else error (malformed_msg s);

 (* ascii symbols *)

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

 fun is_ascii_letter s =

   is_char s andalso

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

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

 fun is_ascii_digit s =

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

 fun is_ascii_hex s =

   is_char s andalso

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

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

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

 fun is_ascii_quasi "_" = true

   | is_ascii_quasi "'" = true

   | is_ascii_quasi _ = false;

 val is_ascii_blank =

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

     | _ => false;

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

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

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

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

 (* encode_raw *)

 fun raw_chr c =

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

   orelse ord c >= 128;

 fun encode_raw "" = ""

   | encode_raw str =

       let

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

         val raw1 = raw0 o implode;

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

         fun encode cs = enc (Library.take_prefix raw_chr cs)

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

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

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

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

       in

         if exists_string (not o raw_chr) str then implode (encode (explode str))

         else raw0 str

       end;

 (* diagnostics *)

 fun beginning n cs =

   let

     val drop_blanks = #1 o Library.take_suffix is_ascii_blank;

     val all_cs = drop_blanks cs;

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

   in

     (drop_blanks (Library.take (n, all_cs))

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

       |> implode) ^ dots

   end;

 (* decode_raw *)

 fun is_raw s =

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

 fun decode_raw s =

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

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

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

 (* symbol variants *)

 datatype sym = Char of string | Sym of string | Ctrl of string | Raw of string;

 fun decode s =

   if is_char s then Char s

   else if is_raw s then Raw (decode_raw s)

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

   else if String.isPrefix "\\<" s then Sym (String.substring (s, 2, size s - 3))

   else error (malformed_msg s);

 (* standard symbol kinds *)

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

 local

   val symbol_kinds = Symtab.make

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 in

   fun kind s =

     if is_ascii_letter s then Letter

     else if is_ascii_digit s then Digit

     else if is_ascii_quasi s then Quasi

     else if is_ascii_blank s then Blank

     else if is_char s then Other

     else the_default Other (Symtab.lookup symbol_kinds s);

 end;

 fun is_letter s = kind s = Letter;

 fun is_digit s = kind s = Digit;

 fun is_quasi s = kind s = Quasi;

 fun is_blank s = kind s = Blank;

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

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

 fun is_ident [] = false

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

 (** symbol input **)

 (* scanning through symbols *)

 fun scanner msg scan chs =

   let

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

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

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

   in

     (case fin_scan chs of

       (result, []) => result

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

   end;

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

 (* source *)

 local

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

 val scan_encoded_newline =

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

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

   $$ "\\" -- Scan.optional ($$ "\\") "" -- Scan.this_string "<^newline>" >> K "\n";

 val scan_raw =

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

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

 val scan =

   Scan.one is_plain ||

   scan_encoded_newline ||

   (($$ "\\" --| Scan.optional ($$ "\\") "") ^^ $$ "<" ^^

     !! (fn (cs, _) => malformed_msg (beginning 10 ("\\" :: "<" :: cs)))

       (($$ "^" ^^ (scan_raw || scan_id) || scan_id) ^^ $$ ">")) ||

   Scan.one not_eof;

 val scan_resync =

   Scan.one is_ascii_blank || $$ "\"" || $$ "`" || $$ "\\" ||

   Scan.this_string "(*" || Scan.this_string "*)" ||

   Scan.this_string "{*" || Scan.this_string "*}";

 val recover =

   (Scan.this (explode "\\\\<") || Scan.this (explode "\\<")) @@@

     Scan.repeat (Scan.unless scan_resync (Scan.one not_eof))

   >> (fn ss => malformed :: ss @ [end_malformed]);

 in

 fun source {do_recover} src =

   Source.source stopper (Scan.bulk scan)

     (if do_recover then SOME (false, K recover) else NONE) src;

 end;

 (* explode *)

 local

 fun no_explode [] = true

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

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

   | no_explode (_ :: cs) = no_explode cs;

 in

 fun sym_explode str =

   let val chs = explode str in

     if no_explode chs then chs

     else Source.exhaust (source {do_recover = false} (Source.of_list chs))

   end;

 end;

 (* escape *)

 val escape = implode o map (fn s => if is_char s then s else "\\" ^ s) o sym_explode;

 (* blanks *)

 fun strip_blanks s =

   sym_explode s

   |> Library.take_prefix is_blank |> #2

   |> Library.take_suffix is_blank |> #1

   |> implode;

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

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

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

   | symbolic_end (s :: _) = is_symbolic s

   | symbolic_end [] = false;

 fun bump_init str =

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

   else str ^ "a";

 fun bump_string str =

   let

     fun bump [] = ["a"]

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

       | bump (s :: ss) =

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

           then chr (ord s + 1) :: ss

           else "a" :: s :: ss;

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

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

   in implode (rev ss' @ qs) end;

 (** symbol output **)

 (* length *)

 fun sym_len s =

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

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

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

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

   else 1;

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

 (* print mode *)

 val xsymbolsN = "xsymbols";

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

 (*final declarations of this structure!*)

 val explode = sym_explode;

 val length = sym_length;

 end;