| Copyright | (c) 2016 Edwin Westbrook |
|---|---|
| License | BSD3 |
| Maintainer | westbrook@galois.com |
| Stability | experimental |
| Portability | GHC |
| Safe Haskell | Safe |
| Language | Haskell98 |
Data.Type.RList
Description
A right list, or RList, is a list where cons adds to the end, or the
right-hand side, of a list. This is useful conceptually for contexts of
name-bindings, where the most recent name-binding is intuitively at the end
of the context.
- data RList a
- type family (r1 :: RList *) :++: (r2 :: RList *) :: RList *
- proxyCons :: Proxy r -> f a -> Proxy (r :> a)
- data Member ctx a where
- Member_Base :: Member (ctx :> a) a
- Member_Step :: Member ctx a -> Member (ctx :> b) a
- showsPrecMember :: Bool -> Member ctx a -> ShowS
- weakenMemberL :: Proxy r1 -> Member r2 a -> Member (r1 :++: r2) a
- membersEq :: Member ctx a -> Member ctx b -> Maybe (a :~: b)
- data Append ctx1 ctx2 ctx where
- Append_Base :: Append ctx RNil ctx
- Append_Step :: Append ctx1 ctx2 ctx -> Append ctx1 (ctx2 :> a) (ctx :> a)
- data MapRList f c where
- empty :: MapRList f RNil
- singleton :: f a -> MapRList f (RNil :> a)
- mapRListLookup :: Member c a -> MapRList f c -> f a
- mapMapRList :: (forall x. f x -> g x) -> MapRList f c -> MapRList g c
- mapMapRList2 :: (forall x. f x -> g x -> h x) -> MapRList f c -> MapRList g c -> MapRList h c
- appendMapRList :: MapRList f c1 -> MapRList f c2 -> MapRList f (c1 :++: c2)
- mkAppend :: MapRList f c2 -> Append c1 c2 (c1 :++: c2)
- mkMonoAppend :: Proxy c1 -> MapRList f c2 -> Append c1 c2 (c1 :++: c2)
- proxiesFromAppend :: Append c1 c2 c -> MapRList Proxy c2
- splitMapRList :: c ~ (c1 :++: c2) => Proxy c1 -> MapRList any c2 -> MapRList f c -> (MapRList f c1, MapRList f c2)
- members :: MapRList f c -> MapRList (Member c) c
- mapRListToList :: MapRList (Constant a) c -> [a]
- class TypeCtx ctx where
Documentation
data Member ctx a where Source #
A Member ctx a is a "proof" that the type a is in the type
list ctx, meaning that ctx equals
t0 ':>' a ':>' t1 ':>' ... ':>' tn
for some types t0,t1,...,tn.
Constructors
| Member_Base :: Member (ctx :> a) a | |
| Member_Step :: Member ctx a -> Member (ctx :> b) a |
data Append ctx1 ctx2 ctx where Source #
An Append ctx1 ctx2 ctx is a "proof" that ctx = ctx1 .:++: ctx2
Constructors
| Append_Base :: Append ctx RNil ctx | |
| Append_Step :: Append ctx1 ctx2 ctx -> Append ctx1 (ctx2 :> a) (ctx :> a) |
data MapRList f c where Source #
A MapRList f r is a vector with exactly one element of type f a for
each type a in the type RList r.
Instances
| Show (MapRList Name c) # | |
| (NuMatching1 f, NuMatchingList ctx) => NuMatching (MapRList f ctx) Source # | |
mapRListLookup :: Member c a -> MapRList f c -> f a Source #
mapMapRList :: (forall x. f x -> g x) -> MapRList f c -> MapRList g c Source #
Map a function on all elements of a MapRList vector.
mapMapRList2 :: (forall x. f x -> g x -> h x) -> MapRList f c -> MapRList g c -> MapRList h c Source #
Map a binary function on all pairs of elements of two MapRList vectors.
appendMapRList :: MapRList f c1 -> MapRList f c2 -> MapRList f (c1 :++: c2) Source #
Append two MapRList vectors.
splitMapRList :: c ~ (c1 :++: c2) => Proxy c1 -> MapRList any c2 -> MapRList f c -> (MapRList f c1, MapRList f c2) Source #
Split an MapRList vector into two pieces. The first argument is a
phantom argument that gives the form of the first list piece.
members :: MapRList f c -> MapRList (Member c) c Source #
Create a vector of proofs that each type in c is a Member of c.
mapRListToList :: MapRList (Constant a) c -> [a] Source #
Convert an MapRList to a list