35096cf · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'master' of github.com:edwinb/Idris-dev

commit35096cfcb4180b41ff14386f9d09a6de568320ac authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 10 Apr 2013, 09:30 (14 years ago) parent8624d06 bb54695

11 files changed+322−6

compare with master

unifiedsplit

effects/Effect/Memory.idr+168 effects/effects.ipkg+3−1 java/src/main/java/org/idris/rts/ForeignPrimitives.java+42 lib/Prelude/Maybe.idr+1−1 rts/idris_rts.c+45 rts/idris_rts.h+10 src/IRTS/CodegenC.hs+4 src/IRTS/CodegenJava.hs+10−4 test/test025/expected+1 test/test025/run+4 test/test025/test025.idr+34

effects/Effect/Memory.idrnew file+168

@@ -0,0 +1,168 @@

1+module Effect.Memory

3+import Effects

4+import Control.IOExcept

6+%access public

8+abstract

9+data MemoryChunk : Nat -> Nat -> Type where

10+ CH : Ptr -> MemoryChunk size initialized

11+

12+abstract

13+data RawMemory : Effect where

14+ Allocate : (n : Nat) ->

15+ RawMemory () (MemoryChunk n 0) ()

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

17+ Initialize : Bits8 ->

18+ (size : Nat) ->

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

20+ RawMemory (MemoryChunk n i) (MemoryChunk n (i + size)) ()

21+ Peek : (offset : Nat) ->

22+ (size : Nat) ->

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

24+ RawMemory (MemoryChunk n i) (MemoryChunk n i) (Vect Bits8 size)

25+ Poke : (offset : Nat) ->

26+ (Vect Bits8 size) ->

27+ so (offset <= i && offset + size <= n) ->

28+ RawMemory (MemoryChunk n i) (MemoryChunk n (max i (offset + size))) ()

29+ Move : (src : MemoryChunk src_size src_init) ->

30+ (dst_offset : Nat) ->

31+ (src_offset : Nat) ->

32+ (size : Nat) ->

33+ so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

34+ so (src_offset + size <= src_init) ->

35+ RawMemory (MemoryChunk dst_size dst_init)

36+ (MemoryChunk dst_size (max dst_init (dst_offset + size))) ()

37+ GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (MemoryChunk n i)

38+

39+private

40+do_malloc : Nat -> IOExcept String Ptr

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

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

43+ fail <- ioe_lift $ nullPtr ptr

44+ if fail then ioe_fail "Cannot allocate memory"

45+ else return ptr

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

47+

48+private

49+do_memset : Ptr -> Nat -> Bits8 -> Nat -> IO ()

50+do_memset ptr offset c size

51+ = mkForeign (FFun "idris_memset" [FPtr, FInt, FAny Bits8, FInt] FUnit)

52+ ptr (cast offset) c (cast size)

53+

54+private

55+do_free : Ptr -> IO ()

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

57+

58+private

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

60+do_memmove dest src dest_offset src_offset size

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

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

63+

64+private

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

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

67+do_peek ptr offset (S n)

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

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

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

71+

72+private

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

74+do_poke _ _ [] = return ()

75+do_poke ptr offset (b::bs)

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

77+ do_poke ptr (S offset) bs

78+

79+instance Handler RawMemory (IOExcept String) where

80+ handle () (Allocate n) k

81+ = do ptr <- do_malloc n

82+ k (CH ptr) ()

83+ handle {res = MemoryChunk _ offset} (CH ptr) (Initialize c size _) k

84+ = ioe_lift (do_memset ptr offset c size) $> k (CH ptr) ()

85+ handle (CH ptr) (Free) k

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

87+ handle (CH ptr) (Peek offset size _) k

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

89+ k (CH ptr) res

90+ handle (CH ptr) (Poke offset content _) k

91+ = do ioe_lift (do_poke ptr offset content)

92+ k (CH ptr) ()

93+ handle (CH dest_ptr) (Move (CH src_ptr) dest_offset src_offset size _ _) k

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

95+ k (CH dest_ptr) ()

96+ handle chunk (GetRawPtr) k

97+ = k chunk chunk

98+

99+RAW_MEMORY : Type -> EFFECT

100+RAW_MEMORY t = MkEff t RawMemory

101+

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

103+allocate size = Allocate size

104+

105+initialize : {i : Nat} ->

106+ {n : Nat} ->

107+ Bits8 ->

108+ (size : Nat) ->

109+ so (i + size <= n) ->

110+ EffM m [RAW_MEMORY (MemoryChunk n i)] [RAW_MEMORY (MemoryChunk n (i + size))] ()

111+initialize c size prf = Initialize c size prf

112+

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

114+free = Free

115+

116+peek : {i : Nat} ->

117+ (offset : Nat) ->

118+ (size : Nat) ->

119+ so (offset + size <= i) ->

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

121+peek offset size prf = Peek offset size prf

122+

123+poke : {n : Nat} ->

124+ {i : Nat} ->

125+ (offset : Nat) ->

126+ Vect Bits8 size ->

127+ so (offset <= i && offset + size <= n) ->

128+ EffM m [RAW_MEMORY (MemoryChunk n i)] [RAW_MEMORY (MemoryChunk n (max i (offset + size)))] ()

129+poke offset content prf = Poke offset content prf

130+

131+private

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

133+getRawPtr = GetRawPtr

134+

135+private

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

137+ {dst_init : Nat} ->

138+ {src_init : Nat} ->

139+ (src_ptr : MemoryChunk src_size src_init) ->

140+ (dst_offset : Nat) ->

141+ (src_offset : Nat) ->

142+ (size : Nat) ->

143+ so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

144+ so (src_offset + size <= src_init) ->

145+ EffM m [RAW_MEMORY (MemoryChunk dst_size dst_init)]

146+ [RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))] ()

147+move' src_ptr dst_offset src_offset size dst_bounds src_bounds

148+ = Move src_ptr dst_offset src_offset size dst_bounds src_bounds

149+

150+data MoveDescriptor = Dst | Src

151+

152+move : {dst_size : Nat} ->

153+ {dst_init : Nat} ->

154+ {src_size : Nat} ->

155+ {src_init : Nat} ->

156+ (dst_offset : Nat) ->

157+ (src_offset : Nat) ->

158+ (size : Nat) ->

159+ so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

160+ so (src_offset + size <= src_init) ->

161+ EffM m [ Dst ::: RAW_MEMORY (MemoryChunk dst_size dst_init)

162+ , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)]

163+ [ Dst ::: RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))

164+ , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)] ()

165+move dst_offset src_offset size dst_bounds src_bounds

166+ = do src_ptr <- Src :- getRawPtr

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

168+ return ()

effects/effects.ipkg+3−1

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

33opts = "-i ../lib"

44modules = Effects,

55 Effect.Exception, Effect.File, Effect.State,

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

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

7+ Effect.Memory

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

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

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

192192 }

193193

194+ public static Object malloc(int size) {

195+ return ByteBuffer.allocate(size);

196+ }

197+

198+ public static void idris_memset(Object buf, int offset, Object c, int size) {

199+ ByteBuffer buffer = (ByteBuffer)buf;

200+ buffer.rewind();

201+ buffer.position(offset);

202+ byte init[] = new byte[size];

203+ Arrays.fill(init, (Byte)c);

204+ buffer.put(init, offset, size);

205+ buffer.rewind();

206+ }

207+

208+ public static void free(Object buf) {

209+ buf = null;

210+ }

211+

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

213+ ByteBuffer buffer = (ByteBuffer)buf;

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

215+ }

216+

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

218+ ByteBuffer buffer = (ByteBuffer)buf;

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

220+ }

221+

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

223+ ByteBuffer dst = (ByteBuffer)dstBuf;

224+ ByteBuffer src = (ByteBuffer)srcBuf;

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

226+ src.rewind();

227+ src.position(srcOffset);

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

229+ src.rewind();

230+ dst.rewind();

231+ dst.position(dstOffset);

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

233+ dst.rewind();

234+ }

235+

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

195237 return result;

196238 }

lib/Prelude/Maybe.idr+1−1

@@ -66,7 +66,7 @@ instance (Eq a) => Eq (Maybe a) where

6666-- | Lift a semigroup into 'Maybe' forming a 'Monoid' according to

6767-- <http://en.wikipedia.org/wiki/Monoid>: "Any semigroup S may be

6868-- turned into a monoid simply by adjoining an element i not in S

69−-- and defining i+i = i and i+s = s = s+i for all s ∈ S."

69+-- and defining i+i = i and i+s = s = s+i for all s in S."

7070

7171instance (Semigroup a) => Semigroup (Maybe a) where

7272 Nothing <+> m = m

rts/idris_rts.c+45

@@ -186,6 +186,34 @@ VAL MKPTRc(VM* vm, void* ptr) {

186186 return cl;

187187}

188188

189+VAL MKB8(VM* vm, uint8_t bits8) {

190+ Closure* cl = allocate(vm, sizeof(Closure), 1);

191+ SETTY(cl, BITS8);

192+ cl -> info.bits8 = bits8;

193+ return cl;

194+}

195+

196+VAL MKB16(VM* vm, uint16_t bits16) {

197+ Closure* cl = allocate(vm, sizeof(Closure), 1);

198+ SETTY(cl, BITS16);

199+ cl -> info.bits16 = bits16;

200+ return cl;

201+}

202+

203+VAL MKB32(VM* vm, uint32_t bits32) {

204+ Closure* cl = allocate(vm, sizeof(Closure), 1);

205+ SETTY(cl, BITS32);

206+ cl -> info.bits32 = bits32;

207+ return cl;

208+}

209+

210+VAL MKB64(VM* vm, uint64_t bits64) {

211+ Closure* cl = allocate(vm, sizeof(Closure), 1);

212+ SETTY(cl, BITS64);

213+ cl -> info.bits64 = bits64;

214+ return cl;

215+}

216+

189217void PROJECT(VM* vm, VAL r, int loc, int arity) {

190218 int i;

191219 for(i = 0; i < arity; ++i) {

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

243271

244272}

245273

274+void idris_memset(void* ptr, i_int offset, VAL c, i_int size) {

275+ memset(((uint8_t*)ptr) + offset, c->info.bits8, size);

276+}

277+

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

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

280+ return (int)res;

281+}

282+

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

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

285+}

286+

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

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

289+}

290+

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

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

248293 SETTY(cl, STRING);

rts/idris_rts.h+10

@@ -147,6 +147,10 @@ typedef intptr_t i_int;

147147VAL MKFLOAT(VM* vm, double val);

148148VAL MKSTR(VM* vm, char* str);

149149VAL MKPTR(VM* vm, void* ptr);

150+VAL MKB8(VM* vm, uint8_t b);

151+VAL MKB16(VM* vm, uint16_t b);

152+VAL MKB32(VM* vm, uint32_t b);

153+VAL MKB64(VM* vm, uint64_t b);

150154

151155// following versions don't take a lock when allocating

152156VAL MKFLOATc(VM* vm, double val);

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

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

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

204208

209+// Raw memory manipulation

210+void idris_memset(void* ptr, i_int offset, VAL c, i_int size);

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

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

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

214+

205215// String primitives

206216

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

src/IRTS/CodegenC.hs+4

@@ -105,6 +105,10 @@ bcc i (ASSIGNCONST l c)

105105 mkConst (Fl f) = "MKFLOAT(vm, " ++ show f ++ ")"

106106 mkConst (Ch c) = "MKINT(" ++ show (fromEnum c) ++ ")"

107107 mkConst (Str s) = "MKSTR(vm, " ++ show s ++ ")"

108+ mkConst (B8 b) = "MKB8(vm, " ++ show b ++")"

109+ mkConst (B16 b) = "MKB16(vm, " ++ show b ++ ")"

110+ mkConst (B32 b) = "MKB32(vm, " ++ show b ++ ")"

111+ mkConst (B64 b) = "MKB64(vm, " ++ show b ++ ")"

108112 mkConst _ = "MKINT(42424242)"

109113bcc i (UPDATE l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"

110114bcc i (MKCON l tag args)

src/IRTS/CodegenJava.hs+10−4

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

418418 cleanReserved "idris_K" = "_idris_K"

419419 cleanReserved "idris_flipK" = "_idris_flipK"

420420 cleanReserved "idris_assignStack" = "_idris_assignStack"

421+ cleanReserved "free" = "_free"

422+ cleanReserved "malloc" = "_malloc"

423+ cleanReserved "idris_memset" = "_idris_memset"

424+ cleanReserved "idris_peek" = "_idris_peek"

425+ cleanReserved "idris_poke" = "_idris_poke"

426+ cleanReserved "idris_memmove" = "_idris_memmove"

421427

422428 cleanReserved x = x

423429

@@ -1233,10 +1239,10 @@ mkExp (SConst BIType) = return $ mkClass bigIntegerType

12331239mkExp (SConst FlType) = return $ mkClass doubleType

12341240mkExp (SConst ChType) = return $ mkClass charType

12351241mkExp (SConst StrType) = return $ mkClass stringType

1236−mkExp (SConst (B8 x)) = return $ mkPrimitive "Byte" (Int (toInteger x))

1237−mkExp (SConst (B16 x)) = return $ mkPrimitive "Short" (Int (toInteger x))

1242+mkExp (SConst (B8 x)) = return $ mkPrimitive "Byte" (String (show x))

1243+mkExp (SConst (B16 x)) = return $ mkPrimitive "Short" (String (show x))

12381244mkExp (SConst (B32 x)) = return $ mkPrimitive "Integer" (Int (toInteger x))

1239−mkExp (SConst (B64 x)) = return $ mkPrimitive "Long" (Int (toInteger x))

1245+mkExp (SConst (B64 x)) = return $ mkPrimitive "Long" (String (show x))

12401246mkExp (SConst (B8Type))= return $ mkClass byteType

12411247mkExp (SConst (B16Type)) = return $ mkClass shortType

12421248mkExp (SConst (B32Type)) = return $ mkClass integerType

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

16521658 []

16531659 (Ident "throwSelf")

16541660 []

1655−mkExp other = error (show other)

1661+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 test025

3+./test025

4+rm -f test025 *.ibc

test/test025/test025.idrnew file+34

@@ -0,0 +1,34 @@

1+module Main

3+import Effects

4+import Effect.Memory

5+import Control.IOExcept

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+ Dst :- initialize (prim__intToB8 1) 2 oh

22+ move 2 2 3 oh oh

23+ Src :- free

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

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

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

27+ Dst :- free

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

29+

30+main : IO ()

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

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

33+

34+