{-# LANGUAGE AllowAmbiguousTypes #-}

-- | Synchronous digital circuits. The tensor preserves the grouping of bit bundles; copying is
-- fan-out, and tracing connects wires without adding a delay. 'register' delays a bit by one
-- clock cycle. 'prepare' rejects observable combinational cycles before simulation.
--
-- >>> simulate notGate [False, True]
-- Right [True,False]
-- >>> simulate (register False) [True, False, True]
-- Right [False,True,False]
module Proarrow.Category.Instance.Circuit
  ( Wires (..)
  , KnownWires
  , Value
  , Sample
  , PREPARED (..)
  , Prepared
  , Circuit
  , constant
  , notGate
  , andGate
  , orGate
  , xorGate
  , mux
  , register
  , Netlist
  , netlist
  , renderNetlist
  , toDot
  , toVerilog
  , CircuitError (..)
  , Simulator
  , prepare
  , step
  , simulate
  ) where

import Control.Monad ((>=>))
import Data.Graph (SCC (..), stronglyConnComp)
import Data.IntMap.Strict qualified as IM
import Data.IntSet qualified as IS
import Data.Kind (Constraint, Type)
import Data.List qualified as List
import Prelude hiding (Functor, fmap, id, (**), (.))
import Prelude qualified as P

import Proarrow.Category.Instance.Simulator (SIMULATOR (..), Simulator (..), runSimulator, step)
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..), Tensor)
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard)
import Proarrow.Category.Monoidal.Strength (Costrong (..))
import Proarrow.Core (CAT, CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault, type (+->))
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Monoid (CocommutativeComonoid, Comonoid (..))
import Proarrow.Profunctor.Representable (Rep (..))

-- | A bit, no wires, or two bundles. Tensor grouping is retained in the type.
type data Wires = Bit | Empty | Pair Wires Wires

type Shape :: Wires -> Type
data Shape a where
  BitS :: Shape Bit
  EmptyS :: Shape Empty
  PairS :: Shape a -> Shape b -> Shape (Pair a b)

type KnownWires :: Wires -> Constraint
class (Is Sim (Value @ Ready a)) => KnownWires a where
  shape :: Shape a
instance KnownWires Bit where shape :: Shape Bit
shape = Shape Bit
BitS
instance KnownWires Empty where shape :: Shape Empty
shape = Shape Empty
EmptyS
instance (KnownWires a, KnownWires b) => KnownWires (Pair a b) where shape :: Shape (Pair a b)
shape = Shape a -> Shape b -> Shape (Pair a b)
forall (a :: Wires) (b :: Wires).
Shape a -> Shape b -> Shape (Pair a b)
PairS (forall (a :: Wires). KnownWires a => Shape a
shape @a) (forall (a :: Wires). KnownWires a => Shape a
shape @b)

-- | Objects of validated circuits, with the same wire shapes as 'Wires'.
type data PREPARED = Ready Wires

-- | Interpret validated circuits as state machines. Bits become 'Bool', the unit becomes @()@,
-- and a tensor becomes a pair, all in the 'SIMULATOR' category.
data family Value :: PREPARED +-> SIMULATOR

-- | The Haskell value for one clock cycle at a wire shape.
type Sample :: Wires -> Type
type Sample a = UN Sim (Value @ Ready a)

type Bundle :: Wires -> Type
data Bundle a where
  BBit :: Int -> Bundle Bit
  BEmpty :: Bundle Empty
  BPair :: Bundle a -> Bundle b -> Bundle (Pair a b)

ports :: Bundle a -> [Int]
ports :: forall (a :: Wires). Bundle a -> [Int]
ports Bundle a
bundle = Bundle a -> [Int] -> [Int]
forall (b :: Wires). Bundle b -> [Int] -> [Int]
go Bundle a
bundle []
  where
    go :: Bundle b -> [Int] -> [Int]
    go :: forall (b :: Wires). Bundle b -> [Int] -> [Int]
go (BBit Int
n) [Int]
rest = Int
n Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
rest
    go Bundle b
BEmpty [Int]
rest = [Int]
rest
    go (BPair Bundle a
a Bundle b
b) [Int]
rest = Bundle a -> [Int] -> [Int]
forall (b :: Wires). Bundle b -> [Int] -> [Int]
go Bundle a
a (Bundle b -> [Int] -> [Int]
forall (b :: Wires). Bundle b -> [Int] -> [Int]
go Bundle b
b [Int]
rest)

inputValues :: Bundle a -> Sample a -> [(Int, Bool)]
inputValues :: forall (a :: Wires). Bundle a -> Sample a -> [(Int, Bool)]
inputValues Bundle a
bundle Sample a
value = Bundle a -> Sample a -> [(Int, Bool)] -> [(Int, Bool)]
forall (b :: Wires).
Bundle b -> Sample b -> [(Int, Bool)] -> [(Int, Bool)]
go Bundle a
bundle Sample a
value []
  where
    go :: Bundle b -> Sample b -> [(Int, Bool)] -> [(Int, Bool)]
    go :: forall (b :: Wires).
Bundle b -> Sample b -> [(Int, Bool)] -> [(Int, Bool)]
go (BBit Int
n) Sample b
bit [(Int, Bool)]
rest = (Int
n, Bool
Sample b
bit) (Int, Bool) -> [(Int, Bool)] -> [(Int, Bool)]
forall a. a -> [a] -> [a]
: [(Int, Bool)]
rest
    go Bundle b
BEmpty () [(Int, Bool)]
rest = [(Int, Bool)]
rest
    go (BPair Bundle a
a Bundle b
b) (UN Sim (Value @ Ready a)
x, UN Sim (Value @ Ready b)
y) [(Int, Bool)]
rest = Bundle a
-> UN Sim (Value @ Ready a) -> [(Int, Bool)] -> [(Int, Bool)]
forall (b :: Wires).
Bundle b -> Sample b -> [(Int, Bool)] -> [(Int, Bool)]
go Bundle a
a UN Sim (Value @ Ready a)
x (Bundle b
-> UN Sim (Value @ Ready b) -> [(Int, Bool)] -> [(Int, Bool)]
forall (b :: Wires).
Bundle b -> Sample b -> [(Int, Bool)] -> [(Int, Bool)]
go Bundle b
b UN Sim (Value @ Ready b)
y [(Int, Bool)]
rest)

output :: Bundle a -> IM.IntMap Bool -> Sample a
output :: forall (a :: Wires). Bundle a -> IntMap Bool -> Sample a
output (BBit Int
n) IntMap Bool
bs = IntMap Bool
bs IntMap Bool -> Int -> Bool
forall a. IntMap a -> Int -> a
IM.! Int
n
output Bundle a
BEmpty IntMap Bool
_ = ()
output (BPair Bundle a
a Bundle b
b) IntMap Bool
bs = (Bundle a -> IntMap Bool -> UN Sim (Value @ Ready a)
forall (a :: Wires). Bundle a -> IntMap Bool -> Sample a
output Bundle a
a IntMap Bool
bs, Bundle b -> IntMap Bool -> UN Sim (Value @ Ready b)
forall (a :: Wires). Bundle a -> IntMap Bool -> Sample a
output Bundle b
b IntMap Bool
bs)

-- Each bit has one driver. Aliases connect the placeholders allocated by a trace.
data Driver
  = Input
  | Constant Bool
  | Not Int
  | And Int Int
  | Or Int Int
  | Xor Int Int
  | Mux Int Int Int
  | Register Bool Int
  | Alias Int
  deriving (Int -> Driver -> ShowS
[Driver] -> ShowS
Driver -> String
(Int -> Driver -> ShowS)
-> (Driver -> String) -> ([Driver] -> ShowS) -> Show Driver
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Driver -> ShowS
showsPrec :: Int -> Driver -> ShowS
$cshow :: Driver -> String
show :: Driver -> String
$cshowList :: [Driver] -> ShowS
showList :: [Driver] -> ShowS
Show)

inputs :: Driver -> [Int]
inputs :: Driver -> [Int]
inputs Driver
Input = []
inputs (Constant Bool
_) = []
inputs (Not Int
a) = [Int
a]
inputs (And Int
a Int
b) = [Int
a, Int
b]
inputs (Or Int
a Int
b) = [Int
a, Int
b]
inputs (Xor Int
a Int
b) = [Int
a, Int
b]
inputs (Mux Int
s Int
a Int
b) = [Int
s, Int
a, Int
b]
inputs (Register Bool
_ Int
a) = [Int
a]
inputs (Alias Int
a) = [Int
a]

data BuildState = BuildState Int (IM.IntMap Driver)
newtype Build a = Build {forall a. Build a -> BuildState -> (a, BuildState)
runBuild :: BuildState -> (a, BuildState)}
instance P.Functor Build where
  fmap :: forall a b. (a -> b) -> Build a -> Build b
fmap a -> b
f (Build BuildState -> (a, BuildState)
g) = (BuildState -> (b, BuildState)) -> Build b
forall a. (BuildState -> (a, BuildState)) -> Build a
Build \BuildState
s -> let (a
x, BuildState
s') = BuildState -> (a, BuildState)
g BuildState
s in (a -> b
f a
x, BuildState
s')
instance Applicative Build where
  pure :: forall a. a -> Build a
pure a
x = (BuildState -> (a, BuildState)) -> Build a
forall a. (BuildState -> (a, BuildState)) -> Build a
Build (a
x,)
  Build (a -> b)
f <*> :: forall a b. Build (a -> b) -> Build a -> Build b
<*> Build a
x = do g <- Build (a -> b)
f; g <$> x
instance Monad Build where
  Build BuildState -> (a, BuildState)
f >>= :: forall a b. Build a -> (a -> Build b) -> Build b
>>= a -> Build b
k = (BuildState -> (b, BuildState)) -> Build b
forall a. (BuildState -> (a, BuildState)) -> Build a
Build \BuildState
s -> let (a
x, BuildState
s') = BuildState -> (a, BuildState)
f BuildState
s in Build b -> BuildState -> (b, BuildState)
forall a. Build a -> BuildState -> (a, BuildState)
runBuild (a -> Build b
k a
x) BuildState
s'

fresh :: Driver -> Build Int
fresh :: Driver -> Build Int
fresh Driver
d = (BuildState -> (Int, BuildState)) -> Build Int
forall a. (BuildState -> (a, BuildState)) -> Build a
Build \(BuildState Int
n IntMap Driver
ds) -> (Int
n, Int -> IntMap Driver -> BuildState
BuildState (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int -> Driver -> IntMap Driver -> IntMap Driver
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
n Driver
d IntMap Driver
ds))

freshBundle :: Driver -> Shape a -> Build (Bundle a)
freshBundle :: forall (a :: Wires). Driver -> Shape a -> Build (Bundle a)
freshBundle Driver
d Shape a
BitS = Int -> Bundle a
Int -> Bundle Bit
BBit (Int -> Bundle a) -> Build Int -> Build (Bundle a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Driver -> Build Int
fresh Driver
d
freshBundle Driver
_ Shape a
EmptyS = Bundle a -> Build (Bundle a)
forall a. a -> Build a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bundle a
Bundle Empty
BEmpty
freshBundle Driver
d (PairS Shape a
a Shape b
b) = Bundle a -> Bundle b -> Bundle a
Bundle a -> Bundle b -> Bundle (Pair a b)
forall (a :: Wires) (b :: Wires).
Bundle a -> Bundle b -> Bundle (Pair a b)
BPair (Bundle a -> Bundle b -> Bundle a)
-> Build (Bundle a) -> Build (Bundle b -> Bundle a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Driver -> Shape a -> Build (Bundle a)
forall (a :: Wires). Driver -> Shape a -> Build (Bundle a)
freshBundle Driver
d Shape a
a Build (Bundle b -> Bundle a)
-> Build (Bundle b) -> Build (Bundle a)
forall a b. Build (a -> b) -> Build a -> Build b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Driver -> Shape b -> Build (Bundle b)
forall (a :: Wires). Driver -> Shape a -> Build (Bundle a)
freshBundle Driver
d Shape b
b

connect :: Bundle a -> Bundle a -> Build ()
connect :: forall (a :: Wires). Bundle a -> Bundle a -> Build ()
connect (BBit Int
a) (BBit Int
b) = (BuildState -> ((), BuildState)) -> Build ()
forall a. (BuildState -> (a, BuildState)) -> Build a
Build \(BuildState Int
n IntMap Driver
ds) -> ((), Int -> IntMap Driver -> BuildState
BuildState Int
n (Int -> Driver -> IntMap Driver -> IntMap Driver
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
a (Int -> Driver
Alias Int
b) IntMap Driver
ds))
connect Bundle a
BEmpty Bundle a
BEmpty = () -> Build ()
forall a. a -> Build a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()
connect (BPair Bundle a
a Bundle b
b) (BPair Bundle a
c Bundle b
d) = Bundle a -> Bundle a -> Build ()
forall (a :: Wires). Bundle a -> Bundle a -> Build ()
connect Bundle a
a Bundle a
Bundle a
c Build () -> Build () -> Build ()
forall a b. Build a -> Build b -> Build b
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Bundle b -> Bundle b -> Build ()
forall (a :: Wires). Bundle a -> Bundle a -> Build ()
connect Bundle b
b Bundle b
Bundle b
d

-- | A typed circuit builder. Constructors are hidden so every output bit has one driver.
type Circuit :: CAT Wires
data Circuit a b where
  Circuit :: (KnownWires a, KnownWires b) => (Bundle a -> Build (Bundle b)) -> Circuit a b

instance CategoryOf Wires where
  type (~>) = Circuit
  type Ob a = KnownWires a
instance Profunctor Circuit where
  dimap :: forall (c :: Wires) (a :: Wires) (b :: Wires) (d :: Wires).
(c ~> a) -> (b ~> d) -> Circuit a b -> Circuit c d
dimap = (c ~> a) -> (b ~> d) -> Circuit a b -> Circuit c d
Circuit c a -> Circuit b d -> Circuit a b -> Circuit c d
forall {k} (p :: CAT k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: Wires) (b :: Wires) r.
((Ob a, Ob b) => r) -> Circuit a b -> r
\\ Circuit{} = r
(Ob a, Ob b) => r
r
instance Promonad Circuit where
  id :: forall (a :: Wires). Ob a => Circuit a a
id = (Bundle a -> Build (Bundle a)) -> Circuit a a
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
(Bundle a -> Build (Bundle b)) -> Circuit a b
Circuit Bundle a -> Build (Bundle a)
forall a. a -> Build a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure
  Circuit Bundle b -> Build (Bundle c)
f . :: forall (b :: Wires) (c :: Wires) (a :: Wires).
Circuit b c -> Circuit a b -> Circuit a c
. Circuit Bundle a -> Build (Bundle b)
g = (Bundle a -> Build (Bundle c)) -> Circuit a c
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
(Bundle a -> Build (Bundle b)) -> Circuit a b
Circuit (Bundle a -> Build (Bundle b)
g (Bundle a -> Build (Bundle b))
-> (Bundle b -> Build (Bundle c)) -> Bundle a -> Build (Bundle c)
forall (m :: Type -> Type) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Bundle b -> Build (Bundle c)
f)
instance MonoidalProfunctor Circuit where
  one :: Circuit Unit Unit
one = (Bundle Empty -> Build (Bundle Empty)) -> Circuit Empty Empty
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
(Bundle a -> Build (Bundle b)) -> Circuit a b
Circuit Bundle Empty -> Build (Bundle Empty)
forall a. a -> Build a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure
  Circuit Bundle x1 -> Build (Bundle x2)
f ** :: forall (x1 :: Wires) (x2 :: Wires) (y1 :: Wires) (y2 :: Wires).
Circuit x1 x2 -> Circuit y1 y2 -> Circuit (x1 ** y1) (x2 ** y2)
** Circuit Bundle y1 -> Build (Bundle y2)
g = (Bundle (Pair x1 y1) -> Build (Bundle (Pair x2 y2)))
-> Circuit (Pair x1 y1) (Pair x2 y2)
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
(Bundle a -> Build (Bundle b)) -> Circuit a b
Circuit \(BPair Bundle a
a Bundle b
b) -> Bundle x2 -> Bundle y2 -> Bundle (Pair x2 y2)
forall (a :: Wires) (b :: Wires).
Bundle a -> Bundle b -> Bundle (Pair a b)
BPair (Bundle x2 -> Bundle y2 -> Bundle (Pair x2 y2))
-> Build (Bundle x2) -> Build (Bundle y2 -> Bundle (Pair x2 y2))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Bundle x1 -> Build (Bundle x2)
f Bundle x1
Bundle a
a Build (Bundle y2 -> Bundle (Pair x2 y2))
-> Build (Bundle y2) -> Build (Bundle (Pair x2 y2))
forall a b. Build (a -> b) -> Build a -> Build b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Bundle y1 -> Build (Bundle y2)
g Bundle y1
Bundle b
b
instance Monoidal Wires where
  type Unit = Empty
  type a ** b = Pair a b
  withOb2 :: forall (a :: Wires) (b :: Wires) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 Ob (a ** b) => r
r = r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: Wires). Ob a => (Unit ** a) ~> a
leftUnitor = (Bundle (Pair Empty a) -> Build (Bundle a))
-> Circuit (Pair Empty a) a
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
(Bundle a -> Build (Bundle b)) -> Circuit a b
Circuit \(BPair Bundle a
BEmpty Bundle b
a) -> Bundle a -> Build (Bundle a)
forall a. a -> Build a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bundle a
Bundle b
a
  leftUnitorInv :: forall (a :: Wires). Ob a => a ~> (Unit ** a)
leftUnitorInv = (Bundle a -> Build (Bundle (Pair Empty a)))
-> Circuit a (Pair Empty a)
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
(Bundle a -> Build (Bundle b)) -> Circuit a b
Circuit \Bundle a
a -> Bundle (Pair Empty a) -> Build (Bundle (Pair Empty a))
forall a. a -> Build a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Bundle Empty -> Bundle a -> Bundle (Pair Empty a)
forall (a :: Wires) (b :: Wires).
Bundle a -> Bundle b -> Bundle (Pair a b)
BPair Bundle Empty
BEmpty Bundle a
a)
  rightUnitor :: forall (a :: Wires). Ob a => (a ** Unit) ~> a
rightUnitor = (Bundle (Pair a Empty) -> Build (Bundle a))
-> Circuit (Pair a Empty) a
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
(Bundle a -> Build (Bundle b)) -> Circuit a b
Circuit \(BPair Bundle a
a Bundle b
BEmpty) -> Bundle a -> Build (Bundle a)
forall a. a -> Build a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bundle a
Bundle a
a
  rightUnitorInv :: forall (a :: Wires). Ob a => a ~> (a ** Unit)
rightUnitorInv = (Bundle a -> Build (Bundle (Pair a Empty)))
-> Circuit a (Pair a Empty)
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
(Bundle a -> Build (Bundle b)) -> Circuit a b
Circuit \Bundle a
a -> Bundle (Pair a Empty) -> Build (Bundle (Pair a Empty))
forall a. a -> Build a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Bundle a -> Bundle Empty -> Bundle (Pair a Empty)
forall (a :: Wires) (b :: Wires).
Bundle a -> Bundle b -> Bundle (Pair a b)
BPair Bundle a
a Bundle Empty
BEmpty)
  associator :: forall (a :: Wires) (b :: Wires) (c :: Wires).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator = (Bundle (Pair (Pair a b) c) -> Build (Bundle (Pair a (Pair b c))))
-> Circuit (Pair (Pair a b) c) (Pair a (Pair b c))
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
(Bundle a -> Build (Bundle b)) -> Circuit a b
Circuit \(BPair (BPair Bundle a
a Bundle b
b) Bundle b
c) -> Bundle (Pair a (Pair b c)) -> Build (Bundle (Pair a (Pair b c)))
forall a. a -> Build a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Bundle a -> Bundle (Pair b b) -> Bundle (Pair a (Pair b b))
forall (a :: Wires) (b :: Wires).
Bundle a -> Bundle b -> Bundle (Pair a b)
BPair Bundle a
a (Bundle b -> Bundle b -> Bundle (Pair b b)
forall (a :: Wires) (b :: Wires).
Bundle a -> Bundle b -> Bundle (Pair a b)
BPair Bundle b
b Bundle b
c))
  associatorInv :: forall (a :: Wires) (b :: Wires) (c :: Wires).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv = (Bundle (Pair a (Pair b c)) -> Build (Bundle (Pair (Pair a b) c)))
-> Circuit (Pair a (Pair b c)) (Pair (Pair a b) c)
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
(Bundle a -> Build (Bundle b)) -> Circuit a b
Circuit \(BPair Bundle a
a (BPair Bundle a
b Bundle b
c)) -> Bundle (Pair (Pair a b) c) -> Build (Bundle (Pair (Pair a b) c))
forall a. a -> Build a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Bundle (Pair a a) -> Bundle b -> Bundle (Pair (Pair a a) b)
forall (a :: Wires) (b :: Wires).
Bundle a -> Bundle b -> Bundle (Pair a b)
BPair (Bundle a -> Bundle a -> Bundle (Pair a a)
forall (a :: Wires) (b :: Wires).
Bundle a -> Bundle b -> Bundle (Pair a b)
BPair Bundle a
a Bundle a
b) Bundle b
c)
instance SymMonoidal Wires where
  swap :: forall (a :: Wires) (b :: Wires).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap = (Bundle (Pair a b) -> Build (Bundle (Pair b a)))
-> Circuit (Pair a b) (Pair b a)
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
(Bundle a -> Build (Bundle b)) -> Circuit a b
Circuit \(BPair Bundle a
a Bundle b
b) -> Bundle (Pair b a) -> Build (Bundle (Pair b a))
forall a. a -> Build a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Bundle b -> Bundle a -> Bundle (Pair b a)
forall (a :: Wires) (b :: Wires).
Bundle a -> Bundle b -> Bundle (Pair a b)
BPair Bundle b
b Bundle a
a)
instance (KnownWires a) => Comonoid a where
  counit :: a ~> Unit
counit = (Bundle a -> Build (Bundle Empty)) -> Circuit a Empty
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
(Bundle a -> Build (Bundle b)) -> Circuit a b
Circuit \Bundle a
_ -> Bundle Empty -> Build (Bundle Empty)
forall a. a -> Build a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bundle Empty
BEmpty
  comult :: a ~> (a ** a)
comult = (Bundle a -> Build (Bundle (Pair a a))) -> Circuit a (Pair a a)
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
(Bundle a -> Build (Bundle b)) -> Circuit a b
Circuit \Bundle a
a -> Bundle (Pair a a) -> Build (Bundle (Pair a a))
forall a. a -> Build a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Bundle a -> Bundle a -> Bundle (Pair a a)
forall (a :: Wires) (b :: Wires).
Bundle a -> Bundle b -> Bundle (Pair a b)
BPair Bundle a
a Bundle a
a)
instance (KnownWires a) => CocommutativeComonoid a
instance CopyDiscard Wires
instance Costrong Tensor Circuit where
  coact :: forall (a :: Wires) (x :: Wires) (y :: Wires).
(Ob a, Ob x, Ob y) =>
Circuit (Act Tensor a x) (Act Tensor a y) -> Circuit x y
coact @a (Circuit Bundle (Act Tensor a x) -> Build (Bundle (Act Tensor a y))
f) = (Bundle x -> Build (Bundle y)) -> Circuit x y
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
(Bundle a -> Build (Bundle b)) -> Circuit a b
Circuit \Bundle x
x -> do
    feedback <- Driver -> Shape a -> Build (Bundle a)
forall (a :: Wires). Driver -> Shape a -> Build (Bundle a)
freshBundle Driver
Input (forall (a :: Wires). KnownWires a => Shape a
shape @a)
    result <- f (BPair feedback x)
    case result of
      BPair Bundle a
feedback' Bundle b
y -> do
        Bundle a -> Bundle a -> Build ()
forall (a :: Wires). Bundle a -> Bundle a -> Build ()
connect Bundle a
feedback Bundle a
Bundle a
feedback'
        Bundle y -> Build (Bundle y)
forall a. a -> Build a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bundle y
Bundle b
y

-- | A constant bit, independent of the clock.
constant :: Bool -> Empty ~> Bit
constant :: Bool -> Empty ~> Bit
constant Bool
b = (Bundle Empty -> Build (Bundle Bit)) -> Circuit Empty Bit
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
(Bundle a -> Build (Bundle b)) -> Circuit a b
Circuit \Bundle Empty
BEmpty -> Int -> Bundle Bit
BBit (Int -> Bundle Bit) -> Build Int -> Build (Bundle Bit)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Driver -> Build Int
fresh (Bool -> Driver
Constant Bool
b)

notGate :: Bit ~> Bit
notGate :: Bit ~> Bit
notGate = (Bundle Bit -> Build (Bundle Bit)) -> Circuit Bit Bit
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
(Bundle a -> Build (Bundle b)) -> Circuit a b
Circuit \(BBit Int
a) -> Int -> Bundle Bit
BBit (Int -> Bundle Bit) -> Build Int -> Build (Bundle Bit)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Driver -> Build Int
fresh (Int -> Driver
Not Int
a)
andGate :: Bit ** Bit ~> Bit
andGate :: (Bit ** Bit) ~> Bit
andGate = (Bundle (Pair Bit Bit) -> Build (Bundle Bit))
-> Circuit (Pair Bit Bit) Bit
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
(Bundle a -> Build (Bundle b)) -> Circuit a b
Circuit \(BPair (BBit Int
a) (BBit Int
b)) -> Int -> Bundle Bit
BBit (Int -> Bundle Bit) -> Build Int -> Build (Bundle Bit)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Driver -> Build Int
fresh (Int -> Int -> Driver
And Int
a Int
b)
orGate :: Bit ** Bit ~> Bit
orGate :: (Bit ** Bit) ~> Bit
orGate = (Bundle (Pair Bit Bit) -> Build (Bundle Bit))
-> Circuit (Pair Bit Bit) Bit
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
(Bundle a -> Build (Bundle b)) -> Circuit a b
Circuit \(BPair (BBit Int
a) (BBit Int
b)) -> Int -> Bundle Bit
BBit (Int -> Bundle Bit) -> Build Int -> Build (Bundle Bit)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Driver -> Build Int
fresh (Int -> Int -> Driver
Or Int
a Int
b)
xorGate :: Bit ** Bit ~> Bit
xorGate :: (Bit ** Bit) ~> Bit
xorGate = (Bundle (Pair Bit Bit) -> Build (Bundle Bit))
-> Circuit (Pair Bit Bit) Bit
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
(Bundle a -> Build (Bundle b)) -> Circuit a b
Circuit \(BPair (BBit Int
a) (BBit Int
b)) -> Int -> Bundle Bit
BBit (Int -> Bundle Bit) -> Build Int -> Build (Bundle Bit)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Driver -> Build Int
fresh (Int -> Int -> Driver
Xor Int
a Int
b)

-- | Select the second input when the first is true, and the third when it is false.
mux :: Bit ** Bit ** Bit ~> Bit
mux :: ((Bit ** Bit) ** Bit) ~> Bit
mux = (Bundle (Pair (Pair Bit Bit) Bit) -> Build (Bundle Bit))
-> Circuit (Pair (Pair Bit Bit) Bit) Bit
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
(Bundle a -> Build (Bundle b)) -> Circuit a b
Circuit \(BPair (BPair (BBit Int
s) (BBit Int
a)) (BBit Int
b)) -> Int -> Bundle Bit
BBit (Int -> Bundle Bit) -> Build Int -> Build (Bundle Bit)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Driver -> Build Int
fresh (Int -> Int -> Int -> Driver
Mux Int
s Int
a Int
b)

-- | A register's output starts at the given value. Each clock edge replaces it with its input
-- from the preceding cycle. All registers update simultaneously.
register :: Bool -> Bit ~> Bit
register :: Bool -> Bit ~> Bit
register Bool
initial = (Bundle Bit -> Build (Bundle Bit)) -> Circuit Bit Bit
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
(Bundle a -> Build (Bundle b)) -> Circuit a b
Circuit \(BBit Int
a) -> Int -> Bundle Bit
BBit (Int -> Bundle Bit) -> Build Int -> Build (Bundle Bit)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Driver -> Build Int
fresh (Bool -> Int -> Driver
Register Bool
initial Int
a)

-- | A netlist with typed boundaries. Disconnected components are omitted.
type Netlist :: Wires -> Wires -> Type
data Netlist a b where
  Netlist :: (KnownWires a, KnownWires b) => Bundle a -> Bundle b -> IM.IntMap Driver -> Netlist a b

-- | Build a netlist, retaining precisely the components that can influence an output, including
-- through a register on a later cycle.
netlist :: Circuit a b -> Netlist a b
netlist :: forall (a :: Wires) (b :: Wires). Circuit a b -> Netlist a b
netlist (Circuit Bundle a -> Build (Bundle b)
f) = Bundle a -> Bundle b -> IntMap Driver -> Netlist a b
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
Bundle a -> Bundle b -> IntMap Driver -> Netlist a b
Netlist Bundle a
ins Bundle b
outs (IntMap Driver -> IntSet -> IntMap Driver
forall a. IntMap a -> IntSet -> IntMap a
IM.restrictKeys IntMap Driver
ds (IntSet -> [Int] -> IntSet
reachable IntSet
IS.empty (Bundle b -> [Int]
forall (a :: Wires). Bundle a -> [Int]
ports Bundle b
outs)))
  where
    ((Bundle a
ins, Bundle b
outs), BuildState Int
_ IntMap Driver
ds) = Build (Bundle a, Bundle b)
-> BuildState -> ((Bundle a, Bundle b), BuildState)
forall a. Build a -> BuildState -> (a, BuildState)
runBuild Build (Bundle a, Bundle b)
build (Int -> IntMap Driver -> BuildState
BuildState Int
0 IntMap Driver
forall a. IntMap a
IM.empty)
    build :: Build (Bundle a, Bundle b)
build = do
      ins' <- Driver -> Shape a -> Build (Bundle a)
forall (a :: Wires). Driver -> Shape a -> Build (Bundle a)
freshBundle Driver
Input Shape a
forall (a :: Wires). KnownWires a => Shape a
shape
      outs' <- f ins'
      pure (ins', outs')
    reachable :: IntSet -> [Int] -> IntSet
reachable IntSet
seen [] = IntSet
seen
    reachable IntSet
seen (Int
n : [Int]
ns)
      | Int -> IntSet -> Bool
IS.member Int
n IntSet
seen = IntSet -> [Int] -> IntSet
reachable IntSet
seen [Int]
ns
      | Bool
otherwise = IntSet -> [Int] -> IntSet
reachable (Int -> IntSet -> IntSet
IS.insert Int
n IntSet
seen) (Driver -> [Int]
inputs (IntMap Driver
ds IntMap Driver -> Int -> Driver
forall a. IntMap a -> Int -> a
IM.! Int
n) [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int]
ns)

-- | A text netlist. Bit numbers are local to this netlist; bundle ports are ordered left to right.
renderNetlist :: Netlist a b -> String
renderNetlist :: forall (a :: Wires) (b :: Wires). Netlist a b -> String
renderNetlist (Netlist Bundle a
ins Bundle b
outs IntMap Driver
ds) =
  [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
    [String
"inputs " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Int] -> String
forall a. Show a => a -> String
show (Bundle a -> [Int]
forall (a :: Wires). Bundle a -> [Int]
ports Bundle a
ins), String
"outputs " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Int] -> String
forall a. Show a => a -> String
show (Bundle b -> [Int]
forall (a :: Wires). Bundle a -> [Int]
ports Bundle b
outs)]
      [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Driver -> String
forall a. Show a => a -> String
show Driver
d | (Int
n, Driver
d) <- IntMap Driver -> [(Int, Driver)]
forall a. IntMap a -> [(Int, a)]
IM.toAscList IntMap Driver
ds]

-- | A Graphviz graph of the same netlist used by the simulator. Register nodes show their
-- initial value. Copying is fan-out of an edge, and feedback aliases are small connection points.
toDot :: Netlist a b -> String
toDot :: forall (a :: Wires) (b :: Wires). Netlist a b -> String
toDot (Netlist Bundle a
ins Bundle b
outs IntMap Driver
ds) =
  [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
    [ String
"digraph circuit {"
    , String
"rankdir=LR; bgcolor=transparent;"
    , String
"node [shape=box, style=rounded, fontname=Helvetica];"
    , String
"edge [fontname=Helvetica, fontsize=10];"
    ]
      [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [Int -> String
forall a. Show a => a -> String
wire Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" [shape=circle, label=\"in " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\"];" | (Int
i, Int
n) <- [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] (Bundle a -> [Int]
forall (a :: Wires). Bundle a -> [Int]
ports Bundle a
ins), Int -> IntMap Driver -> Bool
forall a. Int -> IntMap a -> Bool
IM.member Int
n IntMap Driver
ds]
      [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"{rank=same; " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [Int -> String
forall a. Show a => a -> String
wire Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
";" | (Int
n, Register{}) <- IntMap Driver -> [(Int, Driver)]
forall a. IntMap a -> [(Int, a)]
IM.toAscList IntMap Driver
ds] String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"]
      [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"{rank=sink; " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String
"o" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
";" | Int
i <- [Int
0 .. [Int] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length (Bundle b -> [Int]
forall (a :: Wires). Bundle a -> [Int]
ports Bundle b
outs) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]] String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"]
      [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((Int, Driver) -> [String]) -> [(Int, Driver)] -> [String]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap (Int, Driver) -> [String]
forall {a}. Show a => (a, Driver) -> [String]
draw (IntMap Driver -> [(Int, Driver)]
forall a. IntMap a -> [(Int, a)]
IM.toAscList IntMap Driver
ds)
      [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [[String]] -> [String]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat
        [ [String
"o" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" [shape=circle, label=\"out " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\"];", Int -> String
forall a. Show a => a -> String
wire Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> o" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
";"]
        | (Int
i, Int
n) <- [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] (Bundle b -> [Int]
forall (a :: Wires). Bundle a -> [Int]
ports Bundle b
outs)
        ]
      [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"}"]
  where
    wire :: a -> String
wire a
n = String
"w" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n
    draw :: (a, Driver) -> [String]
draw (a
_, Driver
Input) = []
    draw (a
n, Driver
d) =
      (a -> String
forall a. Show a => a -> String
wire a
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" [" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Driver -> String
attrs Driver
d String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"];")
        String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [ Int -> String
forall a. Show a => a -> String
wire Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
wire a
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" [headlabel=\"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
label String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Driver -> String
layout Driver
d String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"];"
          | (Int
i, String
label) <- [Int] -> [String] -> [(Int, String)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Driver -> [Int]
inputs Driver
d) (Driver -> [String]
portNames Driver
d)
          ]
    layout :: Driver -> String
layout Register{} = String
", constraint=false"
    layout Driver
_ = String
""
    attrs :: Driver -> String
attrs (Alias Int
_) = String
"shape=point, label=\"\""
    attrs (Register Bool
b Int
_) = String
"shape=box, style=\"rounded,filled\", fillcolor=\"#dbeafe\", label=\"D " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bool -> String
bit Bool
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\""
    attrs Driver
d = String
"label=\"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Driver -> String
name Driver
d String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\""
    name :: Driver -> String
name (Constant Bool
b) = Bool -> String
bit Bool
b
    name Not{} = String
"NOT"
    name And{} = String
"AND"
    name Or{} = String
"OR"
    name Xor{} = String
"XOR"
    name Mux{} = String
"MUX"
    name Driver
_ = String
""
    bit :: Bool -> String
bit Bool
False = String
"0"
    bit Bool
True = String
"1"
    portNames :: Driver -> [String]
portNames Mux{} = [String
"sel", String
"1", String
"0"]
    portNames Register{} = [String
"D"]
    portNames Driver
_ = String -> [String]
forall a. a -> [a]
repeat String
""

-- | Verilog with scalar ports @in0@, @in1@, ... and @out0@, @out1@, ... in bundle order,
-- and a shared rising-edge clock @clk@. The caller supplies a valid Verilog module name.
-- Combinational cycles are rejected, and disconnected components are omitted.
--
-- Registers use @initial@ assignments to preserve their starting values in simulation;
-- synthesis support for initialization depends on the hardware target.
toVerilog :: String -> Netlist a b -> Either CircuitError String
toVerilog :: forall (a :: Wires) (b :: Wires).
String -> Netlist a b -> Either CircuitError String
toVerilog String
name graph :: Netlist a b
graph@(Netlist Bundle a
ins Bundle b
outs IntMap Driver
ds) = do
  _ <- Netlist a b -> Either CircuitError (Prepared (Ready a) (Ready b))
forall (a :: Wires) (b :: Wires).
Netlist a b -> Either CircuitError (Prepared (Ready a) (Ready b))
prepare Netlist a b
graph
  pure $
    unlines $
      ["module " ++ name ++ "(" ++ List.intercalate ", " interface ++ ");"]
        ++ ["  " ++ declaration n d | (n, d) <- drivers]
        ++ ["  assign " ++ wire n ++ " = in" ++ show i ++ ";" | (i, n) <- inputPorts, IM.member n ds]
        ++ concatMap emit drivers
        ++ ["  assign out" ++ show i ++ " = " ++ wire n ++ ";" | (i, n) <- outputPorts]
        ++ ["endmodule"]
  where
    inputPorts :: [(Int, Int)]
inputPorts = [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] (Bundle a -> [Int]
forall (a :: Wires). Bundle a -> [Int]
ports Bundle a
ins)
    outputPorts :: [(Int, Int)]
outputPorts = [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] (Bundle b -> [Int]
forall (a :: Wires). Bundle a -> [Int]
ports Bundle b
outs)
    interface :: [String]
interface =
      [String
"input wire clk"]
        [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"input wire in" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i | (Int
i, Int
_) <- [(Int, Int)]
inputPorts]
        [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"output wire out" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i | (Int
i, Int
_) <- [(Int, Int)]
outputPorts]
    drivers :: [(Int, Driver)]
drivers = IntMap Driver -> [(Int, Driver)]
forall a. IntMap a -> [(Int, a)]
IM.toAscList IntMap Driver
ds
    wire :: a -> String
wire a
n = String
"w" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n
    declaration :: a -> Driver -> String
declaration a
n Register{} = String
"reg " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
wire a
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
";"
    declaration a
n Driver
_ = String
"wire " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
wire a
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
";"
    emit :: (a, Driver) -> [String]
emit (a
n, Driver
d) = case Driver
d of
      Driver
Input -> []
      Constant Bool
b -> String -> [String]
assign (Bool -> String
bit Bool
b)
      Not Int
a -> String -> [String]
assign (String
"~" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
wire Int
a)
      And Int
a Int
b -> String -> [String]
assign (String -> Int -> Int -> String
forall {a} {a}. (Show a, Show a) => String -> a -> a -> String
binary String
" & " Int
a Int
b)
      Or Int
a Int
b -> String -> [String]
assign (String -> Int -> Int -> String
forall {a} {a}. (Show a, Show a) => String -> a -> a -> String
binary String
" | " Int
a Int
b)
      Xor Int
a Int
b -> String -> [String]
assign (String -> Int -> Int -> String
forall {a} {a}. (Show a, Show a) => String -> a -> a -> String
binary String
" ^ " Int
a Int
b)
      Mux Int
s Int
a Int
b -> String -> [String]
assign (Int -> String
forall a. Show a => a -> String
wire Int
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ? " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
wire Int
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
wire Int
b)
      Alias Int
a -> String -> [String]
assign (Int -> String
forall a. Show a => a -> String
wire Int
a)
      Register Bool
initial Int
a ->
        [ String
"  initial " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
wire a
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bool -> String
bit Bool
initial String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
";"
        , String
"  always @(posedge clk) " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
wire a
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" <= " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
wire Int
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
";"
        ]
      where
        assign :: String -> [String]
assign String
expression = [String
"  assign " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
wire a
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
expression String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
";"]
    binary :: String -> a -> a -> String
binary String
op a
a a
b = a -> String
forall a. Show a => a -> String
wire a
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
op String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
wire a
b
    bit :: Bool -> String
bit Bool
False = String
"1'b0"
    bit Bool
True = String
"1'b1"

-- | Bits participating in a combinational cycle. Every observable cycle must cross a register.
newtype CircuitError = CombinationalCycle [Int]
  deriving (CircuitError -> CircuitError -> Bool
(CircuitError -> CircuitError -> Bool)
-> (CircuitError -> CircuitError -> Bool) -> Eq CircuitError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CircuitError -> CircuitError -> Bool
== :: CircuitError -> CircuitError -> Bool
$c/= :: CircuitError -> CircuitError -> Bool
/= :: CircuitError -> CircuitError -> Bool
Eq, Int -> CircuitError -> ShowS
[CircuitError] -> ShowS
CircuitError -> String
(Int -> CircuitError -> ShowS)
-> (CircuitError -> String)
-> ([CircuitError] -> ShowS)
-> Show CircuitError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CircuitError -> ShowS
showsPrec :: Int -> CircuitError -> ShowS
$cshow :: CircuitError -> String
show :: CircuitError -> String
$cshowList :: [CircuitError] -> ShowS
showList :: [CircuitError] -> ShowS
Show)

-- | A circuit that passed combinational-cycle validation, carrying its current simulation state.
-- Composition and tensor preserve validity; unrestricted trace is available only before validation.
type Prepared :: CAT PREPARED
data Prepared a b where
  Prepared
    :: (KnownWires a, KnownWires b)
    => Simulator (Value @ Ready a) (Value @ Ready b) -> Prepared (Ready a) (Ready b)

instance CategoryOf PREPARED where
  type (~>) = Prepared
  type Ob a = (Is Ready a, KnownWires (UN Ready a))
instance Profunctor Prepared where
  dimap :: forall (c :: PREPARED) (a :: PREPARED) (b :: PREPARED)
       (d :: PREPARED).
(c ~> a) -> (b ~> d) -> Prepared a b -> Prepared c d
dimap = (c ~> a) -> (b ~> d) -> Prepared a b -> Prepared c d
Prepared c a -> Prepared b d -> Prepared a b -> Prepared c d
forall {k} (p :: CAT k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: PREPARED) (b :: PREPARED) r.
((Ob a, Ob b) => r) -> Prepared a b -> r
\\ Prepared{} = r
(Ob a, Ob b) => r
r
instance Promonad Prepared where
  id :: forall (a :: PREPARED). Ob a => Prepared a a
id = Simulator (Value @ Ready (UN Ready a)) (Value @ Ready (UN Ready a))
-> Prepared (Ready (UN Ready a)) (Ready (UN Ready a))
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
Simulator (Value @ Ready a) (Value @ Ready b)
-> Prepared (Ready a) (Ready b)
Prepared Simulator (Value @ Ready (UN Ready a)) (Value @ Ready (UN Ready a))
Simulator
  (Sim (UN Sim (Value @ Ready (UN Ready a))))
  (Sim (UN Sim (Value @ Ready (UN Ready a))))
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: SIMULATOR). Ob a => Simulator a a
id
  Prepared Simulator (Value @ Ready a) (Value @ Ready b)
f . :: forall (b :: PREPARED) (c :: PREPARED) (a :: PREPARED).
Prepared b c -> Prepared a b -> Prepared a c
. Prepared Simulator (Value @ Ready a) (Value @ Ready b)
g = Simulator (Value @ Ready a) (Value @ Ready b)
-> Prepared (Ready a) (Ready b)
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
Simulator (Value @ Ready a) (Value @ Ready b)
-> Prepared (Ready a) (Ready b)
Prepared (Simulator (Value @ Ready a) (Value @ Ready b)
Simulator
  (Sim (UN Sim (Value @ Ready a))) (Sim (UN Sim (Value @ Ready b)))
f Simulator
  (Sim (UN Sim (Value @ Ready a))) (Sim (UN Sim (Value @ Ready b)))
-> Simulator
     (Sim (UN Sim (Value @ Ready a))) (Sim (UN Sim (Value @ Ready a)))
-> Simulator
     (Sim (UN Sim (Value @ Ready a))) (Sim (UN Sim (Value @ Ready b)))
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: SIMULATOR) (c :: SIMULATOR) (a :: SIMULATOR).
Simulator b c -> Simulator a b -> Simulator a c
. Simulator (Value @ Ready a) (Value @ Ready b)
Simulator
  (Sim (UN Sim (Value @ Ready a))) (Sim (UN Sim (Value @ Ready a)))
g)
instance MonoidalProfunctor Prepared where
  one :: Prepared Unit Unit
one = Simulator (Value @ Ready Empty) (Value @ Ready Empty)
-> Prepared (Ready Empty) (Ready Empty)
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
Simulator (Value @ Ready a) (Value @ Ready b)
-> Prepared (Ready a) (Ready b)
Prepared Simulator (Value @ Ready Empty) (Value @ Ready Empty)
Simulator Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
one
  Prepared Simulator (Value @ Ready a) (Value @ Ready b)
f ** :: forall (x1 :: PREPARED) (x2 :: PREPARED) (y1 :: PREPARED)
       (y2 :: PREPARED).
Prepared x1 x2 -> Prepared y1 y2 -> Prepared (x1 ** y1) (x2 ** y2)
** Prepared Simulator (Value @ Ready a) (Value @ Ready b)
g = Simulator (Value @ Ready (Pair a a)) (Value @ Ready (Pair b b))
-> Prepared (Ready (Pair a a)) (Ready (Pair b b))
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
Simulator (Value @ Ready a) (Value @ Ready b)
-> Prepared (Ready a) (Ready b)
Prepared (Simulator (Value @ Ready a) (Value @ Ready b)
Simulator
  (Sim (UN Sim (Value @ Ready a))) (Sim (UN Sim (Value @ Ready b)))
f Simulator
  (Sim (UN Sim (Value @ Ready a))) (Sim (UN Sim (Value @ Ready b)))
-> Simulator
     (Sim (UN Sim (Value @ Ready a))) (Sim (UN Sim (Value @ Ready b)))
-> Simulator
     (Sim (UN Sim (Value @ Ready a)) ** Sim (UN Sim (Value @ Ready a)))
     (Sim (UN Sim (Value @ Ready b)) ** Sim (UN Sim (Value @ Ready b)))
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: SIMULATOR) (x2 :: SIMULATOR) (y1 :: SIMULATOR)
       (y2 :: SIMULATOR).
Simulator x1 x2
-> Simulator y1 y2 -> Simulator (x1 ** y1) (x2 ** y2)
** Simulator (Value @ Ready a) (Value @ Ready b)
Simulator
  (Sim (UN Sim (Value @ Ready a))) (Sim (UN Sim (Value @ Ready b)))
g)
instance Monoidal PREPARED where
  type Unit = Ready Empty
  type a ** b = Ready (Pair (UN Ready a) (UN Ready b))
  withOb2 :: forall (a :: PREPARED) (b :: PREPARED) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 Ob (a ** b) => r
r = r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: PREPARED). Ob a => (Unit ** a) ~> a
leftUnitor = Simulator
  (Value @ Ready (Pair Empty (UN Ready a)))
  (Value @ Ready (UN Ready a))
-> Prepared (Ready (Pair Empty (UN Ready a))) (Ready (UN Ready a))
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
Simulator (Value @ Ready a) (Value @ Ready b)
-> Prepared (Ready a) (Ready b)
Prepared (Unit ** Sim (UN Sim (Value @ Ready (UN Ready a))))
~> Sim (UN Sim (Value @ Ready (UN Ready a)))
Simulator
  (Value @ Ready (Pair Empty (UN Ready a)))
  (Value @ Ready (UN Ready a))
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
forall (a :: SIMULATOR). Ob a => (Unit ** a) ~> a
leftUnitor
  leftUnitorInv :: forall (a :: PREPARED). Ob a => a ~> (Unit ** a)
leftUnitorInv = Simulator
  (Value @ Ready (UN Ready a))
  (Value @ Ready (Pair Empty (UN Ready a)))
-> Prepared (Ready (UN Ready a)) (Ready (Pair Empty (UN Ready a)))
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
Simulator (Value @ Ready a) (Value @ Ready b)
-> Prepared (Ready a) (Ready b)
Prepared Sim (UN Sim (Value @ Ready (UN Ready a)))
~> (Unit ** Sim (UN Sim (Value @ Ready (UN Ready a))))
Simulator
  (Value @ Ready (UN Ready a))
  (Value @ Ready (Pair Empty (UN Ready a)))
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
forall (a :: SIMULATOR). Ob a => a ~> (Unit ** a)
leftUnitorInv
  rightUnitor :: forall (a :: PREPARED). Ob a => (a ** Unit) ~> a
rightUnitor = Simulator
  (Value @ Ready (Pair (UN Ready a) Empty))
  (Value @ Ready (UN Ready a))
-> Prepared (Ready (Pair (UN Ready a) Empty)) (Ready (UN Ready a))
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
Simulator (Value @ Ready a) (Value @ Ready b)
-> Prepared (Ready a) (Ready b)
Prepared (Sim (UN Sim (Value @ Ready (UN Ready a))) ** Unit)
~> Sim (UN Sim (Value @ Ready (UN Ready a)))
Simulator
  (Value @ Ready (Pair (UN Ready a) Empty))
  (Value @ Ready (UN Ready a))
forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
forall (a :: SIMULATOR). Ob a => (a ** Unit) ~> a
rightUnitor
  rightUnitorInv :: forall (a :: PREPARED). Ob a => a ~> (a ** Unit)
rightUnitorInv = Simulator
  (Value @ Ready (UN Ready a))
  (Value @ Ready (Pair (UN Ready a) Empty))
-> Prepared (Ready (UN Ready a)) (Ready (Pair (UN Ready a) Empty))
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
Simulator (Value @ Ready a) (Value @ Ready b)
-> Prepared (Ready a) (Ready b)
Prepared Sim (UN Sim (Value @ Ready (UN Ready a)))
~> (Sim (UN Sim (Value @ Ready (UN Ready a))) ** Unit)
Simulator
  (Value @ Ready (UN Ready a))
  (Value @ Ready (Pair (UN Ready a) Empty))
forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
forall (a :: SIMULATOR). Ob a => a ~> (a ** Unit)
rightUnitorInv
  associator :: forall (a :: PREPARED) (b :: PREPARED) (c :: PREPARED).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator = Simulator
  (Value
   @ Ready (Pair (Pair (UN Ready a) (UN Ready b)) (UN Ready c)))
  (Value
   @ Ready (Pair (UN Ready a) (Pair (UN Ready b) (UN Ready c))))
-> Prepared
     (Ready (Pair (Pair (UN Ready a) (UN Ready b)) (UN Ready c)))
     (Ready (Pair (UN Ready a) (Pair (UN Ready b) (UN Ready c))))
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
Simulator (Value @ Ready a) (Value @ Ready b)
-> Prepared (Ready a) (Ready b)
Prepared ((Sim (UN Sim (Value @ Ready (UN Ready a)))
  ** Sim (UN Sim (Value @ Ready (UN Ready b))))
 ** Sim (UN Sim (Value @ Ready (UN Ready c))))
~> (Sim (UN Sim (Value @ Ready (UN Ready a)))
    ** (Sim (UN Sim (Value @ Ready (UN Ready b)))
        ** Sim (UN Sim (Value @ Ready (UN Ready c)))))
Simulator
  (Value
   @ Ready (Pair (Pair (UN Ready a) (UN Ready b)) (UN Ready c)))
  (Value
   @ Ready (Pair (UN Ready a) (Pair (UN Ready b) (UN Ready c))))
forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
forall (a :: SIMULATOR) (b :: SIMULATOR) (c :: SIMULATOR).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator
  associatorInv :: forall (a :: PREPARED) (b :: PREPARED) (c :: PREPARED).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv = Simulator
  (Value
   @ Ready (Pair (UN Ready a) (Pair (UN Ready b) (UN Ready c))))
  (Value
   @ Ready (Pair (Pair (UN Ready a) (UN Ready b)) (UN Ready c)))
-> Prepared
     (Ready (Pair (UN Ready a) (Pair (UN Ready b) (UN Ready c))))
     (Ready (Pair (Pair (UN Ready a) (UN Ready b)) (UN Ready c)))
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
Simulator (Value @ Ready a) (Value @ Ready b)
-> Prepared (Ready a) (Ready b)
Prepared (Sim (UN Sim (Value @ Ready (UN Ready a)))
 ** (Sim (UN Sim (Value @ Ready (UN Ready b)))
     ** Sim (UN Sim (Value @ Ready (UN Ready c)))))
~> ((Sim (UN Sim (Value @ Ready (UN Ready a)))
     ** Sim (UN Sim (Value @ Ready (UN Ready b))))
    ** Sim (UN Sim (Value @ Ready (UN Ready c))))
Simulator
  (Value
   @ Ready (Pair (UN Ready a) (Pair (UN Ready b) (UN Ready c))))
  (Value
   @ Ready (Pair (Pair (UN Ready a) (UN Ready b)) (UN Ready c)))
forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
forall (a :: SIMULATOR) (b :: SIMULATOR) (c :: SIMULATOR).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv
instance SymMonoidal PREPARED where
  swap :: forall (a :: PREPARED) (b :: PREPARED).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap = Simulator
  (Value @ Ready (Pair (UN Ready a) (UN Ready b)))
  (Value @ Ready (Pair (UN Ready b) (UN Ready a)))
-> Prepared
     (Ready (Pair (UN Ready a) (UN Ready b)))
     (Ready (Pair (UN Ready b) (UN Ready a)))
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
Simulator (Value @ Ready a) (Value @ Ready b)
-> Prepared (Ready a) (Ready b)
Prepared (Sim (UN Sim (Value @ Ready (UN Ready a)))
 ** Sim (UN Sim (Value @ Ready (UN Ready b))))
~> (Sim (UN Sim (Value @ Ready (UN Ready b)))
    ** Sim (UN Sim (Value @ Ready (UN Ready a))))
Simulator
  (Value @ Ready (Pair (UN Ready a) (UN Ready b)))
  (Value @ Ready (Pair (UN Ready b) (UN Ready a)))
forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall (a :: SIMULATOR) (b :: SIMULATOR).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap
instance (Ob a) => Comonoid (a :: PREPARED) where
  counit :: a ~> Unit
counit = Simulator (Value @ Ready (UN Ready a)) (Value @ Ready Empty)
-> Prepared (Ready (UN Ready a)) (Ready Empty)
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
Simulator (Value @ Ready a) (Value @ Ready b)
-> Prepared (Ready a) (Ready b)
Prepared Sim (UN Sim (Value @ Ready (UN Ready a))) ~> Unit
Simulator (Value @ Ready (UN Ready a)) (Value @ Ready Empty)
forall {k} (c :: k). Comonoid c => c ~> Unit
counit
  comult :: a ~> (a ** a)
comult = Simulator
  (Value @ Ready (UN Ready a))
  (Value @ Ready (Pair (UN Ready a) (UN Ready a)))
-> Prepared
     (Ready (UN Ready a)) (Ready (Pair (UN Ready a) (UN Ready a)))
forall (a :: Wires) (b :: Wires).
(KnownWires a, KnownWires b) =>
Simulator (Value @ Ready a) (Value @ Ready b)
-> Prepared (Ready a) (Ready b)
Prepared Sim (UN Sim (Value @ Ready (UN Ready a)))
~> (Sim (UN Sim (Value @ Ready (UN Ready a)))
    ** Sim (UN Sim (Value @ Ready (UN Ready a))))
Simulator
  (Value @ Ready (UN Ready a))
  (Value @ Ready (Pair (UN Ready a) (UN Ready a)))
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult
instance (Ob a) => CocommutativeComonoid (a :: PREPARED)
instance CopyDiscard PREPARED

instance FunctorForRep Value where
  type Value @ Ready Bit = Sim Bool
  type Value @ Ready Empty = Sim ()
  type Value @ Ready (Pair a b) = Sim (Sample a, Sample b)
  fmap :: forall (a :: PREPARED) (b :: PREPARED).
(a ~> b) -> (Value @ a) ~> (Value @ b)
fmap (Prepared Simulator (Value @ Ready a) (Value @ Ready b)
machine) = (Value @ a) ~> (Value @ b)
Simulator (Value @ Ready a) (Value @ Ready b)
machine

instance MonoidalProfunctor (Rep Value) where
  one :: Rep Value Unit Unit
one = (Sim () ~> (Value @ Ready Empty))
-> Rep Value (Sim ()) (Ready Empty)
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep Sim () ~> (Value @ Ready Empty)
Simulator Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
one
  Rep x1 ~> (Value @ x2)
f ** :: forall (x1 :: SIMULATOR) (x2 :: PREPARED) (y1 :: SIMULATOR)
       (y2 :: PREPARED).
Rep Value x1 x2
-> Rep Value y1 y2 -> Rep Value (x1 ** y1) (x2 ** y2)
** Rep y1 ~> (Value @ y2)
g = (Sim (UN Sim x1, UN Sim y1)
 ~> (Value @ Ready (Pair (UN Ready x2) (UN Ready y2))))
-> Rep
     Value
     (Sim (UN Sim x1, UN Sim y1))
     (Ready (Pair (UN Ready x2) (UN Ready y2)))
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (x1 ~> (Value @ x2)
Simulator x1 (Sim (UN Sim (Value @ Ready (UN Ready x2))))
f Simulator x1 (Sim (UN Sim (Value @ Ready (UN Ready x2))))
-> Simulator y1 (Sim (UN Sim (Value @ Ready (UN Ready y2))))
-> Simulator
     (x1 ** y1)
     (Sim (UN Sim (Value @ Ready (UN Ready x2)))
      ** Sim (UN Sim (Value @ Ready (UN Ready y2))))
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: SIMULATOR) (x2 :: SIMULATOR) (y1 :: SIMULATOR)
       (y2 :: SIMULATOR).
Simulator x1 x2
-> Simulator y1 y2 -> Simulator (x1 ** y1) (x2 ** y2)
** y1 ~> (Value @ y2)
Simulator y1 (Sim (UN Sim (Value @ Ready (UN Ready y2))))
g)

-- | Cut the dependencies through registers and topologically order the combinational nodes.
-- Multiplexers depend on both data inputs, even when their selector is constant.
prepare :: Netlist a b -> Either CircuitError (Prepared (Ready a) (Ready b))
prepare :: forall (a :: Wires) (b :: Wires).
Netlist a b -> Either CircuitError (Prepared (Ready a) (Ready b))
prepare (Netlist Bundle a
ins Bundle b
outs IntMap Driver
ds) = do
  order <- [[(Int, Driver)]] -> [(Int, Driver)]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat ([[(Int, Driver)]] -> [(Int, Driver)])
-> Either CircuitError [[(Int, Driver)]]
-> Either CircuitError [(Int, Driver)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (SCC (Int, Driver) -> Either CircuitError [(Int, Driver)])
-> [SCC (Int, Driver)] -> Either CircuitError [[(Int, Driver)]]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse SCC (Int, Driver) -> Either CircuitError [(Int, Driver)]
acyclic ([((Int, Driver), Int, [Int])] -> [SCC (Int, Driver)]
forall key node. Ord key => [(node, key, [key])] -> [SCC node]
stronglyConnComp [((Int
n, Driver
d), Int
n, Driver -> [Int]
deps Driver
d) | (Int
n, Driver
d) <- IntMap Driver -> [(Int, Driver)]
forall a. IntMap a -> [(Int, a)]
IM.toAscList IntMap Driver
ds])
  let run IntMap Bool
state = (UN Sim (Value @ Ready a)
 -> (UN Sim (Value @ Ready b),
     Simulator
       (Sim (UN Sim (Value @ Ready a))) (Sim (UN Sim (Value @ Ready b)))))
-> Simulator
     (Sim (UN Sim (Value @ Ready a))) (Sim (UN Sim (Value @ Ready b)))
forall a1 b1.
(a1 -> (b1, Simulator (Sim a1) (Sim b1)))
-> Simulator (Sim a1) (Sim b1)
Simulator \UN Sim (Value @ Ready a)
input ->
        let initial :: IntMap Bool
initial = IntMap Bool -> IntMap Bool -> IntMap Bool
forall a. IntMap a -> IntMap a -> IntMap a
IM.union ([(Int, Bool)] -> IntMap Bool
forall a. [(Int, a)] -> IntMap a
IM.fromList (Bundle a -> UN Sim (Value @ Ready a) -> [(Int, Bool)]
forall (a :: Wires). Bundle a -> Sample a -> [(Int, Bool)]
inputValues Bundle a
ins UN Sim (Value @ Ready a)
input)) IntMap Bool
state
            evaluated :: IntMap Bool
evaluated = (IntMap Bool -> (Int, Driver) -> IntMap Bool)
-> IntMap Bool -> [(Int, Driver)] -> IntMap Bool
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' IntMap Bool -> (Int, Driver) -> IntMap Bool
evaluate IntMap Bool
initial [(Int, Driver)]
order
        in (Bundle b -> IntMap Bool -> UN Sim (Value @ Ready b)
forall (a :: Wires). Bundle a -> IntMap Bool -> Sample a
output Bundle b
outs IntMap Bool
evaluated, IntMap Bool
-> Simulator
     (Sim (UN Sim (Value @ Ready a))) (Sim (UN Sim (Value @ Ready b)))
run ((Int -> Bool) -> IntMap Int -> IntMap Bool
forall a b. (a -> b) -> IntMap a -> IntMap b
IM.map (IntMap Bool
evaluated IntMap Bool -> Int -> Bool
forall a. IntMap a -> Int -> a
IM.!) IntMap Int
registerInputs))
  pure (Prepared (run initialRegisters))
  where
    registers :: IntMap (Bool, Int)
registers = (Driver -> Maybe (Bool, Int))
-> IntMap Driver -> IntMap (Bool, Int)
forall a b. (a -> Maybe b) -> IntMap a -> IntMap b
IM.mapMaybe (\case Register Bool
b Int
i -> (Bool, Int) -> Maybe (Bool, Int)
forall a. a -> Maybe a
Just (Bool
b, Int
i); Driver
_ -> Maybe (Bool, Int)
forall a. Maybe a
Nothing) IntMap Driver
ds
    initialRegisters :: IntMap Bool
initialRegisters = ((Bool, Int) -> Bool) -> IntMap (Bool, Int) -> IntMap Bool
forall a b. (a -> b) -> IntMap a -> IntMap b
IM.map (Bool, Int) -> Bool
forall a b. (a, b) -> a
fst IntMap (Bool, Int)
registers
    registerInputs :: IntMap Int
registerInputs = ((Bool, Int) -> Int) -> IntMap (Bool, Int) -> IntMap Int
forall a b. (a -> b) -> IntMap a -> IntMap b
IM.map (Bool, Int) -> Int
forall a b. (a, b) -> b
snd IntMap (Bool, Int)
registers
    deps :: Driver -> [Int]
deps Register{} = []
    deps Driver
d = Driver -> [Int]
inputs Driver
d
    acyclic :: SCC (Int, Driver) -> Either CircuitError [(Int, Driver)]
acyclic (AcyclicSCC (Int
_, Driver
Input)) = [(Int, Driver)] -> Either CircuitError [(Int, Driver)]
forall a b. b -> Either a b
Right []
    acyclic (AcyclicSCC (Int
_, Register{})) = [(Int, Driver)] -> Either CircuitError [(Int, Driver)]
forall a b. b -> Either a b
Right []
    acyclic (AcyclicSCC (Int, Driver)
node) = [(Int, Driver)] -> Either CircuitError [(Int, Driver)]
forall a b. b -> Either a b
Right [(Int, Driver)
node]
    acyclic (CyclicSCC [(Int, Driver)]
ns) = CircuitError -> Either CircuitError [(Int, Driver)]
forall a b. a -> Either a b
Left ([Int] -> CircuitError
CombinationalCycle (((Int, Driver) -> Int) -> [(Int, Driver)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Driver) -> Int
forall a b. (a, b) -> a
fst [(Int, Driver)]
ns))
    evaluate :: IntMap Bool -> (Int, Driver) -> IntMap Bool
evaluate IntMap Bool
bs (Int
n, Driver
d) = Int -> Bool -> IntMap Bool -> IntMap Bool
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
n (Driver -> Bool
value Driver
d) IntMap Bool
bs
      where
        get :: Int -> Bool
get Int
a = IntMap Bool
bs IntMap Bool -> Int -> Bool
forall a. IntMap a -> Int -> a
IM.! Int
a
        value :: Driver -> Bool
value (Constant Bool
b) = Bool
b
        value (Not Int
a) = Bool -> Bool
not (Int -> Bool
get Int
a)
        value (And Int
a Int
b) = Int -> Bool
get Int
a Bool -> Bool -> Bool
&& Int -> Bool
get Int
b
        value (Or Int
a Int
b) = Int -> Bool
get Int
a Bool -> Bool -> Bool
|| Int -> Bool
get Int
b
        value (Xor Int
a Int
b) = Int -> Bool
get Int
a Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Int -> Bool
get Int
b
        value (Mux Int
s Int
a Int
b) = if Int -> Bool
get Int
s then Int -> Bool
get Int
a else Int -> Bool
get Int
b
        value (Alias Int
a) = Int -> Bool
get Int
a
        value Driver
_ = Int -> Bool
get Int
n

-- | Prepare a circuit once and simulate a sequence of clock cycles. Each output is observed
-- before the clock edge for the corresponding input.
simulate :: Circuit a b -> [Sample a] -> Either CircuitError [Sample b]
simulate :: forall (a :: Wires) (b :: Wires).
Circuit a b -> [Sample a] -> Either CircuitError [Sample b]
simulate Circuit a b
circuit [Sample a]
xs = do
  sim <- Netlist a b -> Either CircuitError (Prepared (Ready a) (Ready b))
forall (a :: Wires) (b :: Wires).
Netlist a b -> Either CircuitError (Prepared (Ready a) (Ready b))
prepare (Circuit a b -> Netlist a b
forall (a :: Wires) (b :: Wires). Circuit a b -> Netlist a b
netlist Circuit a b
circuit)
  pure (runSimulator (fmap @Value sim) xs) \\ sim