Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- data GenEnv era = GenEnv {}
- type Depth = Int
- addVar ∷ V era t → t → GenEnv era → GenEnv era
- markSolved ∷ HashSet (Name era) → Depth → GenEnv era → GenEnv era
- addSolvedVar ∷ V era t → t → Depth → GenEnv era → GenEnv era
- depthOfName ∷ GenEnv era → Name era → Depth
- depthOf ∷ GenEnv era → Term era t → Depth
- depthOfSum ∷ GenEnv era → Sum era c → Depth
- genLiteral ∷ ∀ era t. Era era ⇒ GenEnv era → Rep era t → Gen t
- genFreshVarName ∷ GenEnv era → Gen String
- envVarsOfType ∷ Era era ⇒ Env era → Rep era t → [(V era t, t)]
- data VarSpec
- genTerm ∷ Era era ⇒ GenEnv era → Rep era t → VarSpec → Gen (Term era t, GenEnv era)
- genTerm' ∷ ∀ era t. Era era ⇒ GenEnv era → Rep era t → (t → Bool) → Gen t → VarSpec → Gen (Term era t, GenEnv era)
- genMapLiteralWithDom ∷ Era era ⇒ GenEnv era → Rep era v → Set k → Gen (Map k v)
- genMapLiteralWithRng ∷ (Era era, Ord k) ⇒ GenEnv era → Rep era k → Set v → Gen (Map k v)
- data TypeInEra era where
- genKeyType ∷ Gen (TypeInEra era)
- genValType ∷ Gen (TypeInEra era)
- genBaseType ∷ Gen (TypeInEra era)
- genType ∷ Gen (TypeInEra era)
- errPred ∷ [String] → Pred era
- setWithSum ∷ Int → Gen (Set Int)
- listWithSum ∷ Coin → Gen [Coin]
- mapWithSum ∷ Coin → Gen (Map Coin Coin)
- genFromOrdCond ∷ (Arbitrary c, Adds c) ⇒ OrdCond → Bool → c → Gen c
- genPredicate ∷ ∀ era. Era era ⇒ GenEnv era → Gen (Pred era, GenEnv era)
- genPreds ∷ Era era ⇒ GenEnv era → Gen ([Pred era], GenEnv era)
- withEq ∷ Rep era t → (Eq t ⇒ a) → Maybe a
- shrinkPreds ∷ ∀ era. Era era ⇒ ([Pred era], GenEnv era) → [([Pred era], GenEnv era)]
- testProof ∷ Proof ShelleyEra
- testEnv ∷ Env ShelleyEra
- ensureRight ∷ Testable prop ⇒ Either [String] a → (a → prop) → Property
- ifRight ∷ Testable prop ⇒ Either [String] a → (a → prop) → Property
- ensureTyped ∷ Testable prop ⇒ Typed a → (a → prop) → Property
- ifTyped ∷ Testable prop ⇒ Typed a → (a → prop) → Property
- initEnv ∷ OrderInfo → GenEnv ShelleyEra
- showVal ∷ Rep era t → t → String
- showTerm ∷ Term era t → String
- showPred ∷ Pred era → String
- showEnv ∷ Env era → String
- predConstr ∷ Pred era → String
- constraintProperty ∷ Bool → [String] → OrderInfo → ([Pred ShelleyEra] → DependGraph ShelleyEra → Env ShelleyEra → Property) → Property
- checkPredicates ∷ [Pred era] → Env era → Property
- runPreds ∷ [Pred ShelleyEra] → IO ()
- prop_soundness ∷ OrderInfo → Property
- defaultWhitelist ∷ [String]
- prop_soundness' ∷ Bool → [String] → OrderInfo → Property
- prop_shrinking ∷ OrderInfo → Property
- prop_shrinking' ∷ Bool → [String] → OrderInfo → Property
Documentation
VarTerm Depth | Must contain a variable (either unsolved, or solved at least the given depth). Requiring a minimum depth let's us avoid introducing cycles in already solved variables. |
KnownTerm | Can only use solved variables |
genTerm' ∷ ∀ era t. Era era ⇒ GenEnv era → Rep era t → (t → Bool) → Gen t → VarSpec → Gen (Term era t, GenEnv era) Source #
genKeyType ∷ Gen (TypeInEra era) Source #
genValType ∷ Gen (TypeInEra era) Source #
genBaseType ∷ Gen (TypeInEra era) Source #
errPred ∷ [String] → Pred era Source #
Unsatisfiable constraint returned if we fail during constraint generation.
predConstr ∷ Pred era → String Source #
constraintProperty ∷ Bool → [String] → OrderInfo → ([Pred ShelleyEra] → DependGraph ShelleyEra → Env ShelleyEra → Property) → Property Source #
prop_soundness ∷ OrderInfo → Property Source #
Generate a set of satisfiable constraints and check that we can generate a solution and that it actually satisfies the constraints.
prop_soundness' ∷ Bool → [String] → OrderInfo → Property Source #
If argument is True, fail property if constraints cannot be solved. Otherwise discard unsolved constraints.
prop_shrinking ∷ OrderInfo → Property Source #
Check that shrinking is sound, i.e. that all shrink steps preserves constraint satisfaction.