-- | Bind the registration theorem to the shared model comparison.
module Conformance.Lean.Registration
    ( InsertActive
    , modelComparison
    , insertActiveRow
    ) where

import Conformance.Story.Binding (mkBoundObligation)
import Conformance.Story.Live (LiveI, compareWithModel, observe)
import Conformance.Story.Specification
    ( LeanCheck
    , Theorem
    , bindCheck
    , bindTheorem
    )

-- | The registration declaration, distinct from every other theorem marker.
data InsertActive

modelComparison
    :: LeanCheck (LiveI reg wal step obs cmp) InsertActive step
modelComparison :: forall reg wal step obs cmp.
LeanCheck (LiveI reg wal step obs cmp) InsertActive step
modelComparison = Theorem InsertActive
-> (step -> Story (LiveI reg wal step obs cmp) ())
-> LeanCheck (LiveI reg wal step obs cmp) InsertActive step
forall {k} (thm :: k) obs (act :: * -> *).
Theorem thm -> (obs -> Story act ()) -> LeanCheck act thm obs
bindCheck Theorem InsertActive
insertActiveRow ((step -> Story (LiveI reg wal step obs cmp) ())
 -> LeanCheck (LiveI reg wal step obs cmp) InsertActive step)
-> (step -> Story (LiveI reg wal step obs cmp) ())
-> LeanCheck (LiveI reg wal step obs cmp) InsertActive step
forall a b. (a -> b) -> a -> b
$ \step
step -> do
    observation <- step -> Story reg wal step obs cmp obs
forall step reg wal obs cmp. step -> Story reg wal step obs cmp obs
observe step
step
    _ <- compareWithModel step observation
    pure ()

insertActiveRow :: Theorem InsertActive
insertActiveRow :: Theorem InsertActive
insertActiveRow =
    Binding -> Theorem InsertActive
forall {k} (thm :: k). Binding -> Theorem thm
bindTheorem (Binding -> Theorem InsertActive)
-> Binding -> Theorem InsertActive
forall a b. (a -> b) -> a -> b
$
        String -> String -> String -> Binding
mkBoundObligation
            String
"Singular.Statements.insert_active_transaction_row"
            String
"3c8d7b9bd9092b29d2bbb58ebbca15b008dc9b9396899d9d67d55ea66e1f6070"
            String
"265c595edd72eab10f3b08a36cb010ad407cf48b"