1 ------------------------------------------------------------------------------
3 -- Module : Data.Param.TFVec
4 -- Copyright : (c) 2009 Christiaan Baaij
5 -- Licence : BSD-style (see the file LICENCE)
7 -- Maintainer : christiaan.baaij@gmail.com
8 -- Stability : experimental
9 -- Portability : non-portable
11 -- 'TFVec': Fixed sized vectors. Vectors with numerically parameterized size,
12 -- using type-level numerals from 'tfp' library
14 ------------------------------------------------------------------------------
16 module Data.Param.TFVec
62 import Types.Data.Num.Decimal.Literals.TH
63 import Data.RangedWord
65 import Data.Generics (Data)
67 import qualified Prelude as P
68 import Prelude hiding (
69 null, length, head, tail, last, init, take, drop, (++), map, foldl, foldr,
70 zipWith, zip, unzip, concat, reverse, iterate )
71 import qualified Data.Foldable as DF (Foldable, foldr)
72 import qualified Data.Traversable as DT (Traversable(traverse))
73 import Language.Haskell.TH hiding (Pred)
74 import Language.Haskell.TH.Syntax (Lift(..))
76 import Language.Haskell.TH.TypeLib
78 newtype (NaturalT s) => TFVec s a = TFVec {unTFVec :: [a]}
79 deriving (Eq, Typeable)
81 deriving instance (NaturalT s, Typeable s, Data s, Typeable a, Data a) => Data (TFVec s a)
83 -- ==========================
84 -- = Constructing functions =
85 -- ==========================
90 (+>) :: a -> TFVec s a -> TFVec (Succ s) a
91 x +> (TFVec xs) = TFVec (x:xs)
95 singleton :: a -> TFVec D1 a
96 singleton x = x +> empty
98 vectorCPS :: [a] -> (forall s . NaturalT s => TFVec s a -> w) -> w
99 vectorCPS xs = unsafeVectorCPS (toInteger (P.length xs)) xs
101 -- FIXME: Not the most elegant solution... but it works for now in clash
102 vectorTH :: (Lift a, Typeable a) => [a] -> ExpQ
103 -- vectorTH xs = sigE [| (TFVec xs) |] (decTFVecT (toInteger (P.length xs)) xs)
104 vectorTH [] = [| empty |]
105 vectorTH [x] = [| singleton x |]
106 vectorTH (x:xs) = [| x +> $(vectorTH xs) |]
108 unsafeVector :: NaturalT s => s -> [a] -> TFVec s a
110 | fromIntegerT l /= P.length xs =
111 error (show 'unsafeVector P.++ ": dynamic/static lenght mismatch")
112 | otherwise = TFVec xs
114 readTFVec :: (Read a, NaturalT s) => String -> TFVec s a
117 readTFVecCPS :: Read a => String -> (forall s . NaturalT s => TFVec s a -> w) -> w
118 readTFVecCPS str = unsafeVectorCPS (toInteger l) xs
119 where fName = show 'readTFVecCPS
120 (xs,l) = case [(xs,l) | (xs,l,rest) <- readTFVecList str,
121 ("","") <- lexTFVec rest] of
123 [] -> error (fName P.++ ": no parse")
124 _ -> error (fName P.++ ": ambiguous parse")
126 -- =======================
127 -- = Observing functions =
128 -- =======================
129 length :: forall s a . NaturalT s => TFVec s a -> Int
130 length _ = fromIntegerT (undefined :: s)
132 lengthT :: NaturalT s => TFVec s a -> s
135 fromVector :: NaturalT s => TFVec s a -> [a]
136 fromVector (TFVec xs) = xs
138 null :: TFVec D0 a -> Bool
143 , (s :>: u) ~ True) => TFVec s a -> RangedWord u -> a
144 (TFVec xs) ! i = xs !! (fromInteger (toInteger i))
146 -- ==========================
147 -- = Transforming functions =
148 -- ==========================
149 replace :: (PositiveT s, NaturalT u, (s :>: u) ~ True) =>
150 TFVec s a -> RangedWord u -> a -> TFVec s a
151 replace (TFVec xs) i y = TFVec $ replace' xs (toInteger i) y
152 where replace' [] _ _ = []
153 replace' (_:xs) 0 y = (y:xs)
154 replace' (x:xs) n y = x : (replace' xs (n-1) y)
156 head :: PositiveT s => TFVec s a -> a
157 head = P.head . unTFVec
159 tail :: PositiveT s => TFVec s a -> TFVec (Pred s) a
162 last :: PositiveT s => TFVec s a -> a
163 last = P.last . unTFVec
165 init :: PositiveT s => TFVec s a -> TFVec (Pred s) a
168 take :: NaturalT i => i -> TFVec s a -> TFVec (Min s i) a
169 take i = liftV $ P.take (fromIntegerT i)
171 drop :: NaturalT i => i -> TFVec s a -> TFVec (s :-: (Min s i)) a
172 drop i = liftV $ P.drop (fromIntegerT i)
174 select :: (NaturalT f, NaturalT s, NaturalT n, (f :<: i) ~ True,
175 (((s :*: n) :+: f) :<=: i) ~ True) =>
176 f -> s -> n -> TFVec i a -> TFVec n a
177 select f s n = liftV (select' f' s' n')
178 where (f', s', n') = (fromIntegerT f, fromIntegerT s, fromIntegerT n)
179 select' f s n = ((selectFirst0 s n).(P.drop f))
180 selectFirst0 :: Int -> Int -> [a] -> [a]
181 selectFirst0 s n l@(x:_)
182 | n > 0 = x : selectFirst0 s (n-1) (P.drop s l)
184 selectFirst0 _ 0 [] = []
186 (<+) :: TFVec s a -> a -> TFVec (Succ s) a
187 (<+) (TFVec xs) x = TFVec (xs P.++ [x])
189 (++) :: TFVec s a -> TFVec s2 a -> TFVec (s :+: s2) a
195 map :: (a -> b) -> TFVec s a -> TFVec s b
196 map f = liftV (P.map f)
198 zipWith :: (a -> b -> c) -> TFVec s a -> TFVec s b -> TFVec s c
199 zipWith f = liftV2 (P.zipWith f)
201 foldl :: (a -> b -> a) -> a -> TFVec s b -> a
202 foldl f e = (P.foldl f e) . unTFVec
204 foldr :: (b -> a -> a) -> a -> TFVec s b -> a
205 foldr f e = (P.foldr f e) . unTFVec
207 zip :: TFVec s a -> TFVec s b -> TFVec s (a, b)
210 unzip :: TFVec s (a, b) -> (TFVec s a, TFVec s b)
211 unzip (TFVec xs) = let (a,b) = P.unzip xs in (TFVec a, TFVec b)
213 shiftl :: (PositiveT s, NaturalT n, n ~ Pred s, s ~ Succ n) =>
214 TFVec s a -> a -> TFVec s a
215 shiftl xs x = x +> init xs
217 shiftr :: (PositiveT s, NaturalT n, n ~ Pred s, s ~ Succ n) =>
218 TFVec s a -> a -> TFVec s a
219 shiftr xs x = tail xs <+ x
221 rotl :: forall s a . NaturalT s => TFVec s a -> TFVec s a
223 where vlen = fromIntegerT (undefined :: s)
225 rotl' xs = let (i,[l]) = splitAt (vlen - 1) xs
228 rotr :: NaturalT s => TFVec s a -> TFVec s a
232 rotr' (x:xs) = xs P.++ [x]
234 concat :: TFVec s1 (TFVec s2 a) -> TFVec (s1 :*: s2) a
235 concat = liftV (P.foldr ((P.++).unTFVec) [])
237 reverse :: TFVec s a -> TFVec s a
238 reverse = liftV P.reverse
240 iterate :: NaturalT s => (a -> a) -> a -> TFVec s a
241 iterate = iteraten (undefined :: s)
243 iteraten :: NaturalT s => s -> (a -> a) -> a -> TFVec s a
244 iteraten s f x = let s' = fromIntegerT s in TFVec (P.take s' $ P.iterate f x)
246 generate :: NaturalT s => (a -> a) -> a -> TFVec s a
247 generate = generaten (undefined :: s)
249 generaten :: NaturalT s => s -> (a -> a) -> a -> TFVec s a
250 generaten s f x = let s' = fromIntegerT s in TFVec (P.take s' $ P.tail $ P.iterate f x)
252 copy :: NaturalT s => a -> TFVec s a
253 copy x = copyn (undefined :: s) x
255 copyn :: NaturalT s => s -> a -> TFVec s a
256 copyn s x = iteraten s id x
261 instance Show a => Show (TFVec s a) where
262 showsPrec _ = showV.unTFVec
263 where showV [] = showString "<>"
264 showV (x:xs) = showChar '<' . shows x . showl xs
265 where showl [] = showChar '>'
266 showl (x:xs) = showChar ',' . shows x .
269 instance (Read a, NaturalT nT) => Read (TFVec nT a) where
271 | all fitsLength possibilities = P.map toReadS possibilities
272 | otherwise = error (fName P.++ ": string/dynamic length mismatch")
274 fName = "Data.Param.TFVec.read"
275 expectedL = fromIntegerT (undefined :: nT)
276 possibilities = readTFVecList str
277 fitsLength (_, l, _) = l == expectedL
278 toReadS (xs, _, rest) = (TFVec xs, rest)
280 instance NaturalT s => DF.Foldable (TFVec s) where
283 instance NaturalT s => Functor (TFVec s) where
286 instance NaturalT s => DT.Traversable (TFVec s) where
287 traverse f = (fmap TFVec).(DT.traverse f).unTFVec
289 -- instance (Lift a, NaturalT nT) => Lift (TFVec nT a) where
290 -- lift (TFVec xs) = [| unsafeTFVecCoerse
291 -- $(decLiteralV (fromIntegerT (undefined :: nT)))
294 instance (Lift a, Typeable a, NaturalT nT) => Lift (TFVec nT a) where
295 lift (TFVec xs) = sigE [| (TFVec xs) |] (decTFVecT (fromIntegerT (undefined :: nT)) xs)
297 decTFVecT :: Typeable x => Integer -> x -> Q Type
298 decTFVecT n a = appT (appT (conT (''TFVec)) (decLiteralT n)) elemT
300 (con,reps) = splitTyConApp (typeOf a)
301 elemT = typeRep2Type (P.head reps)
304 -- ======================
305 -- = Internal Functions =
306 -- ======================
307 liftV :: ([a] -> [b]) -> TFVec nT a -> TFVec nT' b
308 liftV f = TFVec . f . unTFVec
310 liftV2 :: ([a] -> [b] -> [c]) -> TFVec s a -> TFVec s2 b -> TFVec s3 c
311 liftV2 f a b = TFVec (f (unTFVec a) (unTFVec b))
313 splitAtM :: Int -> [a] -> Maybe ([a],[a])
314 splitAtM n xs = splitAtM' n [] xs
315 where splitAtM' 0 xs ys = Just (xs, ys)
316 splitAtM' n xs (y:ys) | n > 0 = do
317 (ls, rs) <- splitAtM' (n-1) xs ys
319 splitAtM' _ _ _ = Nothing
321 unsafeTFVecCoerse :: nT' -> TFVec nT a -> TFVec nT' a
322 unsafeTFVecCoerse _ (TFVec v) = (TFVec v)
324 unsafeVectorCPS :: forall a w . Integer -> [a] ->
325 (forall s . NaturalT s => TFVec s a -> w) -> w
326 unsafeVectorCPS l xs f = reifyNaturalD l
327 (\(_ :: lt) -> f ((TFVec xs) :: (TFVec lt a)))
329 readTFVecList :: Read a => String -> [([a], Int, String)]
330 readTFVecList = readParen' False (\r -> [pr | ("<",s) <- lexTFVec r,
333 readl s = [([],0,t) | (">",t) <- lexTFVec s] P.++
334 [(x:xs,1+n,u) | (x,t) <- reads s,
335 (xs, n, u) <- readl' t]
336 readl' s = [([],0,t) | (">",t) <- lexTFVec s] P.++
337 [(x:xs,1+n,v) | (",",t) <- lex s,
339 (xs,n,v) <- readl' u]
340 readParen' b g = if b then mandatory else optional
341 where optional r = g r P.++ mandatory r
342 mandatory r = [(x,n,u) | ("(",s) <- lexTFVec r,
343 (x,n,t) <- optional s,
344 (")",u) <- lexTFVec t]
346 -- Custom lexer for FSVecs, we cannot use lex directly because it considers
347 -- sequences of < and > as unique lexemes, and that breaks nested FSVecs, e.g.
349 lexTFVec :: ReadS String
350 lexTFVec ('>':rest) = [(">",rest)]
351 lexTFVec ('<':rest) = [("<",rest)]
352 lexTFVec str = lex str