Skip to content

Commit

Permalink
hack together better error messages when the event logger is unimplem…
Browse files Browse the repository at this point in the history
…ented
  • Loading branch information
goolord committed May 4, 2021
1 parent 343d1a6 commit 0739235
Show file tree
Hide file tree
Showing 2 changed files with 28 additions and 13 deletions.
38 changes: 26 additions & 12 deletions semantics/executable-spec/src/Control/State/Transition/Extended.hs
Expand Up @@ -48,6 +48,8 @@ module Control.State.Transition.Extended
writerEvent,
tellEvent,
tellEvents,
EventPolicyWriter,
EventPolicy(..),

-- * Apply STS
AssertionPolicy (..),
Expand Down Expand Up @@ -160,6 +162,17 @@ instance
(STS sts) =>
Exception (AssertionViolation sts)

data EventPolicy =
EventPolicyWrite
| EventPolicyDiscard

type family EventPolicyWriter (sts :: Type) (x :: Type) :: Type where
EventPolicyWriter sts x = EventPolicyWriter' (EventPolicySTS sts) sts x

type family EventPolicyWriter' (e :: EventPolicy) (sts :: Type) (x :: Type) :: Type where
EventPolicyWriter' 'EventPolicyWrite a x = (x, [Event a])
EventPolicyWriter' 'EventPolicyDiscard a _ = TypeError ('Text "Cannot write events to the monad 'BaseM (" ':<>: 'ShowType a ':<>: 'Text ")'")

-- | State transition system.
class
( Eq (PredicateFailure a),
Expand All @@ -183,11 +196,16 @@ class

type BaseM a = Identity

type EventPolicySTS a :: EventPolicy
type EventPolicySTS a = 'EventPolicyDiscard

type Event a :: Type
type Event a = TypeError ('Text "missing associated type for '" ':<>: 'ShowType (Event a) ':<>: 'Text "'")
type Event a = TypeError ('Text "Missing associated type for 'Event (" ':<>: 'ShowType a ':<>: 'Text ")'")

writer :: EventPolicyWriter a x -> (BaseM a) x
default writer :: forall x. (EventPolicySTS a ~ 'EventPolicyDiscard) => EventPolicyWriter a x -> (BaseM a) x
writer = error "absurd"

writer :: (x, [Event a]) -> (BaseM a) x
writer (x, _) = pure x
-- | Descriptive type for the possible failures which might cause a transition
-- to fail.
--
Expand Down Expand Up @@ -244,9 +262,6 @@ data Clause sts (rtype :: RuleType) a where
-- Subsequent computation with state introduced
(State sub -> a) ->
Clause sts rtype a
Writer ::
(a, [Event sts]) ->
Clause sts rtype a
Predicate ::
[Label] ->
Either e a ->
Expand Down Expand Up @@ -314,17 +329,17 @@ liftSTS f = wrap $ Lift f pure
judgmentContext :: Rule sts rtype (RuleContext rtype sts)
judgmentContext = wrap $ GetCtx pure

writerEvent ::
(a, [Event sts]) ->
writerEvent :: forall sts ctx a. STS sts =>
EventPolicyWriter sts a ->
Rule sts ctx a
writerEvent w = liftF $ Writer w
writerEvent = liftSTS . writer @sts

tellEvent ::
tellEvent ::forall sts ctx. (STS sts, EventPolicyWriter sts () ~ ((), [Event sts])) =>
Event sts ->
Rule sts ctx ()
tellEvent e = tellEvents [e]

tellEvents ::
tellEvents :: forall sts ctx. (STS sts, EventPolicyWriter sts () ~ ((), [Event sts])) =>
[Event sts] ->
Rule sts ctx ()
tellEvents es = writerEvent ((), es)
Expand Down Expand Up @@ -462,7 +477,6 @@ applyRuleInternal vp goSTS jc r = flip runStateT [] $ foldF runClause r
runClause :: Clause s rtype a -> MonadState.StateT [PredicateFailure s] m a
runClause (Lift f next) = next <$> lift f
runClause (GetCtx next) = pure $ next jc
runClause (Writer x) = lift $ writer @s x
runClause (Predicate lbls cond orElse val) =
if validateIf lbls
then do
Expand Down
Expand Up @@ -39,7 +39,7 @@ import Control.State.Transition
judgmentContext,
liftSTS,
tellEvent,
(?!),
(?!), EventPolicy (EventPolicyWrite)
)
import Data.Kind (Type)
import Data.Typeable (Typeable)
Expand Down Expand Up @@ -107,6 +107,7 @@ instance
type BaseM (POOL era) = ShelleyBase
type PredicateFailure (POOL era) = PoolPredicateFailure era
type Event (POOL era) = POOLEvent era
type EventPolicySTS (POOL era) = 'EventPolicyWrite

writer (a, w) = Writer.writer (a, fmap ShelleyPOOLEvent w)
transitionRules = [poolDelegationTransition]
Expand Down

0 comments on commit 0739235

Please sign in to comment.