d6418d7 · Idris-dev · git.iko.soy

libs/base/Data/Buffer.idr+11−37

compare with master

unifiedsplit

@@ -55,32 +55,20 @@ copy { n } = MkBuffer . prim__copy ( bitsFromNat n ) . realBuffer

55-- (i.e. create a view of a subset of the Buffer)

56%assert_total

57public

58−peekBufferNative : Buffer ( m + n ) ->

58+peekBuffer : Buffer ( m + n ) ->

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

59+ ( offset : Fin ( S n ) ) ->

60− Buffer m

60+ Buffer m

61−peekBufferNative ( MkBuffer real ) =

61+peekBuffer ( MkBuffer real ) =

62− MkBuffer . prim__peekBufferNative real . bitsFromFin

62+ MkBuffer . prim__peekBuffer real . bitsFromFin

63−

64−public

65−peekBufferLE : Buffer ( m + n ) ->

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

67− Buffer m

68−peekBufferLE = peekBufferNative

69−

70−public

71−peekBufferBE : Buffer ( m + n ) ->

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

73− Buffer m

74−peekBufferBE = peekBufferNative

75

63

76-- Append count repetitions of a Buffer to another Buffer

64-- Append count repetitions of a Buffer to another Buffer

77%assert_total

65%assert_total

78public

66public

79−appendBufferNative : Buffer n ->

67+appendBuffer : Buffer n ->

80− ( count : Nat ) ->

68+ ( count : Nat ) ->

81− Buffer m ->

69+ Buffer m ->

82− Buffer ( n + m * count )

70+ Buffer ( n + m * count )

83−appendBufferNative { n } { m } ( MkBuffer input ) count =

71+appendBuffer { n } { m } ( MkBuffer input ) count =

84 MkBuffer . app . realBuffer

72 MkBuffer . app . realBuffer

85 where

73 where

86 nBits : Bits64

74 nBits : Bits64

@@ -89,21 +77,7 @@ appendBufferNative { n } { m } ( MkBuffer input ) count =

89 mBits = bitsFromNat m

77 mBits = bitsFromNat m

90 cBits : Bits64

78 cBits : Bits64

91 cBits = bitsFromNat count

79 cBits = bitsFromNat count

92− app = prim__appendBufferNative input nBits cBits mBits

80+ app = prim__appendBuffer input nBits cBits mBits

93−

94−public

95−appendBufferLE : Buffer n ->

96− ( count : Nat ) ->

97− Buffer m ->

98− Buffer ( n + m * count )

99−appendBufferLE = appendBufferNative

100−

101−public

102−appendBufferBE : Buffer n ->

103− ( count : Nat ) ->

104− Buffer m ->

105− Buffer ( n + m * count )

106−appendBufferBE = appendBufferNative

107

81

108

82

109peekBits : ( prim__UnsafeBuffer -> Bits64 -> a ) ->

83peekBits : ( prim__UnsafeBuffer -> Bits64 -> a ) ->

src/IRTS/CodegenC.hs+2−2

@@ -459,8 +459,8 @@ doOp v LStrRev [x] = v ++ "idris_strRev(vm, " ++ creg x ++ ")"

459

460doOp v LAllocate [x] = v ++ "idris_allocate(vm, " ++ creg x ++ ")"

461doOp v LCopy [x, y] = v ++ "idris_copy(vm, " ++ creg x ++ "," ++ creg y ++ ")"

462−doOp v LAppendBufferNative [a, b, c, d, e] = v ++ "idris_appendBuffer(vm, " ++ creg a ++ "," ++ creg b ++ "," ++ creg c ++ "," ++ creg d ++ "," ++ creg e ++ ")"

462+doOp v LAppendBuffer [a, b, c, d, e] = v ++ "idris_appendBuffer(vm, " ++ creg a ++ "," ++ creg b ++ "," ++ creg c ++ "," ++ creg d ++ "," ++ creg e ++ ")"

463−doOp v LPeekBufferNative [x, y] = v ++ "idris_peekBuffer(vm, " ++ creg x ++ "," ++ creg y ++ ")"

463+doOp v LPeekBuffer [x, y] = v ++ "idris_peekBuffer(vm, " ++ creg x ++ "," ++ creg y ++ ")"

464doOp v (LAppend ity en) [a, b, c, d] = v ++ "idris_append" ++ intTyName ity ++ enName en ++ "(vm, " ++ creg a ++ "," ++ creg b ++ "," ++ creg c ++ "," ++ creg d ++ ")"

465doOp v (LPeek ity en) [x, y] = v ++ "idris_peek" ++ intTyName ity ++ enName en ++ "(vm, " ++ creg x ++ "," ++ creg y ++ ")"

466

src/IRTS/Lang.hs+2−2

@@ -60,8 +60,8 @@ data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy

60 -- Buffers

61 | LAllocate

62 | LCopy

63− | LAppendBufferNative

63+ | LAppendBuffer

64− | LPeekBufferNative

64+ | LPeekBuffer

65 | LAppend IntTy Endianness

66 | LPeek IntTy Endianness

67

src/Idris/Primitives.hs+4−4

@@ -178,10 +178,10 @@ primitives =

178 (1, LAllocate) total,

179 Prim (sUN "prim__copy") (ty [AType (ATInt (ITFixed IT64)), BufferType] BufferType) 2 (p_cantreduce)

180 (2, LCopy) partial,

181− Prim (sUN "prim__peekBufferNative") (ty [BufferType, AType (ATInt (ITFixed IT64))] BufferType) 2 (p_cantreduce)

181+ Prim (sUN "prim__peekBuffer") (ty [BufferType, AType (ATInt (ITFixed IT64))] BufferType) 2 (p_cantreduce)

182− (2, LPeekBufferNative) partial,

182+ (2, LPeekBuffer) partial,

183− Prim (sUN "prim__appendBufferNative") (ty [BufferType, AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), BufferType] BufferType) 5 (p_cantreduce)

183+ Prim (sUN "prim__appendBuffer") (ty [BufferType, AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), BufferType] BufferType) 5 (p_cantreduce)

184− (5, LAppendBufferNative) partial

184+ (5, LAppendBuffer) partial

185 ] ++ concatMap intOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64, ITBig, ITNative, ITChar]

186 ++ concatMap vecOps vecTypes

187 ++ concatMap fixedOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64] -- ITNative, ITChar, ATFloat ] ++ vecTypes

test/buffer001/buffer001.idr+1−1

@@ -21,7 +21,7 @@ firstByte : Bits8

21firstByte = peekBits8LE full 0

22

23firstHalfView : Buffer 4

24−firstHalfView = peekBufferLE full 0

24+firstHalfView = peekBuffer full 0

25

26firstHalfCopy : Buffer 4

27firstHalfCopy = copy firstHalfView