init: empty list #371
Assignees
Labels
Comments
|
I believe the code being transformed when the error occurs is in |
|
I suspect the problem here is that reduceFoldr 0 _ _ start _ = changed startto its definition will resolve the issue (although there may be a better way). |
|
I think you're right. I'll have a look this afternoon. |
|
Minimal example triggering bug: module Test4 where
import Clash.Explicit.Prelude
topEntity
:: Clock System Source
-> Reset System Synchronous
-> Signal System ()
topEntity clk rst =
delayBy clk rst (SNat @0) (pure ())
delayBy clk rst n =
foldr (.) id (replicate n id)
{-# NOINLINE delayBy #-} |
martijnbastiaan
added a commit
that referenced
this issue
Oct 8, 2018
martijnbastiaan
added
patch-provided
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
The following program causes the compiler to fail with an "empty list" error from
Data.List.init:{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE UndecidableInstances #-} module Test where import Clash.Sized.RTree as RTree import Clash.Prelude import Data.Functor.Compose import Data.Proxy import Data.Singletons.Prelude (type (@@), TyFun, Apply) import Data.Singletons.TypeLits (withKnownNat) import Data.Kind (Constraint, Type) import Debug.Trace {-# ANN test ((defSyn "test") { t_name = "test" , t_inputs = [ PortName "clock" , PortName "reset" , PortName "x" , PortName "y" ] , t_output = PortName "out" }) #-} test :: Clock System Source -> Reset System Synchronous -> Signal System (Unsigned N) -> Signal System (Unsigned N) -> Signal System (Unsigned N) test clk reset x y = withClockReset clk reset $ fmap fromIntegral $ mul' @4 @_ @4 x y main = do let ns = (,) <$> [100,200,300,400] <*> [0..10] print $ fmap (uncurry (*)) ns print $ simulate (uncurry (mul' @4 @16 @24) . unbundle) ns mul' :: forall chunkSz n m nChunks dom gated synth. (KnownNat chunkSz, KnownNat n, KnownNat m, KnownNat nChunks, HiddenClockReset dom gated synth, (2^m) ~ (chunkSz*nChunks), 1 <= nChunks, Obvious nChunks) => Signal dom (Unsigned (2^n)) -> Signal dom (Unsigned (2^m)) -> Signal dom (Unsigned (2^(n+m+1))) mul' x y = fmap fromIntegral $ delayBy (SNat @1) $ sumTree $ sequenceA $ fmap (vecToRTree 0) $ delayBy (SNat @2) res' where chunks :: Unsigned (2^m) -> Vec nChunks (Unsigned chunkSz) chunks n = bitChunks n chunkSz = fromIntegral $ natVal $ Proxy @chunkSz partial :: Unsigned (2^n) -> Index nChunks -> Unsigned chunkSz -> Unsigned (2^(n+chunkSz)) partial y i x = fromIntegral (y `mul` x) `shiftL` (chunkSz * fromIntegral i) res :: Signal dom (Vec nChunks (Unsigned (2^(n+chunkSz)))) res = zipWith3 partial <$> fmap pure x <*> pure indicesI <*> fmap chunks y res' :: Signal dom (Vec nChunks (Unsigned (2^(n+m+1)))) res' = fmap (fmap fromIntegral) res -- | Latency of @d@. sumTree :: forall d n dom synth gated. (KnownNat d, KnownNat n, HiddenClockReset dom synth gated) => RTree d (Signal dom (Unsigned n)) -> Signal dom (Unsigned (n+d)) sumTree rtree = tdfold (Proxy @(IAccum dom n)) id f rtree where f :: forall l. () => SNat l -> IAccum dom n @@ l -> IAccum dom n @@ l -> IAccum dom n @@ (l+1) f lvl@SNat l r = add <$> delayBy lvl l <*> delayBy lvl r data IAccum (dom :: Domain) (n :: Nat) (f :: TyFun Nat Type) :: Type type instance Apply (IAccum dom n) l = Signal dom (Unsigned (n+l)) vecToRTree :: forall n a. (KnownNat n, 1 <= n, Obvious n) => a -> Vec n a -> RTree (CLog 2 n) a vecToRTree z = v2t . pad where pad :: Vec n a -> Vec (2^(CLog 2 n)) a pad x = x ++ (repeat z :: Vec (2^(CLog 2 n) - n) a) type Obvious n = ((n <= 2^(CLog 2 n)) :: Constraint) bitChunks :: forall m n. (KnownNat m, KnownNat n) => Unsigned (m*n) -> Vec m (Unsigned n) bitChunks x = reverse $ fmap (\i -> fromIntegral $ x `shiftR` (fromIntegral i*n)) indicesI where n = fromIntegral $ natVal $ Proxy @n delayBy :: forall n dom a gated. (Undefined a, HiddenClock dom gated) => SNat n -> Signal dom a -> Signal dom a delayBy n = foldr (.) id (replicate n delay) naive :: HiddenClockReset dom gated synth => Signal dom (Unsigned 16) -> Signal dom (Unsigned 16) -> Signal dom (Unsigned 16) naive x y = delayBy (SNat @16) $ x*y type N = 16The error appears to come from
I added a bit of tracing to the call site with the following patch,
Which yielded the following,
The text was updated successfully, but these errors were encountered: