{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}

-- | A pure meeting driver and the replay oracle (stage 5 of endgame-path).
--
-- A meeting is rounds over a roster: round 1 sees the seed, each later
-- round sees the previous round's outputs.  The log is the seed followed
-- by the concatenated rounds — oldest first, exactly the shape 'cone' and
-- 'branches' resolve against.
--
-- Replay is re-running the same meeting with one box swapped (different
-- model, fixed prompt).  The oracles pin:
--
--   * a fresh identical roster reproduces the log exactly;
--   * posts whose cone avoids the swapped name reproduce identically
--     ('unchanged');
--   * posts downstream of the swap differ;
--   * thread edges are now exact 'PostId's assigned positionally by the
--     driver, so a same-named swap is visible as soon as it reaches a
--     thread edge.
--
-- Approach taken: 'AgentBox' now receives both the input posts and their
-- positional ids for the current round.  The driver assigns ids to the
-- concatenated outputs after each round, so every post in the returned
-- log carries the correct ids and every reply/synthesis can cite them.
module Free.Agent.Meeting
  ( AgentBox (..),
    quoter,
    runAgentBox,
    withIds,
    meet,
    meetLog,
    unchanged,
  )
where

import Circuit.Agent (Agent, Name, Post (..), PostId, coneByIndex)
import Circuit.Agent.Query (synthesisPosts)
import Circuit.System (System, monoDir, monoIn, runSystem, system)
import Circuit.System qualified as System
import Data.List (inits, intersect)
import Data.Text (Text)
import Data.Text qualified as T

-- | Existential box around a pure batch agent, carrying its current state.
--
-- The agent input is a pair: the batch of posts and the positional ids the
-- driver assigned to that batch.  This lets agents thread replies/syntheses
-- by exact reference without inventing ids.
data AgentBox where
  AgentBox :: s -> Agent (->) s ([Post Text], [PostId]) [Post Text] -> AgentBox

-- | One batch step: absorb the input and its ids, emit the answer
-- ('iterateSystem' semantics — output is read from the post-input state).
runAgentBox :: AgentBox -> [Post Text] -> [PostId] -> ([Post Text], AgentBox)
runAgentBox :: AgentBox -> [Post Name] -> [PostId] -> ([Post Name], AgentBox)
runAgentBox (AgentBox s
s Agent (->) s ([Post Name], [PostId]) [Post Name]
ag) [Post Name]
ins [PostId]
ids =
  let s' :: s
s' = ([Post Name], ([Post Name], [PostId]) -> s)
-> ([Post Name], [PostId]) -> s
forall a b. (a, b) -> b
snd (Agent (->) s ([Post Name], [PostId]) [Post Name]
-> s -> ([Post Name], ([Post Name], [PostId]) -> s)
forall s i o. System (->) s (Mono i o) -> s -> (o, i -> s)
System.runSystemMono Agent (->) s ([Post Name], [PostId]) [Post Name]
ag s
s) ([Post Name]
ins, [PostId]
ids)
      ([Post Name]
outs, ([Post Name], [PostId]) -> s
_) = Agent (->) s ([Post Name], [PostId]) [Post Name]
-> s -> ([Post Name], ([Post Name], [PostId]) -> s)
forall s i o. System (->) s (Mono i o) -> s -> (o, i -> s)
System.runSystemMono Agent (->) s ([Post Name], [PostId]) [Post Name]
ag s
s'
   in ([Post Name]
outs, s -> Agent (->) s ([Post Name], [PostId]) [Post Name] -> AgentBox
forall s.
s -> Agent (->) s ([Post Name], [PostId]) [Post Name] -> AgentBox
AgentBox s
s' Agent (->) s ([Post Name], [PostId]) [Post Name]
ag)

-- | Lift an agent that ignores ids into one that accepts the boxed
-- @(posts, ids)@ input.  This is the minimal adapter for existing agents
-- that do not need provenance.
withIds :: Agent (->) s [Post Text] [Post Text] -> Agent (->) s ([Post Text], [PostId]) [Post Text]
withIds :: forall s.
Agent (->) s [Post Name] [Post Name]
-> Agent (->) s ([Post Name], [PostId]) [Post Name]
withIds Agent (->) s [Post Name] [Post Name]
ag = ((s, Dir (Mono ([Post Name], [PostId]) [Post Name]))
 -> (s, Pos (Mono ([Post Name], [PostId]) [Post Name])))
-> System (->) s (Mono ([Post Name], [PostId]) [Post Name])
forall (arr :: * -> * -> *) s (p :: Poly).
arr (s, Dir p) (s, Pos p) -> System arr s p
system (((s, Dir (Mono ([Post Name], [PostId]) [Post Name]))
  -> (s, Pos (Mono ([Post Name], [PostId]) [Post Name])))
 -> System (->) s (Mono ([Post Name], [PostId]) [Post Name]))
-> ((s, Dir (Mono ([Post Name], [PostId]) [Post Name]))
    -> (s, Pos (Mono ([Post Name], [PostId]) [Post Name])))
-> System (->) s (Mono ([Post Name], [PostId]) [Post Name])
forall a b. (a -> b) -> a -> b
$ \(s
s, Dir (Mono ([Post Name], [PostId]) [Post Name])
d) ->
  let ([Post Name]
ins, [PostId]
_ids) = Dir (Mono ([Post Name], [PostId]) (ZonkAny 1))
-> ([Post Name], [PostId])
forall i o. Dir (Mono i o) -> i
monoDir Dir (Mono ([Post Name], [PostId]) [Post Name])
Dir (Mono ([Post Name], [PostId]) (ZonkAny 1))
d
   in Agent (->) s [Post Name] [Post Name]
-> (s, Dir (Mono [Post Name] [Post Name]))
   -> (s, Pos (Mono [Post Name] [Post Name]))
forall (arr :: * -> * -> *) s (p :: Poly).
System arr s p -> arr (s, Dir p) (s, Pos p)
runSystem Agent (->) s [Post Name] [Post Name]
ag (s
s, [Post Name] -> Dir (Mono [Post Name] (ZonkAny 2))
forall i o. i -> Dir (Mono i o)
monoIn [Post Name]
ins)

-- | A deterministic oracle agent: answers each batch with one honest
-- synthesis post ('synthesisPosts') whose body quotes what it saw.  @tag@
-- marks the "model" — swapping the box is swapping the tag.
--
-- Output depends only on the pre-input state (the Moore idiom of 'tape'):
-- the state carries the last batch and its ids seen, and the emit answers
-- it.
quoter :: Name -> Text -> Agent (->) ([Post Text], [PostId], [Post Text], [PostId]) ([Post Text], [PostId]) [Post Text]
quoter :: Name
-> Name
-> Agent
     (->)
     ([Post Name], [PostId], [Post Name], [PostId])
     ([Post Name], [PostId])
     [Post Name]
quoter Name
who Name
tag = ((([Post Name], [PostId], [Post Name], [PostId]),
  Dir (Mono ([Post Name], [PostId]) [Post Name]))
 -> (([Post Name], [PostId], [Post Name], [PostId]),
     Pos (Mono ([Post Name], [PostId]) [Post Name])))
-> Agent
     (->)
     ([Post Name], [PostId], [Post Name], [PostId])
     ([Post Name], [PostId])
     [Post Name]
forall (arr :: * -> * -> *) s (p :: Poly).
arr (s, Dir p) (s, Pos p) -> System arr s p
system (((([Post Name], [PostId], [Post Name], [PostId]),
   Dir (Mono ([Post Name], [PostId]) [Post Name]))
  -> (([Post Name], [PostId], [Post Name], [PostId]),
      Pos (Mono ([Post Name], [PostId]) [Post Name])))
 -> Agent
      (->)
      ([Post Name], [PostId], [Post Name], [PostId])
      ([Post Name], [PostId])
      [Post Name])
-> ((([Post Name], [PostId], [Post Name], [PostId]),
     Dir (Mono ([Post Name], [PostId]) [Post Name]))
    -> (([Post Name], [PostId], [Post Name], [PostId]),
        Pos (Mono ([Post Name], [PostId]) [Post Name])))
-> Agent
     (->)
     ([Post Name], [PostId], [Post Name], [PostId])
     ([Post Name], [PostId])
     [Post Name]
forall a b. (a -> b) -> a -> b
$ \(([Post Name]
hist, [PostId]
histIds, [Post Name]
batch, [PostId]
batchIds), Dir (Mono ([Post Name], [PostId]) [Post Name])
d) ->
  let ([Post Name]
ins, [PostId]
insIds) = Dir (Mono ([Post Name], [PostId]) (ZonkAny 0))
-> ([Post Name], [PostId])
forall i o. Dir (Mono i o) -> i
monoDir Dir (Mono ([Post Name], [PostId]) [Post Name])
Dir (Mono ([Post Name], [PostId]) (ZonkAny 0))
d
      out :: [Post Name]
out = case [Post Name]
batch of
        [] -> []
        [Post Name]
_ -> Name -> [Post Name] -> [PostId] -> Name -> [Post Name]
synthesisPosts Name
who [Post Name]
batch [PostId]
batchIds (Name
tag Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
" saw " Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> String -> Name
T.pack ([Name] -> String
forall a. Show a => a -> String
show ((Post Name -> Name) -> [Post Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Post Name -> Name
forall a. Post a -> Name
from [Post Name]
batch)))
   in (([Post Name] -> [Post Name]
forall a. [a] -> [a]
reverse [Post Name]
ins [Post Name] -> [Post Name] -> [Post Name]
forall a. [a] -> [a] -> [a]
++ [Post Name]
hist, [PostId] -> [PostId]
forall a. [a] -> [a]
reverse [PostId]
insIds [PostId] -> [PostId] -> [PostId]
forall a. [a] -> [a] -> [a]
++ [PostId]
histIds, [Post Name]
ins, [PostId]
insIds), ([Post Name]
out, ()))

-- | Run @n@ rounds over a roster.  Every box sees the previous round's
-- concatenated outputs (round 1 sees the seed).  Returns the rounds.
meet :: Int -> [AgentBox] -> [Post Text] -> [[Post Text]]
meet :: Int -> [AgentBox] -> [Post Name] -> [[Post Name]]
meet Int
n [AgentBox]
boxes [Post Name]
seed = ([(PostId, Post Name)] -> [Post Name])
-> [[(PostId, Post Name)]] -> [[Post Name]]
forall a b. (a -> b) -> [a] -> [b]
map (((PostId, Post Name) -> Post Name)
-> [(PostId, Post Name)] -> [Post Name]
forall a b. (a -> b) -> [a] -> [b]
map (PostId, Post Name) -> Post Name
forall a b. (a, b) -> b
snd) [[(PostId, Post Name)]]
rounds
  where
    ([[(PostId, Post Name)]]
rounds, [AgentBox]
_) = Int
-> [AgentBox]
-> [(PostId, Post Name)]
-> PostId
-> ([[(PostId, Post Name)]], [AgentBox])
meetWithIds Int
n [AgentBox]
boxes ([PostId] -> [Post Name] -> [(PostId, Post Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [PostId
0 ..] [Post Name]
seed) (Int -> PostId
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([Post Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Post Name]
seed))

-- | Internal driver that threads positional ids through the rounds.
meetWithIds :: Int -> [AgentBox] -> [(PostId, Post Text)] -> PostId -> ([[(PostId, Post Text)]], [AgentBox])
meetWithIds :: Int
-> [AgentBox]
-> [(PostId, Post Name)]
-> PostId
-> ([[(PostId, Post Name)]], [AgentBox])
meetWithIds Int
0 [AgentBox]
boxes [(PostId, Post Name)]
_ PostId
_ = ([], [AgentBox]
boxes)
meetWithIds Int
k [AgentBox]
boxes [(PostId, Post Name)]
ins PostId
nextId =
  let ([Post Name]
outs, [AgentBox]
boxes') = [AgentBox] -> [Post Name] -> [PostId] -> ([Post Name], [AgentBox])
runRound [AgentBox]
boxes (((PostId, Post Name) -> Post Name)
-> [(PostId, Post Name)] -> [Post Name]
forall a b. (a -> b) -> [a] -> [b]
map (PostId, Post Name) -> Post Name
forall a b. (a, b) -> b
snd [(PostId, Post Name)]
ins) (((PostId, Post Name) -> PostId)
-> [(PostId, Post Name)] -> [PostId]
forall a b. (a -> b) -> [a] -> [b]
map (PostId, Post Name) -> PostId
forall a b. (a, b) -> a
fst [(PostId, Post Name)]
ins)
      n :: Int
n = [Post Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Post Name]
outs
      outIds :: [PostId]
outIds = Int -> [PostId] -> [PostId]
forall a. Int -> [a] -> [a]
take Int
n [PostId
nextId ..]
      stamped :: [(PostId, Post Name)]
stamped = [PostId] -> [Post Name] -> [(PostId, Post Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [PostId]
outIds [Post Name]
outs
      ([[(PostId, Post Name)]]
rest, [AgentBox]
boxes'') = Int
-> [AgentBox]
-> [(PostId, Post Name)]
-> PostId
-> ([[(PostId, Post Name)]], [AgentBox])
meetWithIds (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [AgentBox]
boxes' [(PostId, Post Name)]
stamped (PostId
nextId PostId -> PostId -> PostId
forall a. Num a => a -> a -> a
+ Int -> PostId
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n)
   in ([(PostId, Post Name)]
stamped [(PostId, Post Name)]
-> [[(PostId, Post Name)]] -> [[(PostId, Post Name)]]
forall a. a -> [a] -> [a]
: [[(PostId, Post Name)]]
rest, [AgentBox]
boxes'')

-- | One round: every box sees the same batch; outputs concatenate in
-- roster order.
runRound :: [AgentBox] -> [Post Text] -> [PostId] -> ([Post Text], [AgentBox])
runRound :: [AgentBox] -> [Post Name] -> [PostId] -> ([Post Name], [AgentBox])
runRound [AgentBox]
boxes [Post Name]
ins [PostId]
ids =
  let results :: [([Post Name], AgentBox)]
results = (AgentBox -> ([Post Name], AgentBox))
-> [AgentBox] -> [([Post Name], AgentBox)]
forall a b. (a -> b) -> [a] -> [b]
map (\AgentBox
b -> AgentBox -> [Post Name] -> [PostId] -> ([Post Name], AgentBox)
runAgentBox AgentBox
b [Post Name]
ins [PostId]
ids) [AgentBox]
boxes
   in ((([Post Name], AgentBox) -> [Post Name])
-> [([Post Name], AgentBox)] -> [Post Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Post Name], AgentBox) -> [Post Name]
forall a b. (a, b) -> a
fst [([Post Name], AgentBox)]
results, (([Post Name], AgentBox) -> AgentBox)
-> [([Post Name], AgentBox)] -> [AgentBox]
forall a b. (a -> b) -> [a] -> [b]
map ([Post Name], AgentBox) -> AgentBox
forall a b. (a, b) -> b
snd [([Post Name], AgentBox)]
results)

-- | The full log of a meeting: seed followed by the rounds, oldest first.
-- Ids are assigned positionally by the driver, so 'thread' fields in the
-- returned posts are valid ids against this log ('indexToIdMap' reproduces
-- the same assignment).
meetLog :: Int -> [AgentBox] -> [Post Text] -> [Post Text]
meetLog :: Int -> [AgentBox] -> [Post Name] -> [Post Name]
meetLog Int
n [AgentBox]
boxes [Post Name]
seed = [Post Name]
seed [Post Name] -> [Post Name] -> [Post Name]
forall a. [a] -> [a] -> [a]
++ [[Post Name]] -> [Post Name]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Int -> [AgentBox] -> [Post Name] -> [[Post Name]]
meet Int
n [AgentBox]
boxes [Post Name]
seed)

-- | The posts of a log whose ancestry cone avoids the given names — the
-- subtrees a swap of those names cannot touch.
unchanged :: [Name] -> [Post Text] -> [Post Text]
unchanged :: [Name] -> [Post Name] -> [Post Name]
unchanged [Name]
banned [Post Name]
posts =
  [ Post Name
p
  | ([Post Name]
prior, Post Name
p) <- [[Post Name]] -> [Post Name] -> [([Post Name], Post Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([Post Name] -> [[Post Name]]
forall a. [a] -> [[a]]
inits [Post Name]
posts) [Post Name]
posts,
    [Name] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Post Name] -> Post Name -> [Name]
forall a. [Post a] -> Post a -> [Name]
coneByIndex [Post Name]
prior Post Name
p [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [Name]
banned)
  ]