# HG changeset patch
# User haftmann
# Date 1243950785 -7200
# Node ID a48f9ef9de1559d6dd6d2dc5fe8ef0e16479c551
# Parent  4356b52b03f78e03f7bed3825f1a34628aef0851
OCaml builtin intergers are elusive; avoid

diff -r 4356b52b03f7 -r a48f9ef9de15 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Tue Jun 02 15:53:04 2009 +0200
+++ b/src/HOL/Code_Numeral.thy	Tue Jun 02 15:53:05 2009 +0200
@@ -279,7 +279,7 @@
 
 code_type code_numeral
   (SML "int")
-  (OCaml "int")
+  (OCaml "Big'_int.big'_int")
   (Haskell "Int")
 
 code_instance code_numeral :: eq
@@ -287,45 +287,46 @@
 
 setup {*
   fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
-    false false) ["SML", "OCaml", "Haskell"]
+    false false) ["SML", "Haskell"]
+  #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral} false true "OCaml"
 *}
 
 code_reserved SML Int int
-code_reserved OCaml Pervasives int
+code_reserved OCaml Big_int
 
 code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   (SML "Int.+/ ((_),/ (_))")
-  (OCaml "Pervasives.( + )")
+  (OCaml "Big'_int.add'_big'_int")
   (Haskell infixl 6 "+")
 
 code_const "subtract_code_numeral \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   (SML "Int.max/ (_/ -/ _,/ 0 : int)")
-  (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
+  (OCaml "Big'_int.max'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)/ Big'_int.zero'_big'_int")
   (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
 
 code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   (SML "Int.*/ ((_),/ (_))")
-  (OCaml "Pervasives.( * )")
+  (OCaml "Big'_int.mult'_big'_int")
   (Haskell infixl 7 "*")
 
 code_const div_mod_code_numeral
   (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
-  (OCaml "(fun n -> fun m ->/ if m = 0/ then (0, n) else/ (n '/ m, n mod m))")
+  (OCaml "(fun k -> fun l ->/ Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int k)/ (Big'_int.abs'_big'_int l))")
   (Haskell "divMod")
 
 code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   (SML "!((_ : Int.int) = _)")
-  (OCaml "!((_ : int) = _)")
+  (OCaml "Big'_int.eq'_big'_int")
   (Haskell infixl 4 "==")
 
 code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   (SML "Int.<=/ ((_),/ (_))")
-  (OCaml "!((_ : int) <= _)")
+  (OCaml "Big'_int.le'_big'_int")
   (Haskell infix 4 "<=")
 
 code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   (SML "Int.</ ((_),/ (_))")
-  (OCaml "!((_ : int) < _)")
+  (OCaml "Big'_int.lt'_big'_int")
   (Haskell infix 4 "<")
 
 end
diff -r 4356b52b03f7 -r a48f9ef9de15 src/HOL/Library/Code_Integer.thy
--- a/src/HOL/Library/Code_Integer.thy	Tue Jun 02 15:53:04 2009 +0200
+++ b/src/HOL/Library/Code_Integer.thy	Tue Jun 02 15:53:05 2009 +0200
@@ -93,11 +93,10 @@
 
 code_const Code_Numeral.int_of
   (SML "IntInf.fromInt")
-  (OCaml "Big'_int.big'_int'_of'_int")
+  (OCaml "_")
   (Haskell "toEnum")
 
 code_reserved SML IntInf
-code_reserved OCaml Big_int
 
 text {* Evaluation *}
 
diff -r 4356b52b03f7 -r a48f9ef9de15 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Tue Jun 02 15:53:04 2009 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jun 02 15:53:05 2009 +0200
@@ -371,12 +371,12 @@
 
 code_const Code_Numeral.of_nat
   (SML "IntInf.toInt")
-  (OCaml "Big'_int.int'_of'_big'_int")
+  (OCaml "_")
   (Haskell "fromEnum")
 
 code_const Code_Numeral.nat_of
   (SML "IntInf.fromInt")
-  (OCaml "Big'_int.big'_int'_of'_int")
+  (OCaml "_")
   (Haskell "toEnum")
 
 text {* Using target language arithmetic operations whenever appropriate *}
diff -r 4356b52b03f7 -r a48f9ef9de15 src/Tools/code/code_ml.ML
--- a/src/Tools/code/code_ml.ML	Tue Jun 02 15:53:04 2009 +0200
+++ b/src/Tools/code/code_ml.ML	Tue Jun 02 15:53:05 2009 +0200
@@ -444,7 +444,8 @@
               |>> (fn p => concat
                   [str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"])
             val (ps, vars') = fold_map pr binds vars;
-          in Pretty.chunks (ps @| pr_term is_closure thm vars' NOBR body) end
+            fun mk_brack (p :: ps) = Pretty.block [str "(", p] :: ps;
+          in Pretty.chunks (mk_brack ps @| Pretty.block [pr_term is_closure thm vars' NOBR body, str ")"]) end
       | pr_case is_closure thm vars fxy (((t, ty), clause :: clauses), _) =
           let
             fun pr delim (pat, body) =
@@ -649,7 +650,7 @@
               str ("type '" ^ v),
               (str o deresolve) class,
               str "=",
-              enum_default "();;" ";" "{" "};;" (
+              enum_default "unit;;" ";" "{" "};;" (
                 map pr_superclass_field superclasses
                 @ map pr_classparam_field classparams
               )
@@ -708,17 +709,17 @@
       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 bignum_ocaml k = if k <= 1073741823
+    then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
+    else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")"
 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 ^ ")"
+      if unbounded then bignum_ocaml 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 ^ ")"
+      if unbounded then "(Big_int.minus_big_int " ^ bignum_ocaml (~ k) ^ ")"
       else (enclose "(" ")" o prefix "-" o string_of_int o op ~) k,
   literal_list = Pretty.enum ";" "[" "]",
   infix_cons = (6, "::")