41ca744 · Idris-dev · git.iko.soy

effects/Effect/Memory.idr+5−5

compare with master

unifiedsplit

@@ -39,7 +39,7 @@ data RawMemory : Effect where

39private

40do_malloc : Nat -> IOExcept String Ptr

41do_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)

43 fail <- ioe_lift $ nullPtr ptr

44 if fail then ioe_fail "Cannot allocate memory"

45 else return ptr

@@ -49,7 +49,7 @@ private

49do_memset : Ptr -> Nat -> Bits8 -> Nat -> IO ()

50do_memset ptr offset c size

51 = 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)

53

54private

55do_free : Ptr -> IO ()

@@ -59,13 +59,13 @@ private

59do_memmove : Ptr -> Ptr -> Nat -> Nat -> Nat -> IO ()

60do_memmove dest src dest_offset src_offset size

61 = 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)

63

64private

65do_peek : Ptr -> Nat -> (size : Nat) -> IO (Vect Bits8 size)

66do_peek _ _ O = return (Prelude.Vect.Nil)

67do_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)

69 bs <- do_peek ptr (S offset) n

70 Prelude.Monad.return (Prelude.Vect.(::) b bs)

71

@@ -73,7 +73,7 @@ private

73do_poke : Ptr -> Nat -> Vect Bits8 size -> IO ()

74do_poke _ _ [] = return ()

75do_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

77 do_poke ptr (S offset) bs

78

79instance Handler RawMemory (IOExcept String) where

javascript/JavaScript.idr+1−1

@@ -46,7 +46,7 @@ data NodeList : Type where

46

47elemAt : NodeList -> Nat -> IO (Maybe Element)

48elemAt (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))

50 d <- isUndefined e

51 if d

52 then return $ Just (MkElem e)

lib/Builtins.idr+15−18

@@ -232,26 +232,23 @@ class Num a where

232 (*) : a -> a -> a

233

234 abs : a -> a

235− fromInteger : Int -> a

235+ fromInteger : Integer -> a

236

237+instance Num Integer where

238+ (+) = prim__addBigInt

239+ (-) = prim__subBigInt

240+ (*) = prim__mulBigInt

237

241

242+ abs x = if x < 0 then -x else x

243+ fromInteger = id

238

244

239instance Num Int where

245instance Num Int where

240 (+) = prim__addInt

246 (+) = prim__addInt

241 (-) = prim__subInt

247 (-) = prim__subInt

242 (*) = prim__mulInt

248 (*) = prim__mulInt

243

249

244− fromInteger = id

250+ fromInteger = prim__truncBigInt_Int

245− abs x = if x<0 then -x else x

251+ abs x = if x < (prim__truncBigInt_Int 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

255

252

256

253

257instance Num Float where

254instance Num Float where

@@ -259,16 +256,16 @@ instance Num Float where

259 (-) = prim__subFloat

256 (-) = prim__subFloat

260 (*) = prim__mulFloat

257 (*) = prim__mulFloat

261

258

262− abs x = if x<0 then -x else x

259+ abs x = if x < (prim__toFloatBigInt 0) then -x else x

263− fromInteger = prim__toFloatInt

260+ fromInteger = prim__toFloatBigInt

264

261

265partial

262partial

266−div : Int -> Int -> Int

263+div : Integer -> Integer -> Integer

267−div = prim__sdivInt

264+div = prim__sdivBigInt

268

265

269partial

266partial

270−mod : Int -> Int -> Int

267+mod : Integer -> Integer -> Integer

271−mod = prim__sremInt

268+mod = prim__sremBigInt

272

269

273

270

274(/) : Float -> Float -> Float

271(/) : Float -> Float -> Float

lib/Data/Bits.idr+13−13

@@ -325,33 +325,33 @@ zeroExtend : Bits n -> Bits (n+m)

325zeroExtend (MkBits x) = MkBits (zext' x)

326

327%assert_total

328−intToBits' : Int -> machineTy (nextBytes n)

328+intToBits' : Integer -> machineTy (nextBytes n)

329intToBits' {n=n} x with (nextBytes n)

330 | 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

332 | 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

334 | 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

336 | 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

338

339public

340−intToBits : Int -> Bits n

340+intToBits : Integer -> Bits n

341intToBits n = MkBits (intToBits' n)

342

343−instance Cast Int (Bits n) where

343+instance Cast Integer (Bits n) where

344 cast = intToBits

345

346−bitsToInt' : machineTy (nextBytes n) -> Int

346+bitsToInt' : machineTy (nextBytes n) -> Integer

347bitsToInt' {n=n} x with (nextBytes n)

348− | O = prim__zextB8_Int x

348+ | O = prim__zextB8_BigInt x

349− | S O = prim__zextB16_Int x

349+ | S O = prim__zextB16_BigInt x

350− | S (S O) = prim__zextB32_Int x

350+ | S (S O) = prim__zextB32_BigInt x

351− | S (S (S _)) = prim__truncB64_Int x

351+ | S (S (S _)) = prim__zextB64_BigInt x

352

353public

354−bitsToInt : Bits n -> Int

354+bitsToInt : Bits n -> Integer

355bitsToInt (MkBits x) = bitsToInt' x

356

357-- Zero out the high bits of a truncated bitstring

lib/Data/Mod2.idr+2−2

@@ -25,7 +25,7 @@ rem = modBin urem

25

26%assert_total

27public

28−intToMod : {n : Nat} -> Int -> Mod2 n

28+intToMod : {n : Nat} -> Integer -> Mod2 n

29intToMod {n=n} x = MkMod2 (intToBits x)

30

31instance Eq (Mod2 n) where

@@ -56,7 +56,7 @@ modToStr x = pack (reverse (helper x))

56 where

57 %assert_total

58 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))))

60 :: (if x < 10 then [] else helper (x `div` 10))

61

62

lib/Data/Z.idr+3−3

@@ -65,7 +65,7 @@ multZ (NegS n) (NegS m) = Pos $ (S n) * (S m)

65multZ (NegS n) (Pos m) = negNat $ (S n) * m

66multZ (Pos n) (NegS m) = negNat $ n * (S m)

67

68−fromInt : Int -> Z

68+fromInt : Integer -> Z

69fromInt n = if n < 0

70 then NegS $ fromInteger {a=Nat} (-n - 1)

71 else Pos $ fromInteger {a=Nat} n

@@ -80,11 +80,11 @@ instance Num Z where

80 abs = cast . absZ

81 fromInteger = fromInt

82

83−instance Cast Z Int where

83+instance Cast Z Integer where

84 cast (Pos n) = cast n

85 cast (NegS n) = (-1) * (cast n + 1)

86

87−instance Cast Int Z where

87+instance Cast Integer Z where

88 cast = fromInteger

89

90

lib/Prelude/Fin.idr+2−2

@@ -19,11 +19,11 @@ finToNat (fS x) a = finToNat x (S a)

19instance Cast (Fin n) Nat where

20 cast x = finToNat x O

21

22−finToInt : Fin n -> Int -> Int

22+finToInt : Fin n -> Integer -> Integer

23finToInt fO a = a

24finToInt (fS x) a = finToInt x (a + 1)

25

26−instance Cast (Fin n) Int where

26+instance Cast (Fin n) Integer where

27 cast x = finToInt x 0

28

29weaken : Fin n -> Fin (S n)

lib/Prelude/Nat.idr+5−2

@@ -107,7 +107,7 @@ instance Eq Nat where

107 (S l) == (S r) = l == r

108 _ == _ = False

109

110−instance Cast Nat Int where

110+instance Cast Nat Integer where

111 cast O = 0

112 cast (S k) = 1 + cast k

113

@@ -127,7 +127,7 @@ instance Num Nat where

127 fromInteger x = fromInteger' x

128 where

129 %assert_total

130− fromInteger' : Int -> Nat

130+ fromInteger' : Integer -> Nat

131 fromInteger' 0 = O

132 fromInteger' n =

133 if (n > 0) then

@@ -135,6 +135,9 @@ instance Num Nat where

135 else

136 O

137

138+instance Cast Integer Nat where

139+ cast = fromInteger

140+

138record Multiplicative : Type where

141record Multiplicative : Type where

139 getMultiplicative : Nat -> Multiplicative

142 getMultiplicative : Nat -> Multiplicative

140

143

lib/Prelude/Strings.idr+1−2

@@ -116,5 +116,4 @@ unwords : List String -> String

116unwords = pack . unwords' . map unpack

117

118length : String -> Nat

119−length = fromInteger . prim_lenString

119+length = fromInteger . prim__zextInt_BigInt . prim_lenString

120−

src/Idris/Parser.hs+12−13

@@ -808,22 +808,21 @@ pCaseOpt syn = do lhs <- pExpr (syn { inPattern = True })

808

809modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

810modifyConst 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)))]]

815 | not (inPattern syn)

811 | not (inPattern syn)

816 = PAlternative False

812 = PAlternative False

817− [PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I (fromInteger x)))],

813+ (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI (fromInteger x)))]

818− PConstant (I (fromInteger x)), PConstant (BI x)]

814+ : consts)

819− | otherwise = PAlternative False

815+ | otherwise = PAlternative False consts

816+ where

817+ consts = [ PConstant (BI x)

820− [PConstant (I (fromInteger x)), 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+ ]

821modifyConst syn fc x = x

824modifyConst syn fc x = x

822

825

823−fitsInt :: Integer -> Bool

824−fitsInt x = let xInt :: Int = fromInteger x

825− xInteger :: Integer = toInteger xInt in

826− x == xInteger

827

826

828pList syn = do lchar '['; fc <- pfc; xs <- sepBy (pExpr syn) (lchar ','); lchar ']'

827pList syn = do lchar '['; fc <- pfc; xs <- sepBy (pExpr syn) (lchar ','); lchar ']'

829 return (mkList fc xs)

828 return (mkList fc xs)

@@ -1149,7 +1148,7 @@ pStatic = do lchar '['

1149

1148

1150table fixes

1149table fixes

1151 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))

1150 = [[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])]]

1153 ++ toTable (reverse fixes) ++

1152 ++ toTable (reverse fixes) ++

1154 [[backtick],

1153 [[backtick],

1155 [binary "=" PEq AssocLeft],

1154 [binary "=" PEq AssocLeft],

test/reg005/reg005.idr+1−1

@@ -29,7 +29,7 @@ compress : Vect Char n -> String

29compress xs with (rle xs)

30 compress Nil | REnd = ""

31 compress (rep (S n) x ++ xs) | RChar _ _ rs

32− = let ni : Int = cast (S n) in

32+ = let ni : Integer = cast (S n) in

33 show ni ++ show x ++ compress xs

34

35compressString : String -> String

test/test015/test015.idr+1−1

@@ -67,7 +67,7 @@ adc (numx # bx) (numy # by) carry

67readNum : IO Nat

68readNum = do putStr "Enter a number:"

69 i <- getLine

70− let n : Int = cast i

70+ let n : Integer = cast i

71 return (fromInteger n)

72

73main : IO ()

test/test020/test020.idr+3−3

@@ -1,7 +1,7 @@

1module Main

2

3implicit

4−natInt : Nat -> Int

4+natInt : Nat -> Integer

5natInt x = cast x

6

7implicit

@@ -12,10 +12,10 @@ forget (x :: xs) = x :: forget xs

12foo : Vect a n -> List a

13foo xs = reverse xs

14

15−implicit intString : Int -> String

15+implicit intString : Integer -> String

16intString = show

17

18−test : Int -> String

18+test : Integer -> String

19test x = "Number " ++ x

20

21main : IO ()

test/test025/test025.idr+2−2

@@ -21,9 +21,9 @@ testMemory = do Src :- allocate 5

21 Dst :- initialize (prim__truncInt_B8 1) 2 oh

22 move 2 2 3 oh oh

23 Src :- free

24− end <- Dst :- peek 4 1 oh

24+ end <- Dst :- peek 4 (S O) oh

25 Dst :- poke 4 (sub1 end) oh

26− res <- Dst :- peek 1 4 oh

26+ res <- Dst :- peek 1 (S(S(S(S O)))) oh

27 Dst :- free

28 return (map (prim__zextB8_Int) res)

29