{-# OPTIONS_GHC -Wno-pattern-namespace-specifier #-}

-- | Bridge: agents as string diagrams (stage 1 of endgame-path).
--
-- A monomial 'System' is a lens from its state interface
-- (@systemAsLens@: @System s p ≅ Poly(S y^S, p)@), and 'box' lifts such a
-- lens into the string-diagram DSL.  The result runs one Moore step per
-- 'runDiagram' call: the forward wire carries state → output, the backward
-- wire carries input-direction → next state.
--
-- Stage 1b: the bend, at the 'Process' layer.  A stateful agent decomposes
-- as a stateless body plus cross-tick feedback: 'register' closes the
-- state wire with 'delay' making the one-tick lag observable (sound for
-- strict state, where the lazy cartesian knot would diverge).  So:
--
-- @
-- agent = box + bend + delay ≡ mooreProcess sys s0 = register s0 body
-- @
--
-- What is still missing is the same wiring inside the
-- 'Circuit.Poly.StringDiagram' surface itself (a delay box and a trace
-- combinator over a 'Process' base); the oracles pin the semantics the
-- surface will need to reproduce.
--
-- Stage 2: 'meetingSkeleton' reads a conversation back as a drawing —
-- the unification claim that the log records the wiring.  Stage 2b draws
-- the full post-DAG: forks and syntheses are visible copy/merge spiders,
-- routed with 'SSwap'-built permutations.
module Free.Agent.Diagram
  ( agentDiagram,
    diagramStep,
    diagramSteps,
    liftProcess,
    mooreBody,
    mooreProcess,
    meetingSkeleton,
    skeletonLabels,
  )
where

import Circuit.Agent (Post (..))
import Circuit.Poly (Mono)
import Circuit.Poly.StringDiagram (Diagram, SDiagram (..), box, runDiagram)
import Circuit.Process (Process (..), register)
import Circuit.System (System, runSystemMono, systemAsLens)
import Data.List (delete, elemIndex, foldl', mapAccumL)
import Data.Text qualified as T

-- | A monomial system as a one-box diagram.
--
-- @box . systemAsLens@: forward wire @s → o@ (state to output), backward
-- wire @i → s@ (input direction to next state).
agentDiagram :: System (->) s (Mono i o) -> Diagram s s o i
agentDiagram :: forall s i o. System (->) s (Mono i o) -> Diagram s s o i
agentDiagram = Morphism (Mono s s) (Mono i o) -> Diagram s s o i
forall da a db b.
Morphism (Mono da a) (Mono db b) -> Diagram a da b db
box (Morphism (Mono s s) (Mono i o) -> Diagram s s o i)
-> (System (->) s (Mono i o) -> Morphism (Mono s s) (Mono i o))
-> System (->) s (Mono i o)
-> Diagram s s o i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. System (->) s (Mono i o) -> Morphism (Mono s s) (Mono i o)
forall s i o.
System (->) s (Mono i o) -> Morphism (Mono s s) (Mono i o)
systemAsLens

-- | One Moore step as a diagram run: @(next state, output at current
-- state)@.  Definitionally @(snd (runSystemMono sys s) i, fst (runSystemMono
-- sys s))@ — the oracle pins exactly this.
diagramStep :: System (->) s (Mono i o) -> s -> i -> (s, o)
diagramStep :: forall s i o. System (->) s (Mono i o) -> s -> i -> (s, o)
diagramStep System (->) s (Mono i o)
sys s
s i
i = Diagram s s o i -> (s, i) -> (s, o)
forall a da b db. Diagram a da b db -> (a, db) -> (da, b)
runDiagram (System (->) s (Mono i o) -> Diagram s s o i
forall s i o. System (->) s (Mono i o) -> Diagram s s o i
agentDiagram System (->) s (Mono i o)
sys) (s
s, i
i)

-- | Iterate a system over inputs through the diagram, mirroring
-- 'iterateSystem' (which emits the output of the state /after/ each
-- transition).  Each step runs the diagram twice with the same input: once
-- to consume (state transition), once to observe (output at the new
-- state).  The backward pass is pure, so the second run is harmless — and
-- both passes go through 'runDiagram', so the oracle exercises the bridge
-- end to end.
diagramSteps :: System (->) s (Mono i o) -> s -> [i] -> [o]
diagramSteps :: forall s i o. System (->) s (Mono i o) -> s -> [i] -> [o]
diagramSteps System (->) s (Mono i o)
_ s
_ [] = []
diagramSteps System (->) s (Mono i o)
sys s
s (i
i : [i]
is) =
  let (s
s', o
_) = System (->) s (Mono i o) -> s -> i -> (s, o)
forall s i o. System (->) s (Mono i o) -> s -> i -> (s, o)
diagramStep System (->) s (Mono i o)
sys s
s i
i
      (s
_, o
o) = System (->) s (Mono i o) -> s -> i -> (s, o)
forall s i o. System (->) s (Mono i o) -> s -> i -> (s, o)
diagramStep System (->) s (Mono i o)
sys s
s' i
i
   in o
o o -> [o] -> [o]
forall a. a -> [a] -> [a]
: System (->) s (Mono i o) -> s -> [i] -> [o]
forall s i o. System (->) s (Mono i o) -> s -> [i] -> [o]
diagramSteps System (->) s (Mono i o)
sys s
s' [i]
is

-- | Lift a pure function to a stateless 'Process' (the box a bend closes).
liftProcess :: (a -> b) -> Process a b
liftProcess :: forall a b. (a -> b) -> Process a b
liftProcess a -> b
f = (a -> a) -> (a -> a -> a) -> (a -> b) -> Process a b
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process a -> a
forall a. a -> a
id ((a -> a) -> a -> a -> a
forall a b. a -> b -> a
const a -> a
forall a. a -> a
id) a -> b
f

-- | The stateless body of a system as a 'Process': consume the input
-- (state transition), then read the output of the new state, and emit the
-- new state on the feedback wire.  This matches 'iterateSystem' /
-- 'systemAsProcess' semantics: the output is read /after/ consuming the
-- input.
mooreBody :: System (->) s (Mono i o) -> Process (i, s) (o, s)
mooreBody :: forall s i o. System (->) s (Mono i o) -> Process (i, s) (o, s)
mooreBody System (->) s (Mono i o)
sys = ((i, s) -> (o, s)) -> Process (i, s) (o, s)
forall a b. (a -> b) -> Process a b
liftProcess (\(i
i, s
s) -> let s' :: s
s' = (o, i -> s) -> i -> s
forall a b. (a, b) -> b
snd (System (->) s (Mono i o) -> s -> (o, i -> s)
forall s i o. System (->) s (Mono i o) -> s -> (o, i -> s)
runSystemMono System (->) s (Mono i o)
sys s
s) i
i in ((o, i -> s) -> o
forall a b. (a, b) -> a
fst (System (->) s (Mono i o) -> s -> (o, i -> s)
forall s i o. System (->) s (Mono i o) -> s -> (o, i -> s)
runSystemMono System (->) s (Mono i o)
sys s
s'), s
s'))

-- | A system as a 'Process': the stateless 'mooreBody' with its state wire
-- bent back through a one-tick 'delay' — 'register' makes the delay
-- explicit in the wiring rather than implicit in a lazy knot.
--
-- Oracle-pinned: @scan (mooreProcess sys s0) is == iterateSystem sys s0 is@.
mooreProcess :: System (->) s (Mono i o) -> s -> Process i o
mooreProcess :: forall s i o. System (->) s (Mono i o) -> s -> Process i o
mooreProcess System (->) s (Mono i o)
sys s
s0 = s -> Process (i, s) (o, s) -> Process i o
forall s a b. s -> Process (a, s) (b, s) -> Process a b
register s
s0 (System (->) s (Mono i o) -> Process (i, s) (o, s)
forall s i o. System (->) s (Mono i o) -> Process (i, s) (o, s)
mooreBody System (->) s (Mono i o)
sys)

-- | The drawing skeleton of a conversation: each post is a box labelled by
-- its sender, wired by its 'thread' ancestry — "the log is the diagram of
-- the meeting that produced it".  A root is @SBox label 0 1@ (nothing
-- feeds it), a reply @SBox label 1 1@, and a synthesis with m parents is
-- preceded by a visible merge spider ('SSpider' @m 1@); a post cited as
-- parent by k > 1 later posts forks its output through a visible copy
-- spider ('SSpider' @1 k@).
--
-- One pass over the log, oldest first: the state is the list of live wire
-- ends (each tagged by the thread edge it feeds, or by the post whose
-- uncited output it carries to the boundary), and each post emits one
-- layer — permute the parent wires to the back (adjacent 'SSwap's), merge,
-- box, fork.  A dangling thread edge (parent not in the log) becomes a
-- free input wire, present from the left boundary.
meetingSkeleton :: [Post a] -> SDiagram
meetingSkeleton :: forall a. [Post a] -> SDiagram
meetingSkeleton [] = SDiagram
SWire
meetingSkeleton [Post a]
ps = (SDiagram -> SDiagram -> SDiagram) -> [SDiagram] -> SDiagram
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 SDiagram -> SDiagram -> SDiagram
SThenD (([Either Int (Int, Int)], [SDiagram]) -> [SDiagram]
forall a b. (a, b) -> b
snd (([Either Int (Int, Int)]
 -> Int -> ([Either Int (Int, Int)], SDiagram))
-> [Either Int (Int, Int)]
-> [Int]
-> ([Either Int (Int, Int)], [SDiagram])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL [Either Int (Int, Int)]
-> Int -> ([Either Int (Int, Int)], SDiagram)
step [Either Int (Int, Int)]
dangling [Int
0 .. [Post a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Post a]
ps Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]))
  where
    -- thread edges are exact positional ids into the oldest-first log;
    -- 'Nothing' is a dangling id (expected not to happen for a well-formed
    -- stamped meeting).
    sources :: [[Maybe PostId]]
sources =
      [ [if PostId
i PostId -> PostId -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> PostId
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
j then PostId -> Maybe PostId
forall a. a -> Maybe a
Just PostId
i else Maybe PostId
forall a. Maybe a
Nothing | PostId
i <- Post a -> [PostId]
forall a. Post a -> [PostId]
thread Post a
p]
      | (Int
j, Post a
p) <- [Int] -> [Post a] -> [(Int, Post a)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([Int
0 ..] :: [Int]) [Post a]
ps
      ]
    -- the citation edges of post j, in consumer (log) order
    cited :: Int -> [(Int, Int)]
cited Int
j = [(Int
i, Int
pos) | (Int
i, [Maybe PostId]
ss) <- [Int] -> [[Maybe PostId]] -> [(Int, [Maybe PostId])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] [[Maybe PostId]]
sources, (Int
pos, Just PostId
j') <- [Int] -> [Maybe PostId] -> [(Int, Maybe PostId)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] [Maybe PostId]
ss, PostId
j' PostId -> PostId -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> PostId
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
j]
    -- one free input wire per dangling edge
    dangling :: [Either Int (Int, Int)]
dangling = [(Int, Int) -> Either Int (Int, Int)
forall a b. b -> Either a b
Right (Int
i, Int
pos) | (Int
i, [Maybe PostId]
ss) <- [Int] -> [[Maybe PostId]] -> [(Int, [Maybe PostId])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] [[Maybe PostId]]
sources, (Int
pos, Maybe PostId
Nothing) <- [Int] -> [Maybe PostId] -> [(Int, Maybe PostId)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] [Maybe PostId]
ss]

    step :: [Either Int (Int, Int)] -> Int -> ([Either Int (Int, Int)], SDiagram)
    step :: [Either Int (Int, Int)]
-> Int -> ([Either Int (Int, Int)], SDiagram)
step [Either Int (Int, Int)]
live Int
i = ([Either Int (Int, Int)]
rest [Either Int (Int, Int)]
-> [Either Int (Int, Int)] -> [Either Int (Int, Int)]
forall a. [a] -> [a] -> [a]
++ [Either Int (Int, Int)]
outs, SDiagram
layer)
      where
        label :: String
label = Text -> String
T.unpack (Post a -> Text
forall a. Post a -> Text
from ([Post a]
ps [Post a] -> Int -> Post a
forall a. HasCallStack => [a] -> Int -> a
!! Int
i))
        m :: Int
m = [PostId] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Post a -> [PostId]
forall a. Post a -> [PostId]
thread ([Post a]
ps [Post a] -> Int -> Post a
forall a. HasCallStack => [a] -> Int -> a
!! Int
i))
        nW :: Int
nW = [Either Int (Int, Int)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Either Int (Int, Int)]
live
        -- bring the m parent wires to the back, in thread order, filling
        -- positions right to left so each bubble only crosses unfixed wires
        ([Int]
swaps, [Either Int (Int, Int)]
ordered) =
          (([Int], [Either Int (Int, Int)])
 -> (Int, Either Int (Int, Int))
 -> ([Int], [Either Int (Int, Int)]))
-> ([Int], [Either Int (Int, Int)])
-> [(Int, Either Int (Int, Int))]
-> ([Int], [Either Int (Int, Int)])
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ([Int], [Either Int (Int, Int)])
-> (Int, Either Int (Int, Int)) -> ([Int], [Either Int (Int, Int)])
forall {a}. Eq a => ([Int], [a]) -> (Int, a) -> ([Int], [a])
bubble ([], [Either Int (Int, Int)]
live) ([Int] -> [Either Int (Int, Int)] -> [(Int, Either Int (Int, Int))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
nW Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1, Int
nW Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2 ..] ([Either Int (Int, Int)] -> [Either Int (Int, Int)]
forall a. [a] -> [a]
reverse ((Int -> Either Int (Int, Int)) -> [Int] -> [Either Int (Int, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Int -> Either Int (Int, Int)
forall {a} {b} {a}. a -> b -> Either a (a, b)
edge Int
i) [Int
0 .. Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1])))
        bubble :: ([Int], [a]) -> (Int, a) -> ([Int], [a])
bubble ([Int]
ss, [a]
xs) (Int
t, a
w) = case a -> [a] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex a
w [a]
xs of
          Maybe Int
Nothing -> String -> ([Int], [a])
forall a. HasCallStack => String -> a
error String
"meetingSkeleton: parent wire not live"
          Just Int
p -> ([Int]
ss [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int
p .. Int
t Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1], Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take Int
t (a -> [a] -> [a]
forall a. Eq a => a -> [a] -> [a]
delete a
w [a]
xs) [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a
w] [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop Int
t (a -> [a] -> [a]
forall a. Eq a => a -> [a] -> [a]
delete a
w [a]
xs))
        rest :: [Either Int (Int, Int)]
rest = Int -> [Either Int (Int, Int)] -> [Either Int (Int, Int)]
forall a. Int -> [a] -> [a]
take (Int
nW Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
m) [Either Int (Int, Int)]
ordered
        outs :: [Either Int (Int, Int)]
outs = case Int -> [(Int, Int)]
cited Int
i of
          [] -> [Int -> Either Int (Int, Int)
forall a b. a -> Either a b
Left Int
i]
          [(Int, Int)]
es -> ((Int, Int) -> Either Int (Int, Int))
-> [(Int, Int)] -> [Either Int (Int, Int)]
forall a b. (a -> b) -> [a] -> [b]
map ((Int -> Int -> Either Int (Int, Int))
-> (Int, Int) -> Either Int (Int, Int)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> Int -> Either Int (Int, Int)
forall {a} {b} {a}. a -> b -> Either a (a, b)
edge) [(Int, Int)]
es
        mergeBox :: SDiagram
mergeBox = case Int
m of
          Int
0 -> String -> Int -> Int -> SDiagram
SBox String
label Int
0 Int
1
          Int
1 -> String -> Int -> Int -> SDiagram
SBox String
label Int
1 Int
1
          Int
_ -> SDiagram -> SDiagram -> SDiagram
SThenD (Int -> Int -> SDiagram
SSpider Int
m Int
1) (String -> Int -> Int -> SDiagram
SBox String
label Int
1 Int
1)
        consumedPart :: SDiagram
consumedPart
          | [Either Int (Int, Int)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Either Int (Int, Int)]
outs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 = SDiagram -> SDiagram -> SDiagram
SThenD SDiagram
mergeBox (Int -> Int -> SDiagram
SSpider Int
1 ([Either Int (Int, Int)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Either Int (Int, Int)]
outs))
          | Bool
otherwise = SDiagram
mergeBox
        body :: SDiagram
body = case [Either Int (Int, Int)]
rest of
          [] -> SDiagram
consumedPart
          [Either Int (Int, Int)]
rs -> SDiagram -> SDiagram -> SDiagram
SBeside (Int -> SDiagram
forall {t}. (Eq t, Num t) => t -> SDiagram
wires ([Either Int (Int, Int)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Either Int (Int, Int)]
rs)) SDiagram
consumedPart
        layer :: SDiagram
layer = case [Int]
swaps of
          [] -> SDiagram
body
          [Int]
ss -> SDiagram -> SDiagram -> SDiagram
SThenD ((SDiagram -> SDiagram -> SDiagram) -> [SDiagram] -> SDiagram
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 SDiagram -> SDiagram -> SDiagram
SThenD ((Int -> SDiagram) -> [Int] -> [SDiagram]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Int -> SDiagram
forall {t}. (Ord t, Num t) => t -> t -> SDiagram
swapAt Int
nW) [Int]
ss)) SDiagram
body

    edge :: a -> b -> Either a (a, b)
edge a
i b
pos = (a, b) -> Either a (a, b)
forall a b. b -> Either a b
Right (a
i, b
pos)

    -- adjacent swap at index s on a bundle of n wires
    swapAt :: t -> t -> SDiagram
swapAt t
n t
s =
      (SDiagram -> SDiagram -> SDiagram) -> [SDiagram] -> SDiagram
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1
        SDiagram -> SDiagram -> SDiagram
SBeside
        ([t -> SDiagram
forall {t}. (Eq t, Num t) => t -> SDiagram
wires t
s | t
s t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
0] [SDiagram] -> [SDiagram] -> [SDiagram]
forall a. [a] -> [a] -> [a]
++ [SDiagram
SSwap] [SDiagram] -> [SDiagram] -> [SDiagram]
forall a. [a] -> [a] -> [a]
++ [t -> SDiagram
forall {t}. (Eq t, Num t) => t -> SDiagram
wires (t
n t -> t -> t
forall a. Num a => a -> a -> a
- t
s t -> t -> t
forall a. Num a => a -> a -> a
- t
2) | t
n t -> t -> t
forall a. Num a => a -> a -> a
- t
s t -> t -> t
forall a. Num a => a -> a -> a
- t
2 t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
0])

    -- identity on a bundle of r >= 1 wires
    wires :: t -> SDiagram
wires t
1 = SDiagram
SWire
    wires t
r = SDiagram -> SDiagram -> SDiagram
SBeside SDiagram
SWire (t -> SDiagram
wires (t
r t -> t -> t
forall a. Num a => a -> a -> a
- t
1))

-- | The box labels of a skeleton, in composition order.
skeletonLabels :: SDiagram -> [String]
skeletonLabels :: SDiagram -> [String]
skeletonLabels SDiagram
SWire = []
skeletonLabels (SBox String
l Int
_ Int
_) = [String
l]
skeletonLabels (SSpider Int
_ Int
_) = [String
"spider"]
skeletonLabels SDiagram
SPrismBox = [String
"prism"]
skeletonLabels (SBeside SDiagram
f SDiagram
g) = SDiagram -> [String]
skeletonLabels SDiagram
f [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ SDiagram -> [String]
skeletonLabels SDiagram
g
skeletonLabels (SThenD SDiagram
f SDiagram
g) = SDiagram -> [String]
skeletonLabels SDiagram
f [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ SDiagram -> [String]
skeletonLabels SDiagram
g
skeletonLabels SDiagram
SBend = [String
"cup"]
skeletonLabels SDiagram
SBend' = [String
"cap"]
skeletonLabels (STurn SDiagram
f) = SDiagram -> [String]
skeletonLabels SDiagram
f
skeletonLabels SDiagram
SUnitL = [String
"unitL"]
skeletonLabels SDiagram
SUnitL' = [String
"unitL'"]
skeletonLabels SDiagram
SUnitR = [String
"unitR"]
skeletonLabels SDiagram
SUnitR' = [String
"unitR'"]
skeletonLabels SDiagram
SAssoc = [String
"assoc"]
skeletonLabels SDiagram
SAssoc' = [String
"assoc'"]
skeletonLabels SDiagram
SSwap = [String
"swap"]
skeletonLabels (STrace SDiagram
f) = SDiagram -> [String]
skeletonLabels SDiagram
f