23 | import Control.Monad.Either
24 | import Decidable.Equality
43 | Ix n = Subset Bits32 $
\ix => ix < n = True
47 | len32 : List a -> Bits32
48 | len32 = fromInteger . natToInteger . length
53 | zipWithIndex : (as : List a) -> List (Ix $
len32 as, a)
54 | zipWithIndex as = run [] 0 as
57 | run : List (Ix $
len32 as, a) -> Bits32 -> List a -> List (Ix $
len32 as, a)
58 | run acc _ [] = reverse acc
59 | run acc n (x :: xs) =
60 | run ((Element n $
believe_me (Refl {x}), x) :: acc) (n+1) xs
65 | toIx : (size : Bits32) -> Bits32 -> Maybe (Ix size)
66 | toIx size x = case decEq (x < size) True of
67 | Yes prf => Just $
Element x prf
75 | data Array : Type -> Type where [external]
84 | %foreign "javascript:lambda:(u,x) => x.length"
85 | prim__sizeIO : forall arr . arr -> PrimIO Bits32
88 | %foreign "javascript:lambda:(u,v,arr,n) => arr[n]"
89 | prim__readIO : forall a,arr . arr -> Bits32 -> PrimIO (UndefOr a)
92 | %foreign "javascript:lambda:(u,x) => x.length"
93 | prim__size : forall arr . arr -> Bits32
96 | %foreign "javascript:lambda:(u,v,arr,n) => arr[n]"
97 | prim__read : forall a,arr . arr -> Bits32 -> a
100 | %foreign "javascript:lambda:(u,arr,n,v) => { arr[n] = v }"
101 | prim__writeIO : forall a . Array a -> Bits32 -> a -> PrimIO ()
104 | %foreign "javascript:lambda:(u,n) => { return new Array(n) }"
105 | prim__newArrayIO : forall a . Bits32 -> PrimIO (Array a)
108 | %foreign "javascript:lambda:x => Array.isArray(x)?1:0"
109 | prim__isArray : AnyPtr -> Bool
112 | %foreign "javascript:lambda:(_arr,_a,x) => Array.from(x)"
113 | prim__fromArrayLikeIO : forall a,arr . arr -> PrimIO (Array a)
138 | interface ArrayLike (0 arr : Type) (0 el : Type) | arr where
141 | sizeIO : (HasIO io, ArrayLike arr el) => arr -> io Bits32
142 | sizeIO v = fromInteger . cast <$> primIO (prim__sizeIO v)
145 | readIO : (HasIO io, ArrayLike arr e) => arr -> Bits32 -> io (Maybe e)
146 | readIO v ix = undeforToMaybe <$> (primIO . prim__readIO v $
toFFI ix)
149 | ArrayLike String Char where
152 | ArrayLike (Array a) a where
154 | export ArrayLike UInt8ClampedArray Bits8 where
155 | export ArrayLike UInt8Array Bits8 where
156 | export ArrayLike UInt16Array Bits16 where
157 | export ArrayLike UInt32Array Bits32 where
158 | export ArrayLike Int8Array Int8 where
159 | export ArrayLike Int16Array Int16 where
160 | export ArrayLike Int32Array Int32 where
161 | export ArrayLike Float64Array Double where
169 | interface ArrayLike arr el => IArrayLike arr el | arr where
172 | size : IArrayLike arr el => arr -> Bits32
173 | size arr = fromInteger . cast $
prim__size arr
176 | read : IArrayLike arr el
177 | => (elems : arr) -> (ix : Ix $
size elems) -> el
178 | read elems (Element ix _) = prim__read elems $
toFFI ix
181 | readMaybe : IArrayLike arr el
182 | => (elems : arr) -> Bits32 -> Maybe el
183 | readMaybe elems = map (read elems) . toIx (size elems)
188 | sameElements : (IArrayLike arr el, Eq el) => arr -> arr -> Bool
189 | sameElements a1 a2 =
190 | case decEq (size a2) (size a1) of
191 | Yes prf => run prf 0
195 | run : (0 _ : size a2 = size a1) -> Bits32 -> Bool
197 | case decEq (ix < size a1) True of
200 | read a1 (Element ix prf) ==
201 | read a2 (Element ix (rewrite refl in prf)) &&
202 | run refl (assert_smaller ix $
ix+1)
206 | IArrayLike arr el => (acc -> el -> acc) -> acc -> arr -> acc
207 | foldlArray f ini arr = run 0 ini
210 | run : Bits32 -> acc -> acc
211 | run n res = case readMaybe arr n of
212 | Just el => run (assert_smaller n $
n+1) (f res el)
217 | IArrayLike arr el => (el -> acc -> acc) -> acc -> arr -> acc
218 | foldrArray f ini arr = run 0
220 | run : Bits32 -> acc
221 | run n = case readMaybe arr n of
222 | Just el => f el $
run (assert_smaller n $
n+1)
226 | arrayToList : IArrayLike arr el => arr -> List el
227 | arrayToList = foldrArray (::) Nil
230 | IArrayLike String Char where
237 | ToFFI (Array a) (Array a) where toFFI = id
240 | FromFFI (Array a) (Array a) where fromFFI = Just
243 | isArray : anyVal -> Bool
244 | isArray v = prim__isArray (toFFI $
MkAny v)
247 | writeIO : HasIO io => Array a -> Bits32 -> a -> io ()
248 | writeIO arr ix v = primIO $
prim__writeIO arr (toFFI ix) v
251 | newArrayIO : HasIO io => Bits32 -> io (Array a)
252 | newArrayIO n = primIO $
prim__newArrayIO (toFFI n)
255 | arrayDataFrom : (HasIO io, ArrayLike arr e) => arr -> io (Array e)
256 | arrayDataFrom arr = primIO $
prim__fromArrayLikeIO arr
263 | fromListIO : HasIO io => List a -> io (Array a)
265 | let len := the Bits32 (fromInteger . natToInteger $
length as)
266 | in newArrayIO len >>= fill 0 as
269 | fill : Bits32 -> List a -> Array a -> io (Array a)
270 | fill _ [] arr = pure arr
271 | fill n (x :: xs) arr = do
276 | fromFoldableIO : (HasIO io, Foldable t) => t a -> io (Array a)
277 | fromFoldableIO = fromListIO . toList
280 | ToFFI a b => ToFFI (List a) (IO $
Array b)
281 | where toFFI = fromListIO . map toFFI
287 | %foreign "javascript:lambda:(u,arr,n,v) => { arr[n] = v; return arr }"
288 | prim__write : forall a . Array a -> Bits32 -> a -> Array a
290 | %foreign "javascript:lambda:(u,n,a) => { var res = new Array(n); return res.fill(a) }"
291 | prim__newArray : forall a . Bits32 -> a -> Array a
293 | %foreign "javascript:lambda:(u,n) => { return new Array(n) }"
294 | prim__undefArray : forall a . Bits32 -> Array a
296 | %foreign "javascript:lambda:u => { return = new Array(0) }"
297 | prim__emptyArray : forall a . Array a
299 | %foreign "javascript:lambda:(u,x,v) => Array.from(v)"
300 | prim__fromArray : forall arr . arr -> Array a
304 | record LinArray (sze : Bits32) (a : Type) where
305 | constructor MkLinArray
309 | thaw : (1 _ : LinArray sze a) -> IO (Array a)
310 | thaw (MkLinArray arr) = pure arr
316 | undefArray : (sze : Bits32) -> (1 _ : (1 _ : LinArray sze a) -> b) -> b
317 | undefArray sze f = f (MkLinArray $
prim__undefArray (toFFI sze))
320 | unsafeWrite : (1 _ : LinArray sze a) -> (n : Bits32) -> a -> LinArray sze a
321 | unsafeWrite (MkLinArray arr) n v = MkLinArray $
prim__write arr (toFFI n) v
324 | emptyArray : (1 _ : (1 _ : LinArray 0 a) -> b) -> b
325 | emptyArray f = f (MkLinArray $
prim__emptyArray)
331 | -> (1 _ : (1 _ : LinArray sze a) -> b)
333 | newArray v sze f = f (MkLinArray $
prim__newArray (toFFI sze) v)
337 | {auto _ : IArrayLike arr el}
339 | -> (1 _ : (1 _ : LinArray (size v) el) -> a)
341 | withArray array f = f (MkLinArray $
prim__fromArray array)
344 | write : (1 _ : LinArray sze a) -> (ix : Ix sze) -> a -> LinArray sze a
345 | write arr (Element n _) = unsafeWrite arr n
349 | (1 _ : LinArray sze a)
351 | -> Res a (const $
LinArray sze a)
352 | lread (MkLinArray arr) (Element ix _) =
353 | prim__read arr (toFFI ix) # MkLinArray arr
356 | lsize : (1 _ : LinArray sze a) -> Res Bits32 (\s => LinArray s a)
357 | lsize (MkLinArray arr) = fromInteger (cast $
prim__size arr) # MkLinArray arr
363 | -> ((1 _ : LinArray sze a) -> b)
365 | iterate' sze f g = undefArray sze (run 0)
368 | run : Bits32 -> (1 _ : LinArray sze a) -> b
369 | run n arr = case toIx sze n of
371 | Just ix => run (assert_smaller n $
n+1) (write arr ix (f ix))
374 | fromList' : (as : List a) -> ((1 _ : LinArray (len32 as) a) -> b) -> b
375 | fromList' as f = undefArray (len32 as) (run $
zipWithIndex as)
378 | run : List (Ix $
len32 as, a) -> (1 _ : LinArray (len32 as) a) -> b
379 | run [] linA = f linA
380 | run ((ix,a) :: t) linA = run t (write linA ix a)
384 | {auto _ : IArrayLike arr a}
386 | -> ((1 _ : LinArray (size vs) b) -> c)
389 | map' vs fromArr f = iterate' (size vs) (\ix => f (read vs ix)) fromArr
393 | (IArrayLike arr1 arr2, IArrayLike arr2 el) => arr1 -> Bits32
394 | totalSize = foldlArray (\n,vs => n + size vs) 0
400 | {auto _ : IArrayLike arr1 arr2}
401 | -> {auto _ : IArrayLike arr2 el}
403 | -> ((1 _ : LinArray (totalSize {arr2} vss) el) -> a)
405 | join' vss f = undefArray (totalSize {arr2} vss) (outer 0 0)
412 | -> (1 _ : LinArray (totalSize {arr2} vss) el)
413 | -> LinArray (totalSize {arr2} vss) el
414 | inner n pos as la =
415 | case readMaybe as n of
416 | Just v => inner (assert_smaller n $
n+1) pos as (unsafeWrite la (pos + n) v)
422 | -> (1 _ : LinArray (totalSize {arr2} vss) el)
425 | case readMaybe vss n of
426 | Just v => outer (assert_smaller n $
n+1) (pos + size v) (inner 0 pos v la)
439 | record IArray (a : Type) where
440 | constructor MkIArray
444 | freezeCloneIO : (HasIO io, ArrayLike arr el) => arr -> io (IArray el)
445 | freezeCloneIO xs = MkIArray <$> primIO (prim__fromArrayLikeIO xs)
448 | freeze : forall sze,a . (1 _ : LinArray sze a) -> IArray a
449 | freeze (MkLinArray arr) = MkIArray arr
452 | fromList : List a -> IArray a
453 | fromList as = fromList' as freeze
456 | singleton : a -> IArray a
457 | singleton = fromList . pure
460 | ArrayLike (IArray a) a where
463 | IArrayLike (IArray a) a where
466 | concat : IArray (IArray a) -> IArray a
467 | concat as = join' {arr2 = IArray a} as freeze
470 | Eq el => Eq (IArray el) where
471 | (==) = sameElements {el}
474 | Show a => Show (IArray a) where
475 | showPrec p v = showCon p "fromList " (show $
arrayToList v)
478 | Semigroup (IArray a) where
479 | a1 <+> a2 = concat $
fromList [a1,a2]
482 | Monoid (IArray a) where
483 | neutral = fromList []
486 | Functor IArray where
487 | map f as = map' as freeze f
490 | Applicative IArray where
492 | fs <*> as = concat $
map (\f => map (apply f) as) fs
499 | Foldable IArray where
502 | null arr = size arr == 0
508 | Traversable IArray where
509 | traverse f arr = fromList <$> traverse f (toList arr)
512 | Alternative IArray where
513 | empty = fromList []
514 | as <|> bs = if null as then bs else as
517 | FromString (IArray Char) where
518 | fromString s = withArray s freeze