{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

-- | A pointed Moore machine packaged as a @Circuit@ base arrow.
--
-- @
-- data Process a b = forall s. Process (a -> s) (s -> a -> s) (s -> b)
-- @
--
-- 'Process' is the monomial special case of 'Circuit.System.System': the
-- interface is @Mono a b@ and the initial state is supplied by the first input.
-- The underlying span-shaped carrier is 'Circuit.Body.Body'.
--
-- * @inject@ converts the first input into an initial state.
-- * @step@ updates the state given the current input.
-- * @extract@ produces the output from the current state.
--
-- This is the circuits-native carrier for streaming state machines. It is
-- intended to replace the hand-rolled state-machine arrow: stats packages
-- become boxes @Process a b@, while the arrow itself lives in the substrate
-- next to 'Circuit.Trace' and 'Circuit.Net'.
--
-- The semantics are intentionally tied to the circuits substrate:
--
-- * 'scan' is the reference runner over lists.
-- * 'scanStream' generalizes this to any 'Uncons' input and 'Cons' output.
-- * 'encode' maps a process into a stream-level 'Trace' 'Either' @(->)@ over
--   lists; the two runners are verified equivalent by oracle.
-- * The arrow-level 'Traced' Either instance is per-tick Conway/Elgot settle,
--   not cross-tick state feedback; see 'register' for the latter.
--
-- = Pointed systems
--
-- The pointed-Moore view of a stateful morphism is 'Circuit.System.System' with
-- an explicit seed.  Use 'Circuit.System.mooreSystem' to build such a system,
-- and 'systemToProcess' to turn it into a first-input-seeded 'Process'.
module Circuit.Process
  ( -- * Stream transformer (monomial special case)
    Process (..),

    -- * Boundary tokens (K + payload)
    Boundary (..),
    isMark,
    isPayload,

    -- * System <-> Process conversions
    systemToProcess,
    systemAsProcess,
    markSystem,

    -- * Runners
    iterateSystem,
    after,
    scan,
    scanStream,
    fold,
    foldStream,
    encode,
    encodeStream,

    -- * Mealy-style processes
    mealy,
    runMealy,
    runMealyStream,

    -- * Cross-tick feedback
    delay,
    register,

    -- * Body conversions
    processToBody,
    processToSomeBody,
  )
where

import Circuit.Bimonoid (Copy, CopyDiscard, Discard, Merge, MergeZero, Zero)
import Circuit.Bimonoid qualified as Bm
import Circuit.Body (Body (..), SomeBody (..))
import Circuit.Category (Category (..))
import Circuit.Channel (Channel (..), Strength (..), Traced (..))
import Circuit.Poly (Mono, Pos)
import Circuit.Shared (Bias (..), Pick (..), Schedule (..), Shared (..), chooseS)
import Circuit.Stream (Cons (..), Uncons (..))
import Circuit.System (System, mooreSystem, runSystem, runSystemMono)
import Circuit.Tensor (Action (..), Tensor (..), Unital (..))
import Circuit.Trace (Trace, base, yank)
import Data.Bifunctor (Bifunctor (..))
import Data.Maybe (fromMaybe)
import Data.These (These (..))
import Prelude hiding (id, (.))

-- $setup
-- >>> import Circuit.Process
-- >>> import Prelude hiding (id, (.))

-- * Boundary tokens (K + payload)

-- | The free boundary @K + payload@.
--
-- A token on the boundary is either a mark from a finite alphabet @k@ or a
-- payload value @a@.  This is the level-0 grammar of process boundaries:
-- marks are the control tokens, payloads are the data.
--
-- 'fmap' acts only on the payload side; marks are carried through unchanged.
--
-- >>> fmap length (Payload "hi")
-- Payload 2
-- >>> fmap length (Mark "halt")
-- Mark "halt"
data Boundary k a
  = -- | Control token from the finite mark alphabet.
    Mark k
  | -- | Data-carrying payload.
    Payload a
  deriving (Boundary k a -> Boundary k a -> Bool
(Boundary k a -> Boundary k a -> Bool)
-> (Boundary k a -> Boundary k a -> Bool) -> Eq (Boundary k a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k a. (Eq k, Eq a) => Boundary k a -> Boundary k a -> Bool
$c== :: forall k a. (Eq k, Eq a) => Boundary k a -> Boundary k a -> Bool
== :: Boundary k a -> Boundary k a -> Bool
$c/= :: forall k a. (Eq k, Eq a) => Boundary k a -> Boundary k a -> Bool
/= :: Boundary k a -> Boundary k a -> Bool
Eq, Int -> Boundary k a -> ShowS
[Boundary k a] -> ShowS
Boundary k a -> String
(Int -> Boundary k a -> ShowS)
-> (Boundary k a -> String)
-> ([Boundary k a] -> ShowS)
-> Show (Boundary k a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k a. (Show k, Show a) => Int -> Boundary k a -> ShowS
forall k a. (Show k, Show a) => [Boundary k a] -> ShowS
forall k a. (Show k, Show a) => Boundary k a -> String
$cshowsPrec :: forall k a. (Show k, Show a) => Int -> Boundary k a -> ShowS
showsPrec :: Int -> Boundary k a -> ShowS
$cshow :: forall k a. (Show k, Show a) => Boundary k a -> String
show :: Boundary k a -> String
$cshowList :: forall k a. (Show k, Show a) => [Boundary k a] -> ShowS
showList :: [Boundary k a] -> ShowS
Show, (forall a b. (a -> b) -> Boundary k a -> Boundary k b)
-> (forall a b. a -> Boundary k b -> Boundary k a)
-> Functor (Boundary k)
forall a b. a -> Boundary k b -> Boundary k a
forall a b. (a -> b) -> Boundary k a -> Boundary k b
forall k a b. a -> Boundary k b -> Boundary k a
forall k a b. (a -> b) -> Boundary k a -> Boundary k b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall k a b. (a -> b) -> Boundary k a -> Boundary k b
fmap :: forall a b. (a -> b) -> Boundary k a -> Boundary k b
$c<$ :: forall k a b. a -> Boundary k b -> Boundary k a
<$ :: forall a b. a -> Boundary k b -> Boundary k a
Functor, (forall m. Monoid m => Boundary k m -> m)
-> (forall m a. Monoid m => (a -> m) -> Boundary k a -> m)
-> (forall m a. Monoid m => (a -> m) -> Boundary k a -> m)
-> (forall a b. (a -> b -> b) -> b -> Boundary k a -> b)
-> (forall a b. (a -> b -> b) -> b -> Boundary k a -> b)
-> (forall b a. (b -> a -> b) -> b -> Boundary k a -> b)
-> (forall b a. (b -> a -> b) -> b -> Boundary k a -> b)
-> (forall a. (a -> a -> a) -> Boundary k a -> a)
-> (forall a. (a -> a -> a) -> Boundary k a -> a)
-> (forall a. Boundary k a -> [a])
-> (forall a. Boundary k a -> Bool)
-> (forall a. Boundary k a -> Int)
-> (forall a. Eq a => a -> Boundary k a -> Bool)
-> (forall a. Ord a => Boundary k a -> a)
-> (forall a. Ord a => Boundary k a -> a)
-> (forall a. Num a => Boundary k a -> a)
-> (forall a. Num a => Boundary k a -> a)
-> Foldable (Boundary k)
forall a. Eq a => a -> Boundary k a -> Bool
forall a. Num a => Boundary k a -> a
forall a. Ord a => Boundary k a -> a
forall m. Monoid m => Boundary k m -> m
forall a. Boundary k a -> Bool
forall a. Boundary k a -> Int
forall a. Boundary k a -> [a]
forall a. (a -> a -> a) -> Boundary k a -> a
forall k a. Eq a => a -> Boundary k a -> Bool
forall k a. Num a => Boundary k a -> a
forall k a. Ord a => Boundary k a -> a
forall k m. Monoid m => Boundary k m -> m
forall m a. Monoid m => (a -> m) -> Boundary k a -> m
forall k a. Boundary k a -> Bool
forall k a. Boundary k a -> Int
forall k a. Boundary k a -> [a]
forall b a. (b -> a -> b) -> b -> Boundary k a -> b
forall a b. (a -> b -> b) -> b -> Boundary k a -> b
forall k a. (a -> a -> a) -> Boundary k a -> a
forall k m a. Monoid m => (a -> m) -> Boundary k a -> m
forall k b a. (b -> a -> b) -> b -> Boundary k a -> b
forall k a b. (a -> b -> b) -> b -> Boundary k a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall k m. Monoid m => Boundary k m -> m
fold :: forall m. Monoid m => Boundary k m -> m
$cfoldMap :: forall k m a. Monoid m => (a -> m) -> Boundary k a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Boundary k a -> m
$cfoldMap' :: forall k m a. Monoid m => (a -> m) -> Boundary k a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Boundary k a -> m
$cfoldr :: forall k a b. (a -> b -> b) -> b -> Boundary k a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Boundary k a -> b
$cfoldr' :: forall k a b. (a -> b -> b) -> b -> Boundary k a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Boundary k a -> b
$cfoldl :: forall k b a. (b -> a -> b) -> b -> Boundary k a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Boundary k a -> b
$cfoldl' :: forall k b a. (b -> a -> b) -> b -> Boundary k a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Boundary k a -> b
$cfoldr1 :: forall k a. (a -> a -> a) -> Boundary k a -> a
foldr1 :: forall a. (a -> a -> a) -> Boundary k a -> a
$cfoldl1 :: forall k a. (a -> a -> a) -> Boundary k a -> a
foldl1 :: forall a. (a -> a -> a) -> Boundary k a -> a
$ctoList :: forall k a. Boundary k a -> [a]
toList :: forall a. Boundary k a -> [a]
$cnull :: forall k a. Boundary k a -> Bool
null :: forall a. Boundary k a -> Bool
$clength :: forall k a. Boundary k a -> Int
length :: forall a. Boundary k a -> Int
$celem :: forall k a. Eq a => a -> Boundary k a -> Bool
elem :: forall a. Eq a => a -> Boundary k a -> Bool
$cmaximum :: forall k a. Ord a => Boundary k a -> a
maximum :: forall a. Ord a => Boundary k a -> a
$cminimum :: forall k a. Ord a => Boundary k a -> a
minimum :: forall a. Ord a => Boundary k a -> a
$csum :: forall k a. Num a => Boundary k a -> a
sum :: forall a. Num a => Boundary k a -> a
$cproduct :: forall k a. Num a => Boundary k a -> a
product :: forall a. Num a => Boundary k a -> a
Foldable, Functor (Boundary k)
Foldable (Boundary k)
(Functor (Boundary k), Foldable (Boundary k)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Boundary k a -> f (Boundary k b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Boundary k (f a) -> f (Boundary k a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Boundary k a -> m (Boundary k b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Boundary k (m a) -> m (Boundary k a))
-> Traversable (Boundary k)
forall k. Functor (Boundary k)
forall k. Foldable (Boundary k)
forall k (m :: * -> *) a.
Monad m =>
Boundary k (m a) -> m (Boundary k a)
forall k (f :: * -> *) a.
Applicative f =>
Boundary k (f a) -> f (Boundary k a)
forall k (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Boundary k a -> m (Boundary k b)
forall k (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Boundary k a -> f (Boundary k b)
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
Boundary k (m a) -> m (Boundary k a)
forall (f :: * -> *) a.
Applicative f =>
Boundary k (f a) -> f (Boundary k a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Boundary k a -> m (Boundary k b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Boundary k a -> f (Boundary k b)
$ctraverse :: forall k (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Boundary k a -> f (Boundary k b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Boundary k a -> f (Boundary k b)
$csequenceA :: forall k (f :: * -> *) a.
Applicative f =>
Boundary k (f a) -> f (Boundary k a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Boundary k (f a) -> f (Boundary k a)
$cmapM :: forall k (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Boundary k a -> m (Boundary k b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Boundary k a -> m (Boundary k b)
$csequence :: forall k (m :: * -> *) a.
Monad m =>
Boundary k (m a) -> m (Boundary k a)
sequence :: forall (m :: * -> *) a.
Monad m =>
Boundary k (m a) -> m (Boundary k a)
Traversable)

instance Bifunctor Boundary where
  bimap :: forall a b c d.
(a -> b) -> (c -> d) -> Boundary a c -> Boundary b d
bimap a -> b
f c -> d
_ (Mark a
k) = b -> Boundary b d
forall k a. k -> Boundary k a
Mark (a -> b
f a
k)
  bimap a -> b
_ c -> d
g (Payload c
a) = d -> Boundary b d
forall k a. a -> Boundary k a
Payload (c -> d
g c
a)

-- | True iff the token is a 'Mark'.
isMark :: Boundary k a -> Bool
isMark :: forall k a. Boundary k a -> Bool
isMark (Mark k
_) = Bool
True
isMark (Payload a
_) = Bool
False

-- | True iff the token is a 'Payload'.
isPayload :: Boundary k a -> Bool
isPayload :: forall k a. Boundary k a -> Bool
isPayload (Mark k
_) = Bool
False
isPayload (Payload a
_) = Bool
True

-- | A stateful process from @a@ to @b@.
--
-- The existential state type @s@ is hidden; the observable interface is the
-- triple @inject / step / extract@. Keeping the triple as the primitive (rather
-- than fusing @extract@ into the step) preserves the streaming-statistics
-- invariant that the first output is @extract (inject x)@, before any step.
data Process a b where
  Process ::
    forall s a b.
    (a -> s) ->
    (s -> a -> s) ->
    (s -> b) ->
    Process a b

-- | Convert a monomial 'System', an explicit seed, and a state observation
-- into a first-input-seeded 'Process'.
--
-- The observation @s -> b@ is applied to the /current/ state to produce each
-- output, including the first output from the seed.  The step system is used
-- only for state transitions.
systemToProcess :: s -> (s -> b) -> System (->) s (Mono a b) -> Process a b
systemToProcess :: forall s b a.
s -> (s -> b) -> System (->) s (Mono a b) -> Process a b
systemToProcess s
s0 s -> b
ex System (->) s (Mono a b)
sys =
  (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process
    (\a
a -> (s, (b, ())) -> s
forall a b. (a, b) -> a
fst (System (->) s (Mono a b)
-> (s, Dir (Mono a b)) -> (s, Pos (Mono a b))
forall (arr :: * -> * -> *) s (p :: Poly).
System arr s p -> arr (s, Dir p) (s, Pos p)
runSystem System (->) s (Mono a b)
sys (s
s0, a -> Either Void a
forall a b. b -> Either a b
Right a
a)))
    (\s
s a
a -> (s, (b, ())) -> s
forall a b. (a, b) -> a
fst (System (->) s (Mono a b)
-> (s, Dir (Mono a b)) -> (s, Pos (Mono a b))
forall (arr :: * -> * -> *) s (p :: Poly).
System arr s p -> arr (s, Dir p) (s, Pos p)
runSystem System (->) s (Mono a b)
sys (s
s, a -> Either Void a
forall a b. b -> Either a b
Right a
a)))
    s -> b
ex

-- | Convert a monomial 'System' into a 'Process' machine with a given initial
-- state.
--
-- The first input is consumed for the state transition from the supplied
-- initial state, matching the coalgebra intuition of a 'System'.
systemAsProcess :: System (->) s (Mono i o) -> s -> Process i o
systemAsProcess :: forall s i o. System (->) s (Mono i o) -> s -> Process i o
systemAsProcess System (->) s (Mono i o)
sys s
s0 =
  (i -> s) -> (s -> i -> s) -> (s -> o) -> Process i o
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process
    ((o, i -> s) -> i -> s
forall a b. (a, b) -> b
snd (System (->) s (Mono i o) -> s -> (o, i -> s)
forall s i o. System (->) s (Mono i o) -> s -> (o, i -> s)
runSystemMono System (->) s (Mono i o)
sys s
s0))
    ((o, i -> s) -> i -> s
forall a b. (a, b) -> b
snd ((o, i -> s) -> i -> s) -> (s -> (o, i -> s)) -> s -> i -> s
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. System (->) s (Mono i o) -> s -> (o, i -> s)
forall s i o. System (->) s (Mono i o) -> s -> (o, i -> s)
runSystemMono System (->) s (Mono i o)
sys)
    ((o, i -> s) -> o
forall a b. (a, b) -> a
fst ((o, i -> s) -> o) -> (s -> (o, i -> s)) -> s -> o
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. System (->) s (Mono i o) -> s -> (o, i -> s)
forall s i o. System (->) s (Mono i o) -> s -> (o, i -> s)
runSystemMono System (->) s (Mono i o)
sys)

-- | Run a system for as many steps as there are inputs, emitting one output
-- per input. The output is the state /after/ consuming the input, matching
-- the 'Process' semantics of 'systemAsProcess'.
iterateSystem :: System (->) s (Mono i o) -> s -> [i] -> [o]
iterateSystem :: forall s i o. System (->) s (Mono i o) -> s -> [i] -> [o]
iterateSystem System (->) s (Mono i o)
_ s
_ [] = []
iterateSystem System (->) s (Mono i o)
sys s
s (i
i : [i]
is) =
  let s' :: s
s' = (o, i -> s) -> i -> s
forall a b. (a, b) -> b
snd (System (->) s (Mono i o) -> s -> (o, i -> s)
forall s i o. System (->) s (Mono i o) -> s -> (o, i -> s)
runSystemMono System (->) s (Mono i o)
sys s
s) i
i
      (o
o, i -> s
_) = System (->) s (Mono i o) -> s -> (o, i -> s)
forall s i o. System (->) s (Mono i o) -> s -> (o, i -> s)
runSystemMono System (->) s (Mono i o)
sys s
s'
   in o
o o -> [o] -> [o]
forall a. a -> [a] -> [a]
: System (->) s (Mono i o) -> s -> [i] -> [o]
forall s i o. System (->) s (Mono i o) -> s -> [i] -> [o]
iterateSystem System (->) s (Mono i o)
sys s
s' [i]
is

-- | State after consuming a list of inputs.
after :: System (->) s (Mono i o) -> s -> [i] -> s
after :: forall s i o. System (->) s (Mono i o) -> s -> [i] -> s
after System (->) s (Mono i o)
_ s
s [] = s
s
after System (->) s (Mono i o)
sys s
s (i
i : [i]
is) = System (->) s (Mono i o) -> s -> [i] -> s
forall s i o. System (->) s (Mono i o) -> s -> [i] -> s
after System (->) s (Mono i o)
sys ((o, i -> s) -> i -> s
forall a b. (a, b) -> b
snd (System (->) s (Mono i o) -> s -> (o, i -> s)
forall s i o. System (->) s (Mono i o) -> s -> (o, i -> s)
runSystemMono System (->) s (Mono i o)
sys s
s) i
i) [i]
is

-- | Lift a monomial 'System' and a state observation into a boundary system
-- over 'Boundary' tokens.
--
-- Payloads are stepped through the inner system.  Marks satisfying the halt
-- predicate freeze the system and produce 'Nothing' thereafter; non-halt
-- marks leave the state unchanged and emit the current output.  The halted
-- state remembers the final inner state.
--
-- The returned system carries state @Either s s@: 'Left' is running, 'Right'
-- is halted.  This is the core combinator behind mark-driven halt: the finite
-- mark alphabet @k@ carries control tokens, while payloads carry data.
markSystem ::
  (k -> Bool) ->
  (s -> b) ->
  System (->) s (Mono a b) ->
  System (->) (Either s s) (Mono (Boundary k a) (Maybe b))
markSystem :: forall k s b a.
(k -> Bool)
-> (s -> b)
-> System (->) s (Mono a b)
-> System (->) (Either s s) (Mono (Boundary k a) (Maybe b))
markSystem k -> Bool
isHalt s -> b
ex System (->) s (Mono a b)
sys =
  (Either s s -> Boundary k a -> Either s s)
-> (Either s s -> Maybe b)
-> System (->) (Either s s) (Mono (Boundary k a) (Maybe b))
forall s a b. (s -> a -> s) -> (s -> b) -> System (->) s (Mono a b)
mooreSystem
    ( \Either s s
s Boundary k a
tok -> case (Either s s
s, Boundary k a
tok) of
        (Left s
s', Payload a
a) -> s -> Either s s
forall a b. a -> Either a b
Left ((s, (b, ())) -> s
forall a b. (a, b) -> a
fst (System (->) s (Mono a b)
-> (s, Dir (Mono a b)) -> (s, Pos (Mono a b))
forall (arr :: * -> * -> *) s (p :: Poly).
System arr s p -> arr (s, Dir p) (s, Pos p)
runSystem System (->) s (Mono a b)
sys (s
s', a -> Either Void a
forall a b. b -> Either a b
Right a
a)))
        (Left s
s', Mark k
k) -> if k -> Bool
isHalt k
k then s -> Either s s
forall a b. b -> Either a b
Right s
s' else s -> Either s s
forall a b. a -> Either a b
Left s
s'
        (Right s
s', Boundary k a
_) -> s -> Either s s
forall a b. b -> Either a b
Right s
s'
    )
    ( \case
        Left s
s -> b -> Maybe b
forall a. a -> Maybe a
Just (s -> b
ex s
s)
        Right s
_ -> Maybe b
forall a. Maybe a
Nothing
    )

-- * Category

instance Category Process where
  id :: Process a a
  id :: forall a. Process a a
id = (a -> a) -> (a -> a -> a) -> (a -> a) -> Process a a
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process a -> a
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id a -> a -> a
forall a b. a -> b -> a
const a -> a
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id
  {-# INLINE id #-}

  (.) :: Process b c -> Process a b -> Process a c
  Process b -> s
i2 s -> b -> s
st2 s -> c
ex2 . :: forall b c a. Process b c -> Process a b -> Process a c
. Process a -> s
i1 s -> a -> s
st1 s -> b
ex1 =
    (a -> (s, s))
-> ((s, s) -> a -> (s, s)) -> ((s, s) -> c) -> Process a c
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process
      (\a
a -> let s1 :: s
s1 = a -> s
i1 a
a in (s
s1, b -> s
i2 (s -> b
ex1 s
s1)))
      ( \(s
s1, s
s2) a
a ->
          let s1' :: s
s1' = s -> a -> s
st1 s
s1 a
a
              s2' :: s
s2' = s -> b -> s
st2 s
s2 (s -> b
ex1 s
s1')
           in (s
s1', s
s2')
      )
      (\(s
_, s
s2) -> s -> c
ex2 s
s2)
  {-# INLINE (.) #-}

-- Channel / Strength / Traced for (,)
--
-- These instances make Process a traced monoidal category under the cartesian
-- tensor. The trace ties a lazy self-referential knot and is productive only
-- when the body is non-strict in the feedback channel. Strict accumulators
-- (e.g. moving averages) diverge under the (,) trace; use Either-trace 'run'
-- or the 'register' combinator for those.

instance Channel (,) Process where
  assoc :: forall a b c. Process ((a, b), c) (a, (b, c))
assoc = (((a, b), c) -> ((a, b), c))
-> (((a, b), c) -> ((a, b), c) -> ((a, b), c))
-> (((a, b), c) -> (a, (b, c)))
-> Process ((a, b), c) (a, (b, c))
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process ((a, b), c) -> ((a, b), c)
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id (\((a, b), c)
_ ((a, b), c)
x -> ((a, b), c)
x) (\(~((a
a, b
b), c
c)) -> (a
a, (b
b, c
c)))
  assoc' :: forall a b c. Process (a, (b, c)) ((a, b), c)
assoc' = ((a, (b, c)) -> (a, (b, c)))
-> ((a, (b, c)) -> (a, (b, c)) -> (a, (b, c)))
-> ((a, (b, c)) -> ((a, b), c))
-> Process (a, (b, c)) ((a, b), c)
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process (a, (b, c)) -> (a, (b, c))
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id (\(a, (b, c))
_ (a, (b, c))
x -> (a, (b, c))
x) (\(a
a, ~(b
b, c
c)) -> ((a
a, b
b), c
c))
  slide :: forall a b c. Process (a, (b, c)) (b, (a, c))
slide = ((a, (b, c)) -> (a, (b, c)))
-> ((a, (b, c)) -> (a, (b, c)) -> (a, (b, c)))
-> ((a, (b, c)) -> (b, (a, c)))
-> Process (a, (b, c)) (b, (a, c))
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process (a, (b, c)) -> (a, (b, c))
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id (\(a, (b, c))
_ (a, (b, c))
x -> (a, (b, c))
x) (\(a
a, ~(b
b, c
c)) -> (b
b, (a
a, c
c)))

instance Strength (,) Process where
  strength :: forall b c a. Process b c -> Process (a, b) (a, c)
strength (Process b -> s
i s -> b -> s
st s -> c
ex) =
    ((a, b) -> (a, s))
-> ((a, s) -> (a, b) -> (a, s))
-> ((a, s) -> (a, c))
-> Process (a, b) (a, c)
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process
      (\(~(a
a, b
b)) -> (a
a, b -> s
i b
b))
      (\(~(a
_, s
s)) (~(a
a', b
b)) -> (a
a', s -> b -> s
st s
s b
b))
      (\(~(a
a, s
s)) -> (a
a, s -> c
ex s
s))

instance Traced (,) Process where
  trace :: forall a b c. Process (a, b) (a, c) -> Process b c
trace (Process (a, b) -> s
i s -> (a, b) -> s
st s -> (a, c)
ex) =
    (b -> s) -> (s -> b -> s) -> (s -> c) -> Process b c
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process
      (\b
b -> let s0 :: s
s0 = (a, b) -> s
i (a
a0, b
b); a0 :: a
a0 = (a, c) -> a
forall a b. (a, b) -> a
fst (s -> (a, c)
ex s
s0) in s
s0)
      ( \s
s b
b ->
          let (s
s', a
_a) = ((s, a) -> (s, a)) -> (s, a)
forall {t}. (t -> t) -> t
fix (\ ~(s
s'', a
a') -> (s -> (a, b) -> s
st s
s (a
a', b
b), (a, c) -> a
forall a b. (a, b) -> a
fst (s -> (a, c)
ex s
s'')))
           in s
s'
      )
      ((a, c) -> c
forall a b. (a, b) -> b
snd ((a, c) -> c) -> (s -> (a, c)) -> s -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. s -> (a, c)
ex)
    where
      fix :: (t -> t) -> t
fix t -> t
f = let x :: t
x = t -> t
f t
x in t
x

-- Tensor / Action / Shared for (,)
--
-- These instances make @Process@ a cartesian monoidal category in its own
-- right, so it can serve as a base category for shared-medium fusion and
-- for @Trace (,) Process@.

instance Unital (,) Process where
  unitl :: forall a. Process (Unit (,), a) a
unitl = (((), a) -> a)
-> (a -> ((), a) -> a) -> (a -> a) -> Process ((), a) a
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process ((), a) -> a
forall a b. (a, b) -> b
snd (\a
_ (()
_, a
a) -> a
a) a -> a
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id
  unitl' :: forall a. Process a (Unit (,), a)
unitl' = (a -> a) -> (a -> a -> a) -> (a -> ((), a)) -> Process a ((), a)
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process a -> a
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id a -> a -> a
forall a b. a -> b -> a
const ((),)
  unitr :: forall a. Process (a, Unit (,)) a
unitr = ((a, ()) -> a)
-> (a -> (a, ()) -> a) -> (a -> a) -> Process (a, ()) a
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process (a, ()) -> a
forall a b. (a, b) -> a
fst (\a
_ (a
a, ()) -> a
a) a -> a
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id
  unitr' :: forall a. Process a (a, Unit (,))
unitr' = (a -> a) -> (a -> a -> a) -> (a -> (a, ())) -> Process a (a, ())
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process a -> a
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id a -> a -> a
forall a b. a -> b -> a
const (,())

instance Tensor (,) Process where
  tensor :: forall a b c d. Process a b -> Process c d -> Process (a, c) (b, d)
tensor (Process a -> s
i1 s -> a -> s
st1 s -> b
ex1) (Process c -> s
i2 s -> c -> s
st2 s -> d
ex2) =
    ((a, c) -> (s, s))
-> ((s, s) -> (a, c) -> (s, s))
-> ((s, s) -> (b, d))
-> Process (a, c) (b, d)
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process
      ((a -> s) -> (c -> s) -> (a, c) -> (s, s)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a -> s
i1 c -> s
i2)
      (\(s
s1, s
s2) (a
a, c
c) -> (s -> a -> s
st1 s
s1 a
a, s -> c -> s
st2 s
s2 c
c))
      ((s -> b) -> (s -> d) -> (s, s) -> (b, d)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap s -> b
ex1 s -> d
ex2)
  {-# INLINE tensor #-}

instance Action (,) Process where
  braid :: forall a b. Process (a, b) (b, a)
braid = ((a, b) -> (a, b))
-> ((a, b) -> (a, b) -> (a, b))
-> ((a, b) -> (b, a))
-> Process (a, b) (b, a)
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process (a, b) -> (a, b)
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id (((a, b) -> (a, b)) -> (a, b) -> (a, b) -> (a, b)
forall a b. a -> b -> a
const (a, b) -> (a, b)
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id) (a, b) -> (b, a)
forall {b} {a}. (b, a) -> (a, b)
sw
    where
      sw :: (b, a) -> (a, b)
sw (b
a, a
b) = (a
b, b
a)
  {-# INLINE braid #-}

-- | Cartesian shared fusion on processes.
--
-- The two processes share one feedback channel @s@. At each tick the schedule
-- chooses which body advances; the gated body's input is discarded and it does
-- not step. Each process is injected lazily on its first firing, so a body that
-- is never scheduled consumes no inputs and produces no outputs.
instance Shared (,) Process where
  sharedBy :: forall s a b c d.
Schedule s
-> Process (s, a) (s, b)
-> Process (s, c) (s, d)
-> Process (s, (a, c)) (s, These b d)
sharedBy Schedule s
sched (Process (s, a) -> s
iL s -> (s, a) -> s
stL s -> (s, b)
exL) (Process (s, c) -> s
iR s -> (s, c) -> s
stR s -> (s, d)
exR) =
    ((s, (a, c)) -> (Maybe s, Maybe s, s, These b d))
-> ((Maybe s, Maybe s, s, These b d)
    -> (s, (a, c)) -> (Maybe s, Maybe s, s, These b d))
-> ((Maybe s, Maybe s, s, These b d) -> (s, These b d))
-> Process (s, (a, c)) (s, These b d)
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process (s, (a, c)) -> (Maybe s, Maybe s, s, These b d)
inject (Maybe s, Maybe s, s, These b d)
-> (s, (a, c)) -> (Maybe s, Maybe s, s, These b d)
step (Maybe s, Maybe s, s, These b d) -> (s, These b d)
forall {a} {b} {a} {b}. (a, b, a, b) -> (a, b)
extract
    where
      inject :: (s, (a, c)) -> (Maybe s, Maybe s, s, These b d)
inject (s
s, (a
a, c
c)) =
        let (s
s', Pick
pick) = Schedule s -> s -> (s, Pick)
forall s. Schedule s -> s -> (s, Pick)
chooseS Schedule s
sched s
s
         in Pick -> s -> a -> c -> (Maybe s, Maybe s, s, These b d)
runInject Pick
pick s
s' a
a c
c

      step :: (Maybe s, Maybe s, s, These b d)
-> (s, (a, c)) -> (Maybe s, Maybe s, s, These b d)
step (Maybe s
msL, Maybe s
msR, s
_, These b d
_) (s
sIn, (a
a, c
c)) =
        let (s
s', Pick
pick) = Schedule s -> s -> (s, Pick)
forall s. Schedule s -> s -> (s, Pick)
chooseS Schedule s
sched s
sIn
         in Pick
-> Maybe s
-> Maybe s
-> s
-> a
-> c
-> (Maybe s, Maybe s, s, These b d)
runStep Pick
pick Maybe s
msL Maybe s
msR s
s' a
a c
c

      extract :: (a, b, a, b) -> (a, b)
extract (a
_, b
_, a
s, b
out) = (a
s, b
out)

      runInject :: Pick -> s -> a -> c -> (Maybe s, Maybe s, s, These b d)
runInject Pick
pick s
s' a
a c
c = case Pick
pick of
        Pick
L ->
          let sL0 :: s
sL0 = (s, a) -> s
iL (s
s', a
a)
              (s
s'', b
b) = s -> (s, b)
exL s
sL0
           in (s -> Maybe s
forall a. a -> Maybe a
Just s
sL0, Maybe s
forall a. Maybe a
Nothing, s
s'', b -> These b d
forall a b. a -> These a b
This b
b)
        Pick
R ->
          let sR0 :: s
sR0 = (s, c) -> s
iR (s
s', c
c)
              (s
s'', d
d) = s -> (s, d)
exR s
sR0
           in (Maybe s
forall a. Maybe a
Nothing, s -> Maybe s
forall a. a -> Maybe a
Just s
sR0, s
s'', d -> These b d
forall a b. b -> These a b
That d
d)
        Both Bias
LeftFirst ->
          let sL0 :: s
sL0 = (s, a) -> s
iL (s
s', a
a)
              (s
sMid, b
b) = s -> (s, b)
exL s
sL0
              sR0 :: s
sR0 = (s, c) -> s
iR (s
sMid, c
c)
              (s
sOut, d
d) = s -> (s, d)
exR s
sR0
           in (s -> Maybe s
forall a. a -> Maybe a
Just s
sL0, s -> Maybe s
forall a. a -> Maybe a
Just s
sR0, s
sOut, b -> d -> These b d
forall a b. a -> b -> These a b
These b
b d
d)
        Both Bias
RightFirst ->
          let sR0 :: s
sR0 = (s, c) -> s
iR (s
s', c
c)
              (s
sMid, d
d) = s -> (s, d)
exR s
sR0
              sL0 :: s
sL0 = (s, a) -> s
iL (s
sMid, a
a)
              (s
sOut, b
b) = s -> (s, b)
exL s
sL0
           in (s -> Maybe s
forall a. a -> Maybe a
Just s
sL0, s -> Maybe s
forall a. a -> Maybe a
Just s
sR0, s
sOut, b -> d -> These b d
forall a b. a -> b -> These a b
These b
b d
d)

      runStep :: Pick
-> Maybe s
-> Maybe s
-> s
-> a
-> c
-> (Maybe s, Maybe s, s, These b d)
runStep Pick
pick Maybe s
msL Maybe s
msR s
s' a
a c
c = case Pick
pick of
        Pick
L ->
          let sL :: s
sL = s -> Maybe s -> s
forall a. a -> Maybe a -> a
fromMaybe ((s, a) -> s
iL (s
s', a
a)) Maybe s
msL
              sL' :: s
sL' = s -> (s, a) -> s
stL s
sL (s
s', a
a)
              (s
s'', b
b) = s -> (s, b)
exL s
sL'
           in (s -> Maybe s
forall a. a -> Maybe a
Just s
sL', Maybe s
msR, s
s'', b -> These b d
forall a b. a -> These a b
This b
b)
        Pick
R ->
          let sR :: s
sR = s -> Maybe s -> s
forall a. a -> Maybe a -> a
fromMaybe ((s, c) -> s
iR (s
s', c
c)) Maybe s
msR
              sR' :: s
sR' = s -> (s, c) -> s
stR s
sR (s
s', c
c)
              (s
s'', d
d) = s -> (s, d)
exR s
sR'
           in (Maybe s
msL, s -> Maybe s
forall a. a -> Maybe a
Just s
sR', s
s'', d -> These b d
forall a b. b -> These a b
That d
d)
        Both Bias
LeftFirst ->
          let sL :: s
sL = s -> Maybe s -> s
forall a. a -> Maybe a -> a
fromMaybe ((s, a) -> s
iL (s
s', a
a)) Maybe s
msL
              sL' :: s
sL' = s -> (s, a) -> s
stL s
sL (s
s', a
a)
              (s
s'', b
b) = s -> (s, b)
exL s
sL'
              sR :: s
sR = s -> Maybe s -> s
forall a. a -> Maybe a -> a
fromMaybe ((s, c) -> s
iR (s
s'', c
c)) Maybe s
msR
              sR' :: s
sR' = s -> (s, c) -> s
stR s
sR (s
s'', c
c)
              (s
s''', d
d) = s -> (s, d)
exR s
sR'
           in (s -> Maybe s
forall a. a -> Maybe a
Just s
sL', s -> Maybe s
forall a. a -> Maybe a
Just s
sR', s
s''', b -> d -> These b d
forall a b. a -> b -> These a b
These b
b d
d)
        Both Bias
RightFirst ->
          let sR :: s
sR = s -> Maybe s -> s
forall a. a -> Maybe a -> a
fromMaybe ((s, c) -> s
iR (s
s', c
c)) Maybe s
msR
              sR' :: s
sR' = s -> (s, c) -> s
stR s
sR (s
s', c
c)
              (s
s'', d
d) = s -> (s, d)
exR s
sR'
              sL :: s
sL = s -> Maybe s -> s
forall a. a -> Maybe a -> a
fromMaybe ((s, a) -> s
iL (s
s'', a
a)) Maybe s
msL
              sL' :: s
sL' = s -> (s, a) -> s
stL s
sL (s
s'', a
a)
              (s
s''', b
b) = s -> (s, b)
exL s
sL'
           in (s -> Maybe s
forall a. a -> Maybe a
Just s
sL', s -> Maybe s
forall a. a -> Maybe a
Just s
sR', s
s''', b -> d -> These b d
forall a b. a -> b -> These a b
These b
b d
d)
  {-# INLINE sharedBy #-}

-- Channel / Strength / Traced for Either
--
-- These instances make Process a traced monoidal category under the Either
-- tensor. The trace is per-tick Conway/Elgot settle: Right injects a value,
-- Left feeds intermediate state back within the same tick until Right exits.
-- This is the instance required by 'Net Either Process' knot bodies.

instance Channel Either Process where
  assoc :: forall a b c.
Process (Either (Either a b) c) (Either a (Either b c))
assoc = (Either (Either a b) c -> Either (Either a b) c)
-> (Either (Either a b) c
    -> Either (Either a b) c -> Either (Either a b) c)
-> (Either (Either a b) c -> Either a (Either b c))
-> Process (Either (Either a b) c) (Either a (Either b c))
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process Either (Either a b) c -> Either (Either a b) c
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id (\Either (Either a b) c
_ Either (Either a b) c
x -> Either (Either a b) c
x) Either (Either a b) c -> Either a (Either b c)
forall {a} {a} {b}. Either (Either a a) b -> Either a (Either a b)
assocEither
    where
      assocEither :: Either (Either a a) b -> Either a (Either a b)
assocEither (Left (Left a
a)) = a -> Either a (Either a b)
forall a b. a -> Either a b
Left a
a
      assocEither (Left (Right a
b)) = Either a b -> Either a (Either a b)
forall a b. b -> Either a b
Right (a -> Either a b
forall a b. a -> Either a b
Left a
b)
      assocEither (Right b
c) = Either a b -> Either a (Either a b)
forall a b. b -> Either a b
Right (b -> Either a b
forall a b. b -> Either a b
Right b
c)
  assoc' :: forall a b c.
Process (Either a (Either b c)) (Either (Either a b) c)
assoc' = (Either a (Either b c) -> Either a (Either b c))
-> (Either a (Either b c)
    -> Either a (Either b c) -> Either a (Either b c))
-> (Either a (Either b c) -> Either (Either a b) c)
-> Process (Either a (Either b c)) (Either (Either a b) c)
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process Either a (Either b c) -> Either a (Either b c)
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id (\Either a (Either b c)
_ Either a (Either b c)
x -> Either a (Either b c)
x) Either a (Either b c) -> Either (Either a b) c
forall {a} {b} {b}. Either a (Either b b) -> Either (Either a b) b
assocEither'
    where
      assocEither' :: Either a (Either b b) -> Either (Either a b) b
assocEither' (Left a
a) = Either a b -> Either (Either a b) b
forall a b. a -> Either a b
Left (a -> Either a b
forall a b. a -> Either a b
Left a
a)
      assocEither' (Right (Left b
b)) = Either a b -> Either (Either a b) b
forall a b. a -> Either a b
Left (b -> Either a b
forall a b. b -> Either a b
Right b
b)
      assocEither' (Right (Right b
c)) = b -> Either (Either a b) b
forall a b. b -> Either a b
Right b
c
  slide :: forall a b c.
Process (Either a (Either b c)) (Either b (Either a c))
slide = (Either a (Either b c) -> Either a (Either b c))
-> (Either a (Either b c)
    -> Either a (Either b c) -> Either a (Either b c))
-> (Either a (Either b c) -> Either b (Either a c))
-> Process (Either a (Either b c)) (Either b (Either a c))
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process Either a (Either b c) -> Either a (Either b c)
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id (\Either a (Either b c)
_ Either a (Either b c)
x -> Either a (Either b c)
x) Either a (Either b c) -> Either b (Either a c)
forall {a} {a} {b}. Either a (Either a b) -> Either a (Either a b)
slideEither
    where
      slideEither :: Either a (Either a b) -> Either a (Either a b)
slideEither (Left a
a) = Either a b -> Either a (Either a b)
forall a b. b -> Either a b
Right (a -> Either a b
forall a b. a -> Either a b
Left a
a)
      slideEither (Right (Left a
b)) = a -> Either a (Either a b)
forall a b. a -> Either a b
Left a
b
      slideEither (Right (Right b
c)) = Either a b -> Either a (Either a b)
forall a b. b -> Either a b
Right (b -> Either a b
forall a b. b -> Either a b
Right b
c)

instance Strength Either Process where
  strength :: forall b c a. Process b c -> Process (Either a b) (Either a c)
strength (Process b -> s
i s -> b -> s
st s -> c
ex) =
    (Either a b -> (Maybe s, Either a c))
-> ((Maybe s, Either a c) -> Either a b -> (Maybe s, Either a c))
-> ((Maybe s, Either a c) -> Either a c)
-> Process (Either a b) (Either a c)
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process
      (\case Left a
a -> (Maybe s
forall a. Maybe a
Nothing, a -> Either a c
forall a b. a -> Either a b
Left a
a); Right b
b -> let s0 :: s
s0 = b -> s
i b
b in (s -> Maybe s
forall a. a -> Maybe a
Just s
s0, c -> Either a c
forall a b. b -> Either a b
Right (s -> c
ex s
s0)))
      ( \(Maybe s
ms, Either a c
_) -> \case
          Left a
a -> (Maybe s
ms, a -> Either a c
forall a b. a -> Either a b
Left a
a)
          Right b
b -> case Maybe s
ms of
            Maybe s
Nothing -> let s0 :: s
s0 = b -> s
i b
b in (s -> Maybe s
forall a. a -> Maybe a
Just s
s0, c -> Either a c
forall a b. b -> Either a b
Right (s -> c
ex s
s0))
            Just s
s -> let s' :: s
s' = s -> b -> s
st s
s b
b in (s -> Maybe s
forall a. a -> Maybe a
Just s
s', c -> Either a c
forall a b. b -> Either a b
Right (s -> c
ex s
s'))
      )
      (Maybe s, Either a c) -> Either a c
forall a b. (a, b) -> b
snd

instance Traced Either Process where
  trace :: forall a b c. Process (Either a b) (Either a c) -> Process b c
trace (Process Either a b -> s
i s -> Either a b -> s
st s -> Either a c
ex) = (b -> s) -> (s -> b -> s) -> (s -> c) -> Process b c
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process b -> s
i' s -> b -> s
st' s -> c
ex'
    where
      settle :: s -> s
settle s
m = case s -> Either a c
ex s
m of
        Left a
s -> s -> s
settle (s -> Either a b -> s
st s
m (a -> Either a b
forall a b. a -> Either a b
Left a
s))
        Right c
_ -> s
m

      i' :: b -> s
i' b
a = s -> s
settle (Either a b -> s
i (b -> Either a b
forall a b. b -> Either a b
Right b
a))
      st' :: s -> b -> s
st' s
m b
a = s -> s
settle (s -> Either a b -> s
st s
m (b -> Either a b
forall a b. b -> Either a b
Right b
a))
      ex' :: s -> c
ex' s
m = case s -> Either a c
ex s
m of
        Right c
b -> c
b
        Left a
_ -> String -> c
forall a. HasCallStack => String -> a
error String
"Circuit.Process.Traced Either: unsettled state"

-- * Bimonoid instances (pointwise lift)

instance (Copy (->) a) => Copy Process a where
  copy :: Process a (a, a)
copy = (a -> a) -> (a -> a -> a) -> (a -> (a, a)) -> Process a (a, a)
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process a -> a
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id (\a
_ a
x -> a
x) a -> (a, a)
forall (arr :: * -> * -> *) a. Copy arr a => arr a (a, a)
Bm.copy

instance Discard Process a where
  discard :: Process a ()
discard = (a -> a) -> (a -> a -> a) -> (a -> ()) -> Process a ()
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process a -> a
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id (\a
_ a
x -> a
x) (() -> a -> ()
forall a b. a -> b -> a
const ())

instance (Merge (->) a) => Merge Process a where
  plus :: Process (a, a) a
plus = ((a, a) -> (a, a))
-> ((a, a) -> (a, a) -> (a, a))
-> ((a, a) -> a)
-> Process (a, a) a
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process (a, a) -> (a, a)
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id (\(a, a)
_ (a, a)
x -> (a, a)
x) (a, a) -> a
forall (arr :: * -> * -> *) a. Merge arr a => arr (a, a) a
Bm.plus

instance (Zero (->) a) => Zero Process a where
  zero :: Process () a
zero = (() -> ()) -> (() -> () -> ()) -> (() -> a) -> Process () a
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process () -> ()
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id (\()
_ ()
x -> ()
x) () -> a
forall {k} (arr :: * -> k -> *) (a :: k). Zero arr a => arr () a
Bm.zero

-- * Runners

-- | Run a process over any stream with an 'Uncons' coalgebra and build the
-- output with a 'Cons' algebra.
--
-- The first element seeds the hidden channel via @inject@; each subsequent
-- element steps it via @step@; each output is @extract@ of the current channel.
scanStream :: forall f a g b. (Uncons f a, Cons g b) => Process a b -> f -> g
scanStream :: forall f a g b. (Uncons f a, Cons g b) => Process a b -> f -> g
scanStream (Process a -> s
inject s -> a -> s
step s -> b
extract) = f -> g
goInit
  where
    nilG :: g
    nilG :: g
nilG = forall f s. Cons f s => f
consNil @g @b

    consG :: b -> g -> g
    consG :: b -> g -> g
consG = b -> g -> g
forall f s. Cons f s => s -> f -> f
cons

    goInit :: f -> g
goInit f
f = case f -> These a f
forall f s. Uncons f s => f -> These s f
uncons f
f of
      That f
_ -> g
nilG
      This a
a -> let s0 :: s
s0 = a -> s
inject a
a in b -> g -> g
consG (s -> b
extract s
s0) g
nilG
      These a
a f
rest -> let s0 :: s
s0 = a -> s
inject a
a in b -> g -> g
consG (s -> b
extract s
s0) (s -> f -> g
go s
s0 f
rest)

    go :: s -> f -> g
go s
s f
f = case f -> These a f
forall f s. Uncons f s => f -> These s f
uncons f
f of
      That f
_ -> g
nilG
      This a
a -> let s' :: s
s' = s -> a -> s
step s
s a
a in b -> g -> g
consG (s -> b
extract s
s') g
nilG
      These a
a f
rest -> let s' :: s
s' = s -> a -> s
step s
s a
a in b -> g -> g
consG (s -> b
extract s
s') (s -> f -> g
go s
s' f
rest)

-- | List specialization of 'scanStream'.
scan :: Process a b -> [a] -> [b]
scan :: forall a b. Process a b -> [a] -> [b]
scan = Process a b -> [a] -> [b]
forall f a g b. (Uncons f a, Cons g b) => Process a b -> f -> g
scanStream
{-# INLINE scan #-}

-- | Run a process over a stream, returning the final output (if any).
foldStream :: (Uncons f a) => Process a b -> f -> Maybe b
foldStream :: forall f a b. Uncons f a => Process a b -> f -> Maybe b
foldStream (Process a -> s
inject s -> a -> s
step s -> b
extract) = f -> Maybe b
goInit
  where
    goInit :: f -> Maybe b
goInit f
f = case f -> These a f
forall f s. Uncons f s => f -> These s f
uncons f
f of
      That f
_ -> Maybe b
forall a. Maybe a
Nothing
      This a
a -> b -> Maybe b
forall a. a -> Maybe a
Just (s -> b
extract (a -> s
inject a
a))
      These a
a f
rest -> b -> Maybe b
forall a. a -> Maybe a
Just (s -> f -> b
go (a -> s
inject a
a) f
rest)

    go :: s -> f -> b
go s
s f
f = case f -> These a f
forall f s. Uncons f s => f -> These s f
uncons f
f of
      That f
_ -> s -> b
extract s
s
      This a
a -> s -> b
extract (s -> a -> s
step s
s a
a)
      These a
a f
rest -> s -> f -> b
go (s -> a -> s
step s
s a
a) f
rest

-- | List specialization of 'foldStream'.
fold :: Process a b -> [a] -> Maybe b
fold :: forall a b. Process a b -> [a] -> Maybe b
fold = Process a b -> [a] -> Maybe b
forall f a b. Uncons f a => Process a b -> f -> Maybe b
foldStream
{-# INLINE fold #-}

-- | Encode a process as a stream-level 'Trace' over arbitrary 'Uncons'/'Cons'
-- streams.
--
-- This is the definitional runner: 'scanStream' is 'Circuit.Syntax.eval'
-- composed with 'encodeStream'. The feedback channel carries
-- @(Maybe channel, remaining input, accumulated output)@.
encodeStream :: (Uncons f a, Cons g b) => Process a b -> Trace Either (->) f g
encodeStream :: forall f a g b.
(Uncons f a, Cons g b) =>
Process a b -> Trace Either (->) f g
encodeStream Process a b
p = case Process a b -> SomeBody Either (->) f g
forall f a g b.
(Uncons f a, Cons g b) =>
Process a b -> SomeBody Either (->) f g
processToBodyStream Process a b
p of
  SomeBody ch
_ (Body Either ch f -> Either ch g
b) -> Trace Either (->) (Either ch f) (Either ch g)
-> Trace Either (->) f g
forall (t :: * -> * -> *) (arr :: * -> * -> *) s a b.
Trace t arr (t s a) (t s b) -> Trace t arr a b
yank ((Either ch f -> Either ch g)
-> Trace Either (->) (Either ch f) (Either ch g)
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base Either ch f -> Either ch g
b)

-- | List specialization of 'encodeStream'.
encode :: Process a b -> Trace Either (->) [a] [b]
encode :: forall a b. Process a b -> Trace Either (->) [a] [b]
encode = Process a b -> Trace Either (->) [a] [b]
forall f a g b.
(Uncons f a, Cons g b) =>
Process a b -> Trace Either (->) f g
encodeStream
{-# INLINE encode #-}

-- * Mealy-style processes

-- | Build a 'Process' from a Mealy-style step.
--
-- The output may depend on the current input. The channel internally stores the
-- most recent output so that the Moore-style 'Process' interface is preserved.
mealy :: ch -> (ch -> a -> (ch, Maybe b)) -> Process a (Maybe b)
mealy :: forall ch a b.
ch -> (ch -> a -> (ch, Maybe b)) -> Process a (Maybe b)
mealy ch
ch0 ch -> a -> (ch, Maybe b)
step = (a -> (ch, Maybe b))
-> ((ch, Maybe b) -> a -> (ch, Maybe b))
-> ((ch, Maybe b) -> Maybe b)
-> Process a (Maybe b)
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process a -> (ch, Maybe b)
inject (ch, Maybe b) -> a -> (ch, Maybe b)
step' (ch, Maybe b) -> Maybe b
forall a b. (a, b) -> b
extract
  where
    inject :: a -> (ch, Maybe b)
inject a
a =
      let (ch
ch, Maybe b
mb) = ch -> a -> (ch, Maybe b)
step ch
ch0 a
a
       in (ch
ch, Maybe b
mb)
    step' :: (ch, Maybe b) -> a -> (ch, Maybe b)
step' (ch
ch, Maybe b
_) a
a =
      let (ch
ch', Maybe b
mb') = ch -> a -> (ch, Maybe b)
step ch
ch a
a
       in (ch
ch', Maybe b
mb')
    extract :: (a, b) -> b
extract = (a, b) -> b
forall a b. (a, b) -> b
snd
{-# INLINEABLE mealy #-}

-- | Collect the emitted outputs of a 'Process (Maybe b)' over any stream.
runMealyStream :: forall f a g b. (Uncons f a, Cons g b) => Process a (Maybe b) -> f -> g
runMealyStream :: forall f a g b.
(Uncons f a, Cons g b) =>
Process a (Maybe b) -> f -> g
runMealyStream (Process a -> s
inject s -> a -> s
step s -> Maybe b
extract) = f -> g
goInit
  where
    nilG :: g
    nilG :: g
nilG = forall f s. Cons f s => f
consNil @g @b

    consG :: b -> g -> g
    consG :: b -> g -> g
consG = b -> g -> g
forall f s. Cons f s => s -> f -> f
cons

    emit :: s -> g -> g
emit s
ch g
rest = case s -> Maybe b
extract s
ch of
      Maybe b
Nothing -> g
rest
      Just b
b -> b -> g -> g
consG b
b g
rest

    goInit :: f -> g
goInit f
f = case f -> These a f
forall f s. Uncons f s => f -> These s f
uncons f
f of
      That f
_ -> g
nilG
      This a
a -> let ch0 :: s
ch0 = a -> s
inject a
a in s -> g -> g
emit s
ch0 g
nilG
      These a
a f
rest -> let ch0 :: s
ch0 = a -> s
inject a
a in s -> g -> g
emit s
ch0 (s -> f -> g
go s
ch0 f
rest)

    go :: s -> f -> g
go s
ch f
f = case f -> These a f
forall f s. Uncons f s => f -> These s f
uncons f
f of
      That f
_ -> g
nilG
      This a
a -> let ch' :: s
ch' = s -> a -> s
step s
ch a
a in s -> g -> g
emit s
ch' g
nilG
      These a
a f
rest -> let ch' :: s
ch' = s -> a -> s
step s
ch a
a in s -> g -> g
emit s
ch' (s -> f -> g
go s
ch' f
rest)

-- | List specialization of 'runMealyStream'.
runMealy :: Process a (Maybe b) -> [a] -> [b]
runMealy :: forall a b. Process a (Maybe b) -> [a] -> [b]
runMealy = Process a (Maybe b) -> [a] -> [b]
forall f a g b.
(Uncons f a, Cons g b) =>
Process a (Maybe b) -> f -> g
runMealyStream
{-# INLINEABLE runMealy #-}

-- * Cross-tick feedback

-- | One-tick delay with an initial value.
--
-- Output is @s0@ on the first tick and the input from the previous tick
-- thereafter. This is the primitive that makes 'register' productive: the
-- feedback wire is observable one tick late.
delay :: s -> Process s s
delay :: forall s. s -> Process s s
delay s
s0 = (s -> s) -> (s -> s -> s) -> (s -> s) -> Process s s
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process (s -> s -> s
forall a b. a -> b -> a
const s
s0) ((s -> s) -> s -> s -> s
forall a b. a -> b -> a
const s -> s
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id) s -> s
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id

-- | Cross-tick register feedback.
--
-- Given an initial feedback value @s0@ and a process @Process (a, s) (b, s)@,
-- close the @s@ wire so that the @s@ produced at one tick is fed back as
-- input at the next tick. This is the productive, strict-accumulator-safe
-- analogue of the cartesian trace: the delay is explicit in the wiring
-- rather than implicit in a lazy knot.
--
-- Compare with the cartesian 'trace' on 'Process', which ties a lazy knot
-- and diverges for strict state; 'register' keeps strict state cells sound
-- by making the one-tick delay observable.
--
-- For bodies whose fixed-point is independent of the initial feedback value
-- (e.g. affine/stateless feedback such as @ewmaBody@), the same wiring can
-- be expressed by swapping the feedback wire into the active position,
-- applying 'strength' ('delay' s0), and tracing.
register :: s -> Process (a, s) (b, s) -> Process a b
register :: forall s a b. s -> Process (a, s) (b, s) -> Process a b
register s
s0 (Process (a, s) -> s
i s -> (a, s) -> s
st s -> (b, s)
ex) = (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process a -> s
i' s -> a -> s
st' s -> b
ex'
  where
    i' :: a -> s
i' a
a = (a, s) -> s
i (a
a, s
s0)
    st' :: s -> a -> s
st' s
s a
a = s -> (a, s) -> s
st s
s (a
a, (b, s) -> s
forall a b. (a, b) -> b
snd (s -> (b, s)
ex s
s))
    ex' :: s -> b
ex' s
s = (b, s) -> b
forall a b. (a, b) -> a
fst (s -> (b, s)
ex s
s)

-- * Body conversions

-- | View a 'Process' as a knot body over the 'Either' tensor, for any
-- 'Uncons' input and 'Cons' output stream.
--
-- This is the same body used by 'encodeStream', now exposed as a value of
-- @Body Either ch (->)@. It confirms the Process / Trace Either round-trip
-- factors through the knot-body category.
processToBodyStream :: forall f a g b. (Uncons f a, Cons g b) => Process a b -> SomeBody Either (->) f g
processToBodyStream :: forall f a g b.
(Uncons f a, Cons g b) =>
Process a b -> SomeBody Either (->) f g
processToBodyStream (Process a -> s
inject s -> a -> s
step s -> b
extract) =
  (Maybe s, f, [b])
-> Body Either (Maybe s, f, [b]) (->) f g
-> SomeBody Either (->) f g
forall {k} {k1} ch (t :: * -> k -> k1) (arr :: k1 -> k1 -> *)
       (a :: k) (b :: k).
ch -> Body t ch arr a b -> SomeBody t arr a b
SomeBody (Maybe s
forall a. Maybe a
Nothing, f
nilF, []) (Body Either (Maybe s, f, [b]) (->) f g
 -> SomeBody Either (->) f g)
-> Body Either (Maybe s, f, [b]) (->) f g
-> SomeBody Either (->) f g
forall a b. (a -> b) -> a -> b
$ (Either (Maybe s, f, [b]) f -> Either (Maybe s, f, [b]) g)
-> Body Either (Maybe s, f, [b]) (->) f g
forall {k} {k1} {k2} (t :: k -> k1 -> k2) (ch :: k)
       (arr :: k2 -> k2 -> *) (a :: k1) (b :: k1).
arr (t ch a) (t ch b) -> Body t ch arr a b
Body ((Either (Maybe s, f, [b]) f -> Either (Maybe s, f, [b]) g)
 -> Body Either (Maybe s, f, [b]) (->) f g)
-> (Either (Maybe s, f, [b]) f -> Either (Maybe s, f, [b]) g)
-> Body Either (Maybe s, f, [b]) (->) f g
forall a b. (a -> b) -> a -> b
$ \case
    Right f
f -> case f -> These a f
forall f s. Uncons f s => f -> These s f
uncons f
f of
      That f
_ -> g -> Either (Maybe s, f, [b]) g
forall a b. b -> Either a b
Right g
nilG
      This a
a ->
        let ch0 :: s
ch0 = a -> s
inject a
a
         in (Maybe s, f, [b]) -> Either (Maybe s, f, [b]) g
forall a b. a -> Either a b
Left (s -> Maybe s
forall a. a -> Maybe a
Just s
ch0, f
nilF, [s -> b
extract s
ch0])
      These a
a f
rest ->
        let ch0 :: s
ch0 = a -> s
inject a
a
         in (Maybe s, f, [b]) -> Either (Maybe s, f, [b]) g
forall a b. a -> Either a b
Left (s -> Maybe s
forall a. a -> Maybe a
Just s
ch0, f
rest, [s -> b
extract s
ch0])
    Left (Maybe s
Nothing, f
_, [b]
_) -> String -> Either (Maybe s, f, [b]) g
forall a. HasCallStack => String -> a
error String
"processToBodyStream: feedback reached before first input"
    Left (Just s
ch, f
f, [b]
bs) -> case f -> These a f
forall f s. Uncons f s => f -> These s f
uncons f
f of
      That f
_ -> g -> Either (Maybe s, f, [b]) g
forall a b. b -> Either a b
Right ((g -> b -> g) -> g -> [b] -> g
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((b -> g -> g) -> g -> b -> g
forall a b c. (a -> b -> c) -> b -> a -> c
flip b -> g -> g
consG) g
nilG [b]
bs)
      This a
a ->
        let ch' :: s
ch' = s -> a -> s
step s
ch a
a
         in (Maybe s, f, [b]) -> Either (Maybe s, f, [b]) g
forall a b. a -> Either a b
Left (s -> Maybe s
forall a. a -> Maybe a
Just s
ch', f
nilF, s -> b
extract s
ch' b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [b]
bs)
      These a
a f
rest ->
        let ch' :: s
ch' = s -> a -> s
step s
ch a
a
         in (Maybe s, f, [b]) -> Either (Maybe s, f, [b]) g
forall a b. a -> Either a b
Left (s -> Maybe s
forall a. a -> Maybe a
Just s
ch', f
rest, s -> b
extract s
ch' b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [b]
bs)
  where
    nilF :: f
    nilF :: f
nilF = forall f s. Uncons f s => f
nil @f @a

    nilG :: g
    nilG :: g
nilG = forall f s. Cons f s => f
consNil @g @b

    consG :: b -> g -> g
    consG :: b -> g -> g
consG = b -> g -> g
forall f s. Cons f s => s -> f -> f
cons

-- | List specialization of 'processToBodyStream'.
processToBody :: Process a b -> SomeBody Either (->) [a] [b]
processToBody :: forall a b. Process a b -> SomeBody Either (->) [a] [b]
processToBody = Process a b -> SomeBody Either (->) [a] [b]
forall f a g b.
(Uncons f a, Cons g b) =>
Process a b -> SomeBody Either (->) f g
processToBodyStream

-- | View a 'Process' as an existentially-quantified 'Body'.
--
-- The process state is exposed as the ambient wire.  The initial state is
-- 'Nothing'; the first input is fed to @inject@ to create the real state, and
-- subsequent inputs use @step@.  The output is always @extract@ of the current
-- state.
processToSomeBody :: Process a b -> SomeBody (,) (->) a b
processToSomeBody :: forall a b. Process a b -> SomeBody (,) (->) a b
processToSomeBody (Process a -> s
inject s -> a -> s
step s -> b
extract) =
  Maybe s -> Body (,) (Maybe s) (->) a b -> SomeBody (,) (->) a b
forall {k} {k1} ch (t :: * -> k -> k1) (arr :: k1 -> k1 -> *)
       (a :: k) (b :: k).
ch -> Body t ch arr a b -> SomeBody t arr a b
SomeBody Maybe s
forall a. Maybe a
Nothing (Body (,) (Maybe s) (->) a b -> SomeBody (,) (->) a b)
-> Body (,) (Maybe s) (->) a b -> SomeBody (,) (->) a b
forall a b. (a -> b) -> a -> b
$ ((Maybe s, a) -> (Maybe s, b)) -> Body (,) (Maybe s) (->) a b
forall {k} {k1} {k2} (t :: k -> k1 -> k2) (ch :: k)
       (arr :: k2 -> k2 -> *) (a :: k1) (b :: k1).
arr (t ch a) (t ch b) -> Body t ch arr a b
Body (((Maybe s, a) -> (Maybe s, b)) -> Body (,) (Maybe s) (->) a b)
-> ((Maybe s, a) -> (Maybe s, b)) -> Body (,) (Maybe s) (->) a b
forall a b. (a -> b) -> a -> b
$ \case
    (Maybe s
Nothing, a
a) ->
      let s :: s
s = a -> s
inject a
a
       in (s -> Maybe s
forall a. a -> Maybe a
Just s
s, s -> b
extract s
s)
    (Just s
s, a
a) ->
      let s' :: s
s' = s -> a -> s
step s
s a
a
       in (s -> Maybe s
forall a. a -> Maybe a
Just s
s', s -> b
extract s
s')