af78968 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'unified-int-primitives-fix' of https://github.com/bitlisp/Idris-dev into bitlisp-unified-int-primitives-fix

af78968Edwin Brady13 years ago

effects/Effect/Memory.idr+4−4

compare with master

unifiedsplit

@@ -48,7 +48,7 @@ do_malloc size with (fromInteger (cast size) == size)

48private

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

50do_memset ptr offset c size

51− = mkForeign (FFun "idris_memset" [FPtr, FInt, FAny Bits8, FInt] FUnit)

51+ = mkForeign (FFun "idris_memset" [FPtr, FInt, FChar, FInt] FUnit)

52 ptr (cast offset) c (cast size)

54private

@@ -65,15 +65,15 @@ private

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] FInt) ptr (cast offset)

68+ = do b <- mkForeign (FFun "idris_peek" [FPtr, FInt] FChar) ptr (cast offset)

69 bs <- do_peek ptr (S offset) n

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

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

72private

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, FAny Bits8] FUnit) ptr (cast offset) b

76+ = do mkForeign (FFun "idris_poke" [FPtr, FInt, FChar] FUnit) ptr (cast offset) b

77 do_poke ptr (S offset) bs

79instance Handler RawMemory (IOExcept String) where

effects/Effect/Random.idr+7−7

@@ -3,19 +3,19 @@ module Effect.Random

3import Effects

5data Random : Type -> Type -> Type -> Type where

6− getRandom : Random Int Int Int

6+ getRandom : Random Integer Integer Integer

8using (m : Type -> Type)

9 instance Handler Random m where

10 handle seed getRandom k

11− = let seed' = 1664525 * seed + 1013904223 in

11+ = let seed' = (1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32) in

12 k seed' seed'

13−

13+

14RND : EFFECT

15−RND = MkEff Int Random

15+RND = MkEff Integer Random

17−rndInt : Int -> Int -> Eff m [RND] Int

17+rndInt : Integer -> Integer -> Eff m [RND] Integer

18−rndInt lower upper = do v <- getRandom

18+rndInt lower upper = do v <- getRandom

19− return (v `mod` (upper - lower) + lower)

19+ return (v `prim__sremBigInt` (upper - lower) + lower)

lib/Builtins.idr+4−4

@@ -251,7 +251,7 @@ instance Num Integer where

251 (*) = prim__mulBigInt

252

253 abs x = if x<0 then -x else x

254− fromInteger = prim__intToBigInt

254+ fromInteger = prim__sextInt_BigInt

255

256

257instance Num Float where

@@ -260,15 +260,15 @@ instance Num Float where

260 (*) = prim__mulFloat

261

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

263− fromInteger = prim__intToFloat

263+ fromInteger = prim__toFloatInt

264

265partial

266div : Int -> Int -> Int

267−div = prim__divInt

267+div = prim__sdivInt

268

269partial

270mod : Int -> Int -> Int

271−mod = prim__modInt

271+mod = prim__sremInt

272

273

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

lib/Data/Bits.idr+40−42

@@ -31,17 +31,17 @@ bitsUsed n = 8 * (2 `power` n)

31natToBits' : machineTy n -> Nat -> machineTy n

32natToBits' a O = a

33natToBits' {n=n} a x with n

34− natToBits' a (S x') | O = natToBits' (prim__addB8 a (prim__intToB8 1)) x'

34+ natToBits' a (S x') | O = natToBits' (prim__addB8 a (prim__truncInt_B8 1)) x'

35− natToBits' a (S x') | S O = natToBits' {n = S O} (prim__addB16 a (prim__intToB16 1)) x'

35+ natToBits' a (S x') | S O = natToBits' (prim__addB16 a (prim__truncInt_B16 1)) x'

36− natToBits' a (S x') | S (S O) = natToBits' {n=S (S O)} (prim__addB32 a (prim__intToB32 1)) x'

36+ natToBits' a (S x') | S (S O) = natToBits' (prim__addB32 a (prim__truncInt_B32 1)) x'

37− natToBits' a (S x') | S (S (S k)) = natToBits' {n = S (S (S k))} (prim__addB64 a (prim__intToB64 1)) x'

37+ natToBits' a (S x') | S (S (S _)) = natToBits' (prim__addB64 a (prim__truncInt_B64 1)) x'

39natToBits : Nat -> machineTy n

40natToBits {n=n} x with n

41− | O = natToBits' {n=O} (prim__intToB8 0) x

41+ | O = natToBits' (prim__truncInt_B8 0) x

42− | S O = natToBits' {n=S O} (prim__intToB16 0) x

42+ | S O = natToBits' (prim__truncInt_B16 0) x

43− | S (S O) = natToBits' {n=S (S O)} (prim__intToB32 0) x

43+ | S (S O) = natToBits' (prim__truncInt_B32 0) x

44− | S (S (S k)) = natToBits' {n=S (S (S k))} (prim__intToB64 0) x

44+ | S (S (S _)) = natToBits' (prim__truncInt_B64 0) x

46getPad : Nat -> machineTy n

47getPad n = natToBits ((bitsUsed (nextBytes n)) - n)

@@ -154,7 +154,6 @@ xor' {n=n} x y with n

154 | S (S O) = prim__xorB32 x y

155 | S (S (S _)) = prim__xorB64 x y

156

157−{-

158public

157public

159xor : Bits n -> Bits n -> Bits n

158xor : Bits n -> Bits n -> Bits n

160xor (MkBits x) (MkBits y) = MkBits (xor' x y)

159xor (MkBits x) (MkBits y) = MkBits (xor' x y)

@@ -310,14 +309,14 @@ complement (MkBits x) = MkBits (complement' x)

310zext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))

309zext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))

311zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

310zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

312 | (O, O) = believe_me x

311 | (O, O) = believe_me x

313− | (O, S O) = believe_me (prim__zextB8_16 (believe_me x))

312+ | (O, S O) = believe_me (prim__zextB8_B16 (believe_me x))

314− | (O, S (S O)) = believe_me (prim__zextB8_32 (believe_me x))

313+ | (O, S (S O)) = believe_me (prim__zextB8_B32 (believe_me x))

315− | (O, S (S (S _))) = believe_me (prim__zextB8_64 (believe_me x))

314+ | (O, S (S (S _))) = believe_me (prim__zextB8_B64 (believe_me x))

316 | (S O, S O) = believe_me x

315 | (S O, S O) = believe_me x

317− | (S O, S (S O)) = believe_me (prim__zextB16_32 (believe_me x))

316+ | (S O, S (S O)) = believe_me (prim__zextB16_B32 (believe_me x))

318− | (S O, S (S (S _))) = believe_me (prim__zextB16_64 (believe_me x))

317+ | (S O, S (S (S _))) = believe_me (prim__zextB16_B64 (believe_me x))

319 | (S (S O), S (S O)) = believe_me x

318 | (S (S O), S (S O)) = believe_me x

320− | (S (S O), S (S (S _))) = believe_me (prim__zextB32_64 (believe_me x))

319+ | (S (S O), S (S (S _))) = believe_me (prim__zextB32_B64 (believe_me x))

321 | (S (S (S _)), S (S (S _))) = believe_me x

320 | (S (S (S _)), S (S (S _))) = believe_me x

322

321

323public

322public

@@ -328,13 +327,13 @@ zeroExtend (MkBits x) = MkBits (zext' x)

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

327intToBits' : Int -> machineTy (nextBytes n)

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

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

330 | O = let pad = getPad {n=0} n in

329 | O = let pad = getPad {n=0} n in

331− prim__lshrB8 (prim__shlB8 (prim__intToB8 x) pad) pad

330+ prim__lshrB8 (prim__shlB8 (prim__truncInt_B8 x) pad) pad

332 | S O = let pad = getPad {n=1} n in

331 | S O = let pad = getPad {n=1} n in

333− prim__lshrB16 (prim__shlB16 (prim__intToB16 x) pad) pad

332+ prim__lshrB16 (prim__shlB16 (prim__truncInt_B16 x) pad) pad

334 | S (S O) = let pad = getPad {n=2} n in

333 | S (S O) = let pad = getPad {n=2} n in

335− prim__lshrB32 (prim__shlB32 (prim__intToB32 x) pad) pad

334+ prim__lshrB32 (prim__shlB32 (prim__truncInt_B32 x) pad) pad

336 | S (S (S _)) = let pad = getPad {n=3} n in

335 | S (S (S _)) = let pad = getPad {n=3} n in

337− prim__lshrB64 (prim__shlB64 (prim__intToB64 x) pad) pad

336+ prim__lshrB64 (prim__shlB64 (prim__truncInt_B64 x) pad) pad

338

337

339public

338public

340intToBits : Int -> Bits n

339intToBits : Int -> Bits n

@@ -345,10 +344,10 @@ instance Cast Int (Bits n) where

345

344

346bitsToInt' : machineTy n -> Int

345bitsToInt' : machineTy n -> Int

347bitsToInt' {n=n} x with n

346bitsToInt' {n=n} x with n

348− | O = prim__B32ToInt (prim__zextB8_32 x)

347+ | O = prim__zextB8_Int x

349− | S O = prim__B32ToInt (prim__zextB16_32 x)

348+ | S O = prim__zextB16_Int x

350− | S (S O) = prim__B32ToInt x

349+ | S (S O) = prim__zextB32_Int x

351− | S (S (S _)) = prim__B32ToInt (prim__truncB64_32 x)

350+ | S (S (S _)) = prim__truncB64_Int x

352

351

353public

352public

354bitsToInt : Bits n -> Int

353bitsToInt : Bits n -> Int

@@ -367,27 +366,27 @@ sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

367 | (O, O) = let pad = getPad {n=0} n in

366 | (O, O) = let pad = getPad {n=0} n in

368 believe_me (prim__ashrB8 (prim__shlB8 (believe_me x) pad) pad)

367 believe_me (prim__ashrB8 (prim__shlB8 (believe_me x) pad) pad)

369 | (O, S O) = let pad = getPad {n=0} n in

368 | (O, S O) = let pad = getPad {n=0} n in

370− believe_me (prim__ashrB16 (prim__sextB8_16 (prim__shlB8 (believe_me x) pad))

369+ believe_me (prim__ashrB16 (prim__sextB8_B16 (prim__shlB8 (believe_me x) pad))

371− (prim__zextB8_16 pad))

370+ (prim__zextB8_B16 pad))

372 | (O, S (S O)) = let pad = getPad {n=0} n in

371 | (O, S (S O)) = let pad = getPad {n=0} n in

373− believe_me (prim__ashrB32 (prim__sextB8_32 (prim__shlB8 (believe_me x) pad))

372+ believe_me (prim__ashrB32 (prim__sextB8_B32 (prim__shlB8 (believe_me x) pad))

374− (prim__zextB8_32 pad))

373+ (prim__zextB8_B32 pad))

375 | (O, S (S (S _))) = let pad = getPad {n=0} n in

374 | (O, S (S (S _))) = let pad = getPad {n=0} n in

376− believe_me (prim__ashrB64 (prim__sextB8_64 (prim__shlB8 (believe_me x) pad))

375+ believe_me (prim__ashrB64 (prim__sextB8_B64 (prim__shlB8 (believe_me x) pad))

377− (prim__zextB8_64 pad))

376+ (prim__zextB8_B64 pad))

378 | (S O, S O) = let pad = getPad {n=1} n in

377 | (S O, S O) = let pad = getPad {n=1} n in

379 believe_me (prim__ashrB16 (prim__shlB16 (believe_me x) pad) pad)

378 believe_me (prim__ashrB16 (prim__shlB16 (believe_me x) pad) pad)

380 | (S O, S (S O)) = let pad = getPad {n=1} n in

379 | (S O, S (S O)) = let pad = getPad {n=1} n in

381− believe_me (prim__ashrB32 (prim__sextB16_32 (prim__shlB16 (believe_me x) pad))

380+ believe_me (prim__ashrB32 (prim__sextB16_B32 (prim__shlB16 (believe_me x) pad))

382− (prim__zextB16_32 pad))

381+ (prim__zextB16_B32 pad))

383 | (S O, S (S (S _))) = let pad = getPad {n=1} n in

382 | (S O, S (S (S _))) = let pad = getPad {n=1} n in

384− believe_me (prim__ashrB64 (prim__sextB16_64 (prim__shlB16 (believe_me x) pad))

383+ believe_me (prim__ashrB64 (prim__sextB16_B64 (prim__shlB16 (believe_me x) pad))

385− (prim__zextB16_64 pad))

384+ (prim__zextB16_B64 pad))

386 | (S (S O), S (S O)) = let pad = getPad {n=2} n in

385 | (S (S O), S (S O)) = let pad = getPad {n=2} n in

387 believe_me (prim__ashrB32 (prim__shlB32 (believe_me x) pad) pad)

386 believe_me (prim__ashrB32 (prim__shlB32 (believe_me x) pad) pad)

388 | (S (S O), S (S (S _))) = let pad = getPad {n=2} n in

387 | (S (S O), S (S (S _))) = let pad = getPad {n=2} n in

389− believe_me (prim__ashrB64 (prim__sextB32_64 (prim__shlB32 (believe_me x) pad))

388+ believe_me (prim__ashrB64 (prim__sextB32_B64 (prim__shlB32 (believe_me x) pad))

390− (prim__zextB32_64 pad))

389+ (prim__zextB32_B64 pad))

391 | (S (S (S _)), S (S (S _))) = let pad = getPad {n=3} n in

390 | (S (S (S _)), S (S (S _))) = let pad = getPad {n=3} n in

392 believe_me (prim__ashrB64 (prim__shlB64 (believe_me x) pad) pad)

391 believe_me (prim__ashrB64 (prim__shlB64 (believe_me x) pad) pad)

393

392

@@ -399,14 +398,14 @@ signExtend {m=m} (MkBits x) = MkBits (zeroUnused (sext' x))

399trunc' : machineTy (nextBytes (n+m)) -> machineTy (nextBytes n)

398trunc' : machineTy (nextBytes (n+m)) -> machineTy (nextBytes n)

400trunc' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

399trunc' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

401 | (O, O) = believe_me x

400 | (O, O) = believe_me x

402− | (O, S O) = believe_me (prim__truncB16_8 (believe_me x))

401+ | (O, S O) = believe_me (prim__truncB16_B8 (believe_me x))

403− | (O, S (S O)) = believe_me (prim__truncB32_8 (believe_me x))

402+ | (O, S (S O)) = believe_me (prim__truncB32_B8 (believe_me x))

404− | (O, S (S (S _))) = believe_me (prim__truncB64_8 (believe_me x))

403+ | (O, S (S (S _))) = believe_me (prim__truncB64_B8 (believe_me x))

405 | (S O, S O) = believe_me x

404 | (S O, S O) = believe_me x

406− | (S O, S (S O)) = believe_me (prim__truncB32_16 (believe_me x))

405+ | (S O, S (S O)) = believe_me (prim__truncB32_B16 (believe_me x))

407− | (S O, S (S (S _))) = believe_me (prim__truncB64_16 (believe_me x))

406+ | (S O, S (S (S _))) = believe_me (prim__truncB64_B16 (believe_me x))

408 | (S (S O), S (S O)) = believe_me x

407 | (S (S O), S (S O)) = believe_me x

409− | (S (S O), S (S (S _))) = believe_me (prim__truncB64_32 (believe_me x))

408+ | (S (S O), S (S (S _))) = believe_me (prim__truncB64_B32 (believe_me x))

410 | (S (S (S _)), S (S (S _))) = believe_me x

409 | (S (S (S _)), S (S (S _))) = believe_me x

411

410

412public

411public

@@ -440,4 +439,3 @@ bitsToStr x = pack (helper last x)

440instance Show (Bits n) where

439instance Show (Bits n) where

441 show = bitsToStr

440 show = bitsToStr

442

441

443−-}

lib/Data/Mod2.idr−2

@@ -4,7 +4,6 @@ import Data.Bits

5%default total

7−{-

8-- Integers modulo 2^n

7-- Integers modulo 2^n

9public

8public

10data Mod2 : Nat -> Type where

9data Mod2 : Nat -> Type where

@@ -63,4 +62,3 @@ modToStr x = pack (reverse (helper x))

64instance Show (Mod2 n) where

63instance Show (Mod2 n) where

65 show = modToStr

64 show = modToStr

66−-}

lib/IO.idr+19−3

@@ -21,12 +21,28 @@ io_return x = prim__IO x

21run__IO : IO () -> IO ()

22run__IO v = io_bind v (\v' => io_return v')

24+data IntTy = ITNative | IT8 | IT16 | IT32 | IT64

26+

27+FInt : FTy

28+FInt = FIntT ITNative

29+

30+FChar : FTy

31+FChar = FIntT IT8

32+

33+FShort : FTy

34+FShort = FIntT IT16

35+

36+FLong : FTy

37+FLong = FIntT IT64

26interpFTy : FTy -> Type

39interpFTy : FTy -> Type

27−interpFTy FInt = Int

40+interpFTy (FIntT ITNative) = Int

41+interpFTy (FIntT IT8) = Bits8

42+interpFTy (FIntT IT16) = Bits16

43+interpFTy (FIntT IT32) = Bits32

44+interpFTy (FIntT IT64) = Bits64

28interpFTy FFloat = Float

45interpFTy FFloat = Float

29−interpFTy FChar = Char

30interpFTy FString = String

46interpFTy FString = String

31interpFTy FPtr = Ptr

47interpFTy FPtr = Ptr

32interpFTy (FAny t) = t

48interpFTy (FAny t) = t

lib/Network/Cgi.idr+1−1

@@ -121,7 +121,7 @@ abstract

121runCGI : CGI a -> IO a

122runCGI prog = do

123 clen_in <- getEnv "CONTENT_LENGTH"

124− let clen = prim__strToInt clen_in

124+ let clen = prim__fromStrInt clen_in

125 content <- getContent clen

126 query <- getEnv "QUERY_STRING"

127 cookie <- getEnv "HTTP_COOKIE"

lib/Prelude.idr+9−5

@@ -29,10 +29,10 @@ instance Show Nat where

29 show (S k) = "s" ++ show k

31instance Show Int where

32− show = prim__intToStr

32+ show = prim__toStrInt

34instance Show Integer where

35− show = prim__bigIntToStr

35+ show = prim__toStrBigInt

37instance Show Float where

38 show = prim__floatToStr

@@ -148,6 +148,10 @@ instance Monad List where

148%include "math.h"

149%lib "m"

150

151+pow : (Num a) => a -> Nat -> a

152+pow x O = 1

153+pow x (S n) = x * (pow x n)

154+

151exp : Float -> Float

155exp : Float -> Float

152exp x = prim__floatExp x

156exp x = prim__floatExp x

153

157

@@ -251,11 +255,11 @@ getLine = return (prim__readString prim__stdin)

251

255

252partial

256partial

253putChar : Char -> IO ()

257putChar : Char -> IO ()

254−putChar c = mkForeign (FFun "putchar" [FChar] FUnit) c

258+putChar c = mkForeign (FFun "putchar" [FInt] FUnit) (cast c)

255

259

256partial

260partial

257getChar : IO Char

261getChar : IO Char

258−getChar = mkForeign (FFun "getchar" [] FChar)

262+getChar = fmap cast $ mkForeign (FFun "getchar" [] FInt)

259

263

260---- some basic file handling

264---- some basic file handling

261

265

@@ -323,7 +327,7 @@ ferror (FHandle h) = do err <- do_ferror h

323

327

324partial

328partial

325nullPtr : Ptr -> IO Bool

329nullPtr : Ptr -> IO Bool

326−nullPtr p = do ok <- mkForeign (FFun "isNull" [FPtr] FInt) p

330+nullPtr p = do ok <- mkForeign (FFun "isNull" [FPtr] FInt) p

327 return (ok /= 0);

331 return (ok /= 0);

328

332

329partial

333partial

lib/Prelude/Cast.idr+7−7

@@ -6,24 +6,24 @@ class Cast from to where

6-- String casts

8instance Cast String Int where

9− cast = prim__strToInt

9+ cast = prim__fromStrInt

11instance Cast String Float where

12 cast = prim__strToFloat

14instance Cast String Integer where

15− cast = prim__strToBigInt

15+ cast = prim__fromStrBigInt

17-- Int casts

19instance Cast Int String where

20− cast = prim__intToStr

20+ cast = prim__toStrInt

22instance Cast Int Float where

23− cast = prim__intToFloat

23+ cast = prim__toFloatInt

25instance Cast Int Integer where

26− cast = prim__intToBigInt

26+ cast = prim__sextInt_BigInt

28instance Cast Int Char where

29 cast = prim__intToChar

@@ -34,12 +34,12 @@ instance Cast Float String where

34 cast = prim__floatToStr

36instance Cast Float Int where

37− cast = prim__floatToInt

37+ cast = prim__fromFloatInt

39-- Integer casts

41instance Cast Integer String where

42− cast = prim__bigIntToStr

42+ cast = prim__toStrBigInt

44-- Char casts

lib/base.ipkg+3−1

@@ -21,7 +21,9 @@ modules = Builtins, Prelude, IO, System,

22 Language.Reflection, Language.Reflection.Utils,

24+ Data.Morphisms,

24− Data.Morphisms, Data.Bits, Data.Mod2, Data.Z, Data.Sign,

25+-- Data.Bits, Data.Mod2,

26+ Data.Z, Data.Sign,

25 Data.SortedMap, Data.SortedSet, Data.BoundedList,

27 Data.SortedMap, Data.SortedSet, Data.BoundedList,

26 Data.Vect.Quantifiers,

28 Data.Vect.Quantifiers,

rts/idris_bitstring.c+28

@@ -60,6 +60,34 @@ VAL idris_castB32Int(VM *vm, VAL a) {

60 return MKINT((i_int)a->info.bits32);

61}

63+VAL idris_b8const(VM *vm, uint8_t a) {

64+ VAL cl = allocate(vm, sizeof(Closure), 0);

65+ SETTY(cl, BITS8);

66+ cl->info.bits8 = a;

67+ return cl;

68+}

69+

70+VAL idris_b16const(VM *vm, uint16_t a) {

71+ VAL cl = allocate(vm, sizeof(Closure), 0);

72+ SETTY(cl, BITS16);

73+ cl->info.bits16 = a;

74+ return cl;

75+}

76+

77+VAL idris_b32const(VM *vm, uint32_t a) {

78+ VAL cl = allocate(vm, sizeof(Closure), 0);

79+ SETTY(cl, BITS32);

80+ cl->info.bits32 = a;

81+ return cl;

82+}

83+

84+VAL idris_b64const(VM *vm, uint64_t a) {

85+ VAL cl = allocate(vm, sizeof(Closure), 0);

86+ SETTY(cl, BITS64);

87+ cl->info.bits64 = a;

88+ return cl;

89+}

90+

63VAL idris_b8Plus(VM *vm, VAL a, VAL b) {

91VAL idris_b8Plus(VM *vm, VAL a, VAL b) {

64 VAL cl = allocate(vm, sizeof(Closure), 0);

92 VAL cl = allocate(vm, sizeof(Closure), 0);

65 SETTY(cl, BITS8);

93 SETTY(cl, BITS8);

rts/idris_bitstring.h+4

@@ -11,6 +11,10 @@ VAL idris_b16(VM *vm, VAL a);

11VAL idris_b32(VM *vm, VAL a);

12VAL idris_b64(VM *vm, VAL a);

13VAL idris_castB32Int(VM *vm, VAL a);

14+VAL idris_b8const(VM *vm, uint8_t a);

15+VAL idris_b16const(VM *vm, uint16_t a);

16+VAL idris_b32const(VM *vm, uint32_t a);

17+VAL idris_b64const(VM *vm, uint64_t a);

15VAL idris_b8Plus(VM *vm, VAL a, VAL b);

19VAL idris_b8Plus(VM *vm, VAL a, VAL b);

16VAL idris_b8Minus(VM *vm, VAL a, VAL b);

20VAL idris_b8Minus(VM *vm, VAL a, VAL b);

rts/idris_gmp.c+28

@@ -52,6 +52,34 @@ VAL MKBIGMc(VM* vm, void* big) {

52 return cl;

53}

55+VAL MKBIGUI(VM* vm, unsigned long val) {

56+ mpz_t* bigint;

57+ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*) +

58+ sizeof(mpz_t), 0);

59+ bigint = (mpz_t*)(((char*)cl) + sizeof(ClosureType) + sizeof(void*));

60+

61+ mpz_init_set_ui(*bigint, val);

62+

63+ SETTY(cl, BIGINT);

64+ cl -> info.ptr = (void*)bigint;

65+

66+ return cl;

67+}

68+

69+VAL MKBIGSI(VM* vm, signed long val) {

70+ mpz_t* bigint;

71+ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*) +

72+ sizeof(mpz_t), 0);

73+ bigint = (mpz_t*)(((char*)cl) + sizeof(ClosureType) + sizeof(void*));

74+

75+ mpz_init_set_si(*bigint, val);

76+

77+ SETTY(cl, BIGINT);

78+ cl -> info.ptr = (void*)bigint;

79+

80+ return cl;

81+}

82+

55VAL GETBIG(VM * vm, VAL x) {

83VAL GETBIG(VM * vm, VAL x) {

56 if (ISINT(x)) {

84 if (ISINT(x)) {

57 mpz_t* bigint;

85 mpz_t* bigint;

rts/idris_gmp.h+2

@@ -5,6 +5,8 @@ VAL MKBIGI(int val);

5VAL MKBIGC(VM* vm, char* bigint);

6VAL MKBIGM(VM* vm, void* bigint);

7VAL MKBIGMc(VM* vm, void* bigint);

8+VAL MKBIGUI(VM* vm, unsigned long val);

9+VAL MKBIGSI(VM* vm, signed long val);

9VAL idris_bigPlus(VM*, VAL x, VAL y);

11VAL idris_bigPlus(VM*, VAL x, VAL y);

10VAL idris_bigMinus(VM*, VAL x, VAL y);

12VAL idris_bigMinus(VM*, VAL x, VAL y);

rts/idris_rts.c+6−7

@@ -271,17 +271,16 @@ void dumpVal(VAL v) {

271

272}

273

274−void idris_memset(void* ptr, i_int offset, VAL c, i_int size) {

274+void idris_memset(void* ptr, i_int offset, uint8_t c, i_int size) {

275− memset(((uint8_t*)ptr) + offset, c->info.bits8, size);

275+ memset(((uint8_t*)ptr) + offset, c, size);

276}

277

278−int idris_peek(void* ptr, i_int offset) {

278+uint8_t idris_peek(void* ptr, i_int offset) {

279− uint8_t res = *(((uint8_t*)ptr) + offset);

279+ return *(((uint8_t*)ptr) + offset);

280− return (int)res;

281}

280}

282

281

283−void idris_poke(void* ptr, i_int offset, VAL data) {

282+void idris_poke(void* ptr, i_int offset, uint8_t data) {

284− *(((uint8_t*)ptr) + offset) = data->info.bits8;

283+ *(((uint8_t*)ptr) + offset) = data;

285}

284}

286

285

287void idris_memmove(void* dest, void* src, i_int dest_offset, i_int src_offset, i_int size) {

286void idris_memmove(void* dest, void* src, i_int dest_offset, i_int src_offset, i_int size) {

rts/idris_rts.h+4−3

@@ -125,6 +125,7 @@ typedef intptr_t i_int;

125#define ISINT(x) ((((i_int)x)&1) == 1)

126

127#define INTOP(op,x,y) MKINT((i_int)((((i_int)x)>>1) op (((i_int)y)>>1)))

128+#define UINTOP(op,x,y) MKINT((i_int)((((uintptr_t)x)>>1) op (((uintptr_t)y)>>1)))

128#define FLOATOP(op,x,y) MKFLOAT(vm, ((GETFLOAT(x)) op (GETFLOAT(y))))

129#define FLOATOP(op,x,y) MKFLOAT(vm, ((GETFLOAT(x)) op (GETFLOAT(y))))

129#define FLOATBOP(op,x,y) MKINT((i_int)(((GETFLOAT(x)) op (GETFLOAT(y)))))

130#define FLOATBOP(op,x,y) MKINT((i_int)(((GETFLOAT(x)) op (GETFLOAT(y)))))

130#define ADD(x,y) (void*)(((i_int)x)+(((i_int)y)-1))

131#define ADD(x,y) (void*)(((i_int)x)+(((i_int)y)-1))

@@ -207,9 +208,9 @@ VAL idris_castFloatStr(VM* vm, VAL i);

207VAL idris_castStrFloat(VM* vm, VAL i);

208VAL idris_castStrFloat(VM* vm, VAL i);

208

209

209// Raw memory manipulation

210// Raw memory manipulation

210−void idris_memset(void* ptr, i_int offset, VAL c, i_int size);

211+void idris_memset(void* ptr, i_int offset, uint8_t c, i_int size);

211−int idris_peek(void* ptr, i_int offset);

212+uint8_t idris_peek(void* ptr, i_int offset);

212−void idris_poke(void* ptr, i_int offset, VAL data);

213+void idris_poke(void* ptr, i_int offset, uint8_t data);

213void idris_memmove(void* dest, void* src, i_int dest_offset, i_int src_offset, i_int size);

214void idris_memmove(void* dest, void* src, i_int dest_offset, i_int src_offset, i_int size);

214

215

215// String primitives

216// String primitives

src/Core/Execute.hs+34−14

@@ -3,6 +3,9 @@ module Core.Execute (execute) where

4import Idris.AbsSyntax

5import Idris.AbsSyntaxTree

6+import IRTS.Lang( IntTy(..)

7+ , intTyToConst

8+ , FType(..))

7import Core.TT

10import Core.TT

8import Core.Evaluate

11import Core.Evaluate

@@ -425,18 +428,16 @@ chooseAlt _ [] = Nothing

425

428

426

429

427

430

429−

430−idrisType :: FTy -> ExecVal

431+idrisType :: FType -> ExecVal

431idrisType FUnit = EP Ref unitTy EErased

432idrisType FUnit = EP Ref unitTy EErased

432idrisType ft = EConstant (idr ft)

433idrisType ft = EConstant (idr ft)

433− where idr FInt = IType

434+ where idr (FInt ty) = intTyToConst ty

434− idr FFloat = FlType

435+ idr FDouble = FlType

435 idr FChar = ChType

436 idr FChar = ChType

436 idr FString = StrType

437 idr FString = StrType

437 idr FPtr = PtrType

438 idr FPtr = PtrType

438

439

439−data Foreign = FFun String [FTy] FTy deriving Show

440+data Foreign = FFun String [FType] FType deriving Show

440

441

442

442call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)

443call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)

@@ -446,11 +447,19 @@ call (FFun name argTypes retType) args =

446 Nothing -> return Nothing

447 Nothing -> return Nothing

447 Just f -> do res <- call' f args retType

448 Just f -> do res <- call' f args retType

448 return . Just . ioWrap $ res

449 return . Just . ioWrap $ res

449− where call' :: ForeignFun -> [ExecVal] -> FTy -> Exec ExecVal

450+ where call' :: ForeignFun -> [ExecVal] -> FType -> Exec ExecVal

450− call' (Fun _ h) args FInt = do res <- execIO $ callFFI h retCInt (prepArgs args)

451+ call' (Fun _ h) args (FInt ITNative) = do res <- execIO $ callFFI h retCInt (prepArgs args)

451− return (EConstant (I (fromIntegral res)))

452+ return (EConstant (I (fromIntegral res)))

453+ call' (Fun _ h) args (FInt IT8) = do res <- execIO $ callFFI h retCChar (prepArgs args)

454+ return (EConstant (B8 (fromIntegral res)))

455+ call' (Fun _ h) args (FInt IT16) = do res <- execIO $ callFFI h retCWchar (prepArgs args)

456+ return (EConstant (B16 (fromIntegral res)))

457+ call' (Fun _ h) args (FInt IT32) = do res <- execIO $ callFFI h retCInt (prepArgs args)

458+ return (EConstant (B32 (fromIntegral res)))

459+ call' (Fun _ h) args (FInt IT64) = do res <- execIO $ callFFI h retCLong (prepArgs args)

460+ return (EConstant (B64 (fromIntegral res)))

452− call' (Fun _ h) args FFloat = do res <- execIO $ callFFI h retCDouble (prepArgs args)

461+ call' (Fun _ h) args FDouble = do res <- execIO $ callFFI h retCDouble (prepArgs args)

453− return (EConstant (Fl (realToFrac res)))

462+ return (EConstant (Fl (realToFrac res)))

454 call' (Fun _ h) args FChar = do res <- execIO $ callFFI h retCChar (prepArgs args)

463 call' (Fun _ h) args FChar = do res <- execIO $ callFFI h retCChar (prepArgs args)

455 return (EConstant (Ch (castCCharToChar res)))

464 return (EConstant (Ch (castCCharToChar res)))

456 call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)

465 call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)

@@ -467,6 +476,10 @@ call (FFun name argTypes retType) args =

467

476

468 prepArgs = map prepArg

477 prepArgs = map prepArg

469 prepArg (EConstant (I i)) = argCInt (fromIntegral i)

478 prepArg (EConstant (I i)) = argCInt (fromIntegral i)

479+ prepArg (EConstant (B8 i)) = argCChar (fromIntegral i)

480+ prepArg (EConstant (B16 i)) = argCWchar (fromIntegral i)

481+ prepArg (EConstant (B32 i)) = argCInt (fromIntegral i)

482+ prepArg (EConstant (B64 i)) = argCLong (fromIntegral i)

470 prepArg (EConstant (Fl f)) = argCDouble (realToFrac f)

483 prepArg (EConstant (Fl f)) = argCDouble (realToFrac f)

471 prepArg (EConstant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars

484 prepArg (EConstant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars

472 prepArg (EConstant (Str s)) = argString s

485 prepArg (EConstant (Str s)) = argString s

@@ -484,11 +497,18 @@ foreignFromTT t = case (unApplyV t) of

484 return $ FFun name argFTy retFTy

497 return $ FFun name argFTy retFTy

485 _ -> trace "failed to construct ffun" Nothing

498 _ -> trace "failed to construct ffun" Nothing

486

499

487−getFTy :: ExecVal -> Maybe FTy

500+getFTy :: ExecVal -> Maybe FType

501+getFTy (EApp (EP _ (UN "FIntT") _) (EP _ (UN intTy) _)) =

502+ case intTy of

503+ "ITNative" -> Just $ FInt ITNative

504+ "IT8" -> Just $ FInt IT8

505+ "IT16" -> Just $ FInt IT16

506+ "IT32" -> Just $ FInt IT32

507+ "IT64" -> Just $ FInt IT64

508+ _ -> Nothing

488getFTy (EP _ (UN t) _) =

509getFTy (EP _ (UN t) _) =

489 case t of

510 case t of

490− "FInt" -> Just FInt

491− "FFloat" -> Just FFloat

511+ "FFloat" -> Just FDouble

492 "FChar" -> Just FChar

512 "FChar" -> Just FChar

493 "FString" -> Just FString

513 "FString" -> Just FString

494 "FPtr" -> Just FPtr

514 "FPtr" -> Just FPtr

src/IRTS/CodegenC.hs+95−180

@@ -10,6 +10,7 @@ import Paths_idris

10import Util.System

12import Data.Char

13+import Data.List (intercalate)

13import System.Process

14import System.Process

14import System.Exit

15import System.Exit

15import System.IO

16import System.IO

@@ -105,10 +106,10 @@ bcc i (ASSIGNCONST l c)

105 mkConst (Fl f) = "MKFLOAT(vm, " ++ show f ++ ")"

106 mkConst (Fl f) = "MKFLOAT(vm, " ++ show f ++ ")"

106 mkConst (Ch c) = "MKINT(" ++ show (fromEnum c) ++ ")"

107 mkConst (Ch c) = "MKINT(" ++ show (fromEnum c) ++ ")"

107 mkConst (Str s) = "MKSTR(vm, " ++ show s ++ ")"

108 mkConst (Str s) = "MKSTR(vm, " ++ show s ++ ")"

108− mkConst (B8 b) = "MKB8(vm, " ++ show b ++")"

109+ mkConst (B8 x) = "idris_b8const(vm, " ++ show x ++ ")"

109− mkConst (B16 b) = "MKB16(vm, " ++ show b ++ ")"

110+ mkConst (B16 x) = "idris_b16const(vm, " ++ show x ++ ")"

110− mkConst (B32 b) = "MKB32(vm, " ++ show b ++ ")"

111+ mkConst (B32 x) = "idris_b32const(vm, " ++ show x ++ ")"

111− mkConst (B64 b) = "MKB64(vm, " ++ show b ++ ")"

112+ mkConst (B64 x) = "idris_b64const(vm, " ++ show x ++ ")"

112 mkConst _ = "MKINT(42424242)"

113 mkConst _ = "MKINT(42424242)"

113bcc i (UPDATE l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"

114bcc i (UPDATE l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"

114bcc i (MKCON l tag args)

115bcc i (MKCON l tag args)

@@ -226,7 +227,10 @@ bcc i (NULL r) = indent i ++ creg r ++ " = NULL;\n" -- clear, so it'll be GCed

226bcc i (ERROR str) = indent i ++ "fprintf(stderr, " ++ show str ++ "); assert(0); exit(-1);"

227bcc i (ERROR str) = indent i ++ "fprintf(stderr, " ++ show str ++ "); assert(0); exit(-1);"

227-- bcc i _ = indent i ++ "// not done yet\n"

228-- bcc i _ = indent i ++ "// not done yet\n"

228

229

230+

231+

229−c_irts FInt l x = l ++ "MKINT((i_int)(" ++ x ++ "))"

232+c_irts (FInt ITNative) l x = l ++ "MKINT((i_int)(" ++ x ++ "))"

233+c_irts (FInt ty) l x = l ++ "idris_b" ++ show (intTyWidth ty) ++ "const(vm, " ++ x ++ ")"

230c_irts FChar l x = l ++ "MKINT((i_int)(" ++ x ++ "))"

234c_irts FChar l x = l ++ "MKINT((i_int)(" ++ x ++ "))"

231c_irts FString l x = l ++ "MKSTR(vm, " ++ x ++ ")"

235c_irts FString l x = l ++ "MKSTR(vm, " ++ x ++ ")"

232c_irts FUnit l x = x

236c_irts FUnit l x = x

@@ -234,7 +238,8 @@ c_irts FPtr l x = l ++ "MKPTR(vm, " ++ x ++ ")"

234c_irts FDouble l x = l ++ "MKFLOAT(vm, " ++ x ++ ")"

238c_irts FDouble l x = l ++ "MKFLOAT(vm, " ++ x ++ ")"

235c_irts FAny l x = l ++ x

239c_irts FAny l x = l ++ x

236

240

237−irts_c FInt x = "GETINT(" ++ x ++ ")"

241+irts_c (FInt ITNative) x = "GETINT(" ++ x ++ ")"

242+irts_c (FInt ty) x = "(" ++ x ++ "->info.bits" ++ show (intTyWidth ty) ++ ")"

238irts_c FChar x = "GETINT(" ++ x ++ ")"

243irts_c FChar x = "GETINT(" ++ x ++ ")"

239irts_c FString x = "GETSTR(" ++ x ++ ")"

244irts_c FString x = "GETSTR(" ++ x ++ ")"

240irts_c FUnit x = x

245irts_c FUnit x = x

@@ -242,22 +247,33 @@ irts_c FPtr x = "GETPTR(" ++ x ++ ")"

242irts_c FDouble x = "GETFLOAT(" ++ x ++ ")"

247irts_c FDouble x = "GETFLOAT(" ++ x ++ ")"

243irts_c FAny x = x

248irts_c FAny x = x

244

249

250+bitOp v op ty args = v ++ "idris_b" ++ show (intTyWidth ty) ++ op ++ "(vm, " ++ intercalate ", " (map creg args) ++ ")"

251+

252+bitCoerce v op input output arg

253+ = v ++ "idris_b" ++ show (intTyWidth input) ++ op ++ show (intTyWidth output) ++ "(vm, " ++ creg arg ++ ")"

254+

255+signedTy :: IntTy -> String

256+signedTy t = "int" ++ show (intTyWidth t) ++ "_t"

257+

245−doOp v LPlus [l, r] = v ++ "ADD(" ++ creg l ++ ", " ++ creg r ++ ")"

258+doOp v (LPlus ITNative) [l, r] = v ++ "ADD(" ++ creg l ++ ", " ++ creg r ++ ")"

246−doOp v LMinus [l, r] = v ++ "INTOP(-," ++ creg l ++ ", " ++ creg r ++ ")"

259+doOp v (LMinus ITNative) [l, r] = v ++ "INTOP(-," ++ creg l ++ ", " ++ creg r ++ ")"

247−doOp v LTimes [l, r] = v ++ "MULT(" ++ creg l ++ ", " ++ creg r ++ ")"

260+doOp v (LTimes ITNative) [l, r] = v ++ "MULT(" ++ creg l ++ ", " ++ creg r ++ ")"

261+doOp v (LUDiv ITNative) [l, r] = v ++ "UINTOP(/," ++ creg l ++ ", " ++ creg r ++ ")"

248−doOp v LDiv [l, r] = v ++ "INTOP(/," ++ creg l ++ ", " ++ creg r ++ ")"

262+doOp v (LSDiv ITNative) [l, r] = v ++ "INTOP(/," ++ creg l ++ ", " ++ creg r ++ ")"

263+doOp v (LURem ITNative) [l, r] = v ++ "UINTOP(%," ++ creg l ++ ", " ++ creg r ++ ")"

249−doOp v LMod [l, r] = v ++ "INTOP(%," ++ creg l ++ ", " ++ creg r ++ ")"

264+doOp v (LSRem ITNative) [l, r] = v ++ "INTOP(%," ++ creg l ++ ", " ++ creg r ++ ")"

250−doOp v LAnd [l, r] = v ++ "INTOP(&," ++ creg l ++ ", " ++ creg r ++ ")"

265+doOp v (LAnd ITNative) [l, r] = v ++ "INTOP(&," ++ creg l ++ ", " ++ creg r ++ ")"

251−doOp v LOr [l, r] = v ++ "INTOP(|," ++ creg l ++ ", " ++ creg r ++ ")"

266+doOp v (LOr ITNative) [l, r] = v ++ "INTOP(|," ++ creg l ++ ", " ++ creg r ++ ")"

252−doOp v LXOr [l, r] = v ++ "INTOP(^," ++ creg l ++ ", " ++ creg r ++ ")"

267+doOp v (LXOr ITNative) [l, r] = v ++ "INTOP(^," ++ creg l ++ ", " ++ creg r ++ ")"

253−doOp v LSHL [l, r] = v ++ "INTOP(<<," ++ creg l ++ ", " ++ creg r ++ ")"

268+doOp v (LSHL ITNative) [l, r] = v ++ "INTOP(<<," ++ creg l ++ ", " ++ creg r ++ ")"

269+doOp v (LLSHR ITNative) [l, r] = v ++ "UINTOP(>>," ++ creg l ++ ", " ++ creg r ++ ")"

254−doOp v LSHR [l, r] = v ++ "INTOP(>>," ++ creg l ++ ", " ++ creg r ++ ")"

270+doOp v (LASHR ITNative) [l, r] = v ++ "INTOP(>>," ++ creg l ++ ", " ++ creg r ++ ")"

255−doOp v LCompl [x] = v ++ "INTOP(~," ++ creg x ++ ")"

271+doOp v (LCompl ITNative) [x] = v ++ "INTOP(~," ++ creg x ++ ")"

256−doOp v LEq [l, r] = v ++ "INTOP(==," ++ creg l ++ ", " ++ creg r ++ ")"

272+doOp v (LEq ITNative) [l, r] = v ++ "INTOP(==," ++ creg l ++ ", " ++ creg r ++ ")"

257−doOp v LLt [l, r] = v ++ "INTOP(<," ++ creg l ++ ", " ++ creg r ++ ")"

273+doOp v (LLt ITNative) [l, r] = v ++ "INTOP(<," ++ creg l ++ ", " ++ creg r ++ ")"

258−doOp v LLe [l, r] = v ++ "INTOP(<=," ++ creg l ++ ", " ++ creg r ++ ")"

274+doOp v (LLe ITNative) [l, r] = v ++ "INTOP(<=," ++ creg l ++ ", " ++ creg r ++ ")"

259−doOp v LGt [l, r] = v ++ "INTOP(>," ++ creg l ++ ", " ++ creg r ++ ")"

275+doOp v (LGt ITNative) [l, r] = v ++ "INTOP(>," ++ creg l ++ ", " ++ creg r ++ ")"

260−doOp v LGe [l, r] = v ++ "INTOP(>=," ++ creg l ++ ", " ++ creg r ++ ")"

276+doOp v (LGe ITNative) [l, r] = v ++ "INTOP(>=," ++ creg l ++ ", " ++ creg r ++ ")"

261

277

262doOp v LFPlus [l, r] = v ++ "FLOATOP(+," ++ creg l ++ ", " ++ creg r ++ ")"

278doOp v LFPlus [l, r] = v ++ "FLOATOP(+," ++ creg l ++ ", " ++ creg r ++ ")"

263doOp v LFMinus [l, r] = v ++ "FLOATOP(-," ++ creg l ++ ", " ++ creg r ++ ")"

279doOp v LFMinus [l, r] = v ++ "FLOATOP(-," ++ creg l ++ ", " ++ creg r ++ ")"

@@ -269,31 +285,30 @@ doOp v LFLe [l, r] = v ++ "FLOATBOP(<=," ++ creg l ++ ", " ++ creg r ++ ")"

269doOp v LFGt [l, r] = v ++ "FLOATBOP(>," ++ creg l ++ ", " ++ creg r ++ ")"

285doOp v LFGt [l, r] = v ++ "FLOATBOP(>," ++ creg l ++ ", " ++ creg r ++ ")"

270doOp v LFGe [l, r] = v ++ "FLOATBOP(>=," ++ creg l ++ ", " ++ creg r ++ ")"

286doOp v LFGe [l, r] = v ++ "FLOATBOP(>=," ++ creg l ++ ", " ++ creg r ++ ")"

271

287

272−doOp v LBPlus [l, r] = v ++ "idris_bigPlus(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

288+doOp v (LPlus ITBig) [l, r] = v ++ "idris_bigPlus(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

273−doOp v LBMinus [l, r] = v ++ "idris_bigMinus(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

289+doOp v (LMinus ITBig) [l, r] = v ++ "idris_bigMinus(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

274−doOp v LBDec [l] = v ++ "idris_bigMinus(vm, " ++ creg l ++ ", MKINT(1))"

275−doOp v LBTimes [l, r] = v ++ "idris_bigTimes(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

290+doOp v (LTimes ITBig) [l, r] = v ++ "idris_bigTimes(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

276−doOp v LBDiv [l, r] = v ++ "idris_bigDivide(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

291+doOp v (LSDiv ITBig) [l, r] = v ++ "idris_bigDivide(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

277−doOp v LBMod [l, r] = v ++ "idris_bigMod(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

292+doOp v (LSRem ITBig) [l, r] = v ++ "idris_bigMod(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

278−doOp v LBEq [l, r] = v ++ "idris_bigEq(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

293+doOp v (LEq ITBig) [l, r] = v ++ "idris_bigEq(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

279−doOp v LBLt [l, r] = v ++ "idris_bigLt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

294+doOp v (LLt ITBig) [l, r] = v ++ "idris_bigLt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

280−doOp v LBLe [l, r] = v ++ "idris_bigLe(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

295+doOp v (LLe ITBig) [l, r] = v ++ "idris_bigLe(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

281−doOp v LBGt [l, r] = v ++ "idris_bigGt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

296+doOp v (LGt ITBig) [l, r] = v ++ "idris_bigGt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

282−doOp v LBGe [l, r] = v ++ "idris_bigGe(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

297+doOp v (LGe ITBig) [l, r] = v ++ "idris_bigGe(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

283

298

284doOp v LStrConcat [l,r] = v ++ "idris_concat(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

299doOp v LStrConcat [l,r] = v ++ "idris_concat(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

285doOp v LStrLt [l,r] = v ++ "idris_strlt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

300doOp v LStrLt [l,r] = v ++ "idris_strlt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

286doOp v LStrEq [l,r] = v ++ "idris_streq(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

301doOp v LStrEq [l,r] = v ++ "idris_streq(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

287doOp v LStrLen [x] = v ++ "idris_strlen(vm, " ++ creg x ++ ")"

302doOp v LStrLen [x] = v ++ "idris_strlen(vm, " ++ creg x ++ ")"

288

303

289−doOp v LIntFloat [x] = v ++ "idris_castIntFloat(" ++ creg x ++ ")"

304+doOp v (LIntFloat ITNative) [x] = v ++ "idris_castIntFloat(" ++ creg x ++ ")"

290−doOp v LFloatInt [x] = v ++ "idris_castFloatInt(" ++ creg x ++ ")"

305+doOp v (LFloatInt ITNative) [x] = v ++ "idris_castFloatInt(" ++ creg x ++ ")"

291−doOp v LIntStr [x] = v ++ "idris_castIntStr(vm, " ++ creg x ++ ")"

292−doOp v LStrInt [x] = v ++ "idris_castStrInt(vm, " ++ creg x ++ ")"

293−doOp v LIntBig [x] = v ++ "idris_castIntBig(vm, " ++ creg x ++ ")"

306+doOp v (LSExt ITNative ITBig) [x] = v ++ "idris_castIntBig(vm, " ++ creg x ++ ")"

294−doOp v LBigInt [x] = v ++ "idris_castBigInt(vm, " ++ creg x ++ ")"

307+doOp v (LTrunc ITBig ITNative) [x] = v ++ "idris_castBigInt(vm, " ++ creg x ++ ")"

295−doOp v LStrBig [x] = v ++ "idris_castStrBig(vm, " ++ creg x ++ ")"

308+doOp v (LStrInt ITBig) [x] = v ++ "idris_castStrBig(vm, " ++ creg x ++ ")"

296−doOp v LBigStr [x] = v ++ "idris_castBigStr(vm, " ++ creg x ++ ")"

309+doOp v (LIntStr ITBig) [x] = v ++ "idris_castBigStr(vm, " ++ creg x ++ ")"

310+doOp v (LIntStr ITNative) [x] = v ++ "idris_castIntStr(vm, " ++ creg x ++ ")"

311+doOp v (LStrInt ITNative) [x] = v ++ "idris_castStrInt(vm, " ++ creg x ++ ")"

297doOp v LFloatStr [x] = v ++ "idris_castFloatStr(vm, " ++ creg x ++ ")"

312doOp v LFloatStr [x] = v ++ "idris_castFloatStr(vm, " ++ creg x ++ ")"

298doOp v LStrFloat [x] = v ++ "idris_castStrFloat(vm, " ++ creg x ++ ")"

313doOp v LStrFloat [x] = v ++ "idris_castStrFloat(vm, " ++ creg x ++ ")"

299

314

@@ -301,143 +316,43 @@ doOp v LReadStr [x] = v ++ "idris_readStr(vm, GETPTR(" ++ creg x ++ "))"

301doOp _ LPrintNum [x] = "printf(\"%ld\\n\", GETINT(" ++ creg x ++ "))"

316doOp _ LPrintNum [x] = "printf(\"%ld\\n\", GETINT(" ++ creg x ++ "))"

302doOp _ LPrintStr [x] = "fputs(GETSTR(" ++ creg x ++ "), stdout)"

317doOp _ LPrintStr [x] = "fputs(GETSTR(" ++ creg x ++ "), stdout)"

303

318

304−doOp v LIntB8 [x] = v ++ "idris_b8(vm, " ++ creg x ++ ")"

319+doOp v (LLt ty) [x, y] = bitOp v "Lt" ty [x, y]

305−doOp v LIntB16 [x] = v ++ "idris_b16(vm, " ++ creg x ++ ")"

320+doOp v (LLe ty) [x, y] = bitOp v "Lte" ty [x, y]

306−doOp v LIntB32 [x] = v ++ "idris_b32(vm, " ++ creg x ++ ")"

321+doOp v (LEq ty) [x, y] = bitOp v "Eq" ty [x, y]

307−doOp v LIntB64 [x] = v ++ "idris_b64(vm, " ++ creg x ++ ")"

322+doOp v (LGe ty) [x, y] = bitOp v "Gte" ty [x, y]

308−

323+doOp v (LGt ty) [x, y] = bitOp v "Gt" ty [x, y]

309−doOp v LB32Int [x] = v ++ "idris_castB32Int(vm, " ++ creg x ++ ")"

324+

310−

325+doOp v (LSHL ty) [x, y] = bitOp v "Shl" ty [x, y]

311−doOp v LB8Lt [x, y] = v ++ "idris_b8Lt(vm, " ++ creg x ++ "," ++ creg y ++ ")"

326+doOp v (LLSHR ty) [x, y] = bitOp v "Shr" ty [x, y]

312−doOp v LB8Lte [x, y] = v ++ "idris_b8Lte(vm, " ++ creg x ++ "," ++ creg y ++ ")"

327+doOp v (LASHR ty) [x, y] = bitOp v "AShr" ty [x, y]

313−doOp v LB8Eq [x, y] = v ++ "idris_b8Eq(vm, " ++ creg x ++ "," ++ creg y ++ ")"

328+doOp v (LAnd ty) [x, y] = bitOp v "And" ty [x, y]

314−doOp v LB8Gte [x, y] = v ++ "idris_b8Gte(vm, " ++ creg x ++ "," ++ creg y ++ ")"

329+doOp v (LOr ty) [x, y] = bitOp v "Or" ty [x, y]

315−doOp v LB8Gt [x, y] = v ++ "idris_b8Gt(vm, " ++ creg x ++ "," ++ creg y ++ ")"

330+doOp v (LXOr ty) [x, y] = bitOp v "Xor" ty [x, y]

316−

331+doOp v (LCompl ty) [x] = bitOp v "Compl" ty [x]

317−doOp v LB8Shl [x, y] = v ++ "idris_b8Shl(vm, " ++ creg x ++ "," ++ creg y ++ ")"

332+

318−doOp v LB8LShr [x, y] = v ++ "idris_b8Shr(vm, " ++ creg x ++ "," ++ creg y ++ ")"

333+doOp v (LPlus ty) [x, y] = bitOp v "Plus" ty [x, y]

319−doOp v LB8AShr [x, y] = v ++ "idris_b8AShr(vm, " ++ creg x ++ "," ++ creg y ++ ")"

334+doOp v (LMinus ty) [x, y] = bitOp v "Minus" ty [x, y]

320−doOp v LB8And [x, y] = v ++ "idris_b8And(vm, " ++ creg x ++ "," ++ creg y ++ ")"

335+doOp v (LTimes ty) [x, y] = bitOp v "Times" ty [x, y]

321−doOp v LB8Or [x, y] = v ++ "idris_b8Or(vm, " ++ creg x ++ "," ++ creg y ++ ")"

336+doOp v (LUDiv ty) [x, y] = bitOp v "UDiv" ty [x, y]

322−doOp v LB8Xor [x, y] = v ++ "idris_b8Xor(vm, " ++ creg x ++ "," ++ creg y ++ ")"

337+doOp v (LSDiv ty) [x, y] = bitOp v "SDiv" ty [x, y]

323−doOp v LB8Compl [x] = v ++ "idris_b8Compl(vm, " ++ creg x ++ ")"

338+doOp v (LURem ty) [x, y] = bitOp v "URem" ty [x, y]

324−

339+doOp v (LSRem ty) [x, y] = bitOp v "SRem" ty [x, y]

325−doOp v LB8Plus [x, y] = v ++ "idris_b8Plus(vm, " ++ creg x ++ "," ++ creg y ++ ")"

340+

326−doOp v LB8Minus [x, y] = v ++ "idris_b8Minus(vm, " ++ creg x ++ "," ++ creg y ++ ")"

341+doOp v (LSExt from ITBig) [x] = v ++ "MKBIGSI(vm, (" ++ signedTy from ++ ")" ++ creg x ++ "->info.bits" ++ show (intTyWidth from) ++ ")"

327−doOp v LB8Times [x, y] = v ++ "idris_b8Times(vm, " ++ creg x ++ "," ++ creg y ++ ")"

342+doOp v (LSExt ITNative to) [x] = v ++ "idris_b" ++ show (intTyWidth to) ++ "const(vm, GETINT(" ++ creg x ++ "))"

328−doOp v LB8UDiv [x, y] = v ++ "idris_b8UDiv(vm, " ++ creg x ++ "," ++ creg y ++ ")"

343+doOp v (LSExt from ITNative) [x] = v ++ "MKINT((i_int)((" ++ signedTy from ++ ")" ++ creg x ++ "->info.bits" ++ show (intTyWidth from) ++ "))"

329−doOp v LB8SDiv [x, y] = v ++ "idris_b8SDiv(vm, " ++ creg x ++ "," ++ creg y ++ ")"

344+doOp v (LSExt from to) [x]

330−doOp v LB8URem [x, y] = v ++ "idris_b8URem(vm, " ++ creg x ++ "," ++ creg y ++ ")"

345+ | intTyWidth from < intTyWidth to = bitCoerce v "S" from to x

331−doOp v LB8SRem [x, y] = v ++ "idris_b8SRem(vm, " ++ creg x ++ "," ++ creg y ++ ")"

346+doOp v (LZExt ITNative to) [x] = v ++ "idris_b" ++ show (intTyWidth to) ++ "const(vm, (uintptr_t)GETINT(" ++ creg x ++ ")"

332−

347+doOp v (LZExt from ITNative) [x] = v ++ "MKINT((i_int)" ++ creg x ++ "->info.bits" ++ show (intTyWidth from) ++ ")"

333−doOp v LB8Z16 [x] = v ++ "idris_b8Z16(vm, " ++ creg x ++ ")"

348+doOp v (LZExt from ITBig) [x] = v ++ "MKBIGUI(vm, " ++ creg x ++ "->info.bits" ++ show (intTyWidth from) ++ ")"

334−doOp v LB8Z32 [x] = v ++ "idris_b8Z32(vm, " ++ creg x ++ ")"

349+doOp v (LZExt from to) [x]

335−doOp v LB8Z64 [x] = v ++ "idris_b8Z64(vm, " ++ creg x ++ ")"

350+ | intTyWidth from < intTyWidth to = bitCoerce v "Z" from to x

336−doOp v LB8S16 [x] = v ++ "idris_b8S16(vm, " ++ creg x ++ ")"

351+doOp v (LTrunc ITNative to) [x] = v ++ "idris_b" ++ show (intTyWidth to) ++ "const(vm, GETINT(" ++ creg x ++ "))"

337−doOp v LB8S32 [x] = v ++ "idris_b8S32(vm, " ++ creg x ++ ")"

352+doOp v (LTrunc from ITNative) [x] = v ++ "MKINT((i_int)" ++ creg x ++ "->info.bits" ++ show (intTyWidth from) ++ ")"

338−doOp v LB8S64 [x] = v ++ "idris_b8S64(vm, " ++ creg x ++ ")"

353+doOp v (LTrunc ITBig to) [x] = v ++ "idris_b" ++ show (intTyWidth to) ++ "const(vm, mpz_get_ui(GETMPZ(" ++ creg x ++ "))"

339−

354+doOp v (LTrunc from to) [x]

340−doOp v LB16Lt [x, y] = v ++ "idris_b16Lt(vm, " ++ creg x ++ "," ++ creg y ++ ")"

355+ | intTyWidth from > intTyWidth to = bitCoerce v "T" from to x

341−doOp v LB16Lte [x, y] = v ++ "idris_b16Lte(vm, " ++ creg x ++ "," ++ creg y ++ ")"

342−doOp v LB16Eq [x, y] = v ++ "idris_b16Eq(vm, " ++ creg x ++ "," ++ creg y ++ ")"

343−doOp v LB16Gte [x, y] = v ++ "idris_b16Gte(vm, " ++ creg x ++ "," ++ creg y ++ ")"

344−doOp v LB16Gt [x, y] = v ++ "idris_b16Gt(vm, " ++ creg x ++ "," ++ creg y ++ ")"

345−

346−doOp v LB16Shl [x, y] = v ++ "idris_b16Shl(vm, " ++ creg x ++ "," ++ creg y ++ ")"

347−doOp v LB16LShr [x, y] = v ++ "idris_b16Shr(vm, " ++ creg x ++ "," ++ creg y ++ ")"

348−doOp v LB16AShr [x, y] = v ++ "idris_b16AShr(vm, " ++ creg x ++ "," ++ creg y ++ ")"

349−doOp v LB16And [x, y] = v ++ "idris_b16And(vm, " ++ creg x ++ "," ++ creg y ++ ")"

350−doOp v LB16Or [x, y] = v ++ "idris_b16Or(vm, " ++ creg x ++ "," ++ creg y ++ ")"

351−doOp v LB16Xor [x, y] = v ++ "idris_b16Xor(vm, " ++ creg x ++ "," ++ creg y ++ ")"

352−doOp v LB16Compl [x] = v ++ "idris_b16Compl(vm, " ++ creg x ++ ")"

353−

354−doOp v LB16Plus [x, y] =

355− v ++ "idris_b16Plus(vm, " ++ creg x ++ "," ++ creg y ++ ")"

356−doOp v LB16Minus [x, y] =

357− v ++ "idris_b16Minus(vm, " ++ creg x ++ "," ++ creg y ++ ")"

358−doOp v LB16Times [x, y] =

359− v ++ "idris_b16Times(vm, " ++ creg x ++ "," ++ creg y ++ ")"

360−doOp v LB16UDiv [x, y] =

361− v ++ "idris_b16UDiv(vm, " ++ creg x ++ "," ++ creg y ++ ")"

362−doOp v LB16SDiv [x, y] =

363− v ++ "idris_b16SDiv(vm, " ++ creg x ++ "," ++ creg y ++ ")"

364−doOp v LB16URem [x, y] =

365− v ++ "idris_b16URem(vm, " ++ creg x ++ "," ++ creg y ++ ")"

366−doOp v LB16SRem [x, y] =

367− v ++ "idris_b16SRem(vm, " ++ creg x ++ "," ++ creg y ++ ")"

368−

369−doOp v LB16Z32 [x] = v ++ "idris_b16Z32(vm, " ++ creg x ++ ")"

370−doOp v LB16Z64 [x] = v ++ "idris_b16Z64(vm, " ++ creg x ++ ")"

371−doOp v LB16S32 [x] = v ++ "idris_b16S32(vm, " ++ creg x ++ ")"

372−doOp v LB16S64 [x] = v ++ "idris_b16S64(vm, " ++ creg x ++ ")"

373−doOp v LB16T8 [x] = v ++ "idris_b16T8(vm, " ++ creg x ++ ")"

374−

375−doOp v LB32Lt [x, y] = v ++ "idris_b32Lt(vm, " ++ creg x ++ "," ++ creg y ++ ")"

376−doOp v LB32Lte [x, y] = v ++ "idris_b32Lte(vm, " ++ creg x ++ "," ++ creg y ++ ")"

377−doOp v LB32Eq [x, y] = v ++ "idris_b32Eq(vm, " ++ creg x ++ "," ++ creg y ++ ")"

378−doOp v LB32Gte [x, y] = v ++ "idris_b32Gte(vm, " ++ creg x ++ "," ++ creg y ++ ")"

379−doOp v LB32Gt [x, y] = v ++ "idris_b32Gt(vm, " ++ creg x ++ "," ++ creg y ++ ")"

380−

381−doOp v LB32Shl [x, y] = v ++ "idris_b32Shl(vm, " ++ creg x ++ "," ++ creg y ++ ")"

382−doOp v LB32LShr [x, y] = v ++ "idris_b32Shr(vm, " ++ creg x ++ "," ++ creg y ++ ")"

383−doOp v LB32AShr [x, y] = v ++ "idris_b32AShr(vm, " ++ creg x ++ "," ++ creg y ++ ")"

384−doOp v LB32And [x, y] = v ++ "idris_b32And(vm, " ++ creg x ++ "," ++ creg y ++ ")"

385−doOp v LB32Or [x, y] = v ++ "idris_b32Or(vm, " ++ creg x ++ "," ++ creg y ++ ")"

386−doOp v LB32Xor [x, y] = v ++ "idris_b32Xor(vm, " ++ creg x ++ "," ++ creg y ++ ")"

387−doOp v LB32Compl [x] = v ++ "idris_b32Compl(vm, " ++ creg x ++ ")"

388−

389−doOp v LB32Plus [x, y] =

390− v ++ "idris_b32Plus(vm, " ++ creg x ++ "," ++ creg y ++ ")"

391−doOp v LB32Minus [x, y] =

392− v ++ "idris_b32Minus(vm, " ++ creg x ++ "," ++ creg y ++ ")"

393−doOp v LB32Times [x, y] =

394− v ++ "idris_b32Times(vm, " ++ creg x ++ "," ++ creg y ++ ")"

395−doOp v LB32UDiv [x, y] =

396− v ++ "idris_b32UDiv(vm, " ++ creg x ++ "," ++ creg y ++ ")"

397−doOp v LB32SDiv [x, y] =

398− v ++ "idris_b32SDiv(vm, " ++ creg x ++ "," ++ creg y ++ ")"

399−doOp v LB32URem [x, y] =

400− v ++ "idris_b32URem(vm, " ++ creg x ++ "," ++ creg y ++ ")"

401−doOp v LB32SRem [x, y] =

402− v ++ "idris_b32SRem(vm, " ++ creg x ++ "," ++ creg y ++ ")"

403−

404−doOp v LB32Z64 [x] = v ++ "idris_b32Z64(vm, " ++ creg x ++ ")"

405−doOp v LB32S64 [x] = v ++ "idris_b32S64(vm, " ++ creg x ++ ")"

406−doOp v LB32T8 [x] = v ++ "idris_b32T8(vm, " ++ creg x ++ ")"

407−doOp v LB32T16 [x] = v ++ "idris_b32T16(vm, " ++ creg x ++ ")"

408−

409−doOp v LB64Lt [x, y] = v ++ "idris_b64Lt(vm, " ++ creg x ++ "," ++ creg y ++ ")"

410−doOp v LB64Lte [x, y] = v ++ "idris_b64Lte(vm, " ++ creg x ++ "," ++ creg y ++ ")"

411−doOp v LB64Eq [x, y] = v ++ "idris_b64Eq(vm, " ++ creg x ++ "," ++ creg y ++ ")"

412−doOp v LB64Gte [x, y] = v ++ "idris_b64Gte(vm, " ++ creg x ++ "," ++ creg y ++ ")"

413−doOp v LB64Gt [x, y] = v ++ "idris_b64Gt(vm, " ++ creg x ++ "," ++ creg y ++ ")"

414−

415−doOp v LB64Shl [x, y] = v ++ "idris_b64Shl(vm, " ++ creg x ++ "," ++ creg y ++ ")"

416−doOp v LB64LShr [x, y] = v ++ "idris_b64Shr(vm, " ++ creg x ++ "," ++ creg y ++ ")"

417−doOp v LB64AShr [x, y] = v ++ "idris_b64AShr(vm, " ++ creg x ++ "," ++ creg y ++ ")"

418−doOp v LB64And [x, y] = v ++ "idris_b64And(vm, " ++ creg x ++ "," ++ creg y ++ ")"

419−doOp v LB64Or [x, y] = v ++ "idris_b64Or(vm, " ++ creg x ++ "," ++ creg y ++ ")"

420−doOp v LB64Xor [x, y] = v ++ "idris_b64Xor(vm, " ++ creg x ++ "," ++ creg y ++ ")"

421−doOp v LB64Compl [x] = v ++ "idris_b64Compl(vm, " ++ creg x ++ ")"

422−

423−doOp v LB64Plus [x, y] =

424− v ++ "idris_b64Plus(vm, " ++ creg x ++ "," ++ creg y ++ ")"

425−doOp v LB64Minus [x, y] =

426− v ++ "idris_b64Minus(vm, " ++ creg x ++ "," ++ creg y ++ ")"

427−doOp v LB64Times [x, y] =

428− v ++ "idris_b64Times(vm, " ++ creg x ++ "," ++ creg y ++ ")"

429−doOp v LB64UDiv [x, y] =

430− v ++ "idris_b64UDiv(vm, " ++ creg x ++ "," ++ creg y ++ ")"

431−doOp v LB64SDiv [x, y] =

432− v ++ "idris_b64SDiv(vm, " ++ creg x ++ "," ++ creg y ++ ")"

433−doOp v LB64URem [x, y] =

434− v ++ "idris_b64URem(vm, " ++ creg x ++ "," ++ creg y ++ ")"

435−doOp v LB64SRem [x, y] =

436− v ++ "idris_b64SRem(vm, " ++ creg x ++ "," ++ creg y ++ ")"

437−

438−doOp v LB64T8 [x] = v ++ "idris_b64T8(vm, " ++ creg x ++ ")"

439−doOp v LB64T16 [x] = v ++ "idris_b64T16(vm, " ++ creg x ++ ")"

440−doOp v LB64T32 [x] = v ++ "idris_b64T32(vm, " ++ creg x ++ ")"

441

356

442doOp v LFExp [x] = v ++ "MKFLOAT(exp(GETFLOAT(" ++ creg x ++ ")))"

357doOp v LFExp [x] = v ++ "MKFLOAT(exp(GETFLOAT(" ++ creg x ++ ")))"

443doOp v LFLog [x] = v ++ "MKFLOAT(log(GETFLOAT(" ++ creg x ++ ")))"

358doOp v LFLog [x] = v ++ "MKFLOAT(log(GETFLOAT(" ++ creg x ++ ")))"

@@ -464,7 +379,7 @@ doOp v LStdErr [] = v ++ "MKPTR(vm, stderr)"

464doOp v LFork [x] = v ++ "MKPTR(vm, vmThread(vm, " ++ cname (MN 0 "EVAL") ++ ", " ++ creg x ++ "))"

379doOp v LFork [x] = v ++ "MKPTR(vm, vmThread(vm, " ++ cname (MN 0 "EVAL") ++ ", " ++ creg x ++ "))"

465doOp v LPar [x] = v ++ creg x -- "MKPTR(vm, vmThread(vm, " ++ cname (MN 0 "EVAL") ++ ", " ++ creg x ++ "))"

380doOp v LPar [x] = v ++ creg x -- "MKPTR(vm, vmThread(vm, " ++ cname (MN 0 "EVAL") ++ ", " ++ creg x ++ "))"

466doOp v LVMPtr [] = v ++ "MKPTR(vm, vm)"

381doOp v LVMPtr [] = v ++ "MKPTR(vm, vm)"

467−doOp v LChInt args = v ++ creg (last args)

382+doOp v (LChInt ITNative) args = v ++ creg (last args)

468−doOp v LIntCh args = v ++ creg (last args)

383+doOp v (LIntCh ITNative) args = v ++ creg (last args)

469doOp v LNoOp args = v ++ creg (last args)

384doOp v LNoOp args = v ++ creg (last args)

470doOp _ op _ = "FAIL /* " ++ show op ++ " */"

385doOp _ op _ = "FAIL /* " ++ show op ++ " */"

src/IRTS/CodegenJava.hs+142−215

@@ -16,6 +16,7 @@ import Control.Monad.Trans.State

16import Data.Char

17import Data.Maybe (fromJust)

18import Data.List (isPrefixOf, isSuffixOf, intercalate, foldl')

19+import Data.Int

19import qualified Data.Text as T

20import qualified Data.Text as T

20import qualified Data.Text.IO as TIO

21import qualified Data.Text.IO as TIO

21import Language.Java.Parser

22import Language.Java.Parser

@@ -468,7 +469,39 @@ integerType :: ClassType

468integerType = ClassType [(Ident "Integer", [])]

469integerType = ClassType [(Ident "Integer", [])]

469

470

470longType :: ClassType

471longType :: ClassType

471−longType = ClassType [(Ident "Integer", [])]

472+longType = ClassType [(Ident "Long", [])]

473+

474+nextIntTy :: IntTy -> IntTy

475+nextIntTy IT8 = IT16

476+nextIntTy IT16 = IT32

477+nextIntTy IT32 = IT64

478+nextIntTy IT64 = IT64

479+nextIntTy ITNative = IT64

480+

481+intTyToIdent :: IntTy -> Ident

482+intTyToIdent IT8 = Ident "Byte"

483+intTyToIdent IT16 = Ident "Short"

484+intTyToIdent IT32 = Ident "Integer"

485+intTyToIdent IT64 = Ident "Long"

486+intTyToIdent ITNative = Ident "Integer"

487+intTyToIdent ITBig = Ident "BigInteger"

488+

489+intTyToClass :: IntTy -> ClassType

490+intTyToClass ty = ClassType [(intTyToIdent ty, [])]

491+

492+intTyToMethod :: IntTy -> String

493+intTyToMethod IT8 = "byteValue"

494+intTyToMethod IT16 = "shortValue"

495+intTyToMethod IT32 = "intValue"

496+intTyToMethod IT64 = "longValue"

497+intTyToMethod ITNative = "intValue"

498+

499+intTyToPrimTy :: IntTy -> PrimType

500+intTyToPrimTy IT8 = ByteT

501+intTyToPrimTy IT16 = ShortT

502+intTyToPrimTy IT32 = IntT

503+intTyToPrimTy IT64 = LongT

504+intTyToPrimTy ITNative = IntT

472

505

473bigIntegerType :: ClassType

506bigIntegerType :: ClassType

474bigIntegerType = ClassType [(Ident "BigInteger", [])]

507bigIntegerType = ClassType [(Ident "BigInteger", [])]

@@ -962,7 +995,7 @@ mkStringAtIndex var indexExp =

962 <$> mkVarAccess (Just stringType) var

995 <$> mkVarAccess (Just stringType) var

963

996

964mkForeignType :: FType -> Maybe ClassType

997mkForeignType :: FType -> Maybe ClassType

965−mkForeignType FInt = return integerType

998+mkForeignType (FInt ty) = return (intTyToClass ty)

966mkForeignType FChar = return integerType

999mkForeignType FChar = return integerType

967mkForeignType FString = return stringType

1000mkForeignType FString = return stringType

968mkForeignType FPtr = return objectType

1001mkForeignType FPtr = return objectType

@@ -971,14 +1004,14 @@ mkForeignType FAny = return objectType

971mkForeignType FUnit = Nothing

1004mkForeignType FUnit = Nothing

972

1005

973mkForeignVarAccess :: FType -> LVar -> CodeGeneration Exp

1006mkForeignVarAccess :: FType -> LVar -> CodeGeneration Exp

974−mkForeignVarAccess FInt var =

1007+mkForeignVarAccess (FInt ty) var =

975− (\ var -> MethodInv $ PrimaryMethodCall (var)

1008+ (\ var -> MethodInv $ PrimaryMethodCall var

976 []

1009 []

977− (Ident "intValue")

1010+ (Ident (intTyToMethod ty))

978 []

1011 []

979 )

1012 )

980− <$> mkVarAccess (Just integerType) var

1013+ <$> mkVarAccess (Just $ intTyToClass ty) var

981−mkForeignVarAccess FChar var = Cast (PrimType CharT) <$> mkForeignVarAccess FInt var

1014+mkForeignVarAccess FChar var = Cast (PrimType CharT) <$> mkForeignVarAccess (FInt IT32) var

982mkForeignVarAccess FDouble var =

1015mkForeignVarAccess FDouble var =

983 (\ var -> MethodInv $ PrimaryMethodCall (var)

1016 (\ var -> MethodInv $ PrimaryMethodCall (var)

984 []

1017 []

@@ -989,12 +1022,12 @@ mkForeignVarAccess FDouble var =

989mkForeignVarAccess otherType var = mkVarAccess (mkForeignType otherType) var

1022mkForeignVarAccess otherType var = mkVarAccess (mkForeignType otherType) var

990

1023

991mkFromForeignType :: FType -> Exp -> Exp

1024mkFromForeignType :: FType -> Exp -> Exp

992−mkFromForeignType FInt from =

1025+mkFromForeignType (FInt ty) from =

993− MethodInv $ TypeMethodCall (J.Name [Ident "Integer"])

1026+ MethodInv $ TypeMethodCall (J.Name [intTyToIdent ty])

994 []

1027 []

995 (Ident "valueOf")

1028 (Ident "valueOf")

996 [from]

1029 [from]

997−mkFromForeignType FChar from = mkFromForeignType FInt from

1030+mkFromForeignType FChar from = mkFromForeignType (FInt IT32) from

998mkFromForeignType FDouble from =

1031mkFromForeignType FDouble from =

999 MethodInv $ TypeMethodCall (J.Name [Ident "Double"])

1032 MethodInv $ TypeMethodCall (J.Name [Ident "Double"])

1000 []

1033 []

@@ -1225,7 +1258,9 @@ mkExp (SCon conId name args) =

1225mkExp (SCase var alts) = mkCase False var alts

1258mkExp (SCase var alts) = mkCase False var alts

1226mkExp (SChkCase var alts) = mkCase True var alts

1259mkExp (SChkCase var alts) = mkCase True var alts

1227mkExp (SProj var i) = mkProjection var i

1260mkExp (SProj var i) = mkProjection var i

1261+mkExp (SConst (I x)) =

1262+ let x' :: Int32; x' = fromInteger (toInteger x) in

1228−mkExp (SConst (I x)) = return $ mkPrimitive "Integer" (Int (toInteger x))

1263+ return $ mkPrimitive "Integer" (Int (fromInteger (toInteger x')))

1229mkExp (SConst (BI x)) =

1264mkExp (SConst (BI x)) =

1230 return $ InstanceCreation []

1265 return $ InstanceCreation []

1231 (ClassType [(Ident "BigInteger", [])])

1266 (ClassType [(Ident "BigInteger", [])])

@@ -1251,24 +1286,22 @@ mkExp (SConst (PtrType)) = return $ mkClass objectType

1251mkExp (SConst (VoidType)) = return $ mkClass voidType

1286mkExp (SConst (VoidType)) = return $ mkClass voidType

1252mkExp (SConst (Forgot)) = return $ mkClass objectType

1287mkExp (SConst (Forgot)) = return $ mkClass objectType

1253mkExp (SForeign _ fType meth args) = mkForeignInvoke fType meth args

1288mkExp (SForeign _ fType meth args) = mkForeignInvoke fType meth args

1254−mkExp (SOp LPlus args) = mkBinOpExp integerType Add args

1289+mkExp (SOp (LPlus ITNative) args) = mkExp (SOp (LPlus IT32) args)

1255−mkExp (SOp LMinus args) = mkBinOpExp integerType Sub args

1290+mkExp (SOp (LMinus ITNative) args) = mkExp (SOp (LMinus IT32) args)

1256−mkExp (SOp LTimes args) = mkBinOpExp integerType Mult args

1291+mkExp (SOp (LTimes ITNative) args) = mkExp (SOp (LTimes IT32) args)

1257−mkExp (SOp LDiv args) = mkBinOpExp integerType Div args

1292+mkExp (SOp (LSDiv ITNative) args) = mkExp (SOp (LSDiv IT32) args)

1258−mkExp (SOp LMod args) = mkBinOpExp integerType Rem args

1293+mkExp (SOp (LSRem ITNative) args) = mkExp (SOp (LSRem IT32) args)

1259−mkExp (SOp LAnd args) = mkBinOpExp integerType And args

1294+mkExp (SOp (LAnd ITNative) args) = mkExp (SOp (LAnd IT32) args)

1260−mkExp (SOp LOr args) = mkBinOpExp integerType Or args

1295+mkExp (SOp (LOr ITNative) args) = mkExp (SOp (LOr IT32) args)

1261−mkExp (SOp LXOr args) = mkBinOpExp integerType Xor args

1296+mkExp (SOp (LXOr ITNative) args) = mkExp (SOp (LXOr IT32) args)

1262−mkExp (SOp LCompl [var]) =

1297+mkExp (SOp (LCompl ITNative) args) = mkExp (SOp (LCompl IT32) args)

1263− PreBitCompl <$> mkVarAccess (Just $ integerType) var

1264−mkExp (SOp LSHL args) = mkBinOpExp integerType LShift args

1298+mkExp (SOp (LSHL ITNative) args) = mkExp (SOp (LSHL IT32) args)

1265−mkExp (SOp LSHR args) = mkBinOpExp integerType RShift args

1299+mkExp (SOp (LASHR ITNative) args) = mkExp (SOp (LASHR IT32) args)

1266−mkExp (SOp LEq args) =

1300+mkExp (SOp (LEq ITNative) args) = mkExp (SOp (LEq IT32) args)

1267− mkMethodOpChain1 (mkBoolToNumber integerType) objectType "equals" args

1268−mkExp (SOp LLt args) = mkLogicalBinOpExp integerType LThan args

1301+mkExp (SOp (LLt ITNative) args) = mkExp (SOp (LLt IT32) args)

1269−mkExp (SOp LLe args) = mkLogicalBinOpExp integerType LThanE args

1302+mkExp (SOp (LLe ITNative) args) = mkExp (SOp (LLe IT32) args)

1270−mkExp (SOp LGt args) = mkLogicalBinOpExp integerType GThan args

1303+mkExp (SOp (LGt ITNative) args) = mkExp (SOp (LGt IT32) args)

1271−mkExp (SOp LGe args) = mkLogicalBinOpExp integerType GThanE args

1304+mkExp (SOp (LGe ITNative) args) = mkExp (SOp (LGe IT32) args)

1272mkExp (SOp LFPlus args) = mkBinOpExp doubleType Add args

1305mkExp (SOp LFPlus args) = mkBinOpExp doubleType Add args

1273mkExp (SOp LFMinus args) = mkBinOpExp doubleType Sub args

1306mkExp (SOp LFMinus args) = mkBinOpExp doubleType Sub args

1274mkExp (SOp LFTimes args) = mkBinOpExp doubleType Mult args

1307mkExp (SOp LFTimes args) = mkBinOpExp doubleType Mult args

@@ -1279,40 +1312,40 @@ mkExp (SOp LFLt args) = mkLogicalBinOpExp integerType LThan args

1279mkExp (SOp LFLe args) = mkLogicalBinOpExp integerType LThanE args

1312mkExp (SOp LFLe args) = mkLogicalBinOpExp integerType LThanE args

1280mkExp (SOp LFGt args) = mkLogicalBinOpExp integerType GThan args

1313mkExp (SOp LFGt args) = mkLogicalBinOpExp integerType GThan args

1281mkExp (SOp LFGe args) = mkLogicalBinOpExp integerType GThanE args

1314mkExp (SOp LFGe args) = mkLogicalBinOpExp integerType GThanE args

1282−mkExp (SOp LBPlus args) = mkMethodOpChain1 id bigIntegerType "add" args

1315+mkExp (SOp (LPlus ITBig) args) = mkMethodOpChain1 id bigIntegerType "add" args

1283−mkExp (SOp LBMinus args) = mkMethodOpChain1 id bigIntegerType "subtract" args

1316+mkExp (SOp (LMinus ITBig) args) = mkMethodOpChain1 id bigIntegerType "subtract" args

1284−mkExp (SOp LBTimes args) = mkMethodOpChain1 id bigIntegerType "multiply" args

1317+mkExp (SOp (LTimes ITBig) args) = mkMethodOpChain1 id bigIntegerType "multiply" args

1285−mkExp (SOp LBDiv args) = mkMethodOpChain1 id bigIntegerType "divide" args

1318+mkExp (SOp (LSDiv ITBig) args) = mkMethodOpChain1 id bigIntegerType "divide" args

1286−mkExp (SOp LBMod args) = mkMethodOpChain1 id bigIntegerType "mod" args

1319+mkExp (SOp (LSRem ITBig) args) = mkMethodOpChain1 id bigIntegerType "mod" args

1287−mkExp (SOp LBEq args) =

1320+mkExp (SOp (LEq ITBig) args) =

1288 mkMethodOpChain1 (mkBoolToNumber bigIntegerType) bigIntegerType "equals" args

1321 mkMethodOpChain1 (mkBoolToNumber bigIntegerType) bigIntegerType "equals" args

1289−mkExp (SOp LBLt args) =

1322+mkExp (SOp (LLt ITBig) args) =

1290 mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1323 mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1291 . mkPartialOrder SLt

1324 . mkPartialOrder SLt

1292 )

1325 )

1293 bigIntegerType

1326 bigIntegerType

1294− "compare"

1327+ "compareTo"

1295 args

1328 args

1296−mkExp (SOp LBLe args) =

1329+mkExp (SOp (LLe ITBig) args) =

1297 mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1330 mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1298 . mkPartialOrder SLe

1331 . mkPartialOrder SLe

1299 )

1332 )

1300 bigIntegerType

1333 bigIntegerType

1301− "compare"

1334+ "compareTo"

1302 args

1335 args

1303−mkExp (SOp LBGt args) =

1336+mkExp (SOp (LGt ITBig) args) =

1304 mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1337 mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1305 . mkPartialOrder SGt

1338 . mkPartialOrder SGt

1306 )

1339 )

1307 bigIntegerType

1340 bigIntegerType

1308− "compare"

1341+ "compareTo"

1309 args

1342 args

1310−mkExp (SOp LBGe args) =

1343+mkExp (SOp (LGe ITBig) args) =

1311 mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1344 mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1312 . mkPartialOrder SGe

1345 . mkPartialOrder SGe

1313 )

1346 )

1314 bigIntegerType

1347 bigIntegerType

1315− "compare"

1348+ "compareTo"

1316 args

1349 args

1317mkExp (SOp LStrConcat args) =

1350mkExp (SOp LStrConcat args) =

1318 mkMethodOpChain (\ exp -> InstanceCreation []

1351 mkMethodOpChain (\ exp -> InstanceCreation []

@@ -1329,158 +1362,56 @@ mkExp (SOp LStrLt args@[_, _]) =

1329 . mkPartialOrder SLt

1362 . mkPartialOrder SLt

1330 )

1363 )

1331 stringType

1364 stringType

1332− "compare"

1365+ "compareTo"

1333 args

1366 args

1334mkExp (SOp LStrEq args@[_, _]) =

1367mkExp (SOp LStrEq args@[_, _]) =

1335 mkMethodOpChain1 ( mkBoolToNumber integerType)

1368 mkMethodOpChain1 ( mkBoolToNumber integerType)

1336 stringType

1369 stringType

1337 "equals"

1370 "equals"

1338 args

1371 args

1339−mkExp (SOp LStrLen [arg]) =

1372+mkExp (SOp LStrLen [arg]) =

1340 (\ var -> MethodInv $ PrimaryMethodCall var [] (Ident "length") [])

1373 (\ var -> MethodInv $ PrimaryMethodCall var [] (Ident "length") [])

1341 <$> mkVarAccess (Just stringType) arg

1374 <$> mkVarAccess (Just stringType) arg

1342−mkExp (SOp LIntFloat [arg]) =

1375+mkExp (SOp (LIntFloat ity) [arg]) =

1343− mkPrimitiveCast integerType doubleType arg

1376+ mkPrimitiveCast (intTyToClass ity) doubleType arg

1344−mkExp (SOp LFloatInt [arg]) =

1377+mkExp (SOp (LFloatInt ity) [arg]) =

1345− mkPrimitiveCast doubleType integerType arg

1378+ mkPrimitiveCast doubleType (intTyToClass ity) arg

1379+mkExp (SOp (LIntStr ITBig) [arg]) =

1380+ (\ var -> InstanceCreation [] bigIntegerType [var] Nothing)

1381+ <$> mkVarAccess (Just stringType) arg

1346−mkExp (SOp LIntStr [arg]) =

1382+mkExp (SOp (LIntStr ity) [arg]) =

1347− mkToString integerType arg

1383+ mkToString (intTyToClass ity) arg

1348−mkExp (SOp LStrInt [arg]) =

1384+mkExp (SOp (LStrInt ity) [arg]) =

1349− mkPrimitiveCast stringType integerType arg

1385+ mkPrimitiveCast stringType (intTyToClass ity) arg

1350mkExp (SOp LFloatStr [arg]) =

1386mkExp (SOp LFloatStr [arg]) =

1351 mkToString doubleType arg

1387 mkToString doubleType arg

1352mkExp (SOp LStrFloat [arg]) =

1388mkExp (SOp LStrFloat [arg]) =

1353 mkPrimitiveCast doubleType stringType arg

1389 mkPrimitiveCast doubleType stringType arg

1354−mkExp (SOp LIntBig [arg]) =

1390+mkExp (SOp (LSExt ITNative ITBig) [arg]) =

1355 mkPrimitiveCast integerType bigIntegerType arg

1391 mkPrimitiveCast integerType bigIntegerType arg

1356−mkExp (SOp LBigInt [arg]) =

1392+mkExp (SOp (LTrunc ITBig ITNative) [arg]) =

1357 mkPrimitiveCast bigIntegerType integerType arg

1393 mkPrimitiveCast bigIntegerType integerType arg

1358−mkExp (SOp LStrBig [arg]) =

1359− (\ var -> InstanceCreation [] bigIntegerType [var] Nothing)

1360− <$> mkVarAccess (Just stringType) arg

1361−mkExp (SOp LBigStr [arg]) =

1362− mkToString bigIntegerType arg

1363−mkExp (SOp LChInt [arg]) =

1394+mkExp (SOp (LChInt ITNative) [arg]) =

1364 mkVarAccess (Just integerType) arg

1395 mkVarAccess (Just integerType) arg

1365−mkExp (SOp LIntCh [arg]) =

1396+mkExp (SOp (LIntCh ITNative) [arg]) =

1366 mkVarAccess (Just integerType) arg

1397 mkVarAccess (Just integerType) arg

1367mkExp (SOp LPrintNum [arg]) =

1398mkExp (SOp LPrintNum [arg]) =

1368 mkSystemOutPrint <$> (mkVarAccess Nothing arg)

1399 mkSystemOutPrint <$> (mkVarAccess Nothing arg)

1369mkExp (SOp LPrintStr [arg]) =

1400mkExp (SOp LPrintStr [arg]) =

1370 mkSystemOutPrint <$> (mkVarAccess (Just stringType) arg)

1401 mkSystemOutPrint <$> (mkVarAccess (Just stringType) arg)

1371mkExp (SOp LReadStr [arg]) = mkExp (SForeign LANG_C FString "idris_readStr" [(FPtr, arg)])

1402mkExp (SOp LReadStr [arg]) = mkExp (SForeign LANG_C FString "idris_readStr" [(FPtr, arg)])

1372−mkExp (SOp LB8Lt args) = mkLogicalBinOpExp byteType LThan args

1403+mkExp (SOp (LLt ty) args) = mkLogicalBinOpExp (intTyToClass ty) LThan args

1373−mkExp (SOp LB8Lte args) = mkLogicalBinOpExp byteType LThanE args

1404+mkExp (SOp (LLe ty) args) = mkLogicalBinOpExp (intTyToClass ty) LThanE args

1374−mkExp (SOp LB8Eq args) =

1405+mkExp (SOp (LEq ty) args) =

1375− mkMethodOpChain1 (mkBoolToNumber byteType) byteType "equals" args

1406+ mkMethodOpChain1 (mkBoolToNumber (intTyToClass ty)) (intTyToClass ty) "equals" args

1376−mkExp (SOp LB8Gt args) = mkLogicalBinOpExp byteType GThan args

1407+mkExp (SOp (LGt ty) args) = mkLogicalBinOpExp (intTyToClass ty) GThan args

1377−mkExp (SOp LB8Gte args) = mkLogicalBinOpExp byteType GThanE args

1408+mkExp (SOp (LGe ty) args) = mkLogicalBinOpExp (intTyToClass ty) GThanE args

1378−mkExp (SOp LB8Plus args) = mkBinOpExp byteType Add args

1409+mkExp (SOp (LPlus ty) args) = mkBinOpExp (intTyToClass ty) Add args

1379−mkExp (SOp LB8Minus args) = mkBinOpExp byteType Sub args

1410+mkExp (SOp (LMinus ty) args) = mkBinOpExp (intTyToClass ty) Sub args

1380−mkExp (SOp LB8Times args) = mkBinOpExp byteType Mult args

1411+mkExp (SOp (LTimes ty) args) = mkBinOpExp (intTyToClass ty) Mult args

1381−mkExp (SOp LB8UDiv args) = mkBinOpExpConv "shortValue" ShortT byteType Div args

1412+mkExp (SOp (LUDiv IT64) (arg:args)) = do

1382−mkExp (SOp LB8SDiv args) = mkBinOpExp byteType Div args

1383−mkExp (SOp LB8URem args) = mkBinOpExpConv "shortValue" ShortT byteType Rem args

1384−mkExp (SOp LB8SRem args) = mkBinOpExp byteType Rem args

1385−mkExp (SOp LB8Shl args) = mkBinOpExp byteType LShift args

1386−mkExp (SOp LB8LShr args) = mkBinOpExp byteType RRShift args

1387−mkExp (SOp LB8AShr args) = mkBinOpExp byteType RShift args

1388−mkExp (SOp LB8And args) = mkBinOpExp byteType And args

1389−mkExp (SOp LB8Or args) = mkBinOpExp byteType Or args

1390−mkExp (SOp LB8Xor args) = mkBinOpExp byteType Xor args

1391−mkExp (SOp LB8Compl [var]) =

1392− PreBitCompl <$> mkVarAccess (Just $ byteType) var

1393−mkExp (SOp LB8Z16 [var]) = mkZeroExt "shortValue" 8 byteType shortType var

1394−mkExp (SOp LB8Z32 [var]) = mkZeroExt "intValue" 8 byteType integerType var

1395−mkExp (SOp LB8Z64 [var]) = mkZeroExt "longValue" 8 byteType longType var

1396−mkExp (SOp LB8S16 [var]) = mkSignedExt "shortValue" byteType shortType var

1397−mkExp (SOp LB8S32 [var]) = mkSignedExt "intValue" byteType integerType var

1398−mkExp (SOp LB8S64 [var]) = mkSignedExt "longValue" byteType longType var

1399−mkExp (SOp LB16Lt args) = mkLogicalBinOpExp shortType LThan args

1400−mkExp (SOp LB16Lte args) = mkLogicalBinOpExp shortType LThanE args

1401−mkExp (SOp LB16Eq args) =

1402− mkMethodOpChain1 (mkBoolToNumber shortType) shortType "equals" args

1403−mkExp (SOp LB16Gt args) = mkLogicalBinOpExp shortType GThan args

1404−mkExp (SOp LB16Gte args) = mkLogicalBinOpExp shortType GThanE args

1405−mkExp (SOp LB16Plus args) = mkBinOpExp shortType Add args

1406−mkExp (SOp LB16Minus args) = mkBinOpExp shortType Sub args

1407−mkExp (SOp LB16Times args) = mkBinOpExp shortType Mult args

1408−mkExp (SOp LB16UDiv args) = mkBinOpExpConv "intValue" IntT shortType Div args

1409−mkExp (SOp LB16SDiv args) = mkBinOpExp shortType Div args

1410−mkExp (SOp LB16URem args) = mkBinOpExpConv "intValue" IntT shortType Rem args

1411−mkExp (SOp LB16SRem args) = mkBinOpExp shortType Rem args

1412−mkExp (SOp LB16Shl args) = mkBinOpExp shortType LShift args

1413−mkExp (SOp LB16LShr args) = mkBinOpExp shortType RRShift args

1414−mkExp (SOp LB16AShr args) = mkBinOpExp shortType RShift args

1415−mkExp (SOp LB16And args) = mkBinOpExp shortType And args

1416−mkExp (SOp LB16Or args) = mkBinOpExp shortType Or args

1417−mkExp (SOp LB16Xor args) = mkBinOpExp shortType Xor args

1418−mkExp (SOp LB16Compl [var]) =

1419− PreBitCompl <$> mkVarAccess (Just $ shortType) var

1420−mkExp (SOp LB16Z32 [var]) = mkZeroExt "intValue" 16 shortType integerType var

1421−mkExp (SOp LB16Z64 [var]) = mkZeroExt "longValue" 16 shortType longType var

1422−mkExp (SOp LB16S32 [var]) = mkSignedExt "intValue" shortType integerType var

1423−mkExp (SOp LB16S64 [var]) = mkSignedExt "longValue" shortType longType var

1424−mkExp (SOp LB16T8 [var]) =

1425− (\ var -> MethodInv $

1426− TypeMethodCall (J.Name [Ident "Byte"])

1427− []

1428− (Ident "valueOf")

1429− [ MethodInv

1430− $ PrimaryMethodCall var [] (Ident "byteValue") [] ]

1431− )

1432− <$> mkVarAccess (Just $ shortType) var

1433−mkExp (SOp LB32Lt args) = mkLogicalBinOpExp integerType LThan args

1434−mkExp (SOp LB32Lte args) = mkLogicalBinOpExp integerType LThanE args

1435−mkExp (SOp LB32Eq args) =

1436− mkMethodOpChain1 (mkBoolToNumber integerType) integerType "equals" args

1437−mkExp (SOp LB32Gt args) = mkLogicalBinOpExp integerType GThan args

1438−mkExp (SOp LB32Gte args) = mkLogicalBinOpExp integerType GThanE args

1439−mkExp (SOp LB32Plus args) = mkBinOpExp integerType Add args

1440−mkExp (SOp LB32Minus args) = mkBinOpExp integerType Sub args

1441−mkExp (SOp LB32Times args) = mkBinOpExp integerType Mult args

1442−mkExp (SOp LB32UDiv args) = mkBinOpExpConv "longValue" LongT integerType Div args

1443−mkExp (SOp LB32SDiv args) = mkBinOpExp integerType Div args

1444−mkExp (SOp LB32URem args) = mkBinOpExpConv "longValue" LongT integerType Rem args

1445−mkExp (SOp LB32SRem args) = mkBinOpExp integerType Rem args

1446−mkExp (SOp LB32Shl args) = mkBinOpExp integerType LShift args

1447−mkExp (SOp LB32LShr args) = mkBinOpExp integerType RRShift args

1448−mkExp (SOp LB32AShr args) = mkBinOpExp integerType RShift args

1449−mkExp (SOp LB32And args) = mkBinOpExp integerType And args

1450−mkExp (SOp LB32Or args) = mkBinOpExp integerType Or args

1451−mkExp (SOp LB32Xor args) = mkBinOpExp integerType Xor args

1452−mkExp (SOp LB32Compl [var]) =

1453− PreBitCompl <$> mkVarAccess (Just $ integerType) var

1454−mkExp (SOp LB32Z64 [var]) = mkZeroExt "longValue" 32 integerType longType var

1455−mkExp (SOp LB32S64 [var]) = mkSignedExt "longValue" integerType longType var

1456−mkExp (SOp LB32T8 [var]) =

1457− (\ var -> MethodInv

1458− $ TypeMethodCall (J.Name [Ident "Byte"])

1459− []

1460− (Ident "valueOf")

1461− [ MethodInv $ PrimaryMethodCall var [] (Ident "byteValue") [] ]

1462− )

1463− <$> mkVarAccess (Just $ integerType) var

1464−mkExp (SOp LB32T16 [var]) =

1465− (\ var -> MethodInv

1466− $ TypeMethodCall (J.Name [Ident "Short"])

1467− []

1468− (Ident "valueOf")

1469− [ MethodInv $ PrimaryMethodCall var [] (Ident "shortValue") [] ]

1470− )

1471− <$> mkVarAccess (Just $ integerType) var

1472−mkExp (SOp LB64Lt args) = mkLogicalBinOpExp longType LThan args

1473−mkExp (SOp LB64Lte args) = mkLogicalBinOpExp longType LThanE args

1474−mkExp (SOp LB64Eq args) =

1475− mkMethodOpChain1 (mkBoolToNumber longType) longType "equals" args

1476−mkExp (SOp LB64Gt args) = mkLogicalBinOpExp longType GThan args

1477−mkExp (SOp LB64Gte args) = mkLogicalBinOpExp longType GThanE args

1478−mkExp (SOp LB64Plus args) = mkBinOpExp longType Add args

1479−mkExp (SOp LB64Minus args) = mkBinOpExp longType Sub args

1480−mkExp (SOp LB64Times args) = mkBinOpExp longType Mult args

1481−mkExp (SOp LB64UDiv (arg:args)) = do

1482 (arg:args) <- mapM (mkVarAccess (Just longType)) (arg:args)

1413 (arg:args) <- mapM (mkVarAccess (Just longType)) (arg:args)

1483− return $ foldl' (\ exp arg ->

1414+ return $ foldl (\ exp arg ->

1484 MethodInv $ PrimaryMethodCall

1415 MethodInv $ PrimaryMethodCall

1485 ( MethodInv $ PrimaryMethodCall

1416 ( MethodInv $ PrimaryMethodCall

1486 ( MethodInv $ TypeMethodCall (J.Name [Ident "BigInteger"])

1417 ( MethodInv $ TypeMethodCall (J.Name [Ident "BigInteger"])

@@ -1502,10 +1433,16 @@ mkExp (SOp LB64UDiv (arg:args)) = do

1502 )

1433 )

1503 arg

1434 arg

1504 args

1435 args

1436+mkExp (SOp (LUDiv ty) args) =

1437+ mkBinOpExpConv (intTyToMethod $ nextIntTy ty)

1438+ (intTyToPrimTy $ nextIntTy ty)

1439+ (intTyToClass ty)

1440+ Div

1441+ args

1505−mkExp (SOp LB64SDiv args) = mkBinOpExp longType Div args

1442+mkExp (SOp (LSDiv ty) args) = mkBinOpExp (intTyToClass ty) Div args

1506−mkExp (SOp LB64URem (arg:args)) = do

1443+mkExp (SOp (LURem IT64) (arg:args)) = do

1507 (arg:args) <- mapM (mkVarAccess (Just longType)) (arg:args)

1444 (arg:args) <- mapM (mkVarAccess (Just longType)) (arg:args)

1508− return $ foldl' (\ exp arg ->

1445+ return $ foldl (\ exp arg ->

1509 MethodInv $ PrimaryMethodCall

1446 MethodInv $ PrimaryMethodCall

1510 ( MethodInv $ PrimaryMethodCall

1447 ( MethodInv $ PrimaryMethodCall

1511 ( MethodInv $ TypeMethodCall (J.Name [Ident "BigInteger"])

1448 ( MethodInv $ TypeMethodCall (J.Name [Ident "BigInteger"])

@@ -1527,46 +1464,36 @@ mkExp (SOp LB64URem (arg:args)) = do

1527 )

1464 )

1528 arg

1465 arg

1529 args

1466 args

1530−mkExp (SOp LB64SRem args) = mkBinOpExp longType Rem args

1467+mkExp (SOp (LURem ty) args) =

1468+ mkBinOpExpConv (intTyToMethod $ nextIntTy ty)

1469+ (intTyToPrimTy $ nextIntTy ty)

1470+ (intTyToClass ty)

1471+ Rem

1472+ args

1473+mkExp (SOp (LSRem ty) args) = mkBinOpExp (intTyToClass ty) Rem args

1531−mkExp (SOp LB64Shl args) = mkBinOpExp longType LShift args

1474+mkExp (SOp (LSHL ty) args) = mkBinOpExp (intTyToClass ty) LShift args

1532−mkExp (SOp LB64LShr args) = mkBinOpExp longType RRShift args

1475+mkExp (SOp (LLSHR ty) args) = mkBinOpExp (intTyToClass ty) RRShift args

1533−mkExp (SOp LB64AShr args) = mkBinOpExp longType RShift args

1476+mkExp (SOp (LASHR ty) args) = mkBinOpExp (intTyToClass ty) RShift args

1534−mkExp (SOp LB64And args) = mkBinOpExp longType And args

1477+mkExp (SOp (LAnd ty) args) = mkBinOpExp (intTyToClass ty) And args

1535−mkExp (SOp LB64Or args) = mkBinOpExp longType Or args

1478+mkExp (SOp (LOr ty) args) = mkBinOpExp (intTyToClass ty) Or args

1536−mkExp (SOp LB64Xor args) = mkBinOpExp longType Xor args

1479+mkExp (SOp (LXOr ty) args) = mkBinOpExp (intTyToClass ty) Xor args

1537−mkExp (SOp LB64Compl [var]) =

1538− PreBitCompl <$> mkVarAccess (Just $ longType) var

1480+mkExp (SOp (LCompl ty) [var]) = PreBitCompl <$> mkVarAccess (Just $ intTyToClass ty) var

1539−mkExp (SOp LB64T8 [var]) =

1481+mkExp (SOp (LZExt from to) [var])

1540− (\ var -> MethodInv

1482+ | intTyWidth from < intTyWidth to

1541− $ TypeMethodCall (J.Name [Ident "Byte"])

1483+ = mkZeroExt (intTyToMethod to) (intTyWidth from) (intTyToClass from) (intTyToClass to) var

1542− []

1543− (Ident "valueOf")

1544− [ MethodInv

1545− $ PrimaryMethodCall var [] (Ident "byteValue") []

1546− ]

1547− )

1548− <$> mkVarAccess (Just $ longType) var

1549−mkExp (SOp LB64T16 [var]) =

1484+mkExp (SOp (LSExt from to) [var])

1550− (\ var -> MethodInv

1485+ | intTyWidth from < intTyWidth to

1551− $ TypeMethodCall (J.Name [Ident "Short"])

1486+ = mkSignedExt (intTyToMethod to) (intTyToClass from) (intTyToClass to) var

1552− []

1487+mkExp (SOp (LTrunc from to) [var])

1553− (Ident "valueOf")

1488+ | intTyWidth from > intTyWidth to

1554− [ MethodInv $ PrimaryMethodCall var [] (Ident "shortValue") [] ]

1555− )

1556− <$> mkVarAccess (Just $ longType) var

1557−mkExp (SOp LB64T32 [var]) =

1558− (\ var -> MethodInv

1489+ = (\ var -> MethodInv $

1559− $ TypeMethodCall (J.Name [Ident "Integer"])

1490+ TypeMethodCall (J.Name [intTyToIdent to])

1560− []

1491+ []

1561− (Ident "valueOf")

1492+ (Ident "valueOf")

1493+ [ MethodInv

1562− [ MethodInv $ PrimaryMethodCall var [] (Ident "intValue") [] ]

1494+ $ PrimaryMethodCall var [] (Ident (intTyToMethod to)) [] ]

1563 )

1495 )

1564− <$> mkVarAccess (Just $ longType) var

1496+ <$> mkVarAccess (Just $ intTyToClass from) var

1565−mkExp (SOp LIntB8 [arg]) = mkExp (SOp LB32T8 [arg])

1566−mkExp (SOp LIntB16 [arg]) = mkExp (SOp LB32T16 [arg])

1567−mkExp (SOp LIntB32 [arg]) = mkExp (SV arg)

1568−mkExp (SOp LIntB64 [arg]) = mkExp (SOp LB32S64 [arg])

1569−mkExp (SOp LB32Int [arg]) = mkExp (SV arg)

1570mkExp (SOp LFExp [arg]) = mkMathFun "exp" arg

1497mkExp (SOp LFExp [arg]) = mkMathFun "exp" arg

1571mkExp (SOp LFLog [arg]) = mkMathFun "log" arg

1498mkExp (SOp LFLog [arg]) = mkMathFun "log" arg

1572mkExp (SOp LFSin [arg]) = mkMathFun "sin" arg

1499mkExp (SOp LFSin [arg]) = mkMathFun "sin" arg

src/IRTS/CodegenJavaScript.hs+36−36

@@ -203,58 +203,58 @@ translateExpression (SApp True name vars) =

203 ++ ";\n});"

204

205translateExpression (SOp op vars)

206− | LPlus <- op

206+ | (LPlus _) <- op

207 , (lhs:rhs:_) <- vars = translateBinaryOp "+" lhs rhs

208− | LMinus <- op

208+ | (LMinus _) <- op

209 , (lhs:rhs:_) <- vars = translateBinaryOp "-" lhs rhs

210− | LTimes <- op

210+ | (LTimes _) <- op

211 , (lhs:rhs:_) <- vars = translateBinaryOp "*" lhs rhs

212− | LDiv <- op

212+ | (LSDiv _) <- op

213 , (lhs:rhs:_) <- vars = translateBinaryOp "/" lhs rhs

214− | LMod <- op

214+ | (LSRem _) <- op

215 , (lhs:rhs:_) <- vars = translateBinaryOp "%" lhs rhs

216− | LEq <- op

216+ | (LEq _) <- op

217 , (lhs:rhs:_) <- vars = translateBinaryOp "==" lhs rhs

218− | LLt <- op

218+ | (LLt _) <- op

219 , (lhs:rhs:_) <- vars = translateBinaryOp "<" lhs rhs

220− | LLe <- op

220+ | (LLe _) <- op

221 , (lhs:rhs:_) <- vars = translateBinaryOp "<=" lhs rhs

222− | LGt <- op

222+ | (LGt _) <- op

223 , (lhs:rhs:_) <- vars = translateBinaryOp ">" lhs rhs

224− | LGe <- op

224+ | (LGe _) <- op

225 , (lhs:rhs:_) <- vars = translateBinaryOp ">=" lhs rhs

226− | LAnd <- op

226+ | (LAnd _) <- op

227 , (lhs:rhs:_) <- vars = translateBinaryOp "&" lhs rhs

228− | LOr <- op

228+ | (LOr _) <- op

229 , (lhs:rhs:_) <- vars = translateBinaryOp "|" lhs rhs

230− | LXOr <- op

230+ | (LXOr _) <- op

231 , (lhs:rhs:_) <- vars = translateBinaryOp "^" lhs rhs

232− | LSHL <- op

232+ | (LSHL _) <- op

233 , (lhs:rhs:_) <- vars = translateBinaryOp "<<" rhs lhs

234− | LSHR <- op

234+ | (LASHR _) <- op

235 , (lhs:rhs:_) <- vars = translateBinaryOp ">>" rhs lhs

236− | LCompl <- op

236+ | (LCompl _) <- op

237 , (arg:_) <- vars = '~' : translateVariableName arg

238

239− | LBPlus <- op

239+ | (LPlus ITBig) <- op

240 , (lhs:rhs:_) <- vars = translateBinaryOp ".add(" lhs rhs ++ ")"

241− | LBMinus <- op

241+ | (LMinus ITBig) <- op

242 , (lhs:rhs:_) <- vars = translateBinaryOp ".minus(" lhs rhs ++ ")"

243− | LBTimes <- op

243+ | (LTimes ITBig) <- op

244 , (lhs:rhs:_) <- vars = translateBinaryOp ".times(" lhs rhs ++ ")"

245− | LBDiv <- op

245+ | (LSDiv ITBig) <- op

246 , (lhs:rhs:_) <- vars = translateBinaryOp ".divide(" lhs rhs ++ ")"

247− | LBMod <- op

247+ | (LSRem ITBig) <- op

248 , (lhs:rhs:_) <- vars = translateBinaryOp ".mod(" lhs rhs ++ ")"

249− | LBEq <- op

249+ | (LEq ITBig) <- op

250 , (lhs:rhs:_) <- vars = translateBinaryOp ".equals(" lhs rhs ++ ")"

251− | LBLt <- op

251+ | (LLt ITBig) <- op

252 , (lhs:rhs:_) <- vars = translateBinaryOp ".lesser(" lhs rhs ++ ")"

253− | LBLe <- op

253+ | (LLe ITBig) <- op

254 , (lhs:rhs:_) <- vars = translateBinaryOp ".lesserOrEquals(" lhs rhs ++ ")"

255− | LBGt <- op

255+ | (LGt ITBig) <- op

256 , (lhs:rhs:_) <- vars = translateBinaryOp ".greater(" lhs rhs ++ ")"

257− | LBGe <- op

257+ | (LGe ITBig) <- op

258 , (lhs:rhs:_) <- vars = translateBinaryOp ".greaterOrEquals(" lhs rhs ++ ")"

259

260 | LFPlus <- op

@@ -285,29 +285,29 @@ translateExpression (SOp op vars)

285 | LStrLen <- op

286 , (arg:_) <- vars = translateVariableName arg ++ ".length"

287

288− | LStrInt <- op

288+ | (LStrInt ITNative) <- op

289 , (arg:_) <- vars = "parseInt(" ++ translateVariableName arg ++ ")"

290− | LIntStr <- op

290+ | (LIntStr ITNative) <- op

291 , (arg:_) <- vars = "String(" ++ translateVariableName arg ++ ")"

292− | LIntBig <- op

292+ | (LSExt ITNative ITBig) <- op

293 , (arg:_) <- vars = "__IDRRT__.bigInt(" ++ translateVariableName arg ++ ")"

294− | LBigInt <- op

294+ | (LTrunc ITBig ITNative) <- op

295 , (arg:_) <- vars = translateVariableName arg ++ ".valueOf()"

296− | LBigStr <- op

296+ | (LIntStr ITBig) <- op

297 , (arg:_) <- vars = translateVariableName arg ++ ".toString()"

298− | LStrBig <- op

298+ | (LStrInt ITBig) <- op

299 , (arg:_) <- vars = "__IDRRT__.bigInt(" ++ translateVariableName arg ++ ")"

300 | LFloatStr <- op

301 , (arg:_) <- vars = "String(" ++ translateVariableName arg ++ ")"

302 | LStrFloat <- op

303 , (arg:_) <- vars = "parseFloat(" ++ translateVariableName arg ++ ")"

304− | LIntFloat <- op

304+ | (LIntFloat ITNative) <- op

305 , (arg:_) <- vars = translateVariableName arg

306− | LFloatInt <- op

306+ | (LFloatInt ITNative) <- op

307 , (arg:_) <- vars = translateVariableName arg

308− | LChInt <- op

308+ | (LChInt ITNative) <- op

309 , (arg:_) <- vars = translateVariableName arg ++ ".charCodeAt(0)"

310− | LIntCh <- op

310+ | (LIntCh ITNative) <- op

311 , (arg:_) <- vars =

312 "String.fromCharCode(" ++ translateVariableName arg ++ ")"

313

src/IRTS/Compiler.hs+7−1

@@ -284,15 +284,21 @@ getFTypes tm = case unApply tm of

284 _ -> Nothing

285

286mkIty' (P _ (UN ty) _) = mkIty ty

287+mkIty' (App (P _ (UN "FIntT") _) (P _ (UN intTy) _)) = mkIntIty intTy

287mkIty' _ = FAny

288mkIty' _ = FAny

288

289

289−mkIty "FInt" = FInt

290mkIty "FFloat" = FDouble

291mkIty "FChar" = FChar

292mkIty "FString" = FString

293mkIty "FPtr" = FPtr

294mkIty "FUnit" = FUnit

295

296+mkIntIty "ITNative" = FInt ITNative

297+mkIntIty "IT8" = FInt IT8

298+mkIntIty "IT16" = FInt IT16

299+mkIntIty "IT32" = FInt IT32

300+mkIntIty "IT64" = FInt IT64

301+

296zname = NS (UN "O") ["Nat","Prelude"]

302zname = NS (UN "O") ["Nat","Prelude"]

297sname = NS (UN "S") ["Nat","Prelude"]

303sname = NS (UN "S") ["Nat","Prelude"]

298

304

src/IRTS/LParser.hs+27−27

@@ -92,39 +92,39 @@ pLDecl = do reserved "data"

93pLExp = buildExpressionParser optable pLExp'

95−optable = [[binary "*" (\x y -> LOp LTimes [x,y]) AssocLeft,

95+optable = [[binary "*" (\x y -> LOp (LTimes ITNative) [x,y]) AssocLeft,

96− binary "/" (\x y -> LOp LDiv [x,y]) AssocLeft,

96+ binary "/" (\x y -> LOp (LSDiv ITNative) [x,y]) AssocLeft,

97 binary "*." (\x y -> LOp LFTimes [x,y]) AssocLeft,

98 binary "/." (\x y -> LOp LFDiv [x,y]) AssocLeft,

99− binary "*:" (\x y -> LOp LBTimes [x,y]) AssocLeft,

99+ binary "*:" (\x y -> LOp (LTimes ITBig) [x,y]) AssocLeft,

100− binary "/:" (\x y -> LOp LBDiv [x,y]) AssocLeft

100+ binary "/:" (\x y -> LOp (LSDiv ITBig) [x,y]) AssocLeft

101 ],

102 [

103− binary "+" (\x y -> LOp LPlus [x,y]) AssocLeft,

103+ binary "+" (\x y -> LOp (LPlus ITNative) [x,y]) AssocLeft,

104− binary "-" (\x y -> LOp LMinus [x,y]) AssocLeft,

104+ binary "-" (\x y -> LOp (LMinus ITNative) [x,y]) AssocLeft,

105 binary "++" (\x y -> LOp LStrConcat [x,y]) AssocLeft,

106 binary "+." (\x y -> LOp LFPlus [x,y]) AssocLeft,

107 binary "-." (\x y -> LOp LFMinus [x,y]) AssocLeft,

108− binary "+:" (\x y -> LOp LBPlus [x,y]) AssocLeft,

108+ binary "+:" (\x y -> LOp (LPlus ITBig) [x,y]) AssocLeft,

109− binary "-:" (\x y -> LOp LBMinus [x,y]) AssocLeft

109+ binary "-:" (\x y -> LOp (LMinus ITBig) [x,y]) AssocLeft

110 ],

111 [

112− binary "==" (\x y -> LOp LEq [x, y]) AssocNone,

112+ binary "==" (\x y -> LOp (LEq ITNative) [x, y]) AssocNone,

113 binary "==." (\x y -> LOp LFEq [x, y]) AssocNone,

114− binary "<" (\x y -> LOp LLt [x, y]) AssocNone,

114+ binary "<" (\x y -> LOp (LLt ITNative) [x, y]) AssocNone,

115 binary "<." (\x y -> LOp LFLt [x, y]) AssocNone,

116− binary ">" (\x y -> LOp LGt [x, y]) AssocNone,

116+ binary ">" (\x y -> LOp (LGt ITNative) [x, y]) AssocNone,

117 binary ">." (\x y -> LOp LFGt [x, y]) AssocNone,

118− binary "<=" (\x y -> LOp LLe [x, y]) AssocNone,

118+ binary "<=" (\x y -> LOp (LLe ITNative) [x, y]) AssocNone,

119 binary "<=." (\x y -> LOp LFLe [x, y]) AssocNone,

120− binary ">=" (\x y -> LOp LGe [x, y]) AssocNone,

120+ binary ">=" (\x y -> LOp (LGe ITNative) [x, y]) AssocNone,

121 binary ">=." (\x y -> LOp LFGe [x, y]) AssocNone,

122

123− binary "==:" (\x y -> LOp LBEq [x, y]) AssocNone,

123+ binary "==:" (\x y -> LOp (LEq ITBig) [x, y]) AssocNone,

124− binary "<:" (\x y -> LOp LBLt [x, y]) AssocNone,

124+ binary "<:" (\x y -> LOp (LLt ITBig) [x, y]) AssocNone,

125− binary ">:" (\x y -> LOp LBGt [x, y]) AssocNone,

125+ binary ">:" (\x y -> LOp (LGt ITBig) [x, y]) AssocNone,

126− binary "<=:" (\x y -> LOp LBLe [x, y]) AssocNone,

126+ binary "<=:" (\x y -> LOp (LLe ITBig) [x, y]) AssocNone,

127− binary ">=:" (\x y -> LOp LBGe [x, y]) AssocNone

127+ binary ">=:" (\x y -> LOp (LGe ITBig) [x, y]) AssocNone

128 ]]

129

130binary name f assoc = Infix (do reservedOp name; return f) assoc

@@ -164,7 +164,7 @@ pLExp' = try (do lchar '%'; pCast)

164

165pLang = do reserved "C"; return LANG_C

166

167−pType = do reserved "Int"; return FInt

167+pType = do reserved "Int"; return (FInt ITNative)

168 <|> do reserved "Float"; return FDouble

169 <|> do reserved "String"; return FString

170 <|> do reserved "Unit"; return FUnit

@@ -184,21 +184,21 @@ pCast = do reserved "FloatString"; lchar '('; e <- pLExp; lchar ')'

184 <|> do reserved "StringFloat"; lchar '('; e <- pLExp; lchar ')'

185 return (LOp LStrFloat [e])

186 <|> do reserved "FloatInt"; lchar '('; e <- pLExp; lchar ')'

187− return (LOp LFloatInt [e])

187+ return (LOp (LFloatInt ITNative) [e])

188 <|> do reserved "IntFloat"; lchar '('; e <- pLExp; lchar ')'

189− return (LOp LIntFloat [e])

189+ return (LOp (LIntFloat ITNative) [e])

190 <|> do reserved "StringInt"; lchar '('; e <- pLExp; lchar ')'

191− return (LOp LStrInt [e])

191+ return (LOp (LStrInt ITNative) [e])

192 <|> do reserved "IntString"; lchar '('; e <- pLExp; lchar ')'

193− return (LOp LIntStr [e])

193+ return (LOp (LIntStr ITNative) [e])

194 <|> do reserved "BigInt"; lchar '('; e <- pLExp; lchar ')'

195− return (LOp LBigInt [e])

195+ return (LOp (LTrunc ITBig ITNative) [e])

196 <|> do reserved "IntBig"; lchar '('; e <- pLExp; lchar ')'

197− return (LOp LIntBig [e])

197+ return (LOp (LSExt ITNative ITBig) [e])

198 <|> do reserved "BigString"; lchar '('; e <- pLExp; lchar ')'

199− return (LOp LBigStr [e])

199+ return (LOp (LIntStr ITBig) [e])

200 <|> do reserved "StringBig"; lchar '('; e <- pLExp; lchar ')'

201− return (LOp LStrBig [e])

201+ return (LOp (LStrInt ITBig) [e])

202

203pPrim :: LParser LExp

204pPrim = do reserved "StrEq"; lchar '(';

src/IRTS/Lang.hs+29−26

@@ -3,6 +3,7 @@ module IRTS.Lang where

3import Core.TT

4import Control.Monad.State hiding(lift)

5import Data.List

6+import Foreign.Storable (sizeOf)

6import Debug.Trace

7import Debug.Trace

8data LVar = Loc Int | Glob Name

9data LVar = Loc Int | Glob Name

@@ -28,36 +29,38 @@ data LExp = LV LVar

28-- Primitive operators. Backends are not *required* to implement all

29-- Primitive operators. Backends are not *required* to implement all

29-- of these, but should report an error if they are unable

30-- of these, but should report an error if they are unable

32+data IntTy = ITNative | IT8 | IT16 | IT32 | IT64 | ITBig

33+ deriving (Show, Eq)

34+

35+intTyWidth :: IntTy -> Int

36+intTyWidth IT8 = 8

37+intTyWidth IT16 = 16

38+intTyWidth IT32 = 32

39+intTyWidth IT64 = 64

40+intTyWidth ITNative = 8 * sizeOf (0 :: Int)

41+intTyWidth ITBig = error "IRTS.Lang.intTyWidth: Big integers have variable width"

42+

43+intTyToConst :: IntTy -> Const

44+intTyToConst IT8 = B8Type

45+intTyToConst IT16 = B16Type

46+intTyToConst IT32 = B32Type

47+intTyToConst IT64 = B64Type

48+intTyToConst ITBig = BIType

49+intTyToConst ITNative = IType

50+

31−data PrimFn = LPlus | LMinus | LTimes | LDiv | LMod

51+data PrimFn = LPlus IntTy | LMinus IntTy | LTimes IntTy

52+ | LUDiv IntTy | LSDiv IntTy | LURem IntTy | LSRem IntTy

53+ | LAnd IntTy | LOr IntTy | LXOr IntTy | LCompl IntTy

54+ | LSHL IntTy | LLSHR IntTy | LASHR IntTy

33− | LEq | LLt | LLe | LGt | LGe

56+ | LSExt IntTy IntTy | LZExt IntTy IntTy | LTrunc IntTy IntTy

34 | LFPlus | LFMinus | LFTimes | LFDiv

57 | LFPlus | LFMinus | LFTimes | LFDiv

38 | LStrConcat | LStrLt | LStrEq | LStrLen

59 | LStrConcat | LStrLt | LStrEq | LStrLen

60+ | LIntFloat IntTy | LFloatInt IntTy | LIntStr IntTy | LStrInt IntTy

61+ | LFloatStr | LStrFloat | LChInt IntTy | LIntCh IntTy

41 | LPrintNum | LPrintStr | LReadStr

62 | LPrintNum | LPrintStr | LReadStr

46− | LB8Z16 | LB8Z32 | LB8Z64 | LB8S16 | LB8S32 | LB8S64 -- Zero/Sign extension

50− | LB16Z32 | LB16Z64 | LB16S32 | LB16S64 | LB16T8 -- and Truncation

54− | LB32Z64 | LB32S64 | LB32T8 | LB32T16

58− | LB64T8 | LB64T16 | LB64T32

60−

62 | LFSqrt | LFFloor | LFCeil

65 | LFSqrt | LFFloor | LFCeil

@@ -76,7 +79,7 @@ data PrimFn = LPlus | LMinus | LTimes | LDiv | LMod

76data FLang = LANG_C

79data FLang = LANG_C

77 deriving (Show, Eq)

80 deriving (Show, Eq)

80 deriving (Show, Eq)

83 deriving (Show, Eq)

82data LAlt = LConCase Int Name [Name] LExp

85data LAlt = LConCase Int Name [Name] LExp

src/Idris/Primitives.hs+224−445

@@ -1,4 +1,4 @@

1−{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}

1+{-# LANGUAGE RankNTypes, ScopedTypeVariables, PatternGuards #-}

3module Idris.Primitives(elabPrims) where

@@ -34,280 +34,73 @@ partial = Partial NotCovering

35primitives =

36 -- operators

37− [Prim (UN "prim__addInt") (ty [IType, IType] IType) 2 (iBin (+))

38− (2, LPlus) total,

39− Prim (UN "prim__subInt") (ty [IType, IType] IType) 2 (iBin (-))

40− (2, LMinus) total,

41− Prim (UN "prim__mulInt") (ty [IType, IType] IType) 2 (iBin (*))

42− (2, LTimes) total,

43− Prim (UN "prim__divInt") (ty [IType, IType] IType) 2 (iBin div)

44− (2, LDiv) partial,

45− Prim (UN "prim__modInt") (ty [IType, IType] IType) 2 (iBin mod)

46− (2, LMod) partial,

47− Prim (UN "prim__andInt") (ty [IType, IType] IType) 2 (iBin (.&.))

48− (2, LAnd) partial,

49− Prim (UN "prim__orInt") (ty [IType, IType] IType) 2 (iBin (.|.))

50− (2, LOr) partial,

51− Prim (UN "prim__xorInt") (ty [IType, IType] IType) 2 (iBin xor)

52− (2, LXOr) partial,

53− Prim (UN "prim__shLInt") (ty [IType, IType] IType) 2 (iBin shiftL)

54− (2, LSHL) partial,

55− Prim (UN "prim__shRInt") (ty [IType, IType] IType) 2 (iBin shiftR)

56− (2, LSHR) partial,

57− Prim (UN "prim__complInt") (ty [IType] IType) 1 (iUn complement)

58− (1, LCompl) partial,

59− Prim (UN "prim__eqInt") (ty [IType, IType] IType) 2 (biBin (==))

60− (2, LEq) total,

61− Prim (UN "prim__ltInt") (ty [IType, IType] IType) 2 (biBin (<))

62− (2, LLt) total,

63− Prim (UN "prim__lteInt") (ty [IType, IType] IType) 2 (biBin (<=))

64− (2, LLe) total,

65− Prim (UN "prim__gtInt") (ty [IType, IType] IType) 2 (biBin (>))

66− (2, LGt) total,

67− Prim (UN "prim__gteInt") (ty [IType, IType] IType) 2 (biBin (>=))

68− (2, LGe) total,

69− Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==))

37+ [Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==))

70− (2, LEq) total,

38+ (2, LEq ITNative) total,

71 Prim (UN "prim__ltChar") (ty [ChType, ChType] IType) 2 (bcBin (<))

39 Prim (UN "prim__ltChar") (ty [ChType, ChType] IType) 2 (bcBin (<))

72− (2, LLt) total,

40+ (2, LLt ITNative) total,

73 Prim (UN "prim__lteChar") (ty [ChType, ChType] IType) 2 (bcBin (<=))

41 Prim (UN "prim__lteChar") (ty [ChType, ChType] IType) 2 (bcBin (<=))

74− (2, LLe) total,

42+ (2, LLe ITNative) total,

75 Prim (UN "prim__gtChar") (ty [ChType, ChType] IType) 2 (bcBin (>))

43 Prim (UN "prim__gtChar") (ty [ChType, ChType] IType) 2 (bcBin (>))

76− (2, LGt) total,

44+ (2, LGt ITNative) total,

77 Prim (UN "prim__gteChar") (ty [ChType, ChType] IType) 2 (bcBin (>=))

45 Prim (UN "prim__gteChar") (ty [ChType, ChType] IType) 2 (bcBin (>=))

78− (2, LGe) total,

46+ (2, LGe ITNative) total,

79−

47+

80− Prim (UN "prim__ltB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (<))

48+ iCoerce IT8 IT16 "zext" zext LZExt,

81− (2, LB8Lt) total,

49+ iCoerce IT8 IT32 "zext" zext LZExt,

82− Prim (UN "prim__lteB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (<=))

50+ iCoerce IT8 IT64 "zext" zext LZExt,

83− (2, LB8Lte) total,

51+ iCoerce IT8 ITBig "zext" zext LZExt,

84− Prim (UN "prim__eqB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (==))

52+ iCoerce IT8 ITNative "zext" zext LZExt,

85− (2, LB8Eq) total,

53+ iCoerce IT16 IT32 "zext" zext LZExt,

86− Prim (UN "prim__gteB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (>))

54+ iCoerce IT16 IT64 "zext" zext LZExt,

87− (2, LB8Gte) total,

55+ iCoerce IT16 ITBig "zext" zext LZExt,

88− Prim (UN "prim__gtB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (>=))

56+ iCoerce IT16 ITNative "zext" zext LZExt,

89− (2, LB8Gt) total,

57+ iCoerce IT32 IT64 "zext" zext LZExt,

90− Prim (UN "prim__addB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (+))

58+ iCoerce IT32 ITBig "zext" zext LZExt,

91− (2, LB8Plus) total,

59+ iCoerce IT32 ITNative "zext" zext LZExt,

92− Prim (UN "prim__subB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (-))

60+ iCoerce IT64 ITBig "zext" zext LZExt,

93− (2, LB8Minus) total,

61+ iCoerce ITNative ITBig "zext" zext LZExt,

94− Prim (UN "prim__mulB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (*))

62+ iCoerce ITNative IT64 "zext" zext LZExt,

95− (2, LB8Times) total,

63+ iCoerce ITNative IT32 "zext" zext LZExt,

96− Prim (UN "prim__udivB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin div)

64+ iCoerce ITNative IT16 "zext" zext LZExt,

97− (2, LB8UDiv) partial,

65+

98− Prim (UN "prim__sdivB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin s8div)

66+ iCoerce IT8 IT16 "sext" sext LSExt,

99− (2, LB8SDiv) partial,

67+ iCoerce IT8 IT32 "sext" sext LSExt,

100− Prim (UN "prim__uremB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin rem)

68+ iCoerce IT8 IT64 "sext" sext LSExt,

101− (2, LB8URem) partial,

69+ iCoerce IT8 ITBig "sext" sext LSExt,

102− Prim (UN "prim__sremB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin s8rem)

70+ iCoerce IT8 ITNative "sext" sext LSExt,

103− (2, LB8SRem) partial,

71+ iCoerce IT16 IT32 "sext" sext LSExt,

104− Prim (UN "prim__shlB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (\x y -> shiftL x (fromIntegral y)))

72+ iCoerce IT16 IT64 "sext" sext LSExt,

105− (2, LB8Shl) total,

73+ iCoerce IT16 ITBig "sext" sext LSExt,

106− Prim (UN "prim__lshrB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (\x y -> shiftR x (fromIntegral y)))

74+ iCoerce IT16 ITNative "sext" sext LSExt,

107− (2, LB8AShr) total,

75+ iCoerce IT32 IT64 "sext" sext LSExt,

108− Prim (UN "prim__ashrB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (\x y -> fromIntegral $

76+ iCoerce IT32 ITBig "sext" sext LSExt,

109− shiftR (fromIntegral x :: Int8)

77+ iCoerce IT32 ITNative "sext" sext LSExt,

110− (fromIntegral y)))

78+ iCoerce IT64 ITBig "sext" sext LSExt,

111− (2, LB8LShr) total,

79+ iCoerce ITNative ITBig "sext" sext LSExt,

112− Prim (UN "prim__andB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (.&.))

80+ iCoerce ITNative ITBig "sext" sext LSExt,

113− (2, LB8And) total,

81+ iCoerce ITNative IT64 "sext" sext LSExt,

114− Prim (UN "prim__orB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (.|.))

82+ iCoerce ITNative IT32 "sext" sext LSExt,

115− (2, LB8Or) total,

83+ iCoerce ITNative IT16 "sext" sext LSExt,

116− Prim (UN "prim__xorB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin xor)

84+

117− (2, LB8Xor) total,

85+ iCoerce IT16 IT8 "trunc" trunc LTrunc,

118− Prim (UN "prim__complB8") (ty [B8Type] B8Type) 1 (b8Un complement)

86+ iCoerce IT32 IT8 "trunc" trunc LTrunc,

119− (1, LB8Compl) total,

87+ iCoerce IT64 IT8 "trunc" trunc LTrunc,

120− Prim (UN "prim__zextB8_16") (ty [B8Type] B16Type) 1 zext8_16

88+ iCoerce ITBig IT8 "trunc" trunc LTrunc,

121− (1, LB8Z16) total,

89+ iCoerce ITNative IT8 "trunc" trunc LTrunc,

122− Prim (UN "prim__zextB8_32") (ty [B8Type] B32Type) 1 zext8_32

90+ iCoerce IT32 IT16 "trunc" trunc LTrunc,

123− (1, LB8Z32) total,

91+ iCoerce IT64 IT16 "trunc" trunc LTrunc,

124− Prim (UN "prim__zextB8_64") (ty [B8Type] B64Type) 1 zext8_64

92+ iCoerce ITBig IT16 "trunc" trunc LTrunc,

125− (1, LB8Z64) total,

93+ iCoerce ITNative IT16 "trunc" trunc LTrunc,

126− Prim (UN "prim__sextB8_16") (ty [B8Type] B16Type) 1 sext8_16

94+ iCoerce IT64 IT32 "trunc" trunc LTrunc,

127− (1, LB8Z16) total,

95+ iCoerce ITBig IT32 "trunc" trunc LTrunc,

128− Prim (UN "prim__sextB8_32") (ty [B8Type] B32Type) 1 sext8_32

96+ iCoerce ITNative IT32 "trunc" trunc LTrunc,

129− (1, LB8Z32) total,

97+ iCoerce ITBig IT64 "trunc" trunc LTrunc,

130− Prim (UN "prim__sextB8_64") (ty [B8Type] B64Type) 1 sext8_64

98+ iCoerce IT16 ITNative "trunc" trunc LTrunc,

131− (1, LB8Z64) total,

99+ iCoerce IT32 ITNative "trunc" trunc LTrunc,

132−

100+ iCoerce IT64 ITNative "trunc" trunc LTrunc,

133− Prim (UN "prim__ltB16") (ty [B16Type, B16Type] IType) 2 (b16Cmp (<))

101+ iCoerce ITBig ITNative "trunc" trunc LTrunc,

134− (2, LB16Lt) total,

102+ iCoerce ITNative IT64 "trunc" trunc LTrunc,

135− Prim (UN "prim__lteB16") (ty [B16Type, B16Type] IType) 2 (b16Cmp (<=))

103+

136− (2, LB16Lte) total,

137− Prim (UN "prim__eqB16") (ty [B16Type, B16Type] IType) 2 (b16Cmp (==))

138− (2, LB16Eq) total,

139− Prim (UN "prim__gteB16") (ty [B16Type, B16Type] IType) 2 (b16Cmp (>))

140− (2, LB16Gte) total,

141− Prim (UN "prim__gtB16") (ty [B16Type, B16Type] IType) 2 (b16Cmp (>=))

142− (2, LB16Gt) total,

143− Prim (UN "prim__addB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (+))

144− (2, LB16Plus) total,

145− Prim (UN "prim__subB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (-))

146− (2, LB16Minus) total,

147− Prim (UN "prim__mulB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (*))

148− (2, LB16Times) total,

149− Prim (UN "prim__udivB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin div)

150− (2, LB16UDiv) partial,

151− Prim (UN "prim__sdivB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin s16div)

152− (2, LB16SDiv) partial,

153− Prim (UN "prim__uremB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin rem)

154− (2, LB16URem) partial,

155− Prim (UN "prim__sremB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin s16rem)

156− (2, LB16SRem) partial,

157− Prim (UN "prim__shlB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (\x y -> shiftL x (fromIntegral y)))

158− (2, LB16Shl) total,

159− Prim (UN "prim__lshrB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (\x y -> shiftR x (fromIntegral y)))

160− (2, LB16AShr) total,

161− Prim (UN "prim__ashrB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (\x y -> fromIntegral $

162− shiftR (fromIntegral x :: Int16)

163− (fromIntegral y)))

164− (2, LB16LShr) total,

165− Prim (UN "prim__andB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (.&.))

166− (2, LB16And) total,

167− Prim (UN "prim__orB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin (.|.))

168− (2, LB16Or) total,

169− Prim (UN "prim__xorB16") (ty [B16Type, B16Type] B16Type) 2 (b16Bin xor)

170− (2, LB16Xor) total,

171− Prim (UN "prim__complB16") (ty [B16Type] B16Type) 1 (b16Un complement)

172− (1, LB16Compl) total,

173− Prim (UN "prim__zextB16_32") (ty [B16Type] B32Type) 1 zext16_32

174− (1, LB16Z32) total,

175− Prim (UN "prim__zextB16_64") (ty [B16Type] B64Type) 1 zext16_64

176− (1, LB16Z64) total,

177− Prim (UN "prim__sextB16_32") (ty [B16Type] B32Type) 1 sext16_32

178− (1, LB16Z32) total,

179− Prim (UN "prim__sextB16_64") (ty [B16Type] B64Type) 1 sext16_64

180− (1, LB16Z64) total,

181− Prim (UN "prim__truncB16_8") (ty [B16Type] B8Type) 1 trunc16_8

182− (1, LB16T8) total,

183−

184− Prim (UN "prim__ltB32") (ty [B32Type, B32Type] IType) 2 (b32Cmp (<))

185− (2, LB32Lt) total,

186− Prim (UN "prim__lteB32") (ty [B32Type, B32Type] IType) 2 (b32Cmp (<=))

187− (2, LB32Lte) total,

188− Prim (UN "prim__eqB32") (ty [B32Type, B32Type] IType) 2 (b32Cmp (==))

189− (2, LB32Eq) total,

190− Prim (UN "prim__gteB32") (ty [B32Type, B32Type] IType) 2 (b32Cmp (>))

191− (2, LB32Gte) total,

192− Prim (UN "prim__gtB32") (ty [B32Type, B32Type] IType) 2 (b32Cmp (>=))

193− (2, LB32Gt) total,

194− Prim (UN "prim__addB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (+))

195− (2, LB32Plus) total,

196− Prim (UN "prim__subB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (-))

197− (2, LB32Minus) total,

198− Prim (UN "prim__mulB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (*))

199− (2, LB32Times) total,

200− Prim (UN "prim__udivB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin div)

201− (2, LB32UDiv) partial,

202− Prim (UN "prim__sdivB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin s32div)

203− (2, LB32SDiv) partial,

204− Prim (UN "prim__uremB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin rem)

205− (2, LB32URem) partial,

206− Prim (UN "prim__sremB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin s32rem)

207− (2, LB32SRem) partial,

208− Prim (UN "prim__shlB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (\x y -> shiftL x (fromIntegral y)))

209− (2, LB32Shl) total,

210− Prim (UN "prim__lshrB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (\x y -> shiftR x (fromIntegral y)))

211− (2, LB32AShr) total,

212− Prim (UN "prim__ashrB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (\x y -> fromIntegral $

213− shiftR (fromIntegral x :: Int32)

214− (fromIntegral y)))

215− (2, LB32LShr) total,

216− Prim (UN "prim__andB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (.&.))

217− (2, LB32And) total,

218− Prim (UN "prim__orB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin (.|.))

219− (2, LB32Or) total,

220− Prim (UN "prim__xorB32") (ty [B32Type, B32Type] B32Type) 2 (b32Bin xor)

221− (2, LB32Xor) total,

222− Prim (UN "prim__complB32") (ty [B32Type] B32Type) 1 (b32Un complement)

223− (1, LB32Compl) total,

224− Prim (UN "prim__zextB32_64") (ty [B32Type] B64Type) 1 zext32_64

225− (1, LB32Z64) total,

226− Prim (UN "prim__sextB32_64") (ty [B32Type] B64Type) 1 sext32_64

227− (1, LB32Z64) total,

228− Prim (UN "prim__truncB32_8") (ty [B32Type] B8Type) 1 trunc32_8

229− (1, LB32T8) total,

230− Prim (UN "prim__truncB32_16") (ty [B32Type] B16Type) 1 trunc32_16

231− (1, LB32T16) total,

232−

233− Prim (UN "prim__ltB64") (ty [B64Type, B64Type] IType) 2 (b64Cmp (<))

234− (2, LB64Lt) total,

235− Prim (UN "prim__lteB64") (ty [B64Type, B64Type] IType) 2 (b64Cmp (<=))

236− (2, LB64Lte) total,

237− Prim (UN "prim__eqB64") (ty [B64Type, B64Type] IType) 2 (b64Cmp (==))

238− (2, LB64Eq) total,

239− Prim (UN "prim__gteB64") (ty [B64Type, B64Type] IType) 2 (b64Cmp (>))

240− (2, LB64Gte) total,

241− Prim (UN "prim__gtB64") (ty [B64Type, B64Type] IType) 2 (b64Cmp (>=))

242− (2, LB64Gt) total,

243− Prim (UN "prim__addB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (+))

244− (2, LB64Plus) total,

245− Prim (UN "prim__subB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (-))

246− (2, LB64Minus) total,

247− Prim (UN "prim__mulB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (*))

248− (2, LB64Times) total,

249− Prim (UN "prim__udivB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin div)

250− (2, LB64UDiv) partial,

251− Prim (UN "prim__sdivB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin s64div)

252− (2, LB64SDiv) partial,

253− Prim (UN "prim__uremB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin rem)

254− (2, LB64URem) partial,

255− Prim (UN "prim__sremB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin s64rem)

256− (2, LB64SRem) partial,

257− Prim (UN "prim__shlB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (\x y -> shiftL x (fromIntegral y)))

258− (2, LB64Shl) total,

259− Prim (UN "prim__lshrB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (\x y -> shiftR x (fromIntegral y)))

260− (2, LB64AShr) total,

261− Prim (UN "prim__ashrB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (\x y -> fromIntegral $

262− shiftR (fromIntegral x :: Int64)

263− (fromIntegral y)))

264− (2, LB64LShr) total,

265− Prim (UN "prim__andB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (.&.))

266− (2, LB64And) total,

267− Prim (UN "prim__orB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin (.|.))

268− (2, LB64Or) total,

269− Prim (UN "prim__xorB64") (ty [B64Type, B64Type] B64Type) 2 (b64Bin xor)

270− (2, LB64Xor) total,

271− Prim (UN "prim__complB64") (ty [B64Type] B64Type) 1 (b64Un complement)

272− (1, LB64Compl) total,

273− Prim (UN "prim__truncB64_8") (ty [B64Type] B8Type) 1 trunc64_8

274− (1, LB64T8) total,

275− Prim (UN "prim__truncB64_16") (ty [B64Type] B16Type) 1 trunc64_16

276− (1, LB64T16) total,

277− Prim (UN "prim__truncB64_32") (ty [B64Type] B32Type) 1 trunc64_32

278− (1, LB64T32) total,

279−

280− Prim (UN "prim__intToB8") (ty [IType] B8Type) 1 intToBits8

281− (1, LIntB8) total,

282− Prim (UN "prim__intToB16") (ty [IType] B16Type) 1 intToBits16

283− (1, LIntB16) total,

284− Prim (UN "prim__intToB32") (ty [IType] B32Type) 1 intToBits32

285− (1, LIntB32) total,

286− Prim (UN "prim__intToB64") (ty [IType] B64Type) 1 intToBits64

287− (1, LIntB64) total,

288− Prim (UN "prim__B32ToInt") (ty [B32Type] IType) 1 bits32ToInt

289− (1, LB32Int) total,

290−

291− Prim (UN "prim__addBigInt") (ty [BIType, BIType] BIType) 2 (bBin (+))

292− (2, LBPlus) total,

293− Prim (UN "prim__subBigInt") (ty [BIType, BIType] BIType) 2 (bBin (-))

294− (2, LBMinus) total,

295− Prim (UN "prim__mulBigInt") (ty [BIType, BIType] BIType) 2 (bBin (*))

296− (2, LBTimes) total,

297− Prim (UN "prim__divBigInt") (ty [BIType, BIType] BIType) 2 (bBin div)

298− (2, LBDiv) partial,

299− Prim (UN "prim__modBigInt") (ty [BIType, BIType] BIType) 2 (bBin mod)

300− (2, LBMod) partial,

301− Prim (UN "prim__eqBigInt") (ty [BIType, BIType] IType) 2 (bbBin (==))

302− (2, LBEq) total,

303− Prim (UN "prim__ltBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<))

304− (2, LBLt) total,

305− Prim (UN "prim__lteBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<=))

306− (2, LBLe) total,

307− Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>))

308− (2, LBGt) total,

309− Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>=))

310− (2, LBGe) total,

311 Prim (UN "prim__addFloat") (ty [FlType, FlType] FlType) 2 (fBin (+))

104 Prim (UN "prim__addFloat") (ty [FlType, FlType] FlType) 2 (fBin (+))

312 (2, LFPlus) total,

105 (2, LFPlus) total,

313 Prim (UN "prim__subFloat") (ty [FlType, FlType] FlType) 2 (fBin (-))

106 Prim (UN "prim__subFloat") (ty [FlType, FlType] FlType) 2 (fBin (-))

@@ -335,30 +128,14 @@ primitives =

335 Prim (UN "prim_lenString") (ty [StrType] IType) 1 (p_strLen)

128 Prim (UN "prim_lenString") (ty [StrType] IType) 1 (p_strLen)

336 (1, LStrLen) total,

129 (1, LStrLen) total,

337 -- Conversions

130 -- Conversions

338− Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt)

339− (1, LStrInt) total,

340− Prim (UN "prim__intToStr") (ty [IType] StrType) 1 (c_intToStr)

341− (1, LIntStr) total,

342 Prim (UN "prim__charToInt") (ty [ChType] IType) 1 (c_charToInt)

131 Prim (UN "prim__charToInt") (ty [ChType] IType) 1 (c_charToInt)

343− (1, LChInt) total,

132+ (1, LChInt ITNative) total,

344 Prim (UN "prim__intToChar") (ty [IType] ChType) 1 (c_intToChar)

133 Prim (UN "prim__intToChar") (ty [IType] ChType) 1 (c_intToChar)

345− (1, LIntCh) total,

134+ (1, LIntCh ITNative) total,

346− Prim (UN "prim__intToBigInt") (ty [IType] BIType) 1 (c_intToBigInt)

347− (1, LIntBig) total,

348− Prim (UN "prim__bigIntToInt") (ty [BIType] IType) 1 (c_bigIntToInt)

349− (1, LBigInt) total,

350− Prim (UN "prim__strToBigInt") (ty [StrType] BIType) 1 (c_strToBigInt)

351− (1, LStrBig) total,

352− Prim (UN "prim__bigIntToStr") (ty [BIType] StrType) 1 (c_bigIntToStr)

353− (1, LBigStr) total,

354 Prim (UN "prim__strToFloat") (ty [StrType] FlType) 1 (c_strToFloat)

135 Prim (UN "prim__strToFloat") (ty [StrType] FlType) 1 (c_strToFloat)

355 (1, LStrFloat) total,

136 (1, LStrFloat) total,

356 Prim (UN "prim__floatToStr") (ty [FlType] StrType) 1 (c_floatToStr)

137 Prim (UN "prim__floatToStr") (ty [FlType] StrType) 1 (c_floatToStr)

357 (1, LFloatStr) total,

138 (1, LFloatStr) total,

358− Prim (UN "prim__intToFloat") (ty [IType] FlType) 1 (c_intToFloat)

359− (1, LIntFloat) total,

360− Prim (UN "prim__floatToInt") (ty [FlType] IType) 1 (c_floatToInt)

361− (1, LFloatInt) total,

362

139

363 Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)

140 Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)

364 (1, LFExp) total,

141 (1, LFExp) total,

@@ -402,7 +179,49 @@ primitives =

402 (0, LStdIn) partial,

179 (0, LStdIn) partial,

403 Prim (UN "prim__believe_me") believeTy 3 (p_believeMe)

180 Prim (UN "prim__believe_me") believeTy 3 (p_believeMe)

404 (3, LNoOp) partial -- ahem

181 (3, LNoOp) partial -- ahem

405− ]

182+ ] ++ concatMap intOps [IT8, IT16, IT32, IT64, ITBig, ITNative]

183+

184+intOps ity =

185+ [ iCmp ity "lt" (bCmp ity (<)) LLt total

186+ , iCmp ity "lte" (bCmp ity (<=)) LLe total

187+ , iCmp ity "eq" (bCmp ity (==)) LEq total

188+ , iCmp ity "gte" (bCmp ity (>=)) LGe total

189+ , iCmp ity "gt" (bCmp ity (>)) LGt total

190+ , iBinOp ity "add" (bitBin ity (+)) LPlus total

191+ , iBinOp ity "sub" (bitBin ity (-)) LMinus total

192+ , iBinOp ity "mul" (bitBin ity (*)) LTimes total

193+ , iBinOp ity "udiv" (bitBin ity div) LUDiv partial

194+ , iBinOp ity "sdiv" (bsdiv ity) LSDiv partial

195+ , iBinOp ity "urem" (bitBin ity rem) LURem partial

196+ , iBinOp ity "srem" (bsrem ity) LSRem partial

197+ , iBinOp ity "shl" (bitBin ity (\x y -> shiftL x (fromIntegral y))) LSHL total

198+ , iBinOp ity "lshr" (bitBin ity (\x y -> shiftR x (fromIntegral y))) LLSHR total

199+ , iBinOp ity "ashr" (bashr ity) LASHR total

200+ , iBinOp ity "and" (bitBin ity (.&.)) LAnd total

201+ , iBinOp ity "or" (bitBin ity (.|.)) LOr total

202+ , iBinOp ity "xor" (bitBin ity (xor)) LXOr total

203+ , iUnOp ity "compl" (bUn ity complement) LCompl total

204+ , Prim (UN $ "prim__toStr" ++ intTyName ity) (ty [intTyToConst ity] StrType) 1 intToStr

205+ (1, LIntStr ity) total

206+ , Prim (UN $ "prim__fromStr" ++ intTyName ity) (ty [StrType] (intTyToConst ity)) 1 (strToInt ity)

207+ (1, LStrInt ity) total

208+ , Prim (UN $ "prim__toFloat" ++ intTyName ity) (ty [intTyToConst ity] FlType) 1 intToFloat

209+ (1, LIntFloat ity) total

210+ , Prim (UN $ "prim__fromFloat" ++ intTyName ity) (ty [FlType] (intTyToConst ity)) 1 (floatToInt ity)

211+ (1, LFloatInt ity) total

212+ ]

213+

214+intTyName :: IntTy -> String

215+intTyName ITNative = "Int"

216+intTyName ITBig = "BigInt"

217+intTyName sized = "B" ++ show (intTyWidth sized)

218+

219+iCmp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty (replicate 2 $ intTyToConst ity) IType) 2 impl (2, irop ity) totality

220+iBinOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty (replicate 2 $ intTyToConst ity) (intTyToConst ity)) 2 impl (2, irop ity) totality

221+iUnOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty [intTyToConst ity] (intTyToConst ity)) 1 impl (1, irop ity) totality

222+iCoerce from to op impl irop =

223+ Prim (UN $ "prim__" ++ op ++ intTyName from ++ "_" ++ intTyName to)

224+ (ty [intTyToConst from] (intTyToConst to)) 1 (impl from to) (1, irop from to) total

406

225

407p_believeMe [_,_,x] = Just x

226p_believeMe [_,_,x] = Just x

408p_believeMe _ = Nothing

227p_believeMe _ = Nothing

@@ -441,161 +260,127 @@ bsBin _ _ = Nothing

441sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))

260sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))

442sBin _ _ = Nothing

261sBin _ _ = Nothing

443

262

444−s8div :: Word8 -> Word8 -> Word8

263+bsrem IT8 [VConstant (B8 x), VConstant (B8 y)]

445−s8div x y = fromIntegral (fromIntegral x `div` fromIntegral y :: Int8)

264+ = Just $ VConstant (B8 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int8)))

446−

265+bsrem IT16 [VConstant (B16 x), VConstant (B16 y)]

447−s16div :: Word16 -> Word16 -> Word16

448−s16div x y = fromIntegral (fromIntegral x `div` fromIntegral y :: Int16)

266+ = Just $ VConstant (B16 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int16)))

449−

267+bsrem IT32 [VConstant (B32 x), VConstant (B32 y)]

450−s32div :: Word32 -> Word32 -> Word32

268+ = Just $ VConstant (B32 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int32)))

269+bsrem IT64 [VConstant (B64 x), VConstant (B64 y)]

451−s32div x y = fromIntegral (fromIntegral x `div` fromIntegral y :: Int32)

270+ = Just $ VConstant (B64 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int64)))

452−

271+bsrem ITNative [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (x `rem` y))

453−s64div :: Word64 -> Word64 -> Word64

272+bsrem _ _ = Nothing

273+

274+bsdiv IT8 [VConstant (B8 x), VConstant (B8 y)]

454−s64div x y = fromIntegral (fromIntegral x `div` fromIntegral y :: Int64)

275+ = Just $ VConstant (B8 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int8)))

455−

276+bsdiv IT16 [VConstant (B16 x), VConstant (B16 y)]

456−s8rem :: Word8 -> Word8 -> Word8

277+ = Just $ VConstant (B16 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int16)))

457−s8rem x y = fromIntegral (fromIntegral x `rem` fromIntegral y :: Int8)

278+bsdiv IT32 [VConstant (B32 x), VConstant (B32 y)]

458−

279+ = Just $ VConstant (B32 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int32)))

459−s16rem :: Word16 -> Word16 -> Word16

280+bsdiv IT64 [VConstant (B64 x), VConstant (B64 y)]

460−s16rem x y = fromIntegral (fromIntegral x `rem` fromIntegral y :: Int16)

281+ = Just $ VConstant (B64 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int64)))

461−

282+bsdiv ITNative [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (x `div` y))

462−s32rem :: Word32 -> Word32 -> Word32

283+bsdiv _ _ = Nothing

463−s32rem x y = fromIntegral (fromIntegral x `rem` fromIntegral y :: Int32)

284+

464−

285+bashr IT8 [VConstant (B8 x), VConstant (B8 y)]

465−s64rem :: Word64 -> Word64 -> Word64

286+ = Just $ VConstant (B8 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int8)))

466−s64rem x y = fromIntegral (fromIntegral x `rem` fromIntegral y :: Int64)

287+bashr IT16 [VConstant (B16 x), VConstant (B16 y)]

467−

288+ = Just $ VConstant (B16 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int16)))

289+bashr IT32 [VConstant (B32 x), VConstant (B32 y)]

290+ = Just $ VConstant (B32 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int32)))

291+bashr IT64 [VConstant (B64 x), VConstant (B64 y)]

292+ = Just $ VConstant (B64 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int64)))

293+bashr ITNative [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (x `shiftR` y))

294+bashr _ _ = Nothing

295+

296+bUn :: IntTy -> (forall a. Bits a => a -> a) -> [Value] -> Maybe Value

297+bUn IT8 op [VConstant (B8 x)] = Just $ VConstant (B8 (op x))

298+bUn IT16 op [VConstant (B16 x)] = Just $ VConstant (B16 (op x))

299+bUn IT32 op [VConstant (B32 x)] = Just $ VConstant (B32 (op x))

300+bUn IT64 op [VConstant (B64 x)] = Just $ VConstant (B64 (op x))

301+bUn ITBig op [VConstant (BI x)] = Just $ VConstant (BI (op x))

302+bUn ITNative op [VConstant (I x)] = Just $ VConstant (I (op x))

303+bUn _ _ _ = Nothing

304+

305+bitBin :: IntTy -> (forall a. (Bits a, Integral a) => a -> a -> a) -> [Value] -> Maybe Value

306+bitBin IT8 op [VConstant (B8 x), VConstant (B8 y)] = Just $ VConstant (B8 (op x y))

468−b8Bin op [VConstant (B8 x), VConstant (B8 y)] = Just $ VConstant (B8 (op x y))

307+bitBin IT16 op [VConstant (B16 x), VConstant (B16 y)] = Just $ VConstant (B16 (op x y))

469−b8Bin _ _ = Nothing

470−

471−b8Un op [VConstant (B8 x)] = Just $ VConstant (B8 (op x))

308+bitBin IT32 op [VConstant (B32 x), VConstant (B32 y)] = Just $ VConstant (B32 (op x y))

472−b8Un _ _ = Nothing

473−

474−b16Bin op [VConstant (B16 x), VConstant (B16 y)] = Just $ VConstant (B16 (op x y))

309+bitBin IT64 op [VConstant (B64 x), VConstant (B64 y)] = Just $ VConstant (B64 (op x y))

475−b16Bin _ _ = Nothing

476−

477−b16Un op [VConstant (B16 x)] = Just $ VConstant (B16 (op x))

310+bitBin ITBig op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (BI (op x y))

478−b16Un _ _ = Nothing

479−

480−b32Bin op [VConstant (B32 x), VConstant (B32 y)] = Just $ VConstant (B32 (op x y))

311+bitBin ITNative op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))

481−b32Bin _ _ = Nothing

312+bitBin _ _ _ = Nothing

482−

313+

483−b32Un op [VConstant (B32 x)] = Just $ VConstant (B32 (op x))

314+bCmp :: IntTy -> (forall a. Ord a => a -> a -> Bool) -> [Value] -> Maybe Value

484−b32Un _ _ = Nothing

485−

486−b64Bin op [VConstant (B64 x), VConstant (B64 y)] = Just $ VConstant (B64 (op x y))

315+bCmp IT8 op [VConstant (B8 x), VConstant (B8 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))

487−b64Bin _ _ = Nothing

488−

489−b64Un op [VConstant (B64 x)] = Just $ VConstant (B64 (op x))

316+bCmp IT16 op [VConstant (B16 x), VConstant (B16 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))

490−b64Un _ _ = Nothing

491−

492−b8Cmp op [VConstant (B8 x), VConstant (B8 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))

317+bCmp IT32 op [VConstant (B32 x), VConstant (B32 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))

493−b8Cmp _ _ = Nothing

494−

495−b16Cmp op [VConstant (B16 x), VConstant (B16 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))

318+bCmp IT64 op [VConstant (B64 x), VConstant (B64 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))

496−b16Cmp _ _ = Nothing

497−

498−b32Cmp op [VConstant (B32 x), VConstant (B32 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))

319+bCmp ITBig op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (I (if (op x y) then 1 else 0))

499−b32Cmp _ _ = Nothing

500−

501−b64Cmp op [VConstant (B64 x), VConstant (B64 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))

320+bCmp ITNative op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (if (op x y) then 1 else 0))

502−b64Cmp _ _ = Nothing

321+bCmp _ _ _ = Nothing

503−

322+

504−toB8 x = VConstant (B8 (fromIntegral x))

323+toInt IT8 x = VConstant (B8 (fromIntegral x))

505−toB16 x = VConstant (B16 (fromIntegral x))

324+toInt IT16 x = VConstant (B16 (fromIntegral x))

506−toB32 x = VConstant (B32 (fromIntegral x))

325+toInt IT32 x = VConstant (B32 (fromIntegral x))

507−toB64 x = VConstant (B64 (fromIntegral x))

326+toInt IT64 x = VConstant (B64 (fromIntegral x))

508−

327+toInt ITBig x = VConstant (BI (fromIntegral x))

509−zext8_16 [VConstant (B8 x)] = Just $ toB16 x

328+toInt ITNative x = VConstant (I (fromIntegral x))

510−zext8_16 _ = Nothing

329+

511−

512−zext8_32 [VConstant (B8 x)] = Just $ toB32 x

513−zext8_32 _ = Nothing

514−

515−zext8_64 [VConstant (B8 x)] = Just $ toB64 x

516−zext8_64 _ = Nothing

517−

518−sext8_16 [VConstant (B8 x)] = Just $ toB16 (fromIntegral x :: Int8)

330+intToInt IT8 out [VConstant (B8 x)] = Just $ toInt out x

519−sext8_16 _ = Nothing

331+intToInt IT16 out [VConstant (B16 x)] = Just $ toInt out x

520−

332+intToInt IT32 out [VConstant (B32 x)] = Just $ toInt out x

521−sext8_32 [VConstant (B8 x)] = Just $ toB32 (fromIntegral x :: Int8)

522−sext8_32 _ = Nothing

523−

524−sext8_64 [VConstant (B8 x)] = Just $ toB64 (fromIntegral x :: Int8)

525−sext8_64 _ = Nothing

526−

527−zext16_32 [VConstant (B16 x)] = Just $ toB32 x

333+intToInt IT64 out [VConstant (B64 x)] = Just $ toInt out x

528−zext16_32 _ = Nothing

529−

530−zext16_64 [VConstant (B16 x)] = Just $ toB64 x

334+intToInt ITBig out [VConstant (BI x)] = Just $ toInt out x

531−zext16_64 _ = Nothing

335+intToInt ITNative out [VConstant (I x)] = Just $ toInt out x

532−

533−sext16_32 [VConstant (B16 x)] = Just $ toB32 (fromIntegral x :: Int16)

534−sext16_32 _ = Nothing

336+intToInt _ _ _ = Nothing

535−

337+

536−sext16_64 [VConstant (B16 x)] = Just $ toB64 (fromIntegral x :: Int16)

338+zext from ITBig val = intToInt from ITBig val

537−sext16_64 _ = Nothing

339+zext ITBig _ _ = Nothing

538−

340+zext from to val

539−trunc16_8 [VConstant (B16 x)] = Just $ toB8 x

341+ | intTyWidth from < intTyWidth to = intToInt from to val

540−trunc16_8 _ = Nothing

342+zext _ _ _ = Nothing

541−

343+

542−zext32_64 [VConstant (B32 x)] = Just $ toB64 x

344+sext IT8 out [VConstant (B8 x)] = Just $ toInt out (fromIntegral x :: Int8)

543−zext32_64 _ = Nothing

544−

545−sext32_64 [VConstant (B32 x)] = Just $ toB64 (fromIntegral x :: Int32)

345+sext IT16 out [VConstant (B16 x)] = Just $ toInt out (fromIntegral x :: Int16)

546−sext32_64 _ = Nothing

547−

548−trunc32_8 [VConstant (B32 x)] = Just $ toB8 x

346+sext IT32 out [VConstant (B32 x)] = Just $ toInt out (fromIntegral x :: Int32)

549−trunc32_8 _ = Nothing

347+sext IT64 out [VConstant (B64 x)] = Just $ toInt out (fromIntegral x :: Int64)

550−

551−trunc32_16 [VConstant (B32 x)] = Just $ toB16 x

552−trunc32_16 _ = Nothing

348+sext ITBig _ _ = Nothing

553−

349+sext from to val = intToInt from to val

554−trunc64_8 [VConstant (B64 x)] = Just $ toB8 x

350+

351+trunc ITBig to val = intToInt ITBig to val

555−trunc64_8 _ = Nothing

352+trunc _ ITBig _ = Nothing

556−

353+trunc from to val | intTyWidth from > intTyWidth to = intToInt from to val

557−trunc64_16 [VConstant (B64 x)] = Just $ toB16 x

558−trunc64_16 _ = Nothing

354+trunc _ _ _ = Nothing

559−

355+

356+getInt :: [Value] -> Maybe Integer

560−trunc64_32 [VConstant (B64 x)] = Just $ toB32 x

357+getInt [VConstant (B8 x)] = Just . toInteger $ x

561−trunc64_32 _ = Nothing

562−

563−intToBits8 [VConstant (I x)] = Just $ toB8 x

358+getInt [VConstant (B16 x)] = Just . toInteger $ x

564−intToBits8 _ = Nothing

565−intToBits16 [VConstant (I x)] = Just $ toB16 x

359+getInt [VConstant (B32 x)] = Just . toInteger $ x

566−intToBits16 _ = Nothing

567−intToBits32 [VConstant (I x)] = Just $ toB32 x

360+getInt [VConstant (B64 x)] = Just . toInteger $ x

568−intToBits32 _ = Nothing

569−intToBits64 [VConstant (I x)] = Just $ toB64 x

361+getInt [VConstant (I x)] = Just . toInteger $ x

570−intToBits64 _ = Nothing

571−

572−bits32ToInt [VConstant (B32 x)] = Just $ VConstant (I (fromIntegral x))

362+getInt [VConstant (BI x)] = Just x

573−bits32ToInt _ = Nothing

363+getInt _ = Nothing

574−

364+

575−c_intToStr [VConstant (I x)] = Just $ VConstant (Str (show x))

365+intToStr val | Just i <- getInt val = Just $ VConstant (Str (show i))

576−c_intToStr _ = Nothing

366+intToStr _ = Nothing

367+

577−c_strToInt [VConstant (Str x)] = case reads x of

368+strToInt ity [VConstant (Str x)] = case reads x of

578− [(n,"")] -> Just $ VConstant (I n)

369+ [(n,"")] -> Just $ toInt ity (n :: Integer)

579− _ -> Just $ VConstant (I 0)

370+ _ -> Just $ VConstant (I 0)

371+strToInt _ _ = Nothing

372+

373+intToFloat val | Just i <- getInt val = Just $ VConstant (Fl (fromIntegral i))

374+intToFloat _ = Nothing

375+

376+floatToInt ity [VConstant (Fl x)] = Just $ toInt ity (truncate x :: Integer)

580−c_strToInt _ = Nothing

377+floatToInt _ _ = Nothing

581

378

582c_intToChar [VConstant (I x)] = Just $ VConstant (Ch (toEnum x))

379c_intToChar [VConstant (I x)] = Just $ VConstant (Ch (toEnum x))

583c_intToChar _ = Nothing

380c_intToChar _ = Nothing

584c_charToInt [VConstant (Ch x)] = Just $ VConstant (I (fromEnum x))

381c_charToInt [VConstant (Ch x)] = Just $ VConstant (I (fromEnum x))

585c_charToInt _ = Nothing

382c_charToInt _ = Nothing

586

383

587−c_intToBigInt [VConstant (I x)] = Just $ VConstant (BI (fromIntegral x))

588−c_intToBigInt _ = Nothing

589−c_bigIntToInt [VConstant (BI x)] = Just $ VConstant (I (fromInteger x))

590−c_bigIntToInt _ = Nothing

591−

592−c_bigIntToStr [VConstant (BI x)] = Just $ VConstant (Str (show x))

593−c_bigIntToStr _ = Nothing

594−c_strToBigInt [VConstant (Str x)] = case reads x of

595− [(n,"")] -> Just $ VConstant (BI n)

596− _ -> Just $ VConstant (BI 0)

597−c_strToBigInt _ = Nothing

598−

599c_floatToStr [VConstant (Fl x)] = Just $ VConstant (Str (show x))

384c_floatToStr [VConstant (Fl x)] = Just $ VConstant (Str (show x))

600c_floatToStr _ = Nothing

385c_floatToStr _ = Nothing

601c_strToFloat [VConstant (Str x)] = case reads x of

386c_strToFloat [VConstant (Str x)] = case reads x of

@@ -603,12 +388,6 @@ c_strToFloat [VConstant (Str x)] = case reads x of

603 _ -> Just $ VConstant (Fl 0)

388 _ -> Just $ VConstant (Fl 0)

604c_strToFloat _ = Nothing

389c_strToFloat _ = Nothing

605

390

606−c_floatToInt [VConstant (Fl x)] = Just $ VConstant (I (truncate x))

607−c_floatToInt _ = Nothing

608−

609−c_intToFloat [VConstant (I x)] = Just $ VConstant (Fl (fromIntegral x))

610−c_intToFloat _ = Nothing

611−

612p_fPrim f [VConstant (Fl x)] = Just $ VConstant (Fl (f x))

391p_fPrim f [VConstant (Fl x)] = Just $ VConstant (Fl (f x))

613p_fPrim f _ = Nothing

392p_fPrim f _ = Nothing

614

393

test/test021/expected+2−2

@@ -2,5 +2,5 @@

2, WORLD!!!

3, ]

5−23

5+15

6−Answer: 107

6+Answer: 99

test/test021/test021a.idr+5−5

@@ -6,18 +6,18 @@ import Effect.Random

6import Effect.StdIO

8data Expr = Var String

9− | Val Int

9+ | Val Integer

10 | Add Expr Expr

11− | Random Int

11+ | Random Integer

13Env : Type

14−Env = List (String, Int)

14+Env = List (String, Integer)

16-- Evaluator : Type -> Type

17-- Evaluator t

18-- = Eff m [EXCEPTION String, RND, STATE Env] t

20−eval : Expr -> Eff IO [EXCEPTION String, STDIO, RND, STATE Env] Int

20+eval : Expr -> Eff IO [EXCEPTION String, STDIO, RND, STATE Env] Integer

21eval (Var x) = do vs <- get

22 case lookup x vs of

23 Nothing => raise ("No such variable " ++ x)

@@ -31,7 +31,7 @@ eval (Random upper) = do val <- rndInt 0 upper

31testExpr : Expr

32testExpr = Add (Add (Var "foo") (Val 42)) (Random 100)

34−runEval : List (String, Int) -> Expr -> IO Int

34+runEval : List (String, Integer) -> Expr -> IO Integer

35runEval args expr = run [(), (), 123456, args] (eval expr)

37main : IO ()

test/test025/test025.idr+4−4

@@ -9,23 +9,23 @@ MemoryIO td ts r = Eff (IOExcept String) [ Dst ::: RAW_MEMORY td

9 , Src ::: RAW_MEMORY ts ] r

11inpVect : Vect Bits8 5

12−inpVect = map prim__intToB8 [0, 1, 2, 3, 5]

12+inpVect = map prim__truncInt_B8 [0, 1, 2, 3, 5]

14sub1 : Vect Bits8 n -> Vect Bits8 n

15−sub1 xs = map (prim__intToB8 . (\ x => x - 1) . prim__B32ToInt . prim__sextB8_32) xs

15+sub1 xs = map (prim__truncInt_B8 . (\ x => x - 1) . prim__zextB8_Int) xs

17testMemory : MemoryIO () () (Vect Int 4)

18testMemory = do Src :- allocate 5

19 Src :- poke 0 inpVect oh

20 Dst :- allocate 5

21− Dst :- initialize (prim__intToB8 1) 2 oh

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

25 Dst :- poke 4 (sub1 end) oh

26 res <- Dst :- peek 1 4 oh

27 Dst :- free

28− return (map (prim__B32ToInt . prim__sextB8_32) res)

28+ return (map (prim__zextB8_Int) res)

30main : IO ()

31main = do ioe_run (run [Dst := (), Src := ()] testMemory)