Safe Haskell | Safe-Inferred |
---|---|

Language | Haskell2010 |

## Synopsis

- class FunctionLike fn where
- 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
- 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
- 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
- data Prod a b = Prod {}
- 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
- 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
- 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
- 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) ⇒ fn '[Set a, Set a] (Set a)
- subsetFn ∷ ∀ fn a. (Member (SetFn fn) fn, Ord a) ⇒ fn '[Set a, Set a] Bool
- memberFn ∷ ∀ fn a. (Member (SetFn fn) fn, Ord a) ⇒ fn '[a, Set a] Bool
- elemFn ∷ ∀ fn a. (Member (SetFn fn) fn, Eq a) ⇒ fn '[a, [a]] Bool
- disjointFn ∷ ∀ fn a. (Member (SetFn fn) fn, Ord 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 ⇒ SetFn fn '[Set a, Set a] Bool
- Disjoint ∷ Ord a ⇒ SetFn fn '[Set a, Set a] Bool
- Member ∷ Ord a ⇒ SetFn fn '[a, Set a] Bool
- Singleton ∷ Ord a ⇒ SetFn fn '[a] (Set a)
- Union ∷ Ord a ⇒ SetFn fn '[Set a, Set a] (Set a)
- Elem ∷ Eq a ⇒ SetFn fn '[a, [a]] Bool
- FromList ∷ Ord a ⇒ SetFn fn '[[a]] (Set a)

- data MapFn (fn ∷ [Type] → Type → Type) args res where
- 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 #

#### Instances

FunctionLike fn ⇒ FunctionLike (FunFn fn) Source # | |

FunctionLike (GenericsFn fn) Source # | |

Defined in Constrained.Spec.Generics | |

FunctionLike (IntFn fn) Source # | |

FunctionLike fn ⇒ FunctionLike (ListFn fn) Source # | |

FunctionLike (OrdFn fn) Source # | |

FunctionLike (SizeFn fn) Source # | |

FunctionLike (TreeFn fn) Source # | |

FunctionLike (BoolFn fn) Source # | |

FunctionLike (EqFn fn) Source # | |

FunctionLike (fn (Fix fn)) ⇒ FunctionLike (Fix fn) Source # | |

FunctionLike (MapFn fn) Source # | |

FunctionLike (PairFn fn) Source # | |

FunctionLike (SetFn fn) Source # | |

FunctionLike (SumFn fn) Source # | |

(FunctionLike (fn fnU), FunctionLike (fn' fnU)) ⇒ FunctionLike (Oneof fn fn' fnU) 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.

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

IsMember fn fn ('[] ∷ [PathElem]) Source # | |

Defined in Constrained.Univ | |

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

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

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

#### Instances

IsMember fn fn ('[] ∷ [PathElem]) Source # | |

Defined in Constrained.Univ | |

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

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

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

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

#### Instances

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

FunctionLike (fn (Fix fn)) ⇒ FunctionLike (Fix fn) Source # | |

(Typeable fn, Functions (fn (Fix fn)) (Fix fn)) ⇒ Functions (Fix fn) (Fix fn) Source # | |

Defined in Constrained.Instances 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 # | |

Eq (fn (Fix fn) as b) ⇒ Eq (Fix fn as b) Source # | |

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

OneofLeft !(fn fnU as b) | |

OneofRight !(fn' fnU as b) |

#### Instances

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

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

(FunctionLike (fn fnU), FunctionLike (fn' fnU)) ⇒ FunctionLike (Oneof fn fn' fnU) Source # | |

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

Defined in Constrained.Instances 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 # | |

(Eq (fn fnU as b), Eq (fn' fnU as b)) ⇒ Eq (Oneof fn fn' fnU as b) 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).

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

#### Instances

FunctionLike (EqFn fn) Source # | |

BaseUniverse fn ⇒ Functions (EqFn fn) fn Source # | |

Defined in Constrained.Instances 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 # | |

Eq (EqFn fn as b) 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.

#### Instances

FunctionLike (BoolFn fn) Source # | |

BaseUniverse fn ⇒ Functions (BoolFn fn) fn Source # | |

Defined in Constrained.Instances 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 # | |

Eq (BoolFn fn as b) Source # | |

#### Instances

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

#### Instances

FunctionLike (PairFn fn) Source # | |

BaseUniverse fn ⇒ Functions (PairFn fn) fn Source # | |

Defined in Constrained.Spec.Pairs 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 # | |

Eq (PairFn fn args res) 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 #

#### Instances

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

#### Instances

FunctionLike (SumFn fn) Source # | |

BaseUniverse fn ⇒ Functions (SumFn fn) fn Source # | |

Defined in Constrained.Spec.Generics 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 # | |

Eq (SumFn fn args res) Source # | |

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

Subset ∷ Ord a ⇒ SetFn fn '[Set a, Set a] Bool | |

Disjoint ∷ Ord a ⇒ SetFn fn '[Set a, Set a] Bool | |

Member ∷ Ord a ⇒ SetFn fn '[a, Set a] Bool | |

Singleton ∷ Ord a ⇒ SetFn fn '[a] (Set a) | |

Union ∷ Ord a ⇒ SetFn fn '[Set a, Set a] (Set a) | |

Elem ∷ Eq a ⇒ SetFn fn '[a, [a]] Bool | |

FromList ∷ Ord a ⇒ SetFn fn '[[a]] (Set a) |

#### Instances

FunctionLike (SetFn fn) Source # | |

BaseUniverse fn ⇒ Functions (SetFn fn) fn Source # | |

Defined in Constrained.Base 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 # | |

Eq (SetFn fn args res) Source # | |

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

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

FunctionLike (MapFn fn) Source # | |

BaseUniverse fn ⇒ Functions (MapFn fn) fn Source # | |

Defined in Constrained.Spec.Map 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 # | |

Eq (MapFn fn args res) Source # | |