keiki-0.1.0.0: src/Keiki/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.Decider",
-- "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.
--
-- * Missing 'goto': caught at finalize time (when 'buildTransducer'
-- evaluates the 'VertexBuilder' do-block) with a runtime error
-- naming the source vertex and edge index.
--
-- * Multiple 'goto's in the same edge body: caught the same way.
--
-- == 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,
-- * 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.Typeable (Typeable)
import GHC.Records (HasField (..))
import GHC.TypeLits (KnownSymbol, Symbol)
import Keiki.Core
( Cmp (..),
Edge (..),
HsPred (..),
InCtor,
Index,
OutFields (..),
OutTerm,
RegFile,
SymTransducer (..),
Term (TReg),
Update (..),
WireCtor,
combine,
inpCtor,
matchInCtor,
oNil,
pack,
(*:),
)
import Keiki.Core qualified as K
import Keiki.Internal.Slots
( Concat,
Disjoint,
HasIndexN (..),
IndexN (..),
)
import Unsafe.Coerce (unsafeCoerce)
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 packages the result into a closed 'Edge'. The
-- existential @w@ on 'Edge''s 'update' field closes here.
data PartialEdge rs ci co v (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', so that the
-- 2-argument 'emit' can recover it without the user repeating
-- it. 'Nothing' inside an 'onEpsilon' body — 'emit' there must
-- use 'emitWith' to supply the 'InCtor' explicitly.
peInCtor :: Maybe (PeInCtor ci)
}
-- | Existential wrapper hiding the @ifs@ slot list of an 'InCtor'.
-- Stored on 'PartialEdge' by 'onCmd' and read back by 'emit'.
--
-- This is a builder-local existential rather than a reuse of
-- 'Keiki.Symbolic.SomeInCtor' because the latter carries an
-- 'ExtractRegFile' constraint the builder does not need and lives
-- in a module that pulls SBV; reusing it would add an SBV edge to
-- every consumer of "Keiki.Builder".
data PeInCtor ci where
PeInCtor :: InCtor ci ifs -> PeInCtor ci
-- | 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 (w :: [Symbol]) (w' :: [Symbol]) a
= EdgeBuilder
{ runEdgeBuilder ::
PartialEdge rs ci co v w ->
(a, PartialEdge rs ci co v 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 w1 w2 a ->
(a -> EdgeBuilder rs ci co v w2 w3 b) ->
EdgeBuilder rs ci co v 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 w1 w2 a ->
EdgeBuilder rs ci co v w2 w3 b ->
EdgeBuilder rs ci co v w1 w3 b
m >> n = m Keiki.Builder.>>= \_ -> n
infixl 1 >>
-- | Embed a value. Slot-set unchanged.
pure :: a -> EdgeBuilder rs ci co v w w a
pure a = EdgeBuilder $ \pe -> (a, pe)
-- | Synonym for 'pure'. Re-exported for @QualifiedDo@.
return :: a -> EdgeBuilder rs ci co v 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 w.
(KnownSymbol name, Disjoint '[name] w) =>
IndexN name rs r ->
Term rs ci ifs r ->
EdgeBuilder rs ci co v 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 w.
(KnownSymbol name, Disjoint '[name] w) =>
IndexN name rs r ->
Term rs ci ifs r ->
EdgeBuilder rs ci co v w (Concat '[name] w) ()
(=:) = (.=)
infixr 6 =:
-- * Termination -----------------------------------------------------------
-- | Set the edge's target vertex. Required exactly once per edge
-- body; missing 'goto' produces a finalize-time runtime error
-- naming the source vertex and edge index, and so does multiple
-- 'goto's in the same body.
goto :: v -> EdgeBuilder rs ci co v 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 from the enclosing 'onCmd'; an 'emit' inside
-- 'onEpsilon' (where no 'InCtor' is bound) raises a finalize-time
-- error directing the user to 'emitWith'.
--
-- == 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 w w ()
emit wc rec = EdgeBuilder $ \pe -> case peInCtor pe of
Just (PeInCtor ic) ->
-- 'onCmd' pins the same 'InCtor' into 'peInCtor' /and/ into the
-- 'PayloadProj' the body projects through, so the record's input
-- field schema 'ifs' (from 'ToOutFields') equals the pinned
-- 'InCtor''s schema. The existential 'PeInCtor' hides that
-- equality; 'reIndexPinnedInCtor' re-establishes it. This does not
-- weaken replay soundness: the resulting 'OPack''s 'InCtor' and
-- 'OutFields' share 'ifs', so 'solveOutput' recovers fields with no
-- coercion (EP-53). Mirrors 'Keiki.Composition.unsafeCoerceInCtor'.
( (),
pe
{ peOutput =
peOutput pe
++ [pack (reIndexPinnedInCtor @ci @_ @ifs ic) wc (toOutFields rec)]
}
)
Nothing ->
error
"Keiki.Builder.emit: no enclosing onCmd pinned an InCtor. \
\Use 'emitWith ic wc fs' inside 'onEpsilon', or move the \
\emit inside an 'onCmd' block."
-- | Re-establish the (existentially hidden) equality between a pinned
-- 'InCtor''s field schema and the schema the enclosing 'onCmd''s
-- 'PayloadProj' exposes. Unsound in general; justified at the single
-- 'emit' call site by 'onCmd' storing one and the same 'InCtor' in both
-- places (see 'emit'). The runtime representation is identical.
reIndexPinnedInCtor :: forall ci ifs0 ifs. InCtor ci ifs0 -> InCtor ci ifs
reIndexPinnedInCtor = unsafeCoerce
-- | Emit an event with an explicit 'InCtor'. The escape hatch for
-- 'onEpsilon' bodies (which do not pin an 'InCtor') and for any
-- caller that needs to override the one bound by the enclosing
-- 'onCmd'. Inside 'onCmd' the InCtor-less 'emit' is preferred.
-- Like 'emit', accumulates into the edge's output list — multiple
-- calls produce a multi-event edge.
emitWith ::
forall co fs rs ci v w ifs rec.
(ToOutFields rec rs ci ifs fs) =>
InCtor ci ifs ->
WireCtor co fs ->
rec ->
EdgeBuilder rs ci co v w w ()
emitWith ic wc rec = EdgeBuilder $ \pe ->
((), pe {peOutput = peOutput pe ++ [pack ic wc (toOutFields rec)]})
-- | Mark the edge as ε-output (no event). Idempotent: an edge with
-- no 'emit' or 'noEmit' call is also an ε-edge by default; 'noEmit'
-- exists only so the user can be explicit about intent. Mixing
-- 'noEmit' and 'emit' in the same body is allowed but the 'noEmit'
-- is a documentation no-op (the 'emit's still produce a non-empty
-- output list).
noEmit :: EdgeBuilder rs ci co v w w ()
noEmit = EdgeBuilder $ \pe -> ((), pe)
-- * 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 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 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 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 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 ->
[Edge (HsPred rs ci) rs ci co v] ->
(a, [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.
(Show v) =>
InCtor ci ifs ->
(PayloadProj rs ci ifs -> EdgeBuilder rs ci co v '[] w ()) ->
EdgeListBuilder rs ci co v ()
onCmd ic body = EdgeListBuilder $ \src acc ->
let initial =
PartialEdge
{ peGuard = matchInCtor ic,
peUpdate = UKeep,
peOutput = [],
peTargets = [],
peInCtor = Just (PeInCtor ic)
}
(_, finalPE) = runEdgeBuilder (body (PayloadProj ic)) initial
edgeIx = length acc
edge = finalizeEdge edgeIx src 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.
(Show v) =>
EdgeBuilder rs ci co v '[] w () ->
EdgeListBuilder rs ci co v ()
onEpsilon body = EdgeListBuilder $ \src acc ->
let initial =
PartialEdge
{ peGuard = PTop,
peUpdate = UKeep,
peOutput = [],
peTargets = [],
peInCtor = Nothing
}
(_, finalPE) = runEdgeBuilder body initial
edgeIx = length acc
edge = finalizeEdge edgeIx src finalPE
in ((), edge : acc)
-- | Close a 'PartialEdge' into an 'Edge'. Validation: 'peTargets'
-- must have exactly one entry; missing or duplicated 'goto' calls
-- raise a runtime 'error' naming the source vertex and edge index.
-- The 'peOutput' list (zero or more 'OutTerm's accumulated by
-- 'emit' / 'emitWith' calls) flows directly into the resulting
-- 'Edge.output' field.
finalizeEdge ::
(Show v) =>
Int ->
v ->
PartialEdge rs ci co v w ->
Edge (HsPred rs ci) rs ci co v
finalizeEdge n src pe = case peTargets pe of
[t] ->
Edge
{ guard = peGuard pe,
update = peUpdate pe,
output = peOutput pe,
target = t
}
[] ->
error $
"Keiki.Builder: edge #"
<> show n
<> " from "
<> show src
<> ": goto missing. Each onCmd/"
<> "onEpsilon body must end with exactly one goto V."
(_ : _ : _) ->
error $
"Keiki.Builder: edge #"
<> show n
<> " from "
<> show src
<> ": goto called more than once. "
<> "Each onCmd/onEpsilon body must end with "
<> "exactly one goto V."
-- * 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, [Edge (HsPred rs ci) rs ci co v])] ->
(a, [(v, [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 ::
(Eq v, Show v) =>
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.
--
-- The @Bounded v@ / @Enum v@ constraints are not currently used by
-- 'buildTransducer' itself but are recorded as reserved for a
-- future @withCompletenessCheck@ combinator that would assert every
-- vertex appears in some 'from' block.
buildTransducer ::
forall rs ci co v.
(Bounded v, Enum v, 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 =
SymTransducer
{ edgesOut = \v -> Prelude.concatMap snd (Prelude.filter ((== v) . fst) vmap),
initial = initS,
initialRegs = initR,
isFinal = isF
}
where
(_, vmap) = runVertexBuilder vb []