Acceptor.hs

-- | First-class projections of a 'SymTransducer' onto one alphabet
-- at a time.
--
-- The foundations chapter
-- @docs/foundations/04-projections-and-deriving-event-sourcing.md@
-- spells out the central insight that any FST has two acceptor
-- projections:
--
-- * The /input projection/ π₁ — drop the events. The remaining
--   transition function is an acceptor over commands. Its language
--   is the set of command sequences the aggregate accepts.
-- * The /output projection/ π₂ — drop the commands by inverting ω.
--   The remaining transition function is @evolve@ (the
--   event-language acceptor). Its language is the set of event
--   sequences the aggregate could have produced — the set of
--   replayable logs.
--
-- In 'Keiki.Core' these projections are /implicit/: π₁ is
-- 'Keiki.Core.delta'; π₂ is 'Keiki.Core.applyEventStreaming'. This module
-- /names/ them as a first-class data type so downstream code (UI,
-- validation, generated documentation) can pattern-match on a known
-- shape instead of plumbing the step functions by hand.
--
-- == Quick reference
--
-- @
-- accepts (inputAcceptor t)  cmds   :: Bool   -- "is this command sequence in the input language?"
-- accepts (outputAcceptor t) events :: Bool   -- "is this event sequence in the output language?"
-- @
--
-- See @docs/research/acceptor-projections-design.md@ for the design
-- record and relationship to Core replay.
module Keiki.Acceptor
  ( -- * The acceptor projection
    Acceptor (..),

    -- * Projecting a transducer
    inputAcceptor,
    outputAcceptor,

    -- * Folding helpers
    runAcceptor,
    accepts,
  )
where

import Keiki.Core
  ( BoolAlg,
    InFlight (..),
    RegFile,
    SymTransducer (..),
    applyEventStreaming,
    delta,
  )

-- | A minimal acceptor over alphabet @a@ with state carrier @s@.
--
-- The three fields are the membership question reduced to its
-- essence:
--
-- * @aStep@ — single-step transition. 'Just' on a successful step;
--   'Nothing' to reject (the absence of a transition /is/ rejection).
-- * @aInitial@ — the start state.
-- * @aIsFinal@ — final-state predicate. A run accepts iff it
--   terminates in a state for which this predicate holds.
--
-- The richer return type of 'Keiki.Core.delta' /
-- 'Keiki.Core.applyEventStreaming' (which thread an updated 'RegFile') is
-- preserved by the projections in this module by hiding the register
-- file inside @s@; see 'inputAcceptor' / 'outputAcceptor'.
--
-- 'Acceptor' carries closures and therefore has no 'Show' or 'Eq'
-- instance; assert on 'runAcceptor' or 'accepts' results instead.
data Acceptor a s = Acceptor
  { aStep :: s -> a -> Maybe s,
    aInitial :: s,
    aIsFinal :: s -> Bool
  }

-- | Project a 'SymTransducer' to its /input/ acceptor (π₁): the
-- acceptor over the command alphabet whose step is
-- 'Keiki.Core.delta'.
--
-- The state carrier is @(s, 'RegFile' rs)@ because edge guards
-- depend on the register file as well as the control vertex.
-- 'aIsFinal' ignores the register file and consults
-- @'isFinal' t@.
--
-- @
-- accepts (inputAcceptor t) cmds  ==  True
-- @
--
-- iff successively applying 'Keiki.Core.delta' to each command
-- reaches a final control vertex. A command sequence is rejected
-- (returns 'False') as soon as any step finds zero or multiple
-- satisfied outgoing edges.
inputAcceptor ::
  (BoolAlg phi (RegFile rs, ci)) =>
  SymTransducer phi rs s ci co ->
  Acceptor ci (s, RegFile rs)
inputAcceptor t =
  Acceptor
    { aStep = \(s, regs) ci -> delta t s regs ci,
      aInitial = (initial t, initialRegs t),
      aIsFinal = \(s, _regs) -> isFinal t s
    }

-- | Project a 'SymTransducer' to its /output/ acceptor (π₂): the
-- acceptor over the event alphabet whose step is
-- 'Keiki.Core.applyEventStreaming'.
--
-- The state carrier is @('Keiki.Core.InFlight' s co, 'RegFile' rs)@
-- because streaming replay must remember the expected tail of a
-- multi-event output chain as well as the register file.
--
-- @
-- accepts (outputAcceptor t) events  ==  True
-- @
--
-- is equivalent to:
--
-- @
-- case 'Keiki.Core.reconstitute' t events of
--   Just (s, _) -> 'isFinal' t s
--   Nothing     -> False
-- @
--
-- A log rejects when an event cannot replay or when the log ends in
-- the middle of a multi-event chain, leaving a non-final 'InFlight'
-- carrier.
outputAcceptor ::
  (BoolAlg phi (RegFile rs, ci), Eq co) =>
  SymTransducer phi rs s ci co ->
  Acceptor co (InFlight s co, RegFile rs)
outputAcceptor t =
  Acceptor
    { aStep = \(wrapper, regs) co ->
        applyEventStreaming t wrapper regs co,
      aInitial = (Settled (initial t), initialRegs t),
      aIsFinal = \(wrapper, _regs) -> case wrapper of
        Settled s -> isFinal t s
        InFlight {} -> False
    }

-- | Run an 'Acceptor' over a sequence. Returns 'Just' the terminal
-- state if every step succeeds, 'Nothing' on the first step that
-- rejects.
--
-- @runAcceptor a@ is @'foldlM' ('aStep' a) ('aInitial' a)@ written
-- longhand; the loose form keeps the import surface minimal and the
-- haddock close to the operational semantics.
runAcceptor :: Acceptor a s -> [a] -> Maybe s
runAcceptor a = go (aInitial a)
  where
    go s [] = Just s
    go s (x : xs) = aStep a s x >>= \s' -> go s' xs

-- | Decide membership: 'True' iff the input is accepted (every step
-- succeeds and the terminal state is final).
--
-- @
-- accepts a xs == case runAcceptor a xs of
--   Just s  -> aIsFinal a s
--   Nothing -> False
-- @
accepts :: Acceptor a s -> [a] -> Bool
accepts a xs = case runAcceptor a xs of
  Just s -> aIsFinal a s
  Nothing -> False