441d941 · Idris-dev · git.iko.soy

effects/Effect/Memory.idrnew file+139

compare with master

unifiedsplit

@@ -0,0 +1,139 @@

1+module Effect.Memory

2+

3+import Effects

4+import Control.IOExcept

5+

6+%access public

7+

8+abstract

9+data MemoryChunk : Nat -> Type where

10+ CH : Ptr -> (size : Nat) -> MemoryChunk size

11+

12+abstract

13+data RawMemory : Effect where

14+ Allocate : (n : Nat) ->

15+ RawMemory () (MemoryChunk n) ()

16+ Free : RawMemory (MemoryChunk n) () ()

17+ Peek : (offset : Nat) ->

18+ (size : Nat) ->

19+ so (offset + size <= n) ->

20+ RawMemory (MemoryChunk n) (MemoryChunk n) (Vect Bits8 size)

21+ Poke : (offset : Nat) ->

22+ (Vect Bits8 size) ->

23+ so (offset + size <= n) ->

24+ RawMemory (MemoryChunk n) (MemoryChunk n) ()

25+ Move : (src : MemoryChunk m) ->

26+ (dest_offset : Nat) ->

27+ (src_offset : Nat) ->

28+ (size : Nat) ->

29+ so (dest_offset + size <= n) ->

30+ so (src_offset + size <= m) ->

31+ RawMemory (MemoryChunk n) (MemoryChunk n) ()

32+ GetRawPtr : RawMemory (MemoryChunk n) (MemoryChunk n) (MemoryChunk n)

33+

34+private

35+do_malloc : Nat -> IOExcept String Ptr

36+do_malloc size with (fromInteger (cast size) == size)

37+ | True = do ptr <- ioe_lift $ mkForeign (FFun "malloc" [FInt] FPtr) (cast size)

38+ fail <- ioe_lift $ nullPtr ptr

39+ if fail then ioe_fail "Cannot allocate memory"

40+ else return ptr

41+ | False = ioe_fail "The target architecture does not support adressing enough memory"

42+

43+private

44+do_free : Ptr -> IO ()

45+do_free ptr = mkForeign (FFun "free" [FPtr] FUnit) ptr

46+

47+private

48+do_memmove : Ptr -> Ptr -> Nat -> Nat -> Nat -> IO ()

49+do_memmove dest src dest_offset src_offset size

50+ = mkForeign (FFun "idris_memmove" [FPtr, FPtr, FInt, FInt, FInt] FUnit)

51+ dest src (cast dest_offset) (cast src_offset) (cast size)

52+

53+private

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

55+do_peek _ _ O = return (Prelude.Vect.Nil)

56+do_peek ptr offset (S n)

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

58+ bs <- do_peek ptr (S offset) n

59+ Prelude.Monad.return (Prelude.Vect.(::) (prim__intToB8 b) bs)

60+

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

62+do_poke _ _ [] = return ()

63+do_poke ptr offset (b::bs)

64+ = do mkForeign (FFun "idris_poke" [FPtr, FInt, FAny Bits8] FUnit) ptr (cast offset) b

65+ do_poke ptr (S offset) bs

66+

67+instance Handler RawMemory (IOExcept String) where

68+ handle () (Allocate n) k

69+ = do ptr <- do_malloc n

70+ k (CH ptr n) ()

71+ handle (CH ptr n) (Free) k

72+ = ioe_lift (do_free ptr) $> k () ()

73+ handle (CH ptr n) (Peek offset size _) k

74+ = do res <- ioe_lift (do_peek ptr offset size)

75+ k (CH ptr n) res

76+ handle (CH ptr n) (Poke offset content _) k

77+ = do ioe_lift (do_poke ptr offset content)

78+ k (CH ptr n) ()

79+ handle (CH dest_ptr n) (Move (CH src_ptr m) dest_offset src_offset size _ _) k

80+ = do ioe_lift (do_memmove dest_ptr src_ptr dest_offset src_offset size)

81+ k (CH dest_ptr n) ()

82+ handle (CH ptr n) (GetRawPtr) k

83+ = k (CH ptr n) (CH ptr n)

84+

85+RAW_MEMORY : Type -> EFFECT

86+RAW_MEMORY t = MkEff t RawMemory

87+

88+allocate : (n : Nat) -> EffM m [RAW_MEMORY ()] [RAW_MEMORY (MemoryChunk n)] ()

89+allocate size = Allocate size

90+

91+free : EffM m [RAW_MEMORY (MemoryChunk n)] [RAW_MEMORY ()] ()

92+free = Free

93+

94+peek : {n : Nat} ->

95+ (offset : Nat) ->

96+ (size : Nat) ->

97+ so (offset + size <= n) ->

98+ Eff m [RAW_MEMORY (MemoryChunk n)] (Vect Bits8 size)

99+peek offset size prf = Peek offset size prf

100+

101+poke : {n : Nat} ->

102+ (offset : Nat) ->

103+ Vect Bits8 size ->

104+ so (offset + size <= n) ->

105+ Eff m [RAW_MEMORY (MemoryChunk n)] ()

106+poke offset content prf = Poke offset content prf

107+

108+private

109+getRawPtr : Eff m [RAW_MEMORY (MemoryChunk n)] (MemoryChunk n)

110+getRawPtr = GetRawPtr

111+

112+private

113+move' : {dst_size : Nat} ->

114+ {src_size : Nat} ->

115+ (src_ptr : MemoryChunk src_size) ->

116+ (dst_offset : Nat) ->

117+ (src_offset : Nat) ->

118+ (size : Nat) ->

119+ so (dst_offset + size <= dst_size) ->

120+ so (src_offset + size <= src_size) ->

121+ Eff m [RAW_MEMORY (MemoryChunk dst_size)] ()

122+move' src_ptr dst_offset src_offset size dst_bounds src_bounds

123+ = Move src_ptr dst_offset src_offset size dst_bounds src_bounds

124+

125+data MoveDescriptor = Dst | Src

126+

127+move : {dst_size : Nat} ->

128+ {src_size : Nat} ->

129+ (dst_offset : Nat) ->

130+ (src_offset : Nat) ->

131+ (size : Nat) ->

132+ so (dst_offset + size <= dst_size) ->

133+ so (src_offset + size <= src_size) ->

134+ Eff m [ Dst ::: RAW_MEMORY (MemoryChunk dst_size)

135+ , Src ::: RAW_MEMORY (MemoryChunk src_size)] ()

136+move dst_offset src_offset size dst_bounds src_bounds

137+ = do src_ptr <- Src :- getRawPtr

138+ Dst :- move' src_ptr dst_offset src_offset size dst_bounds src_bounds

139+ return ()

effects/effects.ipkg+3−1

@@ -3,4 +3,6 @@ package effects

3opts = "-i ../lib"

4modules = Effects,

5 Effect.Exception, Effect.File, Effect.State,

6− Effect.Random, Effect.StdIO, Effect.Select

6+ Effect.Random, Effect.StdIO, Effect.Select,

7+ Effect.Memory

8+

java/src/main/java/org/idris/rts/ForeignPrimitives.java+32

@@ -191,6 +191,38 @@ public class ForeignPrimitives {

191 return (o == null ? 1 : 0);

192 }

193

194+ public static Object malloc(int size) {

195+ return ByteBuffer.allocate(size);

196+ }

197+

198+ public static void free(Object buf) {

199+ buf = null;

200+ }

201+

202+ public static Integer idris_peek(Object buf, int offset) {

203+ ByteBuffer buffer = (ByteBuffer)buf;

204+ return Integer.valueOf(buffer.get(offset));

205+ }

206+

207+ public static void idris_poke(Object buf, int offset, Object data) {

208+ ByteBuffer buffer = (ByteBuffer)buf;

209+ buffer.put(offset, (Byte)data);

210+ }

211+

212+ public static void idris_memmove(Object dstBuf, Object srcBuf, int dstOffset, int srcOffset, int size) {

213+ ByteBuffer dst = (ByteBuffer)dstBuf;

214+ ByteBuffer src = (ByteBuffer)srcBuf;

215+ byte [] srcData = new byte[size];

216+ src.rewind();

217+ src.position(srcOffset);

218+ src.get(srcData, 0, size);

219+ src.rewind();

220+ dst.rewind();

221+ dst.position(dstOffset);

222+ dst.put(srcData, 0, size);

223+ dst.rewind();

224+ }

225+

194 public final static Object idris_K(final Object result, final Object drop) {

226 public final static Object idris_K(final Object result, final Object drop) {

195 return result;

227 return result;

196 }

228 }

rts/idris_rts.c+13

@@ -243,6 +243,19 @@ void dumpVal(VAL v) {

243

244}

245

246+int idris_peek(void* ptr, i_int offset) {

247+ uint8_t res = *(((uint8_t*)ptr) + offset);

248+ return (int)res;

249+}

250+

251+void idris_poke(void* ptr, i_int offset, VAL data) {

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

253+}

254+

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

256+ memmove(dest + dest_offset, src + src_offset, size);

257+}

258+

246VAL idris_castIntStr(VM* vm, VAL i) {

259VAL idris_castIntStr(VM* vm, VAL i) {

247 Closure* cl = allocate(vm, sizeof(Closure) + sizeof(char)*16, 0);

260 Closure* cl = allocate(vm, sizeof(Closure) + sizeof(char)*16, 0);

248 SETTY(cl, STRING);

261 SETTY(cl, STRING);

rts/idris_rts.h+5

@@ -202,6 +202,11 @@ VAL idris_castStrInt(VM* vm, VAL i);

202VAL idris_castFloatStr(VM* vm, VAL i);

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

204

205+// Raw memory manipulation

206+int idris_peek(void* ptr, i_int offset);

207+void idris_poke(void* ptr, i_int offset, VAL data);

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

209+

205// String primitives

210// String primitives

206

211

207VAL idris_concat(VM* vm, VAL l, VAL r);

212VAL idris_concat(VM* vm, VAL l, VAL r);

src/IRTS/CodegenJava.hs+6−1

@@ -418,6 +418,11 @@ mkIdentifier (UN name) =

418 cleanReserved "idris_K" = "_idris_K"

419 cleanReserved "idris_flipK" = "_idris_flipK"

420 cleanReserved "idris_assignStack" = "_idris_assignStack"

421+ cleanReserved "free" = "_free"

422+ cleanReserved "malloc" = "_malloc"

423+ cleanReserved "idris_peek" = "_idris_peek"

424+ cleanReserved "idris_poke" = "_idris_poke"

425+ cleanReserved "idris_memmove" = "_idris_memmove"

421

426

422 cleanReserved x = x

427 cleanReserved x = x

423

428

@@ -1652,4 +1657,4 @@ mkExp (SError err) =

1652 []

1657 []

1653 (Ident "throwSelf")

1658 (Ident "throwSelf")

1654 []

1659 []

1655−mkExp other = error (show other)

1660+mkExp other = error (show other)

test/test025/expectednew file+1

@@ -0,0 +1 @@

1+[1, 2, 3, 4]

test/test025/runnew file+4

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

1+#!/bin/bash

2+idris -p effects $@ test025.idr -o test024

3+./test025

4+rm -f test025 *.ibc

test/test025/test025.idrnew file+33

@@ -0,0 +1,33 @@

1+module Main

2+

3+import Effects

4+import Effect.Memory

5+import Control.IOExcept

6+

7+MemoryIO : Type -> Type -> Type -> Type

8+MemoryIO td ts r = Eff (IOExcept String) [ Dst ::: RAW_MEMORY td

9+ , Src ::: RAW_MEMORY ts ] r

10+

11+inpVect : Vect Bits8 5

12+inpVect = map prim__intToB8 [0, 1, 2, 3, 5]

13+

14+sub1 : Vect Bits8 n -> Vect Bits8 n

15+sub1 xs = map (prim__intToB8 . (\ x => x - 1) . prim__B32ToInt . prim__sextB8_32) xs

16+

17+testMemory : MemoryIO () () (Vect Int 4)

18+testMemory = do Src :- allocate 5

19+ Src :- poke 0 inpVect oh

20+ Dst :- allocate 5

21+ move 1 1 4 oh oh

22+ Src :- free

23+ end <- Dst :- peek 4 1 oh

24+ Dst :- poke 4 (sub1 end) oh

25+ res <- Dst :- peek 1 4 oh

26+ Dst :- free

27+ return (map (prim__B32ToInt . prim__sextB8_32) res)

28+

29+main : IO ()

30+main = do ioe_run (run [Dst := (), Src := ()] testMemory)

31+ (\err => print err) (\ok => print ok)

32+

33+