| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Test.Cardano.Ledger.Conformance.ExecSpecRule.Core
Synopsis
- class (ShelleyEraImp era, STS (EraRule rule era), BaseM (EraRule rule era) ~ ShelleyBase, KnownSymbol rule, ForAllExecSpecRep NFData rule era, ForAllExecSpecRep ToExpr rule era, ForAllExecTypes NFData rule era, ForAllExecTypes ToExpr rule era, ForAllExecTypes EncCBOR rule era, EncCBOR (ExecContext rule era), Eq (SpecState rule era), SpecNormalize (SpecState rule era), NFData (ExecContext rule era), NFData (PredicateFailure (EraRule rule era)), NFData (SpecTRC rule era), ToExpr (ExecContext rule era), ToExpr (PredicateFailure (EraRule rule era))) ⇒ ExecSpecRule (rule ∷ Symbol) era where
- type ExecContext (rule ∷ Symbol) era
- type SpecEnvironment (rule ∷ Symbol) era
- type SpecState (rule ∷ Symbol) era
- type SpecSignal (rule ∷ Symbol) era
- runAgdaRule ∷ SpecTRC rule era → Either Text (SpecState rule era)
- runAgdaRuleWithDebug ∷ SpecTRC rule era → Either Text (SpecState rule era, Text)
- translateInputs ∷ TRC (EraRule rule era) → SpecTransM era (ExecContext rule era) (SpecTRC rule era)
- translateOutput ∷ TRC (EraRule rule era) → State (EraRule rule era) → SpecTransM era (ExecContext rule era) (SpecState rule era)
- extraInfo ∷ Globals → ExecContext rule era → TRC (EraRule rule era) → Either Text (State (EraRule rule era), [Event (EraRule rule era)]) → Doc AnsiStyle
- data ConformanceResult (rule ∷ Symbol) era = ConformanceResult {
- crTranslationResult ∷ Either (NonEmpty (PredicateFailure (EraRule rule era))) (SpecState rule era)
- crSpecificationResult ∷ Either Text (SpecState rule era)
- crImplementationResult ∷ Either (NonEmpty (PredicateFailure (EraRule rule era))) (State (EraRule rule era), [Event (EraRule rule era)])
- data SpecTRC (rule ∷ Symbol) era = SpecTRC {
- strcEnvironment ∷ SpecEnvironment rule era
- strcState ∷ SpecState rule era
- strcSignal ∷ SpecSignal rule era
- generatesWithin ∷ (NFData a, ToExpr a, Typeable a, HasCallStack) ⇒ Gen a → Int → Spec
- runConformance ∷ ∀ (rule ∷ Symbol) era. ExecSpecRule rule era ⇒ ExecContext rule era → TRC (EraRule rule era) → ImpTestM era (ConformanceResult rule era)
- checkConformance ∷ ∀ (rule ∷ Symbol) era. (HasCallStack, Era era, EncCBOR (ExecContext rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), ToExpr (SpecState rule era), Eq (SpecState rule era), SpecNormalize (SpecState rule era)) ⇒ ExecContext rule era → TRC (EraRule rule era) → Either Text (SpecState rule era) → Either Text (SpecState rule era) → ImpTestM era ()
- testConformance ∷ ∀ (rule ∷ Symbol) era. (HasCallStack, ExecSpecRule rule era) ⇒ ExecContext rule era → TRC (EraRule rule era) → Property
- translateWithContext ∷ SpecTranslate era a ⇒ SpecContext era a → a → ImpTestM era (Either Text (SpecRep era a))
- type ForAllExecSpecRep (c ∷ Type → Constraint) (rule ∷ Symbol) era = (c (SpecEnvironment rule era), c (SpecState rule era), c (SpecSignal rule era))
- type ForAllExecTypes (c ∷ Type → Constraint) (rule ∷ Symbol) era = (c (Environment (EraRule rule era)), c (State (EraRule rule era)), c (Signal (EraRule rule era)))
- diffConformance ∷ ToExpr a ⇒ Either Text a → Either Text a → Doc AnsiStyle
- runFromAgdaFunction ∷ ∀ (rule ∷ Symbol) era. (SpecEnvironment rule era → SpecState rule era → SpecSignal rule era → ComputationResult Text (SpecState rule era)) → SpecTRC rule era → Either Text (SpecState rule era)
Documentation
class (ShelleyEraImp era, STS (EraRule rule era), BaseM (EraRule rule era) ~ ShelleyBase, KnownSymbol rule, ForAllExecSpecRep NFData rule era, ForAllExecSpecRep ToExpr rule era, ForAllExecTypes NFData rule era, ForAllExecTypes ToExpr rule era, ForAllExecTypes EncCBOR rule era, EncCBOR (ExecContext rule era), Eq (SpecState rule era), SpecNormalize (SpecState rule era), NFData (ExecContext rule era), NFData (PredicateFailure (EraRule rule era)), NFData (SpecTRC rule era), ToExpr (ExecContext rule era), ToExpr (PredicateFailure (EraRule rule era))) ⇒ ExecSpecRule (rule ∷ Symbol) era where Source #
Minimal complete definition
Nothing
Associated Types
type ExecContext (rule ∷ Symbol) era Source #
type ExecContext (rule ∷ Symbol) era = ()
type SpecEnvironment (rule ∷ Symbol) era Source #
type SpecEnvironment (rule ∷ Symbol) era = SpecRep era (Environment (EraRule rule era))
type SpecState (rule ∷ Symbol) era Source #
type SpecSignal (rule ∷ Symbol) era Source #
type SpecSignal (rule ∷ Symbol) era = SpecRep era (Signal (EraRule rule era))
Methods
runAgdaRule ∷ SpecTRC rule era → Either Text (SpecState rule era) Source #
runAgdaRuleWithDebug ∷ SpecTRC rule era → Either Text (SpecState rule era, Text) Source #
translateInputs ∷ TRC (EraRule rule era) → SpecTransM era (ExecContext rule era) (SpecTRC rule era) Source #
default translateInputs ∷ (SpecTranslate era (Environment (EraRule rule era)), SpecTranslate era (State (EraRule rule era)), SpecTranslate era (Signal (EraRule rule era)), SpecContext era (Environment (EraRule rule era)) ~ ExecContext rule era, SpecContext era (State (EraRule rule era)) ~ ExecContext rule era, SpecContext era (Signal (EraRule rule era)) ~ ExecContext rule era, SpecRep era (Environment (EraRule rule era)) ~ SpecEnvironment rule era, SpecRep era (State (EraRule rule era)) ~ SpecState rule era, SpecRep era (Signal (EraRule rule era)) ~ SpecSignal rule era) ⇒ TRC (EraRule rule era) → SpecTransM era (ExecContext rule era) (SpecTRC rule era) Source #
translateOutput ∷ TRC (EraRule rule era) → State (EraRule rule era) → SpecTransM era (ExecContext rule era) (SpecState rule era) Source #
default translateOutput ∷ (SpecTranslate era (State (EraRule rule era)), SpecContext era (State (EraRule rule era)) ~ (), SpecRep era (State (EraRule rule era)) ~ SpecState rule era) ⇒ TRC (EraRule rule era) → State (EraRule rule era) → SpecTransM era (ExecContext rule era) (SpecState rule era) Source #
extraInfo ∷ Globals → ExecContext rule era → TRC (EraRule rule era) → Either Text (State (EraRule rule era), [Event (EraRule rule era)]) → Doc AnsiStyle Source #
Instances
data ConformanceResult (rule ∷ Symbol) era Source #
Constructors
| ConformanceResult | |
Fields
| |
Instances
| Generic (ConformanceResult rule era) Source # | |||||
Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Core Associated Types
Methods from ∷ ConformanceResult rule era → Rep (ConformanceResult rule era) x # to ∷ Rep (ConformanceResult rule era) x → ConformanceResult rule era # | |||||
| (Show (SpecState rule era), Show (PredicateFailure (EraRule rule era)), Show (State (EraRule rule era)), Show (Event (EraRule rule era))) ⇒ Show (ConformanceResult rule era) Source # | |||||
Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Core Methods showsPrec ∷ Int → ConformanceResult rule era → ShowS # show ∷ ConformanceResult rule era → String # showList ∷ [ConformanceResult rule era] → ShowS # | |||||
| (ToExpr (SpecState rule era), ToExpr (PredicateFailure (EraRule rule era)), ToExpr (State (EraRule rule era)), ToExpr (Event (EraRule rule era))) ⇒ ToExpr (ConformanceResult rule era) Source # | |||||
Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Core Methods toExpr ∷ ConformanceResult rule era → Expr Source # listToExpr ∷ [ConformanceResult rule era] → Expr Source # | |||||
| type Rep (ConformanceResult rule era) Source # | |||||
Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Core type Rep (ConformanceResult rule era) = D1 ('MetaData "ConformanceResult" "Test.Cardano.Ledger.Conformance.ExecSpecRule.Core" "cardano-ledger-conformance-9.9.9.9-inplace" 'False) (C1 ('MetaCons "ConformanceResult" 'PrefixI 'True) (S1 ('MetaSel ('Just "crTranslationResult") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Either (NonEmpty (PredicateFailure (EraRule rule era))) (SpecState rule era))) :*: (S1 ('MetaSel ('Just "crSpecificationResult") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Either Text (SpecState rule era))) :*: S1 ('MetaSel ('Just "crImplementationResult") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Either (NonEmpty (PredicateFailure (EraRule rule era))) (State (EraRule rule era), [Event (EraRule rule era)])))))) | |||||
data SpecTRC (rule ∷ Symbol) era Source #
Constructors
| SpecTRC | |
Fields
| |
Instances
| ForAllExecSpecRep NFData rule era ⇒ NFData (SpecTRC rule era) Source # | |||||
| Generic (SpecTRC rule era) Source # | |||||
Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Core Associated Types
| |||||
| ForAllExecSpecRep Eq rule era ⇒ Eq (SpecTRC rule era) Source # | |||||
| ForAllExecSpecRep ToExpr rule era ⇒ ToExpr (SpecTRC rule era) Source # | |||||
| type Rep (SpecTRC rule era) Source # | |||||
Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Core type Rep (SpecTRC rule era) = D1 ('MetaData "SpecTRC" "Test.Cardano.Ledger.Conformance.ExecSpecRule.Core" "cardano-ledger-conformance-9.9.9.9-inplace" 'False) (C1 ('MetaCons "SpecTRC" 'PrefixI 'True) (S1 ('MetaSel ('Just "strcEnvironment") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (SpecEnvironment rule era)) :*: (S1 ('MetaSel ('Just "strcState") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (SpecState rule era)) :*: S1 ('MetaSel ('Just "strcSignal") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (SpecSignal rule era))))) | |||||
generatesWithin ∷ (NFData a, ToExpr a, Typeable a, HasCallStack) ⇒ Gen a → Int → Spec Source #
runConformance ∷ ∀ (rule ∷ Symbol) era. ExecSpecRule rule era ⇒ ExecContext rule era → TRC (EraRule rule era) → ImpTestM era (ConformanceResult rule era) Source #
checkConformance ∷ ∀ (rule ∷ Symbol) era. (HasCallStack, Era era, EncCBOR (ExecContext rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), ToExpr (SpecState rule era), Eq (SpecState rule era), SpecNormalize (SpecState rule era)) ⇒ ExecContext rule era → TRC (EraRule rule era) → Either Text (SpecState rule era) → Either Text (SpecState rule era) → ImpTestM era () Source #
testConformance ∷ ∀ (rule ∷ Symbol) era. (HasCallStack, ExecSpecRule rule era) ⇒ ExecContext rule era → TRC (EraRule rule era) → Property Source #
translateWithContext ∷ SpecTranslate era a ⇒ SpecContext era a → a → ImpTestM era (Either Text (SpecRep era a)) Source #
Translate a Haskell type a whose translation context is ctx into its Agda type, in the ImpTest monad.
type ForAllExecSpecRep (c ∷ Type → Constraint) (rule ∷ Symbol) era = (c (SpecEnvironment rule era), c (SpecState rule era), c (SpecSignal rule era)) Source #
type ForAllExecTypes (c ∷ Type → Constraint) (rule ∷ Symbol) era = (c (Environment (EraRule rule era)), c (State (EraRule rule era)), c (Signal (EraRule rule era))) Source #
runFromAgdaFunction ∷ ∀ (rule ∷ Symbol) era. (SpecEnvironment rule era → SpecState rule era → SpecSignal rule era → ComputationResult Text (SpecState rule era)) → SpecTRC rule era → Either Text (SpecState rule era) Source #