f2f0e07 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Default to Integer instead of Int, and adjust fromInteger accordingly

commitf2f0e070540178df3562a865f0289efd2806001e authorBenjamin Saunders <besaunde@sfu.ca> dateFri 17 May 2013, 13:06 (13 years ago) parentb915635

9 files changed+46−48

compare with master

unifiedsplit

effects/Effect/Memory.idr+5−5 lib/Builtins.idr+15−18 lib/Data/Z.idr+3−3 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

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

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

33implicit

4−natInt : Nat -> Int

4+natInt : Nat -> Integer

55natInt x = cast x

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