git.iko.soy/Idris-dev
on master help sign in
Merge pull request #316 from bitlisp/default-bignums

Default to Integer instead of Int, and adjust fromInteger accordingly

commit41ca744dde4109f1bf5299b9219e98428c56b89a authorEdwin Brady <edwin.brady@gmail.com> dateSat 22 Jun 2013, 09:11 (13 years ago) parentb9156352fab1b2
14 files changed+66−68
compare with master
unifiedsplit
effects/Effect/Memory.idr+5−5 javascript/JavaScript.idr+1−1 lib/Builtins.idr+15−18 lib/Data/Bits.idr+13−13 lib/Data/Mod2.idr+2−2 lib/Data/Z.idr+3−3 lib/Prelude/Fin.idr+2−2 lib/Prelude/Nat.idr+5−2 lib/Prelude/Strings.idr+1−2 src/Idris/Parser.hs+12−13 test/reg005/reg005.idr+1−1 test/test015/test015.idr+1−1 test/test020/test020.idr+3−3 test/test025/test025.idr+2−2
effects/Effect/Memory.idr+5−5
@@ -39,7 +39,7 @@ data RawMemory : Effect where
3939private
4040do_malloc : Nat -> IOExcept String Ptr
4141do_malloc size with (fromInteger (cast size) == size)
42− | True = do ptr <- ioe_lift $ mkForeign (FFun "malloc" [FInt] FPtr) (cast size)
42+ | True = do ptr <- ioe_lift $ mkForeign (FFun "malloc" [FInt] FPtr) (fromInteger $ cast size)
4343 fail <- ioe_lift $ nullPtr ptr
4444 if fail then ioe_fail "Cannot allocate memory"
4545 else return ptr
@@ -49,7 +49,7 @@ private
4949do_memset : Ptr -> Nat -> Bits8 -> Nat -> IO ()
5050do_memset ptr offset c size
5151 = mkForeign (FFun "idris_memset" [FPtr, FInt, FChar, FInt] FUnit)
52− ptr (cast offset) c (cast size)
52+ ptr (fromInteger $ cast offset) c (fromInteger $ cast size)
5353
5454private
5555do_free : Ptr -> IO ()
@@ -59,13 +59,13 @@ private
5959do_memmove : Ptr -> Ptr -> Nat -> Nat -> Nat -> IO ()
6060do_memmove dest src dest_offset src_offset size
6161 = mkForeign (FFun "idris_memmove" [FPtr, FPtr, FInt, FInt, FInt] FUnit)
62− dest src (cast dest_offset) (cast src_offset) (cast size)
62+ dest src (fromInteger $ cast dest_offset) (fromInteger $ cast src_offset) (fromInteger $ cast size)
6363
6464private
6565do_peek : Ptr -> Nat -> (size : Nat) -> IO (Vect Bits8 size)
6666do_peek _ _ O = return (Prelude.Vect.Nil)
6767do_peek ptr offset (S n)
68− = do b <- mkForeign (FFun "idris_peek" [FPtr, FInt] FChar) ptr (cast offset)
68+ = do b <- mkForeign (FFun "idris_peek" [FPtr, FInt] FChar) ptr (fromInteger $ cast offset)
6969 bs <- do_peek ptr (S offset) n
7070 Prelude.Monad.return (Prelude.Vect.(::) b bs)
7171
@@ -73,7 +73,7 @@ private
7373do_poke : Ptr -> Nat -> Vect Bits8 size -> IO ()
7474do_poke _ _ [] = return ()
7575do_poke ptr offset (b::bs)
76− = do mkForeign (FFun "idris_poke" [FPtr, FInt, FChar] FUnit) ptr (cast offset) b
76+ = do mkForeign (FFun "idris_poke" [FPtr, FInt, FChar] FUnit) ptr (fromInteger $ cast offset) b
7777 do_poke ptr (S offset) bs
7878
7979instance Handler RawMemory (IOExcept String) where
javascript/JavaScript.idr+1−1
@@ -46,7 +46,7 @@ data NodeList : Type where
4646
4747elemAt : NodeList -> Nat -> IO (Maybe Element)
4848elemAt (MkNodeList p) i = do
49− e <- mkForeign (FFun ".item" [FPtr, FInt] FPtr) p (cast i)
49+ e <- mkForeign (FFun ".item" [FPtr, FInt] FPtr) p (prim__truncBigInt_Int (cast i))
5050 d <- isUndefined e
5151 if d
5252 then return $ Just (MkElem e)
lib/Builtins.idr+15−18
@@ -232,26 +232,23 @@ class Num a where
232232 (*) : a -> a -> a
233233
234234 abs : a -> a
235− fromInteger : Int -> a
235+ fromInteger : Integer -> a
236236
237+instance Num Integer where
238+ (+) = prim__addBigInt
239+ (-) = prim__subBigInt
240+ (*) = prim__mulBigInt
237241
242+ abs x = if x < 0 then -x else x
243+ fromInteger = id
238244
239245instance Num Int where
240246 (+) = prim__addInt
241247 (-) = prim__subInt
242248 (*) = prim__mulInt
243249
244− fromInteger = id
245− abs x = if x<0 then -x else x
246−
247−
248−instance Num Integer where
249− (+) = prim__addBigInt
250− (-) = prim__subBigInt
251− (*) = prim__mulBigInt
252−
253− abs x = if x<0 then -x else x
254− fromInteger = prim__sextInt_BigInt
250+ fromInteger = prim__truncBigInt_Int
251+ abs x = if x < (prim__truncBigInt_Int 0) then -x else x
255252
256253
257254instance Num Float where
@@ -259,16 +256,16 @@ instance Num Float where
259256 (-) = prim__subFloat
260257 (*) = prim__mulFloat
261258
262− abs x = if x<0 then -x else x
263− fromInteger = prim__toFloatInt
259+ abs x = if x < (prim__toFloatBigInt 0) then -x else x
260+ fromInteger = prim__toFloatBigInt
264261
265262partial
266−div : Int -> Int -> Int
267−div = prim__sdivInt
263+div : Integer -> Integer -> Integer
264+div = prim__sdivBigInt
268265
269266partial
270−mod : Int -> Int -> Int
271−mod = prim__sremInt
267+mod : Integer -> Integer -> Integer
268+mod = prim__sremBigInt
272269
273270
274271(/) : Float -> Float -> Float
lib/Data/Bits.idr+13−13
@@ -325,33 +325,33 @@ zeroExtend : Bits n -> Bits (n+m)
325325zeroExtend (MkBits x) = MkBits (zext' x)
326326
327327%assert_total
328−intToBits' : Int -> machineTy (nextBytes n)
328+intToBits' : Integer -> machineTy (nextBytes n)
329329intToBits' {n=n} x with (nextBytes n)
330330 | O = let pad = getPad {n=0} n in
331− prim__lshrB8 (prim__shlB8 (prim__truncInt_B8 x) pad) pad
331+ prim__lshrB8 (prim__shlB8 (prim__truncBigInt_B8 x) pad) pad
332332 | S O = let pad = getPad {n=1} n in
333− prim__lshrB16 (prim__shlB16 (prim__truncInt_B16 x) pad) pad
333+ prim__lshrB16 (prim__shlB16 (prim__truncBigInt_B16 x) pad) pad
334334 | S (S O) = let pad = getPad {n=2} n in
335− prim__lshrB32 (prim__shlB32 (prim__truncInt_B32 x) pad) pad
335+ prim__lshrB32 (prim__shlB32 (prim__truncBigInt_B32 x) pad) pad
336336 | S (S (S _)) = let pad = getPad {n=3} n in
337− prim__lshrB64 (prim__shlB64 (prim__truncInt_B64 x) pad) pad
337+ prim__lshrB64 (prim__shlB64 (prim__truncBigInt_B64 x) pad) pad
338338
339339public
340−intToBits : Int -> Bits n
340+intToBits : Integer -> Bits n
341341intToBits n = MkBits (intToBits' n)
342342
343−instance Cast Int (Bits n) where
343+instance Cast Integer (Bits n) where
344344 cast = intToBits
345345
346−bitsToInt' : machineTy (nextBytes n) -> Int
346+bitsToInt' : machineTy (nextBytes n) -> Integer
347347bitsToInt' {n=n} x with (nextBytes n)
348− | O = prim__zextB8_Int x
349− | S O = prim__zextB16_Int x
350− | S (S O) = prim__zextB32_Int x
351− | S (S (S _)) = prim__truncB64_Int x
348+ | O = prim__zextB8_BigInt x
349+ | S O = prim__zextB16_BigInt x
350+ | S (S O) = prim__zextB32_BigInt x
351+ | S (S (S _)) = prim__zextB64_BigInt x
352352
353353public
354−bitsToInt : Bits n -> Int
354+bitsToInt : Bits n -> Integer
355355bitsToInt (MkBits x) = bitsToInt' x
356356
357357-- Zero out the high bits of a truncated bitstring
lib/Data/Mod2.idr+2−2
@@ -25,7 +25,7 @@ rem = modBin urem
2525
2626%assert_total
2727public
28−intToMod : {n : Nat} -> Int -> Mod2 n
28+intToMod : {n : Nat} -> Integer -> Mod2 n
2929intToMod {n=n} x = MkMod2 (intToBits x)
3030
3131instance Eq (Mod2 n) where
@@ -56,7 +56,7 @@ modToStr x = pack (reverse (helper x))
5656 where
5757 %assert_total
5858 helper : Mod2 n -> List Char
59− helper x = strIndex "0123456789" (bitsToInt (cast (x `rem` 10)))
59+ helper x = strIndex "0123456789" (prim__truncBigInt_Int (bitsToInt (cast (x `rem` 10))))
6060 :: (if x < 10 then [] else helper (x `div` 10))
6161
6262
lib/Data/Z.idr+3−3
@@ -65,7 +65,7 @@ multZ (NegS n) (NegS m) = Pos $ (S n) * (S m)
6565multZ (NegS n) (Pos m) = negNat $ (S n) * m
6666multZ (Pos n) (NegS m) = negNat $ n * (S m)
6767
68−fromInt : Int -> Z
68+fromInt : Integer -> Z
6969fromInt n = if n < 0
7070 then NegS $ fromInteger {a=Nat} (-n - 1)
7171 else Pos $ fromInteger {a=Nat} n
@@ -80,11 +80,11 @@ instance Num Z where
8080 abs = cast . absZ
8181 fromInteger = fromInt
8282
83−instance Cast Z Int where
83+instance Cast Z Integer where
8484 cast (Pos n) = cast n
8585 cast (NegS n) = (-1) * (cast n + 1)
8686
87−instance Cast Int Z where
87+instance Cast Integer Z where
8888 cast = fromInteger
8989
9090
lib/Prelude/Fin.idr+2−2
@@ -19,11 +19,11 @@ finToNat (fS x) a = finToNat x (S a)
1919instance Cast (Fin n) Nat where
2020 cast x = finToNat x O
2121
22−finToInt : Fin n -> Int -> Int
22+finToInt : Fin n -> Integer -> Integer
2323finToInt fO a = a
2424finToInt (fS x) a = finToInt x (a + 1)
2525
26−instance Cast (Fin n) Int where
26+instance Cast (Fin n) Integer where
2727 cast x = finToInt x 0
2828
2929weaken : Fin n -> Fin (S n)
lib/Prelude/Nat.idr+5−2
@@ -107,7 +107,7 @@ instance Eq Nat where
107107 (S l) == (S r) = l == r
108108 _ == _ = False
109109
110−instance Cast Nat Int where
110+instance Cast Nat Integer where
111111 cast O = 0
112112 cast (S k) = 1 + cast k
113113
@@ -127,7 +127,7 @@ instance Num Nat where
127127 fromInteger x = fromInteger' x
128128 where
129129 %assert_total
130− fromInteger' : Int -> Nat
130+ fromInteger' : Integer -> Nat
131131 fromInteger' 0 = O
132132 fromInteger' n =
133133 if (n > 0) then
@@ -135,6 +135,9 @@ instance Num Nat where
135135 else
136136 O
137137
138+instance Cast Integer Nat where
139+ cast = fromInteger
140+
138141record Multiplicative : Type where
139142 getMultiplicative : Nat -> Multiplicative
140143
lib/Prelude/Strings.idr+1−2
@@ -116,5 +116,4 @@ unwords : List String -> String
116116unwords = pack . unwords' . map unpack
117117
118118length : String -> Nat
119−length = fromInteger . prim_lenString
120−
119+length = fromInteger . prim__zextInt_BigInt . prim_lenString
src/Idris/Parser.hs+12−13
@@ -808,22 +808,21 @@ pCaseOpt syn = do lhs <- pExpr (syn { inPattern = True })
808808
809809modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
810810modifyConst syn fc (PConstant (BI x))
811− | not (fitsInt x) = PAlternative False
812− [PConstant (BI x),
813− PApp fc (PRef fc (UN "fromInteger"))
814− [pexp (PConstant (I (fromInteger x)))]]
815811 | not (inPattern syn)
816812 = PAlternative False
817− [PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I (fromInteger x)))],
818− PConstant (I (fromInteger x)), PConstant (BI x)]
819− | otherwise = PAlternative False
820− [PConstant (I (fromInteger x)), PConstant (BI x)]
813+ (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI (fromInteger x)))]
814+ : consts)
815+ | otherwise = PAlternative False consts
816+ where
817+ consts = [ PConstant (BI x)
818+ , PConstant (I (fromInteger x))
819+ , PConstant (B8 (fromInteger x))
820+ , PConstant (B16 (fromInteger x))
821+ , PConstant (B32 (fromInteger x))
822+ , PConstant (B64 (fromInteger x))
823+ ]
821824modifyConst syn fc x = x
822825
823−fitsInt :: Integer -> Bool
824−fitsInt x = let xInt :: Int = fromInteger x
825− xInteger :: Integer = toInteger xInt in
826− x == xInteger
827826
828827pList syn = do lchar '['; fc <- pfc; xs <- sepBy (pExpr syn) (lchar ','); lchar ']'
829828 return (mkList fc xs)
@@ -1149,7 +1148,7 @@ pStatic = do lchar '['
11491148
11501149table fixes
11511150 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))
1152− [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I 0))]), pexp x])]]
1151+ [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI 0))]), pexp x])]]
11531152 ++ toTable (reverse fixes) ++
11541153 [[backtick],
11551154 [binary "=" PEq AssocLeft],
test/reg005/reg005.idr+1−1
@@ -29,7 +29,7 @@ compress : Vect Char n -> String
2929compress xs with (rle xs)
3030 compress Nil | REnd = ""
3131 compress (rep (S n) x ++ xs) | RChar _ _ rs
32− = let ni : Int = cast (S n) in
32+ = let ni : Integer = cast (S n) in
3333 show ni ++ show x ++ compress xs
3434
3535compressString : String -> String
test/test015/test015.idr+1−1
@@ -67,7 +67,7 @@ adc (numx # bx) (numy # by) carry
6767readNum : IO Nat
6868readNum = do putStr "Enter a number:"
6969 i <- getLine
70− let n : Int = cast i
70+ let n : Integer = cast i
7171 return (fromInteger n)
7272
7373main : IO ()
test/test020/test020.idr+3−3
@@ -1,7 +1,7 @@
11module Main
22
33implicit
4−natInt : Nat -> Int
4+natInt : Nat -> Integer
55natInt x = cast x
66
77implicit
@@ -12,10 +12,10 @@ forget (x :: xs) = x :: forget xs
1212foo : Vect a n -> List a
1313foo xs = reverse xs
1414
15−implicit intString : Int -> String
15+implicit intString : Integer -> String
1616intString = show
1717
18−test : Int -> String
18+test : Integer -> String
1919test x = "Number " ++ x
2020
2121main : IO ()
test/test025/test025.idr+2−2
@@ -21,9 +21,9 @@ testMemory = do Src :- allocate 5
2121 Dst :- initialize (prim__truncInt_B8 1) 2 oh
2222 move 2 2 3 oh oh
2323 Src :- free
24− end <- Dst :- peek 4 1 oh
24+ end <- Dst :- peek 4 (S O) oh
2525 Dst :- poke 4 (sub1 end) oh
26− res <- Dst :- peek 1 4 oh
26+ res <- Dst :- peek 1 (S(S(S(S O)))) oh
2727 Dst :- free
2828 return (map (prim__zextB8_Int) res)
2929