73ea02b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Remove Buffer and BitVector from parser

73ea02bEdwin Brady12 years ago

idris.cabal−4

compare with master

unifiedsplit

@@ -346,10 +346,6 @@ Extra-source-files:

346 test/basic013/*.idr

347 test/basic013/expected

348

349− test/buffer001-disabled/*.idr

350− test/buffer001-disabled/run

351− test/buffer001-disabled/expected

352−

353 test/delab001/*.idr

349 test/delab001/*.idr

354 test/delab001/run

350 test/delab001/run

355 test/delab001/expected

351 test/delab001/expected

libs/base/Language/Reflection/Utils.idr−10

@@ -93,15 +93,10 @@ instance Show Const where

93 show (B16 b) = "(B16 ...)"

94 show (B32 b) = "(B32 ...)"

95 show (B64 b) = "(B64 ...)"

96− show (B8V xs) = "(B8V ...)"

97− show (B16V xs) = "(B16V ...)"

98− show (B32V xs) = "(B32V ...)"

99− show (B64V xs) = "(B64V ...)"

100 show (AType x) = "(AType ...)"

96 show (AType x) = "(AType ...)"

101 show StrType = "StrType"

97 show StrType = "StrType"

102 show PtrType = "PtrType"

98 show PtrType = "PtrType"

103 show ManagedPtrType = "ManagedPtrType"

99 show ManagedPtrType = "ManagedPtrType"

104− show BufferType = "BufferType"

105 show VoidType = "VoidType"

100 show VoidType = "VoidType"

106 show Forgot = "Forgot"

101 show Forgot = "Forgot"

107

102

@@ -135,15 +130,10 @@ instance Eq Const where

135 (B16 x) == (B16 y) = x == y

130 (B16 x) == (B16 y) = x == y

136 (B32 x) == (B32 y) = x == y

131 (B32 x) == (B32 y) = x == y

137 (B64 x) == (B64 y) = x == y

132 (B64 x) == (B64 y) = x == y

138− (B8V xs) == (B8V ys) = False -- TODO

139− (B16V xs) == (B16V ys) = False -- TODO

140− (B32V xs) == (B32V ys) = False -- TODO

141− (B64V xs) == (B64V ys) = False -- TODO

142 (AType x) == (AType y) = x == y

133 (AType x) == (AType y) = x == y

143 StrType == StrType = True

134 StrType == StrType = True

144 PtrType == PtrType = True

135 PtrType == PtrType = True

145 ManagedPtrType == ManagedPtrType = True

136 ManagedPtrType == ManagedPtrType = True

146− BufferType == BufferType = True

147 VoidType == VoidType = True

137 VoidType == VoidType = True

148 Forgot == Forgot = True

138 Forgot == Forgot = True

149 _ == _ = False

139 _ == _ = False

libs/contrib/Data/Buffer.idrdeleted−254

@@ -1,254 +0,0 @@

1−module Data.Buffer

2−

3−import Data.Fin

4−

5−%default total

6−

7−-- !!! TODO: Open issues:

8−-- 1. It may be theoretically nice to represent Buffer size as

9−-- Fin (2 ^ WORD_BITS) instead of Nat

10−-- 2. Primitives take Bits64 when really they should take the

11−-- equivalent of C's size_t (ideally unboxed)

12−-- 3. If we had access to host system information, we could reduce

13−-- the needed primitives by implementing the LE/BE variants on

14−-- top of the native variant plus a possible swab function

15−-- 4. Would be nice to be able to peek/append Int, Char, and Float,

16−-- all have fixed (though possibly implementation-dependent) widths.

17−-- Currently not in place due to lack of host system introspection.

18−-- 5. Would be nice to be able to peek/append the vector types, but

19−-- for now I'm only touching the C backend which AFAICT doesn't

20−-- support them.

21−-- 6. Conversion from Fin to Bits64 (which, re 2, should eventually

22−-- be a fixed-width implementation-dependent type) is likely

23−-- inefficient relative to conversion from Nat to Bits64

24−-- 7. We may want to have a separate type that is a product of Buffer

25−-- and offset rather than storing the offset in Buffer itself, which

26−-- would require exposing the offset argument of prim__appendBuffer

27−

28−||| A contiguous chunk of n bytes

29−abstract

30−record Buffer : Nat -> Type where

31− MkBuffer : ( offset : Nat ) -> ( realBuffer : prim__UnsafeBuffer ) -> Buffer n

32−

33−bitsFromNat : Nat -> Bits64

34−bitsFromNat Z = 0

35−bitsFromNat (S k) = 1 + bitsFromNat k

36−

37−bitsFromFin : Fin n -> Bits64

38−bitsFromFin FZ = 0

39−bitsFromFin (FS k) = 1 + bitsFromFin k

40−

41−||| Allocate an empty Buffer. The size hint can be used to avoid

42−||| unnecessary reallocations and copies under the hood if the

43−||| approximate ultimate size of the Buffer is known. Users can assume

44−||| the new Buffer is word-aligned.

45−public

46−allocate : ( hint : Nat ) -> Buffer Z

47−allocate = MkBuffer Z . prim__allocate . bitsFromNat

48−

49−||| Append count repetitions of a Buffer to another Buffer

50−%assert_total

51−public

52−appendBuffer : Buffer n ->

53− ( count : Nat ) ->

54− Buffer m ->

55− Buffer ( n + count * m )

56−appendBuffer { n } { m } ( MkBuffer o1 r1 ) c ( MkBuffer o2 r2 ) =

57− MkBuffer o1 $ prim__appendBuffer r1 size1 count size2 off r2

58− where

59− size1 : Bits64

60− size1 = bitsFromNat ( n + o1 )

61− size2 : Bits64

62− size2 = bitsFromNat m

63− count : Bits64

64− count = bitsFromNat c

65− off : Bits64

66− off = bitsFromNat o2

67−

68−||| Copy a buffer, potentially allowing the (potentially large) space it

69−||| pointed to to be freed

70−public

71−copy : Buffer n -> Buffer n

72−copy { n } = replace ( plusZeroRightNeutral n ) . appendBuffer ( allocate n ) 1

73−

74−||| Create a view over a buffer

75−public

76−peekBuffer : { n : Nat } -> { offset : Nat } -> Buffer ( n + offset ) -> ( offset : Nat ) -> Buffer n

77−peekBuffer ( MkBuffer o r ) off = MkBuffer ( o + off ) r

78−

79−peekBits : ( prim__UnsafeBuffer -> Bits64 -> a ) ->

80− Buffer ( m + n ) ->

81− ( offset : Fin ( S n ) ) ->

82− a

83−peekBits prim ( MkBuffer o r ) = prim r . bitsFromNat . plus o . finToNat

84−

85−appendBits : ( prim__UnsafeBuffer ->

86− Bits64 ->

87− Bits64 ->

88− a ->

89− prim__UnsafeBuffer ) ->

90− Buffer n ->

91− ( count : Nat) ->

92− a ->

93− Buffer ( n + count * size )

94−appendBits { n } prim ( MkBuffer o r ) count =

95− MkBuffer o . prim r ( bitsFromNat $ n + o ) ( bitsFromNat count )

96−

97−

98−||| Read a Bits8 from a Buffer starting at offset

99−%assert_total

100−public

101−peekBits8 : Buffer ( 1 + n ) ->

102− ( offset : Fin ( S n ) ) ->

103− Bits8

104−peekBits8 = peekBits { m = 1 } prim__peekB8Native

105−

106−||| Append count repetitions of a Bits8 to a Buffer

107−%assert_total

108−public

109−appendBits8 : Buffer n ->

110− ( count : Nat ) ->

111− Bits8 ->

112− Buffer ( n + count * 1 )

113−appendBits8 = appendBits prim__appendB8Native

114−

115−||| Read a Bits16 in native byte order from a Buffer starting at offset

116−%assert_total

117−public

118−peekBits16Native : Buffer ( 2 + n ) ->

119− ( offset : Fin ( S n ) ) ->

120− Bits16

121−peekBits16Native = peekBits { m = 2 } prim__peekB16Native

122−

123−||| Read a little-endian Bits16 from a Buffer starting at offset

124−%assert_total

125−public

126−peekBits16LE : Buffer ( 2 + n ) -> ( offset : Fin ( S n ) ) -> Bits16

127−peekBits16LE = peekBits { m = 2 } prim__peekB16LE

128−

129−||| Read a big-endian Bits16 from a Buffer starting at offset

130−%assert_total

131−public

132−peekBits16BE : Buffer ( 2 + n ) -> ( offset : Fin ( S n ) ) -> Bits16

133−peekBits16BE = peekBits { m = 2 } prim__peekB16BE

134−

135−||| Append count repetitions of a Bits16 in native byte order to a Buffer

136−%assert_total

137−public

138−appendBits16Native : Buffer n ->

139− ( count : Nat ) ->

140− Bits16 ->

141− Buffer ( n + count * 2 )

142−appendBits16Native = appendBits prim__appendB16Native

143−

144−||| Append count repetitions of a little-endian Bits16 to a Buffer

145−%assert_total

146−public

147−appendBits16LE : Buffer n ->

148− ( count : Nat ) ->

149− Bits16 ->

150− Buffer ( n + count * 2 )

151−appendBits16LE = appendBits prim__appendB16LE

152−

153−||| Append count repetitions of a big-endian Bits16 to a Buffer

154−%assert_total

155−public

156−appendBits16BE : Buffer n ->

157− ( count : Nat ) ->

158− Bits16 ->

159− Buffer ( n + count * 2 )

160−appendBits16BE = appendBits prim__appendB16BE

161−

162−||| Read a Bits32 in native byte order from a Buffer starting at offset

163−%assert_total

164−public

165−peekBits32Native : Buffer ( 4 + n ) ->

166− ( offset : Fin ( S n ) ) ->

167− Bits32

168−peekBits32Native = peekBits { m = 4 } prim__peekB32Native

169−

170−||| Read a little-endian Bits32 from a Buffer starting at offset

171−%assert_total

172−public

173−peekBits32LE : Buffer ( 4 + n ) -> ( offset : Fin ( S n ) ) -> Bits32

174−peekBits32LE = peekBits { m = 4 } prim__peekB32LE

175−

176−||| Read a big-endian Bits32 from a Buffer starting at offset

177−%assert_total

178−public

179−peekBits32BE : Buffer ( 4 + n ) -> ( offset : Fin ( S n ) ) -> Bits32

180−peekBits32BE = peekBits { m = 4 } prim__peekB32BE

181−

182−||| Append count repetitions of a Bits32 in native byte order to a Buffer

183−%assert_total

184−public

185−appendBits32Native : Buffer n ->

186− ( count : Nat ) ->

187− Bits32 ->

188− Buffer ( n + count * 4 )

189−appendBits32Native = appendBits prim__appendB32Native

190−

191−||| Append count repetitions of a little-endian Bits32 to a Buffer

192−%assert_total

193−public

194−appendBits32LE : Buffer n ->

195− ( count : Nat ) ->

196− Bits32 ->

197− Buffer ( n + count * 4 )

198−appendBits32LE = appendBits prim__appendB32LE

199−

200−||| Append count repetitions of a big-endian Bits32 to a Buffer

201−%assert_total

202−public

203−appendBits32BE : Buffer n ->

204− ( count : Nat ) ->

205− Bits32 ->

206− Buffer ( n + count * 4 )

207−appendBits32BE = appendBits prim__appendB32BE

208−

209−||| Read a Bits64 in native byte order from a Buffer starting at offset

210−%assert_total

211−public

212−peekBits64Native : Buffer ( 8 + n ) ->

213− ( offset : Fin ( S n ) ) ->

214− Bits64

215−peekBits64Native = peekBits { m = 8 } prim__peekB64Native

216−

217−||| Read a little-endian Bits64 from a Buffer starting at offset

218−%assert_total

219−public

220−peekBits64LE : Buffer ( 8 + n ) -> ( offset : Fin ( S n ) ) -> Bits64

221−peekBits64LE = peekBits { m = 8 } prim__peekB64LE

222−

223−||| Read a big-endian Bits64 from a Buffer starting at offset

224−%assert_total

225−public

226−peekBits64BE : Buffer ( 8 + n ) -> ( offset : Fin ( S n ) ) -> Bits64

227−peekBits64BE = peekBits { m = 8 } prim__peekB64BE

228−

229−||| Append count repetitions of a Bits64 in native byte order to a Buffer

230−%assert_total

231−public

232−appendBits64Native : Buffer n ->

233− ( count : Nat ) ->

234− Bits64 ->

235− Buffer ( n + count * 8 )

236−appendBits64Native = appendBits prim__appendB64Native

237−

238−||| Append count repetitions of a little-endian Bits64 to a Buffer

239−%assert_total

240−public

241−appendBits64LE : Buffer n ->

242− ( count : Nat ) ->

243− Bits64 ->

244− Buffer ( n + count * 8 )

245−appendBits64LE = appendBits prim__appendB64LE

246−

247−||| Append count repetitions of a big-endian Bits64 to a Buffer

248−%assert_total

249−public

250−appendBits64BE : Buffer n ->

251− ( count : Nat ) ->

252− Bits64 ->

253− Buffer ( n + count * 8 )

254−appendBits64BE = appendBits prim__appendB64BE

libs/contrib/contrib.ipkg+1−1

@@ -4,7 +4,7 @@ opts = "--nobasepkgs --total -i ../prelude -i ../base"

4modules = Control.Algebra,

5 Control.Isomorphism.Primitives,

6 Classes.Verified,

7− Data.Fun, Data.Rel, Data.Buffer,

7+ Data.Fun, Data.Rel,

8 Data.Hash, Data.Matrix,

9 Data.ZZ, Data.Sign,

10 Data.BoundedList,

libs/prelude/IO.idr−4

@@ -135,10 +135,6 @@ data C_IntTypes : Type -> Type where

135 C_IntBits16 : C_IntTypes Bits16

136 C_IntBits32 : C_IntTypes Bits32

137 C_IntBits64 : C_IntTypes Bits64

138− C_IntB8x16 : C_IntTypes Bits8x16

139− C_IntB16x8 : C_IntTypes Bits16x8

140− C_IntB32x4 : C_IntTypes Bits32x4

141− C_IntB64x2 : C_IntTypes Bits64x2

142

138

143-- Supported C foreign types

139-- Supported C foreign types

144data C_Types : Type -> Type where

140data C_Types : Type -> Type where

libs/prelude/Language/Reflection.idr+1−45

@@ -45,10 +45,8 @@ data ArithTy = ATInt Language.Reflection.IntTy | ATFloat

45||| Primitive constants

46data Const = I Int | BI Integer | Fl Float | Ch Char | Str String

47 | B8 Bits8 | B16 Bits16 | B32 Bits32 | B64 Bits64

48− | B8V Bits8x16 | B16V Bits16x8

49− | B32V Bits32x4 | B64V Bits64x2

50 | AType ArithTy | StrType

48 | AType ArithTy | StrType

49+ | PtrType | ManagedPtrType | VoidType | Forgot

52 | WorldType | TheWorld

50 | WorldType | TheWorld

53%name Const c, c'

51%name Const c, c'

@@ -361,38 +359,6 @@ instance Quotable Integer Raw where

361 quotedTy = `(Integer)

359 quotedTy = `(Integer)

362 quote x = RConstant (BI x)

360 quote x = RConstant (BI x)

363

361

364−instance Quotable Bits8x16 TT where

365− quotedTy = `(Bits8x16)

366− quote x = TConst (B8V x)

367−

368−instance Quotable Bits8x16 Raw where

369− quotedTy = `(Bits8x16)

370− quote x = RConstant (B8V x)

371−

372−instance Quotable Bits16x8 TT where

373− quotedTy = `(Bits16x8)

374− quote x = TConst (B16V x)

375−

376−instance Quotable Bits16x8 Raw where

377− quotedTy = `(Bits16x8)

378− quote x = RConstant (B16V x)

379−

380−instance Quotable Bits32x4 TT where

381− quotedTy = `(Bits32x4)

382− quote x = TConst (B32V x)

383−

384−instance Quotable Bits32x4 Raw where

385− quotedTy = `(Bits32x4)

386− quote x = RConstant (B32V x)

387−

388−instance Quotable Bits64x2 TT where

389− quotedTy = `(Bits64x2)

390− quote x = TConst (B64V x)

391−

392−instance Quotable Bits64x2 Raw where

393− quotedTy = `(Bits64x2)

394− quote x = RConstant (B64V x)

395−

396instance Quotable String TT where

362instance Quotable String TT where

397 quotedTy = `(String)

363 quotedTy = `(String)

398 quote x = TConst (Str x)

364 quote x = TConst (Str x)

@@ -490,15 +456,10 @@ instance Quotable Const TT where

490 quote (B16 x) = `(B16 ~(quote x))

456 quote (B16 x) = `(B16 ~(quote x))

491 quote (B32 x) = `(B32 ~(quote x))

457 quote (B32 x) = `(B32 ~(quote x))

492 quote (B64 x) = `(B64 ~(quote x))

458 quote (B64 x) = `(B64 ~(quote x))

493− quote (B8V xs) = `(B8V ~(quote xs))

494− quote (B16V xs) = `(B16V ~(quote xs))

495− quote (B32V xs) = `(B32V ~(quote xs))

496− quote (B64V xs) = `(B64V ~(quote xs))

497 quote (AType x) = `(AType ~(quote x))

459 quote (AType x) = `(AType ~(quote x))

498 quote StrType = `(StrType)

460 quote StrType = `(StrType)

499 quote PtrType = `(PtrType)

461 quote PtrType = `(PtrType)

500 quote ManagedPtrType = `(ManagedPtrType)

462 quote ManagedPtrType = `(ManagedPtrType)

501− quote BufferType = `(BufferType)

502 quote VoidType = `(VoidType)

463 quote VoidType = `(VoidType)

503 quote Forgot = `(Forgot)

464 quote Forgot = `(Forgot)

504 quote WorldType = `(WorldType)

465 quote WorldType = `(WorldType)

@@ -515,15 +476,10 @@ instance Quotable Const Raw where

515 quote (B16 x) = `(B16 ~(quote {t=Raw} x))

476 quote (B16 x) = `(B16 ~(quote {t=Raw} x))

516 quote (B32 x) = `(B32 ~(quote {t=Raw} x))

477 quote (B32 x) = `(B32 ~(quote {t=Raw} x))

517 quote (B64 x) = `(B64 ~(quote {t=Raw} x))

478 quote (B64 x) = `(B64 ~(quote {t=Raw} x))

518− quote (B8V xs) = `(B8V ~(quote {t=Raw} xs))

519− quote (B16V xs) = `(B16V ~(quote {t=Raw} xs))

520− quote (B32V xs) = `(B32V ~(quote {t=Raw} xs))

521− quote (B64V xs) = `(B64V ~(quote {t=Raw} xs))

522 quote (AType x) = `(AType ~(quote {t=Raw} x))

479 quote (AType x) = `(AType ~(quote {t=Raw} x))

523 quote StrType = `(StrType)

480 quote StrType = `(StrType)

524 quote PtrType = `(PtrType)

481 quote PtrType = `(PtrType)

525 quote ManagedPtrType = `(ManagedPtrType)

482 quote ManagedPtrType = `(ManagedPtrType)

526− quote BufferType = `(BufferType)

527 quote VoidType = `(VoidType)

483 quote VoidType = `(VoidType)

528 quote Forgot = `(Forgot)

484 quote Forgot = `(Forgot)

529 quote WorldType = `(WorldType)

485 quote WorldType = `(WorldType)

libs/prelude/Prelude.idr−112

@@ -115,106 +115,6 @@ instance Show Bits32 where

115instance Show Bits64 where

116 show b = b64ToString b

117

118−%assert_total

119−viewB8x16 : Bits8x16 -> (Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8, Bits8)

120−viewB8x16 x = ( prim__indexB8x16 x (prim__truncBigInt_B32 0)

121− , prim__indexB8x16 x (prim__truncBigInt_B32 1)

122− , prim__indexB8x16 x (prim__truncBigInt_B32 2)

123− , prim__indexB8x16 x (prim__truncBigInt_B32 3)

124− , prim__indexB8x16 x (prim__truncBigInt_B32 4)

125− , prim__indexB8x16 x (prim__truncBigInt_B32 5)

126− , prim__indexB8x16 x (prim__truncBigInt_B32 6)

127− , prim__indexB8x16 x (prim__truncBigInt_B32 7)

128− , prim__indexB8x16 x (prim__truncBigInt_B32 8)

129− , prim__indexB8x16 x (prim__truncBigInt_B32 9)

130− , prim__indexB8x16 x (prim__truncBigInt_B32 10)

131− , prim__indexB8x16 x (prim__truncBigInt_B32 11)

132− , prim__indexB8x16 x (prim__truncBigInt_B32 12)

133− , prim__indexB8x16 x (prim__truncBigInt_B32 13)

134− , prim__indexB8x16 x (prim__truncBigInt_B32 14)

135− , prim__indexB8x16 x (prim__truncBigInt_B32 15)

136− )

137−

138−instance Show Bits8x16 where

139− show x =

140− case viewB8x16 x of

141− (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) =>

142− "<" ++ prim__toStrB8 a

143− ++ ", " ++ prim__toStrB8 b

144− ++ ", " ++ prim__toStrB8 c

145− ++ ", " ++ prim__toStrB8 d

146− ++ ", " ++ prim__toStrB8 e

147− ++ ", " ++ prim__toStrB8 f

148− ++ ", " ++ prim__toStrB8 g

149− ++ ", " ++ prim__toStrB8 h

150− ++ ", " ++ prim__toStrB8 i

151− ++ ", " ++ prim__toStrB8 j

152− ++ ", " ++ prim__toStrB8 k

153− ++ ", " ++ prim__toStrB8 l

154− ++ ", " ++ prim__toStrB8 m

155− ++ ", " ++ prim__toStrB8 n

156− ++ ", " ++ prim__toStrB8 o

157− ++ ", " ++ prim__toStrB8 p

158− ++ ">"

159−

160−%assert_total

161−viewB16x8 : Bits16x8 -> (Bits16, Bits16, Bits16, Bits16, Bits16, Bits16, Bits16, Bits16)

162−viewB16x8 x = ( prim__indexB16x8 x (prim__truncBigInt_B32 0)

163− , prim__indexB16x8 x (prim__truncBigInt_B32 1)

164− , prim__indexB16x8 x (prim__truncBigInt_B32 2)

165− , prim__indexB16x8 x (prim__truncBigInt_B32 3)

166− , prim__indexB16x8 x (prim__truncBigInt_B32 4)

167− , prim__indexB16x8 x (prim__truncBigInt_B32 5)

168− , prim__indexB16x8 x (prim__truncBigInt_B32 6)

169− , prim__indexB16x8 x (prim__truncBigInt_B32 7)

170− )

171−

172−instance Show Bits16x8 where

173− show x =

174− case viewB16x8 x of

175− (a, b, c, d, e, f, g, h) =>

176− "<" ++ prim__toStrB16 a

177− ++ ", " ++ prim__toStrB16 b

178− ++ ", " ++ prim__toStrB16 c

179− ++ ", " ++ prim__toStrB16 d

180− ++ ", " ++ prim__toStrB16 e

181− ++ ", " ++ prim__toStrB16 f

182− ++ ", " ++ prim__toStrB16 g

183− ++ ", " ++ prim__toStrB16 h

184− ++ ">"

185−

186−%assert_total

187−viewB32x4 : Bits32x4 -> (Bits32, Bits32, Bits32, Bits32)

188−viewB32x4 x = ( prim__indexB32x4 x (prim__truncBigInt_B32 0)

189− , prim__indexB32x4 x (prim__truncBigInt_B32 1)

190− , prim__indexB32x4 x (prim__truncBigInt_B32 2)

191− , prim__indexB32x4 x (prim__truncBigInt_B32 3)

192− )

193−

194−instance Show Bits32x4 where

195− show x =

196− case viewB32x4 x of

197− (a, b, c, d) =>

198− "<" ++ prim__toStrB32 a

199− ++ ", " ++ prim__toStrB32 b

200− ++ ", " ++ prim__toStrB32 c

201− ++ ", " ++ prim__toStrB32 d

202− ++ ">"

203−

204−%assert_total

205−viewB64x2 : Bits64x2 -> (Bits64, Bits64)

206−viewB64x2 x = ( prim__indexB64x2 x (prim__truncBigInt_B32 0)

207− , prim__indexB64x2 x (prim__truncBigInt_B32 1)

208− )

209−

210−instance Show Bits64x2 where

211− show x =

212− case viewB64x2 x of

213− (a, b) =>

214− "<" ++ prim__toStrB64 a

215− ++ ", " ++ prim__toStrB64 b

216− ++ ">"

217−

218instance (Show a, Show b) => Show (a, b) where

118instance (Show a, Show b) => Show (a, b) where

219 show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"

119 show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"

220

120

@@ -419,18 +319,6 @@ curry f a b = f (a, b)

419uncurry : (a -> b -> c) -> (a, b) -> c

319uncurry : (a -> b -> c) -> (a, b) -> c

420uncurry f (a, b) = f a b

320uncurry f (a, b) = f a b

421

321

422−uniformB8x16 : Bits8 -> Bits8x16

423−uniformB8x16 x = prim__mkB8x16 x x x x x x x x x x x x x x x x

424−

425−uniformB16x8 : Bits16 -> Bits16x8

426−uniformB16x8 x = prim__mkB16x8 x x x x x x x x

427−

428−uniformB32x4 : Bits32 -> Bits32x4

429−uniformB32x4 x = prim__mkB32x4 x x x x

430−

431−uniformB64x2 : Bits64 -> Bits64x2

432−uniformB64x2 x = prim__mkB64x2 x x

433−

434---- some basic io

322---- some basic io

435

323

436||| Output a string to stdout without a trailing newline

324||| Output a string to stdout without a trailing newline

src/Idris/ParseExpr.hs+5−5

@@ -1162,15 +1162,15 @@ constants =

1162 , ("ManagedPtr", ManagedPtrType)

1163 , ("prim__WorldType", WorldType)

1164 , ("prim__TheWorld", TheWorld)

1165− , ("prim__UnsafeBuffer", BufferType)

1165+-- , ("prim__UnsafeBuffer", BufferType)

1166 , ("Bits8", AType (ATInt (ITFixed IT8)))

1167 , ("Bits16", AType (ATInt (ITFixed IT16)))

1168 , ("Bits32", AType (ATInt (ITFixed IT32)))

1169 , ("Bits64", AType (ATInt (ITFixed IT64)))

1170− , ("Bits8x16", AType (ATInt (ITVec IT8 16)))

1170+-- , ("Bits8x16", AType (ATInt (ITVec IT8 16)))

1171− , ("Bits16x8", AType (ATInt (ITVec IT16 8)))

1171+-- , ("Bits16x8", AType (ATInt (ITVec IT16 8)))

1172− , ("Bits32x4", AType (ATInt (ITVec IT32 4)))

1172+-- , ("Bits32x4", AType (ATInt (ITVec IT32 4)))

1173− , ("Bits64x2", AType (ATInt (ITVec IT64 2)))

1173+-- , ("Bits64x2", AType (ATInt (ITVec IT64 2)))

1174 ]

1175

1176constant :: IdrisParser Idris.Core.TT.Const

test/primitives004/expected → test/primitives004-disabled/expectedrenamed

The content is the same.

test/primitives004/primitives004.idr → test/primitives004-disabled/primitives004.idrrenamed

The content is the same.

test/primitives004/run → test/primitives004-disabled/runrenamed

The content is the same.