0 | module Data.Linear.Array
 1 |
 2 | import Data.IOArray
 3 |
 4 | -- Linear arrays. General idea: mutable arrays are constructed linearly,
 5 | -- using newArray. Once everything is set up, they can be converted to
 6 | -- read only arrays with constant time, pure, access, using toIArray.
 7 |
 8 | -- Immutable arrays which can be read in constant time, but not updated
 9 | public export
10 | interface Array arr where
11 |   read : (1 _ : arr t) -> Int -> Maybe t
12 |   size : (1 _ : arr t) -> Int
13 |
14 | -- Mutable arrays which can be used linearly
15 | public export
16 | interface Array arr => MArray arr where
17 |   newArray : (size : Int) -> (1 _ : (1 _ : arr t) -> a) -> a
18 |   -- Array is unchanged if the index is out of bounds
19 |   write : (1 _ : arr t) -> Int -> t -> Res Bool (const (arr t))
20 |
21 |   mread : (1 _ : arr t) -> Int -> Res (Maybe t) (const (arr t))
22 |   msize : (1 _ : arr t) -> Res Int (const (arr t))
23 |
24 | export
25 | data IArray : Type -> Type where
26 |      MkIArray : IOArray t -> IArray t
27 |
28 | export
29 | data LinArray : Type -> Type where
30 |      MkLinArray : IOArray t -> LinArray t
31 |
32 | -- Convert a mutable array to an immutable array
33 | export
34 | toIArray : (1 _ : LinArray t) -> (IArray t -> a) -> a
35 | toIArray (MkLinArray arr) k = k (MkIArray arr)
36 |
37 | export
38 | Array LinArray where
39 |   read (MkLinArray a) i = unsafePerformIO (readArray a i)
40 |   size (MkLinArray a) = max a
41 |
42 | export
43 | MArray LinArray where
44 |   newArray size k = k (MkLinArray (unsafePerformIO (newArray size)))
45 |
46 |   write (MkLinArray a) i el
47 |       = unsafePerformIO (do ok <- writeArray a i el
48 |                             pure (ok # MkLinArray a))
49 |   msize (MkLinArray a) = max a # MkLinArray a
50 |   mread (MkLinArray a) i
51 |       = unsafePerformIO (readArray a i) # MkLinArray a
52 |
53 | export
54 | Array IArray where
55 |   read (MkIArray a) i = unsafePerformIO (readArray a i)
56 |   size (MkIArray a) = max a
57 |
58 | export
59 | copyArray : MArray arr => (newsize : Int) -> (1 _ : arr t) ->
60 |             LPair (arr t) (arr t)
61 | copyArray newsize a
62 |     = let size # a = msize a in
63 |           newArray newsize $
64 |             copyContent (min (newsize - 1) (size - 1)) a
65 |   where
66 |     copyContent : Int -> (1 _ : arr t) -> (1 _ : arr t) -> LPair (arr t) (arr t)
67 |     copyContent pos a a'
68 |         = if pos < 0
69 |              then a # a'
70 |              else let val # a = mread a pos
71 |                       1 a' = case val of
72 |                                   Nothing => a'
73 |                                   Just v => let (ok # a') = write a' pos v in
74 |                                             a' in
75 |                       copyContent (pos - 1) a a'
76 |