{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

-- | Moore agents on a shared, addressed log; opaque shards for effects.
--
-- Pure agent shape:
--
-- @
-- type Agent arr s a b = System arr s (Mono a b)
-- @
--
-- Free carrier @s@ is required by the pretense (tape vs summary).  The common
-- log case is @Agent (->) [Post] Post [Post]@ — state is the received stream.
-- That carrier is a parse of the tape: each committed @Post@ is one token.
--
-- Effectful boundary (preferred pin):
--
-- @
-- type Shard m a b = Ends (K m) a b
-- @
--
-- Symmetric in the common log case: commit a list of posts, emit a list of
-- posts.  One-post reality (hit enter) is not another type — lift with @(:[])@
-- on the commit side (@prefixIn@).  'LogEnds' is the same shape (dual seat on
-- the log).  Opacity is commit\/emit only; no interior.
--
-- Change of base (circuits-parser sense): 'agentShard' reinterprets a pure
-- 'Agent' at @K m@ ends — same Moore citizen, effectful interface.
-- Direct shards (hermes session, muster-agent) skip the pure coalgebra and
-- inhabit 'Shard' only.
--
-- Token seat around a list shard (parser dual): stream @f = [Post]@, token
-- @s = Post@.  'batchEnds' snocs tokens into a stream (build @f@); 'unbatchEnds'
-- peels with the same coalgebra as 'Uncons' on lists.  Compose with the
-- shard via @('>:>')@:
--
-- @
-- portShard = batchEnds … >:> shard >:> unbatchEnds …
--   :: Shard m Post [Post] >:> Shard m [Post] [Post] >:> Shard m [Post] Post
--   :: Port m
-- @
--
-- Queue ends ('openSTM' \/'openIO') are the effectful token wire of the same
-- shape when you need a bare @Post\/@Post@ channel without a shard.
--
-- Design card: @coffee\/loom\/agent.md@.
module Circuit.Agent
  ( -- * Posts and the log
    Post (..),
    PostId,
    mkPost,
    replyTo,
    synthesis,
    sortNub,
    indexToIdMap,
    branches,
    branchesByIndex,
    cone,
    coneByIndex,
    Log,
    emptyLog,
    Name,

    -- * Pure agents
    Agent,
    AgentState (..),
    emptyAgentState,
    tape,
    selfrec,

    -- * Inbox
    Inbox,
    emptyInbox,
    appendInbox,
    unconsInbox,
    inboxWho,
    inboxSubs,

    -- * Delivery
    deliversTo,

    -- * Effectful ends (symmetric streams)
    Shard,
    LogEnds,
    shard,
    logEnds,

    -- * Agent as Shard (change of base into K)
    AgentSeat (..),
    feedAgent,
    flushOutbox,
    agentShard,
    runAgentShard,

    -- * Token seat (stream buffers around a Shard)
    Port,
    Snoc (..),
    snocPost,
    batchEnds,
    unbatchEnds,
    portShard,

    -- * Forces
    watch,
    post,
    turn,
    turnAs,
    hasPending,
    loop,
    loopSubs,
    loopWith,
    loopWithSubs,
    loops,
    loopsSubs,
    loopHetero,
    loopHeteroSubs,
    meetingLoop,
    meetingLoopSubs,
    seedAgentState,
    RosterEntry,

    -- * Derivations
    Derivation (..),

    -- * Session assembly
    session,

    -- * Running one step
    run1,

    -- * Effectful agents
    agentM,
    runAgentM,

    -- * STM agents (S) and IO-bound agents (X)
    AgentS,
    AgentX,
    agentX,
    awaitS,
    raceS,
    raceIO,
    stepS,
    stepsS,
    runAgentS,
    readEndSTM,
    writeEndSTM,
    agentLoopS,
    selfLoopS,
    agentLoopL,
    selfLoopL,

    -- * Container dial (Bag / Seq log algebra)
    Bag (..),
    TurnLog,
    emptyBag,
    singletonBag,
    insertBag,
    toBag,
    fromBag,

    -- * Behaviour (stream semantics)
    Beh,
    beh,
    after,

    -- * Choice (level-1 grammar fragment)
    branchAgent,

    -- * Seat-level tensors (product / await, coproduct / race)
    awaitA,
    raceA,

    -- * Re-exports for end construction
    Poles (..),
    close,
    polesK,
    prefixIn,
    Queue (..),
    ChannelPolicy (..),
    openChannel,
    openChannelSTM,
    openLinearChannel,
    openLinearChannelSTM,
    HaltChannel (..),
    IsLinear,
    openHaltChannel,
    writeHaltChannel,
    readHaltChannel,
    openSTM,
    openIO,
    pipeEnds,

    -- * Shard combinators
    prefixShard,
    suffixShard,
    codecShard,
    composeShard,
    (>:>),
  )
where

import Circuit hiding (eval)
import Circuit.Agent.Ends (ChannelPolicy (..), HaltChannel (..), IsLinear, Queue (..), openChannel, openChannelSTM, openHaltChannel, openIO, openLinearChannel, openLinearChannelSTM, openSTM, pipeEnds, readHaltChannel, writeHaltChannel)
import Circuit.Category (K (..))
import Circuit.Poles (compose, imap, iomap, omap)
import Circuit.Poly (Eval (..), Mono)
import Circuit.Process (after)
import Circuit.Syntax (eval)
import Circuit.System (System, fromEvalSystem, monoDir, monoIn, runSystem, runSystemMono, system)
import Circuit.System qualified as System
import Circuit.Trace (Trace, base, yank)
import Control.Concurrent (threadDelay)
import Control.Concurrent.Async (async, cancel, race, wait)
import Control.Concurrent.STM (STM, atomically, orElse)
import Data.Foldable (traverse_)
import Data.List (find, foldl', genericIndex, genericTake, nub, sort)
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Maybe (fromMaybe, listToMaybe)
import Data.Sequence (Seq)
import Data.Sequence qualified as Seq
import Data.Text (Text, empty)
import Numeric.Natural (Natural)
import "circuits" Circuit.Stream (Cons (..), Snoc (..), These (..), Uncons (..))

-- $setup
-- >>> :set -XOverloadedStrings
-- >>> import Circuit.Agent
-- >>> import Circuit.Process (iterateSystem)

-- | Agent name on the shared log.
type Name = Text

-- | Absolute post identity.  In the stamped log this is the line id assigned
-- by the single writer.  In pure meeting logs it is the position in the
-- oldest-first log, but 'branches' and 'cone' resolve by the id itself, not by
-- position in the passed-in list.  Use 'indexToIdMap' to assign ids [0..] from
-- a chronological list.
type PostId = Natural

-- | A single entry on the shared log, polymorphic in payload.
--
-- Routing is by name list: a post delivers to every agent whose name appears
-- in 'to' (the audience).  'thread' is the ancestry edges: @[]@ for a root
-- post, otherwise the 'PostId's of the posts being replied to or synthesised
-- from.  Parents are a set (duplicates discarded) in normalised (sorted)
-- order — the smart constructors keep it so.
data Post a = Post
  { forall a. Post a -> Name
from :: Name,
    forall a. Post a -> [Name]
to :: [Name],
    forall a. Post a -> [PostId]
thread :: [PostId],
    forall a. Post a -> a
body :: a
  }
  deriving (Int -> Post a -> ShowS
[Post a] -> ShowS
Post a -> String
(Int -> Post a -> ShowS)
-> (Post a -> String) -> ([Post a] -> ShowS) -> Show (Post a)
forall a. Show a => Int -> Post a -> ShowS
forall a. Show a => [Post a] -> ShowS
forall a. Show a => Post a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Post a -> ShowS
showsPrec :: Int -> Post a -> ShowS
$cshow :: forall a. Show a => Post a -> String
show :: Post a -> String
$cshowList :: forall a. Show a => [Post a] -> ShowS
showList :: [Post a] -> ShowS
Show, Post a -> Post a -> Bool
(Post a -> Post a -> Bool)
-> (Post a -> Post a -> Bool) -> Eq (Post a)
forall a. Eq a => Post a -> Post a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Post a -> Post a -> Bool
== :: Post a -> Post a -> Bool
$c/= :: forall a. Eq a => Post a -> Post a -> Bool
/= :: Post a -> Post a -> Bool
Eq, Eq (Post a)
Eq (Post a) =>
(Post a -> Post a -> Ordering)
-> (Post a -> Post a -> Bool)
-> (Post a -> Post a -> Bool)
-> (Post a -> Post a -> Bool)
-> (Post a -> Post a -> Bool)
-> (Post a -> Post a -> Post a)
-> (Post a -> Post a -> Post a)
-> Ord (Post a)
Post a -> Post a -> Bool
Post a -> Post a -> Ordering
Post a -> Post a -> Post a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (Post a)
forall a. Ord a => Post a -> Post a -> Bool
forall a. Ord a => Post a -> Post a -> Ordering
forall a. Ord a => Post a -> Post a -> Post a
$ccompare :: forall a. Ord a => Post a -> Post a -> Ordering
compare :: Post a -> Post a -> Ordering
$c< :: forall a. Ord a => Post a -> Post a -> Bool
< :: Post a -> Post a -> Bool
$c<= :: forall a. Ord a => Post a -> Post a -> Bool
<= :: Post a -> Post a -> Bool
$c> :: forall a. Ord a => Post a -> Post a -> Bool
> :: Post a -> Post a -> Bool
$c>= :: forall a. Ord a => Post a -> Post a -> Bool
>= :: Post a -> Post a -> Bool
$cmax :: forall a. Ord a => Post a -> Post a -> Post a
max :: Post a -> Post a -> Post a
$cmin :: forall a. Ord a => Post a -> Post a -> Post a
min :: Post a -> Post a -> Post a
Ord, (forall a b. (a -> b) -> Post a -> Post b)
-> (forall a b. a -> Post b -> Post a) -> Functor Post
forall a b. a -> Post b -> Post a
forall a b. (a -> b) -> Post a -> Post b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Post a -> Post b
fmap :: forall a b. (a -> b) -> Post a -> Post b
$c<$ :: forall a b. a -> Post b -> Post a
<$ :: forall a b. a -> Post b -> Post a
Functor)

-- | A fresh root post (no parents).
mkPost :: Name -> [Name] -> a -> Post a
mkPost :: forall a. Name -> [Name] -> a -> Post a
mkPost Name
f [Name]
t = Name -> [Name] -> [PostId] -> a -> Post a
forall a. Name -> [Name] -> [PostId] -> a -> Post a
Post Name
f [Name]
t []

-- | A reply: the audience is the parent's sender plus the rest of the
-- parent's audience (minus self); the sole thread edge cites the parent's
-- 'PostId'.
replyTo :: Name -> PostId -> Post a -> b -> Post b
replyTo :: forall a b. Name -> PostId -> Post a -> b -> Post b
replyTo Name
who PostId
parentId Post a
p b
b =
  Post
    { from :: Name
from = Name
who,
      to :: [Name]
to = Post a -> Name
forall a. Post a -> Name
from Post a
p Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
who) (Post a -> [Name]
forall a. Post a -> [Name]
to Post a
p),
      thread :: [PostId]
thread = [PostId
parentId],
      body :: b
body = b
b
    }

-- | A synthesis: one descendant of several parents — the object-level
-- wire-merge dual to merging agents.  The ancestry cites every parent id as
-- a normalised set (sorted, duplicates discarded).
synthesis :: Name -> [Name] -> [PostId] -> b -> Post b
synthesis :: forall a. Name -> [Name] -> [PostId] -> a -> Post a
synthesis Name
who [Name]
audience [PostId]
parentIds b
b =
  Post
    { from :: Name
from = Name
who,
      to :: [Name]
to = [Name]
audience,
      thread :: [PostId]
thread = [PostId] -> [PostId]
forall a. Ord a => [a] -> [a]
sortNub [PostId]
parentIds,
      body :: b
body = b
b
    }

-- | Sorted, duplicate-free.  The normalised-set primitive of the thread
-- design: parent sets, audiences, and cones are all kept in this form.
sortNub :: (Ord a) => [a] -> [a]
sortNub :: forall a. Ord a => [a] -> [a]
sortNub = [a] -> [a]
forall a. Eq a => [a] -> [a]
nub ([a] -> [a]) -> ([a] -> [a]) -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> [a]
forall a. Ord a => [a] -> [a]
sort

-- | Assign positional ids @[0..]@ to a chronological list of posts.  This is
-- the convenience bridge from list-shaped logs to the id-resolved
-- 'branches'/'cone' API.
indexToIdMap :: [Post a] -> Map PostId (Post a)
indexToIdMap :: forall a. [Post a] -> Map PostId (Post a)
indexToIdMap = [(PostId, Post a)] -> Map PostId (Post a)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(PostId, Post a)] -> Map PostId (Post a))
-> ([Post a] -> [(PostId, Post a)])
-> [Post a]
-> Map PostId (Post a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [PostId] -> [Post a] -> [(PostId, Post a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [PostId
0 ..]

-- | The next id after the largest key in the map, or @0@ if empty.
nextId :: Map PostId (Post a) -> PostId
nextId :: forall a. Map PostId (Post a) -> PostId
nextId Map PostId (Post a)
m = if Map PostId (Post a) -> Bool
forall k a. Map k a -> Bool
Map.null Map PostId (Post a)
m then PostId
0 else (PostId, Post a) -> PostId
forall a b. (a, b) -> a
fst (Map PostId (Post a) -> (PostId, Post a)
forall k a. Map k a -> (k, a)
Map.findMax Map PostId (Post a)
m) PostId -> PostId -> PostId
forall a. Num a => a -> a -> a
+ PostId
1

-- | The label-branches from a post to its conversation roots, resolved by
-- exact 'PostId'.  The current post is not in the map; its id is inferred as
-- the id after the largest key in the prior map.  Only thread edges strictly
-- less than the current id are resolved (ancestors must be prior posts).  A
-- dangling or future id is silently ignored.  A root post has one trivial
-- branch; every parent edge contributes its own path.  Branches of replies
-- are pure cons:
--
-- > branches (indexToIdMap prior) (replyTo who i p b)
--     == map (who :) (branches (Map.filterWithKey (\k _ -> k < i) (indexToIdMap prior)) p)
--
-- >>> let p1 = mkPost "tony" ["grok"] "hi" :: Post String; p2 = mkPost "grok" ["tony"] "hello"; r = replyTo "kimi" 1 p2 "a" in branchesByIndex [p1, p2] r == map ("kimi" :) (branchesByIndex [p1, p2] p2)
-- True
--
-- >>> let p1 = mkPost "tony" ["grok"] "hi" :: Post String; p2 = mkPost "grok" ["tony"] "hello"; r1 = replyTo "kimi" 1 p2 "a"; r2 = replyTo "tony" 2 r1 "b" in branchesByIndex [p1, p2, r1] r2
-- [["tony","kimi","grok"]]
branches :: Map PostId (Post a) -> Post a -> [[Name]]
branches :: forall a. Map PostId (Post a) -> Post a -> [[Name]]
branches Map PostId (Post a)
priorMap = PostId -> Post a -> [[Name]]
go (Map PostId (Post a) -> PostId
forall a. Map PostId (Post a) -> PostId
nextId Map PostId (Post a)
priorMap)
  where
    go :: PostId -> Post a -> [[Name]]
go PostId
selfId Post a
p =
      case Post a -> [PostId]
forall a. Post a -> [PostId]
thread Post a
p of
        [] -> [[Post a -> Name
forall a. Post a -> Name
from Post a
p]]
        [PostId]
is -> (PostId -> [[Name]]) -> [PostId] -> [[Name]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (PostId -> Post a -> PostId -> [[Name]]
step PostId
selfId Post a
p) [PostId]
is

    step :: PostId -> Post a -> PostId -> [[Name]]
step PostId
selfId Post a
p PostId
i =
      if PostId
i PostId -> PostId -> Bool
forall a. Ord a => a -> a -> Bool
>= PostId
selfId
        then []
        else case PostId -> Map PostId (Post a) -> Maybe (Post a)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup PostId
i Map PostId (Post a)
priorMap of
          Maybe (Post a)
Nothing -> []
          Just Post a
q -> ([Name] -> [Name]) -> [[Name]] -> [[Name]]
forall a b. (a -> b) -> [a] -> [b]
map (Post a -> Name
forall a. Post a -> Name
from Post a
p Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:) (PostId -> Post a -> [[Name]]
go PostId
i Post a
q)

-- | Convenience wrapper: resolve branches from a chronological list, assigning
-- ids @[0..]@.
branchesByIndex :: [Post a] -> Post a -> [[Name]]
branchesByIndex :: forall a. [Post a] -> Post a -> [[Name]]
branchesByIndex [Post a]
prior = Map PostId (Post a) -> Post a -> [[Name]]
forall a. Map PostId (Post a) -> Post a -> [[Name]]
branches ([Post a] -> Map PostId (Post a)
forall a. [Post a] -> Map PostId (Post a)
indexToIdMap [Post a]
prior)

-- | The ancestry cone: every name appearing on any branch from a post to
-- its roots, as a normalised set — the "who contributed to this" query,
-- free with the log.  Includes the post's own sender.
--
-- Cone-union law:
--
-- > cone (indexToIdMap prior) (synthesis who aud is b)
--     == sortNub (who : concatMap (cone (Map.filterWithKey (\k _ -> k < i) (indexToIdMap prior)) . (priorMap Map.!)) is)
--
-- >>> let p1 = mkPost "tony" ["grok"] "hi" :: Post String; p2 = mkPost "grok" ["tony"] "hello"; r1 = replyTo "kimi" 1 p2 "a"; prior = [p2, p1, r1] in coneByIndex prior (synthesis "sum" [] [2, 0] "Σ") == sortNub ("sum" : concatMap (coneByIndex prior) [r1, p2])
-- True
--
-- >>> let p1 = mkPost "tony" ["grok"] "hi" :: Post String; p2 = mkPost "grok" ["tony"] "hello"; r1 = replyTo "kimi" 1 p2 "a"; prior = [p2, p1, r1] in coneByIndex prior (synthesis "sum" [] [2, 0] "Σ")
-- ["grok","kimi","sum","tony"]
cone :: Map PostId (Post a) -> Post a -> [Name]
cone :: forall a. Map PostId (Post a) -> Post a -> [Name]
cone Map PostId (Post a)
priorMap Post a
p = [Name] -> [Name]
forall a. Ord a => [a] -> [a]
sortNub ([[Name]] -> [Name]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Map PostId (Post a) -> Post a -> [[Name]]
forall a. Map PostId (Post a) -> Post a -> [[Name]]
branches Map PostId (Post a)
priorMap Post a
p))

-- | Convenience wrapper: resolve cone from a chronological list, assigning ids
-- @[0..]@.
coneByIndex :: [Post a] -> Post a -> [Name]
coneByIndex :: forall a. [Post a] -> Post a -> [Name]
coneByIndex [Post a]
prior = Map PostId (Post a) -> Post a -> [Name]
forall a. Map PostId (Post a) -> Post a -> [Name]
cone ([Post a] -> Map PostId (Post a)
forall a. [Post a] -> Map PostId (Post a)
indexToIdMap [Post a]
prior)

-- | The shared append-only log, newest first.
--
-- The log is a stream of 'Post's.  Common case: @Log [Post]@.  Generalizing to
-- any @f@ with 'Cons' and 'Uncons' lets the same delivery machinery run over
-- other stream representations while keeping the addressed read as a list.
type Log f = f

-- | A bag: finite multiset.  Order is forgotten; multiplicity is kept.
newtype Bag a = Bag (Map a Int)
  deriving (Bag a -> Bag a -> Bool
(Bag a -> Bag a -> Bool) -> (Bag a -> Bag a -> Bool) -> Eq (Bag a)
forall a. Eq a => Bag a -> Bag a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Bag a -> Bag a -> Bool
== :: Bag a -> Bag a -> Bool
$c/= :: forall a. Eq a => Bag a -> Bag a -> Bool
/= :: Bag a -> Bag a -> Bool
Eq, Int -> Bag a -> ShowS
[Bag a] -> ShowS
Bag a -> String
(Int -> Bag a -> ShowS)
-> (Bag a -> String) -> ([Bag a] -> ShowS) -> Show (Bag a)
forall a. Show a => Int -> Bag a -> ShowS
forall a. Show a => [Bag a] -> ShowS
forall a. Show a => Bag a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Bag a -> ShowS
showsPrec :: Int -> Bag a -> ShowS
$cshow :: forall a. Show a => Bag a -> String
show :: Bag a -> String
$cshowList :: forall a. Show a => [Bag a] -> ShowS
showList :: [Bag a] -> ShowS
Show)

-- | The empty bag.
emptyBag :: Bag a
emptyBag :: forall a. Bag a
emptyBag = Map a Int -> Bag a
forall a. Map a Int -> Bag a
Bag Map a Int
forall k a. Map k a
Map.empty

-- | One element.
singletonBag :: a -> Bag a
singletonBag :: forall a. a -> Bag a
singletonBag a
a = Map a Int -> Bag a
forall a. Map a Int -> Bag a
Bag (a -> Int -> Map a Int
forall k a. k -> a -> Map k a
Map.singleton a
a Int
1)

-- | Insert one element.
insertBag :: (Ord a) => a -> Bag a -> Bag a
insertBag :: forall a. Ord a => a -> Bag a -> Bag a
insertBag a
a (Bag Map a Int
m) = Map a Int -> Bag a
forall a. Map a Int -> Bag a
Bag ((Int -> Int -> Int) -> a -> Int -> Map a Int -> Map a Int
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) a
a Int
1 Map a Int
m)

-- | Fold a list into a bag, forgetting order.
toBag :: (Ord a) => [a] -> Bag a
toBag :: forall a. Ord a => [a] -> Bag a
toBag = (a -> Bag a -> Bag a) -> Bag a -> [a] -> Bag a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> Bag a -> Bag a
forall a. Ord a => a -> Bag a -> Bag a
insertBag Bag a
forall a. Bag a
emptyBag

-- | Expand a bag into a list in some deterministic order.
fromBag :: Bag a -> [a]
fromBag :: forall a. Bag a -> [a]
fromBag (Bag Map a Int
m) = ((a, Int) -> [a]) -> [(a, Int)] -> [a]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(a
a, Int
n) -> Int -> a -> [a]
forall a. Int -> a -> [a]
replicate Int
n a
a) (Map a Int -> [(a, Int)]
forall k a. Map k a -> [(k, a)]
Map.toList Map a Int
m)

-- | Log algebra: a sequence of bags, one bag per turn.
type TurnLog a = Seq (Bag a)

-- | Agent: a Moore machine with free carrier, polymorphic in the base arrow.
--
-- @System arr s (Mono a b) ≅ arr (s, a) (s, b)@ after collapsing unit
-- positions.  Common log case: @Agent (->) s (Post a) [Post a]@ (input = one post,
-- output = list of posts).  @Agent (K m) s a b@ is the monadic Moore
-- machine.
type Agent arr s a b = System arr s (Mono a b)

-- | Opaque effectful ends: commit an @a@, emit a @b@.
--
-- Common log case: @Shard m [Post] [Post]@.  Pipeline speaks a stream on
-- commit and emit.  Keyboard one-shot:
--
-- @
-- prefixIn (:[])  -- Post -> [Post] on the conjoint
-- @
--
-- Emit is an onslaught of posts (empty = quiet \/ done for that poll).
type Shard m a b = Poles (K m) a b

-- | Same ends shape as 'Shard' — dual seat on the log (journal 013).
type LogEnds m a b = Shard m a b

-- | Build a 'Shard' from monadic commit and emit actions.
shard :: (Monad m) => (a -> m ()) -> m a -> Shard m a a
shard :: forall (m :: * -> *) a.
Monad m =>
(a -> m ()) -> m a -> Shard m a a
shard = (a -> m ()) -> m a -> Poles (K m) a a
forall (m :: * -> *) a b.
Monad m =>
(a -> m ()) -> m b -> Poles (K m) a b
polesK

-- | Build log ends (same as 'shard'; dual seat).
logEnds :: (Monad m) => (a -> m ()) -> m a -> LogEnds m a a
logEnds :: forall (m :: * -> *) a.
Monad m =>
(a -> m ()) -> m a -> Shard m a a
logEnds = (a -> m ()) -> m a -> Poles (K m) a a
forall (m :: * -> *) a b.
Monad m =>
(a -> m ()) -> m b -> Poles (K m) a b
polesK

-- | Born empty, conses each received input onto its history.
--
-- >>> iterateSystem (tape length) [] [1,2,3 :: Int]
-- [1,2,3]
tape :: ([i] -> o) -> Agent (->) [i] i o
tape :: forall i o. ([i] -> o) -> Agent (->) [i] i o
tape [i] -> o
f = (([i], Dir (Mono i o)) -> ([i], Pos (Mono i o)))
-> System (->) [i] (Mono i o)
forall (arr :: * -> * -> *) s (p :: Poly).
arr (s, Dir p) (s, Pos p) -> System arr s p
system ((([i], Dir (Mono i o)) -> ([i], Pos (Mono i o)))
 -> System (->) [i] (Mono i o))
-> (([i], Dir (Mono i o)) -> ([i], Pos (Mono i o)))
-> System (->) [i] (Mono i o)
forall a b. (a -> b) -> a -> b
$ \([i]
hist, Dir (Mono i o)
d) -> (Dir (Mono i (ZonkAny 3)) -> i
forall i o. Dir (Mono i o) -> i
monoDir Dir (Mono i o)
Dir (Mono i (ZonkAny 3))
d i -> [i] -> [i]
forall a. a -> [a] -> [a]
: [i]
hist, ([i] -> o
f [i]
hist, ()))

-- | Like 'tape', but also conses the agent's own output onto its history.
--
-- This is the internal-monologue construction: an agent's outputs are on the
-- same log as its percepts, visible to its own future turns.
selfrec :: ([i] -> i) -> Agent (->) [i] i i
selfrec :: forall i. ([i] -> i) -> Agent (->) [i] i i
selfrec [i] -> i
f = (([i], Dir (Mono i i)) -> ([i], Pos (Mono i i)))
-> System (->) [i] (Mono i i)
forall (arr :: * -> * -> *) s (p :: Poly).
arr (s, Dir p) (s, Pos p) -> System arr s p
system ((([i], Dir (Mono i i)) -> ([i], Pos (Mono i i)))
 -> System (->) [i] (Mono i i))
-> (([i], Dir (Mono i i)) -> ([i], Pos (Mono i i)))
-> System (->) [i] (Mono i i)
forall a b. (a -> b) -> a -> b
$ \([i]
hist, Dir (Mono i i)
d) ->
  let i :: i
i = Dir (Mono i (ZonkAny 2)) -> i
forall i o. Dir (Mono i o) -> i
monoDir Dir (Mono i i)
Dir (Mono i (ZonkAny 2))
d
      h' :: [i]
h' = i
i i -> [i] -> [i]
forall a. a -> [a] -> [a]
: [i]
hist
   in ([i] -> i
f [i]
h' i -> [i] -> [i]
forall a. a -> [a] -> [a]
: [i]
h', ([i] -> i
f [i]
hist, ()))

-- | Addressed stream of unread posts for one agent.
--
-- The 'Inbox' owns a list of subscribed names and the unread stream.  Only
-- posts whose 'to' list intersects the subscription list are peeled by
-- 'unconsInbox'.  The common case is a singleton subscription @[agentName]@;
-- multi-cast wires list several names.
newtype Inbox f = Inbox {forall f. Inbox f -> ([Name], f)
unInbox :: ([Name], f)}
  deriving (Int -> Inbox f -> ShowS
[Inbox f] -> ShowS
Inbox f -> String
(Int -> Inbox f -> ShowS)
-> (Inbox f -> String) -> ([Inbox f] -> ShowS) -> Show (Inbox f)
forall f. Show f => Int -> Inbox f -> ShowS
forall f. Show f => [Inbox f] -> ShowS
forall f. Show f => Inbox f -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall f. Show f => Int -> Inbox f -> ShowS
showsPrec :: Int -> Inbox f -> ShowS
$cshow :: forall f. Show f => Inbox f -> String
show :: Inbox f -> String
$cshowList :: forall f. Show f => [Inbox f] -> ShowS
showList :: [Inbox f] -> ShowS
Show, Inbox f -> Inbox f -> Bool
(Inbox f -> Inbox f -> Bool)
-> (Inbox f -> Inbox f -> Bool) -> Eq (Inbox f)
forall f. Eq f => Inbox f -> Inbox f -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall f. Eq f => Inbox f -> Inbox f -> Bool
== :: Inbox f -> Inbox f -> Bool
$c/= :: forall f. Eq f => Inbox f -> Inbox f -> Bool
/= :: Inbox f -> Inbox f -> Bool
Eq)

-- | Primary owner of the inbox (head of the subscription list).
inboxWho :: Inbox f -> Name
inboxWho :: forall f. Inbox f -> Name
inboxWho = Name -> Maybe Name -> Name
forall a. a -> Maybe a -> a
fromMaybe Name
empty (Maybe Name -> Name) -> (Inbox f -> Maybe Name) -> Inbox f -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> Maybe Name
forall a. [a] -> Maybe a
listToMaybe ([Name] -> Maybe Name)
-> (Inbox f -> [Name]) -> Inbox f -> Maybe Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Name], f) -> [Name]
forall a b. (a, b) -> a
fst (([Name], f) -> [Name])
-> (Inbox f -> ([Name], f)) -> Inbox f -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Inbox f -> ([Name], f)
forall f. Inbox f -> ([Name], f)
unInbox

-- | Full subscription list for the inbox.
inboxSubs :: Inbox f -> [Name]
inboxSubs :: forall f. Inbox f -> [Name]
inboxSubs = ([Name], f) -> [Name]
forall a b. (a, b) -> a
fst (([Name], f) -> [Name])
-> (Inbox f -> ([Name], f)) -> Inbox f -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Inbox f -> ([Name], f)
forall f. Inbox f -> ([Name], f)
unInbox

-- | Empty inbox for the subscribed agent(s).
emptyInbox :: forall a f. (Uncons f (Post a)) => [Name] -> Inbox f
emptyInbox :: forall a f. Uncons f (Post a) => [Name] -> Inbox f
emptyInbox [Name]
subs = ([Name], f) -> Inbox f
forall f. ([Name], f) -> Inbox f
Inbox ([Name]
subs, forall f s. Uncons f s => f
nil @f @(Post a))

-- | Append a post to the right of the inbox.
appendInbox :: (Snoc f (Post a)) => Post a -> Inbox f -> Inbox f
appendInbox :: forall f a. Snoc f (Post a) => Post a -> Inbox f -> Inbox f
appendInbox Post a
p (Inbox ([Name]
subs, f
f)) = ([Name], f) -> Inbox f
forall f. ([Name], f) -> Inbox f
Inbox ([Name]
subs, f -> Post a -> f
forall f s. Snoc f s => f -> s -> f
snoc f
f Post a
p)

-- | Lightweight delivery predicate.
--
-- A post delivers when any of the subscribed names appears in the post's 'to'
-- list.  Multi-cast is direct: a post addressed to several names reaches each
-- subscriber.  A post with @to = ["all"]@ broadcasts to every subscriber;
-- @to = []@ and @to = [""]@ deliver to no one (discard).  This predicate is a
-- small stepping stone toward a relational copy/discard delivery model
-- ('FinRel'); the full wiring is future work.
deliversTo :: Post a -> [Name] -> Bool
deliversTo :: forall a. Post a -> [Name] -> Bool
deliversTo Post a
p [Name]
subs =
  case Post a -> [Name]
forall a. Post a -> [Name]
to Post a
p of
    [] -> Bool
False
    [Name
t] | Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
empty -> Bool
False
    [Name]
ts -> (Name
"all" :: Text) Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
ts Bool -> Bool -> Bool
|| (Name -> Bool) -> [Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
ts) [Name]
subs

-- | Peel the oldest addressed post from the inbox, returning the rest.
--
-- Non-matching posts are skipped and discarded.  An empty or exhausted inbox
-- returns 'That' with an empty inbox.
unconsInbox :: forall a f. (Uncons f (Post a)) => Inbox f -> These (Post a) (Inbox f)
unconsInbox :: forall a f.
Uncons f (Post a) =>
Inbox f -> These (Post a) (Inbox f)
unconsInbox (Inbox ([Name]
subs, f
f)) = f -> These (Post a) (Inbox f)
go f
f
  where
    go :: f -> These (Post a) (Inbox f)
go f
stream = case f -> These (Post a) f
forall f s. Uncons f s => f -> These s f
uncons f
stream of
      That f
rest -> Inbox f -> These (Post a) (Inbox f)
forall a b. b -> These a b
That (([Name], f) -> Inbox f
forall f. ([Name], f) -> Inbox f
Inbox ([Name]
subs, f
rest))
      This Post a
p
        | Post a -> [Name] -> Bool
forall a. Post a -> [Name] -> Bool
deliversTo Post a
p [Name]
subs -> Post a -> These (Post a) (Inbox f)
forall a b. a -> These a b
This Post a
p
        | Bool
otherwise -> Inbox f -> These (Post a) (Inbox f)
forall a b. b -> These a b
That (forall a f. Uncons f (Post a) => [Name] -> Inbox f
emptyInbox @a [Name]
subs)
      These Post a
p f
rest
        | Post a -> [Name] -> Bool
forall a. Post a -> [Name] -> Bool
deliversTo Post a
p [Name]
subs -> Post a -> Inbox f -> These (Post a) (Inbox f)
forall a b. a -> b -> These a b
These Post a
p (([Name], f) -> Inbox f
forall f. ([Name], f) -> Inbox f
Inbox ([Name]
subs, f
rest))
        | Bool
otherwise -> f -> These (Post a) (Inbox f)
go f
rest

-- | State for a pure agent in delivery: free carrier plus an addressed inbox.
data AgentState s f = AgentState
  { forall s f. AgentState s f -> s
asCarrier :: s,
    forall s f. AgentState s f -> Inbox f
asInbox :: Inbox f
  }
  deriving (Int -> AgentState s f -> ShowS
[AgentState s f] -> ShowS
AgentState s f -> String
(Int -> AgentState s f -> ShowS)
-> (AgentState s f -> String)
-> ([AgentState s f] -> ShowS)
-> Show (AgentState s f)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s f. (Show s, Show f) => Int -> AgentState s f -> ShowS
forall s f. (Show s, Show f) => [AgentState s f] -> ShowS
forall s f. (Show s, Show f) => AgentState s f -> String
$cshowsPrec :: forall s f. (Show s, Show f) => Int -> AgentState s f -> ShowS
showsPrec :: Int -> AgentState s f -> ShowS
$cshow :: forall s f. (Show s, Show f) => AgentState s f -> String
show :: AgentState s f -> String
$cshowList :: forall s f. (Show s, Show f) => [AgentState s f] -> ShowS
showList :: [AgentState s f] -> ShowS
Show, AgentState s f -> AgentState s f -> Bool
(AgentState s f -> AgentState s f -> Bool)
-> (AgentState s f -> AgentState s f -> Bool)
-> Eq (AgentState s f)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall s f.
(Eq s, Eq f) =>
AgentState s f -> AgentState s f -> Bool
$c== :: forall s f.
(Eq s, Eq f) =>
AgentState s f -> AgentState s f -> Bool
== :: AgentState s f -> AgentState s f -> Bool
$c/= :: forall s f.
(Eq s, Eq f) =>
AgentState s f -> AgentState s f -> Bool
/= :: AgentState s f -> AgentState s f -> Bool
Eq)

-- | A node in the meeting's derivation tree.
--
-- 'dChildren' is kept flat (empty) in this pass.  Building the causal child
-- tree from routed outputs is future work.
data Derivation a = Derivation
  { forall a. Derivation a -> Name
dAgent :: Name,
    forall a. Derivation a -> Post a
dInput :: Post a,
    forall a. Derivation a -> [Post a]
dOutputs :: [Post a],
    forall a. Derivation a -> [Derivation a]
dChildren :: [Derivation a]
  }
  deriving (Int -> Derivation a -> ShowS
[Derivation a] -> ShowS
Derivation a -> String
(Int -> Derivation a -> ShowS)
-> (Derivation a -> String)
-> ([Derivation a] -> ShowS)
-> Show (Derivation a)
forall a. Show a => Int -> Derivation a -> ShowS
forall a. Show a => [Derivation a] -> ShowS
forall a. Show a => Derivation a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Derivation a -> ShowS
showsPrec :: Int -> Derivation a -> ShowS
$cshow :: forall a. Show a => Derivation a -> String
show :: Derivation a -> String
$cshowList :: forall a. Show a => [Derivation a] -> ShowS
showList :: [Derivation a] -> ShowS
Show, Derivation a -> Derivation a -> Bool
(Derivation a -> Derivation a -> Bool)
-> (Derivation a -> Derivation a -> Bool) -> Eq (Derivation a)
forall a. Eq a => Derivation a -> Derivation a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Derivation a -> Derivation a -> Bool
== :: Derivation a -> Derivation a -> Bool
$c/= :: forall a. Eq a => Derivation a -> Derivation a -> Bool
/= :: Derivation a -> Derivation a -> Bool
Eq)

-- | Empty carrier and empty inbox for the named agent.
emptyAgentState :: forall a s f. (Snoc s (Post a), Uncons f (Post a)) => [Name] -> AgentState s f
emptyAgentState :: forall a s f.
(Snoc s (Post a), Uncons f (Post a)) =>
[Name] -> AgentState s f
emptyAgentState [Name]
subs = s -> Inbox f -> AgentState s f
forall s f. s -> Inbox f -> AgentState s f
AgentState (forall f s. Snoc f s => f
snocNil @s @(Post a)) (forall a f. Uncons f (Post a) => [Name] -> Inbox f
emptyInbox @a [Name]
subs)

-- | Seed an inbox with all posts addressed to any subscription from the log,
-- oldest first.
seedInbox :: forall a f. (Snoc f (Post a), Uncons f (Post a)) => [Name] -> Log f -> Inbox f
seedInbox :: forall a f.
(Snoc f (Post a), Uncons f (Post a)) =>
[Name] -> f -> Inbox f
seedInbox [Name]
subs f
lg = (Inbox f -> Post a -> Inbox f) -> Inbox f -> [Post a] -> Inbox f
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((Post a -> Inbox f -> Inbox f) -> Inbox f -> Post a -> Inbox f
forall a b c. (a -> b -> c) -> b -> a -> c
flip Post a -> Inbox f -> Inbox f
forall f a. Snoc f (Post a) => Post a -> Inbox f -> Inbox f
appendInbox) (forall a f. Uncons f (Post a) => [Name] -> Inbox f
emptyInbox @a [Name]
subs) (forall a f. Uncons f (Post a) => [Name] -> f -> [Post a]
watch @a [Name]
subs f
lg)

-- | Empty carrier and an inbox seeded from the log for the subscribed agent(s).
seedAgentState :: forall a s f. (Snoc s (Post a), Snoc f (Post a), Uncons f (Post a)) => [Name] -> Log f -> AgentState s f
seedAgentState :: forall a s f.
(Snoc s (Post a), Snoc f (Post a), Uncons f (Post a)) =>
[Name] -> f -> AgentState s f
seedAgentState [Name]
subs f
lg = s -> Inbox f -> AgentState s f
forall s f. s -> Inbox f -> AgentState s f
AgentState (forall f s. Snoc f s => f
snocNil @s @(Post a)) (forall a f.
(Snoc f (Post a), Uncons f (Post a)) =>
[Name] -> f -> Inbox f
seedInbox @a [Name]
subs f
lg)

-- | Empty log.
emptyLog :: forall a f. (Cons f (Post a)) => Log f
emptyLog :: forall a f. Cons f (Post a) => f
emptyLog = forall f s. Cons f s => f
consNil @f @(Post a)

-- | Read end of the log: all posts matching any subscription, oldest first.
--
-- Traversal is newest-to-oldest; matching posts are prepended, so the
-- accumulator is already oldest-first.
watch :: forall a f. (Uncons f (Post a)) => [Name] -> Log f -> [Post a]
watch :: forall a f. Uncons f (Post a) => [Name] -> f -> [Post a]
watch [Name]
subs f
t = f -> [Post a] -> [Post a]
go f
t []
  where
    go :: f -> [Post a] -> [Post a]
go f
stream [Post a]
acc =
      case f -> These (Post a) f
forall f s. Uncons f s => f -> These s f
uncons f
stream of
        That f
_ -> [Post a]
acc
        This Post a
p -> if Post a -> [Name] -> Bool
forall a. Post a -> [Name] -> Bool
deliversTo Post a
p [Name]
subs then Post a
p Post a -> [Post a] -> [Post a]
forall a. a -> [a] -> [a]
: [Post a]
acc else [Post a]
acc
        These Post a
p f
rest -> f -> [Post a] -> [Post a]
go f
rest (if Post a -> [Name] -> Bool
forall a. Post a -> [Name] -> Bool
deliversTo Post a
p [Name]
subs then Post a
p Post a -> [Post a] -> [Post a]
forall a. a -> [a] -> [a]
: [Post a]
acc else [Post a]
acc)

-- | Write end of the log: commit a post.
post :: (Cons f (Post a)) => Post a -> Log f -> Log f
post :: forall f a. Cons f (Post a) => Post a -> f -> f
post = Post a -> f -> f
forall f s. Cons f s => s -> f -> f
cons

-- | Per-agent session assembly: the bodies an agent actually sees.
session :: (Uncons f (Post a)) => [Name] -> Log f -> [a]
session :: forall f a. Uncons f (Post a) => [Name] -> f -> [a]
session [Name]
subs = (Post a -> a) -> [Post a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map Post a -> a
forall a. Post a -> a
body ([Post a] -> [a]) -> (f -> [Post a]) -> f -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> f -> [Post a]
forall a f. Uncons f (Post a) => [Name] -> f -> [Post a]
watch [Name]
subs

-- | One delivery round: peel one addressed post, step the machine, 'post' each output.
--
-- The 'AgentState' carries the free carrier @s@ and an addressed inbox.  Only
-- one post is consumed per call; repeated calls drain the inbox.  Outputs are
-- committed newest-first via 'post'.  When a post is processed, the returned
-- 'Derivation' records the agent name, the input post, and the emitted outputs.
--
-- 'turnAs' lets the caller supply the agent identity used in the derivation;
-- this matters when an inbox has multiple subscriptions (card-addressing) and
-- the first subscription is not the agent's own name.
turnAs ::
  forall a s f.
  (Cons f (Post a), Uncons f (Post a)) =>
  -- | Agent identity recorded in the derivation.
  Name ->
  Agent (->) s (Post a) [Post a] ->
  AgentState s f ->
  Log f ->
  (AgentState s f, Log f, Maybe (Derivation a))
turnAs :: forall a s f.
(Cons f (Post a), Uncons f (Post a)) =>
Name
-> Agent (->) s (Post a) [Post a]
-> AgentState s f
-> f
-> (AgentState s f, f, Maybe (Derivation a))
turnAs Name
who Agent (->) s (Post a) [Post a]
sys AgentState s f
st f
log0 =
  let subs :: [Name]
subs = Inbox f -> [Name]
forall f. Inbox f -> [Name]
inboxSubs (AgentState s f -> Inbox f
forall s f. AgentState s f -> Inbox f
asInbox AgentState s f
st)
   in case forall a f.
Uncons f (Post a) =>
Inbox f -> These (Post a) (Inbox f)
unconsInbox @a (AgentState s f -> Inbox f
forall s f. AgentState s f -> Inbox f
asInbox AgentState s f
st) of
        That Inbox f
_ -> (AgentState s f
st, f
log0, Maybe (Derivation a)
forall a. Maybe a
Nothing)
        This Post a
p ->
          let ([Post a]
os, s
seen') = Agent (->) s (Post a) [Post a] -> s -> Post a -> ([Post a], s)
forall s i o. Agent (->) s i o -> s -> i -> (o, s)
run1 Agent (->) s (Post a) [Post a]
sys (AgentState s f -> s
forall s f. AgentState s f -> s
asCarrier AgentState s f
st) Post a
p
           in (s -> Inbox f -> AgentState s f
forall s f. s -> Inbox f -> AgentState s f
AgentState s
seen' (forall a f. Uncons f (Post a) => [Name] -> Inbox f
emptyInbox @a [Name]
subs), (f -> Post a -> f) -> f -> [Post a] -> f
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((Post a -> f -> f) -> f -> Post a -> f
forall a b c. (a -> b -> c) -> b -> a -> c
flip Post a -> f -> f
forall f a. Cons f (Post a) => Post a -> f -> f
post) f
log0 [Post a]
os, Derivation a -> Maybe (Derivation a)
forall a. a -> Maybe a
Just (Name -> Post a -> [Post a] -> [Derivation a] -> Derivation a
forall a.
Name -> Post a -> [Post a] -> [Derivation a] -> Derivation a
Derivation Name
who Post a
p [Post a]
os []))
        These Post a
p Inbox f
rest ->
          let ([Post a]
os, s
seen') = Agent (->) s (Post a) [Post a] -> s -> Post a -> ([Post a], s)
forall s i o. Agent (->) s i o -> s -> i -> (o, s)
run1 Agent (->) s (Post a) [Post a]
sys (AgentState s f -> s
forall s f. AgentState s f -> s
asCarrier AgentState s f
st) Post a
p
           in (s -> Inbox f -> AgentState s f
forall s f. s -> Inbox f -> AgentState s f
AgentState s
seen' Inbox f
rest, (f -> Post a -> f) -> f -> [Post a] -> f
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((Post a -> f -> f) -> f -> Post a -> f
forall a b c. (a -> b -> c) -> b -> a -> c
flip Post a -> f -> f
forall f a. Cons f (Post a) => Post a -> f -> f
post) f
log0 [Post a]
os, Derivation a -> Maybe (Derivation a)
forall a. a -> Maybe a
Just (Name -> Post a -> [Post a] -> [Derivation a] -> Derivation a
forall a.
Name -> Post a -> [Post a] -> [Derivation a] -> Derivation a
Derivation Name
who Post a
p [Post a]
os []))

-- | 'turn' with the agent identity taken from the inbox's first subscription.
--
-- For single-subscription inboxes this is the agent's own name; for
-- multi-subscription inboxes use 'turnAs'.
turn ::
  forall a s f.
  (Cons f (Post a), Uncons f (Post a)) =>
  Agent (->) s (Post a) [Post a] ->
  AgentState s f ->
  Log f ->
  (AgentState s f, Log f, Maybe (Derivation a))
turn :: forall a s f.
(Cons f (Post a), Uncons f (Post a)) =>
Agent (->) s (Post a) [Post a]
-> AgentState s f -> f -> (AgentState s f, f, Maybe (Derivation a))
turn Agent (->) s (Post a) [Post a]
sys AgentState s f
st = Name
-> Agent (->) s (Post a) [Post a]
-> AgentState s f
-> f
-> (AgentState s f, f, Maybe (Derivation a))
forall a s f.
(Cons f (Post a), Uncons f (Post a)) =>
Name
-> Agent (->) s (Post a) [Post a]
-> AgentState s f
-> f
-> (AgentState s f, f, Maybe (Derivation a))
turnAs (Inbox f -> Name
forall f. Inbox f -> Name
inboxWho (AgentState s f -> Inbox f
forall s f. AgentState s f -> Inbox f
asInbox AgentState s f
st)) Agent (->) s (Post a) [Post a]
sys AgentState s f
st

-- | Whether the agent's inbox has an addressed post waiting.
hasPending :: forall a s f. (Uncons f (Post a)) => AgentState s f -> Bool
hasPending :: forall a s f. Uncons f (Post a) => AgentState s f -> Bool
hasPending AgentState s f
st = case forall a f.
Uncons f (Post a) =>
Inbox f -> These (Post a) (Inbox f)
unconsInbox @a (AgentState s f -> Inbox f
forall s f. AgentState s f -> Inbox f
asInbox AgentState s f
st) of That Inbox f
_ -> Bool
False; These (Post a) (Inbox f)
_ -> Bool
True

-- | Stream length via 'Uncons'.
streamLength :: forall f a. (Uncons f a) => f -> Int
streamLength :: forall f a. Uncons f a => f -> Int
streamLength = Int -> f -> Int
go Int
0
  where
    go :: Int -> f -> Int
    go :: Int -> f -> Int
go Int
n f
stream =
      case forall f s. Uncons f s => f -> These s f
uncons @f @a f
stream of
        That f
_ -> Int
n
        This a
_ -> Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
        These a
_ f
rest -> Int -> f -> Int
go (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) f
rest

-- | Take the first @n@ tokens from a stream, returning them as a list in
-- reverse order (oldest-first when the stream itself is newest-first).
takeStream :: forall f a. (Uncons f a) => Int -> f -> [a]
takeStream :: forall f a. Uncons f a => Int -> f -> [a]
takeStream Int
n f
s = Int -> f -> [a] -> [a]
go Int
n f
s []
  where
    go :: Int -> f -> [a] -> [a]
    go :: Int -> f -> [a] -> [a]
go Int
0 f
_ [a]
acc = [a]
acc
    go Int
n' f
stream [a]
acc =
      case forall f s. Uncons f s => f -> These s f
uncons @f @a f
stream of
        That f
_ -> [a]
acc
        This a
x -> a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
acc
        These a
x f
rest -> Int -> f -> [a] -> [a]
go (Int
n' Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) f
rest (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
acc)

-- | A roster entry with explicit subscriptions: agent name, subscription names,
-- and the agent itself.  The subscription list is the set of names whose posts
-- the agent's inbox should receive; the agent's own name need not be in it.
type RosterEntry s a = (Name, [Name], Agent (->) s (Post a) [Post a])

-- | Round-robin turn-loop until no agent has pending deliveries (quiescence).
--
-- Roster order is the schedule.  Each pass runs 'turn' for every agent that
-- still has pending work at its slot.  Passes repeat until a pass starts with
-- nobody pending.  Carriers start empty for every name.
loop ::
  forall a s f.
  (Snoc s (Post a), Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
  [(Name, Agent (->) s (Post a) [Post a])] ->
  Log f ->
  ([(Name, AgentState s f)], Log f, [Derivation a])
loop :: forall a s f.
(Snoc s (Post a), Snoc f (Post a), Cons f (Post a),
 Uncons f (Post a)) =>
[(Name, Agent (->) s (Post a) [Post a])]
-> f -> ([(Name, AgentState s f)], f, [Derivation a])
loop [(Name, Agent (->) s (Post a) [Post a])]
roster = [RosterEntry s a]
-> f -> ([(Name, AgentState s f)], f, [Derivation a])
forall a s f.
(Snoc s (Post a), Snoc f (Post a), Cons f (Post a),
 Uncons f (Post a)) =>
[RosterEntry s a]
-> f -> ([(Name, AgentState s f)], f, [Derivation a])
loopSubs [(Name
n, [Name
n], Agent (->) s (Post a) [Post a]
a) | (Name
n, Agent (->) s (Post a) [Post a]
a) <- [(Name, Agent (->) s (Post a) [Post a])]
roster]

-- | Multi-seat-card variant of 'loop': each agent carries its own subscription
-- list, so several agents can share a card name.
loopSubs ::
  forall a s f.
  (Snoc s (Post a), Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
  [RosterEntry s a] ->
  Log f ->
  ([(Name, AgentState s f)], Log f, [Derivation a])
loopSubs :: forall a s f.
(Snoc s (Post a), Snoc f (Post a), Cons f (Post a),
 Uncons f (Post a)) =>
[RosterEntry s a]
-> f -> ([(Name, AgentState s f)], f, [Derivation a])
loopSubs [RosterEntry s a]
roster f
log0 = [RosterEntry s a]
-> [(Name, AgentState s f)]
-> f
-> ([(Name, AgentState s f)], f, [Derivation a])
forall a s f.
(Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
[RosterEntry s a]
-> [(Name, AgentState s f)]
-> f
-> ([(Name, AgentState s f)], f, [Derivation a])
loopWithSubs [RosterEntry s a]
roster [(Name
n, forall a s f.
(Snoc s (Post a), Snoc f (Post a), Uncons f (Post a)) =>
[Name] -> f -> AgentState s f
seedAgentState @a @s @f [Name]
subs f
log0) | (Name
n, [Name]
subs, Agent (->) s (Post a) [Post a]
_) <- [RosterEntry s a]
roster] f
log0

-- | Resumable 'loop': supply the initial states and inboxes.
--
-- Implemented as an 'Either' trace over the roster: each pass is one
-- iteration of the feedback channel, quiescence returns a 'Right' result.
--
-- Backwards-compatible wrapper; for explicit subscriptions use 'loopWithSubs'.
loopWith ::
  forall a s f.
  (Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
  [(Name, Agent (->) s (Post a) [Post a])] ->
  [(Name, AgentState s f)] ->
  Log f ->
  ([(Name, AgentState s f)], Log f, [Derivation a])
loopWith :: forall a s f.
(Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
[(Name, Agent (->) s (Post a) [Post a])]
-> [(Name, AgentState s f)]
-> f
-> ([(Name, AgentState s f)], f, [Derivation a])
loopWith [(Name, Agent (->) s (Post a) [Post a])]
roster = [RosterEntry s a]
-> [(Name, AgentState s f)]
-> f
-> ([(Name, AgentState s f)], f, [Derivation a])
forall a s f.
(Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
[RosterEntry s a]
-> [(Name, AgentState s f)]
-> f
-> ([(Name, AgentState s f)], f, [Derivation a])
loopWithSubs [(Name
n, [Name
n], Agent (->) s (Post a) [Post a]
a) | (Name
n, Agent (->) s (Post a) [Post a]
a) <- [(Name, Agent (->) s (Post a) [Post a])]
roster]

-- | Multi-seat-card variant of 'loopWith'.
loopWithSubs ::
  forall a s f.
  (Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
  [RosterEntry s a] ->
  [(Name, AgentState s f)] ->
  Log f ->
  ([(Name, AgentState s f)], Log f, [Derivation a])
loopWithSubs :: forall a s f.
(Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
[RosterEntry s a]
-> [(Name, AgentState s f)]
-> f
-> ([(Name, AgentState s f)], f, [Derivation a])
loopWithSubs [RosterEntry s a]
roster [(Name, AgentState s f)]
states0 f
log0 = (Either ([(Name, AgentState s f)], f, [Derivation a]) ()
 -> Either
      ([(Name, AgentState s f)], f, [Derivation a])
      ([(Name, AgentState s f)], f, [Derivation a]))
-> () -> ([(Name, AgentState s f)], f, [Derivation a])
forall a b c. (Either a b -> Either a c) -> b -> c
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Traced t arr =>
arr (t a b) (t a c) -> arr b c
trace Either ([(Name, AgentState s f)], f, [Derivation a]) ()
-> Either
     ([(Name, AgentState s f)], f, [Derivation a])
     ([(Name, AgentState s f)], f, [Derivation a])
body ()
  where
    bundle0 :: ([(Name, AgentState s f)], f, [Derivation a])
bundle0 = ([(Name, AgentState s f)]
states0, f
log0, []) :: ([(Name, AgentState s f)], Log f, [Derivation a])
    body :: Either ([(Name, AgentState s f)], f, [Derivation a]) ()
-> Either
     ([(Name, AgentState s f)], f, [Derivation a])
     ([(Name, AgentState s f)], f, [Derivation a])
body (Right ()) =
      if ((Name, AgentState s f) -> Bool)
-> [(Name, AgentState s f)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a s f. Uncons f (Post a) => AgentState s f -> Bool
hasPending @a (AgentState s f -> Bool)
-> ((Name, AgentState s f) -> AgentState s f)
-> (Name, AgentState s f)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, AgentState s f) -> AgentState s f
forall a b. (a, b) -> b
snd) [(Name, AgentState s f)]
states0
        then ([(Name, AgentState s f)], f, [Derivation a])
-> Either
     ([(Name, AgentState s f)], f, [Derivation a])
     ([(Name, AgentState s f)], f, [Derivation a])
forall a b. a -> Either a b
Left ([(Name, AgentState s f)], f, [Derivation a])
bundle0
        else ([(Name, AgentState s f)], f, [Derivation a])
-> Either
     ([(Name, AgentState s f)], f, [Derivation a])
     ([(Name, AgentState s f)], f, [Derivation a])
forall a b. b -> Either a b
Right ([(Name, AgentState s f)], f, [Derivation a])
bundle0
    body (Left ([(Name, AgentState s f)], f, [Derivation a])
bundle) =
      let bundle' :: ([(Name, AgentState s f)], f, [Derivation a])
bundle' = [RosterEntry s a]
-> ([(Name, AgentState s f)], f, [Derivation a])
-> ([(Name, AgentState s f)], f, [Derivation a])
forall a s f.
(Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
[RosterEntry s a]
-> ([(Name, AgentState s f)], f, [Derivation a])
-> ([(Name, AgentState s f)], f, [Derivation a])
meetingPass [RosterEntry s a]
roster ([(Name, AgentState s f)], f, [Derivation a])
bundle
       in if ((Name, AgentState s f) -> Bool)
-> [(Name, AgentState s f)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a s f. Uncons f (Post a) => AgentState s f -> Bool
hasPending @a (AgentState s f -> Bool)
-> ((Name, AgentState s f) -> AgentState s f)
-> (Name, AgentState s f)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, AgentState s f) -> AgentState s f
forall a b. (a, b) -> b
snd) (([(Name, AgentState s f)], f, [Derivation a])
-> [(Name, AgentState s f)]
forall {a} {b} {c}. (a, b, c) -> a
fst3 ([(Name, AgentState s f)], f, [Derivation a])
bundle')
            then ([(Name, AgentState s f)], f, [Derivation a])
-> Either
     ([(Name, AgentState s f)], f, [Derivation a])
     ([(Name, AgentState s f)], f, [Derivation a])
forall a b. a -> Either a b
Left ([(Name, AgentState s f)], f, [Derivation a])
bundle'
            else ([(Name, AgentState s f)], f, [Derivation a])
-> Either
     ([(Name, AgentState s f)], f, [Derivation a])
     ([(Name, AgentState s f)], f, [Derivation a])
forall a b. b -> Either a b
Right ([(Name, AgentState s f)], f, [Derivation a])
bundle'
    fst3 :: (a, b, c) -> a
fst3 (a
x, b
_, c
_) = a
x

-- | The same meeting as a 'Trace' value: 'yank' body over the 'Either'
-- tensor, quiescence returned as a 'Right' payload.
--
-- Backwards-compatible wrapper; for explicit subscriptions use 'meetingLoopSubs'.
meetingLoop ::
  forall a s f.
  (Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
  [(Name, Agent (->) s (Post a) [Post a])] ->
  Trace Either (->) ([(Name, AgentState s f)], Log f, [Derivation a]) ([(Name, AgentState s f)], Log f, [Derivation a])
meetingLoop :: forall a s f.
(Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
[(Name, Agent (->) s (Post a) [Post a])]
-> Trace
     Either
     (->)
     ([(Name, AgentState s f)], f, [Derivation a])
     ([(Name, AgentState s f)], f, [Derivation a])
meetingLoop [(Name, Agent (->) s (Post a) [Post a])]
roster = [RosterEntry s a]
-> Trace
     Either
     (->)
     ([(Name, AgentState s f)], f, [Derivation a])
     ([(Name, AgentState s f)], f, [Derivation a])
forall a s f.
(Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
[RosterEntry s a]
-> Trace
     Either
     (->)
     ([(Name, AgentState s f)], f, [Derivation a])
     ([(Name, AgentState s f)], f, [Derivation a])
meetingLoopSubs [(Name
n, [Name
n], Agent (->) s (Post a) [Post a]
a) | (Name
n, Agent (->) s (Post a) [Post a]
a) <- [(Name, Agent (->) s (Post a) [Post a])]
roster]

-- | Multi-seat-card variant of 'meetingLoop'.
meetingLoopSubs ::
  forall a s f.
  (Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
  [RosterEntry s a] ->
  Trace Either (->) ([(Name, AgentState s f)], Log f, [Derivation a]) ([(Name, AgentState s f)], Log f, [Derivation a])
meetingLoopSubs :: forall a s f.
(Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
[RosterEntry s a]
-> Trace
     Either
     (->)
     ([(Name, AgentState s f)], f, [Derivation a])
     ([(Name, AgentState s f)], f, [Derivation a])
meetingLoopSubs [RosterEntry s a]
roster = Trace
  Either
  (->)
  (Either
     ([(Name, AgentState s f)], f, [Derivation a])
     ([(Name, AgentState s f)], f, [Derivation a]))
  (Either
     ([(Name, AgentState s f)], f, [Derivation a])
     ([(Name, AgentState s f)], f, [Derivation a]))
-> Trace
     Either
     (->)
     ([(Name, AgentState s f)], f, [Derivation a])
     ([(Name, AgentState s f)], f, [Derivation a])
forall (t :: * -> * -> *) (arr :: * -> * -> *) s a b.
Trace t arr (t s a) (t s b) -> Trace t arr a b
yank ((Either
   ([(Name, AgentState s f)], f, [Derivation a])
   ([(Name, AgentState s f)], f, [Derivation a])
 -> Either
      ([(Name, AgentState s f)], f, [Derivation a])
      ([(Name, AgentState s f)], f, [Derivation a]))
-> Trace
     Either
     (->)
     (Either
        ([(Name, AgentState s f)], f, [Derivation a])
        ([(Name, AgentState s f)], f, [Derivation a]))
     (Either
        ([(Name, AgentState s f)], f, [Derivation a])
        ([(Name, AgentState s f)], f, [Derivation a]))
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base Either
  ([(Name, AgentState s f)], f, [Derivation a])
  ([(Name, AgentState s f)], f, [Derivation a])
-> Either
     ([(Name, AgentState s f)], f, [Derivation a])
     ([(Name, AgentState s f)], f, [Derivation a])
body)
  where
    body :: Either
  ([(Name, AgentState s f)], f, [Derivation a])
  ([(Name, AgentState s f)], f, [Derivation a])
-> Either
     ([(Name, AgentState s f)], f, [Derivation a])
     ([(Name, AgentState s f)], f, [Derivation a])
body (Right bundle :: ([(Name, AgentState s f)], f, [Derivation a])
bundle@([(Name, AgentState s f)]
states, f
_, [Derivation a]
_)) =
      if ((Name, AgentState s f) -> Bool)
-> [(Name, AgentState s f)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a s f. Uncons f (Post a) => AgentState s f -> Bool
hasPending @a (AgentState s f -> Bool)
-> ((Name, AgentState s f) -> AgentState s f)
-> (Name, AgentState s f)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, AgentState s f) -> AgentState s f
forall a b. (a, b) -> b
snd) [(Name, AgentState s f)]
states
        then ([(Name, AgentState s f)], f, [Derivation a])
-> Either
     ([(Name, AgentState s f)], f, [Derivation a])
     ([(Name, AgentState s f)], f, [Derivation a])
forall a b. a -> Either a b
Left ([(Name, AgentState s f)], f, [Derivation a])
bundle
        else ([(Name, AgentState s f)], f, [Derivation a])
-> Either
     ([(Name, AgentState s f)], f, [Derivation a])
     ([(Name, AgentState s f)], f, [Derivation a])
forall a b. b -> Either a b
Right ([(Name, AgentState s f)], f, [Derivation a])
bundle
    body (Left ([(Name, AgentState s f)], f, [Derivation a])
bundle) =
      let bundle' :: ([(Name, AgentState s f)], f, [Derivation a])
bundle'@([(Name, AgentState s f)]
states', f
_, [Derivation a]
_) = [RosterEntry s a]
-> ([(Name, AgentState s f)], f, [Derivation a])
-> ([(Name, AgentState s f)], f, [Derivation a])
forall a s f.
(Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
[RosterEntry s a]
-> ([(Name, AgentState s f)], f, [Derivation a])
-> ([(Name, AgentState s f)], f, [Derivation a])
meetingPass [RosterEntry s a]
roster ([(Name, AgentState s f)], f, [Derivation a])
bundle
       in if ((Name, AgentState s f) -> Bool)
-> [(Name, AgentState s f)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a s f. Uncons f (Post a) => AgentState s f -> Bool
hasPending @a (AgentState s f -> Bool)
-> ((Name, AgentState s f) -> AgentState s f)
-> (Name, AgentState s f)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, AgentState s f) -> AgentState s f
forall a b. (a, b) -> b
snd) [(Name, AgentState s f)]
states'
            then ([(Name, AgentState s f)], f, [Derivation a])
-> Either
     ([(Name, AgentState s f)], f, [Derivation a])
     ([(Name, AgentState s f)], f, [Derivation a])
forall a b. a -> Either a b
Left ([(Name, AgentState s f)], f, [Derivation a])
bundle'
            else ([(Name, AgentState s f)], f, [Derivation a])
-> Either
     ([(Name, AgentState s f)], f, [Derivation a])
     ([(Name, AgentState s f)], f, [Derivation a])
forall a b. b -> Either a b
Right ([(Name, AgentState s f)], f, [Derivation a])
bundle'

-- | One roster pass: schedule every agent that has pending work.
--
-- The roster carries explicit subscriptions; posts are routed to every agent
-- whose subscriptions intersect the post's 'to' list.
meetingPass ::
  forall a s f.
  (Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
  [RosterEntry s a] ->
  ([(Name, AgentState s f)], Log f, [Derivation a]) ->
  ([(Name, AgentState s f)], Log f, [Derivation a])
meetingPass :: forall a s f.
(Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
[RosterEntry s a]
-> ([(Name, AgentState s f)], f, [Derivation a])
-> ([(Name, AgentState s f)], f, [Derivation a])
meetingPass [RosterEntry s a]
roster ([(Name, AgentState s f)]
states, f
lg, [Derivation a]
derivs) = (([(Name, AgentState s f)], f, [Derivation a])
 -> RosterEntry s a
 -> ([(Name, AgentState s f)], f, [Derivation a]))
-> ([(Name, AgentState s f)], f, [Derivation a])
-> [RosterEntry s a]
-> ([(Name, AgentState s f)], f, [Derivation a])
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ([(Name, AgentState s f)], f, [Derivation a])
-> RosterEntry s a -> ([(Name, AgentState s f)], f, [Derivation a])
step ([(Name, AgentState s f)]
states, f
lg, [Derivation a]
derivs) [RosterEntry s a]
roster
  where
    subMap :: Map Name [Name]
subMap = [(Name, [Name])] -> Map Name [Name]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Name
n, [Name]
subs) | (Name
n, [Name]
subs, Agent (->) s (Post a) [Post a]
_) <- [RosterEntry s a]
roster]

    step :: ([(Name, AgentState s f)], f, [Derivation a])
-> RosterEntry s a -> ([(Name, AgentState s f)], f, [Derivation a])
step ([(Name, AgentState s f)]
st, f
l, [Derivation a]
ds) (Name
name, [Name]
_subs, Agent (->) s (Post a) [Post a]
agent) =
      case Name -> [(Name, AgentState s f)] -> Maybe (AgentState s f)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
name [(Name, AgentState s f)]
st of
        Maybe (AgentState s f)
Nothing -> ([(Name, AgentState s f)]
st, f
l, [Derivation a]
ds)
        Just AgentState s f
sti
          | forall a s f. Uncons f (Post a) => AgentState s f -> Bool
hasPending @a AgentState s f
sti ->
              let (AgentState s f
st', f
l', Maybe (Derivation a)
md) = Name
-> Agent (->) s (Post a) [Post a]
-> AgentState s f
-> f
-> (AgentState s f, f, Maybe (Derivation a))
forall a s f.
(Cons f (Post a), Uncons f (Post a)) =>
Name
-> Agent (->) s (Post a) [Post a]
-> AgentState s f
-> f
-> (AgentState s f, f, Maybe (Derivation a))
turnAs Name
name Agent (->) s (Post a) [Post a]
agent AgentState s f
sti f
l
                  newCount :: Int
newCount = forall f a. Uncons f a => f -> Int
streamLength @f @(Post a) f
l' Int -> Int -> Int
forall a. Num a => a -> a -> a
- forall f a. Uncons f a => f -> Int
streamLength @f @(Post a) f
l
                  newPosts :: [Post a]
newPosts = forall f a. Uncons f a => Int -> f -> [a]
takeStream @f @(Post a) Int
newCount f
l'
                  st'' :: [(Name, AgentState s f)]
st'' = ([(Name, AgentState s f)] -> Post a -> [(Name, AgentState s f)])
-> [(Name, AgentState s f)] -> [Post a] -> [(Name, AgentState s f)]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' [(Name, AgentState s f)] -> Post a -> [(Name, AgentState s f)]
routePost (Name
-> AgentState s f
-> [(Name, AgentState s f)]
-> [(Name, AgentState s f)]
forall {a} {b}. Eq a => a -> b -> [(a, b)] -> [(a, b)]
updateState Name
name AgentState s f
st' [(Name, AgentState s f)]
st) [Post a]
newPosts
                  ds' :: [Derivation a]
ds' = [Derivation a]
-> (Derivation a -> [Derivation a])
-> Maybe (Derivation a)
-> [Derivation a]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Derivation a]
ds (\Derivation a
d -> [Derivation a]
ds [Derivation a] -> [Derivation a] -> [Derivation a]
forall a. [a] -> [a] -> [a]
++ [Derivation a
d]) Maybe (Derivation a)
md
               in ([(Name, AgentState s f)]
st'', f
l', [Derivation a]
ds')
          | Bool
otherwise -> ([(Name, AgentState s f)]
st, f
l, [Derivation a]
ds)

    updateState :: a -> b -> [(a, b)] -> [(a, b)]
updateState a
name b
st' = ((a, b) -> (a, b)) -> [(a, b)] -> [(a, b)]
forall a b. (a -> b) -> [a] -> [b]
map (\(a
n, b
s) -> if a
n a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
name then (a
n, b
st') else (a
n, b
s))

    routePost :: [(Name, AgentState s f)] -> Post a -> [(Name, AgentState s f)]
routePost [(Name, AgentState s f)]
states' Post a
p =
      ((Name, AgentState s f) -> (Name, AgentState s f))
-> [(Name, AgentState s f)] -> [(Name, AgentState s f)]
forall a b. (a -> b) -> [a] -> [b]
map
        ( \(Name
n, AgentState s f
st) ->
            if Post a -> [Name] -> Bool
forall a. Post a -> [Name] -> Bool
deliversTo Post a
p ([Name] -> Name -> Map Name [Name] -> [Name]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [Name
n] Name
n Map Name [Name]
subMap)
              then (Name
n, AgentState s f
st {asInbox = appendInbox p (asInbox st)})
              else (Name
n, AgentState s f
st)
        )
        [(Name, AgentState s f)]
states'

-- | Transitive unfolding of a meeting.
--
-- Each element is one state of the round-robin schedule.  Divergence becomes
-- observable (the list is infinite) and 'loop' is simply the last quiescent
-- element.  The third component collects one 'Derivation' for every post that
-- was processed by 'turn' across the schedule.
--
-- Backwards-compatible wrapper; for explicit subscriptions use 'loopsSubs'.
loops ::
  forall a s f.
  (Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
  [(Name, Agent (->) s (Post a) [Post a])] ->
  [(Name, AgentState s f)] ->
  Log f ->
  [([(Name, AgentState s f)], Log f, [Derivation a])]
loops :: forall a s f.
(Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
[(Name, Agent (->) s (Post a) [Post a])]
-> [(Name, AgentState s f)]
-> f
-> [([(Name, AgentState s f)], f, [Derivation a])]
loops [(Name, Agent (->) s (Post a) [Post a])]
roster = [RosterEntry s a]
-> [(Name, AgentState s f)]
-> f
-> [([(Name, AgentState s f)], f, [Derivation a])]
forall a s f.
(Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
[RosterEntry s a]
-> [(Name, AgentState s f)]
-> f
-> [([(Name, AgentState s f)], f, [Derivation a])]
loopsSubs [(Name
n, [Name
n], Agent (->) s (Post a) [Post a]
a) | (Name
n, Agent (->) s (Post a) [Post a]
a) <- [(Name, Agent (->) s (Post a) [Post a])]
roster]

-- | Multi-seat-card variant of 'loops'.
loopsSubs ::
  forall a s f.
  (Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
  [RosterEntry s a] ->
  [(Name, AgentState s f)] ->
  Log f ->
  [([(Name, AgentState s f)], Log f, [Derivation a])]
loopsSubs :: forall a s f.
(Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
[RosterEntry s a]
-> [(Name, AgentState s f)]
-> f
-> [([(Name, AgentState s f)], f, [Derivation a])]
loopsSubs [RosterEntry s a]
roster [(Name, AgentState s f)]
states0 f
log0 = ([(Name, AgentState s f)]
states0, f
log0, []) ([(Name, AgentState s f)], f, [Derivation a])
-> [([(Name, AgentState s f)], f, [Derivation a])]
-> [([(Name, AgentState s f)], f, [Derivation a])]
forall a. a -> [a] -> [a]
: [(Name, AgentState s f)]
-> f
-> [Derivation a]
-> [([(Name, AgentState s f)], f, [Derivation a])]
go [(Name, AgentState s f)]
states0 f
log0 []
  where
    subMap :: Map Name [Name]
subMap = [(Name, [Name])] -> Map Name [Name]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Name
n, [Name]
subs) | (Name
n, [Name]
subs, Agent (->) s (Post a) [Post a]
_) <- [RosterEntry s a]
roster]

    go :: [(Name, AgentState s f)] -> Log f -> [Derivation a] -> [([(Name, AgentState s f)], Log f, [Derivation a])]
    go :: [(Name, AgentState s f)]
-> f
-> [Derivation a]
-> [([(Name, AgentState s f)], f, [Derivation a])]
go [(Name, AgentState s f)]
states f
lg [Derivation a]
derivs
      | Bool -> Bool
not (((Name, AgentState s f) -> Bool)
-> [(Name, AgentState s f)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a s f. Uncons f (Post a) => AgentState s f -> Bool
hasPending @a (AgentState s f -> Bool)
-> ((Name, AgentState s f) -> AgentState s f)
-> (Name, AgentState s f)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, AgentState s f) -> AgentState s f
forall a b. (a, b) -> b
snd) [(Name, AgentState s f)]
states) = []
      | Bool
otherwise =
          let ([(Name, AgentState s f)]
states', f
lg', [Derivation a]
derivs') = (([(Name, AgentState s f)], f, [Derivation a])
 -> RosterEntry s a
 -> ([(Name, AgentState s f)], f, [Derivation a]))
-> ([(Name, AgentState s f)], f, [Derivation a])
-> [RosterEntry s a]
-> ([(Name, AgentState s f)], f, [Derivation a])
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ([(Name, AgentState s f)], f, [Derivation a])
-> RosterEntry s a -> ([(Name, AgentState s f)], f, [Derivation a])
step ([(Name, AgentState s f)]
states, f
lg, [Derivation a]
derivs) [RosterEntry s a]
roster
           in ([(Name, AgentState s f)]
states', f
lg', [Derivation a]
derivs') ([(Name, AgentState s f)], f, [Derivation a])
-> [([(Name, AgentState s f)], f, [Derivation a])]
-> [([(Name, AgentState s f)], f, [Derivation a])]
forall a. a -> [a] -> [a]
: [(Name, AgentState s f)]
-> f
-> [Derivation a]
-> [([(Name, AgentState s f)], f, [Derivation a])]
go [(Name, AgentState s f)]
states' f
lg' [Derivation a]
derivs'

    step :: ([(Name, AgentState s f)], Log f, [Derivation a]) -> RosterEntry s a -> ([(Name, AgentState s f)], Log f, [Derivation a])
    step :: ([(Name, AgentState s f)], f, [Derivation a])
-> RosterEntry s a -> ([(Name, AgentState s f)], f, [Derivation a])
step ([(Name, AgentState s f)]
states, f
lg, [Derivation a]
derivs) (Name
name, [Name]
_subs, Agent (->) s (Post a) [Post a]
agent) =
      case Name -> [(Name, AgentState s f)] -> Maybe (AgentState s f)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
name [(Name, AgentState s f)]
states of
        Maybe (AgentState s f)
Nothing -> ([(Name, AgentState s f)]
states, f
lg, [Derivation a]
derivs)
        Just AgentState s f
st
          | forall a s f. Uncons f (Post a) => AgentState s f -> Bool
hasPending @a AgentState s f
st ->
              let (AgentState s f
st', f
lg', Maybe (Derivation a)
md) = Name
-> Agent (->) s (Post a) [Post a]
-> AgentState s f
-> f
-> (AgentState s f, f, Maybe (Derivation a))
forall a s f.
(Cons f (Post a), Uncons f (Post a)) =>
Name
-> Agent (->) s (Post a) [Post a]
-> AgentState s f
-> f
-> (AgentState s f, f, Maybe (Derivation a))
turnAs Name
name Agent (->) s (Post a) [Post a]
agent AgentState s f
st f
lg
                  newCount :: Int
newCount = forall f a. Uncons f a => f -> Int
streamLength @f @(Post a) f
lg' Int -> Int -> Int
forall a. Num a => a -> a -> a
- forall f a. Uncons f a => f -> Int
streamLength @f @(Post a) f
lg
                  newPosts :: [Post a]
newPosts = forall f a. Uncons f a => Int -> f -> [a]
takeStream @f @(Post a) Int
newCount f
lg'
                  states'' :: [(Name, AgentState s f)]
states'' = ([(Name, AgentState s f)] -> Post a -> [(Name, AgentState s f)])
-> [(Name, AgentState s f)] -> [Post a] -> [(Name, AgentState s f)]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' [(Name, AgentState s f)] -> Post a -> [(Name, AgentState s f)]
routePost (Name
-> AgentState s f
-> [(Name, AgentState s f)]
-> [(Name, AgentState s f)]
updateState Name
name AgentState s f
st' [(Name, AgentState s f)]
states) [Post a]
newPosts
                  derivs' :: [Derivation a]
derivs' = [Derivation a]
-> (Derivation a -> [Derivation a])
-> Maybe (Derivation a)
-> [Derivation a]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Derivation a]
derivs (\Derivation a
d -> [Derivation a]
derivs [Derivation a] -> [Derivation a] -> [Derivation a]
forall a. [a] -> [a] -> [a]
++ [Derivation a
d]) Maybe (Derivation a)
md
               in ([(Name, AgentState s f)]
states'', f
lg', [Derivation a]
derivs')
          | Bool
otherwise -> ([(Name, AgentState s f)]
states, f
lg, [Derivation a]
derivs)

    updateState :: Name -> AgentState s f -> [(Name, AgentState s f)] -> [(Name, AgentState s f)]
    updateState :: Name
-> AgentState s f
-> [(Name, AgentState s f)]
-> [(Name, AgentState s f)]
updateState Name
name AgentState s f
st' = ((Name, AgentState s f) -> (Name, AgentState s f))
-> [(Name, AgentState s f)] -> [(Name, AgentState s f)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, AgentState s f
s) -> if Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
name then (Name
n, AgentState s f
st') else (Name
n, AgentState s f
s))

    routePost :: [(Name, AgentState s f)] -> Post a -> [(Name, AgentState s f)]
    routePost :: [(Name, AgentState s f)] -> Post a -> [(Name, AgentState s f)]
routePost [(Name, AgentState s f)]
states Post a
p =
      ((Name, AgentState s f) -> (Name, AgentState s f))
-> [(Name, AgentState s f)] -> [(Name, AgentState s f)]
forall a b. (a -> b) -> [a] -> [b]
map
        ( \(Name
n, AgentState s f
st) ->
            if Post a -> [Name] -> Bool
forall a. Post a -> [Name] -> Bool
deliversTo Post a
p ([Name] -> Name -> Map Name [Name] -> [Name]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [Name
n] Name
n Map Name [Name]
subMap)
              then (Name
n, AgentState s f
st {asInbox = appendInbox p (asInbox st)})
              else (Name
n, AgentState s f
st)
        )
        [(Name, AgentState s f)]
states

-- | Resumable 'loop' with a heterogeneous roster: each agent supplies its own
-- initial carrier, while inboxes are still seeded from the shared log.
--
-- Backwards-compatible wrapper; for explicit subscriptions use 'loopHeteroSubs'.
loopHetero ::
  forall a s f.
  (Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
  [(Name, s, Agent (->) s (Post a) [Post a])] ->
  Log f ->
  ([(Name, AgentState s f)], Log f, [Derivation a])
loopHetero :: forall a s f.
(Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
[(Name, s, Agent (->) s (Post a) [Post a])]
-> f -> ([(Name, AgentState s f)], f, [Derivation a])
loopHetero [(Name, s, Agent (->) s (Post a) [Post a])]
roster = [(Name, s, [Name], Agent (->) s (Post a) [Post a])]
-> f -> ([(Name, AgentState s f)], f, [Derivation a])
forall a s f.
(Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
[(Name, s, [Name], Agent (->) s (Post a) [Post a])]
-> f -> ([(Name, AgentState s f)], f, [Derivation a])
loopHeteroSubs [(Name
n, s
s, [Name
n], Agent (->) s (Post a) [Post a]
a) | (Name
n, s
s, Agent (->) s (Post a) [Post a]
a) <- [(Name, s, Agent (->) s (Post a) [Post a])]
roster]

-- | Multi-seat-card variant of 'loopHetero'.
loopHeteroSubs ::
  forall a s f.
  (Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
  [(Name, s, [Name], Agent (->) s (Post a) [Post a])] ->
  Log f ->
  ([(Name, AgentState s f)], Log f, [Derivation a])
loopHeteroSubs :: forall a s f.
(Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
[(Name, s, [Name], Agent (->) s (Post a) [Post a])]
-> f -> ([(Name, AgentState s f)], f, [Derivation a])
loopHeteroSubs [(Name, s, [Name], Agent (->) s (Post a) [Post a])]
roster f
log0 =
  [RosterEntry s a]
-> [(Name, AgentState s f)]
-> f
-> ([(Name, AgentState s f)], f, [Derivation a])
forall a s f.
(Snoc f (Post a), Cons f (Post a), Uncons f (Post a)) =>
[RosterEntry s a]
-> [(Name, AgentState s f)]
-> f
-> ([(Name, AgentState s f)], f, [Derivation a])
loopWithSubs
    [(Name
n, [Name]
subs, Agent (->) s (Post a) [Post a]
a) | (Name
n, s
_, [Name]
subs, Agent (->) s (Post a) [Post a]
a) <- [(Name, s, [Name], Agent (->) s (Post a) [Post a])]
roster]
    [(Name
n, s -> Inbox f -> AgentState s f
forall s f. s -> Inbox f -> AgentState s f
AgentState s
s (forall a f.
(Snoc f (Post a), Uncons f (Post a)) =>
[Name] -> f -> Inbox f
seedInbox @a [Name]
subs f
log0)) | (Name
n, s
s, [Name]
subs, Agent (->) s (Post a) [Post a]
_) <- [(Name, s, [Name], Agent (->) s (Post a) [Post a])]
roster]
    f
log0

-- | Run a monomial system for one step.
--
-- Consume @i@, then extract the output from the successor state (Process /
-- 'iterateSystem' timing).
run1 :: Agent (->) s i o -> s -> i -> (o, s)
run1 :: forall s i o. Agent (->) s i o -> s -> i -> (o, s)
run1 Agent (->) s i o
sys s
s i
i =
  let s' :: s
s' = (o, i -> s) -> i -> s
forall a b. (a, b) -> b
snd (Agent (->) s i o -> s -> (o, i -> s)
forall s i o. System (->) s (Mono i o) -> s -> (o, i -> s)
System.runSystemMono Agent (->) s i o
sys s
s) i
i
      (o
o, i -> s
_) = Agent (->) s i o -> s -> (o, i -> s)
forall s i o. System (->) s (Mono i o) -> s -> (o, i -> s)
System.runSystemMono Agent (->) s i o
sys s
s'
   in (o
o, s
s')

-- | Lift a pure agent into the 'K' arrow of any functor.
--
-- This is the change of base from @(->)@ to @K m@ on the agent itself:
-- the same Moore coalgebra, but each step now lives in @m@.
agentM :: (Applicative m) => Agent (->) s a b -> Agent (K m) s a b
agentM :: forall (m :: * -> *) s a b.
Applicative m =>
Agent (->) s a b -> Agent (K m) s a b
agentM Agent (->) s a b
sys = K m (s, Dir (Mono a b)) (s, Pos (Mono a b))
-> System (K m) s (Mono a b)
forall (arr :: * -> * -> *) s (p :: Poly).
arr (s, Dir p) (s, Pos p) -> System arr s p
system (((s, Either Void a) -> m (s, (b, ())))
-> K m (s, Either Void a) (s, (b, ()))
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((s, (b, ())) -> m (s, (b, ()))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((s, (b, ())) -> m (s, (b, ())))
-> ((s, Either Void a) -> (s, (b, ())))
-> (s, Either Void a)
-> m (s, (b, ()))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Agent (->) s 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 Agent (->) s a b
sys))

-- | Run one step of a monadic agent.
runAgentM :: (Monad m) => Agent (K m) s a b -> s -> a -> m (b, s)
runAgentM :: forall (m :: * -> *) s a b.
Monad m =>
Agent (K m) s a b -> s -> a -> m (b, s)
runAgentM Agent (K m) s a b
sys s
s a
a =
  K m (s, Either Void a) (s, (b, ()))
-> (s, Either Void a) -> m (s, (b, ()))
forall {k} (m :: k -> *) a (b :: k). K m a b -> a -> m b
runK (Agent (K m) s a b -> K m (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 Agent (K m) s a b
sys) (s
s, a -> Dir (Mono a (ZonkAny 1))
forall i o. i -> Dir (Mono i o)
monoIn a
a) m (s, (b, ())) -> ((s, (b, ())) -> m (b, s)) -> m (b, s)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(s
s', (b
b, ())) -> (b, s) -> m (b, s)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (b
b, s
s')

-- | STM agent: state is handled transparently inside an STM transaction.
type AgentS s a = Agent (K STM) s a [a]

-- | IO agent: the STM boundary has been crossed; state is no longer
-- transparently handled.
type AgentX s a = Agent (K IO) s a [a]

-- | Cross from the transparent STM world into the IO boundary.
agentX :: AgentS s a -> AgentX s a
agentX :: forall s a. AgentS s a -> AgentX s a
agentX AgentS s a
sys = K IO (s, Dir (Mono a [a])) (s, Pos (Mono a [a]))
-> System (K IO) s (Mono a [a])
forall (arr :: * -> * -> *) s (p :: Poly).
arr (s, Dir p) (s, Pos p) -> System arr s p
system (((s, Either Void a) -> IO (s, ([a], ())))
-> K IO (s, Either Void a) (s, ([a], ()))
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K (\(s
s, Either Void a
d) -> STM (s, ([a], ())) -> IO (s, ([a], ()))
forall a. STM a -> IO a
atomically (K STM (s, Either Void a) (s, ([a], ()))
-> (s, Either Void a) -> STM (s, ([a], ()))
forall {k} (m :: k -> *) a (b :: k). K m a b -> a -> m b
runK (AgentS s a -> K STM (s, Dir (Mono a [a])) (s, Pos (Mono a [a]))
forall (arr :: * -> * -> *) s (p :: Poly).
System arr s p -> arr (s, Dir p) (s, Pos p)
runSystem AgentS s a
sys) (s
s, Either Void a
d))))

-- | Seat-level product / await in STM.
awaitS :: AgentS s1 a -> AgentS s2 a -> AgentS (s1, s2) a
awaitS :: forall s1 a s2. AgentS s1 a -> AgentS s2 a -> AgentS (s1, s2) a
awaitS AgentS s1 a
sys1 AgentS s2 a
sys2 =
  K STM ((s1, s2), Dir (Mono a [a])) ((s1, s2), Pos (Mono a [a]))
-> System (K STM) (s1, s2) (Mono a [a])
forall (arr :: * -> * -> *) s (p :: Poly).
arr (s, Dir p) (s, Pos p) -> System arr s p
system (K STM ((s1, s2), Dir (Mono a [a])) ((s1, s2), Pos (Mono a [a]))
 -> System (K STM) (s1, s2) (Mono a [a]))
-> K STM ((s1, s2), Dir (Mono a [a])) ((s1, s2), Pos (Mono a [a]))
-> System (K STM) (s1, s2) (Mono a [a])
forall a b. (a -> b) -> a -> b
$ (((s1, s2), Dir (Mono a [a])) -> STM ((s1, s2), Pos (Mono a [a])))
-> K STM ((s1, s2), Dir (Mono a [a])) ((s1, s2), Pos (Mono a [a]))
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((((s1, s2), Dir (Mono a [a])) -> STM ((s1, s2), Pos (Mono a [a])))
 -> K STM ((s1, s2), Dir (Mono a [a])) ((s1, s2), Pos (Mono a [a])))
-> (((s1, s2), Dir (Mono a [a]))
    -> STM ((s1, s2), Pos (Mono a [a])))
-> K STM ((s1, s2), Dir (Mono a [a])) ((s1, s2), Pos (Mono a [a]))
forall a b. (a -> b) -> a -> b
$ \((s1
s1, s2
s2), Dir (Mono a [a])
d) -> do
    (s1', (o1, ())) <- K STM (s1, Either Void a) (s1, ([a], ()))
-> (s1, Either Void a) -> STM (s1, ([a], ()))
forall {k} (m :: k -> *) a (b :: k). K m a b -> a -> m b
runK (AgentS s1 a -> K STM (s1, Dir (Mono a [a])) (s1, Pos (Mono a [a]))
forall (arr :: * -> * -> *) s (p :: Poly).
System arr s p -> arr (s, Dir p) (s, Pos p)
runSystem AgentS s1 a
sys1) (s1
s1, Either Void a
Dir (Mono a [a])
d)
    (s2', (o2, ())) <- runK (runSystem sys2) (s2, d)
    pure ((s1', s2'), (o1 <> o2, ()))

-- | Seat-level coproduct / race in STM.
raceS :: AgentS s1 a -> AgentS s2 a -> AgentS (s1, s2) a
raceS :: forall s1 a s2. AgentS s1 a -> AgentS s2 a -> AgentS (s1, s2) a
raceS AgentS s1 a
sys1 AgentS s2 a
sys2 =
  K STM ((s1, s2), Dir (Mono a [a])) ((s1, s2), Pos (Mono a [a]))
-> System (K STM) (s1, s2) (Mono a [a])
forall (arr :: * -> * -> *) s (p :: Poly).
arr (s, Dir p) (s, Pos p) -> System arr s p
system (K STM ((s1, s2), Dir (Mono a [a])) ((s1, s2), Pos (Mono a [a]))
 -> System (K STM) (s1, s2) (Mono a [a]))
-> K STM ((s1, s2), Dir (Mono a [a])) ((s1, s2), Pos (Mono a [a]))
-> System (K STM) (s1, s2) (Mono a [a])
forall a b. (a -> b) -> a -> b
$ (((s1, s2), Dir (Mono a [a])) -> STM ((s1, s2), Pos (Mono a [a])))
-> K STM ((s1, s2), Dir (Mono a [a])) ((s1, s2), Pos (Mono a [a]))
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((((s1, s2), Dir (Mono a [a])) -> STM ((s1, s2), Pos (Mono a [a])))
 -> K STM ((s1, s2), Dir (Mono a [a])) ((s1, s2), Pos (Mono a [a])))
-> (((s1, s2), Dir (Mono a [a]))
    -> STM ((s1, s2), Pos (Mono a [a])))
-> K STM ((s1, s2), Dir (Mono a [a])) ((s1, s2), Pos (Mono a [a]))
forall a b. (a -> b) -> a -> b
$ \((s1
s1, s2
s2), Dir (Mono a [a])
d) -> do
    (s1', (o1, ())) <- K STM (s1, Either Void a) (s1, ([a], ()))
-> (s1, Either Void a) -> STM (s1, ([a], ()))
forall {k} (m :: k -> *) a (b :: k). K m a b -> a -> m b
runK (AgentS s1 a -> K STM (s1, Dir (Mono a [a])) (s1, Pos (Mono a [a]))
forall (arr :: * -> * -> *) s (p :: Poly).
System arr s p -> arr (s, Dir p) (s, Pos p)
runSystem AgentS s1 a
sys1) (s1
s1, Either Void a
Dir (Mono a [a])
d)
    (s2', (o2, ())) <- runK (runSystem sys2) (s2, d)
    let o = if [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
o1 then [a]
o2 else [a]
o1
    pure ((s1', s2'), (o, ()))

-- | Temporal race under IO: run both branches concurrently, return the first
-- branch to emit a non-empty output, and cancel the loser. If the first branch
-- to finish emits nothing, wait for the other branch. If both emit nothing, the
-- right branch's (empty) result is returned.
--
-- This is the honest K-IO refinement of 'raceS': the winner is whichever
-- step produces a mark first, not the left-biased deterministic rule.
raceIO :: AgentX s1 a -> AgentX s2 a -> AgentX (s1, s2) a
raceIO :: forall s1 a s2. AgentX s1 a -> AgentX s2 a -> AgentX (s1, s2) a
raceIO AgentX s1 a
sys1 AgentX s2 a
sys2 =
  K IO ((s1, s2), Dir (Mono a [a])) ((s1, s2), Pos (Mono a [a]))
-> System (K IO) (s1, s2) (Mono a [a])
forall (arr :: * -> * -> *) s (p :: Poly).
arr (s, Dir p) (s, Pos p) -> System arr s p
system (K IO ((s1, s2), Dir (Mono a [a])) ((s1, s2), Pos (Mono a [a]))
 -> System (K IO) (s1, s2) (Mono a [a]))
-> K IO ((s1, s2), Dir (Mono a [a])) ((s1, s2), Pos (Mono a [a]))
-> System (K IO) (s1, s2) (Mono a [a])
forall a b. (a -> b) -> a -> b
$ (((s1, s2), Dir (Mono a [a])) -> IO ((s1, s2), Pos (Mono a [a])))
-> K IO ((s1, s2), Dir (Mono a [a])) ((s1, s2), Pos (Mono a [a]))
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((((s1, s2), Dir (Mono a [a])) -> IO ((s1, s2), Pos (Mono a [a])))
 -> K IO ((s1, s2), Dir (Mono a [a])) ((s1, s2), Pos (Mono a [a])))
-> (((s1, s2), Dir (Mono a [a]))
    -> IO ((s1, s2), Pos (Mono a [a])))
-> K IO ((s1, s2), Dir (Mono a [a])) ((s1, s2), Pos (Mono a [a]))
forall a b. (a -> b) -> a -> b
$ \((s1
s1, s2
s2), Dir (Mono a [a])
d) ->
    IO (s1, ([a], ()))
-> IO (s2, ([a], ())) -> IO (Either (s1, [a]) (s2, [a]))
forall {t :: * -> *} {t :: * -> *} {a} {a} {a} {a}.
(Foldable t, Foldable t) =>
IO (a, (t a, ()))
-> IO (a, (t a, ())) -> IO (Either (a, t a) (a, t a))
raceFirst (K IO (s1, Either Void a) (s1, ([a], ()))
-> (s1, Either Void a) -> IO (s1, ([a], ()))
forall {k} (m :: k -> *) a (b :: k). K m a b -> a -> m b
runK (AgentX s1 a -> K IO (s1, Dir (Mono a [a])) (s1, Pos (Mono a [a]))
forall (arr :: * -> * -> *) s (p :: Poly).
System arr s p -> arr (s, Dir p) (s, Pos p)
runSystem AgentX s1 a
sys1) (s1
s1, Either Void a
Dir (Mono a [a])
d)) (K IO (s2, Either Void a) (s2, ([a], ()))
-> (s2, Either Void a) -> IO (s2, ([a], ()))
forall {k} (m :: k -> *) a (b :: k). K m a b -> a -> m b
runK (AgentX s2 a -> K IO (s2, Dir (Mono a [a])) (s2, Pos (Mono a [a]))
forall (arr :: * -> * -> *) s (p :: Poly).
System arr s p -> arr (s, Dir p) (s, Pos p)
runSystem AgentX s2 a
sys2) (s2
s2, Either Void a
Dir (Mono a [a])
d)) IO (Either (s1, [a]) (s2, [a]))
-> (Either (s1, [a]) (s2, [a]) -> IO ((s1, s2), ([a], ())))
-> IO ((s1, s2), ([a], ()))
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Left (s1
s1', [a]
outs) -> ((s1, s2), ([a], ())) -> IO ((s1, s2), ([a], ()))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((s1
s1', s2
s2), ([a]
outs, ()))
      Right (s2
s2', [a]
outs) -> ((s1, s2), ([a], ())) -> IO ((s1, s2), ([a], ()))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((s1
s1, s2
s2'), ([a]
outs, ()))
  where
    raceFirst :: IO (a, (t a, ()))
-> IO (a, (t a, ())) -> IO (Either (a, t a) (a, t a))
raceFirst IO (a, (t a, ()))
act1 IO (a, (t a, ()))
act2 = do
      a1 <- IO (a, (t a, ())) -> IO (Async (a, (t a, ())))
forall a. IO a -> IO (Async a)
async IO (a, (t a, ()))
act1
      a2 <- async act2
      let finishLeft a
s1' t a
outs = Async (a, (t a, ())) -> IO ()
forall a. Async a -> IO ()
cancel Async (a, (t a, ()))
a2 IO ()
-> IO (Either (a, t a) (a, t a)) -> IO (Either (a, t a) (a, t a))
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Either (a, t a) (a, t a) -> IO (Either (a, t a) (a, t a))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((a, t a) -> Either (a, t a) (a, t a)
forall a b. a -> Either a b
Left (a
s1', t a
outs))
          finishRight a
s2' t a
outs = Async (a, (t a, ())) -> IO ()
forall a. Async a -> IO ()
cancel Async (a, (t a, ()))
a1 IO ()
-> IO (Either (a, t a) (a, t a)) -> IO (Either (a, t a) (a, t a))
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Either (a, t a) (a, t a) -> IO (Either (a, t a) (a, t a))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((a, t a) -> Either (a, t a) (a, t a)
forall a b. b -> Either a b
Right (a
s2', t a
outs))
      race (wait a1) (wait a2) >>= \case
        Left (a
s1', (t a
outs1, ()))
          | Bool -> Bool
not (t a -> Bool
forall a. t a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null t a
outs1) -> a -> t a -> IO (Either (a, t a) (a, t a))
finishLeft a
s1' t a
outs1
          | Bool
otherwise -> do
              (s2', (outs2, ())) <- Async (a, (t a, ())) -> IO (a, (t a, ()))
forall a. Async a -> IO a
wait Async (a, (t a, ()))
a2
              finishRight s2' outs2
        Right (a
s2', (t a
outs2, ()))
          | Bool -> Bool
not (t a -> Bool
forall a. t a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null t a
outs2) -> a -> t a -> IO (Either (a, t a) (a, t a))
finishRight a
s2' t a
outs2
          | Bool
otherwise -> do
              (s1', (outs1, ())) <- Async (a, (t a, ())) -> IO (a, (t a, ()))
forall a. Async a -> IO a
wait Async (a, (t a, ()))
a1
              finishLeft s1' outs1

-- | Run one step of an STM agent.
stepS :: AgentS s a -> s -> a -> STM (s, [a])
stepS :: forall s a. AgentS s a -> s -> a -> STM (s, [a])
stepS AgentS s a
sys s
s a
i = do
  (s', (outs, ())) <- K STM (s, Either Void a) (s, ([a], ()))
-> (s, Either Void a) -> STM (s, ([a], ()))
forall {k} (m :: k -> *) a (b :: k). K m a b -> a -> m b
runK (AgentS s a -> K STM (s, Dir (Mono a [a])) (s, Pos (Mono a [a]))
forall (arr :: * -> * -> *) s (p :: Poly).
System arr s p -> arr (s, Dir p) (s, Pos p)
runSystem AgentS s a
sys) (s
s, a -> Dir (Mono a (ZonkAny 0))
forall i o. i -> Dir (Mono i o)
monoIn a
i)
  pure (s', outs)

-- | Fold an STM agent over a bundle of inputs within one transaction.
--
-- This is the bundle-at-a-time step: one frame consumes a whole @[a]@ and
-- produces the concatenated replies.  Factor of 'runAgentS' that stays in
-- 'STM' so it can sit inside a larger transaction (e.g. a self-loop frame).
stepsS :: AgentS s a -> s -> [a] -> STM (s, [a])
stepsS :: forall s a. AgentS s a -> s -> [a] -> STM (s, [a])
stepsS AgentS s a
sys = s -> [a] -> STM (s, [a])
go
  where
    go :: s -> [a] -> STM (s, [a])
go s
s [] = (s, [a]) -> STM (s, [a])
forall a. a -> STM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (s
s, [])
    go s
s (a
i : [a]
is) = do
      (s', outs) <- AgentS s a -> s -> a -> STM (s, [a])
forall s a. AgentS s a -> s -> a -> STM (s, [a])
stepS AgentS s a
sys s
s a
i
      (sFinal, rest) <- go s' is
      pure (sFinal, outs ++ rest)

-- | Run an STM agent over a list of inputs, crossing into IO at the boundary.
runAgentS :: AgentS s a -> s -> [a] -> IO ([a], s)
runAgentS :: forall s a. AgentS s a -> s -> [a] -> IO ([a], s)
runAgentS AgentS s a
sys s
s0 [a]
ins = (\(s
s, [a]
os) -> ([a]
os, s
s)) ((s, [a]) -> ([a], s)) -> IO (s, [a]) -> IO ([a], s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> STM (s, [a]) -> IO (s, [a])
forall a. STM a -> IO a
atomically (AgentS s a -> s -> [a] -> STM (s, [a])
forall s a. AgentS s a -> s -> [a] -> STM (s, [a])
stepsS AgentS s a
sys s
s0 [a]
ins)

-- | Unit poles for lifting single-token reads/writes out of a 'Poles' value.
unitEndsSTM :: Poles (K STM) () ()
unitEndsSTM :: Poles (K STM) () ()
unitEndsSTM = (() -> STM ()) -> STM () -> Poles (K STM) () ()
forall (m :: * -> *) a b.
Monad m =>
(a -> m ()) -> m b -> Poles (K m) a b
polesK (STM () -> () -> STM ()
forall a b. a -> b -> a
const (() -> STM ()
forall a. a -> STM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())) (() -> STM ()
forall a. a -> STM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())

-- | Read one token from an STM pole.
readEndSTM :: Poles (K STM) a a -> STM a
readEndSTM :: forall a. Poles (K STM) a a -> STM a
readEndSTM Poles (K STM) a a
ends = K STM () a -> () -> STM a
forall {k} (m :: k -> *) a (b :: k). K m a b -> a -> m b
runK (Out (K STM) a -> forall x. In (K STM) x -> K STM x a
forall {k1} {k2} (arr :: k1 -> k2 -> *) (a :: k2).
Out arr a -> forall (x :: k1). In arr x -> arr x a
emit (Poles (K STM) a a -> Out (K STM) a
forall {k1} {k2} (arr :: k1 -> k2 -> *) (a :: k1) (b :: k2).
Poles arr a b -> Out arr b
companion Poles (K STM) a a
ends) (Poles (K STM) () () -> In (K STM) ()
forall {k1} {k2} (arr :: k1 -> k2 -> *) (a :: k1) (b :: k2).
Poles arr a b -> In arr a
conjoint Poles (K STM) () ()
unitEndsSTM)) ()

-- | Write one token to an STM pole.
writeEndSTM :: Poles (K STM) a a -> a -> STM ()
writeEndSTM :: forall a. Poles (K STM) a a -> a -> STM ()
writeEndSTM Poles (K STM) a a
ends = K STM a () -> a -> STM ()
forall {k} (m :: k -> *) a (b :: k). K m a b -> a -> m b
runK (In (K STM) a -> forall x. Out (K STM) x -> K STM a x
forall {k1} {k2} (arr :: k1 -> k2 -> *) (a :: k1).
In arr a -> forall (x :: k2). Out arr x -> arr a x
commit (Poles (K STM) a a -> In (K STM) a
forall {k1} {k2} (arr :: k1 -> k2 -> *) (a :: k1) (b :: k2).
Poles arr a b -> In arr a
conjoint Poles (K STM) a a
ends) (Poles (K STM) () () -> Out (K STM) ()
forall {k1} {k2} (arr :: k1 -> k2 -> *) (a :: k1) (b :: k2).
Poles arr a b -> Out arr b
companion Poles (K STM) () ()
unitEndsSTM))

-- | Wire an STM agent between an inbox and an outbox, running until
-- quiescence.  Quiescence is detected via 'orElse': if the inbox is empty
-- (retry), the loop returns the current state.
agentLoopS :: AgentS s a -> s -> Poles (K STM) a a -> Poles (K STM) a a -> STM s
agentLoopS :: forall s a.
AgentS s a -> s -> Poles (K STM) a a -> Poles (K STM) a a -> STM s
agentLoopS AgentS s a
agent s
s0 Poles (K STM) a a
inbox Poles (K STM) a a
outbox = s -> STM s
go s
s0
  where
    go :: s -> STM s
go s
s =
      ( do
          a <- Poles (K STM) a a -> STM a
forall a. Poles (K STM) a a -> STM a
readEndSTM Poles (K STM) a a
inbox
          (s', outs) <- stepS agent s a
          traverse_ (writeEndSTM outbox) outs
          go s'
      )
        STM s -> STM s -> STM s
forall a. STM a -> STM a -> STM a
`orElse` s -> STM s
forall a. a -> STM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure s
s

-- | Self-loop: the agent reads from and writes to the same STM end.
selfLoopS :: AgentS s a -> s -> Poles (K STM) a a -> STM s
selfLoopS :: forall s a. AgentS s a -> s -> Poles (K STM) a a -> STM s
selfLoopS AgentS s a
agent s
s0 Poles (K STM) a a
ends = AgentS s a -> s -> Poles (K STM) a a -> Poles (K STM) a a -> STM s
forall s a.
AgentS s a -> s -> Poles (K STM) a a -> Poles (K STM) a a -> STM s
agentLoopS AgentS s a
agent s
s0 Poles (K STM) a a
ends Poles (K STM) a a
ends

-- | One frame of the bundle self-loop, expressed in the Either-trace halt
-- alphabet: 'Left' = continue, 'Right' = quiesce and return this state.
selfLoopFrame ::
  AgentS s a ->
  Poles (K STM) [a] [a] ->
  Poles (K STM) [a] [a] ->
  K STM (Either s s) (Either s s)
selfLoopFrame :: forall s a.
AgentS s a
-> Poles (K STM) [a] [a]
-> Poles (K STM) [a] [a]
-> K STM (Either s s) (Either s s)
selfLoopFrame AgentS s a
agent Poles (K STM) [a] [a]
inbox Poles (K STM) [a] [a]
outbox = (Either s s -> STM (Either s s)) -> K STM (Either s s) (Either s s)
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((Either s s -> STM (Either s s))
 -> K STM (Either s s) (Either s s))
-> (Either s s -> STM (Either s s))
-> K STM (Either s s) (Either s s)
forall a b. (a -> b) -> a -> b
$ \case
  Right s
s -> s -> STM (Either s s)
step s
s
  Left s
s -> s -> STM (Either s s)
step s
s
  where
    step :: s -> STM (Either s s)
step s
s = do
      mIns <- ([a] -> Maybe [a]
forall a. a -> Maybe a
Just ([a] -> Maybe [a]) -> STM [a] -> STM (Maybe [a])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Poles (K STM) [a] [a] -> STM [a]
forall a. Poles (K STM) a a -> STM a
readEndSTM Poles (K STM) [a] [a]
inbox) STM (Maybe [a]) -> STM (Maybe [a]) -> STM (Maybe [a])
forall a. STM a -> STM a -> STM a
`orElse` Maybe [a] -> STM (Maybe [a])
forall a. a -> STM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe [a]
forall a. Maybe a
Nothing
      case mIns of
        Maybe [a]
Nothing -> Either s s -> STM (Either s s)
forall a. a -> STM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (s -> Either s s
forall a b. b -> Either a b
Right s
s)
        Just [a]
ins -> do
          (s', outs) <- AgentS s a -> s -> [a] -> STM (s, [a])
forall s a. AgentS s a -> s -> [a] -> STM (s, [a])
stepsS AgentS s a
agent s
s [a]
ins
          if null outs
            then pure (Right s')
            else do
              writeEndSTM outbox outs
              pure (Left s')

-- | Wire an STM agent between an inbox and an outbox, running until
-- quiescence, expressed as a 'Trace Either' value.
agentLoopL ::
  AgentS s a ->
  Poles (K STM) [a] [a] ->
  Poles (K STM) [a] [a] ->
  Trace Either (K STM) s s
agentLoopL :: forall s a.
AgentS s a
-> Poles (K STM) [a] [a]
-> Poles (K STM) [a] [a]
-> Trace Either (K STM) s s
agentLoopL AgentS s a
agent Poles (K STM) [a] [a]
inbox Poles (K STM) [a] [a]
outbox = Trace Either (K STM) (Either s s) (Either s s)
-> Trace Either (K STM) s s
forall (t :: * -> * -> *) (arr :: * -> * -> *) s a b.
Trace t arr (t s a) (t s b) -> Trace t arr a b
yank (K STM (Either s s) (Either s s)
-> Trace Either (K STM) (Either s s) (Either s s)
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base (AgentS s a
-> Poles (K STM) [a] [a]
-> Poles (K STM) [a] [a]
-> K STM (Either s s) (Either s s)
forall s a.
AgentS s a
-> Poles (K STM) [a] [a]
-> Poles (K STM) [a] [a]
-> K STM (Either s s) (Either s s)
selfLoopFrame AgentS s a
agent Poles (K STM) [a] [a]
inbox Poles (K STM) [a] [a]
outbox))

-- | Self-loop as a 'Trace Either' citizen.
selfLoopL ::
  AgentS s a ->
  s ->
  Poles (K STM) [a] [a] ->
  STM s
selfLoopL :: forall s a. AgentS s a -> s -> Poles (K STM) [a] [a] -> STM s
selfLoopL AgentS s a
agent s
s0 Poles (K STM) [a] [a]
ends = K STM s s -> s -> STM s
forall {k} (m :: k -> *) a (b :: k). K m a b -> a -> m b
runK (Syntax (SigCompose :+: SigYank Either) (K STM) s s -> K STM s s
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval (AgentS s a
-> Poles (K STM) [a] [a]
-> Poles (K STM) [a] [a]
-> Syntax (SigCompose :+: SigYank Either) (K STM) s s
forall s a.
AgentS s a
-> Poles (K STM) [a] [a]
-> Poles (K STM) [a] [a]
-> Trace Either (K STM) s s
agentLoopL AgentS s a
agent Poles (K STM) [a] [a]
ends Poles (K STM) [a] [a]
ends)) s
s0

-- | Agent behaviour: a pure function from an input stream to an output stream.
--
-- Each input post is stepped through the agent; the per-step output lists are
-- concatenated into a single output stream.  This is the stream semantics of
-- the Moore coalgebra, independent of any effectful boundary.
type Beh a = [Post a] -> [Post a]

-- | Run an agent from an initial carrier to obtain its 'Beh'aviour.
beh :: Agent (->) s (Post a) [Post a] -> s -> Beh a
beh :: forall s a. Agent (->) s (Post a) [Post a] -> s -> Beh a
beh Agent (->) s (Post a) [Post a]
_sys s
_s0 [] = []
beh Agent (->) s (Post a) [Post a]
sys s
s0 (Post a
i : [Post a]
ins) =
  let ([Post a]
os, s
s') = Agent (->) s (Post a) [Post a] -> s -> Post a -> ([Post a], s)
forall s i o. Agent (->) s i o -> s -> i -> (o, s)
run1 Agent (->) s (Post a) [Post a]
sys s
s0 Post a
i
   in [Post a]
os [Post a] -> [Post a] -> [Post a]
forall a. [a] -> [a] -> [a]
++ Agent (->) s (Post a) [Post a] -> s -> [Post a] -> [Post a]
forall s a. Agent (->) s (Post a) [Post a] -> s -> Beh a
beh Agent (->) s (Post a) [Post a]
sys s
s' [Post a]
ins

-- | Conditional agent: branch between two agents based on the current state.
--
-- This is a level-1 grammar fragment: the carrier can carry a mode, and the
-- agent dispatches to one of two Moore machines depending on that mode. The
-- predicate is evaluated on the carrier before the input is consumed, which
-- is the honest Moore shape: output is a function of state, and the chosen
-- branch's update function determines the next state.
branchAgent :: (s -> Bool) -> Agent (->) s a b -> Agent (->) s a b -> Agent (->) s a b
branchAgent :: forall s a b.
(s -> Bool)
-> Agent (->) s a b -> Agent (->) s a b -> Agent (->) s a b
branchAgent s -> Bool
cond Agent (->) s a b
sys1 Agent (->) s a b
sys2 =
  ((s, Dir (Mono a b)) -> (s, Pos (Mono a b))) -> Agent (->) s a b
forall (arr :: * -> * -> *) s (p :: Poly).
arr (s, Dir p) (s, Pos p) -> System arr s p
system (((s, Dir (Mono a b)) -> (s, Pos (Mono a b))) -> Agent (->) s a b)
-> ((s, Dir (Mono a b)) -> (s, Pos (Mono a b))) -> Agent (->) s a b
forall a b. (a -> b) -> a -> b
$ \(s
state, Dir (Mono a b)
d) ->
    if s -> Bool
cond s
state then Agent (->) s 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 Agent (->) s a b
sys1 (s
state, Either Void a
Dir (Mono a b)
d) else Agent (->) s 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 Agent (->) s a b
sys2 (s
state, Either Void a
Dir (Mono a b)
d)

-- | Seat-level product / await: both agents run on the same input; states are
-- paired; emits are concatenated left-to-right.
awaitA ::
  Agent (->) s1 (Post a) [Post a] ->
  Agent (->) s2 (Post a) [Post a] ->
  Agent (->) (s1, s2) (Post a) [Post a]
awaitA :: forall s1 a s2.
Agent (->) s1 (Post a) [Post a]
-> Agent (->) s2 (Post a) [Post a]
-> Agent (->) (s1, s2) (Post a) [Post a]
awaitA Agent (->) s1 (Post a) [Post a]
sys1 Agent (->) s2 (Post a) [Post a]
sys2 = (((s1, s2), Dir (Mono (Post a) [Post a]))
 -> ((s1, s2), Pos (Mono (Post a) [Post a])))
-> System (->) (s1, s2) (Mono (Post a) [Post a])
forall (arr :: * -> * -> *) s (p :: Poly).
arr (s, Dir p) (s, Pos p) -> System arr s p
system ((((s1, s2), Dir (Mono (Post a) [Post a]))
  -> ((s1, s2), Pos (Mono (Post a) [Post a])))
 -> System (->) (s1, s2) (Mono (Post a) [Post a]))
-> (((s1, s2), Dir (Mono (Post a) [Post a]))
    -> ((s1, s2), Pos (Mono (Post a) [Post a])))
-> System (->) (s1, s2) (Mono (Post a) [Post a])
forall a b. (a -> b) -> a -> b
$ \((s1
s1, s2
s2), Dir (Mono (Post a) [Post a])
d) ->
  let (s1
s1', ([Post a]
o1, ())) = Agent (->) s1 (Post a) [Post a]
-> (s1, Dir (Mono (Post a) [Post a]))
   -> (s1, Pos (Mono (Post a) [Post a]))
forall (arr :: * -> * -> *) s (p :: Poly).
System arr s p -> arr (s, Dir p) (s, Pos p)
runSystem Agent (->) s1 (Post a) [Post a]
sys1 (s1
s1, Either Void (Post a)
Dir (Mono (Post a) [Post a])
d)
      (s2
s2', ([Post a]
o2, ())) = Agent (->) s2 (Post a) [Post a]
-> (s2, Dir (Mono (Post a) [Post a]))
   -> (s2, Pos (Mono (Post a) [Post a]))
forall (arr :: * -> * -> *) s (p :: Poly).
System arr s p -> arr (s, Dir p) (s, Pos p)
runSystem Agent (->) s2 (Post a) [Post a]
sys2 (s2
s2, Either Void (Post a)
Dir (Mono (Post a) [Post a])
d)
   in ((s1
s1', s2
s2'), ([Post a]
o1 [Post a] -> [Post a] -> [Post a]
forall a. Semigroup a => a -> a -> a
<> [Post a]
o2, ()))

-- | Seat-level coproduct / race: both agents run on the same input; states are
-- paired; the left emit wins if non-empty, otherwise the right emit wins.
raceA ::
  Agent (->) s1 (Post a) [Post a] ->
  Agent (->) s2 (Post a) [Post a] ->
  Agent (->) (s1, s2) (Post a) [Post a]
raceA :: forall s1 a s2.
Agent (->) s1 (Post a) [Post a]
-> Agent (->) s2 (Post a) [Post a]
-> Agent (->) (s1, s2) (Post a) [Post a]
raceA Agent (->) s1 (Post a) [Post a]
sys1 Agent (->) s2 (Post a) [Post a]
sys2 = (((s1, s2), Dir (Mono (Post a) [Post a]))
 -> ((s1, s2), Pos (Mono (Post a) [Post a])))
-> System (->) (s1, s2) (Mono (Post a) [Post a])
forall (arr :: * -> * -> *) s (p :: Poly).
arr (s, Dir p) (s, Pos p) -> System arr s p
system ((((s1, s2), Dir (Mono (Post a) [Post a]))
  -> ((s1, s2), Pos (Mono (Post a) [Post a])))
 -> System (->) (s1, s2) (Mono (Post a) [Post a]))
-> (((s1, s2), Dir (Mono (Post a) [Post a]))
    -> ((s1, s2), Pos (Mono (Post a) [Post a])))
-> System (->) (s1, s2) (Mono (Post a) [Post a])
forall a b. (a -> b) -> a -> b
$ \((s1
s1, s2
s2), Dir (Mono (Post a) [Post a])
d) ->
  let (s1
s1', ([Post a]
o1, ())) = Agent (->) s1 (Post a) [Post a]
-> (s1, Dir (Mono (Post a) [Post a]))
   -> (s1, Pos (Mono (Post a) [Post a]))
forall (arr :: * -> * -> *) s (p :: Poly).
System arr s p -> arr (s, Dir p) (s, Pos p)
runSystem Agent (->) s1 (Post a) [Post a]
sys1 (s1
s1, Either Void (Post a)
Dir (Mono (Post a) [Post a])
d)
      (s2
s2', ([Post a]
o2, ())) = Agent (->) s2 (Post a) [Post a]
-> (s2, Dir (Mono (Post a) [Post a]))
   -> (s2, Pos (Mono (Post a) [Post a]))
forall (arr :: * -> * -> *) s (p :: Poly).
System arr s p -> arr (s, Dir p) (s, Pos p)
runSystem Agent (->) s2 (Post a) [Post a]
sys2 (s2
s2, Either Void (Post a)
Dir (Mono (Post a) [Post a])
d)
      o :: [Post a]
o = if [Post a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Post a]
o1 then [Post a]
o2 else [Post a]
o1
   in ((s1
s1', s2
s2'), ([Post a]
o, ()))

-- ---------------------------------------------------------------------------
-- Agent as Shard — change of base into K Ends
-- ---------------------------------------------------------------------------

-- | State behind an 'agentShard': free carrier plus a pending emit queue.
--
-- Commit parses inputs into the carrier and enqueues one output list per
-- input (the Moore step).  Emit flushes the queue — empty means quiet.
data AgentSeat s a = AgentSeat
  { forall s a. AgentSeat s a -> s
asState :: s,
    -- | Pending outputs, oldest first.
    forall s a. AgentSeat s a -> [Post a]
asOutbox :: [Post a]
  }
  deriving (Int -> AgentSeat s a -> ShowS
[AgentSeat s a] -> ShowS
AgentSeat s a -> String
(Int -> AgentSeat s a -> ShowS)
-> (AgentSeat s a -> String)
-> ([AgentSeat s a] -> ShowS)
-> Show (AgentSeat s a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s a. (Show s, Show a) => Int -> AgentSeat s a -> ShowS
forall s a. (Show s, Show a) => [AgentSeat s a] -> ShowS
forall s a. (Show s, Show a) => AgentSeat s a -> String
$cshowsPrec :: forall s a. (Show s, Show a) => Int -> AgentSeat s a -> ShowS
showsPrec :: Int -> AgentSeat s a -> ShowS
$cshow :: forall s a. (Show s, Show a) => AgentSeat s a -> String
show :: AgentSeat s a -> String
$cshowList :: forall s a. (Show s, Show a) => [AgentSeat s a] -> ShowS
showList :: [AgentSeat s a] -> ShowS
Show, AgentSeat s a -> AgentSeat s a -> Bool
(AgentSeat s a -> AgentSeat s a -> Bool)
-> (AgentSeat s a -> AgentSeat s a -> Bool) -> Eq (AgentSeat s a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall s a. (Eq s, Eq a) => AgentSeat s a -> AgentSeat s a -> Bool
$c== :: forall s a. (Eq s, Eq a) => AgentSeat s a -> AgentSeat s a -> Bool
== :: AgentSeat s a -> AgentSeat s a -> Bool
$c/= :: forall s a. (Eq s, Eq a) => AgentSeat s a -> AgentSeat s a -> Bool
/= :: AgentSeat s a -> AgentSeat s a -> Bool
Eq)

-- | Pure parse step: fold committed posts through the coalgebra.
feedAgent :: Agent (->) s (Post a) [Post a] -> [Post a] -> AgentSeat s a -> AgentSeat s a
feedAgent :: forall s a.
Agent (->) s (Post a) [Post a]
-> [Post a] -> AgentSeat s a -> AgentSeat s a
feedAgent Agent (->) s (Post a) [Post a]
sys [Post a]
ins (AgentSeat s
s0 [Post a]
outs0) =
  let ([Post a]
outs1, s
s1) =
        (([Post a], s) -> Post a -> ([Post a], s))
-> ([Post a], s) -> [Post a] -> ([Post a], s)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl'
          ( \([Post a]
outs, s
s) Post a
i ->
              let ([Post a]
os, s
s') = Agent (->) s (Post a) [Post a] -> s -> Post a -> ([Post a], s)
forall s i o. Agent (->) s i o -> s -> i -> (o, s)
run1 Agent (->) s (Post a) [Post a]
sys s
s Post a
i
               in ([Post a]
outs [Post a] -> [Post a] -> [Post a]
forall a. [a] -> [a] -> [a]
++ [Post a]
os, s
s')
          )
          ([], s
s0)
          [Post a]
ins
   in s -> [Post a] -> AgentSeat s a
forall s a. s -> [Post a] -> AgentSeat s a
AgentSeat s
s1 ([Post a]
outs0 [Post a] -> [Post a] -> [Post a]
forall a. [a] -> [a] -> [a]
++ [Post a]
outs1)

-- | Take the outbox; leave carrier unchanged.
flushOutbox :: AgentSeat s a -> ([Post a], AgentSeat s a)
flushOutbox :: forall s a. AgentSeat s a -> ([Post a], AgentSeat s a)
flushOutbox (AgentSeat s
s [Post a]
outs) = ([Post a]
outs, s -> [Post a] -> AgentSeat s a
forall s a. s -> [Post a] -> AgentSeat s a
AgentSeat s
s [])

-- | Reinterpret a pure 'Agent' as a list 'Shard'.
--
-- @
-- agentShard get put sys  ::  Shard m [Post] [Post]
-- @
--
-- is the change of base from @(->)@ (the Moore coalgebra) into
-- @K m@ ends: commit = parse inputs, emit = flush replies.  The
-- interior stays opaque at the 'Shard' boundary — only @[Post]@ in and out.
--
-- @get@ \/ @put@ hold the 'AgentSeat' (e.g. 'Data.IORef' in @IO@, or
-- @State@ in tests).  Example — reply agent over @State@:
--
-- @
-- let sys = tape (\\hist -> (peek hist) { from = "j", to = [from (peek hist)], body = "ack: " <> body (peek hist) })
--     sh  = agentShard get put sys  :: Shard (State (AgentSeat [Post])) [Post] [Post]
-- in  evalState (runK (close (conjoint sh) (companion sh)) [humanPost]) (AgentSeat [] [])
-- @
agentShard ::
  (Monad m) =>
  m (AgentSeat s a) ->
  (AgentSeat s a -> m ()) ->
  Agent (->) s (Post a) [Post a] ->
  Shard m [Post a] [Post a]
agentShard :: forall (m :: * -> *) s a.
Monad m =>
m (AgentSeat s a)
-> (AgentSeat s a -> m ())
-> Agent (->) s (Post a) [Post a]
-> Shard m [Post a] [Post a]
agentShard m (AgentSeat s a)
getSeat AgentSeat s a -> m ()
putSeat Agent (->) s (Post a) [Post a]
sys =
  ([Post a] -> m ()) -> m [Post a] -> Shard m [Post a] [Post a]
forall (m :: * -> *) a.
Monad m =>
(a -> m ()) -> m a -> Shard m a a
shard
    ( \[Post a]
ins -> do
        seat <- m (AgentSeat s a)
getSeat
        putSeat (feedAgent sys ins seat)
    )
    ( do
        seat <- m (AgentSeat s a)
getSeat
        let (outs, seat') = flushOutbox seat
        putSeat seat'
        pure outs
    )

-- | One closed turn of an agent-as-shard: commit @ins@, emit replies, new seat.
--
-- Pure form of @close@ on 'agentShard' without choosing a monad:
--
-- @runAgentShard sys seat ins = runState (close (agentShard get put sys) ins) seat@
runAgentShard :: Agent (->) s (Post a) [Post a] -> AgentSeat s a -> [Post a] -> ([Post a], AgentSeat s a)
runAgentShard :: forall s a.
Agent (->) s (Post a) [Post a]
-> AgentSeat s a -> [Post a] -> ([Post a], AgentSeat s a)
runAgentShard Agent (->) s (Post a) [Post a]
sys AgentSeat s a
seat [Post a]
ins =
  let seat1 :: AgentSeat s a
seat1 = Agent (->) s (Post a) [Post a]
-> [Post a] -> AgentSeat s a -> AgentSeat s a
forall s a.
Agent (->) s (Post a) [Post a]
-> [Post a] -> AgentSeat s a -> AgentSeat s a
feedAgent Agent (->) s (Post a) [Post a]
sys [Post a]
ins AgentSeat s a
seat
      ([Post a]
outs, AgentSeat s a
seat2) = AgentSeat s a -> ([Post a], AgentSeat s a)
forall s a. AgentSeat s a -> ([Post a], AgentSeat s a)
flushOutbox AgentSeat s a
seat1
   in ([Post a]
outs, AgentSeat s a
seat2)

-- ---------------------------------------------------------------------------
-- Token seat — stream coalgebra around a list Shard (parser dual)
-- ---------------------------------------------------------------------------

-- | Single-post ends: keyboard \/ one-out seat.
--
-- Obtained by buffering a list 'Shard' on both sides, or by a bare queue
-- ('openSTM' \/ 'openIO').
--
-- A /tool call/ from an agent is just a 'Post': the 'to' list names the
-- tool, 'body' carries the arguments. No extra type — emit that 'Post' on a
-- 'Port' (or post it on the log for the tool agent to 'watch').
type Port m a = Poles (K m) (Post a) (Post a)

-- 'Snoc' is re-exported from 'Circuit.Stream' (construction dual of 'Uncons').

-- | Snoc a 'Post' onto a post stream. Specialized alias for 'snoc'.
snocPost :: [Post a] -> Post a -> [Post a]
snocPost :: forall a. [Post a] -> Post a -> [Post a]
snocPost = [Post a] -> Post a -> [Post a]
forall f s. Snoc f s => f -> s -> f
snoc

-- | @Ends s f@: commit snocs a token; emit flushes the whole stream
-- (parser @takeRest@ — drain policy is "the stream", not a count).
--
-- @get@ \/ @put@ hold the stream buffer.
batchEnds ::
  forall f s m.
  (Monad m, Snoc f s) =>
  m f ->
  (f -> m ()) ->
  Shard m s f
batchEnds :: forall f s (m :: * -> *).
(Monad m, Snoc f s) =>
m f -> (f -> m ()) -> Shard m s f
batchEnds m f
getBuf f -> m ()
putBuf =
  (s -> m ()) -> m f -> Poles (K m) s f
forall (m :: * -> *) a b.
Monad m =>
(a -> m ()) -> m b -> Poles (K m) a b
polesK
    ( \s
x -> do
        xs <- m f
getBuf
        putBuf (snoc xs x)
    )
    ( do
        xs <- m f
getBuf
        putBuf (snocNil @f @s)
        pure xs
    )

-- | @Ends f s@: commit appends a stream; emit peels one token
-- (parser @next@ \/ 'uncons'). Empty stream is quiet — the buffer is left
-- empty and the returned token is 'undefined' because the polymorphic token
-- type has no empty value.  In practice the list 'Shard' layer ensures quiet
-- periods are represented by an empty stream, so this case should not be
-- reached.
--
-- @get@ \/ @put@ hold the stream buffer.
unbatchEnds ::
  forall f s m.
  (Monad m, Semigroup f, Uncons f s) =>
  m f ->
  (f -> m ()) ->
  Shard m f s
unbatchEnds :: forall f s (m :: * -> *).
(Monad m, Semigroup f, Uncons f s) =>
m f -> (f -> m ()) -> Shard m f s
unbatchEnds m f
getBuf f -> m ()
putBuf =
  (f -> m ()) -> m s -> Poles (K m) f s
forall (m :: * -> *) a b.
Monad m =>
(a -> m ()) -> m b -> Poles (K m) a b
polesK
    ( \f
ys -> do
        xs <- m f
getBuf
        putBuf (xs <> ys)
    )
    ( do
        xs <- m f
getBuf
        case uncons xs of
          That f
_ -> do
            f -> m ()
putBuf (forall f s. Uncons f s => f
nil @f @s)
            s -> m s
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (s
forall a. HasCallStack => a
undefined :: s)
          This s
x -> do
            f -> m ()
putBuf (forall f s. Uncons f s => f
nil @f @s)
            s -> m s
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure s
x
          These s
x f
rest -> do
            f -> m ()
putBuf f
rest
            s -> m s
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure s
x
    )

-- | Token seat around a list 'Shard': buffer on both ends via stream coalgebra.
--
-- @
-- portShard getIn putIn getOut putOut sh
--   = batchEnds getIn putIn >:> sh >:> unbatchEnds getOut putOut
-- @
--
-- Flush\/drain is not a separate policy knob — it /is/ build-stream ('snoc')
-- and peel-stream ('uncons'), the same syntax as parsers over @[s]@.
portShard ::
  (Monad m) =>
  m [Post a] ->
  ([Post a] -> m ()) ->
  m [Post a] ->
  ([Post a] -> m ()) ->
  Shard m [Post a] [Post a] ->
  Port m a
portShard :: forall (m :: * -> *) a.
Monad m =>
m [Post a]
-> ([Post a] -> m ())
-> m [Post a]
-> ([Post a] -> m ())
-> Shard m [Post a] [Post a]
-> Port m a
portShard m [Post a]
getIn [Post a] -> m ()
putIn m [Post a]
getOut [Post a] -> m ()
putOut Shard m [Post a] [Post a]
sh =
  Shard m (Post a) [Post a]
-> Shard m [Post a] (Post a) -> Shard m (Post a) (Post a)
forall (m :: * -> *) a b c.
Monad m =>
Shard m a b -> Shard m b c -> Shard m a c
composeShard (Shard m (Post a) [Post a]
-> Shard m [Post a] [Post a] -> Shard m (Post a) [Post a]
forall (m :: * -> *) a b c.
Monad m =>
Shard m a b -> Shard m b c -> Shard m a c
composeShard (m [Post a] -> ([Post a] -> m ()) -> Shard m (Post a) [Post a]
forall f s (m :: * -> *).
(Monad m, Snoc f s) =>
m f -> (f -> m ()) -> Shard m s f
batchEnds m [Post a]
getIn [Post a] -> m ()
putIn) Shard m [Post a] [Post a]
sh) (m [Post a] -> ([Post a] -> m ()) -> Shard m [Post a] (Post a)
forall f s (m :: * -> *).
(Monad m, Semigroup f, Uncons f s) =>
m f -> (f -> m ()) -> Shard m f s
unbatchEnds m [Post a]
getOut [Post a] -> m ()
putOut)

-- ---------------------------------------------------------------------------
-- Shard combinators
-- ---------------------------------------------------------------------------

-- | Adapt a shard on the commit side (contravariant).
--
-- Transform the input before it is committed.  One common use is
-- session assembly: @prefixShard session@ changes the payload that the
-- shard posts.
prefixShard :: (Monad m) => (a' -> a) -> Shard m a b -> Shard m a' b
prefixShard :: forall (m :: * -> *) a' a b.
Monad m =>
(a' -> a) -> Shard m a b -> Shard m a' b
prefixShard a' -> a
f = K m a' a -> Poles (K m) a b -> Poles (K m) a' b
forall {k} (arr :: k -> k -> *) (a :: k) (a' :: k) (b :: k).
Category arr =>
arr a' a -> Poles arr a b -> Poles arr a' b
imap ((a' -> m a) -> K m a' a
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((a' -> m a) -> K m a' a) -> (a' -> m a) -> K m a' a
forall a b. (a -> b) -> a -> b
$ a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> m a) -> (a' -> a) -> a' -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a' -> a
f)

-- | Adapt a shard on the emit side (covariant).
--
-- Transform the output after it is emitted.  One common use is a
-- transport envelope: @suffixShard (map addHeader)@ decorates every
-- emitted post.
suffixShard :: (Monad m) => (b -> b') -> Shard m a b -> Shard m a b'
suffixShard :: forall (m :: * -> *) b b' a.
Monad m =>
(b -> b') -> Shard m a b -> Shard m a b'
suffixShard b -> b'
g = K m b b' -> Poles (K m) a b -> Poles (K m) a b'
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (b' :: k).
Category arr =>
arr b b' -> Poles arr a b -> Poles arr a b'
omap ((b -> m b') -> K m b b'
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((b -> m b') -> K m b b') -> (b -> m b') -> K m b b'
forall a b. (a -> b) -> a -> b
$ b' -> m b'
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (b' -> m b') -> (b -> b') -> b -> m b'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> b'
g)

-- | Adapt both sides of a shard at once.
--
-- @codecShard f g = prefixShard f . suffixShard g@.
codecShard :: (Monad m) => (a' -> a) -> (b -> b') -> Shard m a b -> Shard m a' b'
codecShard :: forall (m :: * -> *) a' a b b'.
Monad m =>
(a' -> a) -> (b -> b') -> Shard m a b -> Shard m a' b'
codecShard a' -> a
f b -> b'
g = K m a' a -> K m b b' -> Poles (K m) a b -> Poles (K m) a' b'
forall {k} (arr :: k -> k -> *) (a :: k) (a' :: k) (b :: k)
       (b' :: k).
Category arr =>
arr a' a -> arr b b' -> Poles arr a b -> Poles arr a' b'
iomap ((a' -> m a) -> K m a' a
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((a' -> m a) -> K m a' a) -> (a' -> m a) -> K m a' a
forall a b. (a -> b) -> a -> b
$ a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> m a) -> (a' -> a) -> a' -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a' -> a
f) ((b -> m b') -> K m b b'
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((b -> m b') -> K m b b') -> (b -> m b') -> K m b b'
forall a b. (a -> b) -> a -> b
$ b' -> m b'
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (b' -> m b') -> (b -> b') -> b -> m b'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> b'
g)

-- | Sequential composition of shards.
--
-- The output of the first shard feeds the input of the second.  This is
-- the same shape as connecting two effectful agents in series.
composeShard :: forall m a b c. (Monad m) => Shard m a b -> Shard m b c -> Shard m a c
composeShard :: forall (m :: * -> *) a b c.
Monad m =>
Shard m a b -> Shard m b c -> Shard m a c
composeShard = forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k)
       (bot :: k).
HasDual bot arr =>
Poles arr a b -> Poles arr b c -> Poles arr a c
forall (arr :: * -> * -> *) a b c bot.
HasDual bot arr =>
Poles arr a b -> Poles arr b c -> Poles arr a c
compose @(K m) @a @b @c @()