Safe Haskell	Safe-Inferred
Language	Haskell2010

Constrained.Univ

Synopsis

class FunctionLike fn where
- sem ∷ fn as b → FunTy as b
class IsMember (fn ∷ [Type] → Type → Type) fnU (path ∷ [PathElem]) where
- injectFn0 ∷ fn as b → fnU as b
- extractFn0 ∷ fnU as b → Maybe (fn as b)
type Member fn univ = IsMember fn univ (Path fn univ)
injectFn ∷ ∀ fn fnU as b. Member fn fnU ⇒ fn as b → fnU as b
extractFn ∷ ∀ fn fnU as b. Member fn fnU ⇒ fnU as b → Maybe (fn as b)
data PathElem
- = PFix
- | PLeft
- | PRight
newtype Fix (fn ∷ Univ → Univ) (as ∷ [Type]) b = Fix (fn (Fix fn) as b)
type Univ = [Type] → Type → Type
data Oneof fn fn' (fnU ∷ [Type] → Type → Type) (as ∷ [Type]) b
- = OneofLeft !(fn fnU as b)
- | OneofRight !(fn' fnU as b)
type family OneofL as where ...
type family Insert a t where ...
type family MPath fn fnU ∷ Maybe [PathElem] where ...
type family AddFix mpath where ...
type family Resolve a b where ...
type family FromJust m where ...
type family Path fn fn' where ...
equalFn ∷ ∀ fn a. (Eq a, Member (EqFn fn) fn) ⇒ fn '[a, a] Bool
data EqFn (fn ∷ [Type] → Type → Type) as b where
- Equal ∷ Eq a ⇒ EqFn fn '[a, a] Bool
notFn ∷ ∀ fn. Member (BoolFn fn) fn ⇒ fn '[Bool] Bool
orFn ∷ ∀ fn. Member (BoolFn fn) fn ⇒ fn '[Bool, Bool] Bool
data BoolFn (fn ∷ [Type] → Type → Type) as b where
- Not ∷ BoolFn fn '[Bool] Bool
- Or ∷ BoolFn fn '[Bool, Bool] Bool
data Prod a b = Prod {
- prodFst ∷ a
- prodSnd ∷ b
}
fstFn ∷ ∀ fn a b. Member (PairFn fn) fn ⇒ fn '[Prod a b] a
sndFn ∷ ∀ fn a b. Member (PairFn fn) fn ⇒ fn '[Prod a b] b
pairFn ∷ ∀ fn a b. Member (PairFn fn) fn ⇒ fn '[a, b] (Prod a b)
data PairFn (fn ∷ [Type] → Type → Type) args res where
- Pair ∷ PairFn fn '[a, b] (Prod a b)
- Fst ∷ PairFn fn '[Prod a b] a
- Snd ∷ PairFn fn '[Prod a b] b
type family ProdOver as where ...
listToProd ∷ (ProdOver as → r) → List Identity as → r
prodToList ∷ ∀ as. TypeList as ⇒ ProdOver as → List Identity as
appendProd ∷ ∀ xs ys. (TypeList xs, TypeList ys) ⇒ ProdOver xs → ProdOver ys → ProdOver (Append xs ys)
splitProd ∷ ∀ xs ys. (TypeList xs, TypeList ys) ⇒ ProdOver (Append xs ys) → Prod (ProdOver xs) (ProdOver ys)
data Sum a b
- = SumLeft a
- | SumRight b
injLeftFn ∷ ∀ fn a b. Member (SumFn fn) fn ⇒ fn '[a] (Sum a b)
injRightFn ∷ ∀ fn a b. Member (SumFn fn) fn ⇒ fn '[b] (Sum a b)
data SumFn (fn ∷ [Type] → Type → Type) args res where
- InjLeft ∷ SumFn fn '[a] (Sum a b)
- InjRight ∷ SumFn fn '[b] (Sum a b)
type family SumOver as where ...
singletonFn ∷ ∀ fn a. (Member (SetFn fn) fn, Ord a) ⇒ fn '[a] (Set a)
unionFn ∷ ∀ fn a. (Member (SetFn fn) fn, Ord a, Show a, Typeable a) ⇒ fn '[Set a, Set a] (Set a)
subsetFn ∷ ∀ fn a. (Member (SetFn fn) fn, Ord a, Show a, Typeable a) ⇒ fn '[Set a, Set a] Bool
memberFn ∷ ∀ fn a. (Member (SetFn fn) fn, Ord a, Show a, Typeable a) ⇒ fn '[a, Set a] Bool
elemFn ∷ ∀ fn a. (Member (SetFn fn) fn, Eq a, Show a, Typeable a) ⇒ fn '[a, [a]] Bool
disjointFn ∷ ∀ fn a. (Member (SetFn fn) fn, Ord a, Show a, Typeable a) ⇒ fn '[Set a, Set a] Bool
fromListFn ∷ ∀ fn a. (Member (SetFn fn) fn, Ord a) ⇒ fn '[[a]] (Set a)
data SetFn (fn ∷ [Type] → Type → Type) args res where
- Subset ∷ (Ord a, Show a, Typeable a) ⇒ SetFn fn '[Set a, Set a] Bool
- Disjoint ∷ (Ord a, Show a, Typeable a) ⇒ SetFn fn '[Set a, Set a] Bool
- Member ∷ (Ord a, Show a, Typeable a) ⇒ SetFn fn '[a, Set a] Bool
- Singleton ∷ Ord a ⇒ SetFn fn '[a] (Set a)
- Union ∷ (Ord a, Show a, Typeable a) ⇒ SetFn fn '[Set a, Set a] (Set a)
- Elem ∷ (Eq a, Show a, Typeable a) ⇒ SetFn fn '[a, [a]] Bool
- FromList ∷ Ord a ⇒ SetFn fn '[[a]] (Set a)
data MapFn (fn ∷ [Type] → Type → Type) args res where
- Dom ∷ Ord k ⇒ MapFn fn '[Map k v] (Set k)
- Rng ∷ MapFn fn '[Map k v] [v]
- Lookup ∷ Ord k ⇒ MapFn fn '[k, Map k v] (Maybe v)
domFn ∷ ∀ fn k v. (Member (MapFn fn) fn, Ord k) ⇒ fn '[Map k v] (Set k)
rngFn ∷ ∀ fn k v. Member (MapFn fn) fn ⇒ fn '[Map k v] [v]
lookupFn ∷ ∀ fn k v. (Member (MapFn fn) fn, Ord k) ⇒ fn '[k, Map k v] (Maybe v)

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] → Type → Type) 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 ∷ Univ → Univ) (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 showsPrec ∷ Int → Fix fn as b → ShowS Source # show ∷ Fix 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] → Type → Type Source #

data Oneof fn fn' (fnU ∷ [Type] → Type → Type) (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 showsPrec ∷ Int → Oneof fn fn' fnU as b → ShowS Source # show ∷ Oneof 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] → Type → Type) as b where Source #

Constructors

Equal ∷ Eq 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 showsPrec ∷ Int → EqFn fn as b → ShowS Source # show ∷ EqFn 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] → Type → Type) 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

Not ∷ BoolFn fn '[Bool] Bool
Or ∷ BoolFn 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 showsPrec ∷ Int → BoolFn fn as b → ShowS Source # show ∷ BoolFn 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 prodFst ∷ a prodSnd ∷ b

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 emptySpec ∷ TypeSpec fn (Prod a b) Source # combineSpec ∷ TypeSpec fn (Prod a b) → TypeSpec fn (Prod a b) → Specification fn (Prod a b) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (Prod a b) → GenT m (Prod a b) Source # conformsTo ∷ Prod a b → TypeSpec fn (Prod a b) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn (Prod a b) → Prod a b → [Prod a b] Source # toPreds ∷ Term fn (Prod a b) → TypeSpec fn (Prod a b) → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn (Prod a b) → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn (Prod a b) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn (Prod a b) → BinaryShow Source # monadConformsTo ∷ Prod a b → TypeSpec fn (Prod a b) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn (Prod a b) → [Prod a b] → Specification fn (Prod a b) Source # guardTypeSpec ∷ [String] → TypeSpec fn (Prod a b) → Specification fn (Prod a b) Source # prerequisites ∷ Evidence (Prerequisites fn (Prod a b)) Source #
(Show a, Show b) ⇒ Show (Prod a b) Source #
Instance details Defined in Constrained.Univ Methods showsPrec ∷ Int → Prod a b → ShowS Source # show ∷ Prod 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 compare ∷ Prod 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 # max ∷ Prod a b → Prod a b → Prod a b Source # min ∷ Prod 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] → Type → Type) args res where Source #

Constructors

Pair ∷ PairFn fn '[a, b] (Prod a b)
Fst ∷ PairFn fn '[Prod a b] a
Snd ∷ PairFn 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 showsPrec ∷ Int → PairFn fn args res → ShowS Source # show ∷ PairFn 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 emptySpec ∷ TypeSpec fn (Sum a b) Source # combineSpec ∷ TypeSpec fn (Sum a b) → TypeSpec fn (Sum a b) → Specification fn (Sum a b) Source # genFromTypeSpec ∷ ∀ (m ∷ Type → Type). (HasCallStack, MonadGenError m) ⇒ TypeSpec fn (Sum a b) → GenT m (Sum a b) Source # conformsTo ∷ Sum a b → TypeSpec fn (Sum a b) → Bool Source # shrinkWithTypeSpec ∷ TypeSpec fn (Sum a b) → Sum a b → [Sum a b] Source # toPreds ∷ Term fn (Sum a b) → TypeSpec fn (Sum a b) → Pred fn Source # cardinalTypeSpec ∷ TypeSpec fn (Sum a b) → Specification fn Integer Source # cardinalTrueSpec ∷ Specification fn Integer Source # typeSpecHasError ∷ TypeSpec fn (Sum a b) → Maybe (NonEmpty String) Source # alternateShow ∷ TypeSpec fn (Sum a b) → BinaryShow Source # monadConformsTo ∷ Sum a b → TypeSpec fn (Sum a b) → Writer [String] Bool Source # typeSpecOpt ∷ TypeSpec fn (Sum a b) → [Sum a b] → Specification fn (Sum a b) Source # guardTypeSpec ∷ [String] → TypeSpec fn (Sum a b) → Specification fn (Sum a b) Source # prerequisites ∷ Evidence (Prerequisites fn (Sum a b)) Source #
(Show a, Show b) ⇒ Show (Sum a b) Source #
Instance details Defined in Constrained.Univ Methods showsPrec ∷ Int → Sum a b → ShowS Source # show ∷ Sum 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 compare ∷ Sum 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 # max ∷ Sum a b → Sum a b → Sum a b Source # min ∷ Sum 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] → Type → Type) args res where Source #

Constructors

InjLeft ∷ SumFn fn '[a] (Sum a b)
InjRight ∷ SumFn 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 showsPrec ∷ Int → SumFn fn args res → ShowS Source # show ∷ SumFn 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, Show a, Typeable a) ⇒ fn '[Set a, Set a] (Set a) Source #

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

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

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

disjointFn ∷ ∀ fn a. (Member (SetFn fn) fn, Ord a, Show a, Typeable 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] → Type → Type) args res where Source #

Constructors

Subset ∷ (Ord a, Show a, Typeable a) ⇒ SetFn fn '[Set a, Set a] Bool
Disjoint ∷ (Ord a, Show a, Typeable a) ⇒ SetFn fn '[Set a, Set a] Bool
Member ∷ (Ord a, Show a, Typeable a) ⇒ SetFn fn '[a, Set a] Bool
Singleton ∷ Ord a ⇒ SetFn fn '[a] (Set a)
Union ∷ (Ord a, Show a, Typeable a) ⇒ SetFn fn '[Set a, Set a] (Set a)
Elem ∷ (Eq a, Show a, Typeable a) ⇒ SetFn fn '[a, [a]] Bool
FromList ∷ Ord 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 showsPrec ∷ Int → SetFn fn args res → ShowS Source # show ∷ SetFn 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] → Type → Type) args res where Source #

Constructors

Dom ∷ Ord k ⇒ MapFn fn '[Map k v] (Set k)
Rng ∷ MapFn fn '[Map k v] [v]
Lookup ∷ Ord 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 showsPrec ∷ Int → MapFn fn args res → ShowS Source # show ∷ MapFn 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 #