diff -r 64559e1ca05b -r 1f9f973eed2a src/HOL/Tools/literal.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/literal.ML	Tue Apr 24 14:17:58 2018 +0000
@@ -0,0 +1,123 @@
+(*  Title:      HOL/Tools/literal.ML
+    Author:     Florian Haftmann, TU Muenchen
+
+Logical and syntactic operations on literals (see also HOL/Tools/hologic.ML).
+*)
+
+signature LITERAL =
+sig
+  val add_code: string -> theory -> theory
+end
+
+structure Literal: LITERAL =
+struct
+
+datatype character = datatype String_Syntax.character;
+
+fun mk_literal_syntax [] = Syntax.const @{const_syntax String.empty_literal}
+  | mk_literal_syntax (c :: cs) =
+      list_comb (Syntax.const @{const_syntax String.Literal}, String_Syntax.mk_bits_syntax 7 c)
+        $ mk_literal_syntax cs;
+
+val dest_literal_syntax =
+  let
+    fun dest (Const (@{const_syntax String.empty_literal}, _)) = []
+      | dest (Const (@{const_syntax String.Literal}, _) $ b0 $ b1 $ b2 $ b3 $ b4 $ b5 $ b6 $ t) =
+          String_Syntax.classify_character (String_Syntax.dest_bits_syntax [b0, b1, b2, b3, b4, b5, b6]) :: dest t
+      | dest t = raise Match;
+  in dest end;
+
+fun ascii_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
+      c $ ascii_tr [t] $ u
+  | ascii_tr [Const (num, _)] =
+      (mk_literal_syntax o single o (fn n => n mod 128) o #value o Lexicon.read_num) num
+  | ascii_tr ts = raise TERM ("ascii_tr", ts);
+
+fun literal_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
+      c $ literal_tr [t] $ u
+  | literal_tr [Free (str, _)] =
+      (mk_literal_syntax o map ord o String_Syntax.plain_strings_of) str
+  | literal_tr ts = raise TERM ("literal_tr", ts);
+
+fun ascii k = Syntax.const @{syntax_const "_Ascii"}
+  $ Syntax.free (String_Syntax.hex k);
+
+fun literal cs = Syntax.const @{syntax_const "_Literal"}
+  $ Syntax.const (Lexicon.implode_str cs);
+
+fun empty_literal_tr' _ = literal [];
+
+fun literal_tr' [b0, b1, b2, b3, b4, b5, b6, t] =
+      let
+        val cs =
+          dest_literal_syntax (list_comb (Syntax.const @{const_syntax String.Literal}, [b0, b1, b2, b3, b4, b5, b6, t]))
+        fun is_printable (Char _) = true
+          | is_printable (Ord _) = false;
+        fun the_char (Char c) = c;
+        fun the_ascii [Ord i] = i;
+      in
+        if forall is_printable cs
+        then literal (map the_char cs)
+        else if length cs = 1
+        then ascii (the_ascii cs)
+        else raise Match
+      end
+  | literal_tr' _ = raise Match;
+
+open Basic_Code_Thingol;
+
+fun map_partial g f =
+  let
+    fun mapp [] = SOME []
+      | mapp (x :: xs) =
+          (case f x of
+            NONE => NONE
+          | SOME y => 
+            (case mapp xs of
+              NONE => NONE
+            | SOME ys => SOME (y :: ys)))
+  in Option.map g o mapp end;
+
+fun implode_bit (IConst { sym = Code_Symbol.Constant @{const_name False}, ... }) = SOME 0
+  | implode_bit (IConst { sym = Code_Symbol.Constant @{const_name True}, ... }) = SOME 1
+  | implode_bit _ = NONE
+
+fun implode_ascii (b0, b1, b2, b3, b4, b5, b6) =
+  map_partial (chr o Integer.eval_radix 2) implode_bit [b0, b1, b2, b3, b4, b5, b6];
+
+fun implode_literal b0 b1 b2 b3 b4 b5 b6 t =
+  let
+    fun dest_literal (IConst { sym = Code_Symbol.Constant @{const_name String.Literal}, ... }
+          `$ b0 `$ b1 `$ b2 `$ b3 `$ b4 `$ b5 `$ b6 `$ t) = SOME ((b0, b1, b2, b3, b4, b5, b6), t)
+      | dest_literal _ = NONE;
+    val (bss', t') = Code_Thingol.unfoldr dest_literal t;
+    val bss = (b0, b1, b2, b3, b4, b5, b6) :: bss';
+  in
+    case t' of
+      IConst { sym = Code_Symbol.Constant @{const_name String.zero_literal_inst.zero_literal}, ... }
+        => map_partial implode implode_ascii bss
+    | _ => NONE
+  end;
+
+fun add_code target thy =
+  let
+    fun pretty literals _ thm _ _ [(b0, _), (b1, _), (b2, _), (b3, _), (b4, _), (b5, _), (b6, _), (t, _)] =
+      case implode_literal b0 b1 b2 b3 b4 b5 b6 t of
+        SOME s => (Code_Printer.str o Code_Printer.literal_string literals) s
+      | NONE => Code_Printer.eqn_error thy thm "Illegal string literal expression";
+  in
+    thy
+    |> Code_Target.set_printings (Code_Symbol.Constant (@{const_name String.Literal},
+      [(target, SOME (Code_Printer.complex_const_syntax (8, pretty)))]))
+  end;
+
+val _ =
+  Theory.setup
+   (Sign.parse_translation
+     [(@{syntax_const "_Ascii"}, K ascii_tr),
+      (@{syntax_const "_Literal"}, K literal_tr)] #>
+    Sign.print_translation
+     [(@{const_syntax String.Literal}, K literal_tr'),
+      (@{const_syntax String.empty_literal}, K empty_literal_tr')]);
+
+end