| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Constrained.API
Synopsis
- data PredD deps where
- ElemPred ∷ (HasSpecD deps a, Show a) ⇒ Bool → TermD deps a → NonEmpty a → PredD deps
- Monitor ∷ ((∀ a. TermD deps a → a) → Property → Property) → PredD deps
- And ∷ [PredD deps] → PredD deps
- Exists ∷ ((∀ b. TermD deps b → b) → GE a) → BinderD deps a → PredD deps
- Subst ∷ (HasSpecD deps a, Show a) ⇒ Var a → TermD deps a → PredD deps → PredD deps
- Let ∷ TermD deps a → BinderD deps a → PredD deps
- Assert ∷ TermD deps Bool → PredD deps
- Reifies ∷ (HasSpecD deps a, HasSpecD deps b, Show a, Show b) ⇒ TermD deps b → TermD deps a → (a → b) → PredD deps
- DependsOn ∷ (HasSpecD deps a, HasSpecD deps b, Show a, Show b) ⇒ TermD deps a → TermD deps b → PredD deps
- ForAll ∷ (ForallableD deps t e, HasSpecD deps t, HasSpecD deps e, Show t, Show e) ⇒ TermD deps t → BinderD deps e → PredD deps
- Case ∷ (HasSpecD deps (SumOver as), Show (SumOver as)) ⇒ TermD deps (SumOver as) → List (Weighted (BinderD deps)) as → PredD deps
- When ∷ TermD deps Bool → PredD deps → PredD deps
- GenHint ∷ (HasGenHintD deps a, Show a, Show (HintD deps a)) ⇒ HintD deps a → TermD deps a → PredD deps
- TruePred ∷ PredD deps
- FalsePred ∷ NonEmpty String → PredD deps
- Explain ∷ NonEmpty String → PredD deps → PredD deps
- data TermD deps a where
- data SpecificationD deps a where
- ExplainSpec ∷ [String] → SpecificationD deps a → SpecificationD deps a
- MemberSpec ∷ NonEmpty a → SpecificationD deps a
- ErrorSpec ∷ NonEmpty String → SpecificationD deps a
- SuspendedSpec ∷ HasSpecD deps a ⇒ Var a → PredD deps → SpecificationD deps a
- TypeSpecD ∷ HasSpecD deps a ⇒ TypeSpecD deps a → [a] → SpecificationD deps a
- TrueSpec ∷ SpecificationD deps a
- type GenericallyInstantiated a = (AssertComputes (SimpleRep a) (((Text "Trying to use a generic instantiation of " :<>: ShowType a) :<>: Text ", likely in a HasSpec instance.") :$$: Text "However, the type has no definition of SimpleRep, likely because of a missing instance of HasSimpleRep."), HasSimpleRep a, HasSpec (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a))
- class (Typeable t, Semantics t, Syntax t) ⇒ Logic t where
- propagateTypeSpec ∷ (AppRequires t as b, HasSpec a) ⇒ t as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a
- propagateMemberSpec ∷ (AppRequires t as b, HasSpec a) ⇒ t as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a
- propagate ∷ (AppRequires t as b, HasSpec a) ⇒ t as b → ListCtx Value as (HOLE a) → Specification b → Specification a
- rewriteRules ∷ (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ t dom rng → List Term dom → Evidence (AppRequires t dom rng) → Maybe (Term rng)
- mapTypeSpec ∷ ∀ a b. (HasSpec a, HasSpec b) ⇒ t '[a] b → TypeSpec a → Specification b
- saturate ∷ t dom Bool → List Term dom → [Pred]
- class Semantics (t ∷ [Type] → Type → Type) where
- class Syntax (t ∷ [Type] → Type → Type) where
- class (HasSpec a, NumLike a, Logic IntW) ⇒ Foldy a where
- genList ∷ MonadGenError m ⇒ Specification a → Specification a → GenT m [a]
- theAddFn ∷ IntW '[a, a] a
- theZero ∷ a
- genSizedList ∷ MonadGenError m ⇒ Specification Integer → Specification a → Specification a → GenT m [a]
- noNegativeValues ∷ Bool
- data NumSpec n = NumSpecInterval (Maybe n) (Maybe n)
- class MaybeBounded a where
- lowerBound ∷ Maybe a
- upperBound ∷ Maybe a
- data NonEmpty a = a :| [a]
- type Specification = SpecificationD Deps
- pattern TypeSpec ∷ () ⇒ HasSpec a ⇒ TypeSpec a → [a] → Specification a
- type Term = TermD Deps
- data Fun dom rng where
- Fun ∷ ∀ t dom rng. AppRequires t dom rng ⇒ t dom rng → Fun dom rng
- name ∷ String → Term a → Term a
- named ∷ String → Term a → Term a
- type Pred = PredD Deps
- class (Typeable a, Eq a, Show a, TypeSpecEqShow a) ⇒ HasSpec a where
- type TypeSpec a
- type Prerequisites a ∷ Constraint
- emptySpec ∷ TypeSpec a
- combineSpec ∷ TypeSpec a → TypeSpec a → Specification a
- genFromTypeSpec ∷ (HasCallStack, MonadGenError m) ⇒ TypeSpec a → GenT m a
- conformsTo ∷ HasCallStack ⇒ a → TypeSpec a → Bool
- shrinkWithTypeSpec ∷ TypeSpec a → a → [a]
- toPreds ∷ Term a → TypeSpec a → Pred
- cardinalTypeSpec ∷ TypeSpec a → Specification Integer
- cardinalTrueSpec ∷ Specification Integer
- typeSpecHasError ∷ TypeSpec a → Maybe (NonEmpty String)
- alternateShow ∷ TypeSpec a → BinaryShow
- monadConformsTo ∷ a → TypeSpec a → Writer [String] Bool
- typeSpecOpt ∷ TypeSpec a → [a] → Specification a
- guardTypeSpec ∷ [String] → TypeSpec a → Specification a
- prerequisites ∷ Evidence (Prerequisites a)
- class Typeable (SimpleRep a) ⇒ HasSimpleRep a where
- type SimpleRep a
- type TheSop a ∷ [Type]
- toSimpleRep ∷ a → SimpleRep a
- fromSimpleRep ∷ SimpleRep a → a
- class (Ord a, HasSpec a) ⇒ OrdLike a where
- leqSpec ∷ a → Specification a
- ltSpec ∷ a → Specification a
- geqSpec ∷ a → Specification a
- gtSpec ∷ a → Specification a
- conformsToSpecE ∷ ∀ a. HasSpec a ⇒ a → Specification a → NonEmpty String → Maybe (NonEmpty String)
- conformsToSpec ∷ HasSpec a ⇒ a → Specification a → Bool
- satisfies ∷ ∀ a. HasSpec a ⇒ Term a → Specification a → Pred
- genFromSpecT ∷ ∀ a m. (HasCallStack, HasSpec a, MonadGenError m) ⇒ Specification a → GenT m a
- genFromSpec ∷ ∀ a. (HasCallStack, HasSpec a) ⇒ Specification a → Gen a
- debugSpec ∷ ∀ a. HasSpec a ⇒ Specification a → IO ()
- genFromSpecWithSeed ∷ ∀ a. (HasCallStack, HasSpec a) ⇒ Int → Int → Specification a → a
- simplifySpec ∷ HasSpec a ⇒ Specification a → Specification a
- cardinality ∷ ∀ a. (Number Integer, HasSpec a) ⇒ Specification a → Specification Integer
- ifElse ∷ (IsPred p, IsPred q) ⇒ Term Bool → p → q → Pred
- whenTrue ∷ ∀ p. IsPred p ⇒ Term Bool → p → Pred
- simplifyTerm ∷ ∀ a. Term a → Term a
- constrained ∷ ∀ a p. (IsPred p, HasSpec a) ⇒ (Term a → p) → Specification a
- assertExplain ∷ IsPred p ⇒ NonEmpty String → p → Pred
- assert ∷ IsPred p ⇒ p → Pred
- forAll ∷ (Forallable t a, HasSpec t, HasSpec a, IsPred p) ⇒ Term t → (Term a → p) → Pred
- exists ∷ ∀ a p. (HasSpec a, IsPred p) ⇒ ((∀ b. Term b → b) → GE a) → (Term a → p) → Pred
- unsafeExists ∷ ∀ a p. (HasSpec a, IsPred p) ⇒ (Term a → p) → Pred
- letBind ∷ (HasSpec a, IsPred p) ⇒ Term a → (Term a → p) → Pred
- reify ∷ (HasSpec a, HasSpec b, IsPred p) ⇒ Term a → (a → b) → (Term b → p) → Pred
- assertReified ∷ (HasSpec Bool, HasSpec a) ⇒ Term a → (a → Bool) → Pred
- explanation ∷ NonEmpty String → Pred → Pred
- monitor ∷ ((∀ a. Term a → a) → Property → Property) → Pred
- reifies ∷ (HasSpec a, HasSpec b) ⇒ Term b → Term a → (a → b) → Pred
- dependsOn ∷ (HasSpec a, HasSpec b) ⇒ Term a → Term b → Pred
- lit ∷ HasSpec a ⇒ a → Term a
- genHint ∷ ∀ t. HasGenHint t ⇒ Hint t → Term t → Pred
- giveHint ∷ HasGenHint a ⇒ Hint a → Specification a
- (<.) ∷ ∀ a. OrdLike a ⇒ Term a → Term a → Term Bool
- (<=.) ∷ ∀ a. OrdLike a ⇒ Term a → Term a → Term Bool
- (>=.) ∷ ∀ a. OrdLike a ⇒ Term a → Term a → Term Bool
- (>.) ∷ ∀ a. OrdLike a ⇒ Term a → Term a → Term Bool
- (==.) ∷ HasSpec a ⇒ Term a → Term a → Term Bool
- (/=.) ∷ HasSpec a ⇒ Term a → Term a → Term Bool
- not_ ∷ Term Bool → Term Bool
- or_ ∷ Term Bool → Term Bool → Term Bool
- (||.) ∷ Term Bool → Term Bool → Term Bool
- toGeneric_ ∷ ∀ a. GenericRequires a ⇒ Term a → Term (SimpleRep a)
- fromGeneric_ ∷ ∀ a. (GenericRequires a, AppRequires BaseW '[SimpleRep a] a) ⇒ Term (SimpleRep a) → Term a
- (+.) ∷ NumLike a ⇒ Term a → Term a → Term a
- (-.) ∷ Numeric n ⇒ Term n → Term n → Term n
- negate_ ∷ NumLike a ⇒ Term a → Term a
- addFn ∷ ∀ a. NumLike a ⇒ Term a → Term a → Term a
- negateFn ∷ ∀ a. NumLike a ⇒ Term a → Term a
- type Numeric a = (HasSpec a, Ord a, Num a, TypeSpec a ~ NumSpec a, MaybeBounded a)
- pair_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term a → Term b → Term (a, b)
- fst_ ∷ (HasSpec x, HasSpec y) ⇒ Term (x, y) → Term x
- snd_ ∷ (HasSpec x, HasSpec y) ⇒ Term (x, y) → Term y
- prodSnd_ ∷ (HasSpec a, HasSpec b) ⇒ Term (Prod a b) → Term b
- prodFst_ ∷ (HasSpec a, HasSpec b) ⇒ Term (Prod a b) → Term a
- prod_ ∷ (HasSpec a, HasSpec b) ⇒ Term a → Term b → Term (Prod a b)
- type IsNormalType a = (AssertComputes (Cases a) (Text "Failed to compute Cases in a use of IsNormalType for " :$$: (ShowType a :<>: Text ", are you missing an IsNormalType constraint?")), Cases a ~ '[a], AssertComputes (Args a) ((Text "Failed to compute Args in a use of IsNormalType for " :<>: ShowType a) :<>: Text ", are you missing an IsNormalType constraint?"), Args a ~ '[a], IsProd a, CountCases a ~ 1)
- injLeft_ ∷ (HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ Term a → Term (Sum a b)
- injRight_ ∷ (HasSpec a, HasSpec b, KnownNat (CountCases b)) ⇒ Term b → Term (Sum a b)
- left_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term a → Term (Either a b)
- right_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term b → Term (Either a b)
- cJust_ ∷ (HasSpec a, IsNormalType a) ⇒ Term a → Term (Maybe a)
- cNothing_ ∷ (HasSpec a, IsNormalType a) ⇒ Term (Maybe a)
- caseOn ∷ ∀ a. (GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) ⇒ Term a → FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
- branch ∷ ∀ p a. (HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) ⇒ FunTy (MapList Term (Args a)) p → Weighted Binder a
- branchW ∷ ∀ p a. (HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) ⇒ Int → FunTy (MapList Term (Args a)) p → Weighted Binder a
- forAll' ∷ ∀ t a p. (Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t, HasSpec (SimpleRep a), HasSimpleRep a, All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a), IsProductType a, HasSpec a, GenericRequires a, ProdAsListComputes a) ⇒ Term t → FunTy (MapList Term (ProductAsList a)) p → Pred
- constrained' ∷ ∀ a p. (Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a), HasSimpleRep a, All HasSpec (Args (SimpleRep a)), IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p, GenericRequires a, ProdAsListComputes a) ⇒ FunTy (MapList Term (ProductAsList a)) p → Specification a
- reify' ∷ ∀ a b p. (Cases (SimpleRep b) ~ '[SimpleRep b], TypeSpec b ~ TypeSpec (SimpleRep b), HasSpec (SimpleRep b), HasSimpleRep b, All HasSpec (Args (SimpleRep b)), IsProd (SimpleRep b), HasSpec a, HasSpec b, IsProductType b, IsProd a, IsPred p, GenericRequires b, ProdAsListComputes b) ⇒ Term a → (a → b) → FunTy (MapList Term (ProductAsList b)) p → Pred
- con ∷ ∀ c a r. (SimpleRep a ~ SOP (TheSop a), TypeSpec a ~ TypeSpec (SOP (TheSop a)), TypeList (ConstrOf c (TheSop a)), r ~ FunTy (MapList Term (ConstrOf c (TheSop a))) (Term a), ResultType r ~ Term a, SOPTerm c (TheSop a), ConstrTerm (ConstrOf c (TheSop a)), GenericRequires a) ⇒ r
- onCon ∷ ∀ c a p. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), GenericRequires a, SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All HasSpec (Cases (SOP (TheSop a))), HasSpec (ProdOver (ConstrOf c (TheSop a))), IsPred p, Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a), All HasSpec (ConstrOf c (TheSop a)), IsProd (ProdOver (ConstrOf c (TheSop a)))) ⇒ Term a → FunTy (MapList Term (ConstrOf c (TheSop a))) p → Pred
- isCon ∷ ∀ c a. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All HasSpec (Cases (SOP (TheSop a))), HasSpec (ProdOver (ConstrOf c (TheSop a))), GenericRequires a) ⇒ Term a → Pred
- sel ∷ ∀ n a c as. (SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as], TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a, HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) ⇒ Term a → Term (At n as)
- match ∷ ∀ p a. (IsProductType a, IsPred p, GenericRequires a, ProdAsListComputes a) ⇒ Term a → FunTy (MapList Term (ProductAsList a)) p → Pred
- onJust ∷ ∀ a p. (HasSpec a, IsNormalType a, IsPred p) ⇒ Term (Maybe a) → (Term a → p) → Pred
- isJust ∷ ∀ a. (HasSpec a, IsNormalType a) ⇒ Term (Maybe a) → Pred
- chooseSpec ∷ HasSpec a ⇒ (Int, Specification a) → (Int, Specification a) → Specification a
- equalSpec ∷ a → Specification a
- notEqualSpec ∷ ∀ a. HasSpec a ⇒ a → Specification a
- notMemberSpec ∷ ∀ a f. (HasSpec a, Foldable f) ⇒ f a → Specification a
- id_ ∷ ∀ a. HasSpec a ⇒ Term a → Term a
- flip_ ∷ ∀ (t ∷ [Type] → Type → Type) a b r. (HasSpec b, HasSpec a, AppRequires t '[a, b] r) ⇒ t '[a, b] r → Term b → Term a → Term r
- compose_ ∷ ∀ b t1 t2 a r. (AppRequires t1 '[b] r, AppRequires t2 '[a] b) ⇒ t1 '[b] r → t2 '[a] b → Term a → Term r
- foldMap_ ∷ ∀ a b. (Foldy b, HasSpec a) ⇒ (Term a → Term b) → Term [a] → Term b
- sum_ ∷ Foldy a ⇒ Term [a] → Term a
- elem_ ∷ (Sized [a], HasSpec a) ⇒ Term a → Term [a] → Term Bool
- singletonList_ ∷ (Sized [a], HasSpec a) ⇒ Term a → Term [a]
- append_ ∷ (Sized [a], HasSpec a) ⇒ Term [a] → Term [a] → Term [a]
- (++.) ∷ HasSpec a ⇒ Term [a] → Term [a] → Term [a]
- sizeOf ∷ Sized t ⇒ t → Integer
- sizeOf_ ∷ (HasSpec a, Sized a) ⇒ Term a → Term Integer
- null_ ∷ (HasSpec a, Sized a) ⇒ Term a → Term Bool
- hasSize ∷ (HasSpec t, Sized t) ⇒ SizeSpec → Specification t
- rangeSize ∷ Integer → Integer → SizeSpec
- length_ ∷ HasSpec a ⇒ Term [a] → Term Integer
- genFromSizeSpec ∷ MonadGenError m ⇒ Specification Integer → GenT m Integer
- between ∷ (HasSpec a, TypeSpec a ~ NumSpec a) ⇒ a → a → Specification a
- maxSpec ∷ Specification Integer → Specification Integer
- data SetW (d ∷ [Type]) (r ∷ Type) where
- SingletonW ∷ (HasSpec a, Ord a) ⇒ SetW '[a] (Set a)
- UnionW ∷ (HasSpec a, Ord a) ⇒ SetW '[Set a, Set a] (Set a)
- SubsetW ∷ (HasSpec a, Ord a, HasSpec a) ⇒ SetW '[Set a, Set a] Bool
- MemberW ∷ (HasSpec a, Ord a) ⇒ SetW '[a, Set a] Bool
- DisjointW ∷ (HasSpec a, Ord a) ⇒ SetW '[Set a, Set a] Bool
- FromListW ∷ (HasSpec a, Ord a) ⇒ SetW '[[a]] (Set a)
- data SetSpec a = SetSpec (Set a) (Specification a) (Specification Integer)
- singleton_ ∷ (Ord a, HasSpec a) ⇒ Term a → Term (Set a)
- member_ ∷ (Ord a, HasSpec a) ⇒ Term a → Term (Set a) → Term Bool
- union_ ∷ (Ord a, HasSpec a) ⇒ Term (Set a) → Term (Set a) → Term (Set a)
- subset_ ∷ (Ord a, HasSpec a) ⇒ Term (Set a) → Term (Set a) → Term Bool
- disjoint_ ∷ (Ord a, HasSpec a) ⇒ Term (Set a) → Term (Set a) → Term Bool
- fromList_ ∷ ∀ a. (Ord a, HasSpec a) ⇒ Term [a] → Term (Set a)
- pattern Elem ∷ ∀ b. () ⇒ ∀ a. (b ~ Bool, Eq a, HasSpec a) ⇒ Term a → Term [a] → Term b
- pattern ToGeneric ∷ ∀ rng. () ⇒ ∀ a. (rng ~ SimpleRep a, GenericRequires a, HasSpec a, AppRequires BaseW '[a] rng) ⇒ Term a → Term rng
- pattern FromGeneric ∷ ∀ rng. () ⇒ ∀ a. (rng ~ a, GenericRequires a, HasSpec a, AppRequires BaseW '[SimpleRep a] rng) ⇒ Term (SimpleRep a) → Term rng
- pattern Unary ∷ HOLE a' a → ListCtx f '[a] (HOLE a')
- pattern (:<:) ∷ (Typeable b, Show b) ⇒ HOLE c a → b → ListCtx Value '[a, b] (HOLE c)
- pattern (:>:) ∷ (Typeable a, Show a) ⇒ a → HOLE c b → ListCtx Value '[a, b] (HOLE c)
- printPlan ∷ HasSpec a ⇒ Specification a → IO ()
- class (Num a, HasSpec a) ⇒ NumLike a
- data PairSpec a b = Cartesian (Specification a) (Specification b)
- data MapSpec k v = MapSpec {
- mapSpecHint ∷ Maybe Integer
- mapSpecMustKeys ∷ Set k
- mapSpecMustValues ∷ [v]
- mapSpecSize ∷ Specification Integer
- mapSpecElem ∷ Specification (k, v)
- mapSpecFold ∷ FoldSpec v
- dom_ ∷ (HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k, IsNormalType v) ⇒ Term (Map k v) → Term (Set k)
- rng_ ∷ (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) ⇒ Term (Map k v) → Term [v]
- lookup_ ∷ (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) ⇒ Term k → Term (Map k v) → Term (Maybe v)
- fstSpec ∷ ∀ k v. (HasSpec k, HasSpec v) ⇒ Specification (k, v) → Specification k
- sndSpec ∷ ∀ k v. (HasSpec k, HasSpec v) ⇒ Specification (k, v) → Specification v
- var ∷ QuasiQuoter
- data Prod a b = Prod {}
Documentation
data PredD deps where Source #
Constructors
| ElemPred ∷ (HasSpecD deps a, Show a) ⇒ Bool → TermD deps a → NonEmpty a → PredD deps | |
| Monitor ∷ ((∀ a. TermD deps a → a) → Property → Property) → PredD deps | |
| And ∷ [PredD deps] → PredD deps | |
| Exists | |
| Subst ∷ (HasSpecD deps a, Show a) ⇒ Var a → TermD deps a → PredD deps → PredD deps | |
| Let ∷ TermD deps a → BinderD deps a → PredD deps | |
| Assert ∷ TermD deps Bool → PredD deps | |
| Reifies | |
| DependsOn ∷ (HasSpecD deps a, HasSpecD deps b, Show a, Show b) ⇒ TermD deps a → TermD deps b → PredD deps | |
| ForAll ∷ (ForallableD deps t e, HasSpecD deps t, HasSpecD deps e, Show t, Show e) ⇒ TermD deps t → BinderD deps e → PredD deps | |
| Case | |
| When ∷ TermD deps Bool → PredD deps → PredD deps | |
| GenHint ∷ (HasGenHintD deps a, Show a, Show (HintD deps a)) ⇒ HintD deps a → TermD deps a → PredD deps | |
| TruePred ∷ PredD deps | |
| FalsePred ∷ NonEmpty String → PredD deps | |
| Explain ∷ NonEmpty String → PredD deps → PredD deps | |
data TermD deps a where Source #
Constructors
| App ∷ AppRequiresD deps t dom rng ⇒ t dom rng → List (TermD deps) dom → TermD deps rng | |
| Lit ∷ (Typeable a, Eq a, Show a) ⇒ a → TermD deps a | |
| V ∷ (HasSpecD deps a, Typeable a) ⇒ Var a → TermD deps a |
Instances
| (Ord a, HasSpec a, HasSpec (Set a)) ⇒ Monoid (Term (Set a)) Source # | |
| (Ord a, HasSpec a, HasSpec (Set a)) ⇒ Semigroup (Term (Set a)) Source # | |
| NumLike a ⇒ Num (Term a) Source # | |
| IsPred (Term Bool) Source # | |
| Rename (Term a) Source # | |
| HasVariables (Term a) Source # | |
| Show a ⇒ Pretty (WithPrec (TermD deps a)) Source # | |
| Show a ⇒ Show (TermD deps a) Source # | |
| Eq (TermD deps a) Source # | |
| Show a ⇒ Pretty (TermD deps a) Source # | |
| HasVariables (List Term as) Source # | |
data SpecificationD deps a where Source #
A `Specification a` denotes a set of as
Constructors
| ExplainSpec ∷ [String] → SpecificationD deps a → SpecificationD deps a | Explain a Specification |
| MemberSpec | Elements of a known set |
Fields
| |
| ErrorSpec ∷ NonEmpty String → SpecificationD deps a | The empty set |
| SuspendedSpec | The set described by some predicates over the bound variable. |
Fields
| |
| TypeSpecD | A type-specific spec |
Fields
| |
| TrueSpec ∷ SpecificationD deps a | Anything |
Instances
type GenericallyInstantiated a = (AssertComputes (SimpleRep a) (((Text "Trying to use a generic instantiation of " :<>: ShowType a) :<>: Text ", likely in a HasSpec instance.") :$$: Text "However, the type has no definition of SimpleRep, likely because of a missing instance of HasSimpleRep."), HasSimpleRep a, HasSpec (SimpleRep a), TypeSpec a ~ TypeSpec (SimpleRep a)) Source #
class (Typeable t, Semantics t, Syntax t) ⇒ Logic t where Source #
A First-order typed logic has 4 components 1. Terms (Variables (x), Constants (5), and Applications (F x 5) Applications, apply a function symbol to a list of arguments: (FunctionSymbol term1 .. termN) 2. Predicates (Ordered, Odd, ...) 3. Connectives (And, Or, Not, =>, ...) 4. Quantifiers (Forall, Exists)
The Syntax, Semantics, and Logic classes implement new function symbols in the first order logic. Note that a function symbol is first order data, that uniquely identifies a higher order function. The three classes supply varying levels of functionality, relating to the Syntax, Semantics, and Logical operations of the function symbol.
Logical operations are one that support reasoning about how a function symbol relates to logical properties, that we call Specification's
Minimal complete definition
Methods
propagateTypeSpec ∷ (AppRequires t as b, HasSpec a) ⇒ t as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source #
propagateMemberSpec ∷ (AppRequires t as b, HasSpec a) ⇒ t as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source #
propagate ∷ (AppRequires t as b, HasSpec a) ⇒ t as b → ListCtx Value as (HOLE a) → Specification b → Specification a Source #
rewriteRules ∷ (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ t dom rng → List Term dom → Evidence (AppRequires t dom rng) → Maybe (Term rng) Source #
mapTypeSpec ∷ ∀ a b. (HasSpec a, HasSpec b) ⇒ t '[a] b → TypeSpec a → Specification b Source #
Instances
class Semantics (t ∷ [Type] → Type → Type) where Source #
Semantic operations are ones that give the function symbol, meaning as a function. I.e. how to apply the function to a list of arguments and return a value.
Instances
class Syntax (t ∷ [Type] → Type → Type) where Source #
Syntactic operations are ones that have to do with the structure and appearence of the type.
See DependencyInjection to better understand deps - it's a
pointer to postpone having to define HasSpec and friends here.
Minimal complete definition
Nothing
Methods
isInfix ∷ t dom rng → Bool Source #
prettySymbol ∷ ∀ deps dom rng ann. t dom rng → List (TermD deps) dom → Int → Maybe (Doc ann) Source #
Instances
class (HasSpec a, NumLike a, Logic IntW) ⇒ Foldy a where Source #
Minimal complete definition
Methods
genList ∷ MonadGenError m ⇒ Specification a → Specification a → GenT m [a] Source #
theAddFn ∷ IntW '[a, a] a Source #
genSizedList ∷ MonadGenError m ⇒ Specification Integer → Specification a → Specification a → GenT m [a] Source #
Instances
Constructors
| NumSpecInterval (Maybe n) (Maybe n) |
Instances
| (Arbitrary a, Ord a) ⇒ Arbitrary (NumSpec a) Source # | |
| Ord n ⇒ Monoid (NumSpec n) Source # | |
| Ord n ⇒ Semigroup (NumSpec n) Source # | |
| Num (NumSpec Integer) Source # | |
Defined in Constrained.NumSpec Methods (+) ∷ NumSpec Integer → NumSpec Integer → NumSpec Integer # (-) ∷ NumSpec Integer → NumSpec Integer → NumSpec Integer # (*) ∷ NumSpec Integer → NumSpec Integer → NumSpec Integer # negate ∷ NumSpec Integer → NumSpec Integer # abs ∷ NumSpec Integer → NumSpec Integer # | |
| Show n ⇒ Show (NumSpec n) Source # | |
| Ord n ⇒ Eq (NumSpec n) Source # | |
class MaybeBounded a where Source #
Minimal complete definition
Nothing
Methods
lowerBound ∷ Maybe a Source #
default lowerBound ∷ Bounded a ⇒ Maybe a Source #
upperBound ∷ Maybe a Source #
default upperBound ∷ Bounded a ⇒ Maybe a Source #
Instances
| MaybeBounded Int16 Source # | |
Defined in Constrained.NumSpec | |
| MaybeBounded Int32 Source # | |
Defined in Constrained.NumSpec | |
| MaybeBounded Int64 Source # | |
Defined in Constrained.NumSpec | |
| MaybeBounded Int8 Source # | |
Defined in Constrained.NumSpec | |
| MaybeBounded Word16 Source # | |
Defined in Constrained.NumSpec | |
| MaybeBounded Word32 Source # | |
Defined in Constrained.NumSpec | |
| MaybeBounded Word64 Source # | |
Defined in Constrained.NumSpec | |
| MaybeBounded Word8 Source # | |
Defined in Constrained.NumSpec | |
| MaybeBounded Integer Source # | |
Defined in Constrained.NumSpec | |
| MaybeBounded Natural Source # | |
Defined in Constrained.NumSpec | |
| MaybeBounded Float Source # | |
Defined in Constrained.NumSpec | |
| MaybeBounded Int Source # | |
Defined in Constrained.NumSpec | |
| MaybeBounded (Ratio Integer) Source # | |
Defined in Constrained.NumSpec | |
| MaybeBounded (Unbounded a) Source # | |
Defined in Constrained.NumSpec | |
Non-empty (and non-strict) list type.
Since: base-4.9.0.0
Constructors
| a :| [a] infixr 5 |
Instances
type Specification = SpecificationD Deps Source #
data Fun dom rng where Source #
Constructors
| Fun ∷ ∀ t dom rng. AppRequires t dom rng ⇒ t dom rng → Fun dom rng |
named ∷ String → Term a → Term a Source #
Give a Term a nameHint, if its a Var, and doesn't already have one, otherwise return the Term unchanged.
class (Typeable a, Eq a, Show a, TypeSpecEqShow a) ⇒ HasSpec a where Source #
Minimal complete definition
Nothing
Associated Types
The `TypeSpec a` is the type-specific `Specification a`.
type Prerequisites a ∷ Constraint Source #
Prerequisites for the instance that are sometimes necessary
when working with e.g. Specifications or functions in the universe.
type Prerequisites a = ()
Methods
emptySpec ∷ TypeSpec a Source #
default emptySpec ∷ GenericallyInstantiated a ⇒ TypeSpec a Source #
combineSpec ∷ TypeSpec a → TypeSpec a → Specification a Source #
default combineSpec ∷ GenericallyInstantiated a ⇒ TypeSpec a → TypeSpec a → Specification a Source #
genFromTypeSpec ∷ (HasCallStack, MonadGenError m) ⇒ TypeSpec a → GenT m a Source #
Generate a value that satisfies the HasSpec.
The key property for this generator is soundness:
∀ a ∈ genFromTypeSpec spec. a conformsTo spec
default genFromTypeSpec ∷ (GenericallyInstantiated a, HasCallStack, MonadGenError m) ⇒ TypeSpec a → GenT m a Source #
conformsTo ∷ HasCallStack ⇒ a → TypeSpec a → Bool Source #
Check conformance to the spec.
default conformsTo ∷ (GenericallyInstantiated a, HasCallStack) ⇒ a → TypeSpec a → Bool Source #
shrinkWithTypeSpec ∷ TypeSpec a → a → [a] Source #
Shrink an a with the aide of a HasSpec
default shrinkWithTypeSpec ∷ GenericallyInstantiated a ⇒ TypeSpec a → a → [a] Source #
toPreds ∷ Term a → TypeSpec a → Pred Source #
Convert a spec to predicates:
The key property here is:
∀ a. a conformsTo spec == a conformsTo constrained (t -> toPreds t spec)
cardinalTypeSpec ∷ TypeSpec a → Specification Integer Source #
Compute an upper and lower bound on the number of solutions genFromTypeSpec might return
default cardinalTypeSpec ∷ GenericallyInstantiated a ⇒ TypeSpec a → Specification Integer Source #
cardinalTrueSpec ∷ Specification Integer Source #
A bound on the number of solutions `genFromTypeSpec TrueSpec` can produce. For a type with finite elements, we can get a much more accurate answer than TrueSpec
typeSpecHasError ∷ TypeSpec a → Maybe (NonEmpty String) Source #
alternateShow ∷ TypeSpec a → BinaryShow Source #
monadConformsTo ∷ a → TypeSpec a → Writer [String] Bool Source #
typeSpecOpt ∷ TypeSpec a → [a] → Specification a Source #
For some types (especially finite ones) there may be much better ways to construct
a Specification than the default method of just adding a large bad list to TypSpec. This
function allows each HasSpec instance to decide.
guardTypeSpec ∷ [String] → TypeSpec a → Specification a Source #
This can be used to detect self inconsistencies in a (TypeSpec t)
Note this is similar to typeSpecHasError, and the default
value for typeSpecHasError is written in terms of guardTypeSpec
Both typeSpecHasError and guardTypeSpec can be set individually.
prerequisites ∷ Evidence (Prerequisites a) Source #
Materialize the Prerequisites dictionary. It should not be necessary to
implement this function manually.
default prerequisites ∷ Prerequisites a ⇒ Evidence (Prerequisites a) Source #
Instances
class Typeable (SimpleRep a) ⇒ HasSimpleRep a where Source #
Minimal complete definition
Nothing
Associated Types
Methods
toSimpleRep ∷ a → SimpleRep a Source #
default toSimpleRep ∷ (Generic a, SimpleGeneric (Rep a), SimpleRep a ~ SimplifyRep (Rep a)) ⇒ a → SimpleRep a Source #
fromSimpleRep ∷ SimpleRep a → a Source #
default fromSimpleRep ∷ (Generic a, SimpleGeneric (Rep a), SimpleRep a ~ SimplifyRep (Rep a)) ⇒ SimpleRep a → a Source #
Instances
class (Ord a, HasSpec a) ⇒ OrdLike a where Source #
Minimal complete definition
Nothing
Methods
leqSpec ∷ a → Specification a Source #
default leqSpec ∷ (GenericRequires a, OrdLike (SimpleRep a)) ⇒ a → Specification a Source #
ltSpec ∷ a → Specification a Source #
default ltSpec ∷ (OrdLike (SimpleRep a), GenericRequires a) ⇒ a → Specification a Source #
geqSpec ∷ a → Specification a Source #
default geqSpec ∷ (OrdLike (SimpleRep a), GenericRequires a) ⇒ a → Specification a Source #
gtSpec ∷ a → Specification a Source #
default gtSpec ∷ (OrdLike (SimpleRep a), GenericRequires a) ⇒ a → Specification a Source #
Instances
| (Ord a, HasSpec a, MaybeBounded a, Num a, TypeSpec a ~ NumSpec a) ⇒ OrdLike a Source # | This instance should be general enough for every type of Number that has a NumSpec as its TypeSpec |
Defined in Constrained.NumSpec Methods leqSpec ∷ a → Specification a Source # ltSpec ∷ a → Specification a Source # geqSpec ∷ a → Specification a Source # gtSpec ∷ a → Specification a Source # | |
conformsToSpecE ∷ ∀ a. HasSpec a ⇒ a → Specification a → NonEmpty String → Maybe (NonEmpty String) Source #
conformsToSpec with explanation. Nothing if (conformsToSpec a spec), but (Just explanations) if not(conformsToSpec a spec).
conformsToSpec ∷ HasSpec a ⇒ a → Specification a → Bool Source #
genFromSpecT ∷ ∀ a m. (HasCallStack, HasSpec a, MonadGenError m) ⇒ Specification a → GenT m a Source #
Generate a value that satisfies the spec. This function can fail if the spec is inconsistent, there is a dependency error, or if the underlying generators are not flexible enough.
genFromSpec ∷ ∀ a. (HasCallStack, HasSpec a) ⇒ Specification a → Gen a Source #
A version of genFromSpecT that simply errors if the generator fails
debugSpec ∷ ∀ a. HasSpec a ⇒ Specification a → IO () Source #
A version of genFromSpecT that runs in the IO monad. Good for debugging.
genFromSpecWithSeed ∷ ∀ a. (HasCallStack, HasSpec a) ⇒ Int → Int → Specification a → a Source #
A version of genFromSpecT that takes a seed and a size and gives you a result
simplifySpec ∷ HasSpec a ⇒ Specification a → Specification a Source #
cardinality ∷ ∀ a. (Number Integer, HasSpec a) ⇒ Specification a → Specification Integer Source #
Put some (admittedly loose bounds) on the number of solutions that
genFromTypeSpec might return. For lots of types, there is no way to be very accurate.
Here we lift the HasSpec methods cardinalTrueSpec and cardinalTypeSpec
from (TypeSpec Integer) to (Specification Integer)
ifElse ∷ (IsPred p, IsPred q) ⇒ Term Bool → p → q → Pred Source #
If the `Specification Bool` doesn't constrain the boolean you will get a TrueSpec out.
simplifyTerm ∷ ∀ a. Term a → Term a Source #
Simplify a Term, if the Term is an App, apply the rewrite rules
chosen by the (Logic sym t bs a) instance attached
to the function witness f
constrained ∷ ∀ a p. (IsPred p, HasSpec a) ⇒ (Term a → p) → Specification a Source #
assertReified ∷ (HasSpec Bool, HasSpec a) ⇒ Term a → (a → Bool) → Pred Source #
requires (HasSpec Bool)
explanation ∷ NonEmpty String → Pred → Pred Source #
Wrap an Explain around a Pred, unless there is a simpler form.
monitor ∷ ((∀ a. Term a → a) → Property → Property) → Pred Source #
Add QuickCheck monitoring (e.g. collect or counterexample)
to a predicate. To use the monitoring in a property call monitorSpec on the Specification
containing the monitoring and a value generated from the specification.
giveHint ∷ HasGenHint a ⇒ Hint a → Specification a Source #
toGeneric_ ∷ ∀ a. GenericRequires a ⇒ Term a → Term (SimpleRep a) Source #
fromGeneric_ ∷ ∀ a. (GenericRequires a, AppRequires BaseW '[SimpleRep a] a) ⇒ Term (SimpleRep a) → Term a Source #
pair_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term a → Term b → Term (a, b) Source #
type IsNormalType a = (AssertComputes (Cases a) (Text "Failed to compute Cases in a use of IsNormalType for " :$$: (ShowType a :<>: Text ", are you missing an IsNormalType constraint?")), Cases a ~ '[a], AssertComputes (Args a) ((Text "Failed to compute Args in a use of IsNormalType for " :<>: ShowType a) :<>: Text ", are you missing an IsNormalType constraint?"), Args a ~ '[a], IsProd a, CountCases a ~ 1) Source #
left_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term a → Term (Either a b) Source #
right_ ∷ (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) ⇒ Term b → Term (Either a b) Source #
caseOn ∷ ∀ a. (GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) ⇒ Term a → FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred Source #
branch ∷ ∀ p a. (HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) ⇒ FunTy (MapList Term (Args a)) p → Weighted Binder a Source #
branchW ∷ ∀ p a. (HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) ⇒ Int → FunTy (MapList Term (Args a)) p → Weighted Binder a Source #
forAll' ∷ ∀ t a p. (Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t, HasSpec (SimpleRep a), HasSimpleRep a, All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a), IsProductType a, HasSpec a, GenericRequires a, ProdAsListComputes a) ⇒ Term t → FunTy (MapList Term (ProductAsList a)) p → Pred Source #
Like forAll but pattern matches on the `Term a`
constrained' ∷ ∀ a p. (Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a), HasSimpleRep a, All HasSpec (Args (SimpleRep a)), IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p, GenericRequires a, ProdAsListComputes a) ⇒ FunTy (MapList Term (ProductAsList a)) p → Specification a Source #
Like constrained but pattern matches on the bound `Term a`
reify' ∷ ∀ a b p. (Cases (SimpleRep b) ~ '[SimpleRep b], TypeSpec b ~ TypeSpec (SimpleRep b), HasSpec (SimpleRep b), HasSimpleRep b, All HasSpec (Args (SimpleRep b)), IsProd (SimpleRep b), HasSpec a, HasSpec b, IsProductType b, IsProd a, IsPred p, GenericRequires b, ProdAsListComputes b) ⇒ Term a → (a → b) → FunTy (MapList Term (ProductAsList b)) p → Pred Source #
Like reify but pattern matches on the bound `Term b`
con ∷ ∀ c a r. (SimpleRep a ~ SOP (TheSop a), TypeSpec a ~ TypeSpec (SOP (TheSop a)), TypeList (ConstrOf c (TheSop a)), r ~ FunTy (MapList Term (ConstrOf c (TheSop a))) (Term a), ResultType r ~ Term a, SOPTerm c (TheSop a), ConstrTerm (ConstrOf c (TheSop a)), GenericRequires a) ⇒ r Source #
onCon ∷ ∀ c a p. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), GenericRequires a, SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All HasSpec (Cases (SOP (TheSop a))), HasSpec (ProdOver (ConstrOf c (TheSop a))), IsPred p, Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a), All HasSpec (ConstrOf c (TheSop a)), IsProd (ProdOver (ConstrOf c (TheSop a)))) ⇒ Term a → FunTy (MapList Term (ConstrOf c (TheSop a))) p → Pred Source #
isCon ∷ ∀ c a. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All HasSpec (Cases (SOP (TheSop a))), HasSpec (ProdOver (ConstrOf c (TheSop a))), GenericRequires a) ⇒ Term a → Pred Source #
sel ∷ ∀ n a c as. (SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as], TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a, HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) ⇒ Term a → Term (At n as) Source #
match ∷ ∀ p a. (IsProductType a, IsPred p, GenericRequires a, ProdAsListComputes a) ⇒ Term a → FunTy (MapList Term (ProductAsList a)) p → Pred Source #
onJust ∷ ∀ a p. (HasSpec a, IsNormalType a, IsPred p) ⇒ Term (Maybe a) → (Term a → p) → Pred Source #
chooseSpec ∷ HasSpec a ⇒ (Int, Specification a) → (Int, Specification a) → Specification a Source #
ChooseSpec is one of the ways we can Or two Specs together
This works for any kind of type that has a HasSpec instance.
If your type is a Sum type. One can use CaseOn which is much easier.
equalSpec ∷ a → Specification a Source #
notEqualSpec ∷ ∀ a. HasSpec a ⇒ a → Specification a Source #
notMemberSpec ∷ ∀ a f. (HasSpec a, Foldable f) ⇒ f a → Specification a Source #
flip_ ∷ ∀ (t ∷ [Type] → Type → Type) a b r. (HasSpec b, HasSpec a, AppRequires t '[a, b] r) ⇒ t '[a, b] r → Term b → Term a → Term r Source #
compose_ ∷ ∀ b t1 t2 a r. (AppRequires t1 '[b] r, AppRequires t2 '[a] b) ⇒ t1 '[b] r → t2 '[a] b → Term a → Term r Source #
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
maxSpec ∷ Specification Integer → Specification Integer Source #
The widest interval whose largest element is admitted by the original spec
data SetW (d ∷ [Type]) (r ∷ Type) where Source #
Constructors
| SingletonW ∷ (HasSpec a, Ord a) ⇒ SetW '[a] (Set a) | |
| UnionW ∷ (HasSpec a, Ord a) ⇒ SetW '[Set a, Set a] (Set a) | |
| SubsetW ∷ (HasSpec a, Ord a, HasSpec a) ⇒ SetW '[Set a, Set a] Bool | |
| MemberW ∷ (HasSpec a, Ord a) ⇒ SetW '[a, Set a] Bool | |
| DisjointW ∷ (HasSpec a, Ord a) ⇒ SetW '[Set a, Set a] Bool | |
| FromListW ∷ (HasSpec a, Ord a) ⇒ SetW '[[a]] (Set a) |
Instances
| Syntax SetW Source # | |
| Logic SetW Source # | |
Defined in Constrained.Spec.Set Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires SetW as b, HasSpec a) ⇒ SetW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires SetW as b, HasSpec a) ⇒ SetW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires SetW as b, HasSpec a) ⇒ SetW as b → ListCtx Value as (HOLE a) → Specification b → Specification a Source # rewriteRules ∷ ∀ (dom ∷ [Type]) rng. (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ SetW dom rng → List Term dom → Evidence (AppRequires SetW dom rng) → Maybe (Term rng) Source # mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ SetW '[a] b → TypeSpec a → Specification b Source # saturate ∷ ∀ (dom ∷ [Type]). SetW dom Bool → List Term dom → [Pred] Source # | |
| Semantics SetW Source # | |
| Show (SetW ds r) Source # | |
| Eq (SetW dom rng) Source # | |
Constructors
| SetSpec (Set a) (Specification a) (Specification Integer) |
pattern ToGeneric ∷ ∀ rng. () ⇒ ∀ a. (rng ~ SimpleRep a, GenericRequires a, HasSpec a, AppRequires BaseW '[a] rng) ⇒ Term a → Term rng Source #
pattern FromGeneric ∷ ∀ rng. () ⇒ ∀ a. (rng ~ a, GenericRequires a, HasSpec a, AppRequires BaseW '[SimpleRep a] rng) ⇒ Term (SimpleRep a) → Term rng Source #
pattern Unary ∷ HOLE a' a → ListCtx f '[a] (HOLE a') Source #
A Convenient pattern for singleton contexts
pattern (:<:) ∷ (Typeable b, Show b) ⇒ HOLE c a → b → ListCtx Value '[a, b] (HOLE c) Source #
Convenient patterns for binary contexts (the arrow :<: points towards the hole)
pattern (:>:) ∷ (Typeable a, Show a) ⇒ a → HOLE c b → ListCtx Value '[a, b] (HOLE c) Source #
Convenient patterns for binary contexts (the arrow :>: points towards the hole)
class (Num a, HasSpec a) ⇒ NumLike a Source #
Instances
| Numeric a ⇒ NumLike a Source # | |
Defined in Constrained.NumSpec Methods subtractSpec ∷ a → TypeSpec a → Specification a Source # negateSpec ∷ TypeSpec a → Specification a Source # safeSubtract ∷ a → a → Maybe a Source # | |
Constructors
| Cartesian (Specification a) (Specification b) |
Constructors
| MapSpec | |
Fields
| |
Instances
dom_ ∷ (HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k, IsNormalType v) ⇒ Term (Map k v) → Term (Set k) Source #
rng_ ∷ (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) ⇒ Term (Map k v) → Term [v] Source #
lookup_ ∷ (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) ⇒ Term k → Term (Map k v) → Term (Maybe v) Source #
fstSpec ∷ ∀ k v. (HasSpec k, HasSpec v) ⇒ Specification (k, v) → Specification k Source #
sndSpec ∷ ∀ k v. (HasSpec k, HasSpec v) ⇒ Specification (k, v) → Specification v Source #