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