src/HOL/Tools/string_syntax.ML

 (*  Title:      HOL/Tools/string_syntax.ML
     Author:     Makarius
 
-Concrete syntax for hex chars and strings.
+Concrete syntax for chars and strings.
 *)
 
 structure String_Syntax: sig end =
 struct
 
-(* nibble *)
+(* numeral *)
 
-val mk_nib =
-  Ast.Constant o Lexicon.mark_const o
-    fst o Term.dest_Const o HOLogic.mk_nibble;
+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 dest_nib (Ast.Constant s) =
-  (case try Lexicon.unmark_const s of
-    NONE => raise Match
-  | SOME c => (HOLogic.dest_nibble (Const (c, HOLogic.nibbleT)) handle TERM _ => raise Match));
+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 s =
-  let
-    val c =
-      if Symbol.is_ascii s then ord s
-      else if s = "\<newline>" then 10
-      else error ("Bad character: " ^ quote s);
-  in Ast.Appl [Ast.Constant @{const_syntax Char}, mk_nib (c div 16), mk_nib (c mod 16)] end;
+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_chr c1 c2 =
-  let val s = chr (dest_nib c1 * 16 + dest_nib c2) in
-    if not (member (op =) specials s) andalso Symbol.is_ascii s andalso Symbol.is_printable s
-    then s
-    else if s = "\n" then "\<newline>"
-    else raise Match
-  end;
+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.Appl [Ast.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2
-  | dest_char _ = raise Match;
+fun dest_char_ast (Ast.Appl [Ast.Constant @{syntax_const "_Char"}, Ast.Constant s]) =
+      plain_string_of s
+  | dest_char_ast _ = raise Match;
 
-fun syntax_string ss =
-  Ast.Appl [Ast.Constant @{syntax_const "_inner_string"},
-    Ast.Variable (Lexicon.implode_str ss)];
+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_ast_tr [Ast.Variable str] =
-      (case Lexicon.explode_str (str, Position.none) of
-        [(s, _)] => mk_char s
-      | _ => error ("Single character expected: " ^ str))
-  | char_ast_tr [Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, ast1, ast2]] =
-      Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, char_ast_tr [ast1], ast2]
-  | char_ast_tr asts = raise Ast.AST ("char_ast_tr", asts);
-
-fun char_ast_tr' [c1, c2] =
-      Ast.Appl [Ast.Constant @{syntax_const "_Char"}, syntax_string [dest_chr c1 c2]]
-  | char_ast_tr' _ = raise Match;
+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 [] = Ast.Constant @{const_syntax Nil}
-  | mk_string (s :: ss) =
-      Ast.Appl [Ast.Constant @{const_syntax Cons}, mk_char s, mk_string ss];
+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 string_ast_tr [Ast.Variable str] =
-      (case Lexicon.explode_str (str, Position.none) of
-        [] =>
-          Ast.Appl
-            [Ast.Constant @{syntax_const "_constrain"},
-              Ast.Constant @{const_syntax Nil}, Ast.Constant @{type_syntax string}]
-      | ss => mk_string (map Symbol_Pos.symbol ss))
-  | string_ast_tr [Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, ast1, ast2]] =
-      Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, string_ast_tr [ast1], ast2]
-  | string_ast_tr asts = raise Ast.AST ("string_tr", asts);
+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"},
-        syntax_string (map dest_char (Ast.unfold_ast @{syntax_const "_args"} args))]
+        (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_ast_translation
-     [(@{syntax_const "_Char"}, K char_ast_tr),
-      (@{syntax_const "_String"}, K string_ast_tr)] #>
+   (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
-     [(@{const_syntax Char}, K char_ast_tr'),
-      (@{syntax_const "_list"}, K list_ast_tr')]);
+     [(@{syntax_const "_list"}, K list_ast_tr')]);
 
 end;