robustifed infrastructure for complex term syntax during code generation

--- a/src/HOL/Tools/numeral.ML	Wed May 06 19:09:31 2009 +0200
+++ b/src/HOL/Tools/numeral.ML	Wed May 06 19:09:31 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/numeral.ML
-    ID:         $Id$
     Author:     Makarius
 
 Logical operations on numerals (see also HOL/hologic.ML).
@@ -59,13 +58,8 @@
 
 fun add_code number_of negative unbounded target thy =
   let
-    val pr_numeral = (Code_Printer.literal_numeral o Code_Target.the_literals thy) target;
-    fun dest_numeral naming thm =
+    fun dest_numeral pls' min' bit0' bit1' thm =
       let
-        val SOME pls' = Code_Thingol.lookup_const naming @{const_name Int.Pls};
-        val SOME min' = Code_Thingol.lookup_const naming @{const_name Int.Min};
-        val SOME bit0' = Code_Thingol.lookup_const naming @{const_name Int.Bit0};
-        val SOME bit1' = Code_Thingol.lookup_const naming @{const_name Int.Bit1};
         fun dest_bit (IConst (c, _)) = if c = bit0' then 0
               else if c = bit1' then 1
               else Code_Printer.nerror thm "Illegal numeral expression: illegal bit"
@@ -79,11 +73,12 @@
               in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
           | dest_num _ = Code_Printer.nerror thm "Illegal numeral expression: illegal term";
       in dest_num end;
-    fun pretty _ naming thm _ _ [(t, _)] =
-      (Code_Printer.str o pr_numeral unbounded o the_default 0 o dest_numeral naming thm) t;
+    fun pretty literals [pls', min', bit0', bit1'] _ thm _ _ [(t, _)] =
+      (Code_Printer.str o Code_Printer.literal_numeral literals unbounded
+        o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
   in
-    thy
-    |> Code_Target.add_syntax_const target number_of (SOME (1, pretty))
+    thy |>  Code_Target.add_syntax_const target number_of
+      (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min}, @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty)))
   end;
 
 end; (*local*)

--- a/src/Tools/code/code_printer.ML	Wed May 06 19:09:31 2009 +0200
+++ b/src/Tools/code/code_printer.ML	Wed May 06 19:09:31 2009 +0200
@@ -23,6 +23,17 @@
   val intro_vars: string list -> var_ctxt -> var_ctxt
   val lookup_var: var_ctxt -> string -> string
 
+  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
+
   type lrx
   val L: lrx
   val R: lrx
@@ -41,6 +52,7 @@
   type dict = Code_Thingol.dict
   type tyco_syntax
   type const_syntax
+  type proto_const_syntax
   val parse_infix: ('a -> 'b) -> lrx * int -> string
     -> int * ((fixity -> 'b -> Pretty.T)
     -> fixity -> 'a list -> Pretty.T)
@@ -48,26 +60,18 @@
     -> (int * ((fixity -> 'b -> Pretty.T)
     -> fixity -> 'a list -> Pretty.T)) option * OuterParse.token list
   val simple_const_syntax: (int * ((fixity -> iterm -> Pretty.T)
-    -> fixity -> (iterm * itype) list -> Pretty.T)) option -> const_syntax option
+    -> fixity -> (iterm * itype) list -> Pretty.T)) option -> proto_const_syntax option
+  val activate_const_syntax: theory -> literals
+    -> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming
   val gen_pr_app: (thm -> var_ctxt -> const * iterm list -> Pretty.T list)
     -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
-    -> (string -> const_syntax option) -> Code_Thingol.naming
+    -> (string -> const_syntax option)
     -> thm -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
   val gen_pr_bind: ((string option * Pretty.T option) * itype -> Pretty.T)
     -> (thm -> 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 mk_name_module: Name.context -> string option -> (string -> string option)
     -> 'a Graph.T -> string -> string
   val dest_name: string -> string * string
@@ -115,6 +119,25 @@
 val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
 
 
+(** 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;
+
+
 (** syntax printer **)
 
 (* binding priorities *)
@@ -158,17 +181,25 @@
 type tyco_syntax = int * ((fixity -> itype -> Pretty.T)
   -> fixity -> itype list -> Pretty.T);
 type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
-  -> Code_Thingol.naming -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
+  -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
+type proto_const_syntax = int * (string list * (literals -> string list
+  -> (var_ctxt -> fixity -> iterm -> Pretty.T)
+    -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T));
 
-fun simple_const_syntax x = (Option.map o apsnd)
-  (fn pretty => fn pr => fn naming => fn thm => fn vars => pretty (pr vars)) x;
+fun simple_const_syntax (SOME (n, f)) = SOME (n,
+      ([], (fn _ => fn _ => fn pr => fn thm => fn vars => f (pr vars))))
+  | simple_const_syntax NONE = NONE;
 
-fun gen_pr_app pr_app pr_term syntax_const naming thm vars fxy (app as ((c, (_, tys)), ts)) =
+fun activate_const_syntax thy literals (n, (cs, f)) naming =
+  fold_map (Code_Thingol.ensure_declared_const thy) cs naming
+  |-> (fn cs' => pair (n, f literals cs'));
+
+fun gen_pr_app pr_app pr_term syntax_const thm vars fxy (app as ((c, (_, tys)), ts)) =
   case syntax_const c
    of NONE => brackify fxy (pr_app thm vars app)
     | SOME (k, pr) =>
         let
-          fun pr' fxy ts = pr (pr_term thm) naming thm vars fxy (ts ~~ curry Library.take k tys);
+          fun pr' fxy ts = pr (pr_term thm) thm vars fxy (ts ~~ curry Library.take k tys);
         in if k = length ts
           then pr' fxy ts
         else if k < length ts
@@ -253,25 +284,6 @@
 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;
-
-
 (** module name spaces **)
 
 val dest_name =

--- a/src/Tools/code/code_target.ML	Wed May 06 19:09:31 2009 +0200
+++ b/src/Tools/code/code_target.ML	Wed May 06 19:09:31 2009 +0200
@@ -44,7 +44,7 @@
   val add_syntax_class: string -> class -> string option -> theory -> theory
   val add_syntax_inst: string -> string * class -> bool -> theory -> theory
   val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
-  val add_syntax_const: string -> string -> const_syntax option -> theory -> theory
+  val add_syntax_const: string -> string -> proto_const_syntax option -> theory -> theory
   val add_reserved: string -> string -> theory -> theory
 end;
 
@@ -86,7 +86,7 @@
   class: string Symtab.table,
   instance: unit Symreltab.table,
   tyco: tyco_syntax Symtab.table,
-  const: const_syntax Symtab.table
+  const: proto_const_syntax Symtab.table
 };
 
 fun mk_name_syntax_table ((class, instance), (tyco, const)) =
@@ -112,7 +112,6 @@
   -> (string -> string option)          (*class syntax*)
   -> (string -> tyco_syntax option)
   -> (string -> const_syntax option)
-  -> Code_Thingol.naming
   -> Code_Thingol.program
   -> string list                        (*selected statements*)
   -> serialization;
@@ -402,19 +401,34 @@
         val Code_Thingol.Datatype (tyco, _) = Graph.get_node program tyco
       in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end
 
-fun invoke_serializer thy abortable serializer reserved abs_includes 
+fun activate_syntax lookup_name src_tab = Symtab.empty
+  |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier
+       of SOME name => (SOME name,
+            Symtab.update_new (name, the (Symtab.lookup src_tab thing_identifier)) tab)
+        | NONE => (NONE, tab)) (Symtab.keys src_tab)
+  |>> map_filter I;
+
+fun activate_const_syntax thy literals src_tab naming = (Symtab.empty, naming)
+  |> fold_map (fn thing_identifier => fn (tab, naming) =>
+      case Code_Thingol.lookup_const naming thing_identifier
+       of SOME name => let
+              val (syn, naming') = Code_Printer.activate_const_syntax thy
+                literals (the (Symtab.lookup src_tab thing_identifier)) naming
+            in (SOME name, (Symtab.update_new (name, syn) tab, naming')) end
+        | NONE => (NONE, (tab, naming))) (Symtab.keys src_tab)
+  |>> map_filter I;
+
+fun invoke_serializer thy abortable serializer literals reserved abs_includes 
     module_alias class instance tyco const module args naming program2 names1 =
   let
-    fun distill_names lookup_name src_tab = Symtab.empty
-      |> fold_map (fn thing_identifier => fn tab => case lookup_name naming thing_identifier
-           of SOME name => (SOME name, Symtab.update_new (name, the (Symtab.lookup src_tab thing_identifier)) tab)
-            | NONE => (NONE, tab)) (Symtab.keys src_tab)
-      |>> map_filter I;
-    val (names_class, class') = distill_names Code_Thingol.lookup_class class;
+    val (names_class, class') =
+      activate_syntax (Code_Thingol.lookup_class naming) class;
     val names_inst = map_filter (Code_Thingol.lookup_instance naming)
       (Symreltab.keys instance);
-    val (names_tyco, tyco') = distill_names Code_Thingol.lookup_tyco tyco;
-    val (names_const, const') = distill_names Code_Thingol.lookup_const const;
+    val (names_tyco, tyco') =
+      activate_syntax (Code_Thingol.lookup_tyco naming) tyco;
+    val (names_const, (const', _)) =
+      activate_const_syntax thy literals const naming;
     val names_hidden = names_class @ names_inst @ names_tyco @ names_const;
     val names2 = subtract (op =) names_hidden names1;
     val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
@@ -429,7 +443,7 @@
     serializer module args (labelled_name thy program2) reserved includes
       (Symtab.lookup module_alias) (Symtab.lookup class')
       (Symtab.lookup tyco') (Symtab.lookup const')
-      naming program4 names2
+      program4 names2
   end;
 
 fun mount_serializer thy alt_serializer target module args naming program names =
@@ -460,8 +474,9 @@
       ((Symtab.dest o the_includes) data);
     val module_alias = the_module_alias data;
     val { class, instance, tyco, const } = the_name_syntax data;
+    val literals = the_literals thy target;
   in
-    invoke_serializer thy abortable serializer reserved
+    invoke_serializer thy abortable serializer literals reserved
       includes module_alias class instance tyco const module args naming (modify program) names
   end;