fc8d6e1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Expand integer primitive unification to encompass bigints

Conflicts: rts/idris_rts.h src/IRTS/CodegenJava.hs

commitfc8d6e19d95a6ac7a4902f84004a29f77dd396bb authorBenjamin Saunders <besaunde@sfu.ca> dateThu 9 May 2013, 16:08 (13 years ago) parent5e0a907

14 files changed+268−315

compare with master

unifiedsplit

effects/Effect/Memory.idr+2−2 lib/Builtins.idr+4−4 lib/Data/Bits.idr+40−40 lib/Network/Cgi.idr+1−1 lib/Prelude.idr+2−2 lib/Prelude/Cast.idr+7−7 rts/idris_rts.c+2−3 rts/idris_rts.h+1−1 src/IRTS/CodegenC.hs+24−28 src/IRTS/CodegenJava.hs+27−33 src/IRTS/CodegenJavaScript.hs+20−20 src/IRTS/LParser.hs+17−17 src/IRTS/Lang.hs+7−8 src/Idris/Primitives.hs+114−149

effects/Effect/Memory.idr+2−2

@@ -65,9 +65,9 @@ private

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

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

6767do_peek ptr offset (S n)

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

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

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

7171

7272private

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

lib/Builtins.idr+4−4

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

251251 (*) = prim__mulBigInt

252252

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

254− fromInteger = prim__intToBigInt

254+ fromInteger = prim__sextInt_BigInt

255255

256256

257257instance Num Float where

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

260260 (*) = prim__mulFloat

261261

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

263− fromInteger = prim__intToFloat

263+ fromInteger = prim__toFloatInt

264264

265265partial

266266div : Int -> Int -> Int

267−div = prim__divInt

267+div = prim__sdivInt

268268

269269partial

270270mod : Int -> Int -> Int

271−mod = prim__modInt

271+mod = prim__sremInt

272272

273273

274274(/) : Float -> Float -> Float

lib/Data/Bits.idr+40−40

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

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

3232natToBits' a O = a

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

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

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

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

37− natToBits' a (S x') | S (S (S _)) = natToBits' (prim__addB64 a (prim__intToB64 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' (prim__addB16 a (prim__truncInt_B16 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 _)) = natToBits' (prim__addB64 a (prim__truncInt_B64 1)) x'

3838

3939natToBits : Nat -> machineTy n

4040natToBits {n=n} x with n

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

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

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

44− | S (S (S _)) = natToBits' (prim__intToB64 0) x

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

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

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

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

4545

4646getPad : Nat -> machineTy n

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

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

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

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

310310 | (O, O) = believe_me x

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

320320

321321public

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

336336

337337public

338338intToBits : Int -> Bits n

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

343343

344344bitsToInt' : machineTy n -> Int

345345bitsToInt' {n=n} x with n

346− | O = prim__B32ToInt (prim__zextB8_32 x)

347− | S O = prim__B32ToInt (prim__zextB16_32 x)

348− | S (S O) = prim__B32ToInt x

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

346+ | O = prim__zextB8_Int x

347+ | S O = prim__zextB16_Int x

348+ | S (S O) = prim__zextB32_Int x

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

350350

351351public

352352bitsToInt : Bits n -> Int

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

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

366366 believe_me (prim__ashrB8 (prim__shlB8 (believe_me x) pad) pad)

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

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

369− (prim__zextB8_16 pad))

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

369+ (prim__zextB8_B16 pad))

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

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

372− (prim__zextB8_32 pad))

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

372+ (prim__zextB8_B32 pad))

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

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

375− (prim__zextB8_64 pad))

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

375+ (prim__zextB8_B64 pad))

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

377377 believe_me (prim__ashrB16 (prim__shlB16 (believe_me x) pad) pad)

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

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

380− (prim__zextB16_32 pad))

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

380+ (prim__zextB16_B32 pad))

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

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

383− (prim__zextB16_64 pad))

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

383+ (prim__zextB16_B64 pad))

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

385385 believe_me (prim__ashrB32 (prim__shlB32 (believe_me x) pad) pad)

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

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

388− (prim__zextB32_64 pad))

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

388+ (prim__zextB32_B64 pad))

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

390390 believe_me (prim__ashrB64 (prim__shlB64 (believe_me x) pad) pad)

391391

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

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

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

399399 | (O, O) = believe_me x

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

409409

410410public

lib/Network/Cgi.idr+1−1

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

121121runCGI : CGI a -> IO a

122122runCGI prog = do

123123 clen_in <- getEnv "CONTENT_LENGTH"

124− let clen = prim__strToInt clen_in

124+ let clen = prim__fromStrInt clen_in

125125 content <- getContent clen

126126 query <- getEnv "QUERY_STRING"

127127 cookie <- getEnv "HTTP_COOKIE"

lib/Prelude.idr+2−2

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

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

3030

3131instance Show Int where

32− show = prim__intToStr

32+ show = prim__toStrInt

3333

3434instance Show Integer where

35− show = prim__bigIntToStr

35+ show = prim__toStrBigInt

3636

3737instance Show Float where

3838 show = prim__floatToStr

lib/Prelude/Cast.idr+7−7

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

66-- String casts

88instance Cast String Int where

9− cast = prim__strToInt

9+ cast = prim__fromStrInt

1010

1111instance Cast String Float where

1212 cast = prim__strToFloat

1313

1414instance Cast String Integer where

15− cast = prim__strToBigInt

15+ cast = prim__fromStrBigInt

1616

1717-- Int casts

1818

1919instance Cast Int String where

20− cast = prim__intToStr

20+ cast = prim__toStrInt

2121

2222instance Cast Int Float where

23− cast = prim__intToFloat

23+ cast = prim__toFloatInt

2424

2525instance Cast Int Integer where

26− cast = prim__intToBigInt

26+ cast = prim__sextInt_BigInt

2727

2828instance Cast Int Char where

2929 cast = prim__intToChar

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

3434 cast = prim__floatToStr

3535

3636instance Cast Float Int where

37− cast = prim__floatToInt

37+ cast = prim__fromFloatInt

3838

3939-- Integer casts

4040

4141instance Cast Integer String where

42− cast = prim__bigIntToStr

42+ cast = prim__toStrBigInt

4343

4444-- Char casts

4545

rts/idris_rts.c+2−3

@@ -275,9 +275,8 @@ void idris_memset(void* ptr, i_int offset, uint8_t c, i_int size) {

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

276276}

277277

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

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

280− return (int)res;

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

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

281280}

282281

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

rts/idris_rts.h+1−1

@@ -209,7 +209,7 @@ VAL idris_castStrFloat(VM* vm, VAL i);

209209

210210// Raw memory manipulation

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

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

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

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

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

215215

src/IRTS/CodegenC.hs+24−28

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

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

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

284284

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

296295

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

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

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

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

301300

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

312311

@@ -314,13 +313,6 @@ doOp v LReadStr [x] = v ++ "idris_readStr(vm, GETPTR(" ++ creg x ++ "))"

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

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

316315

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

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

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

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

321−

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

323−

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

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

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

@@ -345,8 +337,12 @@ doOp v (LSRem ty) [x, y] = bitOp v "SRem" ty [x, y]

345337

346338doOp v (LSExt from to) [x]

347339 | intTyWidth from < intTyWidth to = bitCoerce v "S" from to x

340+doOp v (LZExt ITNative to) [x] = v ++ "idris_b" ++ show (intTyWidth to) ++ "(vm, " ++ creg x ++ ")"

341+doOp v (LZExt IT32 ITNative) [x] = v ++ "idris_castB32Int(vm, " ++ creg x ++ ")"

348342doOp v (LZExt from to) [x]

349343 | intTyWidth from < intTyWidth to = bitCoerce v "Z" from to x

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

345+doOp v (LTrunc IT32 ITNative) [x] = v ++ "idris_castB32Int(vm, " ++ creg x ++ ")"

350346doOp v (LTrunc from to) [x]

351347 | intTyWidth from > intTyWidth to = bitCoerce v "T" from to x

352348

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

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

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

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

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

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

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

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

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

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

src/IRTS/CodegenJava.hs+27−33

@@ -484,6 +484,7 @@ intTyToIdent IT16 = Ident "Short"

484484intTyToIdent IT32 = Ident "Integer"

485485intTyToIdent IT64 = Ident "Long"

486486intTyToIdent ITNative = Ident "Integer"

487+intTyToIdent ITBig = Ident "BigInteger"

487488

488489intTyToClass :: IntTy -> ClassType

489490intTyToClass ty = ClassType [(intTyToIdent ty, [])]

@@ -1311,35 +1312,35 @@ mkExp (SOp LFLt args) = mkLogicalBinOpExp integerType LThan args

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

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

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

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

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

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

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

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

1319−mkExp (SOp LBEq args) =

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

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

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

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

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

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

13201321 mkMethodOpChain1 (mkBoolToNumber bigIntegerType) bigIntegerType "equals" args

1321−mkExp (SOp LBLt args) =

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

13221323 mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

13231324 . mkPartialOrder SLt

13241325 )

13251326 bigIntegerType

13261327 "compareTo"

13271328 args

1328−mkExp (SOp LBLe args) =

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

13291330 mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

13301331 . mkPartialOrder SLe

13311332 )

13321333 bigIntegerType

13331334 "compareTo"

13341335 args

1335−mkExp (SOp LBGt args) =

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

13361337 mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

13371338 . mkPartialOrder SGt

13381339 )

13391340 bigIntegerType

13401341 "compareTo"

13411342 args

1342−mkExp (SOp LBGe args) =

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

13431344 mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

13441345 . mkPartialOrder SGe

13451346 )

@@ -1368,33 +1369,31 @@ mkExp (SOp LStrEq args@[_, _]) =

13681369 stringType

13691370 "equals"

13701371 args

1371−mkExp (SOp LStrLen [arg]) =

1372+mkExp (SOp LStrLen [arg]) =

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

13731374 <$> mkVarAccess (Just stringType) arg

1374−mkExp (SOp LIntFloat [arg]) =

1375− mkPrimitiveCast integerType doubleType arg

1376−mkExp (SOp LFloatInt [arg]) =

1377− mkPrimitiveCast doubleType integerType arg

1378−mkExp (SOp LIntStr [arg]) =

1379− mkToString integerType arg

1380−mkExp (SOp LStrInt [arg]) =

1381− mkPrimitiveCast stringType integerType arg

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

1376+ mkPrimitiveCast (intTyToClass ity) doubleType arg

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

1378+ mkPrimitiveCast doubleType (intTyToClass ity) arg

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

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

1381+ <$> mkVarAccess (Just stringType) arg

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

1383+ mkToString (intTyToClass ity) arg

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

1385+ mkPrimitiveCast stringType (intTyToClass ity) arg

13821386mkExp (SOp LFloatStr [arg]) =

13831387 mkToString doubleType arg

13841388mkExp (SOp LStrFloat [arg]) =

13851389 mkPrimitiveCast doubleType stringType arg

1386−mkExp (SOp LIntBig [arg]) =

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

13871391 mkPrimitiveCast integerType bigIntegerType arg

1388−mkExp (SOp LBigInt [arg]) =

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

13891393 mkPrimitiveCast bigIntegerType integerType arg

1390−mkExp (SOp LStrBig [arg]) =

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

1392− <$> mkVarAccess (Just stringType) arg

1393−mkExp (SOp LBigStr [arg]) =

1394− mkToString bigIntegerType arg

1395−mkExp (SOp LChInt [arg]) =

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

13961395 mkVarAccess (Just integerType) arg

1397−mkExp (SOp LIntCh [arg]) =

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

13981397 mkVarAccess (Just integerType) arg

13991398mkExp (SOp LPrintNum [arg]) =

14001399 mkSystemOutPrint <$> (mkVarAccess Nothing arg)

@@ -1495,11 +1494,6 @@ mkExp (SOp (LTrunc from to) [var])

14951494 $ PrimaryMethodCall var [] (Ident (intTyToMethod to)) [] ]

14961495 )

14971496 <$> mkVarAccess (Just $ intTyToClass from) var

1498−mkExp (SOp LIntB8 [arg]) = mkExp (SOp (LTrunc IT32 IT8) [arg])

1499−mkExp (SOp LIntB16 [arg]) = mkExp (SOp (LTrunc IT32 IT16) [arg])

1500−mkExp (SOp LIntB32 [arg]) = mkExp (SV arg)

1501−mkExp (SOp LIntB64 [arg]) = mkExp (SOp (LSExt IT32 IT64) [arg])

1502−mkExp (SOp LB32Int [arg]) = mkExp (SV arg)

15031497mkExp (SOp LFExp [arg]) = mkMathFun "exp" arg

15041498mkExp (SOp LFLog [arg]) = mkMathFun "log" arg

15051499mkExp (SOp LFSin [arg]) = mkMathFun "sin" arg

src/IRTS/CodegenJavaScript.hs+20−20

@@ -236,25 +236,25 @@ translateExpression (SOp op vars)

236236 | (LCompl _) <- op

237237 , (arg:_) <- vars = '~' : translateVariableName arg

238238

239− | LBPlus <- op

239+ | (LPlus ITBig) <- op

240240 , (lhs:rhs:_) <- vars = translateBinaryOp ".add(" lhs rhs ++ ")"

241− | LBMinus <- op

241+ | (LMinus ITBig) <- op

242242 , (lhs:rhs:_) <- vars = translateBinaryOp ".minus(" lhs rhs ++ ")"

243− | LBTimes <- op

243+ | (LTimes ITBig) <- op

244244 , (lhs:rhs:_) <- vars = translateBinaryOp ".times(" lhs rhs ++ ")"

245− | LBDiv <- op

245+ | (LSDiv ITBig) <- op

246246 , (lhs:rhs:_) <- vars = translateBinaryOp ".divide(" lhs rhs ++ ")"

247− | LBMod <- op

247+ | (LSRem ITBig) <- op

248248 , (lhs:rhs:_) <- vars = translateBinaryOp ".mod(" lhs rhs ++ ")"

249− | LBEq <- op

249+ | (LEq ITBig) <- op

250250 , (lhs:rhs:_) <- vars = translateBinaryOp ".equals(" lhs rhs ++ ")"

251− | LBLt <- op

251+ | (LLt ITBig) <- op

252252 , (lhs:rhs:_) <- vars = translateBinaryOp ".lesser(" lhs rhs ++ ")"

253− | LBLe <- op

253+ | (LLe ITBig) <- op

254254 , (lhs:rhs:_) <- vars = translateBinaryOp ".lesserOrEquals(" lhs rhs ++ ")"

255− | LBGt <- op

255+ | (LGt ITBig) <- op

256256 , (lhs:rhs:_) <- vars = translateBinaryOp ".greater(" lhs rhs ++ ")"

257− | LBGe <- op

257+ | (LGe ITBig) <- op

258258 , (lhs:rhs:_) <- vars = translateBinaryOp ".greaterOrEquals(" lhs rhs ++ ")"

259259

260260 | LFPlus <- op

@@ -285,29 +285,29 @@ translateExpression (SOp op vars)

285285 | LStrLen <- op

286286 , (arg:_) <- vars = translateVariableName arg ++ ".length"

287287

288− | LStrInt <- op

288+ | (LStrInt ITNative) <- op

289289 , (arg:_) <- vars = "parseInt(" ++ translateVariableName arg ++ ")"

290− | LIntStr <- op

290+ | (LIntStr ITNative) <- op

291291 , (arg:_) <- vars = "String(" ++ translateVariableName arg ++ ")"

292− | LIntBig <- op

292+ | (LSExt ITNative ITBig) <- op

293293 , (arg:_) <- vars = "__IDRRT__.bigInt(" ++ translateVariableName arg ++ ")"

294− | LBigInt <- op

294+ | (LTrunc ITBig ITNative) <- op

295295 , (arg:_) <- vars = translateVariableName arg ++ ".valueOf()"

296− | LBigStr <- op

296+ | (LIntStr ITBig) <- op

297297 , (arg:_) <- vars = translateVariableName arg ++ ".toString()"

298− | LStrBig <- op

298+ | (LStrInt ITBig) <- op

299299 , (arg:_) <- vars = "__IDRRT__.bigInt(" ++ translateVariableName arg ++ ")"

300300 | LFloatStr <- op

301301 , (arg:_) <- vars = "String(" ++ translateVariableName arg ++ ")"

302302 | LStrFloat <- op

303303 , (arg:_) <- vars = "parseFloat(" ++ translateVariableName arg ++ ")"

304− | LIntFloat <- op

304+ | (LIntFloat ITNative) <- op

305305 , (arg:_) <- vars = translateVariableName arg

306− | LFloatInt <- op

306+ | (LFloatInt ITNative) <- op

307307 , (arg:_) <- vars = translateVariableName arg

308− | LChInt <- op

308+ | (LChInt ITNative) <- op

309309 , (arg:_) <- vars = translateVariableName arg ++ ".charCodeAt(0)"

310− | LIntCh <- op

310+ | (LIntCh ITNative) <- op

311311 , (arg:_) <- vars =

312312 "String.fromCharCode(" ++ translateVariableName arg ++ ")"

313313

src/IRTS/LParser.hs+17−17

@@ -96,8 +96,8 @@ optable = [[binary "*" (\x y -> LOp (LTimes ITNative) [x,y]) AssocLeft,

9696 binary "/" (\x y -> LOp (LSDiv ITNative) [x,y]) AssocLeft,

9797 binary "*." (\x y -> LOp LFTimes [x,y]) AssocLeft,

9898 binary "/." (\x y -> LOp LFDiv [x,y]) AssocLeft,

99− binary "*:" (\x y -> LOp LBTimes [x,y]) AssocLeft,

100− binary "/:" (\x y -> LOp LBDiv [x,y]) AssocLeft

99+ binary "*:" (\x y -> LOp (LTimes ITBig) [x,y]) AssocLeft,

100+ binary "/:" (\x y -> LOp (LSDiv ITBig) [x,y]) AssocLeft

101101 ],

102102 [

103103 binary "+" (\x y -> LOp (LPlus ITNative) [x,y]) AssocLeft,

@@ -105,8 +105,8 @@ optable = [[binary "*" (\x y -> LOp (LTimes ITNative) [x,y]) AssocLeft,

105105 binary "++" (\x y -> LOp LStrConcat [x,y]) AssocLeft,

106106 binary "+." (\x y -> LOp LFPlus [x,y]) AssocLeft,

107107 binary "-." (\x y -> LOp LFMinus [x,y]) AssocLeft,

108− binary "+:" (\x y -> LOp LBPlus [x,y]) AssocLeft,

109− binary "-:" (\x y -> LOp LBMinus [x,y]) AssocLeft

108+ binary "+:" (\x y -> LOp (LPlus ITBig) [x,y]) AssocLeft,

109+ binary "-:" (\x y -> LOp (LMinus ITBig) [x,y]) AssocLeft

110110 ],

111111 [

112112 binary "==" (\x y -> LOp (LEq ITNative) [x, y]) AssocNone,

@@ -120,11 +120,11 @@ optable = [[binary "*" (\x y -> LOp (LTimes ITNative) [x,y]) AssocLeft,

120120 binary ">=" (\x y -> LOp (LGe ITNative) [x, y]) AssocNone,

121121 binary ">=." (\x y -> LOp LFGe [x, y]) AssocNone,

122122

123− binary "==:" (\x y -> LOp LBEq [x, y]) AssocNone,

124− binary "<:" (\x y -> LOp LBLt [x, y]) AssocNone,

125− binary ">:" (\x y -> LOp LBGt [x, y]) AssocNone,

126− binary "<=:" (\x y -> LOp LBLe [x, y]) AssocNone,

127− binary ">=:" (\x y -> LOp LBGe [x, y]) AssocNone

123+ binary "==:" (\x y -> LOp (LEq ITBig) [x, y]) AssocNone,

124+ binary "<:" (\x y -> LOp (LLt ITBig) [x, y]) AssocNone,

125+ binary ">:" (\x y -> LOp (LGt ITBig) [x, y]) AssocNone,

126+ binary "<=:" (\x y -> LOp (LLe ITBig) [x, y]) AssocNone,

127+ binary ">=:" (\x y -> LOp (LGe ITBig) [x, y]) AssocNone

128128 ]]

129129

130130binary name f assoc = Infix (do reservedOp name; return f) assoc

@@ -184,21 +184,21 @@ pCast = do reserved "FloatString"; lchar '('; e <- pLExp; lchar ')'

184184 <|> do reserved "StringFloat"; lchar '('; e <- pLExp; lchar ')'

185185 return (LOp LStrFloat [e])

186186 <|> do reserved "FloatInt"; lchar '('; e <- pLExp; lchar ')'

187− return (LOp LFloatInt [e])

187+ return (LOp (LFloatInt ITNative) [e])

188188 <|> do reserved "IntFloat"; lchar '('; e <- pLExp; lchar ')'

189− return (LOp LIntFloat [e])

189+ return (LOp (LIntFloat ITNative) [e])

190190 <|> do reserved "StringInt"; lchar '('; e <- pLExp; lchar ')'

191− return (LOp LStrInt [e])

191+ return (LOp (LStrInt ITNative) [e])

192192 <|> do reserved "IntString"; lchar '('; e <- pLExp; lchar ')'

193− return (LOp LIntStr [e])

193+ return (LOp (LIntStr ITNative) [e])

194194 <|> do reserved "BigInt"; lchar '('; e <- pLExp; lchar ')'

195− return (LOp LBigInt [e])

195+ return (LOp (LTrunc ITBig ITNative) [e])

196196 <|> do reserved "IntBig"; lchar '('; e <- pLExp; lchar ')'

197− return (LOp LIntBig [e])

197+ return (LOp (LSExt ITNative ITBig) [e])

198198 <|> do reserved "BigString"; lchar '('; e <- pLExp; lchar ')'

199− return (LOp LBigStr [e])

199+ return (LOp (LIntStr ITBig) [e])

200200 <|> do reserved "StringBig"; lchar '('; e <- pLExp; lchar ')'

201− return (LOp LStrBig [e])

201+ return (LOp (LStrInt ITBig) [e])

202202

203203pPrim :: LParser LExp

204204pPrim = do reserved "StrEq"; lchar '(';

src/IRTS/Lang.hs+7−8

@@ -3,6 +3,7 @@ module IRTS.Lang where

33import Core.TT

44import Control.Monad.State hiding(lift)

55import Data.List

6+import Foreign.Storable (sizeOf)

67import Debug.Trace

89data LVar = Loc Int | Glob Name

@@ -28,7 +29,7 @@ data LExp = LV LVar

2829-- Primitive operators. Backends are not *required* to implement all

2930-- of these, but should report an error if they are unable

3031

31−data IntTy = ITNative | IT8 | IT16 | IT32 | IT64

32+data IntTy = ITNative | IT8 | IT16 | IT32 | IT64 | ITBig

3233 deriving (Show, Eq)

3334

3435intTyWidth :: IntTy -> Int

@@ -36,13 +37,15 @@ intTyWidth IT8 = 8

3637intTyWidth IT16 = 16

3738intTyWidth IT32 = 32

3839intTyWidth IT64 = 64

39−intTyWidth ITNative = error "IRTS.Lang.intTyWidth: Native integer width is unspecified"

40+intTyWidth ITNative = 8 * sizeOf (0 :: Int)

41+intTyWidth ITBig = error "IRTS.Lang.intTyWidth: Big integers have variable width"

4042

4143intTyToConst :: IntTy -> Const

4244intTyToConst IT8 = B8Type

4345intTyToConst IT16 = B16Type

4446intTyToConst IT32 = B32Type

4547intTyToConst IT64 = B64Type

48+intTyToConst ITBig = BIType

4649intTyToConst ITNative = IType

4750

4851data PrimFn = LPlus IntTy | LMinus IntTy | LTimes IntTy

@@ -53,15 +56,11 @@ data PrimFn = LPlus IntTy | LMinus IntTy | LTimes IntTy

5356 | LSExt IntTy IntTy | LZExt IntTy IntTy | LTrunc IntTy IntTy

5457 | LFPlus | LFMinus | LFTimes | LFDiv

5859 | LStrConcat | LStrLt | LStrEq | LStrLen

60+ | LIntFloat IntTy | LFloatInt IntTy | LIntStr IntTy | LStrInt IntTy

61+ | LFloatStr | LStrFloat | LChInt IntTy | LIntCh IntTy

6162 | LPrintNum | LPrintStr | LReadStr

6263

64−

6665 | LFSqrt | LFFloor | LFCeil

6766

src/Idris/Primitives.hs+114−149

@@ -1,4 +1,4 @@

1−{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}

1+{-# LANGUAGE RankNTypes, ScopedTypeVariables, PatternGuards #-}

33module Idris.Primitives(elabPrims) where

@@ -34,39 +34,7 @@ partial = Partial NotCovering

3434

3535primitives =

3636 -- operators

37− [Prim (UN "prim__addInt") (ty [IType, IType] IType) 2 (iBin (+))

38− (2, LPlus ITNative) total,

39− Prim (UN "prim__subInt") (ty [IType, IType] IType) 2 (iBin (-))

40− (2, LMinus ITNative) total,

41− Prim (UN "prim__mulInt") (ty [IType, IType] IType) 2 (iBin (*))

42− (2, LTimes ITNative) total,

43− Prim (UN "prim__divInt") (ty [IType, IType] IType) 2 (iBin div)

44− (2, LSDiv ITNative) partial,

45− Prim (UN "prim__modInt") (ty [IType, IType] IType) 2 (iBin mod)

46− (2, LSRem ITNative) partial,

47− Prim (UN "prim__andInt") (ty [IType, IType] IType) 2 (iBin (.&.))

48− (2, LAnd ITNative) partial,

49− Prim (UN "prim__orInt") (ty [IType, IType] IType) 2 (iBin (.|.))

50− (2, LOr ITNative) partial,

51− Prim (UN "prim__xorInt") (ty [IType, IType] IType) 2 (iBin xor)

52− (2, LXOr ITNative) partial,

53− Prim (UN "prim__shLInt") (ty [IType, IType] IType) 2 (iBin shiftL)

54− (2, LSHL ITNative) partial,

55− Prim (UN "prim__shRInt") (ty [IType, IType] IType) 2 (iBin shiftR)

56− (2, LASHR ITNative) partial,

57− Prim (UN "prim__complInt") (ty [IType] IType) 1 (iUn complement)

58− (1, LCompl ITNative) partial,

59− Prim (UN "prim__eqInt") (ty [IType, IType] IType) 2 (biBin (==))

60− (2, LEq ITNative) total,

61− Prim (UN "prim__ltInt") (ty [IType, IType] IType) 2 (biBin (<))

62− (2, LLt ITNative) total,

63− Prim (UN "prim__lteInt") (ty [IType, IType] IType) 2 (biBin (<=))

64− (2, LLe ITNative) total,

65− Prim (UN "prim__gtInt") (ty [IType, IType] IType) 2 (biBin (>))

66− (2, LGt ITNative) total,

67− Prim (UN "prim__gteInt") (ty [IType, IType] IType) 2 (biBin (>=))

68− (2, LGe ITNative) total,

69− Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==))

37+ [Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==))

7038 (2, LEq ITNative) total,

7139 Prim (UN "prim__ltChar") (ty [ChType, ChType] IType) 2 (bcBin (<))

7240 (2, LLt ITNative) total,

@@ -80,55 +48,59 @@ primitives =

8048 iCoerce IT8 IT16 "zext" zext LZExt,

8149 iCoerce IT8 IT32 "zext" zext LZExt,

8250 iCoerce IT8 IT64 "zext" zext LZExt,

51+ iCoerce IT8 ITBig "zext" zext LZExt,

52+ iCoerce IT8 ITNative "zext" zext LZExt,

8353 iCoerce IT16 IT32 "zext" zext LZExt,

8454 iCoerce IT16 IT64 "zext" zext LZExt,

55+ iCoerce IT16 ITBig "zext" zext LZExt,

56+ iCoerce IT16 ITNative "zext" zext LZExt,

8557 iCoerce IT32 IT64 "zext" zext LZExt,

58+ iCoerce IT32 ITBig "zext" zext LZExt,

59+ iCoerce IT32 ITNative "zext" zext LZExt,

60+ iCoerce IT64 ITBig "zext" zext LZExt,

61+ iCoerce ITNative ITBig "zext" zext LZExt,

62+ iCoerce ITNative IT64 "zext" zext LZExt,

63+ iCoerce ITNative IT32 "zext" zext LZExt,

64+ iCoerce ITNative IT16 "zext" zext LZExt,

8665

8766 iCoerce IT8 IT16 "sext" sext LSExt,

8867 iCoerce IT8 IT32 "sext" sext LSExt,

8968 iCoerce IT8 IT64 "sext" sext LSExt,

69+ iCoerce IT8 ITBig "sext" sext LSExt,

70+ iCoerce IT8 ITNative "sext" sext LSExt,

9071 iCoerce IT16 IT32 "sext" sext LSExt,

9172 iCoerce IT16 IT64 "sext" sext LSExt,

73+ iCoerce IT16 ITBig "sext" sext LSExt,

74+ iCoerce IT16 ITNative "sext" sext LSExt,

9275 iCoerce IT32 IT64 "sext" sext LSExt,

76+ iCoerce IT32 ITBig "sext" sext LSExt,

77+ iCoerce IT32 ITNative "sext" sext LSExt,

78+ iCoerce IT64 ITBig "sext" sext LSExt,

79+ iCoerce ITNative ITBig "sext" sext LSExt,

80+ iCoerce ITNative ITBig "sext" sext LSExt,

81+ iCoerce ITNative IT64 "sext" sext LSExt,

82+ iCoerce ITNative IT32 "sext" sext LSExt,

83+ iCoerce ITNative IT16 "sext" sext LSExt,

9384

9485 iCoerce IT16 IT8 "trunc" trunc LTrunc,

9586 iCoerce IT32 IT8 "trunc" trunc LTrunc,

9687 iCoerce IT64 IT8 "trunc" trunc LTrunc,

88+ iCoerce ITBig IT8 "trunc" trunc LTrunc,

89+ iCoerce ITNative IT8 "trunc" trunc LTrunc,

9790 iCoerce IT32 IT16 "trunc" trunc LTrunc,

9891 iCoerce IT64 IT16 "trunc" trunc LTrunc,

92+ iCoerce ITBig IT16 "trunc" trunc LTrunc,

93+ iCoerce ITNative IT16 "trunc" trunc LTrunc,

9994 iCoerce IT64 IT32 "trunc" trunc LTrunc,

95+ iCoerce ITBig IT32 "trunc" trunc LTrunc,

96+ iCoerce ITNative IT32 "trunc" trunc LTrunc,

97+ iCoerce ITBig IT64 "trunc" trunc LTrunc,

98+ iCoerce IT16 ITNative "trunc" trunc LTrunc,

99+ iCoerce IT32 ITNative "trunc" trunc LTrunc,

100+ iCoerce IT64 ITNative "trunc" trunc LTrunc,

101+ iCoerce ITBig ITNative "trunc" trunc LTrunc,

102+ iCoerce ITNative IT64 "trunc" trunc LTrunc,

100103

101− Prim (UN "prim__intToB8") (ty [IType] B8Type) 1 intToBits8

102− (1, LIntB8) total,

103− Prim (UN "prim__intToB16") (ty [IType] B16Type) 1 intToBits16

104− (1, LIntB16) total,

105− Prim (UN "prim__intToB32") (ty [IType] B32Type) 1 intToBits32

106− (1, LIntB32) total,

107− Prim (UN "prim__intToB64") (ty [IType] B64Type) 1 intToBits64

108− (1, LIntB64) total,

109− Prim (UN "prim__B32ToInt") (ty [B32Type] IType) 1 bits32ToInt

110− (1, LB32Int) total,

111−

112− Prim (UN "prim__addBigInt") (ty [BIType, BIType] BIType) 2 (bBin (+))

113− (2, LBPlus) total,

114− Prim (UN "prim__subBigInt") (ty [BIType, BIType] BIType) 2 (bBin (-))

115− (2, LBMinus) total,

116− Prim (UN "prim__mulBigInt") (ty [BIType, BIType] BIType) 2 (bBin (*))

117− (2, LBTimes) total,

118− Prim (UN "prim__divBigInt") (ty [BIType, BIType] BIType) 2 (bBin div)

119− (2, LBDiv) partial,

120− Prim (UN "prim__modBigInt") (ty [BIType, BIType] BIType) 2 (bBin mod)

121− (2, LBMod) partial,

122− Prim (UN "prim__eqBigInt") (ty [BIType, BIType] IType) 2 (bbBin (==))

123− (2, LBEq) total,

124− Prim (UN "prim__ltBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<))

125− (2, LBLt) total,

126− Prim (UN "prim__lteBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<=))

127− (2, LBLe) total,

128− Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>))

129− (2, LBGt) total,

130− Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>=))

131− (2, LBGe) total,

132104 Prim (UN "prim__addFloat") (ty [FlType, FlType] FlType) 2 (fBin (+))

133105 (2, LFPlus) total,

134106 Prim (UN "prim__subFloat") (ty [FlType, FlType] FlType) 2 (fBin (-))

@@ -156,30 +128,14 @@ primitives =

156128 Prim (UN "prim_lenString") (ty [StrType] IType) 1 (p_strLen)

157129 (1, LStrLen) total,

158130 -- Conversions

159− Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt)

160− (1, LStrInt) total,

161− Prim (UN "prim__intToStr") (ty [IType] StrType) 1 (c_intToStr)

162− (1, LIntStr) total,

163131 Prim (UN "prim__charToInt") (ty [ChType] IType) 1 (c_charToInt)

164− (1, LChInt) total,

132+ (1, LChInt ITNative) total,

165133 Prim (UN "prim__intToChar") (ty [IType] ChType) 1 (c_intToChar)

166− (1, LIntCh) total,

167− Prim (UN "prim__intToBigInt") (ty [IType] BIType) 1 (c_intToBigInt)

168− (1, LIntBig) total,

169− Prim (UN "prim__bigIntToInt") (ty [BIType] IType) 1 (c_bigIntToInt)

170− (1, LBigInt) total,

171− Prim (UN "prim__strToBigInt") (ty [StrType] BIType) 1 (c_strToBigInt)

172− (1, LStrBig) total,

173− Prim (UN "prim__bigIntToStr") (ty [BIType] StrType) 1 (c_bigIntToStr)

174− (1, LBigStr) total,

134+ (1, LIntCh ITNative) total,

175135 Prim (UN "prim__strToFloat") (ty [StrType] FlType) 1 (c_strToFloat)

176136 (1, LStrFloat) total,

177137 Prim (UN "prim__floatToStr") (ty [FlType] StrType) 1 (c_floatToStr)

178138 (1, LFloatStr) total,

179− Prim (UN "prim__intToFloat") (ty [IType] FlType) 1 (c_intToFloat)

180− (1, LIntFloat) total,

181− Prim (UN "prim__floatToInt") (ty [FlType] IType) 1 (c_floatToInt)

182− (1, LFloatInt) total,

183139

184140 Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)

185141 (1, LFExp) total,

@@ -223,7 +179,7 @@ primitives =

223179 (0, LStdIn) partial,

224180 Prim (UN "prim__believe_me") believeTy 3 (p_believeMe)

225181 (3, LNoOp) partial -- ahem

226− ] ++ concatMap intOps [IT8, IT16, IT32, IT64]

182+ ] ++ concatMap intOps [IT8, IT16, IT32, IT64, ITBig, ITNative]

227183

228184intOps ity =

229185 [ iCmp ity "lt" (bCmp ity (<)) LLt total

@@ -245,13 +201,26 @@ intOps ity =

245201 , iBinOp ity "or" (bitBin ity (.|.)) LOr total

246202 , iBinOp ity "xor" (bitBin ity (xor)) LXOr total

247203 , 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

248212 ]

249213

250−iCmp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ "B" ++ show (intTyWidth ity)) (ty (replicate 2 $ intTyToConst ity) IType) 2 impl (2, irop ity) totality

251−iBinOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ "B" ++ show (intTyWidth ity)) (ty (replicate 2 $ intTyToConst ity) (intTyToConst ity)) 2 impl (2, irop ity) totality

252−iUnOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ "B" ++ show (intTyWidth ity)) (ty [intTyToConst ity] (intTyToConst ity)) 1 impl (1, irop ity) totality

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

253222iCoerce from to op impl irop =

254− Prim (UN $ "prim__" ++ op ++ "B" ++ show (intTyWidth from) ++ "_" ++ show (intTyWidth to))

223+ Prim (UN $ "prim__" ++ op ++ intTyName from ++ "_" ++ intTyName to)

255224 (ty [intTyToConst from] (intTyToConst to)) 1 (impl from to) (1, irop from to) total

256225

257226p_believeMe [_,_,x] = Just x

@@ -329,6 +298,8 @@ bUn IT8 op [VConstant (B8 x)] = Just $ VConstant (B8 (op x))

329298bUn IT16 op [VConstant (B16 x)] = Just $ VConstant (B16 (op x))

330299bUn IT32 op [VConstant (B32 x)] = Just $ VConstant (B32 (op x))

331300bUn 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))

332303bUn _ _ _ = Nothing

333304

334305bitBin :: IntTy -> (forall a. (Bits a, Integral a) => a -> a -> a) -> [Value] -> Maybe Value

@@ -336,6 +307,8 @@ bitBin IT8 op [VConstant (B8 x), VConstant (B8 y)] = Just $ VConstant (B8 (o

336307bitBin IT16 op [VConstant (B16 x), VConstant (B16 y)] = Just $ VConstant (B16 (op x y))

337308bitBin IT32 op [VConstant (B32 x), VConstant (B32 y)] = Just $ VConstant (B32 (op x y))

338309bitBin IT64 op [VConstant (B64 x), VConstant (B64 y)] = Just $ VConstant (B64 (op x y))

310+bitBin ITBig op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (BI (op x y))

311+bitBin ITNative op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))

339312bitBin _ _ _ = Nothing

340313

341314bCmp :: IntTy -> (forall a. Ord a => a -> a -> Bool) -> [Value] -> Maybe Value

@@ -343,73 +316,71 @@ bCmp IT8 op [VConstant (B8 x), VConstant (B8 y)] = Just $ VConstant (I (if (o

343316bCmp IT16 op [VConstant (B16 x), VConstant (B16 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))

344317bCmp IT32 op [VConstant (B32 x), VConstant (B32 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))

345318bCmp IT64 op [VConstant (B64 x), VConstant (B64 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))

320+bCmp ITNative op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (if (op x y) then 1 else 0))

346321bCmp _ _ _ = Nothing

347322

348−toB IT8 x = VConstant (B8 (fromIntegral x))

349−toB IT16 x = VConstant (B16 (fromIntegral x))

350−toB IT32 x = VConstant (B32 (fromIntegral x))

351−toB IT64 x = VConstant (B64 (fromIntegral x))

352−

353−zext IT8 IT16 [VConstant (B8 x)] = Just $ VConstant (B16 (fromIntegral x))

354−zext IT8 IT32 [VConstant (B8 x)] = Just $ VConstant (B32 (fromIntegral x))

355−zext IT8 IT64 [VConstant (B8 x)] = Just $ VConstant (B64 (fromIntegral x))

356−zext IT16 IT32 [VConstant (B16 x)] = Just $ VConstant (B32 (fromIntegral x))

357−zext IT16 IT64 [VConstant (B16 x)] = Just $ VConstant (B64 (fromIntegral x))

358−zext IT32 IT64 [VConstant (B32 x)] = Just $ VConstant (B64 (fromIntegral x))

323+toInt IT8 x = VConstant (B8 (fromIntegral x))

324+toInt IT16 x = VConstant (B16 (fromIntegral x))

325+toInt IT32 x = VConstant (B32 (fromIntegral x))

326+toInt IT64 x = VConstant (B64 (fromIntegral x))

327+toInt ITBig x = VConstant (BI (fromIntegral x))

328+toInt ITNative x = VConstant (I (fromIntegral x))

329+

330+intToInt IT8 out [VConstant (B8 x)] = Just $ toInt out x

331+intToInt IT16 out [VConstant (B16 x)] = Just $ toInt out x

332+intToInt IT32 out [VConstant (B32 x)] = Just $ toInt out x

333+intToInt IT64 out [VConstant (B64 x)] = Just $ toInt out x

334+intToInt ITBig out [VConstant (BI x)] = Just $ toInt out x

335+intToInt ITNative out [VConstant (I x)] = Just $ toInt out x

336+intToInt _ _ _ = Nothing

337+

338+zext from ITBig val = intToInt from ITBig val

339+zext ITBig _ _ = Nothing

340+zext from to val

341+ | intTyWidth from < intTyWidth to = intToInt from to val

359342zext _ _ _ = Nothing

360343

361−sext IT8 IT16 [VConstant (B8 x)] = Just $ VConstant (B16 (fromIntegral (fromIntegral x :: Int8)))

362−sext IT8 IT32 [VConstant (B8 x)] = Just $ VConstant (B32 (fromIntegral (fromIntegral x :: Int8)))

363−sext IT8 IT64 [VConstant (B8 x)] = Just $ VConstant (B64 (fromIntegral (fromIntegral x :: Int8)))

364−sext IT16 IT32 [VConstant (B16 x)] = Just $ VConstant (B32 (fromIntegral (fromIntegral x :: Int16)))

365−sext IT16 IT64 [VConstant (B16 x)] = Just $ VConstant (B64 (fromIntegral (fromIntegral x :: Int16)))

366−sext IT32 IT64 [VConstant (B32 x)] = Just $ VConstant (B64 (fromIntegral (fromIntegral x :: Int32)))

367−sext _ _ _ = Nothing

368−

369−trunc IT16 IT8 [VConstant (B16 x)] = Just $ VConstant (B8 (fromIntegral x))

370−trunc IT32 IT8 [VConstant (B32 x)] = Just $ VConstant (B8 (fromIntegral x))

371−trunc IT64 IT8 [VConstant (B64 x)] = Just $ VConstant (B8 (fromIntegral x))

372−trunc IT32 IT16 [VConstant (B32 x)] = Just $ VConstant (B16 (fromIntegral x))

373−trunc IT64 IT16 [VConstant (B64 x)] = Just $ VConstant (B16 (fromIntegral x))

374−trunc IT64 IT32 [VConstant (B64 x)] = Just $ VConstant (B32 (fromIntegral x))

344+sext IT8 out [VConstant (B8 x)] = Just $ toInt out (fromIntegral x :: Int8)

345+sext IT16 out [VConstant (B16 x)] = Just $ toInt out (fromIntegral x :: Int16)

346+sext IT32 out [VConstant (B32 x)] = Just $ toInt out (fromIntegral x :: Int32)

347+sext IT64 out [VConstant (B64 x)] = Just $ toInt out (fromIntegral x :: Int64)

348+sext ITBig _ _ = Nothing

349+sext from to val = intToInt from to val

350+

351+trunc ITBig to val = intToInt ITBig to val

352+trunc _ ITBig _ = Nothing

353+trunc from to val | intTyWidth from > intTyWidth to = intToInt from to val

375354trunc _ _ _ = Nothing

376355

377−intToBits8 [VConstant (I x)] = Just $ toB IT8 x

378−intToBits8 _ = Nothing

379−intToBits16 [VConstant (I x)] = Just $ toB IT16 x

380−intToBits16 _ = Nothing

381−intToBits32 [VConstant (I x)] = Just $ toB IT32 x

382−intToBits32 _ = Nothing

383−intToBits64 [VConstant (I x)] = Just $ toB IT64 x

384−intToBits64 _ = Nothing

385−

386−bits32ToInt [VConstant (B32 x)] = Just $ VConstant (I (fromIntegral x))

387−bits32ToInt _ = Nothing

388−

389−c_intToStr [VConstant (I x)] = Just $ VConstant (Str (show x))

390−c_intToStr _ = Nothing

391−c_strToInt [VConstant (Str x)] = case reads x of

392− [(n,"")] -> Just $ VConstant (I n)

393− _ -> Just $ VConstant (I 0)

394−c_strToInt _ = Nothing

356+getInt :: [Value] -> Maybe Integer

357+getInt [VConstant (B8 x)] = Just . toInteger $ x

358+getInt [VConstant (B16 x)] = Just . toInteger $ x

359+getInt [VConstant (B32 x)] = Just . toInteger $ x

360+getInt [VConstant (B64 x)] = Just . toInteger $ x

361+getInt [VConstant (I x)] = Just . toInteger $ x

362+getInt [VConstant (BI x)] = Just x

363+getInt _ = Nothing

364+

365+intToStr val | Just i <- getInt val = Just $ VConstant (Str (show i))

366+intToStr _ = Nothing

367+

368+strToInt ity [VConstant (Str x)] = case reads x of

369+ [(n,"")] -> Just $ toInt ity (n :: Integer)

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)

377+floatToInt _ _ = Nothing

395378

396379c_intToChar [VConstant (I x)] = Just $ VConstant (Ch (toEnum x))

397380c_intToChar _ = Nothing

398381c_charToInt [VConstant (Ch x)] = Just $ VConstant (I (fromEnum x))

399382c_charToInt _ = Nothing

400383

401−c_intToBigInt [VConstant (I x)] = Just $ VConstant (BI (fromIntegral x))

402−c_intToBigInt _ = Nothing

403−c_bigIntToInt [VConstant (BI x)] = Just $ VConstant (I (fromInteger x))

404−c_bigIntToInt _ = Nothing

405−

406−c_bigIntToStr [VConstant (BI x)] = Just $ VConstant (Str (show x))

407−c_bigIntToStr _ = Nothing

408−c_strToBigInt [VConstant (Str x)] = case reads x of

409− [(n,"")] -> Just $ VConstant (BI n)

410− _ -> Just $ VConstant (BI 0)

411−c_strToBigInt _ = Nothing

412−

413384c_floatToStr [VConstant (Fl x)] = Just $ VConstant (Str (show x))

414385c_floatToStr _ = Nothing

415386c_strToFloat [VConstant (Str x)] = case reads x of

@@ -417,12 +388,6 @@ c_strToFloat [VConstant (Str x)] = case reads x of

417388 _ -> Just $ VConstant (Fl 0)

418389c_strToFloat _ = Nothing

419390

420−c_floatToInt [VConstant (Fl x)] = Just $ VConstant (I (truncate x))

421−c_floatToInt _ = Nothing

422−

423−c_intToFloat [VConstant (I x)] = Just $ VConstant (Fl (fromIntegral x))

424−c_intToFloat _ = Nothing

425−

426391p_fPrim f [VConstant (Fl x)] = Just $ VConstant (Fl (f x))

427392p_fPrim f _ = Nothing

428393