git.iko.soy/Idris-dev
on master help sign in
More Integer fixups
commit2fab1b21967bb041d79f372d39d4cdae4f738017 authorBenjamin Saunders <besaunde@sfu.ca> dateThu 20 Jun 2013, 08:49 (13 years ago) parentca9fce6
4 files changed+18−18
compare with master
unifiedsplit
javascript/JavaScript.idr+1−1 lib/Data/Bits.idr+13−13 lib/Data/Mod2.idr+2−2 lib/Prelude/Fin.idr+2−2
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/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/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)