Skip to content

Instantly share code, notes, and snippets.

@christiaanb
Created March 10, 2019 20:39
Show Gist options
  • Save christiaanb/8eac9bc72fc2bf44e9cce2a8499a4db8 to your computer and use it in GitHub Desktop.
Save christiaanb/8eac9bc72fc2bf44e9cce2a8499a4db8 to your computer and use it in GitHub Desktop.
{-# LANGUAGE ImplicitParams, RankNTypes, DataKinds,
TypeApplications, ScopedTypeVariables, KindSignatures,
ConstraintKinds, AllowAmbiguousTypes #-}
module NewHidden where
import qualified GHC.Classes
import GHC.TypeLits
import Unsafe.Coerce
type Hidden (x :: Symbol) a = GHC.Classes.IP x a
newtype Secret x a r = Secret (Hidden x a => r)
hide :: forall x a . Hidden x a => a
hide = GHC.Classes.ip @x
{-# INLINE hide #-}
{-# LANGUAGE DataKinds, TypeFamilies, FunctionalDependencies,
MultiParamTypeClasses, FlexibleInstances, GADTs,
ScopedTypeVariables, PolyKinds, TypeApplications,
MagicHash #-}
module NewSignal where
import GHC.TypeLits
data Signal (tag :: Symbol) a
= a :- Signal tag a
data ActiveFlank = Rising | Falling
data SActiveFlag (flank :: ActiveFlank) where
SRising :: SActiveFlag Rising
SFalling :: SActiveFlag Falling
data ResetKind = Asynchronous | Synchronous
data SResetKind (resetKind :: ResetKind) where
SAsynchronous :: SResetKind Asynchronous
SSynchronous :: SResetKind Synchronous
data ClockKind = Regular | Enabled
data SSymbol s where
SSymbol :: KnownSymbol s => SSymbol s
data SNat n where
SNat :: KnownNat n => SNat n
data DomainConfiguration
= Dom
{ tag :: Symbol
, period :: Nat
, flank :: ActiveFlank
, reset :: ResetKind
}
data SDomainConfiguration (conf :: DomainConfiguration) where
SDom :: SSymbol tag
-> SNat period
-> SActiveFlag flank
-> SResetKind reset
-> SDomainConfiguration (Dom tag period flank reset)
class KnownConfiguration (tag :: Symbol) (conf :: DomainConfiguration) | tag -> conf where
knownConfiguration :: SSymbol tag -> SDomainConfiguration conf
data Clock tag where
Clock :: SSymbol tag
-> Maybe (Signal tag Bool)
-> Clock tag
mkClock
:: SSymbol tag
-> Clock tag
mkClock tag = Clock tag Nothing
delay#
:: KnownConfiguration tag conf
=> Clock tag
-> a
-> Signal tag a
-> Signal tag a
delay# (Clock t Nothing) a s = case knownConfiguration t of
SDom {} -> a :- s
unsafeSynchronizer
:: KnownConfiguration tag1 conf1
=> KnownConfiguration tag2 conf2
=> Clock tag1
-> Clock tag2
-> Signal tag1 a
-> Signal tag2 a
unsafeSynchronizer = unsafeSynchronizer
{-# LANGUAGE ConstraintKinds, DataKinds, OverloadedLabels,
MagicHash, FlexibleContexts,
TypeApplications, ScopedTypeVariables, ImplicitParams,
KindSignatures, NoMonomorphismRestriction,
TypeSynonymInstances, FlexibleInstances,
MultiParamTypeClasses, MonoLocalBinds #-}
module NewTest where
import NewSignal
import NewHidden
import GHC.TypeLits
type HiddenClock (tag :: Symbol) (conf :: DomainConfiguration)
= (Hidden (AppendSymbol tag "_clk") (Clock tag), KnownConfiguration tag conf)
hideClock
:: forall tag conf r
. HiddenClock tag conf
=> (Clock tag -> r)
-> r
hideClock = \f -> f (hide @ (AppendSymbol tag "_clk"))
{-# INLINE hideClock #-}
delay = hideClock delay#
-- unsafeSynchronizerU
-- :: HiddenClock tag1 conf1
-- => HiddenClock tag2 conf2
-- => Signal tag1 a
-- -> Signal tag2 a
unsafeSynchronizerU = hideClock (hideClock unsafeSynchronizer)
type SystemConf = Dom "System" 10000 Rising Asynchronous
instance KnownConfiguration "System" SystemConf where
knownConfiguration _ =
SDom SSymbol SNat SRising SAsynchronous
delayM
:: HiddenClock "System" SystemConf
=> Bool
-> Signal "System" Bool
-> Signal "System" Bool
delayM = delay
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment