Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- class FixupSpecRep a where
- fixup ∷ a → a
- class SpecTranslate ctx a where
- type SpecRep a ∷ Type
- toSpecRep ∷ a → SpecTransM ctx (SpecRep a)
- data SpecTransM ctx a
- type SpecTranslationError = Text
- newtype OpaqueErrorString = OpaqueErrorString String
- runSpecTransM ∷ ctx → SpecTransM ctx a → Either SpecTranslationError a
- toTestRep ∷ (SpecTranslate ctx a, FixupSpecRep (SpecRep a)) ⇒ a → SpecTransM ctx (SpecRep a)
- askCtx ∷ ∀ b ctx. Inject ctx b ⇒ SpecTransM ctx b
- withCtx ∷ ctx → SpecTransM ctx a → SpecTransM ctx' a
- 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
- type ExecContext fn rule era
- type ExecEnvironment fn rule era
- type ExecState fn rule era
- type ExecSignal fn rule era
- environmentSpec ∷ HasCallStack ⇒ ExecContext fn rule era → Specification fn (ExecEnvironment fn rule era)
- stateSpec ∷ HasCallStack ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → Specification fn (ExecState fn rule era)
- signalSpec ∷ HasCallStack ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → Specification fn (ExecSignal fn rule era)
- classOf ∷ ExecSignal fn rule era → Maybe String
- genExecContext ∷ HasCallStack ⇒ Gen (ExecContext fn rule era)
- runAgdaRule ∷ HasCallStack ⇒ 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))
- translateInputs ∷ HasCallStack ⇒ 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))
- 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)), 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)), EncCBOR (ExecContext fn rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), ToExpr (ExecContext fn rule era), HasCallStack) ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn rule era → Property
- extraInfo ∷ HasCallStack ⇒ ExecContext fn rule era → Environment (EraRule rule era) → State (EraRule rule era) → Signal (EraRule rule era) → Doc AnsiStyle
- checkConformance ∷ ∀ rule era fn. (Era era, ToExpr (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (SpecRep (ExecState fn rule era)), Eq (SpecRep (PredicateFailure (EraRule rule era))), Eq (SpecRep (ExecState fn rule era)), EncCBOR (ExecContext fn rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), HasCallStack) ⇒ ExecContext fn rule era → Environment (EraRule rule era) → State (EraRule rule era) → Signal (EraRule 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 ()
- defaultTestConformance ∷ ∀ fn era rule. (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))), 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)), EncCBOR (ExecContext fn rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), ToExpr (ExecContext fn rule era), HasCallStack) ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn rule era → Property
- 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), ToExpr (ExecContext fn rule era), HasCallStack) ⇒ 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)))
- 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))), NFData (ExecContext fn 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)), EncCBOR (ExecContext fn rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), HasCallStack) ⇒ Property
- generatesWithin ∷ ∀ a. (NFData a, ToExpr a, Typeable a, HasCallStack) ⇒ Gen a → Int → Spec
- inputsGenerateWithin ∷ ∀ (fn ∷ [Type] → Type → Type) (rule ∷ Symbol) era. ExecSpecRule fn rule era ⇒ Int → Spec
- translateWithContext ∷ SpecTranslate ctx a ⇒ ctx → a → ImpTestM era (SpecRep a)
- agdaHashToBytes ∷ Int → Integer → ByteString
- agdaHashToExpr ∷ Int → Integer → Expr
- hashToInteger ∷ Hash a b → Integer
- computationResultToEither ∷ ComputationResult e a → Either e a
Documentation
class FixupSpecRep a where Source #
Nothing
Instances
class SpecTranslate ctx a where Source #
toSpecRep ∷ a → SpecTransM ctx (SpecRep a) Source #
Instances
data SpecTransM ctx a Source #
Instances
type SpecTranslationError = Text Source #
newtype OpaqueErrorString Source #
OpaqueErrorString behaves like unit in comparisons, but contains an error string that can be displayed.
Instances
Generic OpaqueErrorString Source # | |
FixupSpecRep OpaqueErrorString Source # | |
NFData OpaqueErrorString Source # | |
Defined in Test.Cardano.Ledger.Conformance.SpecTranslate.Core rnf ∷ OpaqueErrorString → () Source # | |
Eq OpaqueErrorString Source # | |
ToExpr OpaqueErrorString Source # | |
type Rep OpaqueErrorString Source # | |
Defined in Test.Cardano.Ledger.Conformance.SpecTranslate.Core type Rep OpaqueErrorString = D1 ('MetaData "OpaqueErrorString" "Test.Cardano.Ledger.Conformance.SpecTranslate.Core" "cardano-ledger-conformance-0.1.0.0-inplace" 'True) (C1 ('MetaCons "OpaqueErrorString" 'PrefixI 'False) (S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) |
runSpecTransM ∷ ctx → SpecTransM ctx a → Either SpecTranslationError a Source #
toTestRep ∷ (SpecTranslate ctx a, FixupSpecRep (SpecRep a)) ⇒ a → SpecTransM ctx (SpecRep a) Source #
askCtx ∷ ∀ b ctx. Inject ctx b ⇒ SpecTransM ctx b Source #
withCtx ∷ ctx → SpecTransM ctx a → SpecTransM ctx' a Source #
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 ∷ HasCallStack ⇒ ExecContext fn rule era → Specification fn (ExecEnvironment fn rule era) Source #
stateSpec ∷ HasCallStack ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → Specification fn (ExecState fn rule era) Source #
signalSpec ∷ HasCallStack ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → Specification fn (ExecSignal fn rule era) Source #
classOf ∷ ExecSignal fn rule era → Maybe String Source #
genExecContext ∷ HasCallStack ⇒ Gen (ExecContext fn rule era) Source #
default genExecContext ∷ Arbitrary (ExecContext fn rule era) ⇒ Gen (ExecContext fn rule era) Source #
runAgdaRule ∷ HasCallStack ⇒ 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 ∷ HasCallStack ⇒ 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)), 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)), EncCBOR (ExecContext fn rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), ToExpr (ExecContext fn rule era), HasCallStack) ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn rule era → Property Source #
extraInfo ∷ HasCallStack ⇒ ExecContext fn rule era → Environment (EraRule rule era) → State (EraRule rule era) → Signal (EraRule rule era) → Doc AnsiStyle Source #
Instances
checkConformance ∷ ∀ rule era fn. (Era era, ToExpr (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (SpecRep (ExecState fn rule era)), Eq (SpecRep (PredicateFailure (EraRule rule era))), Eq (SpecRep (ExecState fn rule era)), EncCBOR (ExecContext fn rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), HasCallStack) ⇒ ExecContext fn rule era → Environment (EraRule rule era) → State (EraRule rule era) → Signal (EraRule 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 #
defaultTestConformance ∷ ∀ fn era rule. (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))), 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)), EncCBOR (ExecContext fn rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), ToExpr (ExecContext fn rule era), HasCallStack) ⇒ ExecContext fn rule era → ExecEnvironment fn rule era → ExecState fn rule era → ExecSignal fn rule era → Property 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), ToExpr (ExecContext fn rule era), HasCallStack) ⇒ 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 #
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))), NFData (ExecContext fn 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)), EncCBOR (ExecContext fn rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), HasCallStack) ⇒ Property Source #
generatesWithin ∷ ∀ a. (NFData a, ToExpr a, Typeable a, HasCallStack) ⇒ Gen a → Int → Spec Source #
inputsGenerateWithin ∷ ∀ (fn ∷ [Type] → Type → Type) (rule ∷ Symbol) era. ExecSpecRule fn rule era ⇒ Int → Spec Source #
translateWithContext ∷ SpecTranslate ctx a ⇒ ctx → a → ImpTestM era (SpecRep a) Source #
Translate a Haskell type a
whose translation context is ctx
into its Agda type, in the ImpTest monad.
agdaHashToBytes ∷ Int → Integer → ByteString Source #
hashToInteger ∷ Hash a b → Integer Source #
computationResultToEither ∷ ComputationResult e a → Either e a Source #