{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | Mark-driven halt machinery for STM agents.
--
-- This module graduates the first machina probe-station combinator into
-- @circuits-agent@.  The design principle: the builder posts its silence as a
-- token, and the runner halts on that read.  There is no 'orElse' fallback —
-- absence is not an opinion here.  If the mark never arrives, the runner
-- blocks; the halt is decided by content, not inferred from quiet.
--
-- The 'Loop Either' form pushes the same halt to the surface of a composition:
-- 'Left' = continue, 'Right' = halt.  This makes the mark-halt a trace citizen,
-- with the continuation folded away by 'trace'.
--
-- The rest of the machina probe station (quiet ends, sealed ends, stream ends)
-- stays in @circuits-agent-machina@ until a consumer appears here.
module Circuit.Agent.Machina.Mark
  ( -- * Mark-driven halt
    spinMark,
    markLoop,
  )
where

import Circuit (trace)
import Circuit.Category (K (..))
import Circuit.Poles (HasDual (..), Poles (..), emit, polesK)
import Circuit.Trace (Trace (..), base, yank)
import Control.Concurrent.STM (STM)
import Data.Function (fix)

-- | Unit poles for plugging the unused slot when reading or writing one end.
endsU :: Poles (K STM) () ()
endsU :: Poles (K STM) () ()
endsU = (() -> 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 ())

-- | Spin until the mark is /read/: the builder posts its silence as a token,
-- and the runner halts on that read.  No 'orElse' — absence is not an opinion
-- here.  If the mark never arrives, this blocks; the halt is decided by
-- content, not inferred from quiet.
--
-- Contrast a plain 'retry'-driven spin: that frame drains the queue and falls
-- through on absence; mark-driven halt is decisive mid-stream — tokens after
-- the mark are never consumed.
spinMark :: (a -> Bool) -> (s -> a -> s) -> Poles (K STM) a a -> K STM s s
spinMark :: forall a s.
(a -> Bool) -> (s -> a -> s) -> Poles (K STM) a a -> K STM s s
spinMark a -> Bool
isMark s -> a -> s
step Poles (K STM) a a
e = (K STM s s -> K STM s s) -> K STM s s
forall a. (a -> a) -> a
fix ((K STM s s -> K STM s s) -> K STM s s)
-> (K STM s s -> K STM s s) -> K STM s s
forall a b. (a -> b) -> a -> b
$ \K STM s s
go -> (s -> STM s) -> K STM s s
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((s -> STM s) -> K STM s s) -> (s -> STM s) -> K STM s s
forall a b. (a -> b) -> a -> b
$ \s
s -> do
  a <- 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
e) (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) () ()
endsU)) ()
  if isMark a
    then pure s
    else runK go (step s a)

-- | One mark frame in the 'Either'-trace halt alphabet: 'Left' = continue,
-- 'Right' = halt.  The read is committed before the decision, so the mark is
-- consumed either way.
markFrame :: (a -> Bool) -> (s -> a -> s) -> Poles (K STM) a a -> K STM (Either s s) (Either s s)
markFrame :: forall a s.
(a -> Bool)
-> (s -> a -> s)
-> Poles (K STM) a a
-> K STM (Either s s) (Either s s)
markFrame a -> Bool
isMark s -> a -> s
step Poles (K STM) a a
e = (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
$ \Either s s
es -> do
  let s :: s
s = (s -> s) -> (s -> s) -> Either s s -> s
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either s -> s
forall a. a -> a
id s -> s
forall a. a -> a
id Either s s
es
  a <- 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
e) (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) () ()
endsU)) ()
  pure
    ( if isMark a
        then Right s
        else Left (step s a)
    )

-- | The mark-halt pushed to the surface of a composition: a @Trace Either@
-- citizen.  The halt decision travels as data through the channel and the
-- 'trace' folds the continuation away — the runner is a value, not a loop
-- spelled in 'fix'.
markLoop :: (a -> Bool) -> (s -> a -> s) -> Poles (K STM) a a -> Trace Either (K STM) s s
markLoop :: forall a s.
(a -> Bool)
-> (s -> a -> s) -> Poles (K STM) a a -> Trace Either (K STM) s s
markLoop a -> Bool
isMark s -> a -> s
step Poles (K STM) a a
e = 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 ((a -> Bool)
-> (s -> a -> s)
-> Poles (K STM) a a
-> K STM (Either s s) (Either s s)
forall a s.
(a -> Bool)
-> (s -> a -> s)
-> Poles (K STM) a a
-> K STM (Either s s) (Either s s)
markFrame a -> Bool
isMark s -> a -> s
step Poles (K STM) a a
e))