git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/libs/effects/Effect/Memory.idr
175 lines 6.7 kB history raw
1module Effect.Memory
3import Effects
4import Control.IOExcept
6%access public
8abstract
9data MemoryChunk : Nat -> Nat -> Type where
10 CH : Ptr -> MemoryChunk size initialized
12abstract
13data RawMemory : Effect where
14 Allocate : (n : Nat) ->
15 RawMemory () () (\v => MemoryChunk n 0)
16 Free : RawMemory () (MemoryChunk n i) (\v => ())
17 Initialize : Bits8 ->
18 (size : Nat) ->
19 So (i + size <= n) ->
20 RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (i + size))
21 Peek : (offset : Nat) ->
22 (size : Nat) ->
23 So (offset + size <= i) ->
24 RawMemory (Vect size Bits8)
25 (MemoryChunk n i) (\v => MemoryChunk n i)
26 Poke : (offset : Nat) ->
27 (Vect size Bits8) ->
28 So (offset <= i && offset + size <= n) ->
29 RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (max i (offset + size)))
30 Move : (src : MemoryChunk src_size src_init) ->
31 (dst_offset : Nat) ->
32 (src_offset : Nat) ->
33 (size : Nat) ->
34 So (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
35 So (src_offset + size <= src_init) ->
36 RawMemory () (MemoryChunk dst_size dst_init)
37 (\v => MemoryChunk dst_size (max dst_init (dst_offset + size)))
38 GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (\v => MemoryChunk n i)
40private
41do_malloc : Nat -> IOExcept String Ptr
42do_malloc size with (fromInteger (cast size) == size)
43 | True = do ptr <- ioe_lift $ mkForeign (FFun "malloc" [FInt] FPtr) (fromInteger $ cast size)
44 fail <- ioe_lift $ nullPtr ptr
45 if fail then ioe_fail "Cannot allocate memory"
46 else return ptr
47 | False = ioe_fail "The target architecture does not support adressing enough memory"
49private
50do_memset : Ptr -> Nat -> Bits8 -> Nat -> IO ()
51do_memset ptr offset c size
52 = mkForeign (FFun "idris_memset" [FPtr, FInt, FByte, FInt] FUnit)
53 ptr (fromInteger $ cast offset) c (fromInteger $ cast size)
55private
56do_free : Ptr -> IO ()
57do_free ptr = mkForeign (FFun "free" [FPtr] FUnit) ptr
59private
60do_memmove : Ptr -> Ptr -> Nat -> Nat -> Nat -> IO ()
61do_memmove dest src dest_offset src_offset size
62 = mkForeign (FFun "idris_memmove" [FPtr, FPtr, FInt, FInt, FInt] FUnit)
63 dest src (fromInteger $ cast dest_offset) (fromInteger $ cast src_offset) (fromInteger $ cast size)
65private
66do_peek : Ptr -> Nat -> (size : Nat) -> IO (Vect size Bits8)
67do_peek _ _ Z = return (Prelude.Vect.Nil)
68do_peek ptr offset (S n)
69 = do b <- mkForeign (FFun "idris_peek" [FPtr, FInt] FByte) ptr (fromInteger $ cast offset)
70 bs <- do_peek ptr (S offset) n
71 Prelude.Monad.return (Prelude.Vect.(::) b bs)
73private
74do_poke : Ptr -> Nat -> Vect size Bits8 -> IO ()
75do_poke _ _ [] = return ()
76do_poke ptr offset (b::bs)
77 = do mkForeign (FFun "idris_poke" [FPtr, FInt, FByte] FUnit) ptr (fromInteger $ cast offset) b
78 do_poke ptr (S offset) bs
80instance Handler RawMemory (IOExcept String) where
81 handle () (Allocate n) k
82 = do ptr <- do_malloc n
83 k () (CH ptr)
84 handle {-{res = MemoryChunk _ offset}-} (CH ptr) (Initialize {i} c size _) k
85 = ioe_lift (do_memset ptr i c size) $> k () (CH ptr)
86 handle (CH ptr) (Free) k
87 = ioe_lift (do_free ptr) $> k () ()
88 handle (CH ptr) (Peek offset size _) k
89 = do res <- ioe_lift (do_peek ptr offset size)
90 k res (CH ptr)
91 handle (CH ptr) (Poke offset content _) k
92 = do ioe_lift (do_poke ptr offset content)
93 k () (CH ptr)
94 handle (CH dest_ptr) (Move (CH src_ptr) dest_offset src_offset size _ _) k
95 = do ioe_lift (do_memmove dest_ptr src_ptr dest_offset src_offset size)
96 k () (CH dest_ptr)
97 handle chunk (GetRawPtr) k
98 = k chunk chunk
100RAW_MEMORY : Type -> EFFECT
101RAW_MEMORY t = MkEff t RawMemory
103allocate : (n : Nat) ->
104 Eff () [RAW_MEMORY ()] (\v => [RAW_MEMORY (MemoryChunk n 0)])
105allocate size = call $ Allocate size
107initialize : {i : Nat} ->
108 {n : Nat} ->
109 Bits8 ->
110 (size : Nat) ->
111 So (i + size <= n) ->
112 Eff () [RAW_MEMORY (MemoryChunk n i)]
113 (\v => [RAW_MEMORY (MemoryChunk n (i + size))])
114initialize c size prf = call $ Initialize c size prf
116free : Eff () [RAW_MEMORY (MemoryChunk n i)] (\v => [RAW_MEMORY ()])
117free = call Free
119peek : {i : Nat} ->
120 (offset : Nat) ->
121 (size : Nat) ->
122 So (offset + size <= i) ->
123 { [RAW_MEMORY (MemoryChunk n i)] } Eff (Vect size Bits8)
124peek offset size prf = call $ Peek offset size prf
126poke : {n : Nat} ->
127 {i : Nat} ->
128 (offset : Nat) ->
129 Vect size Bits8 ->
130 So (offset <= i && offset + size <= n) ->
131 Eff () [RAW_MEMORY (MemoryChunk n i)]
132 (\v => [RAW_MEMORY (MemoryChunk n (max i (offset + size)))])
133poke offset content prf = call $ Poke offset content prf
135private
136getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff (MemoryChunk n i)
137getRawPtr = call $ GetRawPtr
139private
140move' : {dst_size : Nat} ->
141 {dst_init : Nat} ->
142 {src_init : Nat} ->
143 (src_ptr : MemoryChunk src_size src_init) ->
144 (dst_offset : Nat) ->
145 (src_offset : Nat) ->
146 (size : Nat) ->
147 So (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
148 So (src_offset + size <= src_init) ->
149 Eff () [RAW_MEMORY (MemoryChunk dst_size dst_init)]
150 (\v => [RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))])
151move' src_ptr dst_offset src_offset size dst_bounds src_bounds
152 = call $ Move src_ptr dst_offset src_offset size dst_bounds src_bounds
154data MoveDescriptor = Dst | Src
156move : {dst_size : Nat} ->
157 {dst_init : Nat} ->
158 {src_size : Nat} ->
159 {src_init : Nat} ->
160 (dst_offset : Nat) ->
161 (src_offset : Nat) ->
162 (size : Nat) ->
163 So (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
164 So (src_offset + size <= src_init) ->
165 Eff ()
166 [ Dst ::: RAW_MEMORY (MemoryChunk dst_size dst_init)
167 , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)]
168 (\v =>
169 [ Dst ::: RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))
170 , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)])
171move dst_offset src_offset size dst_bounds src_bounds
172 = do src_ptr <- Src :- getRawPtr
173 Dst :- move' src_ptr dst_offset src_offset size dst_bounds src_bounds
174 return ()