restructured code generation of literals

--- a/src/HOL/Library/Code_Char.thy	Fri Aug 29 20:36:08 2008 +0200
+++ b/src/HOL/Library/Code_Char.thy	Mon Sep 01 10:18:37 2008 +0200
@@ -36,9 +36,9 @@
     @{const_name NibbleC}, @{const_name NibbleD},
     @{const_name NibbleE}, @{const_name NibbleF}];
 in
-  fold (fn target => Code_Target.add_pretty_char target charr nibbles)
+  fold (fn target => Code_Target.add_literal_char target charr nibbles)
     ["SML", "OCaml", "Haskell"]
-  #> Code_Target.add_pretty_list_string "Haskell"
+  #> Code_Target.add_literal_list_string "Haskell"
     @{const_name Nil} @{const_name Cons} charr nibbles
 end
 *}

--- a/src/HOL/Library/Code_Message.thy	Fri Aug 29 20:36:08 2008 +0200
+++ b/src/HOL/Library/Code_Message.thy	Mon Sep 01 10:18:37 2008 +0200
@@ -51,7 +51,7 @@
     @{const_name NibbleC}, @{const_name NibbleD},
     @{const_name NibbleE}, @{const_name NibbleF}];
 in
-  fold (fn target => Code_Target.add_pretty_message target
+  fold (fn target => Code_Target.add_literal_message target
     charr nibbles @{const_name Nil} @{const_name Cons} @{const_name STR})
   ["SML", "OCaml", "Haskell"]
 end

--- a/src/HOL/List.thy	Fri Aug 29 20:36:08 2008 +0200
+++ b/src/HOL/List.thy	Mon Sep 01 10:18:37 2008 +0200
@@ -3450,7 +3450,7 @@
   (Haskell "[]")
 
 setup {*
-  fold (fn target => Code_Target.add_pretty_list target
+  fold (fn target => Code_Target.add_literal_list target
     @{const_name Nil} @{const_name Cons}
   ) ["SML", "OCaml", "Haskell"]
 *}

--- a/src/HOL/Tools/numeral.ML	Fri Aug 29 20:36:08 2008 +0200
+++ b/src/HOL/Tools/numeral.ML	Mon Sep 01 10:18:37 2008 +0200
@@ -56,7 +56,7 @@
 (* code generator *)
 
 fun add_code number_of negative unbounded target =
-  Code_Target.add_pretty_numeral target negative unbounded number_of
+  Code_Target.add_literal_numeral target negative unbounded number_of
   @{const_name Int.Pls} @{const_name Int.Min}
   @{const_name Int.Bit0} @{const_name Int.Bit1};
 

--- a/src/Tools/code/code_haskell.ML	Fri Aug 29 20:36:08 2008 +0200
+++ b/src/Tools/code/code_haskell.ML	Mon Sep 01 10:18:37 2008 +0200
@@ -408,6 +408,20 @@
       destination
   end;
 
+val literals = let
+  fun char_haskell c =
+    let
+      val s = ML_Syntax.print_char c;
+    in if s = "'" then "\\'" else s end;
+in Literals {
+  literal_char = enclose "'" "'" o char_haskell,
+  literal_string = quote o translate_string char_haskell,
+  literal_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
+    else enclose "(" ")" (signed_string_of_int k),
+  literal_list = Pretty.enum "," "[" "]",
+  infix_cons = (5, ":")
+} end;
+
 
 (** optional monad syntax **)
 
@@ -474,7 +488,7 @@
   );
 
 val setup =
-  Code_Target.add_target (target, isar_seri_haskell)
+  Code_Target.add_target (target, (isar_seri_haskell, literals))
   #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
       brackify_infix (1, R) fxy [
         pr_typ (INFX (1, X)) ty1,

--- a/src/Tools/code/code_ml.ML	Fri Aug 29 20:36:08 2008 +0200
+++ b/src/Tools/code/code_ml.ML	Mon Sep 01 10:18:37 2008 +0200
@@ -329,6 +329,16 @@
     @@ str ("end; (*struct " ^ name ^ "*)")
   );
 
+val literals_sml = Literals {
+  literal_char = prefix "#" o quote o ML_Syntax.print_char,
+  literal_string = quote o translate_string ML_Syntax.print_char,
+  literal_numeral = fn unbounded => fn k =>
+    if unbounded then "(" ^ string_of_int k ^ " : IntInf.int)"
+    else string_of_int k,
+  literal_list = Pretty.enum "," "[" "]",
+  infix_cons = (7, "::")
+};
+
 
 (** OCaml serializer **)
 
@@ -633,6 +643,35 @@
     @@ str ("end;; (*struct " ^ name ^ "*)")
   );
 
+val literals_ocaml = let
+  fun chr i =
+    let
+      val xs = string_of_int i;
+      val ys = replicate_string (3 - length (explode xs)) "0";
+    in "\\" ^ ys ^ xs end;
+  fun char_ocaml c =
+    let
+      val i = ord c;
+      val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126
+        then chr i else c
+    in s end;
+in Literals {
+  literal_char = enclose "'" "'" o char_ocaml,
+  literal_string = quote o translate_string char_ocaml,
+  literal_numeral = fn unbounded => fn k => if k >= 0 then
+      if unbounded then
+        "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
+      else string_of_int k
+    else
+      if unbounded then
+        "(Big_int.big_int_of_int " ^ (enclose "(" ")" o prefix "-"
+          o string_of_int o op ~) k ^ ")"
+      else (enclose "(" ")" o prefix "-" o string_of_int o op ~) k,
+  literal_list = Pretty.enum ";" "[" "]",
+  infix_cons = (6, "::")
+} end;
+
+
 
 (** SML/OCaml generic part **)
 
@@ -839,7 +878,8 @@
 (** ML (system language) code for evaluation and instrumentalization **)
 
 fun ml_code_of thy = Code_Target.serialize_custom thy
-  (target_SML, (fn _ => fn [] => serialize_ml target_SML (SOME (K ())) (K Pretty.chunks) pr_sml_stmt (SOME "")));
+  (target_SML, (fn _ => fn [] => serialize_ml target_SML (SOME (K ())) (K Pretty.chunks) pr_sml_stmt (SOME ""),
+  literals_sml));
 
 
 (* evaluation *)
@@ -935,8 +975,8 @@
       pr_ocaml_module pr_ocaml_stmt module_name);
 
 val setup =
-  Code_Target.add_target (target_SML, isar_seri_sml)
-  #> Code_Target.add_target (target_OCaml, isar_seri_ocaml)
+  Code_Target.add_target (target_SML, (isar_seri_sml, literals_sml))
+  #> Code_Target.add_target (target_OCaml, (isar_seri_ocaml, literals_ocaml))
   #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
       brackify_infix (1, R) fxy [
         pr_typ (INFX (1, X)) ty1,

--- a/src/Tools/code/code_printer.ML	Fri Aug 29 20:36:08 2008 +0200
+++ b/src/Tools/code/code_printer.ML	Mon Sep 01 10:18:37 2008 +0200
@@ -59,6 +59,16 @@
     -> (thm -> bool -> var_ctxt -> fixity -> iterm -> Pretty.T)
     -> thm -> fixity -> (string option * iterm option) * itype -> var_ctxt -> Pretty.T * var_ctxt
 
+  type literals
+  val Literals: { literal_char: string -> string, literal_string: string -> string,
+        literal_numeral: bool -> int -> string, literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string }
+    -> literals
+  val literal_char: literals -> string -> string
+  val literal_string: literals -> string -> string
+  val literal_numeral: literals -> bool -> int -> string
+  val literal_list: literals -> Pretty.T list -> Pretty.T
+  val infix_cons: literals -> int * string
+
   val nerror: thm -> string -> 'a
 end;
 
@@ -276,4 +286,23 @@
 
 val _ = List.app OuterKeyword.keyword [infixK, infixlK, infixrK];
 
+
+(** pretty literals **)
+
+datatype literals = Literals of {
+  literal_char: string -> string,
+  literal_string: string -> string,
+  literal_numeral: bool -> int -> string,
+  literal_list: Pretty.T list -> Pretty.T,
+  infix_cons: int * string
+};
+
+fun dest_Literals (Literals lits) = lits;
+
+val literal_char = #literal_char o dest_Literals;
+val literal_string = #literal_string o dest_Literals;
+val literal_numeral = #literal_numeral o dest_Literals;
+val literal_list = #literal_list o dest_Literals;
+val infix_cons = #infix_cons o dest_Literals;
+
 end; (*struct*)

--- a/src/Tools/code/code_target.ML	Fri Aug 29 20:36:08 2008 +0200
+++ b/src/Tools/code/code_target.ML	Mon Sep 01 10:18:37 2008 +0200
@@ -10,7 +10,7 @@
   include CODE_PRINTER
 
   type serializer
-  val add_target: string * serializer -> theory -> theory
+  val add_target: string * (serializer * literals) -> theory -> theory
   val extend_target: string * (string * (Code_Thingol.program -> Code_Thingol.program))
     -> theory -> theory
   val assert_target: theory -> string -> string
@@ -28,7 +28,7 @@
     -> 'a -> serialization
   val serialize: theory -> string -> string option -> Args.T list
     -> Code_Thingol.program -> string list -> serialization
-  val serialize_custom: theory -> string * serializer
+  val serialize_custom: theory -> string * (serializer * literals)
     -> Code_Thingol.program -> string list -> string * string list
   val compile: serialization -> unit
   val export: serialization -> unit
@@ -51,13 +51,13 @@
     -> (theory -> theory) * OuterParse.token list
   val add_reserved: string -> string -> theory -> theory
 
-  val add_pretty_list: string -> string -> string -> theory -> theory
-  val add_pretty_list_string: string -> string -> string
+  val add_literal_list: string -> string -> string -> theory -> theory
+  val add_literal_list_string: string -> string -> string
     -> string -> string list -> theory -> theory
-  val add_pretty_char: string -> string -> string list -> theory -> theory
-  val add_pretty_numeral: string -> bool -> bool -> string -> string -> string
+  val add_literal_char: string -> string -> string list -> theory -> theory
+  val add_literal_numeral: string -> bool -> bool -> string -> string -> string
     -> string -> string -> theory -> theory
-  val add_pretty_message: string -> string -> string list -> string
+  val add_literal_message: string -> string -> string list -> string
     -> string -> string -> theory -> theory
 end;
 
@@ -147,67 +147,7 @@
   in dest_numeral #> the_default 0 end;
 
 
-(* pretty syntax printing *)
-
-local
-
-fun ocaml_char c =
-  let
-    fun chr i =
-      let
-        val xs = string_of_int i;
-        val ys = replicate_string (3 - length (explode xs)) "0";
-      in "\\" ^ ys ^ xs end;
-    val i = ord c;
-    val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126
-      then chr i else c
-  in s end;
-
-fun haskell_char c =
-  let
-    val s = ML_Syntax.print_char c;
-  in if s = "'" then "\\'" else s end;
-
-val pretty : (string * {
-    pretty_char: string -> string,
-    pretty_string: string -> string,
-    pretty_numeral: bool -> int -> string,
-    pretty_list: Pretty.T list -> Pretty.T,
-    infix_cons: int * string
-  }) list = [
-  ("SML", { pretty_char = prefix "#" o quote o ML_Syntax.print_char,
-      pretty_string = quote o translate_string ML_Syntax.print_char,
-      pretty_numeral = fn unbounded => fn k =>
-        if unbounded then "(" ^ string_of_int k ^ " : IntInf.int)"
-        else string_of_int k,
-      pretty_list = Pretty.enum "," "[" "]",
-      infix_cons = (7, "::")}),
-  ("OCaml", { pretty_char = enclose "'" "'" o ocaml_char,
-      pretty_string = quote o translate_string ocaml_char,
-      pretty_numeral = fn unbounded => fn k => if k >= 0 then
-            if unbounded then
-              "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
-            else string_of_int k
-          else
-            if unbounded then
-              "(Big_int.big_int_of_int " ^ (enclose "(" ")" o prefix "-"
-                o string_of_int o op ~) k ^ ")"
-            else (enclose "(" ")" o prefix "-" o string_of_int o op ~) k,
-      pretty_list = Pretty.enum ";" "[" "]",
-      infix_cons = (6, "::")}),
-  ("Haskell", { pretty_char = enclose "'" "'" o haskell_char,
-      pretty_string = quote o translate_string haskell_char,
-      pretty_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
-          else enclose "(" ")" (signed_string_of_int k),
-      pretty_list = Pretty.enum "," "[" "]",
-      infix_cons = (5, ":")})
-];
-
-in
-
-fun pr_pretty target = case AList.lookup (op =) pretty target
- of SOME x => x
-  | NONE => error ("Unknown code target language: " ^ quote target);
+(* literal syntax printing *)
 
 fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
   brackify_infix (target_fxy, R) fxy [
@@ -216,51 +156,48 @@
     pr (INFX (target_fxy, R)) t2
   ];
 
-fun pretty_list c_nil c_cons target =
+fun pretty_list c_nil c_cons literals =
   let
-    val pretty_ops = pr_pretty target;
-    val mk_list = #pretty_list pretty_ops;
+    val mk_list = literal_list literals;
     fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] =
       case Option.map (cons t1) (implode_list c_nil c_cons t2)
        of SOME ts => mk_list (map (pr vars NOBR) ts)
-        | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;
+        | NONE => default_list (infix_cons literals) (pr vars) fxy t1 t2;
   in (2, pretty) end;
 
-fun pretty_list_string c_nil c_cons c_char c_nibbles target =
+fun pretty_list_string c_nil c_cons c_char c_nibbles literals =
   let
-    val pretty_ops = pr_pretty target;
-    val mk_list = #pretty_list pretty_ops;
-    val mk_char = #pretty_char pretty_ops;
-    val mk_string = #pretty_string pretty_ops;
+    val mk_list = literal_list literals;
+    val mk_char = literal_char literals;
+    val mk_string = literal_string literals;
     fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] =
       case Option.map (cons t1) (implode_list c_nil c_cons t2)
        of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts
            of SOME p => p
             | NONE => mk_list (map (pr vars NOBR) ts))
-        | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;
+        | NONE => default_list (infix_cons literals) (pr vars) fxy t1 t2;
   in (2, pretty) end;
 
-fun pretty_char c_char c_nibbles target =
+fun pretty_char c_char c_nibbles literals =
   let
-    val mk_char = #pretty_char (pr_pretty target);
+    val mk_char = literal_char literals;
     fun pretty _ thm _ _ _ [(t1, _), (t2, _)] =
       case decode_char c_nibbles (t1, t2)
        of SOME c => (str o mk_char) c
         | NONE => nerror thm "Illegal character expression";
   in (2, pretty) end;
 
-fun pretty_numeral unbounded negative c_pls c_min c_bit0 c_bit1 target =
+fun pretty_numeral unbounded negative c_pls c_min c_bit0 c_bit1 literals =
   let
-    val mk_numeral = #pretty_numeral (pr_pretty target);
+    val mk_numeral = literal_numeral literals;
     fun pretty _ thm _ _ _ [(t, _)] =
       (str o mk_numeral unbounded o implode_numeral thm negative c_pls c_min c_bit0 c_bit1) t;
   in (1, pretty) end;
 
-fun pretty_message c_char c_nibbles c_nil c_cons target =
+fun pretty_message c_char c_nibbles c_nil c_cons literals =
   let
-    val pretty_ops = pr_pretty target;
-    val mk_char = #pretty_char pretty_ops;
-    val mk_string = #pretty_string pretty_ops;
+    val mk_char = literal_char literals;
+    val mk_string = literal_string literals;
     fun pretty _ thm _ _ _ [(t, _)] =
       case implode_list c_nil c_cons t
        of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts
@@ -269,8 +206,6 @@
         | NONE => nerror thm "Illegal message expression";
   in (1, pretty) end;
 
-end; (*local*)
-
 
 (** theory data **)
 
@@ -308,7 +243,7 @@
   -> string list                        (*selected statements*)
   -> serialization;
 
-datatype serializer_entry = Serializer of serializer
+datatype serializer_entry = Serializer of serializer * literals
   | Extends of string * (Code_Thingol.program -> Code_Thingol.program);
 
 datatype target = Target of {
@@ -562,57 +497,67 @@
 fun add_syntax_constP target c = parse_syntax fst
   >> (add_syntax_const_cmd target c o Code_Printer.simple_const_syntax);
 
-fun add_pretty_list target nill cons thy =
+fun the_literals thy =
+  let
+    val (targets, _) = CodeTargetData.get thy;
+    fun literals target = case Symtab.lookup targets target
+     of SOME data => (case the_serializer data
+         of Serializer (_, literals) => literals
+          | Extends (super, _) => literals super)
+      | NONE => error ("Unknown code target language: " ^ quote target);
+  in literals end;
+
+fun add_literal_list target nill cons thy =
   let
     val nil' = Code_Name.const thy nill;
     val cons' = Code_Name.const thy cons;
-    val pr = pretty_list nil' cons' target;
-  in
-    thy
-    |> add_syntax_const target cons (SOME pr)
-  end;
-
-fun add_pretty_list_string target nill cons charr nibbles thy =
-  let
-    val nil' = Code_Name.const thy nill;
-    val cons' = Code_Name.const thy cons;
-    val charr' = Code_Name.const thy charr;
-    val nibbles' = map (Code_Name.const thy) nibbles;
-    val pr = pretty_list_string nil' cons' charr' nibbles' target;
+    val pr = pretty_list nil' cons' (the_literals thy target);
   in
     thy
     |> add_syntax_const target cons (SOME pr)
   end;
 
-fun add_pretty_char target charr nibbles thy =
+fun add_literal_list_string target nill cons charr nibbles thy =
+  let
+    val nil' = Code_Name.const thy nill;
+    val cons' = Code_Name.const thy cons;
+    val charr' = Code_Name.const thy charr;
+    val nibbles' = map (Code_Name.const thy) nibbles;
+    val pr = pretty_list_string nil' cons' charr' nibbles' (the_literals thy target);
+  in
+    thy
+    |> add_syntax_const target cons (SOME pr)
+  end;
+
+fun add_literal_char target charr nibbles thy =
   let
     val charr' = Code_Name.const thy charr;
     val nibbles' = map (Code_Name.const thy) nibbles;
-    val pr = pretty_char charr' nibbles' target;
+    val pr = pretty_char charr' nibbles' (the_literals thy target);
   in
     thy
     |> add_syntax_const target charr (SOME pr)
   end;
 
-fun add_pretty_numeral target unbounded negative number_of pls min bit0 bit1 thy =
+fun add_literal_numeral target unbounded negative number_of pls min bit0 bit1 thy =
   let
     val pls' = Code_Name.const thy pls;
     val min' = Code_Name.const thy min;
     val bit0' = Code_Name.const thy bit0;
     val bit1' = Code_Name.const thy bit1;
-    val pr = pretty_numeral unbounded negative pls' min' bit0' bit1' target;
+    val pr = pretty_numeral unbounded negative pls' min' bit0' bit1' (the_literals thy target);
   in
     thy
     |> add_syntax_const target number_of (SOME pr)
   end;
 
-fun add_pretty_message target charr nibbles nill cons str thy =
+fun add_literal_message target charr nibbles nill cons str thy =
   let
     val charr' = Code_Name.const thy charr;
     val nibbles' = map (Code_Name.const thy) nibbles;
     val nil' = Code_Name.const thy nill;
     val cons' = Code_Name.const thy cons;
-    val pr = pretty_message charr' nibbles' nil' cons' target;
+    val pr = pretty_message charr' nibbles' nil' cons' (the_literals thy target);
   in
     thy
     |> add_syntax_const target str (SOME pr)
@@ -658,7 +603,7 @@
           in (modify' #> modify, merge_target false target (data', data)) end
       end;
     val (modify, data) = collapse_hierarchy target;
-    val serializer = the_default (case the_serializer data
+    val (serializer, _) = the_default (case the_serializer data
      of Serializer seri => seri) alt_serializer;
     val reserved = the_reserved data;
     val includes = Symtab.dest (the_includes data);