more concise string serialization

--- a/src/HOL/List.thy	Mon Aug 21 11:02:39 2006 +0200
+++ b/src/HOL/List.thy	Mon Aug 21 11:02:40 2006 +0200
@@ -2721,16 +2721,28 @@
         else NONE
     | NONE => NONE;
 
+val print_list = Pretty.enum "," "[" "]";
+
+fun print_char c =
+  let
+    val i = ord c
+  in if i < 32
+    then prefix "\\" (string_of_int i)
+    else c
+  end;
+
+val print_string = quote;
+
 in
 
 val list_codegen_setup =
   Codegen.add_codegen "list_codegen" list_codegen
   #> Codegen.add_codegen "char_codegen" char_codegen
-  #> fold (CodegenPackage.add_pretty_list "Nil" "Cons") [
-       ("ml", (7, "::")),
-       ("haskell", (5, ":"))
-     ]
-  #> CodegenPackage.add_appconst
+  #> CodegenPackage.add_pretty_list "ml" "Nil" "Cons"
+       print_list NONE (7, "::")
+  #> CodegenPackage.add_pretty_list "haskell" "Nil" "Cons"
+       print_list (SOME (print_char, print_string)) (5, ":")
+  #> CodegenPackage.add_appconst_i
        ("List.char.Char", CodegenPackage.appgen_char dest_char);
 
 end;
@@ -2776,8 +2788,10 @@
     ml (target_atom "char")
     haskell (target_atom "Char")
 
-code_constapp Char
-  ml (target_atom "(__,/ __)")
+code_constapp
+  Char
+    ml (target_atom "(__,/ __)")
+    haskell (target_atom "(__,/ __)")
 
 setup list_codegen_setup
 

--- a/src/Pure/Tools/codegen_package.ML	Mon Aug 21 11:02:39 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Mon Aug 21 11:02:40 2006 +0200
@@ -19,8 +19,11 @@
     -> ((string * CodegenThingol.funn) list -> Pretty.T)
         * ((string * CodegenThingol.datatyp) list -> Pretty.T);
 
-  val add_pretty_list: string -> string -> string * (int * string)
-    -> theory -> theory;
+  val add_pretty_list: string -> string -> string -> (Pretty.T list -> Pretty.T)
+   -> ((string -> string) * (string -> string)) option -> int * string
+   -> theory -> theory;
+  val add_pretty_ml_string: string -> string -> string -> string
+   -> (string -> string) -> (string -> string) -> string -> theory -> theory;
   val purge_code: theory -> theory;
 
   type appgen;
@@ -708,6 +711,9 @@
 
 fun eval_term (ref_spec, t) thy =
   let
+    val _ = Term.fold_atyps (fn _ =>
+      error ("Term" ^ Sign.string_of_term thy t ^ "is polymorhpic"))
+      (Term.fastype_of t);
     fun preprocess_term t =
       let
         val x = Free (Name.variant (add_term_names (t, [])) "x", fastype_of t);
@@ -845,7 +851,7 @@
     #-> (fn reader => pair (mk reader))
   end;
 
-fun add_pretty_list raw_nil raw_cons (target, seri) thy =
+fun add_pretty_list target raw_nil raw_cons mk_list mk_char_string target_cons thy =
   let
     val _ = get_serializer target;
     fun prep_const raw =
@@ -859,12 +865,30 @@
       idf_of_const thy (snd tabs) c_ty;
     val nil'' = mk_const nil';
     val cons'' = mk_const cons';
-    val pr = CodegenSerializer.pretty_list nil'' cons'' seri;
+    val pr = CodegenSerializer.pretty_list nil'' cons'' mk_list mk_char_string target_cons;
   in
     thy
     |> add_pretty_syntax_const cons'' target pr
   end;
 
+fun add_pretty_ml_string target raw_nil raw_cons raw_str mk_char mk_string target_implode thy =
+  let
+    val _ = get_serializer target;
+    fun prep_const raw =
+      let
+        val c = Sign.intern_const thy raw
+      in (c, Sign.the_const_type thy c) end;
+    val cs' = map prep_const [raw_nil, raw_cons, raw_str];
+    val tabs = mk_tabs thy NONE cs';
+    fun mk_const c_ty =
+      idf_of_const thy (snd tabs) c_ty;
+    val [nil', cons', str'] = map mk_const cs';
+    val pr = CodegenSerializer.pretty_ml_string nil' cons' mk_char mk_string target_implode;
+  in
+    thy
+    |> add_pretty_syntax_const str' target pr
+  end;
+
 
 
 (** code basis change notifications **)

--- a/src/Pure/Tools/codegen_serializer.ML	Mon Aug 21 11:02:39 2006 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML	Mon Aug 21 11:02:40 2006 +0200
@@ -20,7 +20,11 @@
       * OuterParse.token list;
   val parse_syntax: ('b -> int) -> (string -> 'b -> 'a * 'b) -> OuterParse.token list ->
     ('b -> 'a pretty_syntax * 'b) * OuterParse.token list;
-  val pretty_list: string -> string -> int * string -> CodegenThingol.iterm pretty_syntax;
+  val pretty_list: string -> string -> (Pretty.T list -> Pretty.T)
+    -> ((string -> string) * (string -> string)) option
+    -> int * string -> CodegenThingol.iterm pretty_syntax;
+  val pretty_ml_string: string -> string -> (string -> string) -> (string -> string)
+    -> string -> CodegenThingol.iterm pretty_syntax;
   val serializers: {
     ml: string * (string -> serializer),
     haskell: string * (string * string list -> serializer)
@@ -305,29 +309,56 @@
           | _ => SOME)
        | _ => Scan.fail ());
 
-(* list serializer *)
 
-fun pretty_list thingol_nil thingol_cons (target_pred, target_cons) =
+(* list and string serializers *)
+
+fun implode_list c_nil c_cons e =
   let
     fun dest_cons (IConst (c, _) `$ e1 `$ e2) =
-          if c = thingol_cons
+          if c = c_cons
           then SOME (e1, e2)
           else NONE
       | dest_cons  _ = NONE;
-    fun pretty_default fxy pr e1 e2 =
-      brackify_infix (target_pred, R) fxy [
-        pr (INFX (target_pred, X)) e1,
+    val (es, e') = CodegenThingol.unfoldr dest_cons e;
+  in case e'
+   of IConst (c, _) => if c = c_nil then SOME es else NONE
+    | _ => NONE
+  end;
+
+fun implode_string mk_char mk_string es =
+  if forall (fn IChar _ => true | _ => false) es
+  then (SOME o str o mk_string o implode o map (fn IChar (c, _) => mk_char c)) es
+  else NONE;
+
+fun pretty_ml_string c_nil c_cons mk_char mk_string target_implode =
+  let
+    fun pretty fxy pr [e] =
+      case implode_list c_nil c_cons e
+       of SOME es => (case implode_string mk_char mk_string es
+           of SOME p => p
+            | NONE => Pretty.block [str target_implode, Pretty.brk 1, pr BR e])
+        | NONE => Pretty.block [str target_implode, Pretty.brk 1, pr BR e]
+  in ((1, 1), pretty) end;
+
+fun pretty_list c_nil c_cons mk_list mk_char_string (target_fxy, target_cons) =
+  let
+    fun default fxy pr e1 e2 =
+      brackify_infix (target_fxy, R) fxy [
+        pr (INFX (target_fxy, X)) e1,
         str target_cons,
-        pr (INFX (target_pred, R)) e2
+        pr (INFX (target_fxy, R)) e2
       ];
-    fun pretty_compact fxy pr [e1, e2] =
-      case CodegenThingol.unfoldr dest_cons e2
-       of (es, IConst (c, _)) =>
-            if c = thingol_nil
-            then Pretty.enum "," "[" "]" (map (pr NOBR) (e1::es))
-            else pretty_default fxy pr e1 e2
-        | _ => pretty_default fxy pr e1 e2;
-  in ((2, 2), pretty_compact) end;
+    fun pretty fxy pr [e1, e2] =
+      case Option.map (cons e1) (implode_list c_nil c_cons e2)
+       of SOME es =>
+            (case mk_char_string
+             of SOME (mk_char, mk_string) =>
+                  (case implode_string mk_char mk_string es
+                   of SOME p => p
+                    | NONE => mk_list (map (pr NOBR) es))
+              | NONE => mk_list (map (pr NOBR) es))
+        | NONE => default fxy pr e1 e2;
+  in ((2, 2), pretty) end;
 
 
 
@@ -336,8 +367,9 @@
 local
 
 val reserved_ml = ThmDatabase.ml_reserved @ [
-  "bool", "int", "list", "unit", "option", "true", "false", "not", "None", "Some", "o"
-];  (* FIXME None/Some no longer used *)
+  "bool", "int", "list", "unit", "option", "true", "false", "not", "NONE", "SOME",
+  "o", "string", "char", "String", "Term"
+];
 
 structure NameMangler = NameManglerFun (
   type ctxt = string list;
@@ -355,17 +387,18 @@
     val ml_from_label =
       str o translate_string (fn "_" => "__" | "." => "_" | c => c)
         o NameSpace.base o resolv;
+    fun ml_from_dictvar v = 
+      str (Symbol.to_ascii_upper v ^ "_");
     fun ml_from_tyvar (v, []) =
           str "()"
       | ml_from_tyvar (v, sort) =
           let
-            val w = Symbol.to_ascii_upper v;
             fun mk_class class =
               str (prefix "'" v ^ " " ^ resolv class);
           in
             Pretty.block [
               str "(",
-              str w,
+              ml_from_dictvar v,
               str ":",
               case sort
                of [class] => mk_class class
@@ -380,17 +413,17 @@
             if (is_some o Int.fromString) l then str l
             else ml_from_label l
           ];
-        fun from_lookup fxy [] v =
-              v
-          | from_lookup fxy [l] v =
+        fun from_lookup fxy [] p =
+              p
+          | from_lookup fxy [l] p =
               brackify fxy [
                 from_label l,
-                v
+                p
               ]
-          | from_lookup fxy ls v =
+          | from_lookup fxy ls p =
               brackify fxy [
                 Pretty.enum " o" "(" ")" (map from_label ls),
-                v
+                p
               ];
         fun from_classlookup fxy (Instance (inst, lss)) =
               brackify fxy (
@@ -399,10 +432,10 @@
               )
           | from_classlookup fxy (Lookup (classes, (v, ~1))) =
               from_lookup BR classes
-                ((str o Symbol.to_ascii_upper) v)
+                (ml_from_dictvar v)
           | from_classlookup fxy (Lookup (classes, (v, i))) =
               from_lookup BR (string_of_int (i+1) :: classes)
-                ((str o Symbol.to_ascii_upper) v)
+                (ml_from_dictvar v)
       in case lss
        of [] => str "()"
         | [ls] => from_classlookup fxy ls
@@ -757,9 +790,16 @@
         str ("end; (* struct " ^ name ^ " *)")
       ]);
     val is_cons = ml_annotators nsp_dtcon;
+    fun postproc (shallow, n) =
+      let
+        fun ch_first f = String.implode o nth_map 0 f o String.explode;
+      in if shallow = nsp_dtcon
+        then ch_first Char.toUpper n
+        else n
+      end;
   in abstract_serializer (target, nspgrp)
     root_name (ml_from_defs is_cons, ml_from_module,
-     abstract_validator reserved_ml, snd) end;
+     abstract_validator reserved_ml, postproc) end;
 
 in
 
@@ -786,8 +826,10 @@
   let
     val (val_name, modl') = CodegenThingol.add_eval_def (nsp_eval, e) modl;
     val struct_name = "EVAL";
+    fun output p = if !eval_verbose then (Pretty.writeln p; Pretty.output p)
+      else Pretty.output p;
     val serializer = ml_serializer struct_name "ml" nsp_dtcon nspgrp
-      (fn "" => (fn p => (use_text Context.ml_output (!eval_verbose) (Pretty.output p); NONE))
+      (fn "" => (fn p => (use_text Context.ml_output (!eval_verbose) (output p); NONE))
         | _ => SOME) (K NONE, syntax_tyco, syntax_const) (hidden, SOME [NameSpace.pack [nsp_eval, val_name]]);
     val _ = serializer modl';
     val val_name_struct = NameSpace.append struct_name val_name;
@@ -951,22 +993,19 @@
             ] |> SOME
           else SOME body end
       | hs_from_def (name, CodegenThingol.Typesyn (sctxt, ty)) =
-          Pretty.block [
-            str "type ",
+          (Pretty.block o Pretty.breaks) [
+            str "type",
             hs_from_sctxt_tycoexpr (sctxt, (resolv_here name, map (ITyVar o fst) sctxt)),
-            str " =",
-            Pretty.brk 1,
+            str "=",
             hs_from_sctxt_type ([], ty)
           ] |> SOME
-      | hs_from_def (name, CodegenThingol.Datatype (sctxt, [(co, tys)])) =
+      | hs_from_def (name, CodegenThingol.Datatype (sctxt, [(co, [ty])])) =
           (Pretty.block o Pretty.breaks) [
             str "newtype",
             hs_from_sctxt_tycoexpr (sctxt, (resolv_here name, map (ITyVar o fst) sctxt)),
             str "=",
-            (Pretty.block o Pretty.breaks) (
-              (str o resolv_here) co
-              :: map (hs_from_type BR) tys
-            )
+            (str o resolv_here) co,
+            hs_from_type BR ty
           ] |> SOME
       | hs_from_def (name, CodegenThingol.Datatype (sctxt, constrs)) =
           let
@@ -1036,7 +1075,8 @@
       "import", "default", "forall", "let", "in", "class", "qualified", "data",
       "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
     ] @ [
-      "Bool", "Integer", "Maybe", "True", "False", "Nothing", "Just", "not", "negate"
+      "Bool", "Integer", "Maybe", "True", "False", "Nothing", "Just", "not", "negate",
+      "String", "Char"
     ];
     fun is_cons c = CodegenThingol.has_nsp c nsp_dtcon;
     fun hs_from_module resolv imps ((_, name), ps) =