Safe Haskell	None
Language	Haskell98

Language.SMTLib2.Internals.Type.List

Synopsis

Documentation

type family Head (lst :: [a]) :: a where ... Source #

Equations

Head (x ': xs) = x

type family Tail (lst :: [a]) :: [a] where ... Source #

Equations

Tail (x ': xs) = xs

type family Index (lst :: [a]) (idx :: Nat) :: a where ... Source #

Equations

Index (x ': xs) Z = x
Index (x ': xs) (S n) = Index xs n

type family Insert (lst :: [a]) (idx :: Nat) (el :: a) :: [a] where ... Source #

Equations

Insert (x ': xs) Z y = y ': xs
Insert (x ': xs) (S n) y = x ': Insert xs n y

type family Remove (lst :: [a]) (idx :: Nat) :: [a] where ... Source #

Equations

Remove (x ': xs) Z = xs
Remove (x ': xs) (S n) = x ': Remove xs n

type family Append (lst :: [a]) (el :: a) :: [a] where ... Source #

Equations

Append '[] y = y ': '[]
Append (x ': xs) y = x ': Append xs y

type family Length (lst :: [a]) :: Nat where ... Source #

Equations

Length '[] = Z
Length (x ': xs) = S (Length xs)

type family Drop (lst :: [a]) (i :: Nat) :: [a] where ... Source #

Equations

Drop lst Z = lst
Drop (x ': xs) (S n) = Drop xs n

type family Take (lst :: [a]) (i :: Nat) :: [a] where ... Source #

Equations

Take xs Z = '[]
Take (x ': xs) (S n) = x ': Take xs n

type family StripPrefix (lst :: [a]) (pre :: [a]) :: [a] where ... Source #

Equations

StripPrefix xs '[] = xs
StripPrefix (x ': xs) (x ': ys) = StripPrefix xs ys

type family Last (lst :: [a]) :: a where ... Source #

Equations

Last '[x] = x
Last (x ': (y ': rest)) = Last (y ': rest)

type family DropLast (lst :: [a]) :: [a] where ... Source #

Equations

DropLast '[x] = '[]
DropLast (x ': (y ': rest)) = x ': DropLast (y ': rest)

type family Reverse (lst :: [a]) :: [a] where ... Source #

Equations

Reverse '[] = '[]
Reverse (x ': xs) = Append (Reverse xs) x

type family Map (lst :: [a]) (f :: a -> b) :: [b] where ... Source #

Equations

Map '[] f = '[]
Map (x ': xs) f = f x ': Map xs f

type family Concat (xs :: [a]) (ys :: [a]) :: [a] where ... Source #

Equations

Concat '[] ys = ys
Concat (x ': xs) ys = x ': Concat xs ys

type family Replicate (n :: Nat) (x :: a) :: [a] where ... Source #

Equations

Replicate Z x = '[]
Replicate (S n) x = x ': Replicate n x

data List e tp where Source #

Strongly typed heterogenous lists.

A List e '[tp1,tp2,tp3] contains 3 elements of types e tp1, e tp2 and e tp3 respectively.

As an example, the following list contains two types:

>>> int ::: bool ::: Nil :: List Repr '[IntType,BoolType]
[IntRepr,BoolRepr]

Constructors

Nil :: List e '[]
(:::) :: e x -> List e xs -> List e (x ': xs) infixr 9

Instances

HasMonad (m (List Type e tp)) Source #
Associated Types type MatchMonad (m (List Type e tp)) (m :: * -> ) :: Constraint Source # type MonadResult (m (List Type e tp)) :: Source # Methods embedM :: (Applicative m, MatchMonad (m (List Type e tp)) m) => m (List Type e tp) -> m (MonadResult (m (List Type e tp))) Source #
GCompare a e => GCompare [a] (List a e) Source #
Methods gcompare :: f a -> f b -> GOrdering (List a e) a b #
GEq a e => GEq [a] (List a e) Source #
Methods geq :: f a -> f b -> Maybe ((List a e := a) b) #
GShow a e => GShow [a] (List a e) Source #
Methods gshowsPrec :: Int -> t a -> ShowS #
GEq a e => Eq (List a e lst) Source #
Methods (==) :: List a e lst -> List a e lst -> Bool # (/=) :: List a e lst -> List a e lst -> Bool #
GCompare a e => Ord (List a e lst) Source #
Methods compare :: List a e lst -> List a e lst -> Ordering # (<) :: List a e lst -> List a e lst -> Bool # (<=) :: List a e lst -> List a e lst -> Bool # (>) :: List a e lst -> List a e lst -> Bool # (>=) :: List a e lst -> List a e lst -> Bool # max :: List a e lst -> List a e lst -> List a e lst # min :: List a e lst -> List a e lst -> List a e lst #
GShow a e => Show (List a e lst) Source #
Methods showsPrec :: Int -> List a e lst -> ShowS # show :: List a e lst -> String # showList :: [List a e lst] -> ShowS #
HasMonad (List Type e tp) Source #
Associated Types type MatchMonad (List Type e tp) (m :: * -> ) :: Constraint Source # type MonadResult (List Type e tp) :: Source # Methods embedM :: (Applicative m, MatchMonad (List Type e tp) m) => List Type e tp -> m (MonadResult (List Type e tp)) Source #
type MonadResult (m (List Type e tp)) Source #
type MonadResult (m (List Type e tp)) = List Type e tp
type MatchMonad (m (List Type e tp)) m' Source #
type MatchMonad (m (List Type e tp)) m' = (~) (* -> *) m m'
type MonadResult (List Type e tp) Source #
type MonadResult (List Type e tp) = List Type e tp
type MatchMonad (List Type e tp) m Source #
type MatchMonad (List Type e tp) m = ()

list :: [ExpQ] -> ExpQ Source #

nil :: List e '[] Source #

list1 :: e t1 -> List e '[t1] Source #

list2 :: e t1 -> e t2 -> List e '[t1, t2] Source #

list3 :: e t1 -> e t2 -> e t3 -> List e '[t1, t2, t3] Source #

reifyList :: (forall r'. a -> (forall tp. e tp -> r') -> r') -> [a] -> (forall tp. List e tp -> r) -> r Source #

Get a static representation of a dynamic list.

For example, to convert a list of strings into a list of types:

>>> reifyList (\name f -> case name of { "int" -> f int ; "bool" -> f bool }) ["bool","int"] show
"[BoolRepr,IntRepr]"

access :: Monad m => List e lst -> Natural idx -> (e (Index lst idx) -> m (a, e tp)) -> m (a, List e (Insert lst idx tp)) Source #

access' :: Monad m => List e lst -> Natural idx -> (e (Index lst idx) -> m (a, e (Index lst idx))) -> m (a, List e lst) Source #

head :: List e lst -> e (Head lst) Source #

tail :: List e lst -> List e (Tail lst) Source #

index :: List e lst -> Natural idx -> e (Index lst idx) Source #

indexDyn :: Integral i => List e tps -> i -> (forall tp. e tp -> a) -> a Source #

insert :: List e lst -> Natural idx -> e tp -> List e (Insert lst idx tp) Source #

remove :: List e lst -> Natural idx -> List e (Remove lst idx) Source #

mapM :: Monad m => (forall x. e x -> m (e' x)) -> List e lst -> m (List e' lst) Source #

mapIndexM :: Monad m => (forall n. Natural n -> e (Index lst n) -> m (e' (Index lst n))) -> List e lst -> m (List e' lst) Source #

traverse :: Applicative f => (forall x. e x -> f (e' x)) -> List e lst -> f (List e' lst) Source #

cons :: e x -> List e xs -> List e (x ': xs) Source #

append :: List e xs -> e x -> List e (Append xs x) Source #

length :: List e lst -> Natural (Length lst) Source #

drop :: List e lst -> Natural i -> List e (Drop lst i) Source #

take :: List e lst -> Natural i -> List e (Take lst i) Source #

last :: List e lst -> e (Last lst) Source #

dropLast :: List e lst -> List e (DropLast lst) Source #

stripPrefix :: GEq e => List e lst -> List e pre -> Maybe (List e (StripPrefix lst pre)) Source #

reverse :: List e lst -> List e (Reverse lst) Source #

map :: List e lst -> (forall x. e x -> e (f x)) -> List e (Map lst f) Source #

unmap :: List p lst -> List e (Map lst f) -> (forall x. e (f x) -> e x) -> List e lst Source #

unmapM :: Monad m => List p lst -> List e (Map lst f) -> (forall x. e (f x) -> m (e x)) -> m (List e lst) Source #

mapM' :: Monad m => List e lst -> (forall x. e x -> m (e (f x))) -> m (List e (Map lst f)) Source #

concat :: List e xs -> List e ys -> List e (Concat xs ys) Source #

replicate :: Natural n -> e x -> List e (Replicate n x) Source #

toList :: Monad m => (forall x. e x -> m a) -> List e lst -> m [a] Source #

toListIndex :: Monad m => (forall n. Natural n -> e (Index lst n) -> m a) -> List e lst -> m [a] Source #

foldM :: Monad m => (forall x. s -> e x -> m s) -> s -> List e lst -> m s Source #

zipWithM :: Monad m => (forall x. e1 x -> e2 x -> m (e3 x)) -> List e1 lst -> List e2 lst -> m (List e3 lst) Source #

zipToListM :: Monad m => (forall x. e1 x -> e2 x -> m a) -> List e1 lst -> List e2 lst -> m [a] Source #

mapAccumM :: Monad m => (forall x. s -> e x -> m (s, e' x)) -> s -> List e xs -> m (s, List e' xs) Source #