constrained-generators-0.2.0.0: Framework for generating constrained random data using a subset of first order logic
Safe HaskellSafe-Inferred
LanguageHaskell2010

Constrained.Univ

Synopsis

Documentation

class FunctionLike fn where Source #

Methods

sem ∷ fn as b → FunTy as b Source #

The semantics of a function is given by sem

Instances

Instances details
FunctionLike fn ⇒ FunctionLike (FunFn fn) Source # 
Instance details

Defined in Constrained.Base

Methods

sem ∷ ∀ (as ∷ [Type]) b. FunFn fn as b → FunTy as b Source #

FunctionLike (GenericsFn fn) Source # 
Instance details

Defined in Constrained.Spec.Generics

Methods

sem ∷ ∀ (as ∷ [Type]) b. GenericsFn fn as b → FunTy as b Source #

FunctionLike (IntFn fn) Source # 
Instance details

Defined in Constrained.Base

Methods

sem ∷ ∀ (as ∷ [Type]) b. IntFn fn as b → FunTy as b Source #

FunctionLike fn ⇒ FunctionLike (ListFn fn) Source # 
Instance details

Defined in Constrained.Base

Methods

sem ∷ ∀ (as ∷ [Type]) b. ListFn fn as b → FunTy as b Source #

FunctionLike (OrdFn fn) Source # 
Instance details

Defined in Constrained.Base

Methods

sem ∷ ∀ (as ∷ [Type]) b. OrdFn fn as b → FunTy as b Source #

FunctionLike (SizeFn fn) Source # 
Instance details

Defined in Constrained.Base

Methods

sem ∷ ∀ (as ∷ [Type]) b. SizeFn fn as b → FunTy as b Source #

FunctionLike (TreeFn fn) Source # 
Instance details

Defined in Constrained.Spec.Tree

Methods

sem ∷ ∀ (as ∷ [Type]) b. TreeFn fn as b → FunTy as b Source #

FunctionLike (BoolFn fn) Source # 
Instance details

Defined in Constrained.Univ

Methods

sem ∷ ∀ (as ∷ [Type]) b. BoolFn fn as b → FunTy as b Source #

FunctionLike (EqFn fn) Source # 
Instance details

Defined in Constrained.Univ

Methods

sem ∷ ∀ (as ∷ [Type]) b. EqFn fn as b → FunTy as b Source #

FunctionLike (fn (Fix fn)) ⇒ FunctionLike (Fix fn) Source # 
Instance details

Defined in Constrained.Univ

Methods

sem ∷ ∀ (as ∷ [Type]) b. Fix fn as b → FunTy as b Source #

FunctionLike (MapFn fn) Source # 
Instance details

Defined in Constrained.Univ

Methods

sem ∷ ∀ (as ∷ [Type]) b. MapFn fn as b → FunTy as b Source #

FunctionLike (PairFn fn) Source # 
Instance details

Defined in Constrained.Univ

Methods

sem ∷ ∀ (as ∷ [Type]) b. PairFn fn as b → FunTy as b Source #

FunctionLike (SetFn fn) Source # 
Instance details

Defined in Constrained.Univ

Methods

sem ∷ ∀ (as ∷ [Type]) b. SetFn fn as b → FunTy as b Source #

FunctionLike (SumFn fn) Source # 
Instance details

Defined in Constrained.Univ

Methods

sem ∷ ∀ (as ∷ [Type]) b. SumFn fn as b → FunTy as b Source #

(FunctionLike (fn fnU), FunctionLike (fn' fnU)) ⇒ FunctionLike (Oneof fn fn' fnU) Source # 
Instance details

Defined in Constrained.Univ

Methods

sem ∷ ∀ (as ∷ [Type]) b. Oneof fn fn' fnU as b → FunTy as b Source #

class IsMember (fn ∷ [Type] → TypeType) fnU (path ∷ [PathElem]) where Source #

Evidence that fn exists somewhere in fnU. To make it possible for fnU to consist of a balanced tree of functions we need the path to help GHC disambiguate instances of this class during solving.

Methods

injectFn0 ∷ fn as b → fnU as b Source #

Inject a specific function symbol into a function universe.

extractFn0 ∷ fnU as b → Maybe (fn as b) Source #

Instances

Instances details
IsMember fn fn ('[] ∷ [PathElem]) Source # 
Instance details

Defined in Constrained.Univ

Methods

injectFn0 ∷ ∀ (as ∷ [Type]) b. fn as b → fn as b Source #

extractFn0 ∷ ∀ (as ∷ [Type]) b. fn as b → Maybe (fn as b) Source #

IsMember fn (fn' (Fix fn')) path ⇒ IsMember fn (Fix fn') ('PFix ': path) Source # 
Instance details

Defined in Constrained.Univ

Methods

injectFn0 ∷ ∀ (as ∷ [Type]) b. fn as b → Fix fn' as b Source #

extractFn0 ∷ ∀ (as ∷ [Type]) b. Fix fn' as b → Maybe (fn as b) Source #

IsMember fn (fn' fnU) path ⇒ IsMember fn (Oneof fn' fn'' fnU) ('PLeft ': path) Source # 
Instance details

Defined in Constrained.Univ

Methods

injectFn0 ∷ ∀ (as ∷ [Type]) b. fn as b → Oneof fn' fn'' fnU as b Source #

extractFn0 ∷ ∀ (as ∷ [Type]) b. Oneof fn' fn'' fnU as b → Maybe (fn as b) Source #

IsMember fn (fn'' fnU) path ⇒ IsMember fn (Oneof fn' fn'' fnU) ('PRight ': path) Source # 
Instance details

Defined in Constrained.Univ

Methods

injectFn0 ∷ ∀ (as ∷ [Type]) b. fn as b → Oneof fn' fn'' fnU as b Source #

extractFn0 ∷ ∀ (as ∷ [Type]) b. Oneof fn' fn'' fnU as b → Maybe (fn as b) Source #

type Member fn univ = IsMember fn univ (Path fn univ) Source #

injectFn ∷ ∀ fn fnU as b. Member fn fnU ⇒ fn as b → fnU as b Source #

extractFn ∷ ∀ fn fnU as b. Member fn fnU ⇒ fnU as b → Maybe (fn as b) Source #

data PathElem Source #

Constructors

PFix 
PLeft 
PRight 

Instances

Instances details
IsMember fn fn ('[] ∷ [PathElem]) Source # 
Instance details

Defined in Constrained.Univ

Methods

injectFn0 ∷ ∀ (as ∷ [Type]) b. fn as b → fn as b Source #

extractFn0 ∷ ∀ (as ∷ [Type]) b. fn as b → Maybe (fn as b) Source #

IsMember fn (fn' (Fix fn')) path ⇒ IsMember fn (Fix fn') ('PFix ': path) Source # 
Instance details

Defined in Constrained.Univ

Methods

injectFn0 ∷ ∀ (as ∷ [Type]) b. fn as b → Fix fn' as b Source #

extractFn0 ∷ ∀ (as ∷ [Type]) b. Fix fn' as b → Maybe (fn as b) Source #

IsMember fn (fn' fnU) path ⇒ IsMember fn (Oneof fn' fn'' fnU) ('PLeft ': path) Source # 
Instance details

Defined in Constrained.Univ

Methods

injectFn0 ∷ ∀ (as ∷ [Type]) b. fn as b → Oneof fn' fn'' fnU as b Source #

extractFn0 ∷ ∀ (as ∷ [Type]) b. Oneof fn' fn'' fnU as b → Maybe (fn as b) Source #

IsMember fn (fn'' fnU) path ⇒ IsMember fn (Oneof fn' fn'' fnU) ('PRight ': path) Source # 
Instance details

Defined in Constrained.Univ

Methods

injectFn0 ∷ ∀ (as ∷ [Type]) b. fn as b → Oneof fn' fn'' fnU as b Source #

extractFn0 ∷ ∀ (as ∷ [Type]) b. Oneof fn' fn'' fnU as b → Maybe (fn as b) Source #

newtype Fix (fn ∷ UnivUniv) (as ∷ [Type]) b Source #

Constructors

Fix (fn (Fix fn) as b) 

Instances

Instances details
IsMember fn (fn' (Fix fn')) path ⇒ IsMember fn (Fix fn') ('PFix ': path) Source # 
Instance details

Defined in Constrained.Univ

Methods

injectFn0 ∷ ∀ (as ∷ [Type]) b. fn as b → Fix fn' as b Source #

extractFn0 ∷ ∀ (as ∷ [Type]) b. Fix fn' as b → Maybe (fn as b) Source #

FunctionLike (fn (Fix fn)) ⇒ FunctionLike (Fix fn) Source # 
Instance details

Defined in Constrained.Univ

Methods

sem ∷ ∀ (as ∷ [Type]) b. Fix fn as b → FunTy as b Source #

(Typeable fn, Functions (fn (Fix fn)) (Fix fn)) ⇒ Functions (Fix fn) (Fix fn) Source # 
Instance details

Defined in Constrained.Instances

Methods

propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec (Fix fn) a, HasSpec (Fix fn) b, All (HasSpec (Fix fn)) as) ⇒ Fix fn as b → ListCtx Value as (HOLE a) → Specification (Fix fn) b → Specification (Fix fn) a Source #

rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec (Fix fn) b, All (HasSpec (Fix fn)) as) ⇒ Fix fn as b → List (Term (Fix fn)) as → Maybe (Term (Fix fn) b) Source #

mapTypeSpec ∷ (HasSpec (Fix fn) a, HasSpec (Fix fn) b) ⇒ Fix fn '[a] b → TypeSpec (Fix fn) a → Specification (Fix fn) b Source #

Show (fn (Fix fn) as b) ⇒ Show (Fix fn as b) Source # 
Instance details

Defined in Constrained.Univ

Methods

showsPrecIntFix fn as b → ShowS Source #

showFix fn as b → String Source #

showList ∷ [Fix fn as b] → ShowS Source #

Eq (fn (Fix fn) as b) ⇒ Eq (Fix fn as b) Source # 
Instance details

Defined in Constrained.Univ

Methods

(==)Fix fn as b → Fix fn as b → Bool Source #

(/=)Fix fn as b → Fix fn as b → Bool Source #

type Univ = [Type] → TypeType Source #

data Oneof fn fn' (fnU ∷ [Type] → TypeType) (as ∷ [Type]) b Source #

Constructors

OneofLeft !(fn fnU as b) 
OneofRight !(fn' fnU as b) 

Instances

Instances details
IsMember fn (fn' fnU) path ⇒ IsMember fn (Oneof fn' fn'' fnU) ('PLeft ': path) Source # 
Instance details

Defined in Constrained.Univ

Methods

injectFn0 ∷ ∀ (as ∷ [Type]) b. fn as b → Oneof fn' fn'' fnU as b Source #

extractFn0 ∷ ∀ (as ∷ [Type]) b. Oneof fn' fn'' fnU as b → Maybe (fn as b) Source #

IsMember fn (fn'' fnU) path ⇒ IsMember fn (Oneof fn' fn'' fnU) ('PRight ': path) Source # 
Instance details

Defined in Constrained.Univ

Methods

injectFn0 ∷ ∀ (as ∷ [Type]) b. fn as b → Oneof fn' fn'' fnU as b Source #

extractFn0 ∷ ∀ (as ∷ [Type]) b. Oneof fn' fn'' fnU as b → Maybe (fn as b) Source #

(FunctionLike (fn fnU), FunctionLike (fn' fnU)) ⇒ FunctionLike (Oneof fn fn' fnU) Source # 
Instance details

Defined in Constrained.Univ

Methods

sem ∷ ∀ (as ∷ [Type]) b. Oneof fn fn' fnU as b → FunTy as b Source #

(Typeable fn, Typeable fn', Typeable fnU, Functions (fn fnU) fnU, Functions (fn' fnU) fnU) ⇒ Functions (Oneof fn fn' fnU) fnU Source # 
Instance details

Defined in Constrained.Instances

Methods

propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fnU a, HasSpec fnU b, All (HasSpec fnU) as) ⇒ Oneof fn fn' fnU as b → ListCtx Value as (HOLE a) → Specification fnU b → Specification fnU a Source #

rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fnU b, All (HasSpec fnU) as) ⇒ Oneof fn fn' fnU as b → List (Term fnU) as → Maybe (Term fnU b) Source #

mapTypeSpec ∷ (HasSpec fnU a, HasSpec fnU b) ⇒ Oneof fn fn' fnU '[a] b → TypeSpec fnU a → Specification fnU b Source #

(Show (fn fnU as b), Show (fn' fnU as b)) ⇒ Show (Oneof fn fn' fnU as b) Source # 
Instance details

Defined in Constrained.Univ

Methods

showsPrecIntOneof fn fn' fnU as b → ShowS Source #

showOneof fn fn' fnU as b → String Source #

showList ∷ [Oneof fn fn' fnU as b] → ShowS Source #

(Eq (fn fnU as b), Eq (fn' fnU as b)) ⇒ Eq (Oneof fn fn' fnU as b) Source # 
Instance details

Defined in Constrained.Univ

Methods

(==)Oneof fn fn' fnU as b → Oneof fn fn' fnU as b → Bool Source #

(/=)Oneof fn fn' fnU as b → Oneof fn fn' fnU as b → Bool Source #

type family OneofL as where ... Source #

Build a balanced tree of Oneof from a list of function universes. NOTE: it is important that this is a balanced tree as that reduces the amount of overhead in injectFn and extractFn from `O(n)` to `O(log(n))`. Surprisingly, we've observed this making more than 10% difference in runtime on some generation tasks even though the list as is typically small (< 20 elements).

Equations

OneofL '[t] = t 
OneofL (t ': ts) = Insert t (OneofL ts) 

type family Insert a t where ... Source #

Equations

Insert a (Oneof fn fn') = Oneof fn' (Insert a fn) 
Insert a t = Oneof a t 

type family MPath fn fnU ∷ Maybe [PathElem] where ... Source #

Compute the path to look up fn in fnU

Equations

MPath fn fn = 'Just '[] 
MPath fn (Oneof fn' fn'' fnU) = Resolve (MPath fn (fn' fnU)) (MPath fn (fn'' fnU)) 
MPath fn (Fix fn') = AddFix (MPath fn (fn' (Fix fn'))) 
MPath _ _ = 'Nothing 

type family AddFix mpath where ... Source #

Equations

AddFix ('Just path) = 'Just ('PFix ': path) 
AddFix 'Nothing = 'Nothing 

type family Resolve a b where ... Source #

Equations

Resolve ('Just as) _ = 'Just ('PLeft ': as) 
Resolve _ ('Just bs) = 'Just ('PRight ': bs) 
Resolve _ _ = 'Nothing 

type family FromJust m where ... Source #

Equations

FromJust ('Just a) = a 

type family Path fn fn' where ... Source #

Equations

Path fn fn' = FromJust (MPath fn fn') 

equalFn ∷ ∀ fn a. (Eq a, Member (EqFn fn) fn) ⇒ fn '[a, a] Bool Source #

data EqFn (fn ∷ [Type] → TypeType) as b where Source #

Constructors

EqualEq a ⇒ EqFn fn '[a, a] Bool 

Instances

Instances details
FunctionLike (EqFn fn) Source # 
Instance details

Defined in Constrained.Univ

Methods

sem ∷ ∀ (as ∷ [Type]) b. EqFn fn as b → FunTy as b Source #

BaseUniverse fn ⇒ Functions (EqFn fn) fn Source # 
Instance details

Defined in Constrained.Instances

Methods

propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ EqFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source #

rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ EqFn fn as b → List (Term fn) as → Maybe (Term fn b) Source #

mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ EqFn fn '[a] b → TypeSpec fn a → Specification fn b Source #

Show (EqFn fn as b) Source # 
Instance details

Defined in Constrained.Univ

Methods

showsPrecIntEqFn fn as b → ShowS Source #

showEqFn fn as b → String Source #

showList ∷ [EqFn fn as b] → ShowS Source #

Eq (EqFn fn as b) Source # 
Instance details

Defined in Constrained.Univ

Methods

(==)EqFn fn as b → EqFn fn as b → Bool Source #

(/=)EqFn fn as b → EqFn fn as b → Bool Source #

notFn ∷ ∀ fn. Member (BoolFn fn) fn ⇒ fn '[Bool] Bool Source #

orFn ∷ ∀ fn. Member (BoolFn fn) fn ⇒ fn '[Bool, Bool] Bool Source #

data BoolFn (fn ∷ [Type] → TypeType) as b where Source #

Operations on Bool. One might expect And :: BoolFn fn '[Bool, Bool] Bool But this is problematic because a Term like ( p x &&. q y ) has to solve for x or y first, choose x, so once x is fixed, it might be impossible to solve for y Luckily we can get conjuction by using Preds, in fact using Preds, the x and y can even be the same variable. Or can be problematic too (by using a form of DeMorgan's laws: x && y = not(not x || not y)) but while that is possible, there are many scenarios which can only be specified using Or. If one inadvertantly uses a form of DeMorgan's laws, the worst that can happen is an ErrorSpec is returned, and the user can reformulate using Preds. So Or is incomplete, but sound, when it works.

Constructors

NotBoolFn fn '[Bool] Bool 
OrBoolFn fn '[Bool, Bool] Bool 

Instances

Instances details
FunctionLike (BoolFn fn) Source # 
Instance details

Defined in Constrained.Univ

Methods

sem ∷ ∀ (as ∷ [Type]) b. BoolFn fn as b → FunTy as b Source #

BaseUniverse fn ⇒ Functions (BoolFn fn) fn Source # 
Instance details

Defined in Constrained.Instances

Methods

propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ BoolFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source #

rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ BoolFn fn as b → List (Term fn) as → Maybe (Term fn b) Source #

mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ BoolFn fn '[a] b → TypeSpec fn a → Specification fn b Source #

Show (BoolFn fn as b) Source # 
Instance details

Defined in Constrained.Univ

Methods

showsPrecIntBoolFn fn as b → ShowS Source #

showBoolFn fn as b → String Source #

showList ∷ [BoolFn fn as b] → ShowS Source #

Eq (BoolFn fn as b) Source # 
Instance details

Defined in Constrained.Univ

Methods

(==)BoolFn fn as b → BoolFn fn as b → Bool Source #

(/=)BoolFn fn as b → BoolFn fn as b → Bool Source #

data Prod a b Source #

Constructors

Prod 

Fields

Instances

Instances details
(HasSpec fn a, HasSpec fn b) ⇒ HasSpec fn (Prod a b) Source # 
Instance details

Defined in Constrained.Spec.Pairs

Associated Types

type TypeSpec fn (Prod a b) Source #

type Prerequisites fn (Prod a b) Source #

Methods

emptySpecTypeSpec fn (Prod a b) Source #

combineSpecTypeSpec fn (Prod a b) → TypeSpec fn (Prod a b) → Specification fn (Prod a b) Source #

genFromTypeSpec ∷ ∀ (m ∷ TypeType). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (Prod a b) → GenT m (Prod a b) Source #

conformsToProd a b → TypeSpec fn (Prod a b) → Bool Source #

shrinkWithTypeSpecTypeSpec fn (Prod a b) → Prod a b → [Prod a b] Source #

toPredsTerm fn (Prod a b) → TypeSpec fn (Prod a b) → Pred fn Source #

cardinalTypeSpecTypeSpec fn (Prod a b) → Specification fn Integer Source #

cardinalTrueSpecSpecification fn Integer Source #

typeSpecOptTypeSpec fn (Prod a b) → [Prod a b] → Specification fn (Prod a b) Source #

prerequisitesEvidence (Prerequisites fn (Prod a b)) Source #

(Show a, Show b) ⇒ Show (Prod a b) Source # 
Instance details

Defined in Constrained.Univ

Methods

showsPrecIntProd a b → ShowS Source #

showProd a b → String Source #

showList ∷ [Prod a b] → ShowS Source #

(Eq a, Eq b) ⇒ Eq (Prod a b) Source # 
Instance details

Defined in Constrained.Univ

Methods

(==)Prod a b → Prod a b → Bool Source #

(/=)Prod a b → Prod a b → Bool Source #

(Ord a, Ord b) ⇒ Ord (Prod a b) Source # 
Instance details

Defined in Constrained.Univ

Methods

compareProd a b → Prod a b → Ordering Source #

(<)Prod a b → Prod a b → Bool Source #

(<=)Prod a b → Prod a b → Bool Source #

(>)Prod a b → Prod a b → Bool Source #

(>=)Prod a b → Prod a b → Bool Source #

maxProd a b → Prod a b → Prod a b Source #

minProd a b → Prod a b → Prod a b Source #

type Prerequisites fn (Prod a b) Source # 
Instance details

Defined in Constrained.Spec.Pairs

type Prerequisites fn (Prod a b) = (HasSpec fn a, HasSpec fn b)
type TypeSpec fn (Prod a b) Source # 
Instance details

Defined in Constrained.Spec.Pairs

type TypeSpec fn (Prod a b) = PairSpec fn a b

fstFn ∷ ∀ fn a b. Member (PairFn fn) fn ⇒ fn '[Prod a b] a Source #

sndFn ∷ ∀ fn a b. Member (PairFn fn) fn ⇒ fn '[Prod a b] b Source #

pairFn ∷ ∀ fn a b. Member (PairFn fn) fn ⇒ fn '[a, b] (Prod a b) Source #

data PairFn (fn ∷ [Type] → TypeType) args res where Source #

Constructors

PairPairFn fn '[a, b] (Prod a b) 
FstPairFn fn '[Prod a b] a 
SndPairFn fn '[Prod a b] b 

Instances

Instances details
FunctionLike (PairFn fn) Source # 
Instance details

Defined in Constrained.Univ

Methods

sem ∷ ∀ (as ∷ [Type]) b. PairFn fn as b → FunTy as b Source #

BaseUniverse fn ⇒ Functions (PairFn fn) fn Source # 
Instance details

Defined in Constrained.Spec.Pairs

Methods

propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ PairFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source #

rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ PairFn fn as b → List (Term fn) as → Maybe (Term fn b) Source #

mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ PairFn fn '[a] b → TypeSpec fn a → Specification fn b Source #

Show (PairFn fn args res) Source # 
Instance details

Defined in Constrained.Univ

Methods

showsPrecIntPairFn fn args res → ShowS Source #

showPairFn fn args res → String Source #

showList ∷ [PairFn fn args res] → ShowS Source #

Eq (PairFn fn args res) Source # 
Instance details

Defined in Constrained.Univ

Methods

(==)PairFn fn args res → PairFn fn args res → Bool Source #

(/=)PairFn fn args res → PairFn fn args res → Bool Source #

type family ProdOver as where ... Source #

Equations

ProdOver '[] = () 
ProdOver '[a] = a 
ProdOver (a ': as) = Prod a (ProdOver as) 

listToProd ∷ (ProdOver as → r) → List Identity as → r Source #

prodToList ∷ ∀ as. TypeList as ⇒ ProdOver as → List Identity as Source #

appendProd ∷ ∀ xs ys. (TypeList xs, TypeList ys) ⇒ ProdOver xs → ProdOver ys → ProdOver (Append xs ys) Source #

splitProd ∷ ∀ xs ys. (TypeList xs, TypeList ys) ⇒ ProdOver (Append xs ys) → Prod (ProdOver xs) (ProdOver ys) Source #

data Sum a b Source #

Constructors

SumLeft a 
SumRight b 

Instances

Instances details
(HasSpec fn a, HasSpec fn b, KnownNat (CountCases b)) ⇒ HasSpec fn (Sum a b) Source # 
Instance details

Defined in Constrained.Base

Associated Types

type TypeSpec fn (Sum a b) Source #

type Prerequisites fn (Sum a b) Source #

Methods

emptySpecTypeSpec fn (Sum a b) Source #

combineSpecTypeSpec fn (Sum a b) → TypeSpec fn (Sum a b) → Specification fn (Sum a b) Source #

genFromTypeSpec ∷ ∀ (m ∷ TypeType). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (Sum a b) → GenT m (Sum a b) Source #

conformsToSum a b → TypeSpec fn (Sum a b) → Bool Source #

shrinkWithTypeSpecTypeSpec fn (Sum a b) → Sum a b → [Sum a b] Source #

toPredsTerm fn (Sum a b) → TypeSpec fn (Sum a b) → Pred fn Source #

cardinalTypeSpecTypeSpec fn (Sum a b) → Specification fn Integer Source #

cardinalTrueSpecSpecification fn Integer Source #

typeSpecOptTypeSpec fn (Sum a b) → [Sum a b] → Specification fn (Sum a b) Source #

prerequisitesEvidence (Prerequisites fn (Sum a b)) Source #

(Show a, Show b) ⇒ Show (Sum a b) Source # 
Instance details

Defined in Constrained.Univ

Methods

showsPrecIntSum a b → ShowS Source #

showSum a b → String Source #

showList ∷ [Sum a b] → ShowS Source #

(Eq a, Eq b) ⇒ Eq (Sum a b) Source # 
Instance details

Defined in Constrained.Univ

Methods

(==)Sum a b → Sum a b → Bool Source #

(/=)Sum a b → Sum a b → Bool Source #

(Ord a, Ord b) ⇒ Ord (Sum a b) Source # 
Instance details

Defined in Constrained.Univ

Methods

compareSum a b → Sum a b → Ordering Source #

(<)Sum a b → Sum a b → Bool Source #

(<=)Sum a b → Sum a b → Bool Source #

(>)Sum a b → Sum a b → Bool Source #

(>=)Sum a b → Sum a b → Bool Source #

maxSum a b → Sum a b → Sum a b Source #

minSum a b → Sum a b → Sum a b Source #

type Prerequisites fn (Sum a b) Source # 
Instance details

Defined in Constrained.Base

type Prerequisites fn (Sum a b) = (HasSpec fn a, HasSpec fn b)
type TypeSpec fn (Sum a b) Source # 
Instance details

Defined in Constrained.Base

type TypeSpec fn (Sum a b) = SumSpec fn a b

injLeftFn ∷ ∀ fn a b. Member (SumFn fn) fn ⇒ fn '[a] (Sum a b) Source #

injRightFn ∷ ∀ fn a b. Member (SumFn fn) fn ⇒ fn '[b] (Sum a b) Source #

data SumFn (fn ∷ [Type] → TypeType) args res where Source #

Constructors

InjLeftSumFn fn '[a] (Sum a b) 
InjRightSumFn fn '[b] (Sum a b) 

Instances

Instances details
FunctionLike (SumFn fn) Source # 
Instance details

Defined in Constrained.Univ

Methods

sem ∷ ∀ (as ∷ [Type]) b. SumFn fn as b → FunTy as b Source #

BaseUniverse fn ⇒ Functions (SumFn fn) fn Source # 
Instance details

Defined in Constrained.Spec.Generics

Methods

propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ SumFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source #

rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ SumFn fn as b → List (Term fn) as → Maybe (Term fn b) Source #

mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ SumFn fn '[a] b → TypeSpec fn a → Specification fn b Source #

Show (SumFn fn args res) Source # 
Instance details

Defined in Constrained.Univ

Methods

showsPrecIntSumFn fn args res → ShowS Source #

showSumFn fn args res → String Source #

showList ∷ [SumFn fn args res] → ShowS Source #

Eq (SumFn fn args res) Source # 
Instance details

Defined in Constrained.Univ

Methods

(==)SumFn fn args res → SumFn fn args res → Bool Source #

(/=)SumFn fn args res → SumFn fn args res → Bool Source #

type family SumOver as where ... Source #

Equations

SumOver '[a] = a 
SumOver (a ': as) = Sum a (SumOver as) 

singletonFn ∷ ∀ fn a. (Member (SetFn fn) fn, Ord a) ⇒ fn '[a] (Set a) Source #

unionFn ∷ ∀ fn a. (Member (SetFn fn) fn, Ord a) ⇒ fn '[Set a, Set a] (Set a) Source #

subsetFn ∷ ∀ fn a. (Member (SetFn fn) fn, Ord a) ⇒ fn '[Set a, Set a] Bool Source #

memberFn ∷ ∀ fn a. (Member (SetFn fn) fn, Ord a) ⇒ fn '[a, Set a] Bool Source #

elemFn ∷ ∀ fn a. (Member (SetFn fn) fn, Eq a) ⇒ fn '[a, [a]] Bool Source #

disjointFn ∷ ∀ fn a. (Member (SetFn fn) fn, Ord a) ⇒ fn '[Set a, Set a] Bool Source #

fromListFn ∷ ∀ fn a. (Member (SetFn fn) fn, Ord a) ⇒ fn '[[a]] (Set a) Source #

data SetFn (fn ∷ [Type] → TypeType) args res where Source #

Constructors

SubsetOrd a ⇒ SetFn fn '[Set a, Set a] Bool 
DisjointOrd a ⇒ SetFn fn '[Set a, Set a] Bool 
MemberOrd a ⇒ SetFn fn '[a, Set a] Bool 
SingletonOrd a ⇒ SetFn fn '[a] (Set a) 
UnionOrd a ⇒ SetFn fn '[Set a, Set a] (Set a) 
ElemEq a ⇒ SetFn fn '[a, [a]] Bool 
FromListOrd a ⇒ SetFn fn '[[a]] (Set a) 

Instances

Instances details
FunctionLike (SetFn fn) Source # 
Instance details

Defined in Constrained.Univ

Methods

sem ∷ ∀ (as ∷ [Type]) b. SetFn fn as b → FunTy as b Source #

BaseUniverse fn ⇒ Functions (SetFn fn) fn Source # 
Instance details

Defined in Constrained.Base

Methods

propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ SetFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source #

rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ SetFn fn as b → List (Term fn) as → Maybe (Term fn b) Source #

mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ SetFn fn '[a] b → TypeSpec fn a → Specification fn b Source #

Show (SetFn fn args res) Source # 
Instance details

Defined in Constrained.Univ

Methods

showsPrecIntSetFn fn args res → ShowS Source #

showSetFn fn args res → String Source #

showList ∷ [SetFn fn args res] → ShowS Source #

Eq (SetFn fn args res) Source # 
Instance details

Defined in Constrained.Univ

Methods

(==)SetFn fn args res → SetFn fn args res → Bool Source #

(/=)SetFn fn args res → SetFn fn args res → Bool Source #

data MapFn (fn ∷ [Type] → TypeType) args res where Source #

Constructors

DomOrd k ⇒ MapFn fn '[Map k v] (Set k) 
RngMapFn fn '[Map k v] [v] 
LookupOrd k ⇒ MapFn fn '[k, Map k v] (Maybe v) 

Instances

Instances details
FunctionLike (MapFn fn) Source # 
Instance details

Defined in Constrained.Univ

Methods

sem ∷ ∀ (as ∷ [Type]) b. MapFn fn as b → FunTy as b Source #

BaseUniverse fn ⇒ Functions (MapFn fn) fn Source # 
Instance details

Defined in Constrained.Spec.Map

Methods

propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ MapFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source #

rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ MapFn fn as b → List (Term fn) as → Maybe (Term fn b) Source #

mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ MapFn fn '[a] b → TypeSpec fn a → Specification fn b Source #

Show (MapFn fn args res) Source # 
Instance details

Defined in Constrained.Univ

Methods

showsPrecIntMapFn fn args res → ShowS Source #

showMapFn fn args res → String Source #

showList ∷ [MapFn fn args res] → ShowS Source #

Eq (MapFn fn args res) Source # 
Instance details

Defined in Constrained.Univ

Methods

(==)MapFn fn args res → MapFn fn args res → Bool Source #

(/=)MapFn fn args res → MapFn fn args res → Bool Source #

domFn ∷ ∀ fn k v. (Member (MapFn fn) fn, Ord k) ⇒ fn '[Map k v] (Set k) Source #

rngFn ∷ ∀ fn k v. Member (MapFn fn) fn ⇒ fn '[Map k v] [v] Source #

lookupFn ∷ ∀ fn k v. (Member (MapFn fn) fn, Ord k) ⇒ fn '[k, Map k v] (Maybe v) Source #