Transducer.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE QualifiedDo #-}
-- @generated by keiro-dsl 0.21.0.0 (language keiro-dsl 4) from aggregate Assignment; do not edit.
module Proof.WorkspaceProof.Assignment.Generated.Transducer
  ( assignmentTransducer
  , assignmentFoldFingerprint
  , BehaviorOwnership (..)
  , assignmentPredicateVerifications
  ) where

import Proof.WorkspaceProof.Assignment.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
import Proof.WorkspaceProof.Assignment.Holes qualified as Holes
import Data.Text qualified as T
import Keiro.Snapshot.Codec (FoldVersion (..))

assignmentTransducer
  :: SymTransducer
       (HsPred AssignmentRegs AssignmentCommand)
       AssignmentRegs
       AssignmentVertex
       AssignmentCommand
       AssignmentEvent
assignmentTransducer =
  B.buildTransducer AssignmentActive initialAssignmentRegs isTerminal do
    B.from AssignmentActive do
      B.onCmd inCtorSetProperty $ \d -> B.do
        Holes.transition1ActiveSetPropertyHole d
        B.emit wirePropertySet (PropertySetTermFields
          { key = d.key
          , value = d.value
          })
        B.goto AssignmentActive
      B.onCmd inCtorClearProperty $ \d -> B.do
        Holes.transition2ActiveClearPropertyHole d
        B.emit wirePropertyCleared (PropertyClearedTermFields
          { key = d.key
          })
        B.goto AssignmentActive
      B.onCmd inCtorTouch $ \d -> B.do
        B.emit wireTouched (TouchedTermFields
          { note = d.note
          })
        B.goto AssignmentActive
      B.onCmd inCtorClearProperty $ \d -> B.do
        B.replayOnly
        Holes.transition4ActiveClearPropertyHole d
        B.emit wirePropertyCleared (PropertyClearedTermFields
          { key = d.key
          })
        B.goto AssignmentActive
 where
  isTerminal = \case

    _ -> False

assignmentFoldFingerprint :: Text
assignmentFoldFingerprint = T.intercalate "|" ("a54553687057587434f20f69114efc14" : [foldToken Holes.transition1ActiveSetPropertyHoleFoldVersion, foldToken Holes.transition2ActiveClearPropertyHoleFoldVersion, foldToken Holes.transition4ActiveClearPropertyHoleFoldVersion] ) where foldToken (FoldVersion token) = T.pack (show (T.length token)) <> ":" <> token

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.
assignmentPredicateVerifications :: IO [(Text, BehaviorOwnership, S.PredicateVerification)]
assignmentPredicateVerifications = sequence
  [ verifyTransition "transition1ActiveSetProperty" HoleOwned AssignmentActive 0
  , verifyTransition "transition2ActiveClearProperty" HoleOwned AssignmentActive 1
  , verifyTransition "transition3ActiveTouch" GeneratedOwned AssignmentActive 2
  , verifyTransition "transition4ActiveClearProperty" HoleOwned AssignmentActive 3
  ]
 where
  verifyTransition label owner source edgeIndex =
    case drop edgeIndex (K.edgesOut assignmentTransducer source) of
      K.Edge predicate _ _ _ _ : _ -> (\result -> (label, owner, result)) <$> S.verifyPredicate predicate
      [] -> pure (label, owner, S.UnverifiedSolverFailure "generated transition edge missing")