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

Constrained.List

Synopsis

Documentation

data List (f ∷ k → Type) (as ∷ [k]) where Source #

A heterogeneous list / an inductive tuple. We use this heavily to represent arguments to functions in terms. A term application (c.f. Base) is represented as `App :: fn as b -> List (Term fn) as -> Term fn b` for example.

Constructors

NilList f '[] 
(:>) ∷ f a → List f as → List f (a ': as) infixr 5 

Instances

Instances details
HasVariables fn (List (Term fn) as) Source # 
Instance details

Defined in Constrained.Base

Methods

freeVarsList (Term fn) as → FreeVars fn Source #

freeVarSetList (Term fn) as → Set (Name fn) Source #

countOfName fn → List (Term fn) as → Int Source #

appearsInName fn → List (Term fn) as → Bool Source #

HasVariables fn (List (Weighted (Binder fn)) as) Source # 
Instance details

Defined in Constrained.Base

Methods

freeVarsList (Weighted (Binder fn)) as → FreeVars fn Source #

freeVarSetList (Weighted (Binder fn)) as → Set (Name fn) Source #

countOfName fn → List (Weighted (Binder fn)) as → Int Source #

appearsInName fn → List (Weighted (Binder fn)) as → Bool Source #

(∀ (a ∷ k). Show (f a)) ⇒ Show (List f as) Source # 
Instance details

Defined in Constrained.List

Methods

showsPrecIntList f as → ShowS Source #

showList f as → String Source #

showList ∷ [List f as] → ShowS Source #

(∀ a. Rename (f a)) ⇒ Rename (List f as) Source # 
Instance details

Defined in Constrained.Core

Methods

renameTypeable x ⇒ Var x → Var x → List f as → List f as Source #

(∀ (a ∷ k). Eq (f a)) ⇒ Eq (List f as) Source # 
Instance details

Defined in Constrained.List

Methods

(==)List f as → List f as → Bool Source #

(/=)List f as → List f as → Bool Source #

mapList ∷ (∀ a. f a → g a) → List f as → List g as Source #

mapListC ∷ ∀ c as f g. All c as ⇒ (∀ a. c a ⇒ f a → g a) → List f as → List g as Source #

mapMListApplicative m ⇒ (∀ a. f a → m (g a)) → List f as → m (List g as) Source #

mapMListC ∷ ∀ c as f g m. (Applicative m, All c as) ⇒ (∀ a. c a ⇒ f a → m (g a)) → List f as → m (List g as) Source #

foldMapListMonoid b ⇒ (∀ a. f a → b) → List f as → b Source #

foldMapListC ∷ ∀ c as b f. (All c as, Monoid b) ⇒ (∀ a. c a ⇒ f a → b) → List f as → b Source #

appendListList f as → List f bs → List f (Append as bs) Source #

lengthListList f as → Int Source #

type family Append as as' where ... Source #

Append two type-level lists

Equations

Append '[] as' = as' 
Append (a ': as) as' = a ': Append as as' 

type family MapList (f ∷ k → j) as where ... Source #

Map a type functor over a list

Equations

MapList f '[] = '[] 
MapList f (a ': as) = f a ': MapList f as 

data ListCtx f (as ∷ [Type]) c where Source #

A List with a hole in it, can be seen as a zipper over type-level lists.

We use this to represent contexts over terms in Base. For example, an application of f to a single variable of type a would be the pair `(fn as b, ListCtx Value as (HOLE a))` where HOLE (c.f. Base) is isomorphic to :~:.

Constructors

(:?) ∷ c a → List f as → ListCtx f (a ': as) c infixr 5 
(:!) ∷ f a → ListCtx f as c → ListCtx f (a ': as) c infixr 5 

pattern NilCtx ∷ c a → ListCtx f '[a] c Source #

A Convenient pattern for singleton contexts

pattern ListCtx ∷ () ⇒ as'' ~ Append as (a ': as') ⇒ List f as → c a → List f as' → ListCtx f as'' c Source #

A view of a ListCtx where you see the whole context at the same time.

data ListCtxWhole f as c where Source #

Internals for the ListCtx pattern

Constructors

ListCtxWholeList f as → c a → List f as' → ListCtxWhole f (Append as (a ': as')) c 

toWholeCtxListCtx f as c → ListCtxWhole f as c Source #

fromWholeCtxListCtxWhole f as c → ListCtx f as c Source #

fillListCtxListCtx f as c → (∀ a. c a → f a) → List f as Source #

mapListCtx ∷ (∀ a. f a → g a) → ListCtx f as c → ListCtx g as c Source #

mapListCtxC ∷ ∀ c as f g h. All c as ⇒ (∀ a. c a ⇒ f a → g a) → ListCtx f as h → ListCtx g as h Source #

type family FunTy ts res where ... Source #

A function type from ts to res: FunTy '[Int, Bool] Double = Int -> Bool -> Double

Equations

FunTy '[] a = a 
FunTy (a ': as) r = a → FunTy as r 

listShape ∷ ∀ as. TypeList as ⇒ List (Const ()) as Source #

Materialize the shape of the type list as, this is very useful for avoiding having to write type classes that recurse over as.

class TypeList ts where Source #

Higher-order functions for working on Lists

Methods

uncurryListFunTy (MapList f ts) r → List f ts → r Source #

uncurryList_ ∷ (∀ a. f a → a) → FunTy ts r → List f ts → r Source #

curryList ∷ (List f ts → r) → FunTy (MapList f ts) r Source #

curryList_ ∷ (∀ a. a → f a) → (List f ts → r) → FunTy ts r Source #

unfoldList ∷ (∀ a as. List f as → f a) → List f ts Source #

Instances

Instances details
TypeList ('[] ∷ [Type]) Source #

NOTE: the two instances for TypeList are `TypeList '[]` and `TypeList '(a : as)`. That way its basically just a structurally recursive function on type-level lists that computes the TypeList dictionary.

Instance details

Defined in Constrained.List

Methods

uncurryList ∷ ∀ (f ∷ TypeType) r. FunTy (MapList f '[]) r → List f '[] → r Source #

uncurryList_ ∷ (∀ a. f a → a) → FunTy '[] r → List f '[] → r Source #

curryList ∷ ∀ (f ∷ TypeType) r. (List f '[] → r) → FunTy (MapList f '[]) r Source #

curryList_ ∷ (∀ a. a → f a) → (List f '[] → r) → FunTy '[] r Source #

unfoldList ∷ (∀ a (as ∷ [Type]). List f as → f a) → List f '[] Source #

TypeList as ⇒ TypeList (a ': as) Source # 
Instance details

Defined in Constrained.List

Methods

uncurryList ∷ ∀ (f ∷ TypeType) r. FunTy (MapList f (a ': as)) r → List f (a ': as) → r Source #

uncurryList_ ∷ (∀ a0. f a0 → a0) → FunTy (a ': as) r → List f (a ': as) → r Source #

curryList ∷ ∀ (f ∷ TypeType) r. (List f (a ': as) → r) → FunTy (MapList f (a ': as)) r Source #

curryList_ ∷ (∀ a0. a0 → f a0) → (List f (a ': as) → r) → FunTy (a ': as) r Source #

unfoldList ∷ (∀ a0 (as0 ∷ [Type]). List f as0 → f a0) → List f (a ': as) Source #

type family All (c ∷ k → Constraint) (as ∷ [k]) ∷ Constraint where ... Source #

Equations

All c '[] = () 
All c (a ': as) = (c a, All c as)