hobbits-1.3.1: A library for canonically representing terms with binding
Copyright(c) 2016 Edwin Westbrook
LicenseBSD3
Maintainerwestbrook@galois.com
Stabilityexperimental
PortabilityGHC
Safe HaskellSafe-Inferred
LanguageHaskell2010

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.

Synopsis

Right-lists as a datatype

data RList a Source #

A form of lists where elements are added to the right instead of the left

Constructors

RNil 
(RList a) :> a 

type family (r1 :: RList k) :++: (r2 :: RList k) :: RList k infixr 5 Source #

Append two RLists at the type level

Instances

Instances details
type (r :: RList k) :++: ('RNil :: RList k) Source # 
Instance details

Defined in Data.Type.RList

type (r :: RList k) :++: ('RNil :: RList k) = r
type (r1 :: RList a1) :++: (r2 :> a2 :: RList a1) Source # 
Instance details

Defined in Data.Type.RList

type (r1 :: RList a1) :++: (r2 :> a2 :: RList a1) = (r1 :++: r2) :> a2

Proofs of membership in a type-level list

data Member (ctx :: RList k1) (a :: k2) 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 

Instances

Instances details
TestEquality (Member ctx :: k -> Type) Source # 
Instance details

Defined in Data.Type.RList

Methods

testEquality :: forall (a :: k0) (b :: k0). Member ctx a -> Member ctx b -> Maybe (a :~: b) #

Eq (Member ctx a) Source # 
Instance details

Defined in Data.Type.RList

Methods

(==) :: Member ctx a -> Member ctx a -> Bool #

(/=) :: Member ctx a -> Member ctx a -> Bool #

Show (Member r a) Source # 
Instance details

Defined in Data.Type.RList

Methods

showsPrec :: Int -> Member r a -> ShowS #

show :: Member r a -> String #

showList :: [Member r a] -> ShowS #

NuMatching (Member ctx a) Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatchingInstances

Closable (Member ctx a) Source # 
Instance details

Defined in Data.Binding.Hobbits.Closed

Methods

toClosed :: Member ctx a -> Closed (Member ctx a) Source #

Liftable (Member c a) Source # 
Instance details

Defined in Data.Binding.Hobbits.Liftable

Methods

mbLift :: forall k (ctx :: RList k). Mb ctx (Member c a) -> Member c a Source #

weakenMemberL :: Proxy r1 -> Member r2 a -> Member (r1 :++: r2) a Source #

Weaken a Member proof by prepending another context to the context it proves membership in

Proofs that one list equals the append of two others

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) 

mkAppend :: RAssign f c2 -> Append c1 c2 (c1 :++: c2) Source #

Make an Append proof from any RAssign vector for the second argument of the append.

mkMonoAppend :: Proxy c1 -> RAssign f c2 -> Append c1 c2 (c1 :++: c2) Source #

A version of mkAppend that takes in a Proxy argument.

proxiesFromAppend :: Append c1 c2 c -> RAssign Proxy c2 Source #

The inverse of mkAppend, that builds an RAssign from an Append

Contexts

data RAssign (f :: k -> *) (c :: RList k) where Source #

An RAssign f r an assignment of an f a for each a in the RList r

Constructors

MNil :: RAssign f RNil 
(:>:) :: RAssign f c -> f a -> RAssign f (c :> a) 

Instances

Instances details
Show (RAssign (Name :: k -> Type) c) Source # 
Instance details

Defined in Data.Binding.Hobbits.Internal.Name

NuMatchingAny1 f => NuMatching (RAssign f ctx) Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

ClosableAny1 f => Closable (RAssign f ctx) Source # 
Instance details

Defined in Data.Binding.Hobbits.Closed

Methods

toClosed :: RAssign f ctx -> Closed (RAssign f ctx) Source #

empty :: RAssign f RNil Source #

Create an empty RAssign vector.

singleton :: f a -> RAssign f (RNil :> a) Source #

Create a singleton RAssign vector.

get :: Member c a -> RAssign f c -> f a Source #

Look up an element of an RAssign vector using a Member proof

data HApply (f :: k1 -> Type) (a :: k2) where Source #

Heterogeneous type application, including a proof that the input kind of the function equals the kind of the type argument

Constructors

HApply :: forall k (f :: k -> Type) (a :: k). f a -> HApply f a 

hget :: forall k1 k2 (f :: k1 -> Type) (c :: RList k1) (a :: k2). Member c a -> RAssign f c -> HApply f a Source #

Look up an element of an RAssign vector using a Member proof at what GHC thinks might be a different kind, i.e., heterogeneously

modify :: Member c a -> (f a -> f a) -> RAssign f c -> RAssign f c Source #

Modify an element of an RAssign vector using a Member proof.

set :: Member c a -> f a -> RAssign f c -> RAssign f c Source #

Set an element of an RAssign vector using a Member proof.

memberElem :: TestEquality f => f a -> RAssign f ctx -> Maybe (Member ctx a) Source #

Test if an object is in an RAssign, returning a Member proof if it is

map :: (forall x. f x -> g x) -> RAssign f c -> RAssign g c Source #

Map a function on all elements of an RAssign vector.

mapRAssign :: (forall x. f x -> g x) -> RAssign f c -> RAssign g c Source #

An alternate name for map that does not clash with the prelude

map2 :: (forall x. f x -> g x -> h x) -> RAssign f c -> RAssign g c -> RAssign h c Source #

Map a binary function on all pairs of elements of two RAssign vectors.

tail :: RAssign f (ctx :> a) -> RAssign f ctx Source #

Take the tail of an RAssign

toList :: RAssign (Constant a) c -> [a] Source #

Convert a monomorphic RAssign to a list

mapToList :: (forall a. f a -> b) -> RAssign f ctx -> [b] Source #

Map a function with monomorphic output type across an RAssign to create a standard list:

mapToList f = toList . map (Constant . f)

append :: RAssign f c1 -> RAssign f c2 -> RAssign f (c1 :++: c2) Source #

Append two RAssign vectors.

foldr :: (forall a. f a -> r -> r) -> r -> RAssign f ctx -> r Source #

Perform a right fold across an RAssign

split :: c ~ (c1 :++: c2) => prx c1 -> RAssign any c2 -> RAssign f c -> (RAssign f c1, RAssign f c2) Source #

Split an RAssign vector into two pieces. The first argument is a phantom argument that gives the form of the first list piece.

members :: RAssign f c -> RAssign (Member c) c Source #

Create a vector of proofs that each type in c is a Member of c.

class TypeCtx ctx where Source #

A type-class which ensures that ctx is a valid context, i.e., has | the form (RNil :> t1 :> ... :> tn) for some types t1 through tn

Instances

Instances details
TypeCtx ('RNil :: RList k) Source # 
Instance details

Defined in Data.Type.RList

TypeCtx ctx => TypeCtx (ctx :> a :: RList k) Source # 
Instance details

Defined in Data.Type.RList