parameterized-utils-1.0.1: Classes and data structures for working with data-kind indexed types

Copyright(c) Galois Inc 2014-16
MaintainerJoe Hendrix <jhendrix@galois.com>
Safe HaskellTrustworthy
LanguageHaskell98

Data.Parameterized.Context

Contents

Description

This module reexports either Data.Parameterized.Context.Safe or Data.Parameterized.Context.Unsafe depending on the the unsafe-operations compile-time flag.

It also defines some utility typeclasses for transforming between curried and uncurried versions of functions over contexts.

Synopsis

Documentation

singleton :: f tp -> Assignment f (EmptyCtx ::> tp) Source #

Create a single element context.

toVector :: Assignment f tps -> (forall tp. f tp -> e) -> Vector e Source #

Convert the assignment to a vector.

pattern (:>) :: () => ctx' ~ (ctx ::> tp) => Assignment f ctx -> f tp -> Assignment f ctx' infixl 9 Source #

Pattern synonym for extending an assignment on the right

pattern Empty :: () => ctx ~ EmptyCtx => Assignment f ctx Source #

Pattern synonym for the empty assignment

decompose :: Assignment f (ctx ::> tp) -> (Assignment f ctx, f tp) Source #

null :: Assignment f ctx -> Bool Source #

Views

Return true if assignment is empty.

init :: Assignment f (ctx ::> tp) -> Assignment f ctx Source #

Return assignment with all but the last block.

last :: Assignment f (ctx ::> tp) -> f tp Source #

Return the last element in the assignment.

view :: forall f ctx. Assignment f ctx -> AssignView f ctx Source #

Deprecated: Use viewAssign or the Empty and :> patterns instead.

View an assignment as either empty or an assignment with one appended.

forIndexM :: forall ctx m. Applicative m => Size ctx -> (forall tp. Index ctx tp -> m ()) -> m () Source #

'forIndexM sz f' calls f on indices '[0..sz-1]'.

generateSome :: forall f. Int -> (Int -> Some f) -> Some (Assignment f) Source #

Generate an assignment with some context type that is not known.

generateSomeM :: forall m f. Applicative m => Int -> (Int -> m (Some f)) -> m (Some (Assignment f)) Source #

Generate an assignment with some context type that is not known.

fromList :: [Some f] -> Some (Assignment f) Source #

Create an assignment from a list of values.

Context extension and embedding utilities

data CtxEmbedding (ctx :: Ctx k) (ctx' :: Ctx k) Source #

Context embedding.

Constructors

CtxEmbedding 

Fields

class ExtendContext (f :: Ctx k -> *) where Source #

Minimal complete definition

extendContext

Methods

extendContext :: Diff ctx ctx' -> f ctx -> f ctx' Source #

class ExtendContext' (f :: Ctx k -> k' -> *) where Source #

Minimal complete definition

extendContext'

Methods

extendContext' :: Diff ctx ctx' -> f ctx v -> f ctx' v Source #

Instances
ExtendContext' (Index :: Ctx k' -> k' -> *) Source # 
Instance details

Defined in Data.Parameterized.Context

Methods

extendContext' :: Diff ctx ctx' -> Index ctx v -> Index ctx' v Source #

class ApplyEmbedding (f :: Ctx k -> *) where Source #

Minimal complete definition

applyEmbedding

Methods

applyEmbedding :: CtxEmbedding ctx ctx' -> f ctx -> f ctx' Source #

class ApplyEmbedding' (f :: Ctx k -> k' -> *) where Source #

Minimal complete definition

applyEmbedding'

Methods

applyEmbedding' :: CtxEmbedding ctx ctx' -> f ctx v -> f ctx' v Source #

Instances
ApplyEmbedding' (Index :: Ctx k' -> k' -> *) Source # 
Instance details

Defined in Data.Parameterized.Context

Methods

applyEmbedding' :: CtxEmbedding ctx ctx' -> Index ctx v -> Index ctx' v Source #

extendEmbeddingRightDiff :: forall ctx ctx' ctx''. Diff ctx' ctx'' -> CtxEmbedding ctx ctx' -> CtxEmbedding ctx ctx'' Source #

extendEmbeddingBoth :: forall ctx ctx' tp. CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp) Source #

ctxeAssignment :: Lens (CtxEmbedding ctx1 ctx') (CtxEmbedding ctx2 ctx') (Assignment (Index ctx') ctx1) (Assignment (Index ctx') ctx2) Source #

Static indexing and lenses for assignments

type Idx n ctx r = (ValidIx n ctx, Idx' (FromLeft ctx n) ctx r) Source #

Constraint synonym used for getting an Index into a Ctx. n is the zero-based, left-counted index into the list of types ctx which has the type r.

field :: forall n ctx f r. Idx n ctx r => Lens' (Assignment f ctx) (f r) Source #

Get a lens for an position in an Assignment by zero-based, left-to-right position. The position must be specified using TypeApplications for the n parameter.

natIndex :: forall n ctx r. Idx n ctx r => Index ctx r Source #

Compute an Index value for a particular position in a Ctx. The TypeApplications extension will be needed to disambiguate the choice of the type n.

natIndexProxy :: forall n ctx r proxy. Idx n ctx r => proxy n -> Index ctx r Source #

This version of natIndex is suitable for use without the TypeApplications extension.

Currying and uncurrying for assignments

type family CurryAssignment (ctx :: Ctx k) (f :: k -> *) (x :: *) :: * where ... Source #

This type family is used to define currying/uncurrying operations on assignments. It is best understood by seeing its evaluation on several examples:

CurryAssignment EmptyCtx f x = x
CurryAssignment (EmptyCtx ::> a) f x = f a -> x
CurryAssignment (EmptyCtx ::> a ::> b) f x = f a -> f b -> x
CurryAssignment (EmptyCtx ::> a ::> b ::> c) f x = f a -> f b -> f c -> x

Equations

CurryAssignment EmptyCtx f x = x 
CurryAssignment (ctx ::> a) f x = CurryAssignment ctx f (f a -> x) 

class CurryAssignmentClass (ctx :: Ctx k) where Source #

This class implements two methods that witness the isomorphism between curried and uncurried functions.

Minimal complete definition

curryAssignment, uncurryAssignment

Methods

curryAssignment :: (Assignment f ctx -> x) -> CurryAssignment ctx f x Source #

Transform a function that accepts an assignment into one with a separate variable for each element of the assignment.

uncurryAssignment :: CurryAssignment ctx f x -> Assignment f ctx -> x Source #

Transform a curried function into one that accepts an assignment value.

Size and Index values

size3 :: Size (((EmptyCtx ::> a) ::> b) ::> c) Source #

size4 :: Size ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) Source #

size5 :: Size (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) Source #

size6 :: Size ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) Source #

i1of3 :: Index (((EmptyCtx ::> a) ::> b) ::> c) a Source #

i2of3 :: Index (((EmptyCtx ::> a) ::> b) ::> c) b Source #

i3of3 :: Index (((EmptyCtx ::> a) ::> b) ::> c) c Source #

i1of4 :: Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) a Source #

i2of4 :: Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) b Source #

i3of4 :: Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) c Source #

i4of4 :: Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) d Source #

i1of5 :: Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) a Source #

i2of5 :: Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) b Source #

i3of5 :: Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) c Source #

i4of5 :: Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) d Source #

i5of5 :: Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) e Source #

i1of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) a Source #

i2of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) b Source #

i3of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) c Source #

i4of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) d Source #

i5of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) e Source #

i6of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) f Source #