0 | {--
  1 | Copyright (C) 2026  Joel Berkeley
  2 |
  3 | This program is free software: you can redistribute it and/or modify
  4 | it under the terms of the GNU Affero General Public License as published
  5 | by the Free Software Foundation, either version 3 of the License, or
  6 | (at your option) any later version.
  7 |
  8 | This program is distributed in the hope that it will be useful,
  9 | but WITHOUT ANY WARRANTY; without even the implied warranty of
 10 | MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 11 | GNU Affero General Public License for more details.
 12 |
 13 | You should have received a copy of the GNU Affero General Public License
 14 | along with this program.  If not, see <https://www.gnu.org/licenses/>.
 15 | --}
 16 | ||| For internal spidr use only.
 17 | module Spidr.Compiler.Array
 18 |
 19 | import Spidr.Compiler.FFI
 20 | import Spidr.Data.List
 21 |
 22 | ffi : String -> String
 23 | ffi = libxla "c/array.h"
 24 |
 25 | export
 26 | %foreign (ffi "sizeof_ptr")
 27 | sizeofPtr : Bits64
 28 |
 29 | export
 30 | %foreign (ffi "get_array_void_ptr")
 31 | prim__getArrayVoidPtr : AnyPtr -> Bits64 -> AnyPtr
 32 |
 33 | export
 34 | %foreign (ffi "set_array_void_ptr")
 35 | prim__setArrayVoidPtr : AnyPtr -> Bits64 -> AnyPtr -> PrimIO ()
 36 |
 37 | public export
 38 | data Array a = MkArray GCAnyPtr Bits64
 39 |
 40 | public export
 41 | interface ArrayType a where
 42 |   elemSize : Bits64
 43 |   get : Array a -> Nat -> a
 44 |   set : HasIO io => Array a -> Nat -> a -> io ()
 45 |
 46 | %foreign (ffi "sizeof_int8_t")
 47 | sizeofInt8 : Bits64
 48 |
 49 | %foreign (ffi "get_array_int8_t")
 50 | prim__getArrayInt8 : GCAnyPtr -> Bits64 -> Int8
 51 |
 52 | %foreign (ffi "set_array_int8_t")
 53 | prim__setArrayInt8 : GCAnyPtr -> Bits64 -> Int8 -> PrimIO ()
 54 |
 55 | export
 56 | ArrayType Int8 where
 57 |   elemSize = sizeofInt8
 58 |   get (MkArray arr _) idx = prim__getArrayInt8 arr (cast idx)
 59 |   set (MkArray arr _) idx x = primIO $ prim__setArrayInt8 arr (cast idx) x
 60 |
 61 | %foreign (ffi "sizeof_int16_t")
 62 | sizeofInt16 : Bits64
 63 |
 64 | %foreign (ffi "get_array_int16_t")
 65 | prim__getArrayInt16 : GCAnyPtr -> Bits64 -> Int16
 66 |
 67 | %foreign (ffi "set_array_int16_t")
 68 | prim__setArrayInt16 : GCAnyPtr -> Bits64 -> Int16 -> PrimIO ()
 69 |
 70 | export
 71 | ArrayType Int16 where
 72 |   elemSize = sizeofInt16
 73 |   get (MkArray arr _) idx = prim__getArrayInt16 arr (cast idx)
 74 |   set (MkArray arr _) idx x = primIO $ prim__setArrayInt16 arr (cast idx) x
 75 |
 76 | %foreign (ffi "sizeof_int32_t")
 77 | sizeofInt32 : Bits64
 78 |
 79 | %foreign (ffi "get_array_int32_t")
 80 | prim__getArrayInt32 : GCAnyPtr -> Bits64 -> Int32
 81 |
 82 | %foreign (ffi "set_array_int32_t")
 83 | prim__setArrayInt32 : GCAnyPtr -> Bits64 -> Int32 -> PrimIO ()
 84 |
 85 | export
 86 | ArrayType Int32 where
 87 |   elemSize = sizeofInt32
 88 |   get (MkArray arr _) idx = prim__getArrayInt32 arr (cast idx)
 89 |   set (MkArray arr _) idx x = primIO $ prim__setArrayInt32 arr (cast idx) x
 90 |
 91 | %foreign (ffi "sizeof_int64_t")
 92 | sizeofInt64 : Bits64
 93 |
 94 | %foreign (ffi "get_array_int64_t")
 95 | prim__getArrayInt64 : GCAnyPtr -> Bits64 -> Int64
 96 |
 97 | %foreign (ffi "set_array_int64_t")
 98 | prim__setArrayInt64 : GCAnyPtr -> Bits64 -> Int64 -> PrimIO ()
 99 |
100 | export
101 | ArrayType Int64 where
102 |   elemSize = sizeofInt64
103 |   get (MkArray arr _) idx = prim__getArrayInt64 arr (cast idx)
104 |   set (MkArray arr _) idx x = primIO $ prim__setArrayInt64 arr (cast idx) x
105 |
106 | %foreign (ffi "sizeof_uint8_t")
107 | sizeofUInt8 : Bits64
108 |
109 | %foreign (ffi "get_array_uint8_t")
110 | prim__getArrayUInt8 : GCAnyPtr -> Bits64 -> Bits8
111 |
112 | %foreign (ffi "set_array_uint8_t")
113 | prim__setArrayUInt8 : GCAnyPtr -> Bits64 -> Bits8 -> PrimIO ()
114 |
115 | export
116 | ArrayType Bits8 where
117 |   elemSize = sizeofUInt8
118 |   get (MkArray arr _) idx = prim__getArrayUInt8 arr (cast idx)
119 |   set (MkArray arr _) idx x = primIO $ prim__setArrayUInt8 arr (cast idx) x
120 |
121 | %foreign (ffi "sizeof_uint16_t")
122 | sizeofUInt16 : Bits64
123 |
124 | %foreign (ffi "get_array_uint16_t")
125 | prim__getArrayUInt16 : GCAnyPtr -> Bits64 -> Bits16
126 |
127 | %foreign (ffi "set_array_uint16_t")
128 | prim__setArrayUInt16 : GCAnyPtr -> Bits64 -> Bits16 -> PrimIO ()
129 |
130 | export
131 | ArrayType Bits16 where
132 |   elemSize = sizeofUInt16
133 |   get (MkArray arr _) idx = prim__getArrayUInt16 arr (cast idx)
134 |   set (MkArray arr _) idx x = primIO $ prim__setArrayUInt16 arr (cast idx) x
135 |
136 | %foreign (ffi "sizeof_uint32_t")
137 | sizeofUInt32 : Bits64
138 |
139 | %foreign (ffi "get_array_uint32_t")
140 | prim__getArrayUInt32 : GCAnyPtr -> Bits64 -> Bits32
141 |
142 | %foreign (ffi "set_array_uint32_t")
143 | prim__setArrayUInt32 : GCAnyPtr -> Bits64 -> Bits32 -> PrimIO ()
144 |
145 | export
146 | ArrayType Bits32 where
147 |   elemSize = sizeofUInt32
148 |   get (MkArray arr _) idx = prim__getArrayUInt32 arr (cast idx)
149 |   set (MkArray arr _) idx x = primIO $ prim__setArrayUInt32 arr (cast idx) x
150 |
151 | %foreign (ffi "sizeof_uint64_t")
152 | sizeofUInt64 : Bits64
153 |
154 | %foreign (ffi "get_array_uint64_t")
155 | prim__getArrayUInt64 : GCAnyPtr -> Bits64 -> Bits64
156 |
157 | %foreign (ffi "set_array_uint64_t")
158 | prim__setArrayUInt64 : GCAnyPtr -> Bits64 -> Bits64 -> PrimIO ()
159 |
160 | export
161 | ArrayType Bits64 where
162 |   elemSize = sizeofUInt64
163 |   get (MkArray arr _) idx = prim__getArrayUInt64 arr (cast idx)
164 |   set (MkArray arr _) idx x = primIO $ prim__setArrayUInt64 arr (cast idx) x
165 |
166 | %foreign (ffi "sizeof_double")
167 | sizeofDouble : Bits64
168 |
169 | %foreign (ffi "get_array_double")
170 | prim__getArrayDouble : GCAnyPtr -> Bits64 -> Double
171 |
172 | %foreign (ffi "set_array_double")
173 | prim__setArrayDouble : GCAnyPtr -> Bits64 -> Double -> PrimIO ()
174 |
175 | export
176 | ArrayType Double where
177 |   elemSize = sizeofDouble
178 |   get (MkArray arr _) idx = prim__getArrayDouble arr (cast idx)
179 |   set (MkArray arr _) idx x = primIO $ prim__setArrayDouble arr (cast idx) x
180 |
181 | %foreign (ffi "sizeof_bool")
182 | sizeofBool : Bits64
183 |
184 | %foreign (ffi "get_array_bool")
185 | prim__getArrayBool : GCAnyPtr -> Bits64 -> Int
186 |
187 | %foreign (ffi "set_array_bool")
188 | prim__setArrayBool : GCAnyPtr -> Bits64 -> Int -> PrimIO ()
189 |
190 | export
191 | ArrayType Bool where
192 |   elemSize = sizeofBool
193 |   get (MkArray arr _) idx = cIntToBool $ prim__getArrayBool arr (cast idx)
194 |   set (MkArray arr _) idx x = primIO $ prim__setArrayBool arr (cast idx) (boolToCInt x)
195 |
196 | ||| An uninitialized array. Contents may be anything.
197 | export
198 | mkArray : HasIO io => ArrayType a => Nat -> io (Array a)
199 | mkArray elemCount = do
200 |   let bytes : Bits64 = cast elemCount * elemSize {a}
201 |   arr <- malloc (cast bytes)
202 |   arr <- onCollectAny' arr free
203 |   pure $ MkArray arr (cast elemCount)
204 |
205 | export
206 | fromList : HasIO io => ArrayType a => List a -> io (Array a)
207 | fromList xs = do
208 |   arr <- mkArray (length xs)
209 |   traverse_ (\(idx, x) => set arr (cast idx) x) (enumerate xs)
210 |   pure arr
211 |
212 | export
213 | toList : ArrayType a => Array a -> List a
214 | toList arr@(MkArray _ len) = map (\i => get arr i) $ range (cast {to = Nat} len)
215 |