Created
February 9, 2020 13:09
-
-
Save TheZoq2/d17a4c37f160b5cf8a3ea08d0406c6d1 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
```haskell | |
{-# LANGUAGE ExplicitForAll #-} | |
{-# LANGUAGE ScopedTypeVariables #-} | |
{-# LANGUAGE StarIsType #-} | |
import Clash.Prelude | |
-- import Data.Singletons.Prelude | |
import Data.Singletons (TyFun, Apply) | |
import Data.Proxy | |
import Data.Kind | |
-- Helper function to remove one bit | |
truncate1 :: KnownNat x => Unsigned (x+1) -> Unsigned x | |
truncate1 input = truncateB input | |
data TypeGen (x :: Nat) (n :: Nat) (f :: TyFun Nat *) :: * | |
type instance Apply (TypeGen x n) l = | |
Unsigned (x-l) | |
stage :: KnownNat x | |
=> 1 <= x | |
=> () | |
-> Unsigned x | |
-> Unsigned (x-1) | |
stage _ input = | |
truncate1 input | |
pl :: forall x n | |
. KnownNat x | |
=> KnownNat n | |
=> 1 <= x | |
=> (1+n) <= x | |
=> Unsigned x | |
-> Unsigned (x-n) | |
pl input = | |
dfold | |
(Proxy :: Proxy (TypeGen x d)) | |
go | |
input | |
(repeat ()) | |
where | |
go :: forall l x. SystemClockResetEnable | |
=> KnownNat x | |
=> 1 <= x | |
-- I think this is needed because (x-(l+1)) can not be negative | |
=> (1+l) <= x | |
-- Number of previous folds | |
=> SNat l | |
-- Input to each element in the circuit | |
-> () | |
-- Input from previous element | |
-> Unsigned (x-l) | |
-- Output from this element | |
-> Unsigned (x-(l+1)) | |
go (l@SNat) allInputs prevStage = | |
stage allInputs prevStage | |
``` |
Author
TheZoq2
commented
Feb 9, 2020
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment