src/HOL/List.thy

--- a/src/HOL/List.thy	Sun Dec 10 19:37:25 2006 +0100
+++ b/src/HOL/List.thy	Sun Dec 10 19:37:25 2006 +0100
@@ -7,6 +7,7 @@
 
 theory List
 imports PreList
+uses "Tools/string_syntax.ML"
 begin
 
 datatype 'a list =
@@ -108,7 +109,7 @@
   "map f (x#xs) = f(x)#map f xs"
 
 primrec
-  append_Nil:"[]@ys = ys"
+  append_Nil: "[]@ys = ys"
   append_Cons: "(x#xs)@ys = x#(xs@ys)"
 
 primrec
@@ -2515,58 +2516,7 @@
   "_Char" :: "xstr => char"    ("CHR _")
   "_String" :: "xstr => string"    ("_")
 
-parse_ast_translation {*
-  let
-    val constants = Syntax.Appl o map Syntax.Constant;
-
-    fun mk_nib n = "Nibble" ^ chr (n + (if n <= 9 then ord "0" else ord "A" - 10));
-    fun mk_char c =
-      if Symbol.is_ascii c andalso Symbol.is_printable c then
-        constants ["Char", mk_nib (ord c div 16), mk_nib (ord c mod 16)]
-      else error ("Printable ASCII character expected: " ^ quote c);
-
-    fun mk_string [] = Syntax.Constant "Nil"
-      | mk_string (c :: cs) = Syntax.Appl [Syntax.Constant "Cons", mk_char c, mk_string cs];
-
-    fun char_ast_tr [Syntax.Variable xstr] =
-        (case Syntax.explode_xstr xstr of
-          [c] => mk_char c
-        | _ => error ("Single character expected: " ^ xstr))
-      | char_ast_tr asts = raise AST ("char_ast_tr", asts);
-
-    fun string_ast_tr [Syntax.Variable xstr] =
-        (case Syntax.explode_xstr xstr of
-          [] => constants [Syntax.constrainC, "Nil", "string"]
-        | cs => mk_string cs)
-      | string_ast_tr asts = raise AST ("string_tr", asts);
-  in [("_Char", char_ast_tr), ("_String", string_ast_tr)] end;
-*}
-
-print_ast_translation {*
-  let
-    fun dest_nib (Syntax.Constant c) =
-        (case explode c of
-          ["N", "i", "b", "b", "l", "e", h] => HOLogic.int_of_nibble h
-        | _ => raise Match)
-      | dest_nib _ = raise Match;
-
-    fun dest_chr c1 c2 =
-      let val c = chr (dest_nib c1 * 16 + dest_nib c2)
-      in if Symbol.is_printable c then c else raise Match end;
-
-    fun dest_char (Syntax.Appl [Syntax.Constant "Char", c1, c2]) = dest_chr c1 c2
-      | dest_char _ = raise Match;
-
-    fun xstr cs = Syntax.Appl [Syntax.Constant "_xstr", Syntax.Variable (Syntax.implode_xstr cs)];
-
-    fun char_ast_tr' [c1, c2] = Syntax.Appl [Syntax.Constant "_Char", xstr [dest_chr c1 c2]]
-      | char_ast_tr' _ = raise Match;
-
-    fun list_ast_tr' [args] = Syntax.Appl [Syntax.Constant "_String",
-            xstr (map dest_char (Syntax.unfold_ast "_args" args))]
-      | list_ast_tr' ts = raise Match;
-  in [("Char", char_ast_tr'), ("@list", list_ast_tr')] end;
-*}
+setup StringSyntax.setup
 
 
 subsection {* Code generator *}
@@ -2633,7 +2583,7 @@
   in SOME (gr', Pretty.list "[" "]" ps) end handle TERM _ => NONE;
 
 fun char_codegen thy defs gr dep thyname b t =
-  case (Option.map chr o HOLogic.dest_char) t 
+  case (Option.map chr o try HOLogic.dest_char) t 
    of SOME c =>
         if Symbol.is_printable c
         then SOME (gr, (Pretty.quote o Pretty.str) c)
@@ -2647,9 +2597,9 @@
   #> CodegenSerializer.add_pretty_list "SML" "List.list.Nil" "List.list.Cons"
        (Pretty.enum "," "[" "]") NONE (7, "::")
   #> CodegenSerializer.add_pretty_list "Haskell" "List.list.Nil" "List.list.Cons"
-       (Pretty.enum "," "[" "]") (SOME (HOLogic.print_char, HOLogic.print_string)) (5, ":")
+       (Pretty.enum "," "[" "]") (SOME (ML_Syntax.print_char, ML_Syntax.print_string)) (5, ":")
   #> CodegenPackage.add_appconst
-       ("List.char.Char", CodegenPackage.appgen_char HOLogic.dest_char)
+       ("List.char.Char", CodegenPackage.appgen_char (try HOLogic.dest_char))
 
 end;
 *}
@@ -2704,19 +2654,20 @@
   "itrev (x#xs) ys = itrev xs (x#ys)"
 
 text {*
-  Only use @{text mem} for generating executable code.  Otherwise
-  use @{prop "x : set xs"} instead --- it is much easier to reason about.
+  Only use @{text mem} for generating executable code.  Otherwise use
+  @{prop "x : set xs"} instead --- it is much easier to reason about.
   The same is true for @{const list_all} and @{const list_ex}: write
   @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"} instead because the HOL
-  quantifiers are aleady known to the automatic provers. In fact,
-  the declarations in the code subsection make sure that @{text "\<in>"}, @{text "\<forall>x\<in>set xs"}
-  and @{text "\<exists>x\<in>set xs"} are implemented efficiently.
+  quantifiers are aleady known to the automatic provers. In fact, the
+  declarations in the code subsection make sure that @{text "\<in>"},
+  @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"} are implemented
+  efficiently.
 
   Efficient emptyness check is implemented by @{const null}.
 
-  The functions @{const itrev}, @{const filtermap} and @{const map_filter}
-  are just there to generate efficient code. Do not use them
-  for modelling and proving.
+  The functions @{const itrev}, @{const filtermap} and @{const
+  map_filter} are just there to generate efficient code. Do not use
+  them for modelling and proving.
 *}
 
 lemma mem_iff [normal post]: