| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Test.Cardano.Ledger.Conformance
Synopsis
- newtype OpaqueErrorString = OpaqueErrorString (NonEmpty Text)
- 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
- 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
- showOpaqueErrorString ∷ ToExpr a ⇒ a → OpaqueErrorString
- unComputationResult ∷ ComputationResult Text a → Either OpaqueErrorString a
- unComputationResult_ ∷ ComputationResult Void a → Either e a
- class (ForAllExecTypes HasSpec rule era, ForAllExecTypes ToExpr rule era, ForAllExecTypes NFData rule era, KnownSymbol rule, STS (EraRule rule era), BaseM (EraRule rule era) ~ ShelleyBase, SpecTranslate (ExecContext rule era) (PredicateFailure (EraRule rule era)), Inject (ExecEnvironment rule era) (Environment (EraRule rule era)), Inject (ExecState rule era) (State (EraRule rule era)), Inject (ExecSignal rule era) (Signal (EraRule rule era))) ⇒ ExecSpecRule (rule ∷ Symbol) era where
- type ExecContext rule era
- type ExecEnvironment rule era
- type ExecState rule era
- type ExecSignal rule era
- environmentSpec ∷ HasCallStack ⇒ ExecContext rule era → Specification (ExecEnvironment rule era)
- stateSpec ∷ HasCallStack ⇒ ExecContext rule era → ExecEnvironment rule era → Specification (ExecState rule era)
- signalSpec ∷ HasCallStack ⇒ ExecContext rule era → ExecEnvironment rule era → ExecState rule era → Specification (ExecSignal rule era)
- classOf ∷ ExecSignal rule era → Maybe String
- genExecContext ∷ HasCallStack ⇒ Gen (ExecContext rule era)
- runAgdaRule ∷ HasCallStack ⇒ SpecRep (ExecEnvironment rule era) → SpecRep (ExecState rule era) → SpecRep (ExecSignal rule era) → Either OpaqueErrorString (SpecRep (ExecState rule era))
- translateInputs ∷ HasCallStack ⇒ ExecEnvironment rule era → ExecState rule era → ExecSignal rule era → ExecContext rule era → ImpTestM era (SpecRep (ExecEnvironment rule era), SpecRep (ExecState rule era), SpecRep (ExecSignal rule era))
- testConformance ∷ (ShelleyEraImp era, SpecTranslate (ExecContext rule era) (State (EraRule rule era)), ForAllExecSpecRep NFData rule era, ForAllExecSpecRep ToExpr rule era, NFData (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (SpecRep (PredicateFailure (EraRule rule era))), Eq (SpecRep (PredicateFailure (EraRule rule era))), Eq (SpecRep (ExecState rule era)), Inject (State (EraRule rule era)) (ExecState rule era), SpecTranslate (ExecContext rule era) (ExecState rule era), FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))), FixupSpecRep (SpecRep (ExecState rule era)), Inject (ExecEnvironment rule era) (Environment (EraRule rule era)), Inject (ExecState rule era) (State (EraRule rule era)), Inject (ExecSignal rule era) (Signal (EraRule rule era)), EncCBOR (ExecContext rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), ToExpr (ExecContext rule era), ToExpr (PredicateFailure (EraRule rule era)), NFData (PredicateFailure (EraRule rule era)), HasCallStack) ⇒ ExecContext rule era → ExecEnvironment rule era → ExecState rule era → ExecSignal rule era → Property
- extraInfo ∷ HasCallStack ⇒ Globals → ExecContext rule era → Environment (EraRule rule era) → State (EraRule rule era) → Signal (EraRule rule era) → Either OpaqueErrorString (State (EraRule rule era), [Event (EraRule rule era)]) → Doc AnsiStyle
- type ForAllExecSpecRep (c ∷ Type → Constraint) rule era = (c (SpecRep (ExecEnvironment rule era)), c (SpecRep (ExecState rule era)), c (SpecRep (ExecSignal rule era)))
- type ForAllExecTypes (c ∷ Type → Constraint) rule era = (c (ExecEnvironment rule era), c (ExecState rule era), c (ExecSignal rule era))
- diffConformance ∷ ToExpr a ⇒ a → a → Doc AnsiStyle
- checkConformance ∷ ∀ rule era. (Era era, ToExpr (SpecRep (ExecState rule era)), Eq (SpecRep (ExecState rule era)), EncCBOR (ExecContext rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), HasCallStack) ⇒ ExecContext rule era → Environment (EraRule rule era) → State (EraRule rule era) → Signal (EraRule rule era) → Either OpaqueErrorString (SpecRep (ExecState rule era)) → Either OpaqueErrorString (SpecRep (ExecState rule era)) → ImpTestM era ()
- defaultTestConformance ∷ ∀ era rule. (HasCallStack, ShelleyEraImp era, ExecSpecRule rule era, ForAllExecSpecRep NFData rule era, ForAllExecSpecRep ToExpr rule era, NFData (PredicateFailure (EraRule rule era)), Eq (SpecRep (ExecState rule era)), Inject (State (EraRule rule era)) (ExecState rule era), SpecTranslate (ExecContext rule era) (ExecState rule era), FixupSpecRep (SpecRep (ExecState rule era)), EncCBOR (ExecContext rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), ToExpr (ExecContext rule era), ToExpr (PredicateFailure (EraRule rule era))) ⇒ ExecContext rule era → ExecEnvironment rule era → ExecState rule era → ExecSignal rule era → Property
- runConformance ∷ ∀ (rule ∷ Symbol) era. (ExecSpecRule rule era, ForAllExecSpecRep NFData rule era, ForAllExecSpecRep ToExpr rule era, FixupSpecRep (SpecRep (ExecState rule era)), Inject (State (EraRule rule era)) (ExecState rule era), SpecTranslate (ExecContext rule era) (ExecState rule era), ToExpr (ExecContext rule era), HasCallStack, NFData (PredicateFailure (EraRule rule era))) ⇒ ExecContext rule era → ExecEnvironment rule era → ExecState rule era → ExecSignal rule era → ImpTestM era (Either (NonEmpty (PredicateFailure (EraRule rule era))) (SpecRep (ExecState rule era)), Either OpaqueErrorString (SpecRep (ExecState rule era)), Either (NonEmpty (PredicateFailure (EraRule rule era))) (State (EraRule rule era), [Event (EraRule rule era)]))
- conformsToImpl ∷ ∀ (rule ∷ Symbol) era. (ShelleyEraImp era, ExecSpecRule rule era, ForAllExecSpecRep NFData rule era, ForAllExecSpecRep ToExpr rule era, NFData (SpecRep (PredicateFailure (EraRule rule era))), NFData (ExecContext rule era), ToExpr (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (ExecContext rule era), SpecTranslate (ExecContext rule era) (State (EraRule rule era)), Eq (SpecRep (PredicateFailure (EraRule rule era))), Inject (State (EraRule rule era)) (ExecState rule era), Eq (SpecRep (ExecState rule era)), SpecTranslate (ExecContext rule era) (ExecState rule era), FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))), FixupSpecRep (SpecRep (ExecState rule era)), EncCBOR (ExecContext rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), HasCallStack, NFData (PredicateFailure (EraRule rule era)), ToExpr (PredicateFailure (EraRule rule era))) ⇒ Property
- generatesWithin ∷ ∀ a. (NFData a, ToExpr a, Typeable a, HasCallStack) ⇒ Gen a → Int → Spec
- inputsGenerateWithin ∷ ∀ (rule ∷ Symbol) era. ExecSpecRule rule era ⇒ Int → Spec
- translateWithContext ∷ SpecTranslate ctx a ⇒ ctx → a → ImpTestM era (SpecRep a)
- standardHashSize ∷ Int
- standardAddrHashSize ∷ Int
- agdaHashToBytes ∷ Int → Integer → ByteString
- agdaHashToExpr ∷ Int → Integer → Expr
- hashToInteger ∷ Hash a b → Integer
- integerToHash ∷ ∀ h a. HashAlgorithm h ⇒ Integer → Maybe (Hash h a)
Documentation
newtype OpaqueErrorString Source #
OpaqueErrorString behaves like unit in comparisons, but contains an error string that can be displayed.
Constructors
| OpaqueErrorString (NonEmpty Text) |
Instances
class FixupSpecRep a where Source #
Minimal complete definition
Nothing
Instances
class SpecTranslate ctx a where Source #
Methods
toSpecRep ∷ a → SpecTransM ctx (SpecRep a) Source #
Instances
data SpecTransM ctx a Source #
Instances
type SpecTranslationError = Text Source #
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 #
showOpaqueErrorString ∷ ToExpr a ⇒ a → OpaqueErrorString Source #
unComputationResult_ ∷ ComputationResult Void a → Either e a Source #
class (ForAllExecTypes HasSpec rule era, ForAllExecTypes ToExpr rule era, ForAllExecTypes NFData rule era, KnownSymbol rule, STS (EraRule rule era), BaseM (EraRule rule era) ~ ShelleyBase, SpecTranslate (ExecContext rule era) (PredicateFailure (EraRule rule era)), Inject (ExecEnvironment rule era) (Environment (EraRule rule era)), Inject (ExecState rule era) (State (EraRule rule era)), Inject (ExecSignal rule era) (Signal (EraRule rule era))) ⇒ ExecSpecRule (rule ∷ Symbol) era where Source #
Minimal complete definition
Associated Types
type ExecContext rule era Source #
type ExecContext rule era = ()
type ExecEnvironment rule era Source #
type ExecEnvironment rule era = Environment (EraRule rule era)
type ExecState rule era Source #
type ExecSignal rule era Source #
type ExecSignal rule era = Signal (EraRule rule era)
Methods
environmentSpec ∷ HasCallStack ⇒ ExecContext rule era → Specification (ExecEnvironment rule era) Source #
stateSpec ∷ HasCallStack ⇒ ExecContext rule era → ExecEnvironment rule era → Specification (ExecState rule era) Source #
signalSpec ∷ HasCallStack ⇒ ExecContext rule era → ExecEnvironment rule era → ExecState rule era → Specification (ExecSignal rule era) Source #
classOf ∷ ExecSignal rule era → Maybe String Source #
genExecContext ∷ HasCallStack ⇒ Gen (ExecContext rule era) Source #
default genExecContext ∷ Arbitrary (ExecContext rule era) ⇒ Gen (ExecContext rule era) Source #
runAgdaRule ∷ HasCallStack ⇒ SpecRep (ExecEnvironment rule era) → SpecRep (ExecState rule era) → SpecRep (ExecSignal rule era) → Either OpaqueErrorString (SpecRep (ExecState rule era)) Source #
translateInputs ∷ HasCallStack ⇒ ExecEnvironment rule era → ExecState rule era → ExecSignal rule era → ExecContext rule era → ImpTestM era (SpecRep (ExecEnvironment rule era), SpecRep (ExecState rule era), SpecRep (ExecSignal rule era)) Source #
default translateInputs ∷ (ForAllExecTypes (SpecTranslate (ExecContext rule era)) rule era, ForAllExecSpecRep ToExpr rule era) ⇒ ExecEnvironment rule era → ExecState rule era → ExecSignal rule era → ExecContext rule era → ImpTestM era (SpecRep (ExecEnvironment rule era), SpecRep (ExecState rule era), SpecRep (ExecSignal rule era)) Source #
testConformance ∷ (ShelleyEraImp era, SpecTranslate (ExecContext rule era) (State (EraRule rule era)), ForAllExecSpecRep NFData rule era, ForAllExecSpecRep ToExpr rule era, NFData (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (SpecRep (PredicateFailure (EraRule rule era))), Eq (SpecRep (PredicateFailure (EraRule rule era))), Eq (SpecRep (ExecState rule era)), Inject (State (EraRule rule era)) (ExecState rule era), SpecTranslate (ExecContext rule era) (ExecState rule era), FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))), FixupSpecRep (SpecRep (ExecState rule era)), Inject (ExecEnvironment rule era) (Environment (EraRule rule era)), Inject (ExecState rule era) (State (EraRule rule era)), Inject (ExecSignal rule era) (Signal (EraRule rule era)), EncCBOR (ExecContext rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), ToExpr (ExecContext rule era), ToExpr (PredicateFailure (EraRule rule era)), NFData (PredicateFailure (EraRule rule era)), HasCallStack) ⇒ ExecContext rule era → ExecEnvironment rule era → ExecState rule era → ExecSignal rule era → Property Source #
extraInfo ∷ HasCallStack ⇒ Globals → ExecContext rule era → Environment (EraRule rule era) → State (EraRule rule era) → Signal (EraRule rule era) → Either OpaqueErrorString (State (EraRule rule era), [Event (EraRule rule era)]) → Doc AnsiStyle Source #
Instances
type ForAllExecSpecRep (c ∷ Type → Constraint) rule era = (c (SpecRep (ExecEnvironment rule era)), c (SpecRep (ExecState rule era)), c (SpecRep (ExecSignal rule era))) Source #
type ForAllExecTypes (c ∷ Type → Constraint) rule era = (c (ExecEnvironment rule era), c (ExecState rule era), c (ExecSignal rule era)) Source #
checkConformance ∷ ∀ rule era. (Era era, ToExpr (SpecRep (ExecState rule era)), Eq (SpecRep (ExecState rule era)), EncCBOR (ExecContext rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), HasCallStack) ⇒ ExecContext rule era → Environment (EraRule rule era) → State (EraRule rule era) → Signal (EraRule rule era) → Either OpaqueErrorString (SpecRep (ExecState rule era)) → Either OpaqueErrorString (SpecRep (ExecState rule era)) → ImpTestM era () Source #
defaultTestConformance ∷ ∀ era rule. (HasCallStack, ShelleyEraImp era, ExecSpecRule rule era, ForAllExecSpecRep NFData rule era, ForAllExecSpecRep ToExpr rule era, NFData (PredicateFailure (EraRule rule era)), Eq (SpecRep (ExecState rule era)), Inject (State (EraRule rule era)) (ExecState rule era), SpecTranslate (ExecContext rule era) (ExecState rule era), FixupSpecRep (SpecRep (ExecState rule era)), EncCBOR (ExecContext rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), ToExpr (ExecContext rule era), ToExpr (PredicateFailure (EraRule rule era))) ⇒ ExecContext rule era → ExecEnvironment rule era → ExecState rule era → ExecSignal rule era → Property Source #
runConformance ∷ ∀ (rule ∷ Symbol) era. (ExecSpecRule rule era, ForAllExecSpecRep NFData rule era, ForAllExecSpecRep ToExpr rule era, FixupSpecRep (SpecRep (ExecState rule era)), Inject (State (EraRule rule era)) (ExecState rule era), SpecTranslate (ExecContext rule era) (ExecState rule era), ToExpr (ExecContext rule era), HasCallStack, NFData (PredicateFailure (EraRule rule era))) ⇒ ExecContext rule era → ExecEnvironment rule era → ExecState rule era → ExecSignal rule era → ImpTestM era (Either (NonEmpty (PredicateFailure (EraRule rule era))) (SpecRep (ExecState rule era)), Either OpaqueErrorString (SpecRep (ExecState rule era)), Either (NonEmpty (PredicateFailure (EraRule rule era))) (State (EraRule rule era), [Event (EraRule rule era)])) Source #
conformsToImpl ∷ ∀ (rule ∷ Symbol) era. (ShelleyEraImp era, ExecSpecRule rule era, ForAllExecSpecRep NFData rule era, ForAllExecSpecRep ToExpr rule era, NFData (SpecRep (PredicateFailure (EraRule rule era))), NFData (ExecContext rule era), ToExpr (SpecRep (PredicateFailure (EraRule rule era))), ToExpr (ExecContext rule era), SpecTranslate (ExecContext rule era) (State (EraRule rule era)), Eq (SpecRep (PredicateFailure (EraRule rule era))), Inject (State (EraRule rule era)) (ExecState rule era), Eq (SpecRep (ExecState rule era)), SpecTranslate (ExecContext rule era) (ExecState rule era), FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))), FixupSpecRep (SpecRep (ExecState rule era)), EncCBOR (ExecContext rule era), EncCBOR (Environment (EraRule rule era)), EncCBOR (State (EraRule rule era)), EncCBOR (Signal (EraRule rule era)), HasCallStack, NFData (PredicateFailure (EraRule rule era)), ToExpr (PredicateFailure (EraRule rule era))) ⇒ Property Source #
generatesWithin ∷ ∀ a. (NFData a, ToExpr a, Typeable a, HasCallStack) ⇒ Gen a → Int → Spec Source #
inputsGenerateWithin ∷ ∀ (rule ∷ Symbol) era. ExecSpecRule 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 #
integerToHash ∷ ∀ h a. HashAlgorithm h ⇒ Integer → Maybe (Hash h a) Source #