Transducer.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE QualifiedDo #-}
-- @generated by keiro-dsl 0.15.0.0 (language keiro-dsl 4) from aggregate Alpha; do not edit.
module Proof.WorkspaceProof.Alpha.Generated.Transducer
  ( alphaTransducer
  , alphaFoldFingerprint
  , BehaviorOwnership (..)
  , alphaPredicateVerifications
  ) where

import Proof.WorkspaceProof.Alpha.Generated.Domain
import Data.Text (Text)
import Keiki.Builder qualified as B
import Keiki.Core (HsPred, SymTransducer, (.==))
import Keiki.Core qualified as K
import Keiki.Symbolic qualified as S

alphaTransducer
  :: SymTransducer
       (HsPred AlphaRegs AlphaCommand)
       AlphaRegs
       AlphaVertex
       AlphaCommand
       AlphaEvent
alphaTransducer =
  B.buildTransducer AlphaActive initialAlphaRegs isTerminal do
    B.from AlphaActive do
      B.onCmd inCtorPingAlpha $ \d -> B.do
        B.requireGuard $
          d.current .== K.lit False
        B.emit wireAlphaPinged (AlphaPingedTermFields
          { proofId = d.proofId
          , current = d.current
          })
        B.goto AlphaActive
      B.onCmd inCtorPingAlpha $ \d -> B.do
        B.replayOnly
        B.requireGuard $
          d.current .== K.lit True
        B.emit wireAlphaPinged (AlphaPingedTermFields
          { proofId = d.proofId
          , current = d.current
          })
        B.goto AlphaActive
      B.onCmd inCtorLegacyPingAlpha $ \d -> B.do
        B.replayOnly
        B.emit wireLegacyAlphaPinged (LegacyAlphaPingedTermFields
          { proofId = d.proofId
          })
        B.goto AlphaActive
 where
  isTerminal = \case

    _ -> False

alphaFoldFingerprint :: Text
alphaFoldFingerprint = "50a497dba43db7b912bdbd023c623c29"

data BehaviorOwnership = GeneratedOwned | HoleOwned
  deriving stock (Eq, Show)

-- Every checked transition predicate is audited through Keiki's conservative
-- symbolic verifier. Opaque Hole terms remain explicitly unverified.
alphaPredicateVerifications :: IO [(Text, BehaviorOwnership, S.PredicateVerification)]
alphaPredicateVerifications = sequence
  [ verifyTransition "transition1ActivePingAlpha" GeneratedOwned AlphaActive 0
  , verifyTransition "transition2ActivePingAlpha" GeneratedOwned AlphaActive 1
  , verifyTransition "transition3ActiveLegacyPingAlpha" GeneratedOwned AlphaActive 2
  ]
 where
  verifyTransition label owner source edgeIndex =
    case drop edgeIndex (K.edgesOut alphaTransducer source) of
      K.Edge predicate _ _ _ _ : _ -> (\result -> (label, owner, result)) <$> S.verifyPredicate predicate
      [] -> pure (label, owner, S.UnverifiedSolverFailure "generated transition edge missing")