| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Test.Cardano.Ledger.Conformance
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 era
- type SpecEnvironment rule era
- type SpecState rule era
- type SpecSignal rule era
- runAgdaRule ∷ HasCallStack ⇒ SpecTRC rule era → Either Text (SpecState rule era)
- translateInputs ∷ HasCallStack ⇒ ExecContext rule era → TRC (EraRule rule era) → Either Text (SpecTRC rule era)
- translateOutput ∷ ExecContext rule era → TRC (EraRule rule era) → State (EraRule rule era) → Either Text (SpecState rule era)
- extraInfo ∷ HasCallStack ⇒ Globals → ExecContext rule era → TRC (EraRule rule era) → Either Text (State (EraRule rule era), [Event (EraRule rule era)]) → Doc AnsiStyle
- data ConformanceResult rule 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 era = SpecTRC {
- strcEnvironment ∷ SpecEnvironment rule era
- strcState ∷ SpecState rule era
- strcSignal ∷ SpecSignal rule era
- type ForAllExecSpecRep (c ∷ Type → Constraint) rule era = (c (SpecEnvironment rule era), c (SpecState rule era), c (SpecSignal rule era))
- type ForAllExecTypes (c ∷ Type → Constraint) rule era = (c (Environment (EraRule rule era)), c (State (EraRule rule era)), c (Signal (EraRule rule era)))
- class SpecNormalize a where
- specNormalize ∷ a → a
- class SpecTranslate ctx a where
- type SpecRep a ∷ Type
- toSpecRep ∷ a → SpecTransM ctx (SpecRep a)
- newtype OpaqueErrorString = OpaqueErrorString (NonEmpty Text)
- data SpecTransM ctx a
- generatesWithin ∷ ∀ a. (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 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 era. (HasCallStack, ExecSpecRule rule era) ⇒ ExecContext rule era → TRC (EraRule rule era) → Property
- translateWithContext ∷ SpecTranslate ctx a ⇒ ctx → a → ImpTestM era (Either Text (SpecRep a))
- diffConformance ∷ ToExpr a ⇒ Either Text a → Either Text a → Doc AnsiStyle
- runFromAgdaFunction ∷ (SpecEnvironment rule era → SpecState rule era → SpecSignal rule era → ComputationResult Text (SpecState rule era)) → SpecTRC rule era → Either Text (SpecState rule era)
- runSpecTransM ∷ ctx → SpecTransM ctx a → Either Text a
- unComputationResult ∷ ComputationResult Text a → Either Text a
- askCtx ∷ ∀ b ctx. Inject ctx b ⇒ SpecTransM ctx b
- withCtx ∷ ctx → SpecTransM ctx a → SpecTransM ctx' a
- unComputationResult_ ∷ ComputationResult Void a → Either e a
- toSpecRep_ ∷ SpecTranslate () a ⇒ a → SpecRep a
- agdaHashToBytes ∷ Int → Integer → ByteString
- integerToHash ∷ ∀ h a. HashAlgorithm h ⇒ Integer → Maybe (Hash h a)
- signatureFromInteger ∷ DSIGNAlgorithm v ⇒ Integer → Maybe (SigDSIGN v)
- vkeyFromInteger ∷ Integer → Maybe (VKey kd)
- committeeCredentialToStrictMaybe ∷ CommitteeAuthorization → StrictMaybe (Credential 'HotCommitteeRole)
- hashToInteger ∷ Hash a b → Integer
- vkeyToInteger ∷ VKey kd → Integer
- signatureToInteger ∷ DSIGNAlgorithm v ⇒ SigDSIGN v → Integer
- agdaHashToExpr ∷ Int → Integer → Expr
- unionsHSMap ∷ Ord k ⇒ [HSMap k v] → HSMap k v
- unionHSMap ∷ Ord k ⇒ HSMap k v → HSMap k v → HSMap k v
- mapHSMapKey ∷ (k → l) → HSMap k v → HSMap l v
- bimapMHSMap ∷ Applicative m ⇒ (k → m k') → (v → m v') → HSMap k v → m (HSMap k' v')
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
Associated Types
type ExecContext rule era Source #
type ExecContext rule era = ()
type SpecEnvironment rule era Source #
type SpecEnvironment rule era = SpecRep (Environment (EraRule rule era))
type SpecState rule era Source #
type SpecSignal rule era Source #
type SpecSignal rule era = SpecRep (Signal (EraRule rule era))
Methods
runAgdaRule ∷ HasCallStack ⇒ SpecTRC rule era → Either Text (SpecState rule era) Source #
translateInputs ∷ HasCallStack ⇒ ExecContext rule era → TRC (EraRule rule era) → Either Text (SpecTRC rule era) Source #
default translateInputs ∷ (SpecTranslate (ExecContext rule era) (Environment (EraRule rule era)), SpecTranslate (ExecContext rule era) (State (EraRule rule era)), SpecTranslate (ExecContext rule era) (Signal (EraRule rule era)), SpecRep (Environment (EraRule rule era)) ~ SpecEnvironment rule era, SpecRep (State (EraRule rule era)) ~ SpecState rule era, SpecRep (Signal (EraRule rule era)) ~ SpecSignal rule era) ⇒ ExecContext rule era → TRC (EraRule rule era) → Either Text (SpecTRC rule era) Source #
translateOutput ∷ ExecContext rule era → TRC (EraRule rule era) → State (EraRule rule era) → Either Text (SpecState rule era) Source #
default translateOutput ∷ (SpecTranslate (ExecContext rule era) (State (EraRule rule era)), SpecRep (State (EraRule rule era)) ~ SpecState rule era) ⇒ ExecContext rule era → TRC (EraRule rule era) → State (EraRule rule era) → Either Text (SpecState rule era) Source #
extraInfo ∷ HasCallStack ⇒ 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 era Source #
Constructors
| ConformanceResult | |
Fields
| |
Instances
data SpecTRC rule era Source #
Constructors
| SpecTRC | |
Fields
| |
Instances
| Generic (SpecTRC rule era) Source # | |
| ForAllExecSpecRep NFData rule era ⇒ NFData (SpecTRC rule era) Source # | |
| 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))))) | |
type ForAllExecSpecRep (c ∷ Type → Constraint) rule era = (c (SpecEnvironment rule era), c (SpecState rule era), c (SpecSignal rule era)) Source #
type ForAllExecTypes (c ∷ Type → Constraint) rule era = (c (Environment (EraRule rule era)), c (State (EraRule rule era)), c (Signal (EraRule rule era))) Source #
class SpecNormalize a where Source #
Minimal complete definition
Nothing
Methods
specNormalize ∷ a → a Source #
default specNormalize ∷ (Generic a, GSpecNormalize (Rep a)) ⇒ a → a Source #
Instances
class SpecTranslate ctx a where Source #
Methods
toSpecRep ∷ a → SpecTransM ctx (SpecRep a) Source #
Instances
newtype OpaqueErrorString Source #
OpaqueErrorString behaves like unit in comparisons, but contains an error string that can be displayed.
Constructors
| OpaqueErrorString (NonEmpty Text) |
Instances
data SpecTransM ctx a Source #
Instances
generatesWithin ∷ ∀ a. (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 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 era. (HasCallStack, ExecSpecRule rule era) ⇒ ExecContext rule era → TRC (EraRule rule era) → Property Source #
translateWithContext ∷ SpecTranslate ctx a ⇒ ctx → a → ImpTestM era (Either Text (SpecRep a)) Source #
Translate a Haskell type a whose translation context is ctx into its Agda type, in the ImpTest monad.
runFromAgdaFunction ∷ (SpecEnvironment rule era → SpecState rule era → SpecSignal rule era → ComputationResult Text (SpecState rule era)) → SpecTRC rule era → Either Text (SpecState rule era) Source #
runSpecTransM ∷ ctx → SpecTransM ctx a → Either Text a Source #
askCtx ∷ ∀ b ctx. Inject ctx b ⇒ SpecTransM ctx b Source #
withCtx ∷ ctx → SpecTransM ctx a → SpecTransM ctx' a Source #
unComputationResult_ ∷ ComputationResult Void a → Either e a Source #
toSpecRep_ ∷ SpecTranslate () a ⇒ a → SpecRep a Source #
agdaHashToBytes ∷ Int → Integer → ByteString Source #
integerToHash ∷ ∀ h a. HashAlgorithm h ⇒ Integer → Maybe (Hash h a) Source #
signatureFromInteger ∷ DSIGNAlgorithm v ⇒ Integer → Maybe (SigDSIGN v) Source #
committeeCredentialToStrictMaybe ∷ CommitteeAuthorization → StrictMaybe (Credential 'HotCommitteeRole) Source #
hashToInteger ∷ Hash a b → Integer Source #
vkeyToInteger ∷ VKey kd → Integer Source #
signatureToInteger ∷ DSIGNAlgorithm v ⇒ SigDSIGN v → Integer Source #
mapHSMapKey ∷ (k → l) → HSMap k v → HSMap l v Source #
bimapMHSMap ∷ Applicative m ⇒ (k → m k') → (v → m v') → HSMap k v → m (HSMap k' v') Source #