Safe Haskell | Safe-Inferred |
---|---|

Language | Haskell2010 |

# Documentation

class (ForAllExecTypes (HasSpec fn) fn rule era, ForAllExecTypes ToExpr fn rule era, ForAllExecTypes NFData fn rule era, KnownSymbol rule, STS (EraRule rule era), BaseM (EraRule rule era) ~ ShelleyBase, SpecTranslate (ExecContext fn rule era) (PredicateFailure (EraRule rule era)), Inject (ExecEnvironment fn rule era) (Environment (EraRule rule era)), Inject (ExecState fn rule era) (State (EraRule rule era)), Inject (ExecSignal fn rule era) (Signal (EraRule rule era))) ⇒ ExecSpecRule fn (rule ∷ Symbol) era where Source #

type ExecContext fn rule era Source #

type ExecContext fn rule era = ()

type ExecEnvironment fn rule era Source #

type ExecEnvironment fn rule era = Environment (EraRule rule era)

type ExecState fn rule era Source #

type ExecSignal fn rule era Source #

type ExecSignal fn rule era = Signal (EraRule rule era)

environmentSpec ∷ ExecContext fn rule era → Specification fn (ExecEnvironment fn rule era) Source #

stateSpec ∷ ExecContext fn rule era → ExecEnvironment fn rule era → Specification fn (ExecState fn rule era) Source #

signalSpec ∷ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → Specification fn (ExecSignal fn rule era) Source #

genExecContext ∷ Gen (ExecContext fn rule era) Source #

default genExecContext ∷ Arbitrary (ExecContext fn rule era) ⇒ Gen (ExecContext fn rule era) Source #

runAgdaRule ∷ SpecRep (ExecEnvironment fn rule era) → SpecRep (ExecState fn rule era) → SpecRep (ExecSignal fn rule era) → Either (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) (SpecRep (ExecState fn rule era)) Source #

translateInputs ∷ ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn rule era → ExecContext fn rule era → ImpTestM era (SpecRep (ExecEnvironment fn rule era), SpecRep (ExecState fn rule era), SpecRep (ExecSignal fn rule era)) Source #

default translateInputs ∷ (ForAllExecTypes (SpecTranslate (ExecContext fn rule era)) fn rule era, ForAllExecSpecRep ToExpr fn rule era) ⇒ ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn rule era → ExecContext fn rule era → ImpTestM era (SpecRep (ExecEnvironment fn rule era), SpecRep (ExecState fn rule era), SpecRep (ExecSignal fn rule era)) Source #

testConformance ∷ (ShelleyEraImp era, SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)), ForAllExecSpecRep NFData fn rule era, ForAllExecSpecRep ToExpr fn rule era, NFData (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (SpecRep (PredicateFailure (EraRule rule era))), Eq (SpecRep (PredicateFailure (EraRule rule era))), Eq (SpecRep (ExecState fn rule era)), Inject (State (EraRule rule era)) (ExecState fn rule era), SpecTranslate (ExecContext fn rule era) (ExecState fn rule era), FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))), FixupSpecRep (SpecRep (ExecState fn rule era))) ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn rule era → Property Source #

extraInfo ∷ ExecContext fn rule era → Environment (EraRule rule era) → State (EraRule rule era) → Signal (EraRule rule era) → String Source #

#### Instances

conformsToImpl ∷ ∀ (rule ∷ Symbol) fn era. (ShelleyEraImp era, ExecSpecRule fn rule era, ForAllExecSpecRep NFData fn rule era, ForAllExecSpecRep ToExpr fn rule era, NFData (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (ExecContext fn rule era), SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)), Eq (SpecRep (PredicateFailure (EraRule rule era))), Inject (State (EraRule rule era)) (ExecState fn rule era), Eq (SpecRep (ExecState fn rule era)), SpecTranslate (ExecContext fn rule era) (ExecState fn rule era), FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))), FixupSpecRep (SpecRep (ExecState fn rule era))) ⇒ Property Source #

computationResultToEither ∷ ComputationResult e a → Either e a Source #

runConformance ∷ ∀ (rule ∷ Symbol) (fn ∷ [Type] → Type → Type) era. (ExecSpecRule fn rule era, NFData (SpecRep (PredicateFailure (EraRule rule era))), ForAllExecSpecRep NFData fn rule era, ForAllExecSpecRep ToExpr fn rule era, FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))), FixupSpecRep (SpecRep (ExecState fn rule era)), Inject (State (EraRule rule era)) (ExecState fn rule era), SpecTranslate (ExecContext fn rule era) (ExecState fn rule era)) ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn rule era → ImpTestM era (Either (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) (SpecRep (ExecState fn rule era)), Either (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) (SpecRep (ExecState fn rule era))) Source #

checkConformance ∷ (ToExpr (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (SpecRep (ExecState fn rule era)), Eq (SpecRep (PredicateFailure (EraRule rule era))), Eq (SpecRep (ExecState fn rule era))) ⇒ Either (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) (SpecRep (ExecState fn rule era)) → Either (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) (SpecRep (ExecState fn rule era)) → ImpTestM era () Source #