UserRegistration.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE QualifiedDo #-}
{-# LANGUAGE TemplateHaskell #-}

-- | The User Registration aggregate from synthesis §4, transcribed in
-- the v1 'Keiki.Core' DSL. This module is the smoke test for the
-- master plan's "the synthesis holds" gate.
--
-- See:
--
--   * @docs/research/synthesis-c-foundation-b-presentation-with-worked-examples.md@
--     §4 — the original walkthrough.
--   * @docs/research/dsl-shape-for-symbolic-register.md@ — the DSL note's
--     "Worked example" section, which this module reproduces.
--
-- v1 deviations from synthesis §4:
--
--   * 'AccountConfirmedData' carries the @confirmCode@ field (synthesis
--     §4 fix-1). This is the "fixed" schema. The "unfixed" schema —
--     'Jitsurei.UserRegistrationV0' — is a separate module that
--     drops the field for the M7 hidden-input demonstration.
--   * 'ResendConfirmationData' carries a @code@ field (the new
--     confirmation code). Per the EP-3 effects-boundary note, fresh
--     codes are generated by the runtime adapter, not pulled from
--     'IO' inside the transducer.
--   * Each output is built with 'OPack' plus a v1 hand-written
--     inverse. The DSL note's 'OPack' was extended in M4 to carry that
--     inverse; see EP-4's Decision Log.
module Keiki.Fixtures.UserRegistration
  ( -- * Domain types
    Email,
    ConfirmationCode,

    -- * Command payloads
    StartRegistrationData (..),
    ConfirmAccountData (..),
    ResendConfirmationData (..),
    FulfillGDPRRequestData (..),
    UserCmd (..),

    -- * Event payloads
    RegistrationStartedData (..),
    ConfirmationEmailSentData (..),
    AccountConfirmedData (..),
    ConfirmationResentData (..),
    AccountDeletedData (..),
    UserEvent (..),

    -- * Register file and control vertices
    UserRegRegs,
    Vertex (..),

    -- * The transducer
    userReg,
    userRegAST,
    emptyRegs,

    -- * Multi-event driver configuration (EP-20 M4)

    -- * Wire constructors (exported for testing)
    wireRegistrationStarted,
    wireConfirmationEmailSent,
    wireAccountConfirmed,
    wireConfirmationResent,
    wireAccountDeleted,

    -- * Input constructors (exported for testing and reuse)
    inCtorStart,
    inCtorConfirm,
    inCtorResend,
    inCtorGdpr,
    inpStart,
    inpConfirm,
    inpResend,
    inpGdpr,

    -- * B-presentation views (TH-derived; see EP-13 / MP-5)
    SUserVertex (..),
    UserView (..),
    userView,
  )
where

import Data.Text (Text)
import Data.Time (UTCTime)
import GHC.Generics (Generic)
import Keiki.Builder ((.=))
import Keiki.Builder qualified as B
import Keiki.Core
import Keiki.Generics (emptyRegFile)
import Keiki.Generics.TH (deriveAggregateCtors, deriveView, deriveWireCtors)
import Keiki.Symbolic (KnownInCtors (..), SomeInCtor (..))

-- * Domain types ------------------------------------------------------------

type Email = Text

type ConfirmationCode = Text

-- * Command payloads --------------------------------------------------------

data StartRegistrationData = StartRegistrationData
  { email :: Email,
    confirmCode :: ConfirmationCode,
    at :: UTCTime
  }
  deriving (Eq, Show, Generic)

data ConfirmAccountData = ConfirmAccountData
  { confirmCode :: ConfirmationCode,
    at :: UTCTime
  }
  deriving (Eq, Show, Generic)

-- | Per the effects-boundary note: fresh confirmation codes are
-- generated by the runtime adapter and arrive in the command. The
-- pure layer never pulls randomness.
data ResendConfirmationData = ResendConfirmationData
  { code :: ConfirmationCode,
    at :: UTCTime
  }
  deriving (Eq, Show, Generic)

newtype FulfillGDPRRequestData = FulfillGDPRRequestData {at :: UTCTime}
  deriving (Eq, Show, Generic)

data UserCmd
  = StartRegistration StartRegistrationData
  | ConfirmAccount ConfirmAccountData
  | ResendConfirmation ResendConfirmationData
  | FulfillGDPRRequest FulfillGDPRRequestData
  deriving (Eq, Show, Generic)

-- * Event payloads ----------------------------------------------------------

data RegistrationStartedData = RegistrationStartedData
  { email :: Email,
    confirmCode :: ConfirmationCode,
    at :: UTCTime
  }
  deriving (Eq, Show, Generic)

newtype ConfirmationEmailSentData = ConfirmationEmailSentData {email :: Email}
  deriving (Eq, Show, Generic)

-- | Synthesis §4 fix-1 schema: includes the @confirmCode@ field.
data AccountConfirmedData = AccountConfirmedData
  { email :: Email,
    confirmCode :: ConfirmationCode,
    at :: UTCTime
  }
  deriving (Eq, Show, Generic)

data ConfirmationResentData = ConfirmationResentData
  { email :: Email,
    confirmCode :: ConfirmationCode,
    at :: UTCTime
  }
  deriving (Eq, Show, Generic)

data AccountDeletedData = AccountDeletedData
  { email :: Email,
    at :: UTCTime
  }
  deriving (Eq, Show, Generic)

data UserEvent
  = RegistrationStarted RegistrationStartedData
  | ConfirmationEmailSent ConfirmationEmailSentData
  | AccountConfirmed AccountConfirmedData
  | ConfirmationResent ConfirmationResentData
  | AccountDeleted AccountDeletedData
  deriving (Eq, Show, Generic)

-- * Register file and control vertices -------------------------------------

type UserRegRegs =
  '[ '("email", Email),
     '("confirmCode", ConfirmationCode),
     '("registeredAt", UTCTime),
     '("confirmedAt", UTCTime),
     '("deletedAt", UTCTime)
   ]

data Vertex
  = PotentialCustomer
  | RequiresConfirmation
  | Confirmed
  | Deleted
  deriving (Eq, Ord, Show, Enum, Bounded)

-- | Initial register file. Each slot is pre-bound to a deferred
-- @"uninit: <slot>"@ error by 'Keiki.Generics.emptyRegFile' so reads
-- of an uninitialized slot crash with a targeted message instead of
-- a silent bottom.
emptyRegs :: RegFile UserRegRegs
emptyRegs = emptyRegFile

-- * Per-constructor input projections + guards (TH-derived) --------------

--
-- One 'InCtor' value per command constructor describes how to match
-- and re-build the constructor's payload as a typed 'RegFile'. The
-- per-constructor 'inpFoo' helpers turn an 'Index' (typically written
-- via 'OverloadedLabels' as @inpStart #email@) into a 'Term' that
-- structurally projects the named field of the named command
-- constructor. The matching @isFoo@ guards reduce to
-- @PInCtor@ atoms that the SBV-backed 'BoolAlg' instance recognizes
-- symbolically. 'solveOutput' walks the 'OutFields' bound by an
-- edge's @output@ and reconstructs the input @ci@ mechanically; no
-- per-edge inverse function is needed.
--
-- All declarations in this section are emitted by the splice below;
-- the slot-list types come from 'Keiki.Generics.RegFieldsOf' applied
-- to each command payload's 'Generic' representation. Singleton
-- 'Continue' uses 'mkInCtor0' under the hood (no @inp@ projection
-- because @'Index' \'[]@ is uninhabited).

$( deriveAggregateCtors
     ''UserCmd
     ''UserRegRegs
     [ ("StartRegistration", "Start"),
       ("ConfirmAccount", "Confirm"),
       ("ResendConfirmation", "Resend"),
       ("FulfillGDPRRequest", "Gdpr")
     ]
 )

-- | Enumerate the five 'InCtor' values of 'UserCmd' so 'symSatExt'
-- can rebuild a concrete 'UserCmd' from an SBV model: the model's
-- @"inputCtor"@ string is matched against these entries' 'icName',
-- and the matching entry's @icBuild@ is called over a 'RegFile'
-- assembled from the @"inp/<icName>/<slot>"@ model values.
instance KnownInCtors UserCmd where
  allInCtors =
    [ SomeInCtor inCtorStart,
      SomeInCtor inCtorConfirm,
      SomeInCtor inCtorResend,
      SomeInCtor inCtorGdpr
    ]

-- * Wire constructors for events (TH-derived) ----------------------------

--
-- One 'WireCtor' value per event constructor. The nested-pair field
-- tuple comes from each event record's 'Generic' instance via
-- 'Keiki.Generics.FieldsOf'.

$( deriveWireCtors
     ''UserEvent
     [ ("RegistrationStarted", "RegistrationStarted"),
       ("ConfirmationEmailSent", "ConfirmationEmailSent"),
       ("AccountConfirmed", "AccountConfirmed"),
       ("ConfirmationResent", "ConfirmationResent"),
       ("AccountDeleted", "AccountDeleted")
     ]
 )

-- * B-presentation views (TH-derived) ------------------------------------

--
-- The B-view is a per-vertex projection on top of the shared
-- 'RegFile UserRegRegs'. For each control vertex 'v' the splice
-- generates a 'UserView' constructor that exposes only the slots the
-- vertex actually uses (the "live" slots). Pattern-matching on
-- @userView SConfirmed regs@ yields a @ConfirmedV { cEmail = …,
-- cConfirmedAt = … }@ value whose record selectors are the live
-- slots only — the type system blocks the reader from asking
-- @SPotentialCustomer@ for @cConfirmedAt@.
--
-- The projection is opt-in and downstream of the transducer: nothing
-- in 'userReg' below references 'userView'. See
-- @docs/research/genview-th-splice-design.md@ and the synthesis
-- note's §3 for the design rationale.

$( deriveView
     ''Vertex
     ''UserRegRegs
     "SUserVertex"
     "UserView"
     "userView"
     [ ("PotentialCustomer", []),
       ("RequiresConfirmation", ["email", "confirmCode"]),
       ("Confirmed", ["email", "confirmedAt"]),
       ("Deleted", ["email", "deletedAt"])
     ]
 )

-- * The transducer ---------------------------------------------------------

-- | The aggregate's transducer, authored with 'Keiki.Builder'. This
-- is the canonical form every downstream consumer
-- ('Keiki.Composition.compose', the deciders, the symbolic
-- analyses, the example specs) uses by name.
userReg ::
  SymTransducer
    (HsPred UserRegRegs UserCmd)
    UserRegRegs
    Vertex
    UserCmd
    UserEvent
userReg = B.buildTransducer
  PotentialCustomer
  emptyRegs
  (\case Deleted -> True; _ -> False)
  do
    B.from PotentialCustomer do
      -- EP-19 M7: collapsed entrance — two emits in one transition.
      B.onCmd inCtorStart $ \d -> B.do
        B.slot @"email" .= d.email
        B.slot @"confirmCode" .= d.confirmCode
        B.slot @"registeredAt" .= d.at
        B.emit
          wireRegistrationStarted
          RegistrationStartedTermFields
            { email = d.email,
              confirmCode = d.confirmCode,
              at = d.at
            }
        B.emit
          wireConfirmationEmailSent
          ConfirmationEmailSentTermFields {email = d.email}
        B.goto RequiresConfirmation

    B.from RequiresConfirmation do
      -- Right code: confirm. The InCtor-match guard from `onCmd`
      -- short-circuits the d.confirmCode read for non-ConfirmAccount
      -- inputs.
      B.onCmd inCtorConfirm $ \d -> B.do
        B.requireEq d.confirmCode #confirmCode
        B.slot @"confirmedAt" .= d.at
        B.emit
          wireAccountConfirmed
          AccountConfirmedTermFields
            { email = #email,
              confirmCode = d.confirmCode,
              at = d.at
            }
        B.goto Confirmed

      -- Resend: rotate the code (code arrives in the command).
      B.onCmd inCtorResend $ \d -> B.do
        B.slot @"confirmCode" .= d.code
        B.slot @"registeredAt" .= d.at
        B.emit
          wireConfirmationResent
          ConfirmationResentTermFields
            { email = #email,
              confirmCode = d.code,
              at = d.at
            }
        B.goto RequiresConfirmation

      -- GDPR before confirmation is durable just like post-confirmation
      -- deletion: changing state without an event would be lost on replay.
      B.onCmd inCtorGdpr $ \d -> B.do
        B.slot @"deletedAt" .= d.at
        B.emit
          wireAccountDeleted
          AccountDeletedTermFields
            { email = #email,
              at = d.at
            }
        B.goto Deleted

    B.from Confirmed do
      B.onCmd inCtorGdpr $ \d -> B.do
        B.slot @"deletedAt" .= d.at
        B.emit
          wireAccountDeleted
          AccountDeletedTermFields
            { email = #email,
              at = d.at
            }
        B.goto Deleted

-- Deleted is terminal; defaults to [] without an explicit `from`.

-- * AST form (legacy, retained for the M5 equivalence test) ----------------

-- | The same transducer hand-authored against the post-MP-6
-- "Keiki.Core" AST. Retained as a side-by-side reference for the
-- 'Jitsurei.UserRegistrationBuilderSpec' equivalence test;
-- removable in a follow-up plan once the migration is judged
-- stable.
userRegAST ::
  SymTransducer
    (HsPred UserRegRegs UserCmd)
    UserRegRegs
    Vertex
    UserCmd
    UserEvent
userRegAST =
  SymTransducer
    { edgesOut = userRegASTEdges,
      initial = PotentialCustomer,
      initialRegs = emptyRegs,
      isFinal = \case Deleted -> True; _ -> False
    }

userRegASTEdges ::
  Vertex ->
  [Edge (HsPred UserRegRegs UserCmd) UserRegRegs UserCmd UserEvent Vertex]
userRegASTEdges = \case
  -- EP-19 M7: collapsed to one length-2 multi-event edge.
  PotentialCustomer ->
    [ Edge
        { guard = isStart,
          update =
            USet (#email :: IndexN "email" UserRegRegs Email) (inpStart #email)
              `combine` USet
                (#confirmCode :: IndexN "confirmCode" UserRegRegs ConfirmationCode)
                (inpStart #confirmCode)
              `combine` USet
                (#registeredAt :: IndexN "registeredAt" UserRegRegs UTCTime)
                (inpStart #at),
          output =
            [ pack
                inCtorStart
                wireRegistrationStarted
                ( OFCons
                    (inpStart #email)
                    ( OFCons
                        (inpStart #confirmCode)
                        (OFCons (inpStart #at) OFNil)
                    )
                ),
              pack
                inCtorStart
                wireConfirmationEmailSent
                (OFCons (inpStart #email) OFNil)
            ],
          target = RequiresConfirmation
        }
    ]
  RequiresConfirmation ->
    [ -- Right code: confirm. The 'isConfirm' conjunct short-circuits the
      -- inpConfirm read for non-ConfirmAccount inputs.
      Edge
        { guard =
            PAnd
              isConfirm
              ( inpConfirm #confirmCode
                  .== proj (#confirmCode :: Index UserRegRegs ConfirmationCode)
              ),
          update =
            USet
              (#confirmedAt :: IndexN "confirmedAt" UserRegRegs UTCTime)
              (inpConfirm #at),
          output =
            [ pack
                inCtorConfirm
                wireAccountConfirmed
                ( OFCons
                    (proj (#email :: Index UserRegRegs Email))
                    ( OFCons
                        (inpConfirm #confirmCode)
                        (OFCons (inpConfirm #at) OFNil)
                    )
                )
            ],
          target = Confirmed
        },
      -- Resend: rotate the code (code arrives in the command).
      Edge
        { guard = isResend,
          update =
            USet
              (#confirmCode :: IndexN "confirmCode" UserRegRegs ConfirmationCode)
              (inpResend #code)
              `combine` USet
                (#registeredAt :: IndexN "registeredAt" UserRegRegs UTCTime)
                (inpResend #at),
          output =
            [ pack
                inCtorResend
                wireConfirmationResent
                ( OFCons
                    (proj (#email :: Index UserRegRegs Email))
                    ( OFCons
                        (inpResend #code)
                        (OFCons (inpResend #at) OFNil)
                    )
                )
            ],
          target = RequiresConfirmation
        },
      -- GDPR before confirmation emits the deletion event so replay observes
      -- the state and register change.
      Edge
        { guard = isGdpr,
          update =
            USet
              (#deletedAt :: IndexN "deletedAt" UserRegRegs UTCTime)
              (inpGdpr #at),
          output =
            [ pack
                inCtorGdpr
                wireAccountDeleted
                ( OFCons
                    (proj (#email :: Index UserRegRegs Email))
                    (OFCons (inpGdpr #at) OFNil)
                )
            ],
          target = Deleted
        }
    ]
  Confirmed ->
    [ Edge
        { guard = isGdpr,
          update =
            USet
              (#deletedAt :: IndexN "deletedAt" UserRegRegs UTCTime)
              (inpGdpr #at),
          output =
            [ pack
                inCtorGdpr
                wireAccountDeleted
                ( OFCons
                    (proj (#email :: Index UserRegRegs Email))
                    (OFCons (inpGdpr #at) OFNil)
                )
            ],
          target = Deleted
        }
    ]
  Deleted -> []