Safe Haskell	Safe-Inferred
Language	Haskell2010

Constrained.Spec.Size

Contents

Orphan instances

Synopsis

genFromSizeSpec ∷ MonadGenError m ⇒ Specification Integer → GenT m Integer
data SizeW (s ∷ Symbol) (dom ∷ [Type]) rng ∷ Type where
- SizeOfW ∷ ∀ n. Sized n ⇒ SizeW "sizeOf_" '[n] Integer
sizeOfFn ∷ ∀ a. (HasSpec a, Sized a) ⇒ Fun '[a] Integer
sizeOf_ ∷ (HasSpec t, Sized t) ⇒ Term t → Term Integer
rangeSize ∷ Integer → Integer → SizeSpec
between ∷ (HasSpec a, TypeSpec a ~ NumSpec a) ⇒ a → a → Specification a
maxSpec ∷ Specification Integer → Specification Integer
type SizeSpec = NumSpec Integer
class Sized t where
- sizeOf ∷ t → Integer
- liftSizeSpec ∷ HasSpec t ⇒ SizeSpec → [Integer] → Specification t
- liftMemberSpec ∷ HasSpec t ⇒ [Integer] → Specification t
- sizeOfTypeSpec ∷ HasSpec t ⇒ TypeSpec t → Specification Integer
hasSize ∷ (HasSpec t, Sized t) ⇒ SizeSpec → Specification t

Documentation

genFromSizeSpec ∷ MonadGenError m ⇒ Specification Integer → GenT m Integer Source #

Because Sizes should always be >= 0, We provide this alternate generator that can be used to replace (genFromSpecT @Integer), to ensure this important property

data SizeW (s ∷ Symbol) (dom ∷ [Type]) rng ∷ Type where Source #

Constructors

SizeOfW ∷ ∀ n. Sized n ⇒ SizeW "sizeOf_" '[n] Integer

Instances

Instances details

Semantics SizeW Source #
Instance details Defined in Constrained.Spec.Size Methods semantics ∷ ∀ (s ∷ Symbol) (d ∷ [Type]) r. SizeW s d r → FunTy d r Source #
Syntax SizeW Source #
Instance details Defined in Constrained.Spec.Size Methods isInFix ∷ ∀ (s ∷ Symbol) (dom ∷ [Type]) rng. SizeW s dom rng → Bool Source # prettyWit ∷ ∀ (s ∷ Symbol) (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ SizeW s dom rng → List Term dom → Int → Maybe (Doc ann) Source #
(Sized t, HasSpec t) ⇒ Logic "sizeOf_" SizeW '[t] Integer Source #
Instance details Defined in Constrained.Spec.Size Methods info ∷ SizeW "sizeOf_" '[t] Integer → String Source # propagate ∷ Context "sizeOf_" SizeW '[t] Integer hole → Specification Integer → Specification hole Source # rewriteRules ∷ SizeW "sizeOf_" '[t] Integer → List Term '[t] → Evidence (AppRequires "sizeOf_" SizeW '[t] Integer) → Maybe (Term Integer) Source # mapTypeSpec ∷ ('[t] ~ '[a], Integer ~ b, HasSpec a, HasSpec b) ⇒ SizeW "sizeOf_" '[a] b → TypeSpec a → Specification b Source # saturate ∷ SizeW "sizeOf_" '[t] Bool → List Term '[t] → [Pred] Source #
Show (SizeW s d r) Source #
Instance details Defined in Constrained.Spec.Size Methods showsPrec ∷ Int → SizeW s d r → ShowS show ∷ SizeW s d r → String showList ∷ [SizeW s d r] → ShowS
Eq (SizeW s ds r) Source #
Instance details Defined in Constrained.Spec.Size Methods (==) ∷ SizeW s ds r → SizeW s ds r → Bool (/=) ∷ SizeW s ds r → SizeW s ds r → Bool

sizeOfFn ∷ ∀ a. (HasSpec a, Sized a) ⇒ Fun '[a] Integer Source #

sizeOf_ ∷ (HasSpec t, Sized t) ⇒ Term t → Term Integer Source #

rangeSize ∷ Integer → Integer → SizeSpec Source #

between ∷ (HasSpec a, TypeSpec a ~ NumSpec a) ⇒ a → a → Specification a Source #

maxSpec ∷ Specification Integer → Specification Integer Source #

The widest interval whose largest element is admitted by the original spec

type SizeSpec = NumSpec Integer Source #

class Sized t where Source #

Minimal complete definition

Nothing

Methods

sizeOf ∷ t → Integer Source #

default sizeOf ∷ (HasSimpleRep t, Sized (SimpleRep t)) ⇒ t → Integer Source #

liftSizeSpec ∷ HasSpec t ⇒ SizeSpec → [Integer] → Specification t Source #

default liftSizeSpec ∷ (HasSpec t, HasSimpleRep t, Sized (SimpleRep t), HasSpec (SimpleRep t), TypeSpec t ~ TypeSpec (SimpleRep t)) ⇒ SizeSpec → [Integer] → Specification t Source #

liftMemberSpec ∷ HasSpec t ⇒ [Integer] → Specification t Source #

default liftMemberSpec ∷ (HasSpec t, HasSpec (SimpleRep t), HasSimpleRep t, Sized (SimpleRep t), TypeSpec t ~ TypeSpec (SimpleRep t)) ⇒ [Integer] → Specification t Source #

sizeOfTypeSpec ∷ HasSpec t ⇒ TypeSpec t → Specification Integer Source #

default sizeOfTypeSpec ∷ (HasSpec (SimpleRep t), Sized (SimpleRep t), TypeSpec t ~ TypeSpec (SimpleRep t)) ⇒ TypeSpec t → Specification Integer Source #

Instances

Instances details

Ord a ⇒ Sized (Set a) Source #
Instance details Defined in Constrained.Spec.Set Methods sizeOf ∷ Set a → Integer Source # liftSizeSpec ∷ SizeSpec → [Integer] → Specification (Set a) Source # liftMemberSpec ∷ [Integer] → Specification (Set a) Source # sizeOfTypeSpec ∷ TypeSpec (Set a) → Specification Integer Source #
Sized [a] Source #
Instance details Defined in Constrained.Spec.ListFoldy Methods sizeOf ∷ [a] → Integer Source # liftSizeSpec ∷ SizeSpec → [Integer] → Specification [a] Source # liftMemberSpec ∷ [Integer] → Specification [a] Source # sizeOfTypeSpec ∷ TypeSpec [a] → Specification Integer Source #
Ord a ⇒ Sized (Map a b) Source #
Instance details Defined in Constrained.Spec.Map Methods sizeOf ∷ Map a b → Integer Source # liftSizeSpec ∷ SizeSpec → [Integer] → Specification (Map a b) Source # liftMemberSpec ∷ [Integer] → Specification (Map a b) Source # sizeOfTypeSpec ∷ TypeSpec (Map a b) → Specification Integer Source #

hasSize ∷ (HasSpec t, Sized t) ⇒ SizeSpec → Specification t Source #

Orphan instances

(Sized t, HasSpec t) ⇒ Logic "sizeOf_" SizeW '[t] Integer Source #

Instance details

Methods

info ∷ SizeW "sizeOf_" '[t] Integer → String Source #

propagate ∷ Context "sizeOf_" SizeW '[t] Integer hole → Specification Integer → Specification hole Source #

rewriteRules ∷ SizeW "sizeOf_" '[t] Integer → List Term '[t] → Evidence (AppRequires "sizeOf_" SizeW '[t] Integer) → Maybe (Term Integer) Source #

mapTypeSpec ∷ ('[t] ~ '[a], Integer ~ b, HasSpec a, HasSpec b) ⇒ SizeW "sizeOf_" '[a] b → TypeSpec a → Specification b Source #

saturate ∷ SizeW "sizeOf_" '[t] Bool → List Term '[t] → [Pred] Source #