Builder.hs

-- 'Disjoint' on '(.=)' is the static check itself; GHC otherwise warns.
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- | A monadic edge-builder DSL for authoring 'SymTransducer's. The
-- builder is purely additive on top of "Keiki.Core": every edge it
-- produces is a value of the existing 'Keiki.Core.Edge' type, and
-- the resulting 'Keiki.Core.SymTransducer' is consumed unchanged by
-- "Keiki.Acceptor", "Keiki.Composition",
-- "Keiki.Symbolic", and the example-side specs.
--
-- == Why a builder
--
-- A hand-written transducer in the AST surface needs four nested
-- pieces of boilerplate per edge: the 'Edge' record literal, an
-- @'IndexN' \"name\" Regs T@ annotation on every register write, an
-- infix @\`combine\`@ chain stitching the writes together, and an
-- @'OFCons' … 'OFNil'@ chain (plus a 'pack' prefix and a 'Just'
-- wrapper) describing the output. The builder collapses each piece:
--
--   * 'buildTransducer' assembles a 'SymTransducer' from a
--     'VertexBuilder' and three scalar arguments (initial vertex,
--     initial register file, finality predicate).
--   * 'from' tags one source vertex; 'onCmd' / 'onEpsilon' add one
--     edge each.
--   * '(.=)' adds one register write to the edge under construction.
--     The slot name flows through a type-level @(w :: [Symbol])@
--     index so that a duplicated @'(.=)'@ to the same slot fails to
--     type-check at the offending line.
--   * 'emit' takes a 'WireCtor' and a per-event
--     @\<CtorName\>TermFields rs ci@ record (emitted by
--     'Keiki.Generics.TH.deriveWireCtors'); fields read top-to-
--     bottom keyed by the wire side's payload field names. The
--     'InCtor' is recovered from the enclosing 'onCmd'; the lower-
--     level operator-form @(t1 *: t2 *: oNil)@ remains available
--     as an escape hatch via the same overload.
--
-- See @docs\/research\/edge-builder-dsl-shape.md@ for the full
-- design and per-question rationale (carrier monad,
-- distinct-targets enforcement, 'goto' termination semantics, etc).
--
-- == Worked example: the EmailDelivery aggregate
--
-- @
-- import qualified Keiki.Builder as B
-- import Keiki.Builder        ((.=))
-- import qualified Prelude
--
-- emailDelivery
--   :: 'Keiki.Core.SymTransducer' ('Keiki.Core.HsPred' EmailRegs EmailCmd)
--                                  EmailRegs EmailVertex
--                                  EmailCmd EmailEvent
-- emailDelivery = B.'buildTransducer' EmailPending emptyEmailRegs
--                   (\\case EmailSentVertex -> True; _ -> False)
--                   $ Prelude.do        -- VertexBuilder is a plain Monad
--
--     B.'from' EmailPending Prelude.do  -- EdgeListBuilder is plain
--       B.'onCmd' inCtorSendEmail $ \\d -> B.do  -- EdgeBuilder is indexed
--         B.'slot' \@\"emailRecipient\" .= d.recipient
--         B.'slot' \@\"emailSubject\"   .= d.subject
--         B.'slot' \@\"emailSentAt\"    .= d.at
--         B.'emit' wireEmailSent EmailSentTermFields
--           { recipient = d.recipient
--           , subject   = d.subject
--           , at        = d.at
--           }
--         B.'goto' EmailSentVertex
--
--     B.'from' EmailSentVertex (Prelude.pure ())  -- terminal
-- @
--
-- The user's aggregate module needs three pragmas / imports:
--
--   * @{-\# LANGUAGE QualifiedDo \#-}@ — so @B.do@ resolves to this
--     module's indexed bind.
--   * @{-\# LANGUAGE BlockArguments \#-}@ — so a @B.do@ block can
--     appear as a function argument without parentheses.
--   * @import qualified Keiki.Builder as B@ /and/
--     @import Keiki.Builder ((.=))@ — the operator must be in scope
--     unqualified; @B.(.=)@ is unreadable.
--
-- The @\<CtorName\>TermFields@ record (e.g. @EmailSentTermFields@)
-- is generated by 'Keiki.Generics.TH.deriveWireCtors' alongside the
-- existing @wire\<CtorName\>@ value. For ad-hoc cases that do not
-- correspond to a single event ctor, the lower-level operator sugar
-- '(*:)' / 'oNil' (re-exports of 'Keiki.Core.OFCons' /
-- 'Keiki.Core.OFNil') builds the 'OutFields' HList directly:
--
-- @
-- B.'emit' wireEmailSent (d.recipient *: d.subject *: d.at *: B.'oNil')
-- @
--
-- Both shapes resolve through the 'ToOutFields' typeclass; both
-- produce the same 'Keiki.Core.OPack' AST node.
--
-- == Three-layer monad shape
--
-- Three carriers, only the innermost is indexed:
--
--   1. 'VertexBuilder' (plain 'Monad') — the top-level. State is
--      a list @[(v, [Edge ...])]@; 'from' writes one entry.
--   2. 'EdgeListBuilder' (plain 'Monad') — the per-source-vertex
--      layer. State is the list of edges out of that vertex;
--      'onCmd' \/ 'onEpsilon' each prepend one.
--   3. 'EdgeBuilder' (indexed) — the per-edge body. Type-level
--      @(w :: [Symbol])@ tracks the slots written so far; '(.=)'
--      extends @w@ and inherits a 'Disjoint'-driven static check.
--
-- The 'QualifiedDo' machinery only re-binds @(>>=)@/@(>>)@ for the
-- innermost layer; the outer two use 'Prelude.do'.
--
-- == Misuse diagnostics
--
-- * Duplicate '(.=)' to the same slot: caught at compile time via
--   the 'Keiki.Internal.Slots.Disjoint' 'GHC.TypeError.TypeError',
--   which names the duplicated slot.
--
-- * Duplicate names in the register file: caught at compile time by
--   the 'Keiki.Internal.Slots.DistinctNames' constraint on the two
--   build entry points.
--
-- * An 'emit' whose term-fields schema differs from its enclosing
--   'onCmd', or an 'emit' inside 'onEpsilon': caught at compile time.
--
-- * Missing or multiple 'goto's: every declared edge is checked when
--   the transducer returned by 'buildTransducer' is first evaluated,
--   even if its source vertex is never inspected. All defects are
--   reported together with source vertices and edge indices. Use
--   'buildTransducerEither' to receive them as structured values.
--
-- * An 'emitWith' inside 'onCmd' whose explicit input constructor
--   differs in name or slot names from the enclosing constructor:
--   rejected by the same eager validation pass.
--
-- * An edge with neither 'emit' / 'emitWith' nor 'noEmit': rejected
--   by eager validation with a located structured defect directing
--   the user to declare whether the edge emits or is deliberately
--   silent.
--
-- == When to drop down to the AST
--
-- Use the AST directly when:
--
--   * The aggregate has bespoke guard logic the builder does not
--     express (a hand-built 'HsPred' tree the builder cannot
--     accumulate via 'requireEq' / 'requireGuard').
--   * The aggregate composes 'Edge' values from helper functions
--     defined elsewhere (the builder is meant to /author/ edges, not
--     to be a pluggable assembly tool).
--
-- Both directions can coexist in one module: the builder produces
-- @'SymTransducer'@s of the same type the AST does, and
-- "Keiki.Composition" 'Keiki.Composition.compose' takes the
-- builder-produced values without modification.
module Keiki.Builder
  ( -- * Top-level entry point
    buildTransducer,
    buildTransducerEither,
    BuilderDefect (..),
    BuilderError (..),
    renderBuilderErrors,

    -- * Vertex-level builder
    VertexBuilder,
    from,

    -- * Edge-list builder (per source vertex)
    EdgeListBuilder,
    onCmd,
    onEpsilon,

    -- * Edge body builder (per outgoing transition)
    EdgeBuilder,

    -- ** Slot writes
    slot,
    (.=),
    (=:),
    reg,

    -- ** Outputs
    emit,
    emitWith,
    noEmit,

    -- ** Output-fields HList sugar
    (*:),
    oNil,

    -- ** Field-keyed record sugar
    ToOutFields (..),

    -- ** Guards
    requireEq,
    requireGuard,
    Cmp (..),
    requireCmp,
    requireLt,
    requireLe,
    requireGt,
    requireGe,

    -- ** Termination
    goto,

    -- ** Payload projection (OverloadedRecordDot)
    PayloadProj,

    -- * QualifiedDo bind/return exports
    -- $qualifiedDo
    (>>=),
    (>>),
    pure,
    return,
  )
where

import Data.List (intercalate)
import Data.List.NonEmpty (NonEmpty)
import Data.List.NonEmpty qualified as NonEmpty
import Data.Typeable (Typeable)
import GHC.Records (HasField (..))
import GHC.TypeLits (KnownSymbol, Symbol)
import Keiki.Core
  ( Cmp (..),
    Edge (..),
    HsPred (..),
    InCtor (..),
    Index,
    OutFields (..),
    OutTerm (..),
    RegFile,
    Slot,
    SymTransducer (..),
    Term (TReg),
    Update (..),
    WireCtor,
    combine,
    inpCtor,
    matchInCtor,
    oNil,
    pack,
    slotNamesOf,
    (*:),
  )
import Keiki.Core qualified as K
import Keiki.Internal.Slots
  ( Concat,
    Disjoint,
    DistinctNames,
    HasIndexN (..),
    IndexN (..),
    Names,
  )
import Prelude hiding (pure, return, (>>), (>>=))
import Prelude qualified

-- $qualifiedDo
--
-- @QualifiedDo@ desugars @B.do { … }@ to @B.>>=@, @B.>>@, @B.pure@,
-- @B.return@. These exports are the indexed analogues that thread
-- the type-level slot-set through every edge-body step. They are
-- not the right operators for the outer 'VertexBuilder' /
-- 'EdgeListBuilder' layers — those use the regular 'Prelude.do'
-- syntax with the 'Monad' instances declared below.

-- * The per-edge state ----------------------------------------------------

-- | The growing edge state inside an 'EdgeBuilder' body. Lifecycle:
-- 'onCmd' / 'onEpsilon' construct an initial 'PartialEdge' (with
-- 'PTop' or @'matchInCtor' ic@ as guard, 'UKeep' as update, no
-- output, no targets); each step in the body modifies one or more
-- fields; 'finalizeEdge' validates that exactly one 'goto' was
-- called and that output intent was declared, then packages the
-- result into a closed 'Edge'. The
-- existential @w@ on 'Edge''s 'update' field closes here.
data PartialEdge rs ci co v (pin :: Maybe [Slot]) (w :: [Symbol]) = PartialEdge
  { peGuard :: HsPred rs ci,
    peUpdate :: Update rs w ci,
    -- | Output terms accumulated by 'emit' / 'emitWith' calls in
    -- declaration order (snoc-appended). The empty list is an ε-edge
    -- (@output = []@ on the resulting 'Edge'); a single 'emit' yields
    -- a length-1 list (today's letter behaviour); two or more 'emit's
    -- in one body yield a multi-event edge (EP-19).
    peOutput :: [OutTerm rs ci co],
    -- | Reverse-order list of every 'goto' invocation in the body.
    -- Finalization requires exactly one element.
    peTargets :: [v],
    -- | The 'InCtor' bound by the enclosing 'onCmd', indexed by its
    -- real input-field schema. 'PinNone' marks an 'onEpsilon' body.
    pePinned :: Pinned ci pin,
    -- | Whether the body explicitly chose to emit or remain silent.
    -- Any 'emit', 'emitWith', or 'noEmit' call sets this to 'True'.
    peOutputDecided :: Bool
  }

-- | Whether an edge body has an enclosing input constructor. The
-- schema index preserves the equality that 'emit' needs.
data Pinned ci (pin :: Maybe [Slot]) where
  PinNone :: Pinned ci 'Nothing
  PinCtor :: InCtor ci ifs -> Pinned ci ('Just ifs)

-- | The per-edge indexed-state monad. The two phantom slot-set
-- indices @(w :: [Symbol])@ (before this step) and @(w' :: [Symbol])@
-- (after this step) make every '(.=)' visible to the type system,
-- so a duplicated @'(.=)'@ to the same slot fails at the offending
-- line via the 'Keiki.Internal.Slots.Disjoint' constraint that
-- 'Keiki.Core.combine' carries.
--
-- Functor / Applicative / Monad instances are not provided because
-- they would be 'IxFunctor' / 'IxApplicative' / 'IxMonad' (the
-- type-level slot-set changes between operand and result), which
-- requires a separate type-class hierarchy. Instead, this module
-- exports its own @(>>=)@ / @(>>)@ / 'pure' / 'return' for use
-- with @QualifiedDo@.
newtype EdgeBuilder rs ci co v (pin :: Maybe [Slot]) (w :: [Symbol]) (w' :: [Symbol]) a
  = EdgeBuilder
  { runEdgeBuilder ::
      PartialEdge rs ci co v pin w ->
      (a, PartialEdge rs ci co v pin w')
  }

-- * QualifiedDo bind/return exports ----------------------------------------

-- | Indexed bind. The @w@ index of the first argument flows through
-- the second argument's @w@ argument, and the second argument's @w'@
-- index becomes the result's @w'@. Re-export for @QualifiedDo@.
(>>=) ::
  EdgeBuilder rs ci co v pin w1 w2 a ->
  (a -> EdgeBuilder rs ci co v pin w2 w3 b) ->
  EdgeBuilder rs ci co v pin w1 w3 b
EdgeBuilder f >>= k = EdgeBuilder $ \pe ->
  let (a, pe1) = f pe
      EdgeBuilder g = k a
   in g pe1

infixl 1 >>=

-- | Sequence. Defined in terms of '(>>=)'.
(>>) ::
  EdgeBuilder rs ci co v pin w1 w2 a ->
  EdgeBuilder rs ci co v pin w2 w3 b ->
  EdgeBuilder rs ci co v pin w1 w3 b
m >> n = m Keiki.Builder.>>= \_ -> n

infixl 1 >>

-- | Embed a value. Slot-set unchanged.
pure :: a -> EdgeBuilder rs ci co v pin w w a
pure a = EdgeBuilder $ \pe -> (a, pe)

-- | Synonym for 'pure'. Re-exported for @QualifiedDo@.
return :: a -> EdgeBuilder rs ci co v pin w w a
return = Keiki.Builder.pure

-- * Slot writes ----------------------------------------------------------

-- | Lift a slot name (supplied via @TypeApplication@) to its
-- slot-name-tagged register index. Use with '(.=)':
--
-- > slot @"emailRecipient" .= d.recipient
--
-- == Why @slot \@\"name\"@ instead of @\#name@
--
-- The @\#name@ overloaded-label syntax tries to resolve
-- @IsLabel \"name\" (IndexN s rs r)@ against the instance head
-- @IsLabel s (IndexN s rs r)@. GHC will not commit to @s ~ \"name\"@
-- when @name@ is a quantified type variable in the enclosing
-- operator's signature (the pattern-side @s@ appears at two
-- positions in the constraint head; without an explicit annotation,
-- GHC defers commitment). 'slot' pins the symbol via TypeApplication
-- so the inference proceeds without ambiguity. Slot name still
-- appears once.
slot ::
  forall (name :: Symbol) rs r.
  (KnownSymbol name, HasIndexN name rs r) =>
  IndexN name rs r
slot = indexN @name @rs @r

-- | Read a register slot into a 'Keiki.Core.Term', the read-side
-- mirror of 'slot'. The slot name is supplied via @TypeApplication@,
-- so @reg \@\"appCreditScore\"@ needs no @:: 'Keiki.Core.Index' Regs
-- Ty@ annotation:
--
-- > approvalGuard = reg \@\"appCreditScore\" .>= lit 650
--
-- == When to use @reg \@\"name\"@ versus @\#name@
--
-- A bare overloaded label @\#name@ already resolves to a register-read
-- 'Keiki.Core.Term' through the @'GHC.OverloadedLabels.IsLabel' s
-- ('Keiki.Core.Term' rs ci r)@ instance, and is the lighter form
-- wherever GHC can infer the slot list @rs@ and value type @r@ — for
-- example the right-hand side of '(.=)', or an argument of
-- 'Keiki.Core.TApp1'. In positions where inference fails — notably a
-- hand-written guard conjunction, or an 'OutFields' element — @\#name@
-- needs the verbose @'Keiki.Core.proj' (\#name :: 'Keiki.Core.Index'
-- Regs Ty)@ annotation. 'reg' removes exactly that annotation by
-- pinning the name with a type application, the same way 'slot' does on
-- the write side. A consumer whose prelude re-exports @generic-lens@
-- (which ships its own @IsLabel@ instance that shadows keiki's) loses
-- the bare-@\#name@ read path entirely; because 'reg' goes through a
-- type application rather than an overloaded label, it is unaffected.
reg ::
  forall (name :: Symbol) rs ci ifs r.
  (KnownSymbol name, HasIndexN name rs r) =>
  Term rs ci ifs r
reg = TReg (indexNToIndex (indexN @name @rs @r))

-- | Slot assignment. The slot name is supplied by 'slot' (via
-- TypeApplication); the value is a 'Term'. The
-- @'Disjoint' '[name] w@ constraint inherits the type-level
-- distinct-targets check from 'Keiki.Core.combine': a duplicated
-- @'(.=)'@ to the same slot fails to type-check at the offending
-- line, with the existing 'Keiki.Internal.Slots.Disjoint'
-- 'GHC.TypeError.TypeError' naming the slot.
--
-- The RHS is a 'Term' (not a bare value); use
-- 'Keiki.Core.lit' / 'Keiki.Core.proj' / 'Keiki.Core.inpCtor' or
-- @d.fieldName@ via 'PayloadProj' to construct it.
(.=) ::
  forall name r rs ci ifs co v pin w.
  (KnownSymbol name, Disjoint '[name] w) =>
  IndexN name rs r ->
  Term rs ci ifs r ->
  EdgeBuilder rs ci co v pin w (Concat '[name] w) ()
ix .= t = EdgeBuilder $ \pe ->
  ((), pe {peUpdate = USet ix t `combine` peUpdate pe})

infixr 6 .=

-- | Slot assignment, an exact synonym for '(.=)': @slot \@\"x\" =: t@
-- is @slot \@\"x\" .= t@ and produces the identical 'Keiki.Core.Update'.
-- It exists for one reason — to dodge the name clash with
-- @Control.Lens.(.=)@. A module that authors edges /and/ imports
-- "Control.Lens" would otherwise need @import Control.Lens hiding
-- ((.=))@; with '(=:)' it can keep both imports unqualified and use
-- '(=:)' for slot writes. Modules that do not import "Control.Lens"
-- should keep using '(.=)', which matches the @.=@ spelling of @aeson@
-- \/ @lens@ \/ @mtl@. (A colon-prefixed @:=@ is not available: GHC
-- reserves operators beginning with a colon for data constructors, so a
-- value-level synonym must start with another symbol — hence @=:@.)
(=:) ::
  forall name r rs ci ifs co v pin w.
  (KnownSymbol name, Disjoint '[name] w) =>
  IndexN name rs r ->
  Term rs ci ifs r ->
  EdgeBuilder rs ci co v pin w (Concat '[name] w) ()
(=:) = (.=)

infixr 6 =:

-- * Termination -----------------------------------------------------------

-- | Set the edge's target vertex. Required exactly once per edge
-- body; missing or multiple 'goto's are reported by the eager
-- validation pass, with the source vertex and edge index.
goto :: v -> EdgeBuilder rs ci co v pin w w ()
goto v = EdgeBuilder $ \pe ->
  ((), pe {peTargets = v : peTargets pe})

-- * Outputs ---------------------------------------------------------------

-- | Emit an event. Takes the wire-side 'WireCtor' and an output
-- description that resolves to an 'OutFields' via 'ToOutFields' —
-- either a per-event @\<CtorName\>TermFields rs ci@ record (emitted
-- by 'Keiki.Generics.TH.deriveWireCtors') or a bare 'OutFields'
-- HList constructed with '(*:)' / 'oNil'. The input-side 'InCtor'
-- is recovered at its real schema from the enclosing 'onCmd'. An
-- 'emit' inside 'onEpsilon' is a compile error; use 'emitWith' there.
--
-- == Multi-event commands (EP-19)
--
-- Each 'emit' call snoc-appends one 'OutTerm' to the edge's output
-- list. A single 'emit' in the body produces a letter edge
-- (@output = [o]@); two or more 'emit's in the same body produce a
-- multi-event edge (@output = [o1, o2, ...]@) whose semantics is
-- documented at 'Keiki.Core.Edge'. The 'OutTerm's evaluate against
-- the same pre-transition @(regs, ci)@ snapshot; register updates
-- accumulated by '(.=)' apply once at the edge level, not per
-- emitted event.
emit ::
  forall co fs rs ci ifs v w rec.
  (ToOutFields rec rs ci ifs fs) =>
  WireCtor co fs ->
  rec ->
  EdgeBuilder rs ci co v ('Just ifs) w w ()
emit wc rec = EdgeBuilder $ \pe -> case pePinned pe of
  PinCtor ic ->
    ( (),
      pe
        { peOutput =
            peOutput pe
              ++ [pack ic wc (toOutFields rec)],
          peOutputDecided = True
        }
    )

-- | Emit an event with an explicit 'InCtor'. This is the output form
-- for 'onEpsilon' bodies, which have no pinned constructor. Inside
-- 'onCmd', the supplied constructor must have the same name and slot
-- names as the pinned constructor; 'buildTransducer' rejects a
-- mismatch eagerly because it would invert replay to another command.
-- The InCtor-less 'emit' is preferred inside 'onCmd'. Like 'emit',
-- accumulates into the edge's output list — multiple calls produce a
-- multi-event edge.
emitWith ::
  forall co fs rs ci v pin w ifs rec.
  (ToOutFields rec rs ci ifs fs) =>
  InCtor ci ifs ->
  WireCtor co fs ->
  rec ->
  EdgeBuilder rs ci co v pin w w ()
emitWith ic wc rec = EdgeBuilder $ \pe ->
  ( (),
    pe
      { peOutput = peOutput pe ++ [pack ic wc (toOutFields rec)],
        peOutputDecided = True
      }
  )

-- | Declare the edge deliberately silent (an ε-edge with
-- @output = []@). Every body that does not call 'emit' or 'emitWith'
-- must call 'noEmit'; otherwise eager builder validation rejects the
-- edge. Mixing 'noEmit' and 'emit' in one body is allowed, and the
-- emitted terms still populate the output list.
noEmit :: EdgeBuilder rs ci co v pin w w ()
noEmit = EdgeBuilder $ \pe -> ((), pe {peOutputDecided = True})

-- * Field-keyed record sugar ---------------------------------------------

-- | Convert a value of any type bearing the wire-side fields of an
-- event to the 'OutFields' HList that 'pack' (and therefore 'OPack')
-- consumes.
--
-- Two kinds of inhabitant matter:
--
--   * The TH-emitted per-event record type
--     @\<CtorName\>TermFields rs ci@ (one record per event ctor in
--     'Keiki.Generics.TH.deriveWireCtors''s spec list). Its fields
--     are 'Term'-typed mirrors of the payload's fields, so call
--     sites read top-to-bottom keyed by name.
--
--   * The bare 'OutFields' value built with '(*:)' \/ 'oNil', for
--     which the passthrough instance (id) makes the same 'B.emit'
--     overload accept the operator form unchanged.
--
-- The functional dependency @rec -> rs ci fs@ ensures a record type
-- uniquely determines all of @rs@, @ci@, and @fs@, so type
-- inference at call sites is local: GHC propagates them from the
-- record's type alone.
class ToOutFields rec rs ci ifs fs | rec -> rs ci ifs fs where
  toOutFields :: rec -> OutFields rs ci ifs fs

-- | Passthrough: a bare 'OutFields' is its own conversion. Lets
-- 'B.emit' accept either a per-event record or an
-- @(t1 *: t2 *: oNil)@ chain through the same overload.
instance ToOutFields (OutFields rs ci ifs fs) rs ci ifs fs where
  toOutFields = id

-- * Guards ----------------------------------------------------------------

-- | Conjoin an arbitrary 'HsPred' with the edge's existing guard.
-- Use this when the structural sugar of 'requireEq' is not enough
-- (e.g. for negated predicates, disjunctions, or guards constructed
-- by helper functions).
requireGuard :: HsPred rs ci -> EdgeBuilder rs ci co v pin w w ()
requireGuard p = EdgeBuilder $ \pe ->
  ((), pe {peGuard = PAnd (peGuard pe) p})

-- | Conjoin an equality predicate (@a '==' b@) with the edge's
-- existing guard.
requireEq ::
  (Eq r, Typeable r) =>
  Term rs ci ifs1 r ->
  Term rs ci ifs2 r ->
  EdgeBuilder rs ci co v pin w w ()
requireEq a b = requireGuard (PEq a b)

-- | Conjoin an ordering predicate (@a `op` b@ for the relation named
-- by 'Cmp') with the edge's existing guard. Unlike a threshold lifted
-- through 'Keiki.Core.TApp1'\/'TApp2', a 'PCmp' guard is structural and
-- visible to the SBV-backed analyses. The four direction-specific
-- conveniences 'requireLt'\/'requireLe'\/'requireGt'\/'requireGe' wrap
-- this with a fixed 'Cmp'.
requireCmp ::
  (Ord r, Typeable r) =>
  Cmp ->
  Term rs ci ifs1 r ->
  Term rs ci ifs2 r ->
  EdgeBuilder rs ci co v pin w w ()
requireCmp op a b = requireGuard (PCmp op a b)

-- | Require @a < b@. See 'requireCmp'.
requireLt,
  requireLe,
  requireGt,
  requireGe ::
    (Ord r, Typeable r) =>
    Term rs ci ifs1 r ->
    Term rs ci ifs2 r ->
    EdgeBuilder rs ci co v pin w w ()
requireLt = requireCmp CmpLt
requireLe = requireCmp CmpLe
requireGt = requireCmp CmpGt
requireGe = requireCmp CmpGe

-- * Payload projection ----------------------------------------------------

-- | An opaque wrapper around an 'InCtor' that lets the user project
-- the input symbol's fields via 'OverloadedRecordDot' inside an
-- 'onCmd' body. The 'HasField' instance translates @d.fieldName@ to
-- @inpCtor ic (indexN \@fieldName \@ifs \@r)@.
--
-- 'PayloadProj' has no record selectors of its own so the user's
-- @d.fieldName@ never collides with a built-in selector.
data PayloadProj rs ci ifs = PayloadProj (InCtor ci ifs)

-- | OverloadedRecordDot resolution: @d.fieldName@ on a 'PayloadProj'
-- builds a 'TInpCtorField' term that projects the named field of the
-- input symbol's payload.
instance
  (HasIndexN name ifs r) =>
  HasField name (PayloadProj rs ci ifs) (Term rs ci ifs r)
  where
  getField (PayloadProj ic) =
    inpCtor ic (indexNToIndex (indexN @name @ifs @r))

-- | Translate the slot-name-tagged 'IndexN' into the legacy
-- existentially-typed 'Index' that 'Keiki.Core.inpCtor' expects.
-- Both indices have the same runtime structure; the translation is
-- a structural recursion. (M3+ may widen 'inpCtor' to take 'IndexN'
-- directly; this helper keeps the spike's legacy bridge.)
indexNToIndex :: forall name rs r. IndexN name rs r -> Index rs r
indexNToIndex IZ = K.ZIdx
indexNToIndex (IS i) = K.SIdx (indexNToIndex i)

-- * Edge-list builder -----------------------------------------------------

-- | Per-source-vertex builder. Accumulates the list of outgoing
-- edges for the @from@-scope's vertex; each 'onCmd' / 'onEpsilon'
-- call prepends one edge (the list is reversed in 'from' before
-- storage so declaration order is preserved).
newtype EdgeListBuilder rs ci co v a = EdgeListBuilder
  { runEdgeListBuilder ::
      v ->
      [Either BuilderDefect (Edge (HsPred rs ci) rs ci co v)] ->
      (a, [Either BuilderDefect (Edge (HsPred rs ci) rs ci co v)])
  }

instance Functor (EdgeListBuilder rs ci co v) where
  fmap f (EdgeListBuilder k) = EdgeListBuilder $ \src acc ->
    let (a, acc') = k src acc in (f a, acc')

instance Applicative (EdgeListBuilder rs ci co v) where
  pure a = EdgeListBuilder $ \_ acc -> (a, acc)
  EdgeListBuilder kf <*> EdgeListBuilder ka = EdgeListBuilder $ \src acc ->
    let (f, acc1) = kf src acc
        (a, acc2) = ka src acc1
     in (f a, acc2)

instance Monad (EdgeListBuilder rs ci co v) where
  (>>=) (EdgeListBuilder k) f = EdgeListBuilder $ \src acc ->
    let (a, acc') = k src acc
        EdgeListBuilder k' = f a
     in k' src acc'

-- | Per-edge entry. Wires the InCtor's match-guard, gives the user
-- a 'PayloadProj' handle (so OverloadedRecordDot resolves
-- @d.field@), runs the body to accumulate the edge, and finalizes
-- into a closed 'Edge'.
onCmd ::
  forall ci ifs rs co v w.
  InCtor ci ifs ->
  (PayloadProj rs ci ifs -> EdgeBuilder rs ci co v ('Just ifs) '[] w ()) ->
  EdgeListBuilder rs ci co v ()
onCmd ic body = EdgeListBuilder $ \_src acc ->
  let initial =
        PartialEdge
          { peGuard = matchInCtor ic,
            peUpdate = UKeep,
            peOutput = [],
            peTargets = [],
            pePinned = PinCtor ic,
            peOutputDecided = False
          }
      (_, finalPE) = runEdgeBuilder (body (PayloadProj ic)) initial
      edge = finalizeEdge finalPE
   in ((), edge : acc)

-- | ε-edge entry: no input projection, no input-ctor match-guard.
-- The guard starts at 'PTop' (so any conjuncts the body adds via
-- 'requireEq' / 'requireGuard' constitute the full guard). Inside
-- the body, no 'PayloadProj' is supplied, so 'OverloadedRecordDot'
-- access to the input is unavailable; use 'Keiki.Core.inpCtor'
-- directly with an explicit 'InCtor' if needed.
onEpsilon ::
  forall rs ci co v w.
  EdgeBuilder rs ci co v 'Nothing '[] w () ->
  EdgeListBuilder rs ci co v ()
onEpsilon body = EdgeListBuilder $ \_src acc ->
  let initial =
        PartialEdge
          { peGuard = PTop,
            peUpdate = UKeep,
            peOutput = [],
            peTargets = [],
            pePinned = PinNone,
            peOutputDecided = False
          }
      (_, finalPE) = runEdgeBuilder body initial
      edge = finalizeEdge finalPE
   in ((), edge : acc)

-- | One structural problem found while closing a single edge body.
data BuilderDefect
  = -- | The body never called 'goto'.
    DefectMissingGoto
  | -- | The body called 'goto' more than once; carries the count.
    DefectMultipleGoto Int
  | -- | An output constructor contradicts the enclosing 'onCmd'.
    DefectOutputCtorMismatch String [String] String [String]
  | -- | The body neither emitted nor explicitly declared silence.
    DefectMissingOutputIntent
  deriving stock (Eq, Show)

-- | A defect located at a specific edge of a specific source vertex.
-- The edge index is assigned after duplicate-'from' merging.
data BuilderError v = BuilderError
  { beVertex :: v,
    beEdgeIndex :: Int,
    beDefect :: BuilderDefect
  }
  deriving stock (Eq, Show)

-- | Close a 'PartialEdge' into an 'Edge'. Validation: 'peTargets'
-- must have exactly one entry; missing or duplicated 'goto' calls are
-- returned structurally. A single-target edge must also declare output
-- intent with 'emit', 'emitWith', or 'noEmit'; otherwise finalization
-- returns 'DefectMissingOutputIntent'. 'buildTransducerEither' attaches location.
-- The 'peOutput' list (zero or more 'OutTerm's accumulated by
-- 'emit' / 'emitWith' calls) flows directly into the resulting
-- 'Edge.output' field.
finalizeEdge ::
  PartialEdge rs ci co v pin w ->
  Either BuilderDefect (Edge (HsPred rs ci) rs ci co v)
finalizeEdge pe = case peTargets pe of
  [t] -> case outputCtorMismatch (pePinned pe) (peOutput pe) of
    Just defect -> Left defect
    Nothing
      | not (peOutputDecided pe) -> Left DefectMissingOutputIntent
      | otherwise ->
          Right
            Edge
              { guard = peGuard pe,
                update = peUpdate pe,
                output = peOutput pe,
                target = t
              }
  [] -> Left DefectMissingGoto
  ts@(_ : _ : _) -> Left (DefectMultipleGoto (length ts))

outputCtorMismatch :: Pinned ci pin -> [OutTerm rs ci co] -> Maybe BuilderDefect
outputCtorMismatch PinNone _ = Nothing
outputCtorMismatch (PinCtor pinned) outputs = go outputs
  where
    expectedName = icName pinned
    expectedSlots = slotNamesOf pinned

    go [] = Nothing
    go (OPack actual _ _ : rest)
      | icName actual /= expectedName || slotNamesOf actual /= expectedSlots =
          Just
            ( DefectOutputCtorMismatch
                expectedName
                expectedSlots
                (icName actual)
                (slotNamesOf actual)
            )
      | otherwise = go rest

-- * Vertex builder --------------------------------------------------------

-- | Top-level builder. Accumulates @[(v, [Edge ...])]@ entries, one
-- per 'from' call. 'buildTransducer' converts the result into a
-- 'SymTransducer''s 'edgesOut' function via @lookup@ with @[]@ as
-- default for unmentioned vertices.
newtype VertexBuilder rs ci co v a = VertexBuilder
  { runVertexBuilder ::
      [(v, [Either BuilderDefect (Edge (HsPred rs ci) rs ci co v)])] ->
      (a, [(v, [Either BuilderDefect (Edge (HsPred rs ci) rs ci co v)])])
  }

instance Functor (VertexBuilder rs ci co v) where
  fmap f (VertexBuilder k) = VertexBuilder $ \vs ->
    let (a, vs') = k vs in (f a, vs')

instance Applicative (VertexBuilder rs ci co v) where
  pure a = VertexBuilder $ \vs -> (a, vs)
  VertexBuilder kf <*> VertexBuilder ka = VertexBuilder $ \vs ->
    let (f, vs1) = kf vs
        (a, vs2) = ka vs1
     in (f a, vs2)

instance Monad (VertexBuilder rs ci co v) where
  (>>=) (VertexBuilder k) f = VertexBuilder $ \vs ->
    let (a, vs') = k vs
        VertexBuilder k' = f a
     in k' vs'

-- | Group edges by source vertex. The argument is an
-- 'EdgeListBuilder' do-block of 'onCmd' / 'onEpsilon' calls; each
-- call adds one outgoing edge to the named vertex.
--
-- A vertex not mentioned in any 'from' block defaults to @[]@
-- (terminal). To assert "this vertex is terminal" explicitly,
-- write @from V (Prelude.pure ())@.
from ::
  v ->
  EdgeListBuilder rs ci co v () ->
  VertexBuilder rs ci co v ()
from v eb = VertexBuilder $ \vs ->
  let (_, accFinal) = runEdgeListBuilder eb v []
      entry = (v, Prelude.reverse accFinal)
   in ((), entry : vs)

-- | Top-level entry. Run the 'VertexBuilder' do-block to produce a
-- list of @(vertex, edges)@ pairs, then assemble a 'SymTransducer'
-- from the initial vertex, initial register file, finality
-- predicate, and a closure over the lookup table.
--
-- Duplicate-vertex entries (which can arise when two 'from' blocks
-- accidentally declare the same vertex) are merged: 'edgesOut'
-- returns the concatenation of every entry's edges in declaration
-- order.
--
-- Every declared edge is validated before the result is returned.
-- Forcing the returned transducer to weak head normal form therefore
-- reports malformed edges even when their source vertices are never
-- otherwise inspected. Use 'buildTransducerEither' for structured
-- diagnostics instead of an exception.
buildTransducer ::
  forall rs ci co v.
  (DistinctNames (Names rs), Eq v, Show v) =>
  v ->
  RegFile rs ->
  (v -> Bool) ->
  VertexBuilder rs ci co v () ->
  SymTransducer (HsPred rs ci) rs v ci co
buildTransducer initS initR isF vb =
  case buildTransducerEither initS initR isF vb of
    Left errs -> error (renderBuilderErrors errs)
    Right tr -> tr

-- | Validating entry point. Runs the complete 'VertexBuilder', merges
-- duplicate vertices in declaration order, assigns stable per-vertex
-- edge indices, and returns every structural defect found.
buildTransducerEither ::
  forall rs ci co v.
  (DistinctNames (Names rs), Eq v) =>
  v ->
  RegFile rs ->
  (v -> Bool) ->
  VertexBuilder rs ci co v () ->
  Either
    (NonEmpty (BuilderError v))
    (SymTransducer (HsPred rs ci) rs v ci co)
buildTransducerEither initS initR isF vb =
  forceBuilderErrors errors `seq`
    forceEdgeTable cleanTable `seq`
      case NonEmpty.nonEmpty errors of
        Just errs -> Left errs
        Nothing ->
          Right
            SymTransducer
              { edgesOut = \v -> maybe [] id (lookup v cleanTable),
                initial = initS,
                initialRegs = initR,
                isFinal = isF
              }
  where
    (_, rawEntries) = runVertexBuilder vb []
    mergedEntries = foldl' mergeEntry [] (Prelude.reverse rawEntries)
    locatedEntries =
      [ (v, zipWith (locate v) [0 ..] results)
      | (v, results) <- mergedEntries
      ]
    errors =
      [ builderError
      | (_, results) <- locatedEntries,
        Left builderError <- results
      ]
    cleanTable =
      [ (v, [edge | Right edge <- results])
      | (v, results) <- locatedEntries
      ]

    mergeEntry acc (v, edges) =
      case break ((== v) . fst) acc of
        (_, []) -> acc ++ [(v, edges)]
        (before, (existingV, existingEdges) : after) ->
          before ++ (existingV, existingEdges ++ edges) : after

    locate v edgeIndex = \case
      Left defect -> Left (BuilderError v edgeIndex defect)
      Right edge -> Right edge

-- | Render structured builder errors in the historical message format.
-- Multiple errors are joined by newlines in declaration order.
renderBuilderErrors :: (Show v) => NonEmpty (BuilderError v) -> String
renderBuilderErrors = intercalate "\n" . fmap renderBuilderError . NonEmpty.toList

renderBuilderError :: (Show v) => BuilderError v -> String
renderBuilderError (BuilderError src n defect) =
  "Keiki.Builder: edge #"
    <> show n
    <> " from "
    <> show src
    <> case defect of
      DefectMissingGoto ->
        ": goto missing. Each onCmd/onEpsilon body must end with exactly one goto V."
      DefectMultipleGoto _ ->
        ": goto called more than once. Each onCmd/onEpsilon body must end with exactly one goto V."
      DefectOutputCtorMismatch expectedName expectedSlots actualName actualSlots ->
        ": emitWith InCtor "
          <> show actualName
          <> " (slots "
          <> renderSlotNames actualSlots
          <> ") contradicts the enclosing onCmd's InCtor "
          <> show expectedName
          <> " (slots "
          <> renderSlotNames expectedSlots
          <> "). An onCmd edge's outputs must pack the command constructor the edge matches on, or replay will invert the event to a different command."
      DefectMissingOutputIntent ->
        ": no emit or noEmit. Each onCmd/onEpsilon body must call 'emit' (or 'emitWith') to produce an event, or 'noEmit' to declare the edge deliberately silent (ε-edge)."

renderSlotNames :: [String] -> String
renderSlotNames names = "[" <> intercalate "," names <> "]"

forceBuilderErrors :: [BuilderError v] -> ()
forceBuilderErrors [] = ()
forceBuilderErrors (builderError : rest) = builderError `seq` forceBuilderErrors rest

forceEdgeTable :: [(v, [Edge p rs ci co v])] -> ()
forceEdgeTable [] = ()
forceEdgeTable ((_, edges) : rest) = forceEdges edges `seq` forceEdgeTable rest
  where
    forceEdges [] = ()
    forceEdges (edge : more) =
      edge `seq` forceOutputSpine (output edge) `seq` forceEdges more

    forceOutputSpine [] = ()
    forceOutputSpine (_ : outputs) = forceOutputSpine outputs