# HG changeset patch
# User haftmann
# Date 1279875493 -7200
# Node ID 844977c7abebe212e974d9d8f7aeb92ed33ab5f6
# Parent  be3c0df7bb90cc67398b61af1a70b842c923bd16
avoid unreliable Haskell Int type

diff -r be3c0df7bb90 -r 844977c7abeb src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Fri Jul 23 10:25:00 2010 +0200
+++ b/src/HOL/Code_Numeral.thy	Fri Jul 23 10:58:13 2010 +0200
@@ -298,7 +298,7 @@
 code_type code_numeral
   (SML "int")
   (OCaml "Big'_int.big'_int")
-  (Haskell "Int")
+  (Haskell "Integer")
   (Scala "Int")
 
 code_instance code_numeral :: eq
@@ -306,11 +306,9 @@
 
 setup {*
   fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
-    false Code_Printer.literal_naive_numeral) ["SML", "Haskell"]
-  #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
-    false Code_Printer.literal_numeral "OCaml"
-  #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
-    false Code_Printer.literal_naive_numeral "Scala"
+    false Code_Printer.literal_naive_numeral) ["SML", "Scala"]
+  #> fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
+    false Code_Printer.literal_numeral) ["OCaml", "Haskell"]
 *}
 
 code_reserved SML Int int
@@ -325,7 +323,7 @@
 code_const "subtract_code_numeral \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   (SML "Int.max/ (_/ -/ _,/ 0 : int)")
   (OCaml "Big'_int.max'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)/ Big'_int.zero'_big'_int")
-  (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
+  (Haskell "max/ (_/ -/ _)/ (0 :: Integer)")
   (Scala "!(_/ -/ _).max(0)")
 
 code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
diff -r be3c0df7bb90 -r 844977c7abeb src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 23 10:25:00 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 23 10:58:13 2010 +0200
@@ -433,28 +433,28 @@
 type RealWorld = Control.Monad.ST.RealWorld;
 type ST s a = Control.Monad.ST.ST s a;
 type STRef s a = Data.STRef.STRef s a;
-type STArray s a = Data.Array.ST.STArray s Int a;
+type STArray s a = Data.Array.ST.STArray s Integer a;
 
 newSTRef = Data.STRef.newSTRef;
 readSTRef = Data.STRef.readSTRef;
 writeSTRef = Data.STRef.writeSTRef;
 
-newArray :: Int -> a -> ST s (STArray s a);
+newArray :: Integer -> a -> ST s (STArray s a);
 newArray k = Data.Array.ST.newArray (0, k);
 
 newListArray :: [a] -> ST s (STArray s a);
-newListArray xs = Data.Array.ST.newListArray (0, length xs) xs;
+newListArray xs = Data.Array.ST.newListArray (0, toInteger (length xs)) xs;
 
-newFunArray :: Int -> (Int -> a) -> ST s (STArray s a);
+newFunArray :: Integer -> (Integer -> a) -> ST s (STArray s a);
 newFunArray k f = Data.Array.ST.newListArray (0, k) (map f [0..k-1]);
 
-lengthArray :: STArray s a -> ST s Int;
+lengthArray :: STArray s a -> ST s Integer;
 lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
 
-readArray :: STArray s a -> Int -> ST s a;
+readArray :: STArray s a -> Integer -> ST s a;
 readArray = Data.Array.ST.readArray;
 
-writeArray :: STArray s a -> Int -> a -> ST s ();
+writeArray :: STArray s a -> Integer -> a -> ST s ();
 writeArray = Data.Array.ST.writeArray;*}
 
 code_reserved Haskell Heap
diff -r be3c0df7bb90 -r 844977c7abeb src/HOL/Library/Code_Integer.thy
--- a/src/HOL/Library/Code_Integer.thy	Fri Jul 23 10:25:00 2010 +0200
+++ b/src/HOL/Library/Code_Integer.thy	Fri Jul 23 10:58:13 2010 +0200
@@ -112,7 +112,7 @@
 code_const Code_Numeral.int_of
   (SML "IntInf.fromInt")
   (OCaml "_")
-  (Haskell "toEnum")
+  (Haskell "_")
   (Scala "!BigInt((_))")
 
 text {* Evaluation *}
diff -r be3c0df7bb90 -r 844977c7abeb src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Fri Jul 23 10:25:00 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Fri Jul 23 10:58:13 2010 +0200
@@ -412,13 +412,13 @@
 code_const Code_Numeral.of_nat
   (SML "IntInf.toInt")
   (OCaml "_")
-  (Haskell "fromEnum")
+  (Haskell "toInteger")
   (Scala "!_.as'_Int")
 
 code_const Code_Numeral.nat_of
   (SML "IntInf.fromInt")
   (OCaml "_")
-  (Haskell "toEnum")
+  (Haskell "fromInteger")
   (Scala "Nat")
 
 text {* Using target language arithmetic operations whenever appropriate *}