src/Pure/Tools/codegen_serializer.ML

--- a/src/Pure/Tools/codegen_serializer.ML	Thu Jul 19 21:47:45 2007 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML	Thu Jul 19 21:47:46 2007 +0200
@@ -23,7 +23,7 @@
   val add_pretty_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 -> string * typ -> string -> string -> string
+  val add_pretty_numeral: string -> bool -> string * typ -> string -> string -> string
     -> string -> string -> theory -> theory;
   val add_pretty_ml_string: string -> string -> string list -> string
     -> string -> string -> theory -> theory;
@@ -1635,13 +1635,15 @@
 val pretty : (string * {
     pretty_char: string -> string,
     pretty_string: string -> string,
-    pretty_numeral: IntInf.int -> string,
+    pretty_numeral: bool -> IntInf.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 = ML_Syntax.print_string,
-      pretty_numeral = fn k => "(" ^ IntInf.toString k ^ " : IntInf.int)",
+      pretty_numeral = fn unbounded => fn k =>
+        if unbounded then "(" ^ IntInf.toString k ^ " : IntInf.int)"
+        else IntInf.toString k,
       pretty_list = Pretty.enum "," "[" "]",
       infix_cons = (7, "::")}),
   ("OCaml", { pretty_char = fn c => enclose "'" "'"
@@ -1651,11 +1653,15 @@
             else c
           end),
       pretty_string = (fn _ => error "OCaml: no pretty strings"),
-      pretty_numeral = fn k => if k >= IntInf.fromInt 0 then
-            "(Big_int.big_int_of_int " ^ IntInf.toString k ^ ")"
+      pretty_numeral = fn unbounded => fn k => if k >= IntInf.fromInt 0 then
+            if unbounded then
+              "(Big_int.big_int_of_int " ^ IntInf.toString k ^ ")"
+            else IntInf.toString k
           else
-            "(Big_int.big_int_of_int " ^ (enclose "(" ")" o prefix "-"
-              o IntInf.toString o op ~) k ^ ")",
+            if unbounded then
+              "(Big_int.big_int_of_int " ^ (enclose "(" ")" o prefix "-"
+                o IntInf.toString o op ~) k ^ ")"
+            else (enclose "(" ")" o prefix "-" o IntInf.toString o op ~) k,
       pretty_list = Pretty.enum ";" "[" "]",
       infix_cons = (6, "::")}),
   ("Haskell", { pretty_char = fn c => enclose "'" "'"
@@ -1665,7 +1671,7 @@
             else c
           end),
       pretty_string = ML_Syntax.print_string,
-      pretty_numeral = fn k => if k >= IntInf.fromInt 0 then
+      pretty_numeral = fn unbounded => fn k => if k >= IntInf.fromInt 0 then
             IntInf.toString k
           else
             (enclose "(" ")" o Library.prefix "-" o IntInf.toString o IntInf.~) k,
@@ -1719,12 +1725,12 @@
         | NONE => error "Illegal character expression";
   in (2, pretty) end;
 
-fun pretty_numeral c_bit0 c_bit1 c_pls c_min c_bit target =
+fun pretty_numeral unbounded c_bit0 c_bit1 c_pls c_min c_bit target =
   let
     val mk_numeral = #pretty_numeral (pr_pretty target);
     fun pretty _ _ _ [(t, _)] =
       case implode_numeral c_bit0 c_bit1 c_pls c_min c_bit t
-       of SOME k => (str o mk_numeral) k
+       of SOME k => (str o mk_numeral unbounded) k
         | NONE => error "Illegal numeral expression";
   in (1, pretty) end;
 
@@ -1994,7 +2000,7 @@
     |> add_syntax_const target charr' (SOME pr)
   end;
 
-fun add_pretty_numeral target number_of b0 b1 pls min bit thy =
+fun add_pretty_numeral target unbounded number_of b0 b1 pls min bit thy =
   let
     val number_of' = CodegenConsts.const_of_cexpr thy number_of;
     val (_, b0'') = idfs_of_const thy b0;
@@ -2002,7 +2008,7 @@
     val (_, pls'') = idfs_of_const thy pls;
     val (_, min'') = idfs_of_const thy min;
     val (_, bit'') = idfs_of_const thy bit;
-    val pr = pretty_numeral b0'' b1'' pls'' min'' bit'' target;
+    val pr = pretty_numeral unbounded b0'' b1'' pls'' min'' bit'' target;
   in
     thy
     |> add_syntax_const target number_of' (SOME pr)