git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/libs/effects/Effect/Memory.idr
177 lines 6.7 kB history raw
1module Effect.Memory
3import Effects
4import Control.IOExcept
5import Data.Vect
6import public Data.So
8%access public
10abstract
11data MemoryChunk : Nat -> Nat -> Type where
12 CH : Ptr -> MemoryChunk size initialized
14abstract
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 return 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 = return (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 Monad.return (Vect.(::) b bs)
75private
76do_poke : Ptr -> Nat -> Vect size Bits8 -> IO ()
77do_poke _ _ [] = return ()
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
82instance 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
105allocate : (n : Nat) ->
106 Eff () [RAW_MEMORY ()] (\v => [RAW_MEMORY (MemoryChunk n 0)])
107allocate size = call $ Allocate size
109initialize : {i : Nat} ->
110 {n : Nat} ->
111 Bits8 ->
112 (size : Nat) ->
113 So (i + size <= n) ->
114 Eff () [RAW_MEMORY (MemoryChunk n i)]
115 (\v => [RAW_MEMORY (MemoryChunk n (i + size))])
116initialize c size prf = call $ Initialize c size prf
118free : Eff () [RAW_MEMORY (MemoryChunk n i)] (\v => [RAW_MEMORY ()])
119free = call Free
121peek : {i : Nat} ->
122 (offset : Nat) ->
123 (size : Nat) ->
124 So (offset + size <= i) ->
125 { [RAW_MEMORY (MemoryChunk n i)] } Eff (Vect size Bits8)
126peek offset size prf = call $ Peek offset size prf
128poke : {n : Nat} ->
129 {i : Nat} ->
130 (offset : Nat) ->
131 Vect size Bits8 ->
132 So (offset <= i && offset + size <= n) ->
133 Eff () [RAW_MEMORY (MemoryChunk n i)]
134 (\v => [RAW_MEMORY (MemoryChunk n (max i (offset + size)))])
135poke offset content prf = call $ Poke offset content prf
137private
138getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff (MemoryChunk n i)
139getRawPtr = call $ GetRawPtr
141private
142move' : {dst_size : Nat} ->
143 {dst_init : Nat} ->
144 {src_init : Nat} ->
145 (src_ptr : MemoryChunk src_size src_init) ->
146 (dst_offset : Nat) ->
147 (src_offset : Nat) ->
148 (size : Nat) ->
149 So (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
150 So (src_offset + size <= src_init) ->
151 Eff () [RAW_MEMORY (MemoryChunk dst_size dst_init)]
152 (\v => [RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))])
153move' src_ptr dst_offset src_offset size dst_bounds src_bounds
154 = call $ Move src_ptr dst_offset src_offset size dst_bounds src_bounds
156data MoveDescriptor = Dst | Src
158move : {dst_size : Nat} ->
159 {dst_init : Nat} ->
160 {src_size : Nat} ->
161 {src_init : Nat} ->
162 (dst_offset : Nat) ->
163 (src_offset : Nat) ->
164 (size : Nat) ->
165 So (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
166 So (src_offset + size <= src_init) ->
167 Eff ()
168 [ Dst ::: RAW_MEMORY (MemoryChunk dst_size dst_init)
169 , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)]
170 (\v =>
171 [ Dst ::: RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))
172 , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)])
173move dst_offset src_offset size dst_bounds src_bounds
174 = do src_ptr <- Src :- getRawPtr
175 Dst :- move' src_ptr dst_offset src_offset size dst_bounds src_bounds
176 return ()