Signal.hs

-- 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)))