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 # | |