src/HOL/Tools/string_syntax.ML

new/improved theories involving convergence; better pretty-printing for bounded quantifiers and sum/product

(*  Title:      HOL/Tools/string_syntax.ML
    Author:     Makarius

Concrete syntax for chars and strings.
*)

structure String_Syntax: sig end =
struct

(* numeral *)

fun hex_digit n = if n = 10 then "A"
  else if n = 11 then "B"
  else if n = 12 then "C"
  else if n = 13 then "D"
  else if n = 14 then "E"
  else if n = 15 then "F"
  else string_of_int n;

fun hex_prefix ms = "0x" ^ implode (replicate (2 - length ms) "0" @ ms);

fun hex n = hex_prefix (map hex_digit (radixpand (16, n)));


(* char *)

fun mk_char_syntax n =
  if n = 0 then Syntax.const @{const_name Groups.zero}
  else Syntax.const @{const_syntax Char} $ Numeral.mk_num_syntax n;

fun mk_char_syntax' c =
  if Symbol.is_ascii c then mk_char_syntax (ord c)
  else if c = "\<newline>" then mk_char_syntax 10
  else error ("Bad character: " ^ quote c);

fun plain_string_of str =
  map fst (Lexicon.explode_str (str, Position.none));

datatype character = Char of string | Ord of int | Unprintable;

val specials = raw_explode "\\\"`'";

fun dest_char_syntax c =
  case try Numeral.dest_num_syntax c of
    SOME n =>
      if n < 256 then
        let
          val s = chr n
        in
          if not (member (op =) specials s) andalso Symbol.is_ascii s andalso Symbol.is_printable s
          then Char s
          else if s = "\n" then Char "\<newline>"
          else Ord n
        end
      else Unprintable
  | NONE => Unprintable;

fun dest_char_ast (Ast.Appl [Ast.Constant @{syntax_const "_Char"}, Ast.Constant s]) =
      plain_string_of s
  | dest_char_ast _ = raise Match;

fun char_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
      c $ char_tr [t] $ u
  | char_tr [Free (str, _)] =
      (case plain_string_of str of
        [c] => mk_char_syntax' c
      | _ => error ("Single character expected: " ^ str))
  | char_tr ts = raise TERM ("char_tr", ts);

fun char_ord_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
      c $ char_ord_tr [t] $ u
  | char_ord_tr [Const (num, _)] =
      (mk_char_syntax o #value o Lexicon.read_num) num
  | char_ord_tr ts = raise TERM ("char_ord_tr", ts);

fun char_tr' [t] = (case dest_char_syntax t of
        Char s => Syntax.const @{syntax_const "_Char"} $
          Syntax.const (Lexicon.implode_str [s])
      | Ord n => 
          if n = 0
          then Syntax.const @{const_syntax Groups.zero}
          else Syntax.const @{syntax_const "_Char_ord"} $
            Syntax.free (hex n)
      | _ => raise Match)
  | char_tr' _ = raise Match;


(* string *)

fun mk_string_syntax [] = Syntax.const @{const_syntax Nil}
  | mk_string_syntax (c :: cs) =
      Syntax.const @{const_syntax Cons} $ mk_char_syntax' c $ mk_string_syntax cs;

fun mk_string_ast ss =
  Ast.Appl [Ast.Constant @{syntax_const "_inner_string"},
    Ast.Variable (Lexicon.implode_str ss)];

fun string_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
      c $ string_tr [t] $ u
  | string_tr [Free (str, _)] =
      mk_string_syntax (plain_string_of str)
  | string_tr ts = raise TERM ("char_tr", ts);

fun list_ast_tr' [args] =
      Ast.Appl [Ast.Constant @{syntax_const "_String"},
        (mk_string_ast o maps dest_char_ast o Ast.unfold_ast @{syntax_const "_args"}) args]
  | list_ast_tr' _ = raise Match;


(* theory setup *)

val _ =
  Theory.setup
   (Sign.parse_translation
     [(@{syntax_const "_Char"}, K char_tr),
      (@{syntax_const "_Char_ord"}, K char_ord_tr),
      (@{syntax_const "_String"}, K string_tr)] #>
    Sign.print_translation
     [(@{const_syntax Char}, K char_tr')] #>
    Sign.print_ast_translation
     [(@{syntax_const "_list"}, K list_ast_tr')]);

end;