f2f0e07 · 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

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/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/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 ()