src/Pure/General/symbol.ML

more robust persistent storage;
tuned;

(*  Title:      Pure/General/symbol.ML
    Author:     Markus Wenzel, TU Muenchen

Generalized characters with infinitely many named symbols.
*)

signature SYMBOL =
sig
  type symbol = string
  val spaces: int -> string
  val STX: symbol
  val DEL: symbol
  val open_: symbol
  val close: symbol
  val space: symbol
  val is_space: symbol -> bool
  val comment: symbol
  val is_char: symbol -> bool
  val is_utf8: symbol -> bool
  val is_symbolic: symbol -> bool
  val is_symbolic_char: symbol -> bool
  val is_printable: symbol -> bool
  val is_control: symbol -> bool
  val eof: symbol
  val is_eof: symbol -> bool
  val not_eof: symbol -> bool
  val stopper: symbol Scan.stopper
  val is_malformed: symbol -> bool
  val malformed_msg: symbol -> string
  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_control: symbol -> bool
  val is_ascii_letdig: 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_ascii_identifier: string -> bool
  val scan_ascii_id: string list -> string * string list
  val is_raw: symbol -> bool
  val decode_raw: symbol -> string
  val encode_raw: string -> string
  datatype sym =
    Char of string | UTF8 of string | Sym of string | Control of string | Raw of string |
    Malformed of string | EOF
  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_block_ctrl: symbol -> bool
  val is_quasi_letter: symbol -> bool
  val is_letdig: symbol -> bool
  val beginning: int -> symbol list -> string
  val source: (string, 'a) Source.source -> (symbol, (string, 'a) Source.source) Source.source
  val explode: string -> symbol list
  val esc: symbol -> string
  val escape: string -> string
  val scanner: string -> (string list -> 'a * string list) -> symbol list -> 'a
  val split_words: symbol list -> string list
  val explode_words: string -> string list
  val trim_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.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 STX = chr 2;
val DEL = chr 127;

val open_ = "\<open>";
val close = "\<close>";

val space = chr 32;
fun is_space s = s = space;

local
  val small_spaces = Vector.tabulate (65, fn i => replicate_string i space);
in
  fun spaces n =
    if n < 64 then Vector.sub (small_spaces, n)
    else
      replicate_string (n div 64) (Vector.sub (small_spaces, 64)) ^
        Vector.sub (small_spaces, n mod 64);
end;

val comment = "\<comment>";

fun is_char s = size s = 1;

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

fun raw_symbolic s =
  String.isPrefix "\092<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\092<^" s);

fun is_symbolic s =
  s <> open_ andalso s <> close andalso raw_symbolic s;

val is_symbolic_char = member (op =) (raw_explode "!#$%&*+-/<=>?@^_|~");

fun is_printable s =
  if is_char s then ord space <= ord s andalso ord s <= ord "~"
  else is_utf8 s orelse raw_symbolic s;

fun is_control s =
  String.isPrefix "\092<^" s andalso String.isSuffix ">" s;


(* 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;

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

fun malformed_msg s = "Malformed symbolic character: " ^ quote 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 | "\f" => true | "\^M" => true
    | _ => false;

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

fun is_ascii_letdig s = is_ascii_letter s orelse is_ascii_digit s orelse is_ascii_quasi s;

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;

fun is_ascii_identifier s =
  size s > 0 andalso is_ascii_letter (String.substring (s, 0, 1)) andalso
  forall_string is_ascii_letdig s;

val scan_ascii_id = Scan.one is_ascii_letter ^^ (Scan.many is_ascii_letdig >> implode);


(* encode_raw *)

fun raw_chr c =
  is_char c andalso
    (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 "\092<^raw:" ">";
        val raw1 = raw0 o implode;
        val raw2 = enclose "\092<^raw" ">" o string_of_int o ord;

        fun encode cs = enc (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 (raw_explode str))
        else raw0 str
      end;


(* diagnostics *)

fun beginning n cs =
  let
    val drop_blanks = #1 o take_suffix is_ascii_blank;
    val all_cs = drop_blanks cs;
    val dots = if length all_cs > n then " ..." else "";
  in
    (drop_blanks (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 "\092<^raw" s andalso String.isSuffix ">" s;

fun decode_raw s =
  if not (is_raw s) then error (malformed_msg s)
  else if String.isPrefix "\092<^raw:" s then String.substring (s, 7, size s - 8)
  else chr (#1 (Library.read_int (raw_explode (String.substring (s, 6, size s - 7)))));


(* symbol variants *)

datatype sym =
  Char of string | UTF8 of string | Sym of string | Control of string | Raw of string |
  Malformed of string | EOF;

fun decode s =
  if s = "" then EOF
  else if is_char s then Char s
  else if is_utf8 s then UTF8 s
  else if is_raw s then Raw (decode_raw s)
  else if is_malformed s then Malformed s
  else if is_control s then Control (String.substring (s, 3, size s - 4))
  else Sym (String.substring (s, 2, size s - 3));


(* standard symbol kinds *)

local
  val letter_symbols =
    Symtab.make_set [
      "\<A>",
      "\<B>",
      "\<C>",
      "\<D>",
      "\<E>",
      "\<F>",
      "\<G>",
      "\<H>",
      "\<I>",
      "\<J>",
      "\<K>",
      "\<L>",
      "\<M>",
      "\<N>",
      "\<O>",
      "\<P>",
      "\<Q>",
      "\<R>",
      "\<S>",
      "\<T>",
      "\<U>",
      "\<V>",
      "\<W>",
      "\<X>",
      "\<Y>",
      "\<Z>",
      "\<a>",
      "\<b>",
      "\<c>",
      "\<d>",
      "\<e>",
      "\<f>",
      "\<g>",
      "\<h>",
      "\<i>",
      "\<j>",
      "\<k>",
      "\<l>",
      "\<m>",
      "\<n>",
      "\<o>",
      "\<p>",
      "\<q>",
      "\<r>",
      "\<s>",
      "\<t>",
      "\<u>",
      "\<v>",
      "\<w>",
      "\<x>",
      "\<y>",
      "\<z>",
      "\<AA>",
      "\<BB>",
      "\<CC>",
      "\<DD>",
      "\<EE>",
      "\<FF>",
      "\<GG>",
      "\<HH>",
      "\<II>",
      "\<JJ>",
      "\<KK>",
      "\<LL>",
      "\<MM>",
      "\<NN>",
      "\<OO>",
      "\<PP>",
      "\<QQ>",
      "\<RR>",
      "\<SS>",
      "\<TT>",
      "\<UU>",
      "\<VV>",
      "\<WW>",
      "\<XX>",
      "\<YY>",
      "\<ZZ>",
      "\<aa>",
      "\<bb>",
      "\<cc>",
      "\<dd>",
      "\<ee>",
      "\<ff>",
      "\<gg>",
      "\<hh>",
      "\<ii>",
      "\<jj>",
      "\<kk>",
      "\<ll>",
      "\<mm>",
      "\<nn>",
      "\<oo>",
      "\<pp>",
      "\<qq>",
      "\<rr>",
      "\<ss>",
      "\<tt>",
      "\<uu>",
      "\<vv>",
      "\<ww>",
      "\<xx>",
      "\<yy>",
      "\<zz>",
      "\<alpha>",
      "\<beta>",
      "\<gamma>",
      "\<delta>",
      "\<epsilon>",
      "\<zeta>",
      "\<eta>",
      "\<theta>",
      "\<iota>",
      "\<kappa>",
      (*"\<lambda>", sic!*)
      "\<mu>",
      "\<nu>",
      "\<xi>",
      "\<pi>",
      "\<rho>",
      "\<sigma>",
      "\<tau>",
      "\<upsilon>",
      "\<phi>",
      "\<chi>",
      "\<psi>",
      "\<omega>",
      "\<Gamma>",
      "\<Delta>",
      "\<Theta>",
      "\<Lambda>",
      "\<Xi>",
      "\<Pi>",
      "\<Sigma>",
      "\<Upsilon>",
      "\<Phi>",
      "\<Psi>",
      "\<Omega>"
    ];
in

val is_letter_symbol = Symtab.defined letter_symbols;

end;

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

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 if is_letter_symbol s then Letter
  else Other;

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;

val is_block_ctrl = member (op =) ["\<^bsub>", "\<^esub>", "\<^bsup>", "\<^esup>"];

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;



(** symbol input **)

(* source *)

local

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

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

fun implode_pseudo_utf8 (cs as ["\192", c]) =
      if ord c < 160 then chr (ord c - 128) else implode cs
  | implode_pseudo_utf8 cs = implode cs;

val scan_encoded_newline =
  $$ "\^M" -- $$ "\n" >> K "\n" ||
  $$ "\^M" >> 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_total =
  Scan.one is_plain ||
  Scan.one is_utf8 ::: Scan.many is_utf8_trailer >> implode_pseudo_utf8 ||
  scan_encoded_newline ||
  ($$ "\\" ^^ $$ "<" ^^
    (($$ "^" ^^ Scan.optional (scan_raw || scan_ascii_id) "" || Scan.optional scan_ascii_id "") ^^
      Scan.optional ($$ ">") "")) ||
  Scan.one not_eof;

in

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

end;


(* explode *)

local

fun no_explode [] = true
  | no_explode ("\\" :: "<" :: _) = false
  | no_explode ("\^M" :: _) = false
  | no_explode (c :: cs) = is_ascii c andalso no_explode cs;

in

fun sym_explode str =
  let val chs = raw_explode str in
    if no_explode chs then chs
    else Source.exhaust (source (Source.of_list chs))
  end;

end;


(* escape *)

val esc = fn s =>
  if is_char s then s
  else if is_utf8 s then translate_string (fn c => "\\" ^ string_of_int (ord c)) s
  else "\\" ^ s;

val escape = implode o map esc o sym_explode;



(** scanning through symbols **)

(* scanner *)

fun scanner msg scan syms =
  let
    fun message (ss, NONE) = (fn () => msg ^ ": " ^ quote (beginning 10 ss))
      | message (ss, SOME msg') = (fn () => msg ^ ", " ^ msg' () ^ ": " ^ quote (beginning 10 ss));
    val finite_scan = Scan.error (Scan.finite stopper (!! message scan));
  in
    (case finite_scan syms of
      (result, []) => result
    | (_, rest) => error (message (rest, NONE) ()))
  end;


(* space-separated words *)

val scan_word =
  Scan.many1 is_ascii_blank >> K NONE ||
  Scan.many1 (fn s => not (is_ascii_blank s) andalso not_eof s) >> (SOME o implode);

val split_words = scanner "Bad text" (Scan.repeat scan_word >> map_filter I);

val explode_words = split_words o sym_explode;


(* blanks *)

val trim_blanks = sym_explode #> trim is_blank #> implode;


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

fun symbolic_end (_ :: "\<^sub>" :: _) = true
  | symbolic_end ("'" :: ss) = symbolic_end ss
  | symbolic_end (s :: _) = raw_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 (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 "\092<long" s then 2
  else if String.isPrefix "\092<Long" s 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;