Skip to content

Instantly share code, notes, and snippets.

@christiaanb
Last active May 23, 2016 16:13
Show Gist options
  • Save christiaanb/8298743add74e5c566ecfca354ba6a76 to your computer and use it in GitHub Desktop.
Save christiaanb/8298743add74e5c566ecfca354ba6a76 to your computer and use it in GitHub Desktop.
-- NOINLINE means it is a primitive
{-# LANGUAGE DataKinds, KindSignatures, GADTs, PatternSynonyms,
GeneralizedNewtypeDeriving, ImplicitParams, RecordWildCards,
TypeOperators #-}
module Signal where
import Control.Applicative
import Data.Reflection (reifyNat)
import GHC.TypeLits
import Data.Maybe
import Unsafe.Coerce
data SSymbol :: Symbol -> * where
SSymbol :: KnownSymbol s => SSymbol s
data SNat :: Nat -> * where
SNat :: KnownNat n => SNat n
snatToInteger :: SNat n -> Integer
snatToInteger s@SNat = natVal s
snatProxy :: KnownNat n => proxy n -> SNat n
snatProxy = const SNat
addSNat :: SNat a -> SNat b -> SNat (a+b)
addSNat x y = reifyNat (snatToInteger x + snatToInteger y)
$ \p -> unsafeCoerce (snatProxy p)
mulSNat :: SNat a -> SNat b -> SNat (a*b)
mulSNat x y = reifyNat (snatToInteger x * snatToInteger y)
$ \p -> unsafeCoerce (snatProxy p)
divSNat :: SNat (a*b) -> SNat b -> SNat a
divSNat x y = reifyNat (snatToInteger x `div` snatToInteger y)
$ \p -> unsafeCoerce (snatProxy p)
data Clock = Clk Symbol Nat
data SClock (clk :: Clock) where
SClock :: { clkName :: SSymbol s
, clkRate :: SNat n
, clkEn :: Signal ('Clk s n) Bool
}
-> SClock ('Clk s n)
data ResKind = Sync | Async
data SResKind :: ResKind -> * where
SSync :: SResKind Sync
SAsync :: SResKind Async
data SReset (resKind :: ResKind) (clk :: Clock) where
SReset :: { resetKind :: SResKind resKind
, resetSignal :: Signal clk Bool
}
-> SReset resKind clk
data Signal (clk :: Clock) a = a :- Signal clk a
infixr 5 :-
newtype X a = X' { unX :: Maybe a }
deriving (Functor,Applicative)
pattern X :: X a
pattern X <- X' Nothing
where
X = X' Nothing
{-# NOINLINE toX #-}
toX :: a -> X a
toX = X' . Just
{-# NOINLINE fromX #-}
fromX :: X a -> a
fromX = fromJust . unX
instance Functor (Signal clk) where
fmap f (s :- ss) = f s :- fmap f ss
instance Applicative (Signal clk) where
pure x = let s = x :- s in s
(f :- fs) <*> ~(a :- as) = f a :- (fs <*> as)
{-# NOINLINE register' #-}
register' :: SReset resKind clk -> SClock clk -> a -> Signal clk a -> Signal clk a
register' (SReset SSync r) (SClock _ _ en) i d =
let q = reg q'
q' = mux en d' q
d' = mux (not <$> r) (pure i) d
in q
where
reg s = i :- s
register' (SReset SAsync _) (SClock _ _ en) i d =
let q = reg q'
q' = mux en d q
in q
where
reg s = i :- s
register :: (?clk :: SClock clk, ?reset :: SReset resKind clk) => a -> Signal clk a -> Signal clk a
register i d = register' ?reset ?clk i d
{-# NOINLINE delay' #-}
delay' :: SClock clk -> Signal clk a -> Signal clk (X a)
delay' clk = register' (SReset SAsync undefined) clk X . fmap toX
delay :: (?clk :: SClock clk) => Signal clk a -> Signal clk (X a)
delay = delay' ?clk
mux :: Applicative f => f Bool -> f a -> f a -> f a
mux = liftA3 (\b t f -> if b then t else f)
clockGate :: SClock clk -> Signal clk Bool -> SClock clk
clockGate (SClock {..}) en = SClock {clkEn = en, ..}
unsafeReclock :: Signal clk1 a -> Signal clk2 a
unsafeReclock = unsafeCoerce
{-# NOINLINE pll #-}
pll :: ((x * num) ~ (y * denom)) => SNat num
-> SNat denom
-> SClock ('Clk nm x)
-> (SClock ('Clk nm y), SReset Async ('Clk nm y))
pll num denom (SClock {clkRate = x, ..}) =
(SClock { clkRate = (x `mulSNat` num) `divSNat` denom
, clkEn = unsafeReclock clkEn
, ..
}
,SReset SAsync (pure True)
)
-- Should this be NOINLINE? I don't think so
resetSync :: SClock clk -> SReset Async clk -> SReset Async clk
resetSync clk sr@(SReset SAsync r) = SReset SAsync (register' sr clk False (register' sr clk False (pure True)))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment