git.iko.soy/Idris-dev
on bfa39bf help sign in
Idris-dev/effects/Effect/Memory.idr
168 lines 6.5 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 () (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 size Bits8)
25 Poke : (offset : Nat) ->
26 (Vect size Bits8) ->
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)
39private
40do_malloc : Nat -> IOExcept String Ptr
41do_malloc size with (fromInteger (cast size) == size)
42 | True = do ptr <- ioe_lift $ mkForeign (FFun "malloc" [FInt] FPtr) (fromInteger $ 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"
48private
49do_memset : Ptr -> Nat -> Bits8 -> Nat -> IO ()
50do_memset ptr offset c size
51 = mkForeign (FFun "idris_memset" [FPtr, FInt, FByte, FInt] FUnit)
52 ptr (fromInteger $ cast offset) c (fromInteger $ cast size)
54private
55do_free : Ptr -> IO ()
56do_free ptr = mkForeign (FFun "free" [FPtr] FUnit) ptr
58private
59do_memmove : Ptr -> Ptr -> Nat -> Nat -> Nat -> IO ()
60do_memmove dest src dest_offset src_offset size
61 = mkForeign (FFun "idris_memmove" [FPtr, FPtr, FInt, FInt, FInt] FUnit)
62 dest src (fromInteger $ cast dest_offset) (fromInteger $ cast src_offset) (fromInteger $ cast size)
64private
65do_peek : Ptr -> Nat -> (size : Nat) -> IO (Vect size Bits8)
66do_peek _ _ Z = return (Prelude.Vect.Nil)
67do_peek ptr offset (S n)
68 = do b <- mkForeign (FFun "idris_peek" [FPtr, FInt] FByte) ptr (fromInteger $ cast offset)
69 bs <- do_peek ptr (S offset) n
70 Prelude.Monad.return (Prelude.Vect.(::) b bs)
72private
73do_poke : Ptr -> Nat -> Vect size Bits8 -> IO ()
74do_poke _ _ [] = return ()
75do_poke ptr offset (b::bs)
76 = do mkForeign (FFun "idris_poke" [FPtr, FInt, FByte] FUnit) ptr (fromInteger $ cast offset) b
77 do_poke ptr (S offset) bs
79instance 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
99RAW_MEMORY : Type -> EFFECT
100RAW_MEMORY t = MkEff t RawMemory
102allocate : (n : Nat) -> EffM m [RAW_MEMORY ()] [RAW_MEMORY (MemoryChunk n 0)] ()
103allocate size = Allocate size
105initialize : {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))] ()
111initialize c size prf = Initialize c size prf
113free : EffM m [RAW_MEMORY (MemoryChunk n i)] [RAW_MEMORY ()] ()
114free = Free
116peek : {i : Nat} ->
117 (offset : Nat) ->
118 (size : Nat) ->
119 so (offset + size <= i) ->
120 Eff m [RAW_MEMORY (MemoryChunk n i)] (Vect size Bits8)
121peek offset size prf = Peek offset size prf
123poke : {n : Nat} ->
124 {i : Nat} ->
125 (offset : Nat) ->
126 Vect size Bits8 ->
127 so (offset <= i && offset + size <= n) ->
128 EffM m [RAW_MEMORY (MemoryChunk n i)] [RAW_MEMORY (MemoryChunk n (max i (offset + size)))] ()
129poke offset content prf = Poke offset content prf
131private
132getRawPtr : Eff m [RAW_MEMORY (MemoryChunk n i)] (MemoryChunk n i)
133getRawPtr = GetRawPtr
135private
136move' : {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)))] ()
147move' src_ptr dst_offset src_offset size dst_bounds src_bounds
148 = Move src_ptr dst_offset src_offset size dst_bounds src_bounds
150data MoveDescriptor = Dst | Src
152move : {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)] ()
165move 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 ()