NewHidden.hs

{-# 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 #-}

NewSignal.hs

{-# 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

NewTest.hs

{-# 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