avoid unreliable Haskell Int type
authorhaftmann
Fri Jul 23 10:58:13 2010 +0200 (2010-07-23)
changeset 37947844977c7abeb
parent 37946 be3c0df7bb90
child 37948 94e9302a7fd0
child 37960 e557d511c791
avoid unreliable Haskell Int type
src/HOL/Code_Numeral.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Library/Code_Integer.thy
src/HOL/Library/Efficient_Nat.thy
     1.1 --- a/src/HOL/Code_Numeral.thy	Fri Jul 23 10:25:00 2010 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Fri Jul 23 10:58:13 2010 +0200
     1.3 @@ -298,7 +298,7 @@
     1.4  code_type code_numeral
     1.5    (SML "int")
     1.6    (OCaml "Big'_int.big'_int")
     1.7 -  (Haskell "Int")
     1.8 +  (Haskell "Integer")
     1.9    (Scala "Int")
    1.10  
    1.11  code_instance code_numeral :: eq
    1.12 @@ -306,11 +306,9 @@
    1.13  
    1.14  setup {*
    1.15    fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
    1.16 -    false Code_Printer.literal_naive_numeral) ["SML", "Haskell"]
    1.17 -  #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
    1.18 -    false Code_Printer.literal_numeral "OCaml"
    1.19 -  #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
    1.20 -    false Code_Printer.literal_naive_numeral "Scala"
    1.21 +    false Code_Printer.literal_naive_numeral) ["SML", "Scala"]
    1.22 +  #> fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
    1.23 +    false Code_Printer.literal_numeral) ["OCaml", "Haskell"]
    1.24  *}
    1.25  
    1.26  code_reserved SML Int int
    1.27 @@ -325,7 +323,7 @@
    1.28  code_const "subtract_code_numeral \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
    1.29    (SML "Int.max/ (_/ -/ _,/ 0 : int)")
    1.30    (OCaml "Big'_int.max'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)/ Big'_int.zero'_big'_int")
    1.31 -  (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
    1.32 +  (Haskell "max/ (_/ -/ _)/ (0 :: Integer)")
    1.33    (Scala "!(_/ -/ _).max(0)")
    1.34  
    1.35  code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
     2.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 23 10:25:00 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 23 10:58:13 2010 +0200
     2.3 @@ -433,28 +433,28 @@
     2.4  type RealWorld = Control.Monad.ST.RealWorld;
     2.5  type ST s a = Control.Monad.ST.ST s a;
     2.6  type STRef s a = Data.STRef.STRef s a;
     2.7 -type STArray s a = Data.Array.ST.STArray s Int a;
     2.8 +type STArray s a = Data.Array.ST.STArray s Integer a;
     2.9  
    2.10  newSTRef = Data.STRef.newSTRef;
    2.11  readSTRef = Data.STRef.readSTRef;
    2.12  writeSTRef = Data.STRef.writeSTRef;
    2.13  
    2.14 -newArray :: Int -> a -> ST s (STArray s a);
    2.15 +newArray :: Integer -> a -> ST s (STArray s a);
    2.16  newArray k = Data.Array.ST.newArray (0, k);
    2.17  
    2.18  newListArray :: [a] -> ST s (STArray s a);
    2.19 -newListArray xs = Data.Array.ST.newListArray (0, length xs) xs;
    2.20 +newListArray xs = Data.Array.ST.newListArray (0, toInteger (length xs)) xs;
    2.21  
    2.22 -newFunArray :: Int -> (Int -> a) -> ST s (STArray s a);
    2.23 +newFunArray :: Integer -> (Integer -> a) -> ST s (STArray s a);
    2.24  newFunArray k f = Data.Array.ST.newListArray (0, k) (map f [0..k-1]);
    2.25  
    2.26 -lengthArray :: STArray s a -> ST s Int;
    2.27 +lengthArray :: STArray s a -> ST s Integer;
    2.28  lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
    2.29  
    2.30 -readArray :: STArray s a -> Int -> ST s a;
    2.31 +readArray :: STArray s a -> Integer -> ST s a;
    2.32  readArray = Data.Array.ST.readArray;
    2.33  
    2.34 -writeArray :: STArray s a -> Int -> a -> ST s ();
    2.35 +writeArray :: STArray s a -> Integer -> a -> ST s ();
    2.36  writeArray = Data.Array.ST.writeArray;*}
    2.37  
    2.38  code_reserved Haskell Heap
     3.1 --- a/src/HOL/Library/Code_Integer.thy	Fri Jul 23 10:25:00 2010 +0200
     3.2 +++ b/src/HOL/Library/Code_Integer.thy	Fri Jul 23 10:58:13 2010 +0200
     3.3 @@ -112,7 +112,7 @@
     3.4  code_const Code_Numeral.int_of
     3.5    (SML "IntInf.fromInt")
     3.6    (OCaml "_")
     3.7 -  (Haskell "toEnum")
     3.8 +  (Haskell "_")
     3.9    (Scala "!BigInt((_))")
    3.10  
    3.11  text {* Evaluation *}
     4.1 --- a/src/HOL/Library/Efficient_Nat.thy	Fri Jul 23 10:25:00 2010 +0200
     4.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Fri Jul 23 10:58:13 2010 +0200
     4.3 @@ -412,13 +412,13 @@
     4.4  code_const Code_Numeral.of_nat
     4.5    (SML "IntInf.toInt")
     4.6    (OCaml "_")
     4.7 -  (Haskell "fromEnum")
     4.8 +  (Haskell "toInteger")
     4.9    (Scala "!_.as'_Int")
    4.10  
    4.11  code_const Code_Numeral.nat_of
    4.12    (SML "IntInf.fromInt")
    4.13    (OCaml "_")
    4.14 -  (Haskell "toEnum")
    4.15 +  (Haskell "fromInteger")
    4.16    (Scala "Nat")
    4.17  
    4.18  text {* Using target language arithmetic operations whenever appropriate *}