b35df0d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'bitstring' of https://github.com/bitlisp/Idris-dev into bitlisp-bitstring

b35df0dEdwin Brady14 years ago

lib/Builtins.idr+4

compare with master

unifiedsplit

@@ -83,6 +83,10 @@ boolElim False t e = e

84data so : Bool -> Type where oh : so True

86+data Equality : {A : Type} -> (x : A) -> (y : A) -> Type where

87+ Unequal : {A : Type} -> {x : A} -> {y : A} -> (x = y -> _|_) -> Equality x y

88+ Equal : {A : Type} -> {x : A} -> {y : A} -> (x = y) -> Equality x y

89+

86syntax if [test] then [t] else [e] = boolElim test t e

90syntax if [test] then [t] else [e] = boolElim test t e

87syntax [test] "?" [t] ":" [e] = if test then t else e

91syntax [test] "?" [t] ":" [e] = if test then t else e

lib/Data/Bits.idr+432−18

@@ -1,25 +1,439 @@

1module Data.Bits

3−%access public

4−%default partial

3+%default total

6−infixl 5 .|.

5+divCeil : Nat -> Nat -> Nat

7−infixl 7 .&.

6+divCeil x y = case x `mod` y of

7+ O => x `div` y

8+ S _ => S (x `div` y)

10+nextPow2 : Nat -> Nat

11+nextPow2 O = O

12+nextPow2 x = if x == (2 `power` l2x)

13+ then l2x

14+ else S l2x

9−class Num a => Bits a where

15+ where

10− (.|.) : a -> a -> a

16+ l2x = log2 x

11− (.&.) : a -> a -> a

13− xor : a -> a -> a

18+nextBytes : Nat -> Nat

14− complement : a -> a

19+nextBytes bits = (nextPow2 (bits `divCeil` 8))

15− shiftL : a -> Int -> a

16− shiftR : a -> Int -> a

18−instance Bits Int where

21+machineTy : Nat -> Type

19− (.|.) = prim__orInt

22+machineTy O = Bits8

20− (.&.) = prim__andInt

23+machineTy (S O) = Bits16

24+machineTy (S (S O)) = Bits32

25+machineTy (S (S (S _))) = Bits64

22− xor = prim__xorInt

27+bitsUsed : Nat -> Nat

23− complement = prim__complInt

28+bitsUsed n = 8 * (2 `power` n)

24− shiftL = prim__shLInt

29+

25− shiftR = prim__shRInt

30+%assert_total

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

32+natToBits' a O = a

33+natToBits' {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'

38+

39+natToBits : Nat -> machineTy n

40+natToBits {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

45+

46+getPad : Nat -> machineTy n

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

48+

49+public

50+data Bits : Nat -> Type where

51+ MkBits : machineTy (nextBytes n) -> Bits n

52+

53+pad8 : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8

54+pad8 n f x y = prim__lshrB8 (f (prim__shlB8 x pad) (prim__shlB8 y pad)) pad

55+ where

56+ pad = getPad {n=0} n

57+

58+pad16 : Nat -> (Bits16 -> Bits16 -> Bits16) -> Bits16 -> Bits16 -> Bits16

59+pad16 n f x y = prim__lshrB16 (f (prim__shlB16 x pad) (prim__shlB16 y pad)) pad

60+ where

61+ pad = getPad {n=1} n

62+

63+pad32 : Nat -> (Bits32 -> Bits32 -> Bits32) -> Bits32 -> Bits32 -> Bits32

64+pad32 n f x y = prim__lshrB32 (f (prim__shlB32 x pad) (prim__shlB32 y pad)) pad

65+ where

66+ pad = getPad {n=2} n

67+

68+pad64 : Nat -> (Bits64 -> Bits64 -> Bits64) -> Bits64 -> Bits64 -> Bits64

69+pad64 n f x y = prim__lshrB64 (f (prim__shlB64 x pad) (prim__shlB64 y pad)) pad

70+ where

71+ pad = getPad {n=3} n

72+

73+-- These versions only pad the first operand

74+pad8' : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8

75+pad8' n f x y = prim__lshrB8 (f (prim__shlB8 x pad) y) pad

76+ where

77+ pad = getPad {n=0} n

78+

79+pad16' : Nat -> (Bits16 -> Bits16 -> Bits16) -> Bits16 -> Bits16 -> Bits16

80+pad16' n f x y = prim__lshrB16 (f (prim__shlB16 x pad) y) pad

81+ where

82+ pad = getPad {n=1} n

83+

84+pad32' : Nat -> (Bits32 -> Bits32 -> Bits32) -> Bits32 -> Bits32 -> Bits32

85+pad32' n f x y = prim__lshrB32 (f (prim__shlB32 x pad) y) pad

86+ where

87+ pad = getPad {n=2} n

88+

89+pad64' : Nat -> (Bits64 -> Bits64 -> Bits64) -> Bits64 -> Bits64 -> Bits64

90+pad64' n f x y = prim__lshrB64 (f (prim__shlB64 x pad) y) pad

91+ where

92+ pad = getPad {n=3} n

93+

94+shiftLeft' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

95+shiftLeft' {n=n} x c with (nextBytes n)

96+ | O = pad8' n prim__shlB8 x c

97+ | S O = pad16' n prim__shlB16 x c

98+ | S (S O) = pad32' n prim__shlB32 x c

99+ | S (S (S _)) = pad64' n prim__shlB64 x c

100+

101+public

102+shiftLeft : Bits n -> Bits n -> Bits n

103+shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)

104+

105+shiftRightLogical' : machineTy n -> machineTy n -> machineTy n

106+shiftRightLogical' {n=n} x c with n

107+ | O = prim__lshrB8 x c

108+ | S O = prim__lshrB16 x c

109+ | S (S O) = prim__lshrB32 x c

110+ | S (S (S _)) = prim__lshrB64 x c

111+

112+public

113+shiftRightLogical : Bits n -> Bits n -> Bits n

114+shiftRightLogical (MkBits x) (MkBits y) = MkBits (shiftRightLogical' x y)

115+

116+shiftRightArithmetic' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

117+shiftRightArithmetic' {n=n} x c with (nextBytes n)

118+ | O = pad8' n prim__ashrB8 x c

119+ | S O = pad16' n prim__ashrB16 x c

120+ | S (S O) = pad32' n prim__ashrB32 x c

121+ | S (S (S _)) = pad64' n prim__ashrB64 x c

122+

123+public

124+shiftRightArithmetic : Bits n -> Bits n -> Bits n

125+shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)

126+

127+and' : machineTy n -> machineTy n -> machineTy n

128+and' {n=n} x y with n

129+ | O = prim__andB8 x y

130+ | S O = prim__andB16 x y

131+ | S (S O) = prim__andB32 x y

132+ | S (S (S _)) = prim__andB64 x y

133+

134+public

135+and : Bits n -> Bits n -> Bits n

136+and (MkBits x) (MkBits y) = MkBits (and' x y)

137+

138+or' : machineTy n -> machineTy n -> machineTy n

139+or' {n=n} x y with n

140+ | O = prim__orB8 x y

141+ | S O = prim__orB16 x y

142+ | S (S O) = prim__orB32 x y

143+ | S (S (S _)) = prim__orB64 x y

144+

145+public

146+or : Bits n -> Bits n -> Bits n

147+or (MkBits x) (MkBits y) = MkBits (or' x y)

148+

149+xor' : machineTy n -> machineTy n -> machineTy n

150+xor' {n=n} x y with n

151+ | O = prim__xorB8 x y

152+ | S O = prim__xorB16 x y

153+ | S (S O) = prim__xorB32 x y

154+ | S (S (S _)) = prim__xorB64 x y

155+

156+public

157+xor : Bits n -> Bits n -> Bits n

158+xor (MkBits x) (MkBits y) = MkBits (xor' x y)

159+

160+plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

161+plus' {n=n} x y with (nextBytes n)

162+ | O = pad8 n prim__addB8 x y

163+ | S O = pad16 n prim__addB16 x y

164+ | S (S O) = pad32 n prim__addB32 x y

165+ | S (S (S _)) = pad64 n prim__addB64 x y

166+

167+public

168+plus : Bits n -> Bits n -> Bits n

169+plus (MkBits x) (MkBits y) = MkBits (plus' x y)

170+

171+minus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

172+minus' {n=n} x y with (nextBytes n)

173+ | O = pad8 n prim__subB8 x y

174+ | S O = pad16 n prim__subB16 x y

175+ | S (S O) = pad32 n prim__subB32 x y

176+ | S (S (S _)) = pad64 n prim__subB64 x y

177+

178+public

179+minus : Bits n -> Bits n -> Bits n

180+minus (MkBits x) (MkBits y) = MkBits (minus' x y)

181+

182+times' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

183+times' {n=n} x y with (nextBytes n)

184+ | O = pad8 n prim__mulB8 x y

185+ | S O = pad16 n prim__mulB16 x y

186+ | S (S O) = pad32 n prim__mulB32 x y

187+ | S (S (S _)) = pad64 n prim__mulB64 x y

188+

189+public

190+times : Bits n -> Bits n -> Bits n

191+times (MkBits x) (MkBits y) = MkBits (times' x y)

192+

193+partial

194+sdiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

195+sdiv' {n=n} x y with (nextBytes n)

196+ | O = prim__sdivB8 x y

197+ | S O = prim__sdivB16 x y

198+ | S (S O) = prim__sdivB32 x y

199+ | S (S (S _)) = prim__sdivB64 x y

200+

201+public partial

202+sdiv : Bits n -> Bits n -> Bits n

203+sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y)

204+

205+partial

206+udiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

207+udiv' {n=n} x y with (nextBytes n)

208+ | O = prim__udivB8 x y

209+ | S O = prim__udivB16 x y

210+ | S (S O) = prim__udivB32 x y

211+ | S (S (S _)) = prim__udivB64 x y

212+

213+public partial

214+udiv : Bits n -> Bits n -> Bits n

215+udiv (MkBits x) (MkBits y) = MkBits (udiv' x y)

216+

217+partial

218+srem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

219+srem' {n=n} x y with (nextBytes n)

220+ | O = prim__sremB8 x y

221+ | S O = prim__sremB16 x y

222+ | S (S O) = prim__sremB32 x y

223+ | S (S (S _)) = prim__sremB64 x y

224+

225+public partial

226+srem : Bits n -> Bits n -> Bits n

227+srem (MkBits x) (MkBits y) = MkBits (srem' x y)

228+

229+partial

230+urem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)

231+urem' {n=n} x y with (nextBytes n)

232+ | O = prim__uremB8 x y

233+ | S O = prim__uremB16 x y

234+ | S (S O) = prim__uremB32 x y

235+ | S (S (S _)) = prim__uremB64 x y

236+

237+public partial

238+urem : Bits n -> Bits n -> Bits n

239+urem (MkBits x) (MkBits y) = MkBits (urem' x y)

240+

241+-- TODO: Proofy comparisons via postulates

242+lt : machineTy n -> machineTy n -> Int

243+lt {n=n} x y with n

244+ | O = prim__ltB8 x y

245+ | S O = prim__ltB16 x y

246+ | S (S O) = prim__ltB32 x y

247+ | S (S (S _)) = prim__ltB64 x y

248+

249+lte : machineTy n -> machineTy n -> Int

250+lte {n=n} x y with n

251+ | O = prim__lteB8 x y

252+ | S O = prim__lteB16 x y

253+ | S (S O) = prim__lteB32 x y

254+ | S (S (S _)) = prim__lteB64 x y

255+

256+eq : machineTy n -> machineTy n -> Int

257+eq {n=n} x y with n

258+ | O = prim__eqB8 x y

259+ | S O = prim__eqB16 x y

260+ | S (S O) = prim__eqB32 x y

261+ | S (S (S _)) = prim__eqB64 x y

262+

263+gte : machineTy n -> machineTy n -> Int

264+gte {n=n} x y with n

265+ | O = prim__gteB8 x y

266+ | S O = prim__gteB16 x y

267+ | S (S O) = prim__gteB32 x y

268+ | S (S (S _)) = prim__gteB64 x y

269+

270+gt : machineTy n -> machineTy n -> Int

271+gt {n=n} x y with n

272+ | O = prim__gtB8 x y

273+ | S O = prim__gtB16 x y

274+ | S (S O) = prim__gtB32 x y

275+ | S (S (S _)) = prim__gtB64 x y

276+

277+instance Eq (Bits n) where

278+ (MkBits x) == (MkBits y) = boolOp eq x y

279+

280+instance Ord (Bits n) where

281+ (MkBits x) < (MkBits y) = boolOp lt x y

282+ (MkBits x) <= (MkBits y) = boolOp lte x y

283+ (MkBits x) >= (MkBits y) = boolOp gte x y

284+ (MkBits x) > (MkBits y) = boolOp gt x y

285+ compare (MkBits x) (MkBits y) =

286+ if boolOp lt x y

287+ then LT

288+ else if boolOp eq x y

289+ then EQ

290+ else GT

291+

292+complement' : machineTy (nextBytes n) -> machineTy (nextBytes n)

293+complement' {n=n} x with (nextBytes n)

294+ | O = let pad = getPad {n=0} n in

295+ prim__complB8 (x `prim__shlB8` pad) `prim__lshrB8` pad

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

297+ prim__complB16 (x `prim__shlB16` pad) `prim__lshrB16` pad

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

299+ prim__complB32 (x `prim__shlB32` pad) `prim__lshrB32` pad

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

301+ prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad

302+

303+public

304+complement : Bits n -> Bits n

305+complement (MkBits x) = MkBits (complement' x)

306+

307+-- TODO: Prove

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

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

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

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

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

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

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

320+

321+public

322+zeroExtend : Bits n -> Bits (n+m)

323+zeroExtend (MkBits x) = MkBits (zext' x)

324+

325+%assert_total

326+intToBits' : Int -> machineTy (nextBytes n)

327+intToBits' {n=n} x with (nextBytes n)

328+ | O = let pad = getPad {n=0} n in

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

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

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

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

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

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

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

336+

337+public

338+intToBits : Int -> Bits n

339+intToBits n = MkBits (intToBits' n)

340+

341+instance Cast Int (Bits n) where

342+ cast = intToBits

343+

344+bitsToInt' : machineTy n -> Int

345+bitsToInt' {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)

350+

351+public

352+bitsToInt : Bits n -> Int

353+bitsToInt (MkBits x) = bitsToInt' x

354+

355+-- Zero out the high bits of a truncated bitstring

356+zeroUnused : machineTy (nextBytes n) -> machineTy (nextBytes n)

357+zeroUnused x = x `and'` complement' (intToBits' 0)

358+

359+instance Cast Nat (Bits n) where

360+ cast x = MkBits (zeroUnused (natToBits n))

361+

362+-- TODO: Prove

363+sext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))

364+sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

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

366+ believe_me (prim__ashrB8 (prim__shlB8 (believe_me x) pad) pad)

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

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

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

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

377+ believe_me (prim__ashrB16 (prim__shlB16 (believe_me x) pad) pad)

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

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

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

385+ believe_me (prim__ashrB32 (prim__shlB32 (believe_me x) pad) pad)

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

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

390+ believe_me (prim__ashrB64 (prim__shlB64 (believe_me x) pad) pad)

391+

392+public

393+signExtend : Bits n -> Bits (n+m)

394+signExtend {m=m} (MkBits x) = MkBits (zeroUnused (sext' x))

395+

396+-- TODO: Prove

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

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

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

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

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

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

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

409+

410+public

411+truncate : Bits (n+m) -> Bits n

412+truncate (MkBits x) = MkBits (zeroUnused (trunc' x))

413+

414+public

415+bitAt : Fin n -> Bits n

416+bitAt n = intToBits 1 `shiftLeft` intToBits (cast n)

417+

418+public

419+getBit : Fin n -> Bits n -> Bool

420+getBit n x = (x `and` (bitAt n)) /= intToBits 0

421+

422+public

423+setBit : Fin n -> Bits n -> Bits n

424+setBit n x = x `or` (bitAt n)

425+

426+public

427+unsetBit : Fin n -> Bits n -> Bits n

428+unsetBit n x = x `and` complement (bitAt n)

429+

430+bitsToStr : Bits n -> String

431+bitsToStr x = pack (helper last x)

432+ where

433+ %assert_total

434+ helper : Fin (S n) -> Bits n -> List Char

435+ helper fO _ = []

436+ helper (fS x) b = (if getBit x b then '1' else '0') :: helper (weaken x) b

437+

438+instance Show (Bits n) where

439+ show = bitsToStr

lib/Data/Mod2.idrnew file+64

@@ -0,0 +1,64 @@

1+module Data.Mod2

3+import Data.Bits

5+%default total

7+-- Integers modulo 2^n

8+public

9+data Mod2 : Nat -> Type where

10+ MkMod2 : {n : Nat} -> Bits n -> Mod2 n

11+

12+modBin : (Bits n -> Bits n -> Bits n) -> Mod2 n -> Mod2 n -> Mod2 n

13+modBin f (MkMod2 x) (MkMod2 y) = MkMod2 (f x y)

14+

15+modComp : (Bits n -> Bits n -> a) -> Mod2 n -> Mod2 n -> a

16+modComp f (MkMod2 x) (MkMod2 y) = f x y

17+

18+public partial

19+div : Mod2 n -> Mod2 n -> Mod2 n

20+div = modBin udiv

21+

22+public partial

23+rem : Mod2 n -> Mod2 n -> Mod2 n

24+rem = modBin urem

25+

26+%assert_total

27+public

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

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

30+

31+instance Eq (Mod2 n) where

32+ (==) = modComp (==)

33+

34+instance Ord (Mod2 n) where

35+ (<) = modComp (<)

36+ (<=) = modComp (<=)

37+ (>=) = modComp (>=)

38+ (>) = modComp (>)

39+ compare = modComp compare

40+

41+instance Num (Mod2 n) where

42+ (+) = modBin plus

43+ (-) = modBin minus

44+ (*) = modBin times

45+ abs = id

46+ fromInteger = intToMod

47+

48+instance Cast (Mod2 n) (Bits n) where

49+ cast (MkMod2 x) = x

50+

51+instance Cast (Bits n) (Mod2 n) where

52+ cast x = MkMod2 x

53+

54+modToStr : Mod2 n -> String

55+modToStr x = pack (reverse (helper x))

56+ where

57+ %assert_total

58+ helper : Mod2 n -> List Char

59+ helper x = strIndex "0123456789" (bitsToInt (cast (x `rem` 10)))

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

61+

62+

63+instance Show (Mod2 n) where

64+ show = modToStr

lib/Data/Word.idrdeleted−19

@@ -1,19 +0,0 @@

1−module Data.Word

2−

3−%access public

4−

5−instance Num Word8 where

6− (+) = prim__addW8

7− (-) = prim__subW8

8− (*) = prim__mulW8

9−

10− abs x = x

11− fromInteger = prim__intToWord8

12−

13−instance Num Word16 where

14− (+) = prim__addW16

15− (-) = prim__subW16

16− (*) = prim__mulW16

17−

18− abs x = x

19− fromInteger = prim__intToWord16

lib/Prelude/Fin.idr+14

@@ -12,6 +12,20 @@ instance Eq (Fin n) where

12 (==) (fS k) (fS k') = k == k'

13 (==) _ _ = False

15+finToNat : Fin n -> Nat -> Nat

16+finToNat fO a = a

17+finToNat (fS x) a = finToNat x (S a)

18+

19+instance Cast (Fin n) Nat where

20+ cast x = finToNat x O

21+

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

23+finToInt fO a = a

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

25+

26+instance Cast (Fin n) Int where

27+ cast x = finToInt x 0

28+

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

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

16weaken fO = fO

30weaken fO = fO

17weaken (fS k) = fS (weaken k)

31weaken (fS k) = fS (weaken k)

lib/Prelude/Nat.idr+6

@@ -233,6 +233,12 @@ div left (S right) = div' left left right

233 else

234 S (div' left (centre - (S right)) right)

235

236+%assert_total

237+log2 : Nat -> Nat

238+log2 O = O

239+log2 (S O) = O

240+log2 n = S (log2 (n `div` 2))

241+

236--------------------------------------------------------------------------------

242--------------------------------------------------------------------------------

237-- Properties

243-- Properties

238--------------------------------------------------------------------------------

244--------------------------------------------------------------------------------

lib/base.ipkg+1−1

@@ -15,7 +15,7 @@ modules = Builtins, Prelude, IO, System,

16 Language.Reflection,

18− Data.Morphisms, Data.Bits, Data.Word,

18+ Data.Morphisms, Data.Bits, Data.Mod2,

20 Control.Monad.Identity, Control.Monad.State, Control.Category,

21 Control.Arrow

rts/Makefile+2−2

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

1include ../config.mk

3−OBJS = idris_rts.o idris_gc.o idris_gmp.o idris_stdfgn.o

3+OBJS = idris_rts.o idris_gc.o idris_gmp.o idris_stdfgn.o idris_bitstring.o

4−HDRS = idris_rts.h idris_gc.h idris_gmp.h idris_stdfgn.h

4+HDRS = idris_rts.h idris_gc.h idris_gmp.h idris_stdfgn.h idris_bitstring.h

5CFLAGS = -O2 -Wall

6ifneq ($(GMP_INCLUDE_DIR),)

7 CFLAGS += -isystem $(GMP_INCLUDE_DIR)

rts/idris_bitstring.cnew file+666

@@ -0,0 +1,666 @@

1+#include "idris_rts.h"

3+VAL idris_b8CopyForGC(VM *vm, VAL a) {

4+ VAL cl = allocate(vm, sizeof(Closure), 1);

5+ SETTY(cl, BITS8);

6+ cl->info.bits8 = a->info.bits8;

7+ return cl;

8+}

10+VAL idris_b16CopyForGC(VM *vm, VAL a) {

11+ VAL cl = allocate(vm, sizeof(Closure), 1);

12+ SETTY(cl, BITS16);

13+ cl->info.bits16 = a->info.bits16;

14+ return cl;

15+}

16+

17+VAL idris_b32CopyForGC(VM *vm, VAL a) {

18+ VAL cl = allocate(vm, sizeof(Closure), 1);

19+ SETTY(cl, BITS32);

20+ cl->info.bits32 = a->info.bits32;

21+ return cl;

22+}

23+

24+VAL idris_b64CopyForGC(VM *vm, VAL a) {

25+ VAL cl = allocate(vm, sizeof(Closure), 1);

26+ SETTY(cl, BITS64);

27+ cl->info.bits64 = a->info.bits64;

28+ return cl;

29+}

30+

31+VAL idris_b8(VM *vm, VAL a) {

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

33+ SETTY(cl, BITS8);

34+ cl->info.bits8 = (uint8_t) GETINT(a);

35+ return cl;

36+}

37+

38+VAL idris_b16(VM *vm, VAL a) {

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

40+ SETTY(cl, BITS16);

41+ cl->info.bits16 = (uint16_t) GETINT(a);

42+ return cl;

43+}

44+

45+VAL idris_b32(VM *vm, VAL a) {

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

47+ SETTY(cl, BITS32);

48+ cl->info.bits32 = (uint32_t) GETINT(a);

49+ return cl;

50+}

51+

52+VAL idris_b64(VM *vm, VAL a) {

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

54+ SETTY(cl, BITS64);

55+ cl->info.bits64 = (uint64_t) GETINT(a);

56+ return cl;

57+}

58+

59+VAL idris_castB32Int(VM *vm, VAL a) {

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

61+}

62+

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

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

65+ SETTY(cl, BITS8);

66+ cl->info.bits8 = a->info.bits8 + b->info.bits8;

67+ return cl;

68+}

69+

70+VAL idris_b8Minus(VM *vm, VAL a, VAL b) {

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

72+ SETTY(cl, BITS8);

73+ cl->info.bits8 = a->info.bits8 - b->info.bits8;

74+ return cl;

75+}

76+

77+VAL idris_b8Times(VM *vm, VAL a, VAL b) {

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

79+ SETTY(cl, BITS8);

80+ cl->info.bits8 = a->info.bits8 * b->info.bits8;

81+ return cl;

82+}

83+

84+VAL idris_b8UDiv(VM *vm, VAL a, VAL b) {

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

86+ SETTY(cl, BITS8);

87+ cl->info.bits8 = a->info.bits8 / b->info.bits8;

88+ return cl;

89+}

90+

91+VAL idris_b8SDiv(VM *vm, VAL a, VAL b) {

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

93+ SETTY(cl, BITS8);

94+ cl->info.bits8 = (uint8_t) (((int8_t) a->info.bits8) / ((int8_t) b->info.bits8));

95+ return cl;

96+}

97+

98+VAL idris_b8URem(VM *vm, VAL a, VAL b) {

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

100+ SETTY(cl, BITS8);

101+ cl->info.bits8 = a->info.bits8 % b->info.bits8;

102+ return cl;

103+}

104+

105+VAL idris_b8SRem(VM *vm, VAL a, VAL b) {

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

107+ SETTY(cl, BITS8);

108+ cl->info.bits8 = (uint8_t) (((int8_t) a->info.bits8) % ((int8_t) b->info.bits8));

109+ return cl;

110+}

111+

112+VAL idris_b8Lt(VM *vm, VAL a, VAL b) {

113+ return MKINT((i_int) (a->info.bits8 < b->info.bits8));

114+}

115+

116+VAL idris_b8Gt(VM *vm, VAL a, VAL b) {

117+ return MKINT((i_int) (a->info.bits8 > b->info.bits8));

118+}

119+

120+VAL idris_b8Eq(VM *vm, VAL a, VAL b) {

121+ return MKINT((i_int) (a->info.bits8 == b->info.bits8));

122+}

123+

124+VAL idris_b8Lte(VM *vm, VAL a, VAL b) {

125+ return MKINT((i_int) (a->info.bits8 <= b->info.bits8));

126+}

127+

128+VAL idris_b8Gte(VM *vm, VAL a, VAL b) {

129+ return MKINT((i_int) (a->info.bits8 >= b->info.bits8));

130+}

131+

132+VAL idris_b8Compl(VM *vm, VAL a) {

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

134+ SETTY(cl, BITS8);

135+ cl->info.bits8 = ~ a->info.bits8;

136+ return cl;

137+}

138+

139+VAL idris_b8And(VM *vm, VAL a, VAL b) {

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

141+ SETTY(cl, BITS8);

142+ cl->info.bits8 = a->info.bits8 & b->info.bits8;

143+ return cl;

144+}

145+

146+VAL idris_b8Or(VM *vm, VAL a, VAL b) {

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

148+ SETTY(cl, BITS8);

149+ cl->info.bits8 = a->info.bits8 | b->info.bits8;

150+ return cl;

151+}

152+

153+VAL idris_b8Xor(VM *vm, VAL a, VAL b) {

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

155+ SETTY(cl, BITS8);

156+ cl->info.bits8 = a->info.bits8 ^ b->info.bits8;

157+ return cl;

158+}

159+

160+VAL idris_b8Shl(VM *vm, VAL a, VAL b) {

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

162+ SETTY(cl, BITS8);

163+ cl->info.bits8 = a->info.bits8 << b->info.bits8;

164+ return cl;

165+}

166+

167+VAL idris_b8LShr(VM *vm, VAL a, VAL b) {

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

169+ SETTY(cl, BITS8);

170+ cl->info.bits8 = a->info.bits8 >> b->info.bits8;

171+ return cl;

172+}

173+

174+VAL idris_b8AShr(VM *vm, VAL a, VAL b) {

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

176+ SETTY(cl, BITS8);

177+ cl->info.bits8 = (uint8_t) (((int8_t)a->info.bits8) >> ((int8_t)b->info.bits8));

178+ return cl;

179+}

180+

181+VAL idris_b16Plus(VM *vm, VAL a, VAL b) {

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

183+ SETTY(cl, BITS16);

184+ cl->info.bits16 = a->info.bits16 + b->info.bits16;

185+ return cl;

186+}

187+

188+VAL idris_b16Minus(VM *vm, VAL a, VAL b) {

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

190+ SETTY(cl, BITS16);

191+ cl->info.bits16 = a->info.bits16 - b->info.bits16;

192+ return cl;

193+}

194+

195+VAL idris_b16Times(VM *vm, VAL a, VAL b) {

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

197+ SETTY(cl, BITS16);

198+ cl->info.bits16 = a->info.bits16 * b->info.bits16;

199+ return cl;

200+}

201+

202+VAL idris_b16UDiv(VM *vm, VAL a, VAL b) {

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

204+ SETTY(cl, BITS16);

205+ cl->info.bits16 = a->info.bits16 / b->info.bits16;

206+ return cl;

207+}

208+

209+VAL idris_b16SDiv(VM *vm, VAL a, VAL b) {

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

211+ SETTY(cl, BITS16);

212+ cl->info.bits16 =

213+ (uint16_t) (((int16_t) a->info.bits16) / ((int16_t) b->info.bits16));

214+ return cl;

215+}

216+

217+VAL idris_b16URem(VM *vm, VAL a, VAL b) {

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

219+ SETTY(cl, BITS16);

220+ cl->info.bits16 = a->info.bits16 % b->info.bits16;

221+ return cl;

222+}

223+

224+VAL idris_b16SRem(VM *vm, VAL a, VAL b) {

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

226+ SETTY(cl, BITS16);

227+ cl->info.bits16 =

228+ (uint16_t) (((int16_t) a->info.bits16) % ((int16_t) b->info.bits16));

229+ return cl;

230+}

231+

232+VAL idris_b16Lt(VM *vm, VAL a, VAL b) {

233+ return MKINT((i_int) (a->info.bits16 < b->info.bits16));

234+}

235+

236+VAL idris_b16Gt(VM *vm, VAL a, VAL b) {

237+ return MKINT((i_int) (a->info.bits16 > b->info.bits16));

238+}

239+

240+VAL idris_b16Eq(VM *vm, VAL a, VAL b) {

241+ return MKINT((i_int) (a->info.bits16 == b->info.bits16));

242+}

243+

244+VAL idris_b16Lte(VM *vm, VAL a, VAL b) {

245+ return MKINT((i_int) (a->info.bits16 <= b->info.bits16));

246+}

247+

248+VAL idris_b16Gte(VM *vm, VAL a, VAL b) {

249+ return MKINT((i_int) (a->info.bits16 >= b->info.bits16));

250+}

251+

252+VAL idris_b16Compl(VM *vm, VAL a) {

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

254+ SETTY(cl, BITS16);

255+ cl->info.bits16 = ~ a->info.bits16;

256+ return cl;

257+}

258+

259+VAL idris_b16And(VM *vm, VAL a, VAL b) {

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

261+ SETTY(cl, BITS16);

262+ cl->info.bits16 = a->info.bits16 & b->info.bits16;

263+ return cl;

264+}

265+

266+VAL idris_b16Or(VM *vm, VAL a, VAL b) {

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

268+ SETTY(cl, BITS16);

269+ cl->info.bits16 = a->info.bits16 | b->info.bits16;

270+ return cl;

271+}

272+

273+VAL idris_b16Xor(VM *vm, VAL a, VAL b) {

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

275+ SETTY(cl, BITS16);

276+ cl->info.bits16 = a->info.bits16 ^ b->info.bits16;

277+ return cl;

278+}

279+

280+VAL idris_b16Shl(VM *vm, VAL a, VAL b) {

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

282+ SETTY(cl, BITS16);

283+ cl->info.bits16 = a->info.bits16 << b->info.bits16;

284+ return cl;

285+}

286+

287+VAL idris_b16LShr(VM *vm, VAL a, VAL b) {

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

289+ SETTY(cl, BITS16);

290+ cl->info.bits16 = a->info.bits16 >> b->info.bits16;

291+ return cl;

292+}

293+

294+VAL idris_b16AShr(VM *vm, VAL a, VAL b) {

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

296+ SETTY(cl, BITS16);

297+ cl->info.bits16 = (uint16_t) (((int16_t)a->info.bits16) >> ((int16_t)b->info.bits16));

298+ return cl;

299+}

300+

301+VAL idris_b32Plus(VM *vm, VAL a, VAL b) {

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

303+ SETTY(cl, BITS32);

304+ cl->info.bits32 = a->info.bits32 + b->info.bits32;

305+ return cl;

306+}

307+

308+VAL idris_b32Minus(VM *vm, VAL a, VAL b) {

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

310+ SETTY(cl, BITS32);

311+ cl->info.bits32 = a->info.bits32 - b->info.bits32;

312+ return cl;

313+}

314+

315+VAL idris_b32Times(VM *vm, VAL a, VAL b) {

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

317+ SETTY(cl, BITS32);

318+ cl->info.bits32 = a->info.bits32 * b->info.bits32;

319+ return cl;

320+}

321+

322+VAL idris_b32UDiv(VM *vm, VAL a, VAL b) {

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

324+ SETTY(cl, BITS32);

325+ cl->info.bits32 = a->info.bits32 / b->info.bits32;

326+ return cl;

327+}

328+

329+VAL idris_b32SDiv(VM *vm, VAL a, VAL b) {

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

331+ SETTY(cl, BITS32);

332+ cl->info.bits32 =

333+ (uint32_t) (((int32_t) a->info.bits32) / ((int32_t) b->info.bits32));

334+ return cl;

335+}

336+

337+VAL idris_b32URem(VM *vm, VAL a, VAL b) {

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

339+ SETTY(cl, BITS32);

340+ cl->info.bits32 = a->info.bits32 % b->info.bits32;

341+ return cl;

342+}

343+

344+VAL idris_b32SRem(VM *vm, VAL a, VAL b) {

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

346+ SETTY(cl, BITS32);

347+ cl->info.bits32 =

348+ (uint32_t) (((int32_t) a->info.bits32) % ((int32_t) b->info.bits32));

349+ return cl;

350+}

351+

352+VAL idris_b32Lt(VM *vm, VAL a, VAL b) {

353+ return MKINT((i_int) (a->info.bits32 < b->info.bits32));

354+}

355+

356+VAL idris_b32Gt(VM *vm, VAL a, VAL b) {

357+ return MKINT((i_int) (a->info.bits32 > b->info.bits32));

358+}

359+

360+VAL idris_b32Eq(VM *vm, VAL a, VAL b) {

361+ return MKINT((i_int) (a->info.bits32 == b->info.bits32));

362+}

363+

364+VAL idris_b32Lte(VM *vm, VAL a, VAL b) {

365+ return MKINT((i_int) (a->info.bits32 <= b->info.bits32));

366+}

367+

368+VAL idris_b32Gte(VM *vm, VAL a, VAL b) {

369+ return MKINT((i_int) (a->info.bits32 >= b->info.bits32));

370+}

371+

372+VAL idris_b32Compl(VM *vm, VAL a) {

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

374+ SETTY(cl, BITS32);

375+ cl->info.bits32 = ~ a->info.bits32;

376+ return cl;

377+}

378+

379+VAL idris_b32And(VM *vm, VAL a, VAL b) {

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

381+ SETTY(cl, BITS32);

382+ cl->info.bits32 = a->info.bits32 & b->info.bits32;

383+ return cl;

384+}

385+

386+VAL idris_b32Or(VM *vm, VAL a, VAL b) {

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

388+ SETTY(cl, BITS32);

389+ cl->info.bits32 = a->info.bits32 | b->info.bits32;

390+ return cl;

391+}

392+

393+VAL idris_b32Xor(VM *vm, VAL a, VAL b) {

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

395+ SETTY(cl, BITS32);

396+ cl->info.bits32 = a->info.bits32 ^ b->info.bits32;

397+ return cl;

398+}

399+

400+VAL idris_b32Shl(VM *vm, VAL a, VAL b) {

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

402+ SETTY(cl, BITS32);

403+ cl->info.bits32 = a->info.bits32 << b->info.bits32;

404+ return cl;

405+}

406+

407+VAL idris_b32LShr(VM *vm, VAL a, VAL b) {

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

409+ SETTY(cl, BITS32);

410+ cl->info.bits32 = a->info.bits32 >> b->info.bits32;

411+ return cl;

412+}

413+

414+VAL idris_b32AShr(VM *vm, VAL a, VAL b) {

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

416+ SETTY(cl, BITS32);

417+ cl->info.bits32 = (uint32_t) (((int32_t)a->info.bits32) >> ((int32_t)b->info.bits32));

418+ return cl;

419+}

420+

421+VAL idris_b64Plus(VM *vm, VAL a, VAL b) {

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

423+ SETTY(cl, BITS64);

424+ cl->info.bits64 = a->info.bits64 + b->info.bits64;

425+ return cl;

426+}

427+

428+VAL idris_b64Minus(VM *vm, VAL a, VAL b) {

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

430+ SETTY(cl, BITS64);

431+ cl->info.bits64 = a->info.bits64 - b->info.bits64;

432+ return cl;

433+}

434+

435+VAL idris_b64Times(VM *vm, VAL a, VAL b) {

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

437+ SETTY(cl, BITS64);

438+ cl->info.bits64 = a->info.bits64 * b->info.bits64;

439+ return cl;

440+}

441+

442+VAL idris_b64UDiv(VM *vm, VAL a, VAL b) {

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

444+ SETTY(cl, BITS64);

445+ cl->info.bits64 = a->info.bits64 / b->info.bits64;

446+ return cl;

447+}

448+

449+VAL idris_b64SDiv(VM *vm, VAL a, VAL b) {

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

451+ SETTY(cl, BITS64);

452+ cl->info.bits64 =

453+ (uint64_t) (((int64_t) a->info.bits64) / ((int64_t) b->info.bits64));

454+ return cl;

455+}

456+

457+VAL idris_b64URem(VM *vm, VAL a, VAL b) {

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

459+ SETTY(cl, BITS64);

460+ cl->info.bits64 = a->info.bits64 % b->info.bits64;

461+ return cl;

462+}

463+

464+VAL idris_b64SRem(VM *vm, VAL a, VAL b) {

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

466+ SETTY(cl, BITS64);

467+ cl->info.bits64 =

468+ (uint64_t) (((int64_t) a->info.bits64) % ((int64_t) b->info.bits64));

469+ return cl;

470+}

471+

472+VAL idris_b64Lt(VM *vm, VAL a, VAL b) {

473+ return MKINT((i_int) (a->info.bits64 < b->info.bits64));

474+}

475+

476+VAL idris_b64Gt(VM *vm, VAL a, VAL b) {

477+ return MKINT((i_int) (a->info.bits64 > b->info.bits64));

478+}

479+

480+VAL idris_b64Eq(VM *vm, VAL a, VAL b) {

481+ return MKINT((i_int) (a->info.bits64 == b->info.bits64));

482+}

483+

484+VAL idris_b64Lte(VM *vm, VAL a, VAL b) {

485+ return MKINT((i_int) (a->info.bits64 <= b->info.bits64));

486+}

487+

488+VAL idris_b64Gte(VM *vm, VAL a, VAL b) {

489+ return MKINT((i_int) (a->info.bits64 >= b->info.bits64));

490+}

491+

492+VAL idris_b64Compl(VM *vm, VAL a) {

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

494+ SETTY(cl, BITS64);

495+ cl->info.bits64 = ~ a->info.bits64;

496+ return cl;

497+}

498+

499+VAL idris_b64And(VM *vm, VAL a, VAL b) {

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

501+ SETTY(cl, BITS64);

502+ cl->info.bits64 = a->info.bits64 & b->info.bits64;

503+ return cl;

504+}

505+

506+VAL idris_b64Or(VM *vm, VAL a, VAL b) {

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

508+ SETTY(cl, BITS64);

509+ cl->info.bits64 = a->info.bits64 | b->info.bits64;

510+ return cl;

511+}

512+

513+VAL idris_b64Xor(VM *vm, VAL a, VAL b) {

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

515+ SETTY(cl, BITS64);

516+ cl->info.bits64 = a->info.bits64 ^ b->info.bits64;

517+ return cl;

518+}

519+

520+VAL idris_b64Shl(VM *vm, VAL a, VAL b) {

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

522+ SETTY(cl, BITS64);

523+ cl->info.bits64 = a->info.bits64 << b->info.bits64;

524+ return cl;

525+}

526+

527+VAL idris_b64LShr(VM *vm, VAL a, VAL b) {

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

529+ SETTY(cl, BITS64);

530+ cl->info.bits64 = a->info.bits64 >> b->info.bits64;

531+ return cl;

532+}

533+

534+VAL idris_b64AShr(VM *vm, VAL a, VAL b) {

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

536+ SETTY(cl, BITS64);

537+ cl->info.bits64 = (uint64_t) (((int64_t)a->info.bits64) >> ((int64_t)b->info.bits64));

538+ return cl;

539+}

540+

541+VAL idris_b8Z16(VM *vm, VAL a) {

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

543+ SETTY(cl, BITS16);

544+ cl->info.bits16 = (uint16_t) a->info.bits8;

545+ return cl;

546+}

547+

548+VAL idris_b8Z32(VM *vm, VAL a) {

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

550+ SETTY(cl, BITS32);

551+ cl->info.bits32 = (uint32_t) a->info.bits8;

552+ return cl;

553+}

554+

555+VAL idris_b8Z64(VM *vm, VAL a) {

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

557+ SETTY(cl, BITS16);

558+ cl->info.bits64 = (uint64_t) a->info.bits8;

559+ return cl;

560+}

561+

562+VAL idris_b8S16(VM *vm, VAL a) {

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

564+ SETTY(cl, BITS16);

565+ cl->info.bits16 = (uint16_t) (int16_t) (int8_t) a->info.bits8;

566+ return cl;

567+}

568+

569+VAL idris_b8S32(VM *vm, VAL a) {

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

571+ SETTY(cl, BITS32);

572+ cl->info.bits32 = (uint32_t) (int32_t) (int8_t) a->info.bits8;

573+ return cl;

574+}

575+

576+VAL idris_b8S64(VM *vm, VAL a) {

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

578+ SETTY(cl, BITS64);

579+ cl->info.bits64 = (uint64_t) (int64_t) (int8_t) a->info.bits8;

580+ return cl;

581+}

582+

583+VAL idris_b16Z32(VM *vm, VAL a) {

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

585+ SETTY(cl, BITS32);

586+ cl->info.bits32 = (uint32_t) a->info.bits16;

587+ return cl;

588+}

589+

590+VAL idris_b16Z64(VM *vm, VAL a) {

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

592+ SETTY(cl, BITS64);

593+ cl->info.bits64 = (uint64_t) a->info.bits16;

594+ return cl;

595+}

596+

597+VAL idris_b16S32(VM *vm, VAL a) {

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

599+ SETTY(cl, BITS32);

600+ cl->info.bits32 = (uint32_t) (int32_t) (int16_t) a->info.bits16;

601+ return cl;

602+}

603+

604+VAL idris_b16S64(VM *vm, VAL a) {

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

606+ SETTY(cl, BITS64);

607+ cl->info.bits64 = (uint64_t) (int64_t) (int16_t) a->info.bits16;

608+ return cl;

609+}

610+

611+VAL idris_b16T8(VM *vm, VAL a) {

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

613+ SETTY(cl, BITS8);

614+ cl->info.bits8 = (uint8_t) a->info.bits16;

615+ return cl;

616+}

617+

618+VAL idris_b32Z64(VM *vm, VAL a) {

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

620+ SETTY(cl, BITS64);

621+ cl->info.bits64 = (uint64_t) a->info.bits32;

622+ return cl;

623+}

624+

625+VAL idris_b32S64(VM *vm, VAL a) {

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

627+ SETTY(cl, BITS64);

628+ cl->info.bits64 = (uint64_t) (int64_t) (int32_t) a->info.bits32;

629+ return cl;

630+}

631+

632+VAL idris_b32T8(VM *vm, VAL a) {

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

634+ SETTY(cl, BITS8);

635+ cl->info.bits8 = (uint8_t) a->info.bits32;

636+ return cl;

637+}

638+

639+VAL idris_b32T16(VM *vm, VAL a) {

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

641+ SETTY(cl, BITS16);

642+ cl->info.bits16 = (uint16_t) a->info.bits32;

643+ return cl;

644+}

645+

646+VAL idris_b64T8(VM *vm, VAL a) {

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

648+ SETTY(cl, BITS8);

649+ cl->info.bits8 = (uint8_t) a->info.bits64;

650+ return cl;

651+}

652+

653+VAL idris_b64T16(VM *vm, VAL a) {

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

655+ SETTY(cl, BITS16);

656+ cl->info.bits16 = (uint16_t) a->info.bits64;

657+ return cl;

658+}

659+

660+VAL idris_b64T32(VM *vm, VAL a) {

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

662+ SETTY(cl, BITS32);

663+ cl->info.bits32 = (uint32_t) a->info.bits64;

664+ return cl;

665+}

666+

rts/idris_bitstring.hnew file+125

@@ -0,0 +1,125 @@

1+#ifndef _IDRISBITSTRING_H

2+#define _IDRISBITSTRING_H

4+VAL idris_b8CopyForGC(VM *vm, VAL a);

5+VAL idris_b16CopyForGC(VM *vm, VAL a);

6+VAL idris_b32CopyForGC(VM *vm, VAL a);

7+VAL idris_b64CopyForGC(VM *vm, VAL a);

9+VAL idris_b8(VM *vm, VAL a);

10+VAL idris_b16(VM *vm, VAL a);

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

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

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

14+

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

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

17+VAL idris_b8Times(VM *vm, VAL a, VAL b);

18+VAL idris_b8UDiv(VM *vm, VAL a, VAL b);

19+VAL idris_b8SDiv(VM *vm, VAL a, VAL b);

20+VAL idris_b8URem(VM *vm, VAL a, VAL b);

21+VAL idris_b8SRem(VM *vm, VAL a, VAL b);

22+VAL idris_b8Lt(VM *vm, VAL a, VAL b);

23+VAL idris_b8Gt(VM *vm, VAL a, VAL b);

24+VAL idris_b8Eq(VM *vm, VAL a, VAL b);

25+VAL idris_b8Lte(VM *vm, VAL a, VAL b);

26+VAL idris_b8Gte(VM *vm, VAL a, VAL b);

27+VAL idris_b8Compl(VM *vm, VAL a);

28+VAL idris_b8And(VM *vm, VAL a, VAL b);

29+VAL idris_b8Or(VM *vm, VAL a, VAL b);

30+VAL idris_b8Neg(VM *vm, VAL a);

31+VAL idris_b8XOr(VM *vm, VAL a, VAL b);

32+VAL idris_b8Shl(VM *vm, VAL a, VAL b);

33+VAL idris_b8LShr(VM *vm, VAL a, VAL b);

34+VAL idris_b8AShr(VM *vm, VAL a, VAL b);

35+

36+VAL idris_b16Eq(VM *vm, VAL a, VAL b);

37+VAL idris_b32Eq(VM *vm, VAL a, VAL b);

38+VAL idris_b64Eq(VM *vm, VAL a, VAL b);

39+

40+VAL idris_b8Z16(VM *vm, VAL a);

41+VAL idris_b8Z32(VM *vm, VAL a);

42+VAL idris_b8Z64(VM *vm, VAL a);

43+VAL idris_b8S16(VM *vm, VAL a);

44+VAL idris_b8S32(VM *vm, VAL a);

45+VAL idris_b8S64(VM *vm, VAL a);

46+

47+VAL idris_b16Plus(VM *vm, VAL a, VAL b);

48+VAL idris_b16Minus(VM *vm, VAL a, VAL b);

49+VAL idris_b16Times(VM *vm, VAL a, VAL b);

50+VAL idris_b16UDiv(VM *vm, VAL a, VAL b);

51+VAL idris_b16SDiv(VM *vm, VAL a, VAL b);

52+VAL idris_b16URem(VM *vm, VAL a, VAL b);

53+VAL idris_b16SRem(VM *vm, VAL a, VAL b);

54+VAL idris_b16Lt(VM *vm, VAL a, VAL b);

55+VAL idris_b16Gt(VM *vm, VAL a, VAL b);

56+VAL idris_b16Eq(VM *vm, VAL a, VAL b);

57+VAL idris_b16Lte(VM *vm, VAL a, VAL b);

58+VAL idris_b16Gte(VM *vm, VAL a, VAL b);

59+VAL idris_b16Compl(VM *vm, VAL a);

60+VAL idris_b16And(VM *vm, VAL a, VAL b);

61+VAL idris_b16Or(VM *vm, VAL a, VAL b);

62+VAL idris_b16Neg(VM *vm, VAL a);

63+VAL idris_b16XOr(VM *vm, VAL a, VAL b);

64+VAL idris_b16Shl(VM *vm, VAL a, VAL b);

65+VAL idris_b16LShr(VM *vm, VAL a, VAL b);

66+VAL idris_b16AShr(VM *vm, VAL a, VAL b);

67+

68+VAL idris_b16Z32(VM *vm, VAL a);

69+VAL idris_b16Z64(VM *vm, VAL a);

70+VAL idris_b16S32(VM *vm, VAL a);

71+VAL idris_b16S64(VM *vm, VAL a);

72+VAL idris_b16T8(VM *vm, VAL a);

73+

74+VAL idris_b32Plus(VM *vm, VAL a, VAL b);

75+VAL idris_b32Minus(VM *vm, VAL a, VAL b);

76+VAL idris_b32Times(VM *vm, VAL a, VAL b);

77+VAL idris_b32UDiv(VM *vm, VAL a, VAL b);

78+VAL idris_b32SDiv(VM *vm, VAL a, VAL b);

79+VAL idris_b32URem(VM *vm, VAL a, VAL b);

80+VAL idris_b32SRem(VM *vm, VAL a, VAL b);

81+VAL idris_b32Lt(VM *vm, VAL a, VAL b);

82+VAL idris_b32Gt(VM *vm, VAL a, VAL b);

83+VAL idris_b32Eq(VM *vm, VAL a, VAL b);

84+VAL idris_b32Lte(VM *vm, VAL a, VAL b);

85+VAL idris_b32Gte(VM *vm, VAL a, VAL b);

86+VAL idris_b32Compl(VM *vm, VAL a);

87+VAL idris_b32And(VM *vm, VAL a, VAL b);

88+VAL idris_b32Or(VM *vm, VAL a, VAL b);

89+VAL idris_b32Neg(VM *vm, VAL a);

90+VAL idris_b32XOr(VM *vm, VAL a, VAL b);

91+VAL idris_b32Shl(VM *vm, VAL a, VAL b);

92+VAL idris_b32LShr(VM *vm, VAL a, VAL b);

93+VAL idris_b32AShr(VM *vm, VAL a, VAL b);

94+

95+VAL idris_b32Z64(VM *vm, VAL a);

96+VAL idris_b32S64(VM *vm, VAL a);

97+VAL idris_b32T8(VM *vm, VAL a);

98+VAL idris_b32T16(VM *vm, VAL a);

99+

100+VAL idris_b64Plus(VM *vm, VAL a, VAL b);

101+VAL idris_b64Minus(VM *vm, VAL a, VAL b);

102+VAL idris_b64Times(VM *vm, VAL a, VAL b);

103+VAL idris_b64UDiv(VM *vm, VAL a, VAL b);

104+VAL idris_b64SDiv(VM *vm, VAL a, VAL b);

105+VAL idris_b64URem(VM *vm, VAL a, VAL b);

106+VAL idris_b64SRem(VM *vm, VAL a, VAL b);

107+VAL idris_b64Lt(VM *vm, VAL a, VAL b);

108+VAL idris_b64Gt(VM *vm, VAL a, VAL b);

109+VAL idris_b64Eq(VM *vm, VAL a, VAL b);

110+VAL idris_b64Lte(VM *vm, VAL a, VAL b);

111+VAL idris_b64Gte(VM *vm, VAL a, VAL b);

112+VAL idris_b64Compl(VM *vm, VAL a);

113+VAL idris_b64And(VM *vm, VAL a, VAL b);

114+VAL idris_b64Or(VM *vm, VAL a, VAL b);

115+VAL idris_b64Neg(VM *vm, VAL a);

116+VAL idris_b64XOr(VM *vm, VAL a, VAL b);

117+VAL idris_b64Shl(VM *vm, VAL a, VAL b);

118+VAL idris_b64LShr(VM *vm, VAL a, VAL b);

119+VAL idris_b64AShr(VM *vm, VAL a, VAL b);

120+

121+VAL idris_b64T8(VM *vm, VAL a);

122+VAL idris_b64T16(VM *vm, VAL a);

123+VAL idris_b64T32(VM *vm, VAL a);

124+

125+#endif

rts/idris_gc.c+13

@@ -1,5 +1,6 @@

1#include "idris_rts.h"

2#include "idris_gc.h"

3+#include "idris_bitstring.h"

3#include <assert.h>

4#include <assert.h>

5VAL copy(VM* vm, VAL x) {

6VAL copy(VM* vm, VAL x) {

@@ -29,6 +30,18 @@ VAL copy(VM* vm, VAL x) {

29 case PTR:

30 case PTR:

30 cl = MKPTRc(vm, x->info.ptr);

31 cl = MKPTRc(vm, x->info.ptr);

31 break;

32 break;

33+ case BITS8:

34+ cl = idris_b8CopyForGC(vm, x);

35+ break;

36+ case BITS16:

37+ cl = idris_b16CopyForGC(vm, x);

38+ break;

39+ case BITS32:

40+ cl = idris_b32CopyForGC(vm, x);

41+ break;

42+ case BITS64:

43+ cl = idris_b64CopyForGC(vm, x);

44+ break;

32 case FWD:

45 case FWD:

33 return x->info.ptr;

46 return x->info.ptr;

34 default:

47 default:

rts/idris_rts.c+13

@@ -8,6 +8,7 @@

9#include "idris_rts.h"

10#include "idris_gc.h"

11+#include "idris_bitstring.h"

12VM* init_vm(int stack_size, size_t heap_size,

13VM* init_vm(int stack_size, size_t heap_size,

13 int max_threads, // not implemented yet

14 int max_threads, // not implemented yet

@@ -444,6 +445,18 @@ VAL copyTo(VM* vm, VAL x) {

444 case PTR:

445 case PTR:

445 cl = MKPTRc(vm, x->info.ptr);

446 cl = MKPTRc(vm, x->info.ptr);

446 break;

447 break;

448+ case BITS8:

449+ cl = idris_b8CopyForGC(vm, x);

450+ break;

451+ case BITS16:

452+ cl = idris_b16CopyForGC(vm, x);

453+ break;

454+ case BITS32:

455+ cl = idris_b32CopyForGC(vm, x);

456+ break;

457+ case BITS64:

458+ cl = idris_b64CopyForGC(vm, x);

459+ break;

447 default:

460 default:

448 assert(0); // We're in trouble if this happens...

461 assert(0); // We're in trouble if this happens...

449 }

462 }

rts/idris_rts.h+6−1

@@ -7,11 +7,12 @@

7#include <unistd.h>

8#include <stdarg.h>

9#include <pthread.h>

10+#include <stdint.h>

11// Closures

12// Closures

13typedef enum {

14typedef enum {

14− CON, INT, BIGINT, FLOAT, STRING, UNIT, PTR, FWD

15+ CON, INT, BIGINT, FLOAT, STRING, BITS8, BITS16, BITS32, BITS64, UNIT, PTR, FWD

15} ClosureType;

16} ClosureType;

17typedef struct Closure *VAL;

18typedef struct Closure *VAL;

@@ -31,6 +32,10 @@ typedef struct Closure {

31 double f;

32 double f;

32 char* str;

33 char* str;

33 void* ptr;

34 void* ptr;

35+ uint8_t bits8;

36+ uint16_t bits16;

37+ uint32_t bits32;

38+ uint64_t bits64;

34 } info;

39 } info;

35} Closure;

40} Closure;

src/Core/CaseTree.hs+5−3

@@ -226,9 +226,11 @@ toPat tc tms = evalState (mapM (\x -> toPat' x []) tms) []

226 toPat' (Constant ChType) [] | tc = return $ PCon (UN "Char") 3 []

227 toPat' (Constant StrType) [] | tc = return $ PCon (UN "String") 4 []

228 toPat' (Constant PtrType) [] | tc = return $ PCon (UN "Ptr") 5 []

229− toPat' (Constant BIType) [] | tc = return $ PCon (UN "Integer") 6 []

229+ toPat' (Constant BIType) [] | tc = return $ PCon (UN "Integer") 6 []

230− toPat' (Constant W8Type) [] | tc = return $ PCon (UN "Word8") 7 []

230+ toPat' (Constant B8Type) [] | tc = return $ PCon (UN "Bits8") 7 []

231− toPat' (Constant W16Type) [] | tc = return $ PCon (UN "Word16") 8 []

231+ toPat' (Constant B16Type) [] | tc = return $ PCon (UN "Bits16") 8 []

232+ toPat' (Constant B32Type) [] | tc = return $ PCon (UN "Bits32") 9 []

233+ toPat' (Constant B64Type) [] | tc = return $ PCon (UN "Bits64") 10 []

232

234

233 toPat' (P Bound n _) [] = do ns <- get

235 toPat' (P Bound n _) [] = do ns <- get

234 if n `elem` ns

236 if n `elem` ns

src/Core/CoreParser.hs+1−1

@@ -36,7 +36,7 @@ idrisDef = haskellDef {

36 "using", "namespace", "class", "instance",

37 "public", "private", "abstract",

38 "Int", "Integer", "Float", "Char", "String", "Ptr",

39− "Word8", "Word16"]

39+ "Bits8", "Bits16", "Bits32", "Bits64"]

40 }

42iOpStart = oneOf ":!#$%&*+./<=>?@\\^|-~"

src/Core/Evaluate.hs+5−2

@@ -507,8 +507,11 @@ eval_hnf ctxt statics genv tm = ev [] tm where

507 findConst ChType (ConCase n 3 [] v : xs) = Just v

508 findConst StrType (ConCase n 4 [] v : xs) = Just v

509 findConst PtrType (ConCase n 5 [] v : xs) = Just v

510− findConst W8Type (ConCase n 6 [] v : xs) = Just v

510+ findConst BIType (ConCase n 6 [] v : xs) = Just v

511− findConst W16Type (ConCase n 7 [] v : xs) = Just v

511+ findConst B8Type (ConCase n 7 [] v : xs) = Just v

512+ findConst B16Type (ConCase n 8 [] v : xs) = Just v

513+ findConst B32Type (ConCase n 9 [] v : xs) = Just v

514+ findConst B64Type (ConCase n 10 [] v : xs) = Just v

512 findConst c (_ : xs) = findConst c xs

515 findConst c (_ : xs) = findConst c xs

513

516

514 getValArgs (HApp t env args) = (t, env, args)

517 getValArgs (HApp t env args) = (t, env, args)

src/Core/TT.hs+14−8

@@ -260,8 +260,8 @@ addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)

260data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

262

263− | W8 Word8 | W16 Word16

263+ | B8 Word8 | B16 Word16 | B32 Word32 | B64 Word64

264− | W8Type | W16Type

264+ | B8Type | B16Type | B32Type | B64Type

265

266 | PtrType | VoidType | Forgot

267 deriving (Eq, Ord)

@@ -286,8 +286,10 @@ instance Pretty Const where

286 pretty PtrType = text "Ptr"

287 pretty VoidType = text "Void"

288 pretty Forgot = text "Forgot"

289− pretty W8Type = text "Word8"

289+ pretty B8Type = text "Bits8"

290+ pretty B16Type = text "Bits16"

291+ pretty B32Type = text "Bits32"

290− pretty W16Type = text "Word16"

292+ pretty B64Type = text "Bits64"

291

293

292data Raw = Var Name

294data Raw = Var Name

293 | RBind Name (Binder Raw) Raw

295 | RBind Name (Binder Raw) Raw

@@ -689,16 +691,20 @@ instance Show Const where

689 show (Fl f) = show f

691 show (Fl f) = show f

690 show (Ch c) = show c

692 show (Ch c) = show c

691 show (Str s) = show s

693 show (Str s) = show s

694+ show (B8 x) = show x

695+ show (B16 x) = show x

692− show (W8 x) = show x

696+ show (B32 x) = show x

693− show (W16 x) = show x

697+ show (B64 x) = show x

694 show IType = "Int"

698 show IType = "Int"

695 show BIType = "Integer"

699 show BIType = "Integer"

696 show FlType = "Float"

700 show FlType = "Float"

697 show ChType = "Char"

701 show ChType = "Char"

698 show StrType = "String"

702 show StrType = "String"

699 show PtrType = "Ptr"

703 show PtrType = "Ptr"

700− show W8Type = "Word8"

704+ show B8Type = "Bits8"

701− show W16Type = "Word16"

705+ show B16Type = "Bits16"

706+ show B32Type = "Bits32"

707+ show B64Type = "Bits64"

702 show VoidType = "Void"

708 show VoidType = "Void"

703

709

704showEnv env t = showEnv' env t False

710showEnv env t = showEnv' env t False

src/Core/Typecheck.hs+4−2

@@ -103,8 +103,10 @@ check' holes ctxt env top = chk env top where

103 constType (Fl _) = Constant FlType

104 constType (Ch _) = Constant ChType

105 constType (Str _) = Constant StrType

106− constType (W8 _) = Constant W8Type

106+ constType (B8 _) = Constant B8Type

107+ constType (B16 _) = Constant B16Type

108+ constType (B32 _) = Constant B32Type

107− constType (W16 _) = Constant W16Type

109+ constType (B64 _) = Constant B64Type

108 constType Forgot = Erased

110 constType Forgot = Erased

109 constType _ = TType (UVal 0)

111 constType _ = TType (UVal 0)

110 chk env (RForce t) = do (_, ty) <- chk env t

112 chk env (RForce t) = do (_, ty) <- chk env t

src/IRTS/CodegenC.hs+140−2

@@ -62,7 +62,7 @@ codegenC defs out exec incs objs libs dbg

62headers xs =

63 concatMap

64 (\h -> "#include <" ++ h ++ ">\n")

65− (xs ++ ["idris_rts.h", "idris_stdfgn.h", "gmp.h", "assert.h"])

65+ (xs ++ ["idris_rts.h", "idris_bitstring.h", "idris_stdfgn.h", "gmp.h", "assert.h"])

67debug TRACE = "#define IDRIS_TRACE\n\n"

68debug _ = ""

@@ -297,6 +297,144 @@ doOp v LReadStr [x] = v ++ "idris_readStr(vm, GETPTR(" ++ creg x ++ "))"

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

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

299

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

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

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

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

304+

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

306+

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

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

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

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

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

312+

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

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

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

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

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

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

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

320+

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

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

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

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

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

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

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

328+

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

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

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

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

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

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

335+

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

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

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

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

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

341+

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

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

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

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

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

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

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

349+

350+doOp v LB16Plus [x, y] =

351+ v ++ "idris_b16Plus(vm, " ++ creg x ++ "," ++ creg y ++ ")"

352+doOp v LB16Minus [x, y] =

353+ v ++ "idris_b16Minus(vm, " ++ creg x ++ "," ++ creg y ++ ")"

354+doOp v LB16Times [x, y] =

355+ v ++ "idris_b16Times(vm, " ++ creg x ++ "," ++ creg y ++ ")"

356+doOp v LB16UDiv [x, y] =

357+ v ++ "idris_b16UDiv(vm, " ++ creg x ++ "," ++ creg y ++ ")"

358+doOp v LB16SDiv [x, y] =

359+ v ++ "idris_b16SDiv(vm, " ++ creg x ++ "," ++ creg y ++ ")"

360+doOp v LB16URem [x, y] =

361+ v ++ "idris_b16URem(vm, " ++ creg x ++ "," ++ creg y ++ ")"

362+doOp v LB16SRem [x, y] =

363+ v ++ "idris_b16SRem(vm, " ++ creg x ++ "," ++ creg y ++ ")"

364+

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

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

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

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

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

370+

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

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

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

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

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

376+

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

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

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

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

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

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

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

384+

385+doOp v LB32Plus [x, y] =

386+ v ++ "idris_b32Plus(vm, " ++ creg x ++ "," ++ creg y ++ ")"

387+doOp v LB32Minus [x, y] =

388+ v ++ "idris_b32Minus(vm, " ++ creg x ++ "," ++ creg y ++ ")"

389+doOp v LB32Times [x, y] =

390+ v ++ "idris_b32Times(vm, " ++ creg x ++ "," ++ creg y ++ ")"

391+doOp v LB32UDiv [x, y] =

392+ v ++ "idris_b32UDiv(vm, " ++ creg x ++ "," ++ creg y ++ ")"

393+doOp v LB32SDiv [x, y] =

394+ v ++ "idris_b32SDiv(vm, " ++ creg x ++ "," ++ creg y ++ ")"

395+doOp v LB32URem [x, y] =

396+ v ++ "idris_b32URem(vm, " ++ creg x ++ "," ++ creg y ++ ")"

397+doOp v LB32SRem [x, y] =

398+ v ++ "idris_b32SRem(vm, " ++ creg x ++ "," ++ creg y ++ ")"

399+

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

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

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

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

404+

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

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

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

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

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

410+

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

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

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

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

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

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

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

418+

419+doOp v LB64Plus [x, y] =

420+ v ++ "idris_b64Plus(vm, " ++ creg x ++ "," ++ creg y ++ ")"

421+doOp v LB64Minus [x, y] =

422+ v ++ "idris_b64Minus(vm, " ++ creg x ++ "," ++ creg y ++ ")"

423+doOp v LB64Times [x, y] =

424+ v ++ "idris_b64Times(vm, " ++ creg x ++ "," ++ creg y ++ ")"

425+doOp v LB64UDiv [x, y] =

426+ v ++ "idris_b64UDiv(vm, " ++ creg x ++ "," ++ creg y ++ ")"

427+doOp v LB64SDiv [x, y] =

428+ v ++ "idris_b64SDiv(vm, " ++ creg x ++ "," ++ creg y ++ ")"

429+doOp v LB64URem [x, y] =

430+ v ++ "idris_b64URem(vm, " ++ creg x ++ "," ++ creg y ++ ")"

431+doOp v LB64SRem [x, y] =

432+ v ++ "idris_b64SRem(vm, " ++ creg x ++ "," ++ creg y ++ ")"

433+

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

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

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

437+

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

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

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

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

302doOp v LFSin [x] = v ++ "MKFLOAT(sin(GETFLOAT(" ++ creg x ++ ")))"

440doOp v LFSin [x] = v ++ "MKFLOAT(sin(GETFLOAT(" ++ creg x ++ ")))"

@@ -325,4 +463,4 @@ doOp v LVMPtr [] = v ++ "MKPTR(vm, vm)"

325doOp v LChInt args = v ++ creg (last args)

463doOp v LChInt args = v ++ creg (last args)

326doOp v LIntCh args = v ++ creg (last args)

464doOp v LIntCh args = v ++ creg (last args)

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

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

328−doOp _ _ _ = "FAIL"

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

src/IRTS/Compiler.hs+4−2

@@ -341,8 +341,10 @@ instance ToIR SC where

341 matchableTy ChType = True

342 matchableTy StrType = True

343

344− matchableTy W8Type = True

344+ matchableTy B8Type = True

345− matchableTy W16Type = True

345+ matchableTy B16Type = True

346+ matchableTy B32Type = True

347+ matchableTy B64Type = True

346

348

347 matchableTy _ = False

349 matchableTy _ = False

348

350

src/IRTS/Lang.hs+17−4

@@ -40,10 +40,23 @@ data PrimFn = LPlus | LMinus | LTimes | LDiv | LMod

41 | LPrintNum | LPrintStr | LReadStr

43− | LW8 | LW16

44−

45− | LW8Plus | LW8Minus | LW8Times

46− | LW16Plus | LW16Minus | LW16Times

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

49 | LFSqrt | LFFloor | LFCeil

62 | LFSqrt | LFFloor | LFCeil

src/Idris/IBC.hs+33−20

@@ -353,16 +353,22 @@ instance Binary Const where

353 put x1

354 Str x1 -> do putWord8 4

355 put x1

356− IType -> putWord8 5

356+ B8 x1 -> putWord8 5 >> put x1

357− BIType -> putWord8 6

357+ B16 x1 -> putWord8 6 >> put x1

358− FlType -> putWord8 7

358+ B32 x1 -> putWord8 7 >> put x1

359− ChType -> putWord8 8

359+ B64 x1 -> putWord8 8 >> put x1

360+

360− StrType -> putWord8 9

361+ IType -> putWord8 9

361− PtrType -> putWord8 10

362+ BIType -> putWord8 10

362− Forgot -> putWord8 11

363+ FlType -> putWord8 11

363−

364− W8Type -> putWord8 12

364+ ChType -> putWord8 12

365− W16Type -> putWord8 13

365+ StrType -> putWord8 13

366+ PtrType -> putWord8 14

367+ Forgot -> putWord8 15

368+ B8Type -> putWord8 16

369+ B16Type -> putWord8 17

370+ B32Type -> putWord8 18

371+ B64Type -> putWord8 19

366 get

372 get

367 = do i <- getWord8

373 = do i <- getWord8

368 case i of

374 case i of

@@ -376,16 +382,23 @@ instance Binary Const where

376 return (Ch x1)

382 return (Ch x1)

377 4 -> do x1 <- get

383 4 -> do x1 <- get

378 return (Str x1)

384 return (Str x1)

379− 5 -> return IType

385+ 5 -> fmap B8 get

380− 6 -> return BIType

386+ 6 -> fmap B16 get

381− 7 -> return FlType

387+ 7 -> fmap B32 get

382− 8 -> return ChType

388+ 8 -> fmap B64 get

389+

383− 9 -> return StrType

390+ 9 -> return IType

384− 10 -> return PtrType

391+ 10 -> return BIType

385− 11 -> return Forgot

392+ 11 -> return FlType

386−

387− 12 -> return W8Type

393+ 12 -> return ChType

388− 13 -> return W16Type

394+ 13 -> return StrType

395+ 14 -> return PtrType

396+ 15 -> return Forgot

397+

398+ 16 -> return B8Type

399+ 17 -> return B16Type

400+ 18 -> return B32Type

401+ 19 -> return B64Type

389

402

390 _ -> error "Corrupted binary data for Const"

403 _ -> error "Corrupted binary data for Const"

391

404

src/Idris/Parser.hs+4−2

@@ -1085,8 +1085,10 @@ pConstant = do reserved "Integer";return BIType

1085 <|> do reserved "Float"; return FlType

1086 <|> do reserved "String"; return StrType

1087 <|> do reserved "Ptr"; return PtrType

1088− <|> do reserved "Word8"; return W8Type

1088+ <|> do reserved "Bits8"; return B8Type

1089+ <|> do reserved "Bits16"; return B16Type

1090+ <|> do reserved "Bits32"; return B32Type

1089− <|> do reserved "Word16"; return W16Type

1091+ <|> do reserved "Bits64"; return B64Type

1090 <|> try (do f <- float; return $ Fl f)

1092 <|> try (do f <- float; return $ Fl f)

1091-- <|> try (do i <- natural; lchar 'L'; return $ BI i)

1093-- <|> try (do i <- natural; lchar 'L'; return $ BI i)

1092 <|> try (do i <- natural; return $ I (fromInteger i))

1094 <|> try (do i <- natural; return $ I (fromInteger i))

src/Idris/Primitives.hs+339−28

@@ -11,6 +11,8 @@ import IRTS.Lang

11import Core.TT

12import Core.Evaluate

13import Data.Bits

14+import Data.Word

15+import Data.Int

15data Prim = Prim { p_name :: Name,

17data Prim = Prim { p_name :: Name,

16 p_type :: Type,

18 p_type :: Type,

@@ -75,24 +77,216 @@ primitives =

75 Prim (UN "prim__gteChar") (ty [ChType, ChType] IType) 2 (bcBin (>=))

77 Prim (UN "prim__gteChar") (ty [ChType, ChType] IType) 2 (bcBin (>=))

76 (2, LGe) total,

78 (2, LGe) total,

78− Prim (UN "prim__addW8") (ty [W8Type, W8Type] W8Type) 2 (w8Bin (+))

80+ Prim (UN "prim__ltB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (<))

81+ (2, LB8Lt) total,

82+ Prim (UN "prim__lteB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (<=))

79− (2, LW8Plus) total,

83+ (2, LB8Lte) total,

80− Prim (UN "prim__subW8") (ty [W8Type, W8Type] W8Type) 2 (w8Bin (-))

84+ Prim (UN "prim__eqB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (==))

81− (2, LW8Minus) total,

85+ (2, LB8Eq) total,

82− Prim (UN "prim__mulW8") (ty [W8Type, W8Type] W8Type) 2 (w8Bin (*))

86+ Prim (UN "prim__gteB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (>))

83− (2, LW8Times) total,

87+ (2, LB8Gte) total,

84−

88+ Prim (UN "prim__gtB8") (ty [B8Type, B8Type] IType) 2 (b8Cmp (>=))

85− Prim (UN "prim__addW16") (ty [W16Type, W16Type] W16Type) 2 (w16Bin (+))

89+ (2, LB8Gt) total,

90+ Prim (UN "prim__addB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (+))

86− (2, LW16Plus) total,

91+ (2, LB8Plus) total,

87− Prim (UN "prim__subW16") (ty [W16Type, W16Type] W16Type) 2 (w16Bin (-))

92+ Prim (UN "prim__subB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (-))

88− (2, LW16Minus) total,

93+ (2, LB8Minus) total,

89− Prim (UN "prim__mulW16") (ty [W16Type, W16Type] W16Type) 2 (w16Bin (*))

94+ Prim (UN "prim__mulB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (*))

90− (2, LW16Times) total,

95+ (2, LB8Times) total,

91−

96+ Prim (UN "prim__udivB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin div)

92− Prim (UN "prim__intToWord8") (ty [IType] W8Type) 1 intToWord8

97+ (2, LB8UDiv) partial,

93− (1, LW8) total,

98+ Prim (UN "prim__sdivB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin s8div)

94− Prim (UN "prim__intToWord16") (ty [IType] W16Type) 1 intToWord16

99+ (2, LB8SDiv) partial,

100+ Prim (UN "prim__uremB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin rem)

101+ (2, LB8URem) partial,

102+ Prim (UN "prim__sremB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin s8rem)

103+ (2, LB8SRem) partial,

104+ Prim (UN "prim__shlB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (\x y -> shiftL x (fromIntegral y)))

105+ (2, LB8Shl) total,

106+ Prim (UN "prim__lshrB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (\x y -> shiftR x (fromIntegral y)))

107+ (2, LB8AShr) total,

108+ Prim (UN "prim__ashrB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (\x y -> fromIntegral $

109+ shiftR (fromIntegral x :: Int8)

110+ (fromIntegral y)))

111+ (2, LB8LShr) total,

112+ Prim (UN "prim__andB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (.&.))

113+ (2, LB8And) total,

114+ Prim (UN "prim__orB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin (.|.))

115+ (2, LB8Or) total,

116+ Prim (UN "prim__xorB8") (ty [B8Type, B8Type] B8Type) 2 (b8Bin xor)

117+ (2, LB8Xor) total,

118+ Prim (UN "prim__complB8") (ty [B8Type] B8Type) 1 (b8Un complement)

119+ (1, LB8Compl) total,

120+ Prim (UN "prim__zextB8_16") (ty [B8Type] B16Type) 1 zext8_16

121+ (1, LB8Z16) total,

122+ Prim (UN "prim__zextB8_32") (ty [B8Type] B32Type) 1 zext8_32

123+ (1, LB8Z32) total,

124+ Prim (UN "prim__zextB8_64") (ty [B8Type] B64Type) 1 zext8_64

125+ (1, LB8Z64) total,

126+ Prim (UN "prim__sextB8_16") (ty [B8Type] B16Type) 1 sext8_16

127+ (1, LB8Z16) total,

128+ Prim (UN "prim__sextB8_32") (ty [B8Type] B32Type) 1 sext8_32

129+ (1, LB8Z32) total,

130+ Prim (UN "prim__sextB8_64") (ty [B8Type] B64Type) 1 sext8_64

131+ (1, LB8Z64) total,

132+

133+ Prim (UN "prim__ltB16") (ty [B16Type, B16Type] IType) 2 (b16Cmp (<))

134+ (2, LB16Lt) total,

135+ Prim (UN "prim__lteB16") (ty [B16Type, B16Type] IType) 2 (b16Cmp (<=))

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

95− (1, LW16) total,

289+ (1, LB32Int) total,

290

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

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

98 (2, LBPlus) total,

292 (2, LBPlus) total,

@@ -245,19 +439,136 @@ bsBin _ _ = Nothing

245sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))

439sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))

246sBin _ _ = Nothing

440sBin _ _ = Nothing

247

441

248−w8Bin op [VConstant (W8 x), VConstant (W8 y)] = Just $ VConstant (W8 (op x y))

442+s8div :: Word8 -> Word8 -> Word8

249−w8Bin _ _ = Nothing

443+s8div x y = fromIntegral (fromIntegral x `div` fromIntegral y :: Int8)

250

444

251−w16Bin op [VConstant (W16 x), VConstant (W16 y)] = Just $ VConstant (W16 (op x y))

445+s16div :: Word16 -> Word16 -> Word16

252−w16Bin _ _ = Nothing

446+s16div x y = fromIntegral (fromIntegral x `div` fromIntegral y :: Int16)

253

447

254−-- w32Bin op [VConstant (W32 x), VConstant (W32 y)] = Just $ VConstant (W32 (op x y))

448+s32div :: Word32 -> Word32 -> Word32

255−-- w32Bin _ _ = Nothing

449+s32div x y = fromIntegral (fromIntegral x `div` fromIntegral y :: Int32)

256

450

257−intToWord8 [VConstant (I x)] = Just $ VConstant (W8 $ fromIntegral x)

451+s64div :: Word64 -> Word64 -> Word64

452+s64div x y = fromIntegral (fromIntegral x `div` fromIntegral y :: Int64)

453+

454+s8rem :: Word8 -> Word8 -> Word8

455+s8rem x y = fromIntegral (fromIntegral x `rem` fromIntegral y :: Int8)

456+

457+s16rem :: Word16 -> Word16 -> Word16

458+s16rem x y = fromIntegral (fromIntegral x `rem` fromIntegral y :: Int16)

459+

460+s32rem :: Word32 -> Word32 -> Word32

461+s32rem x y = fromIntegral (fromIntegral x `rem` fromIntegral y :: Int32)

462+

463+s64rem :: Word64 -> Word64 -> Word64

464+s64rem x y = fromIntegral (fromIntegral x `rem` fromIntegral y :: Int64)

465+

466+b8Bin op [VConstant (B8 x), VConstant (B8 y)] = Just $ VConstant (B8 (op x y))

467+b8Bin _ _ = Nothing

468+

469+b8Un op [VConstant (B8 x)] = Just $ VConstant (B8 (op x))

470+b8Un _ _ = Nothing

471+

472+b16Bin op [VConstant (B16 x), VConstant (B16 y)] = Just $ VConstant (B16 (op x y))

473+b16Bin _ _ = Nothing

474+

475+b16Un op [VConstant (B16 x)] = Just $ VConstant (B16 (op x))

476+b16Un _ _ = Nothing

477+

478+b32Bin op [VConstant (B32 x), VConstant (B32 y)] = Just $ VConstant (B32 (op x y))

479+b32Bin _ _ = Nothing

480+

481+b32Un op [VConstant (B32 x)] = Just $ VConstant (B32 (op x))

482+b32Un _ _ = Nothing

483+

484+b64Bin op [VConstant (B64 x), VConstant (B64 y)] = Just $ VConstant (B64 (op x y))

485+b64Bin _ _ = Nothing

486+

487+b64Un op [VConstant (B64 x)] = Just $ VConstant (B64 (op x))

488+b64Un _ _ = Nothing

489+

490+b8Cmp op [VConstant (B8 x), VConstant (B8 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))

491+b8Cmp _ _ = Nothing

492+

493+b16Cmp op [VConstant (B16 x), VConstant (B16 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))

494+b16Cmp _ _ = Nothing

495+

496+b32Cmp op [VConstant (B32 x), VConstant (B32 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))

497+b32Cmp _ _ = Nothing

498+

499+b64Cmp op [VConstant (B64 x), VConstant (B64 y)] = Just $ VConstant (I (if (op x y) then 1 else 0))

500+b64Cmp _ _ = Nothing

501+

502+toB8 x = VConstant (B8 (fromIntegral x))

503+toB16 x = VConstant (B16 (fromIntegral x))

504+toB32 x = VConstant (B32 (fromIntegral x))

505+toB64 x = VConstant (B64 (fromIntegral x))

506+

507+zext8_16 [VConstant (B8 x)] = Just $ toB16 x

508+zext8_16 _ = Nothing

509+

510+zext8_32 [VConstant (B8 x)] = Just $ toB32 x

511+zext8_32 _ = Nothing

512+

513+zext8_64 [VConstant (B8 x)] = Just $ toB64 x

514+zext8_64 _ = Nothing

515+

516+sext8_16 [VConstant (B8 x)] = Just $ toB16 (fromIntegral x :: Int8)

517+sext8_16 _ = Nothing

518+

519+sext8_32 [VConstant (B8 x)] = Just $ toB32 (fromIntegral x :: Int8)

520+sext8_32 _ = Nothing

521+

522+sext8_64 [VConstant (B8 x)] = Just $ toB64 (fromIntegral x :: Int8)

523+sext8_64 _ = Nothing

524+

525+zext16_32 [VConstant (B16 x)] = Just $ toB32 x

526+zext16_32 _ = Nothing

527+

528+zext16_64 [VConstant (B16 x)] = Just $ toB64 x

529+zext16_64 _ = Nothing

530+

531+sext16_32 [VConstant (B16 x)] = Just $ toB32 (fromIntegral x :: Int16)

532+sext16_32 _ = Nothing

533+

534+sext16_64 [VConstant (B16 x)] = Just $ toB64 (fromIntegral x :: Int16)

535+sext16_64 _ = Nothing

536+

537+trunc16_8 [VConstant (B16 x)] = Just $ toB8 x

538+trunc16_8 _ = Nothing

539+

540+zext32_64 [VConstant (B32 x)] = Just $ toB64 x

541+zext32_64 _ = Nothing

542+

543+sext32_64 [VConstant (B32 x)] = Just $ toB64 (fromIntegral x :: Int32)

544+sext32_64 _ = Nothing

545+

546+trunc32_8 [VConstant (B32 x)] = Just $ toB8 x

547+trunc32_8 _ = Nothing

548+

549+trunc32_16 [VConstant (B32 x)] = Just $ toB16 x

550+trunc32_16 _ = Nothing

551+

552+trunc64_8 [VConstant (B64 x)] = Just $ toB8 x

553+trunc64_8 _ = Nothing

554+

555+trunc64_16 [VConstant (B64 x)] = Just $ toB16 x

556+trunc64_16 _ = Nothing

557+

558+trunc64_32 [VConstant (B64 x)] = Just $ toB32 x

559+trunc64_32 _ = Nothing

560+

561+intToBits8 [VConstant (I x)] = Just $ toB8 x

562+intToBits8 _ = Nothing

563+intToBits16 [VConstant (I x)] = Just $ toB16 x

564+intToBits16 _ = Nothing

565+intToBits32 [VConstant (I x)] = Just $ toB32 x

258−intToWord8 _ = Nothing

566+intToBits32 _ = Nothing

567+intToBits64 [VConstant (I x)] = Just $ toB64 x

568+intToBits64 _ = Nothing

569+

259−intToWord16 [VConstant (I x)] = Just $ VConstant (W16 $ fromIntegral x)

570+bits32ToInt [VConstant (B32 x)] = Just $ VConstant (I (fromIntegral x))

260−intToWord16 _ = Nothing

571+bits32ToInt _ = Nothing

261

572

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

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

263c_intToStr _ = Nothing

574c_intToStr _ = Nothing

test/test007/test007.idr+1−1

@@ -36,6 +36,6 @@ runEval env e with (eval e) {

37main : IO ()

38main = do print [| (\x => x *2) (Just 4) |]

39− print [| plus (Just 4) (Just 5) |]

39+ print [| plus (Just 4) (Just 5) |]

40 print (runEval [("x",21), ("y", 20)] (Add (Val 1) (Add (Var "x") (Var "y"))))

41 print (runEval [("x",21)] (Add (Val 1) (Add (Var "x") (Var "y"))))