-- | Clocked state machines. Each step consumes one input and produces one output and the next
-- machine. Composition and tensor advance every component once per clock cycle.
--
-- >>> runSimulator (stateless not) [False, True]
-- [True,False]
-- >>> runSimulator (stateless (+ 1) . stateless (* 2)) [1 :: Int, 2]
-- [3,5]
module Proarrow.Category.Instance.Simulator
  ( SIMULATOR (..)
  , Simulator (..)
  , stateless
  , step
  , runSimulator
  ) where

import Data.Kind (Type)
import Prelude hiding (id, (**), (.))

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard)
import Proarrow.Core (CAT, CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault)
import Proarrow.Monoid (CocommutativeComonoid, Comonoid (..))

type data SIMULATOR = Sim Type

-- | A machine and its current state, represented by its next step.
type Simulator :: CAT SIMULATOR
data Simulator a b where
  Simulator :: (a -> (b, Simulator (Sim a) (Sim b))) -> Simulator (Sim a) (Sim b)

-- | Apply a function independently in every clock cycle.
stateless :: (a -> b) -> Simulator (Sim a) (Sim b)
stateless :: forall a b. (a -> b) -> Simulator (Sim a) (Sim b)
stateless a -> b
f = Simulator (Sim a) (Sim b)
machine
  where
    machine :: Simulator (Sim a) (Sim b)
machine = (a -> (b, Simulator (Sim a) (Sim b))) -> Simulator (Sim a) (Sim b)
forall a b.
(a -> (b, Simulator (Sim a) (Sim b))) -> Simulator (Sim a) (Sim b)
Simulator \a
x -> (a -> b
f a
x, Simulator (Sim a) (Sim b)
machine)

instance CategoryOf SIMULATOR where
  type (~>) = Simulator
  type Ob a = Is Sim a
instance Profunctor Simulator where
  dimap :: forall (c :: SIMULATOR) (a :: SIMULATOR) (b :: SIMULATOR)
       (d :: SIMULATOR).
(c ~> a) -> (b ~> d) -> Simulator a b -> Simulator c d
dimap = (c ~> a) -> (b ~> d) -> Simulator a b -> Simulator c d
Simulator c a -> Simulator b d -> Simulator a b -> Simulator 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 :: SIMULATOR) (b :: SIMULATOR) r.
((Ob a, Ob b) => r) -> Simulator a b -> r
\\ Simulator{} = r
(Ob a, Ob b) => r
r
instance Promonad Simulator where
  id :: forall (a :: SIMULATOR). Ob a => Simulator a a
id = (UN Sim a -> UN Sim a)
-> Simulator (Sim (UN Sim a)) (Sim (UN Sim a))
forall a b. (a -> b) -> Simulator (Sim a) (Sim b)
stateless \UN Sim a
x -> UN Sim a
x
  Simulator a -> (b, Simulator (Sim a) (Sim b))
f . :: forall (b :: SIMULATOR) (c :: SIMULATOR) (a :: SIMULATOR).
Simulator b c -> Simulator a b -> Simulator a c
. Simulator a -> (b, Simulator (Sim a) (Sim b))
g = (a -> (b, Simulator (Sim a) (Sim b))) -> Simulator (Sim a) (Sim b)
forall a b.
(a -> (b, Simulator (Sim a) (Sim b))) -> Simulator (Sim a) (Sim b)
Simulator \a
x ->
    let (b
y, Simulator (Sim a) (Sim b)
g') = a -> (b, Simulator (Sim a) (Sim b))
g a
x
        (b
z, Simulator (Sim a) (Sim b)
f') = a -> (b, Simulator (Sim a) (Sim b))
f a
b
y
    in (b
z, Simulator (Sim a) (Sim b)
f' Simulator (Sim a) (Sim b)
-> Simulator (Sim a) (Sim a) -> Simulator (Sim a) (Sim 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 (Sim a) (Sim a)
Simulator (Sim a) (Sim b)
g')
instance MonoidalProfunctor Simulator where
  one :: Simulator Unit Unit
one = Simulator Unit Unit
Simulator (Sim ()) (Sim ())
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: SIMULATOR). Ob a => Simulator a a
id
  Simulator a -> (b, Simulator (Sim a) (Sim b))
f ** :: forall (x1 :: SIMULATOR) (x2 :: SIMULATOR) (y1 :: SIMULATOR)
       (y2 :: SIMULATOR).
Simulator x1 x2
-> Simulator y1 y2 -> Simulator (x1 ** y1) (x2 ** y2)
** Simulator a -> (b, Simulator (Sim a) (Sim b))
g = ((a, a) -> ((b, b), Simulator (Sim (a, a)) (Sim (b, b))))
-> Simulator (Sim (a, a)) (Sim (b, b))
forall a b.
(a -> (b, Simulator (Sim a) (Sim b))) -> Simulator (Sim a) (Sim b)
Simulator \(a
x, a
y) ->
    let (b
x', Simulator (Sim a) (Sim b)
f') = a -> (b, Simulator (Sim a) (Sim b))
f a
x
        (b
y', Simulator (Sim a) (Sim b)
g') = a -> (b, Simulator (Sim a) (Sim b))
g a
y
    in ((b
x', b
y'), Simulator (Sim a) (Sim b)
f' Simulator (Sim a) (Sim b)
-> Simulator (Sim a) (Sim b)
-> Simulator (Sim a ** Sim a) (Sim b ** Sim 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 (Sim a) (Sim b)
g')
instance Monoidal SIMULATOR where
  type Unit = Sim ()
  type a ** b = Sim (UN Sim a, UN Sim b)
  withOb2 :: forall (a :: SIMULATOR) (b :: SIMULATOR) 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 :: SIMULATOR). Ob a => (Unit ** a) ~> a
leftUnitor = (((), UN Sim a) -> UN Sim a)
-> Simulator (Sim ((), UN Sim a)) (Sim (UN Sim a))
forall a b. (a -> b) -> Simulator (Sim a) (Sim b)
stateless \((), UN Sim a
x) -> UN Sim a
x
  leftUnitorInv :: forall (a :: SIMULATOR). Ob a => a ~> (Unit ** a)
leftUnitorInv = (UN Sim a -> ((), UN Sim a))
-> Simulator (Sim (UN Sim a)) (Sim ((), UN Sim a))
forall a b. (a -> b) -> Simulator (Sim a) (Sim b)
stateless ((),)
  rightUnitor :: forall (a :: SIMULATOR). Ob a => (a ** Unit) ~> a
rightUnitor = ((UN Sim a, ()) -> UN Sim a)
-> Simulator (Sim (UN Sim a, ())) (Sim (UN Sim a))
forall a b. (a -> b) -> Simulator (Sim a) (Sim b)
stateless \(UN Sim a
x, ()) -> UN Sim a
x
  rightUnitorInv :: forall (a :: SIMULATOR). Ob a => a ~> (a ** Unit)
rightUnitorInv = (UN Sim a -> (UN Sim a, ()))
-> Simulator (Sim (UN Sim a)) (Sim (UN Sim a, ()))
forall a b. (a -> b) -> Simulator (Sim a) (Sim b)
stateless (,())
  associator :: forall (a :: SIMULATOR) (b :: SIMULATOR) (c :: SIMULATOR).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator = (((UN Sim a, UN Sim b), UN Sim c)
 -> (UN Sim a, (UN Sim b, UN Sim c)))
-> Simulator
     (Sim ((UN Sim a, UN Sim b), UN Sim c))
     (Sim (UN Sim a, (UN Sim b, UN Sim c)))
forall a b. (a -> b) -> Simulator (Sim a) (Sim b)
stateless \((UN Sim a
x, UN Sim b
y), UN Sim c
z) -> (UN Sim a
x, (UN Sim b
y, UN Sim c
z))
  associatorInv :: forall (a :: SIMULATOR) (b :: SIMULATOR) (c :: SIMULATOR).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv = ((UN Sim a, (UN Sim b, UN Sim c))
 -> ((UN Sim a, UN Sim b), UN Sim c))
-> Simulator
     (Sim (UN Sim a, (UN Sim b, UN Sim c)))
     (Sim ((UN Sim a, UN Sim b), UN Sim c))
forall a b. (a -> b) -> Simulator (Sim a) (Sim b)
stateless \(UN Sim a
x, (UN Sim b
y, UN Sim c
z)) -> ((UN Sim a
x, UN Sim b
y), UN Sim c
z)
instance SymMonoidal SIMULATOR where
  swap :: forall (a :: SIMULATOR) (b :: SIMULATOR).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap = ((UN Sim a, UN Sim b) -> (UN Sim b, UN Sim a))
-> Simulator (Sim (UN Sim a, UN Sim b)) (Sim (UN Sim b, UN Sim a))
forall a b. (a -> b) -> Simulator (Sim a) (Sim b)
stateless \(UN Sim a
x, UN Sim b
y) -> (UN Sim b
y, UN Sim a
x)
instance (Ob a) => Comonoid (a :: SIMULATOR) where
  counit :: a ~> Unit
counit = (UN Sim a -> ()) -> Simulator (Sim (UN Sim a)) (Sim ())
forall a b. (a -> b) -> Simulator (Sim a) (Sim b)
stateless (() -> UN Sim a -> ()
forall a b. a -> b -> a
const ())
  comult :: a ~> (a ** a)
comult = (UN Sim a -> (UN Sim a, UN Sim a))
-> Simulator (Sim (UN Sim a)) (Sim (UN Sim a, UN Sim a))
forall a b. (a -> b) -> Simulator (Sim a) (Sim b)
stateless \UN Sim a
x -> (UN Sim a
x, UN Sim a
x)
instance (Ob a) => CocommutativeComonoid (a :: SIMULATOR)
instance CopyDiscard SIMULATOR

-- | Observe the current output and advance one clock cycle.
step :: Simulator (Sim a) (Sim b) -> a -> (b, Simulator (Sim a) (Sim b))
step :: forall a b.
Simulator (Sim a) (Sim b) -> a -> (b, Simulator (Sim a) (Sim b))
step (Simulator a -> (b, Simulator (Sim a) (Sim b))
run) = a -> (b, Simulator (Sim a) (Sim b))
a -> (b, Simulator (Sim a) (Sim b))
run

-- | Run a sequence of inputs, starting from the machine's current state.
runSimulator :: Simulator (Sim a) (Sim b) -> [a] -> [b]
runSimulator :: forall a b. Simulator (Sim a) (Sim b) -> [a] -> [b]
runSimulator Simulator (Sim a) (Sim b)
_ [] = []
runSimulator Simulator (Sim a) (Sim b)
machine (a
x : [a]
xs) =
  let (b
y, Simulator (Sim a) (Sim b)
next) = Simulator (Sim a) (Sim b) -> a -> (b, Simulator (Sim a) (Sim b))
forall a b.
Simulator (Sim a) (Sim b) -> a -> (b, Simulator (Sim a) (Sim b))
step Simulator (Sim a) (Sim b)
machine a
x
  in b
y b -> [b] -> [b]
forall a. a -> [a] -> [a]
: Simulator (Sim a) (Sim b) -> [a] -> [b]
forall a b. Simulator (Sim a) (Sim b) -> [a] -> [b]
runSimulator Simulator (Sim a) (Sim b)
next [a]
xs