-- | Derivations: the 2-cells where the two dimensions meet (stage 6 of
-- endgame-path).
--
-- A derivation is a square: the horizontal edge is the agent box (the
-- sender — process dimension); the vertical edges are the ancestry,
-- resolved to strictly-earlier posts (record dimension).  With honest
-- ancestry ('synthesisPosts', stage 4) the square is /recoverable from
-- the log alone/ — the record projects the derivation, which is the
-- unification claim of the endgame.
--
-- Pasting:
--
--   * /horizontal/ — merging two boxes ('both') pastes their squares side
--     by side: the merged box derives the same log as the two boxes in a
--     roster.  Oracle: @meetLog n [both a b] seed == meetLog n [a, b] seed@.
--
--   * /vertical/ — stacking squares in time: chasing resolved parents
--     from any post walks the pasting back to the roots.  Oracle: the
--     chase from the last post of a meeting covers the whole log.
module Free.Agent.Derivation
  ( Derivation (..),
    derivation,
    valid,
    chaseLog,
  )
where

import Circuit.Agent (Post (..))
import Data.List (genericIndex)

-- | A derivation square: @dPost@ is the output (the square's target);
-- @dParents@ are the resolved vertical sources, in 'thread' order.
-- Dangling ids are an error (the log is expected to be well-formed).
data Derivation a = Derivation
  { forall a. Derivation a -> Post a
dPost :: Post a,
    forall a. Derivation a -> [Post a]
dParents :: [Post 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)

-- | The square of a post against the posts prior to it (oldest first).
-- Each 'thread' edge is a 'PostId' interpreted as a positional index into
-- @prior@, exactly as in 'Circuit.Agent.branches'.
derivation :: [Post a] -> Post a -> Derivation a
derivation :: forall a. [Post a] -> Post a -> Derivation a
derivation [Post a]
prior Post a
p =
  Post a -> [Post a] -> Derivation a
forall a. Post a -> [Post a] -> Derivation a
Derivation
    Post a
p
    [ [Post a]
prior [Post a] -> PostId -> Post a
forall i a. Integral i => [a] -> i -> a
`genericIndex` PostId
i
    | PostId
i <- Post a -> [PostId]
forall a. Post a -> [PostId]
thread Post a
p
    ]

-- | A square is valid when every vertical edge resolves to a
-- strictly-earlier post — no dangling ancestry.
valid :: [Post a] -> Post a -> Bool
valid :: forall a. [Post a] -> Post a -> Bool
valid [Post a]
prior Post a
p = (PostId -> Bool) -> [PostId] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (PostId -> PostId -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> PostId
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([Post a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Post a]
prior)) (Post a -> [PostId]
forall a. Post a -> [PostId]
thread Post a
p)

-- | The posts reachable from the last post by chasing derivations back
-- through the log (vertical pasting made executable).  When ancestry is
-- honest and the log is one meeting, the chase covers the whole log.
--
-- Posts are compared by value; duplicate posts collapse (bag at the wire,
-- but the chase is a set walk).
chaseLog :: (Eq a) => [Post a] -> [Post a]
chaseLog :: forall a. Eq a => [Post a] -> [Post a]
chaseLog [] = []
chaseLog [Post a]
posts = [Post a] -> [Post a] -> [Post a]
go [] [[Post a] -> Post a
forall a. HasCallStack => [a] -> a
last [Post a]
posts]
  where
    priorOf :: Post a -> [Post a]
priorOf Post a
p = (Post a -> Bool) -> [Post a] -> [Post a]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Post a -> Post a -> Bool
forall a. Eq a => a -> a -> Bool
/= Post a
p) [Post a]
posts
    go :: [Post a] -> [Post a] -> [Post a]
go [Post a]
acc [] = [Post a]
acc
    go [Post a]
acc (Post a
p : [Post a]
ps)
      | Post a
p Post a -> [Post a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Post a]
acc = [Post a] -> [Post a] -> [Post a]
go [Post a]
acc [Post a]
ps
      | Bool
otherwise = [Post a] -> [Post a] -> [Post a]
go (Post a
p Post a -> [Post a] -> [Post a]
forall a. a -> [a] -> [a]
: [Post a]
acc) (Derivation a -> [Post a]
forall a. Derivation a -> [Post a]
dParents ([Post a] -> Post a -> Derivation a
forall a. [Post a] -> Post a -> Derivation a
derivation (Post a -> [Post a]
priorOf Post a
p) Post a
p) [Post a] -> [Post a] -> [Post a]
forall a. [a] -> [a] -> [a]
++ [Post a]
ps)