1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
|
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ConstraintKinds #-}
module Basement.Sized.Vect
( Vect
, MVect
, unVect
, toVect
, empty
, singleton
, replicate
, thaw
, freeze
, index
, map
, foldl'
, foldr
, cons
, snoc
, elem
, sub
, uncons
, unsnoc
, splitAt
, all
, any
, find
, reverse
, sortBy
, intersperse
) where
import Basement.Compat.Base
import Basement.Nat
import Basement.NormalForm
import Basement.Types.OffsetSize
import Basement.Monad
import Basement.PrimType (PrimType)
import qualified Basement.BoxedArray as A
--import qualified Basement.BoxedArray.Mutable as A hiding (sub)
import Data.Proxy
newtype Vect (n :: Nat) a = Vect { unVect :: A.Array a } deriving (NormalForm, Eq, Show)
newtype MVect (n :: Nat) ty st = MVect { unMVect :: A.MArray ty st }
instance Functor (Vect n) where
fmap = map
toVect :: forall n ty . (KnownNat n, Countable ty n) => A.Array ty -> Maybe (Vect n ty)
toVect b
| expected == A.length b = Just (Vect b)
| otherwise = Nothing
where
expected = toCount @n
empty :: Vect 0 ty
empty = Vect A.empty
singleton :: ty -> Vect 1 ty
singleton a = Vect (A.singleton a)
create :: forall a (n :: Nat) . (Countable a n, KnownNat n) => (Offset a -> a) -> Vect n a
create f = Vect $ A.create sz f
where
sz = natValCountOf (Proxy :: Proxy n)
replicate :: forall n ty . (KnownNat n, Countable ty n) => ty -> Vect n ty
replicate a = Vect (A.replicate (toCount @n) a)
thaw :: (KnownNat n, PrimMonad prim) => Vect n ty -> prim (MVect n ty (PrimState prim))
thaw b = MVect <$> A.thaw (unVect b)
freeze :: (PrimMonad prim, Countable ty n) => MVect n ty (PrimState prim) -> prim (Vect n ty)
freeze b = Vect <$> A.freeze (unMVect b)
write :: PrimMonad prim => MVect n ty (PrimState prim) -> Offset ty -> ty -> prim ()
write (MVect ma) ofs v = A.write ma ofs v
read :: PrimMonad prim => MVect n ty (PrimState prim) -> Offset ty -> prim ty
read (MVect ma) ofs = A.read ma ofs
indexStatic :: forall i n ty . (KnownNat i, CmpNat i n ~ 'LT, Offsetable ty i) => Vect n ty -> ty
indexStatic b = A.unsafeIndex (unVect b) (toOffset @i)
index :: Vect n ty -> Offset ty -> ty
index b ofs = A.index (unVect b) ofs
map :: (a -> b) -> Vect n a -> Vect n b
map f b = Vect (fmap f (unVect b))
foldl' :: (a -> ty -> a) -> a -> Vect n ty -> a
foldl' f acc b = A.foldl' f acc (unVect b)
foldr :: (ty -> a -> a) -> a -> Vect n ty -> a
foldr f acc b = A.foldr f acc (unVect b)
cons :: ty -> Vect n ty -> Vect (n+1) ty
cons e = Vect . A.cons e . unVect
snoc :: Vect n ty -> ty -> Vect (n+1) ty
snoc b = Vect . A.snoc (unVect b)
sub :: forall i j n ty
. ( (i <=? n) ~ 'True
, (j <=? n) ~ 'True
, (i <=? j) ~ 'True
, KnownNat i
, KnownNat j
, Offsetable ty i
, Offsetable ty j )
=> Vect n ty
-> Vect (j-i) ty
sub block = Vect (A.sub (unVect block) (toOffset @i) (toOffset @j))
uncons :: forall n ty . (CmpNat 0 n ~ 'LT, KnownNat n, Offsetable ty n)
=> Vect n ty
-> (ty, Vect (n-1) ty)
uncons b = (indexStatic @0 b, Vect (A.sub (unVect b) 1 (toOffset @n)))
unsnoc :: forall n ty . (CmpNat 0 n ~ 'LT, KnownNat n, Offsetable ty n)
=> Vect n ty
-> (Vect (n-1) ty, ty)
unsnoc b =
( Vect (A.sub (unVect b) 0 (toOffset @n `offsetSub` 1))
, A.unsafeIndex (unVect b) (toOffset @n `offsetSub` 1))
splitAt :: forall i n ty . (CmpNat i n ~ 'LT, KnownNat i, Countable ty i) => Vect n ty -> (Vect i ty, Vect (n-i) ty)
splitAt b =
let (left, right) = A.splitAt (toCount @i) (unVect b)
in (Vect left, Vect right)
elem :: Eq ty => ty -> Vect n ty -> Bool
elem e b = A.elem e (unVect b)
all :: (ty -> Bool) -> Vect n ty -> Bool
all p b = A.all p (unVect b)
any :: (ty -> Bool) -> Vect n ty -> Bool
any p b = A.any p (unVect b)
find :: (ty -> Bool) -> Vect n ty -> Maybe ty
find p b = A.find p (unVect b)
reverse :: Vect n ty -> Vect n ty
reverse = Vect . A.reverse . unVect
sortBy :: (ty -> ty -> Ordering) -> Vect n ty -> Vect n ty
sortBy f b = Vect (A.sortBy f (unVect b))
intersperse :: (CmpNat n 1 ~ 'GT) => ty -> Vect n ty -> Vect (n+n-1) ty
intersperse sep b = Vect (A.intersperse sep (unVect b))
toCount :: forall n ty . (KnownNat n, Countable ty n) => CountOf ty
toCount = natValCountOf (Proxy @n)
toOffset :: forall n ty . (KnownNat n, Offsetable ty n) => Offset ty
toOffset = natValOffset (Proxy @n)
|
