Copyright	(c) Galois Inc 2014-16
Maintainer	Joe Hendrix <jhendrix@galois.com>
Safe Haskell	Trustworthy
Language	Haskell98

Data.Parameterized.Context

Contents

Context extension and embedding utilities
Static indexing and lenses for assignments
Currying and uncurrying for assignments
Size and Index values

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

module Data.Parameterized.Context.Unsafe
singleton :: f tp -> Assignment f (EmptyCtx ::> tp)
toVector :: Assignment f tps -> (forall tp. f tp -> e) -> Vector e
pattern (:>) :: () => ctx' ~ (ctx ::> tp) => Assignment f ctx -> f tp -> Assignment f ctx'
pattern Empty :: () => ctx ~ EmptyCtx => Assignment f ctx
decompose :: Assignment f (ctx ::> tp) -> (Assignment f ctx, f tp)
null :: Assignment f ctx -> Bool
init :: Assignment f (ctx ::> tp) -> Assignment f ctx
last :: Assignment f (ctx ::> tp) -> f tp
view :: forall f ctx. Assignment f ctx -> AssignView f ctx
forIndexM :: forall ctx m. Applicative m => Size ctx -> (forall tp. Index ctx tp -> m ()) -> m ()
generateSome :: forall f. Int -> (Int -> Some f) -> Some (Assignment f)
generateSomeM :: forall m f. Applicative m => Int -> (Int -> m (Some f)) -> m (Some (Assignment f))
fromList :: [Some f] -> Some (Assignment f)
data CtxEmbedding (ctx :: Ctx k) (ctx' :: Ctx k) = CtxEmbedding {
- _ctxeSize :: Size ctx'
- _ctxeAssignment :: Assignment (Index ctx') ctx
}
class ExtendContext (f :: Ctx k -> *) where
class ExtendContext' (f :: Ctx k -> k' -> *) where
class ApplyEmbedding (f :: Ctx k -> *) where
class ApplyEmbedding' (f :: Ctx k -> k' -> *) where
identityEmbedding :: Size ctx -> CtxEmbedding ctx ctx
extendEmbeddingRightDiff :: forall ctx ctx' ctx''. Diff ctx' ctx'' -> CtxEmbedding ctx ctx' -> CtxEmbedding ctx ctx''
extendEmbeddingRight :: CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp)
extendEmbeddingBoth :: forall ctx ctx' tp. CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
ctxeSize :: Simple Lens (CtxEmbedding ctx ctx') (Size ctx')
ctxeAssignment :: Lens (CtxEmbedding ctx1 ctx') (CtxEmbedding ctx2 ctx') (Assignment (Index ctx') ctx1) (Assignment (Index ctx') ctx2)
type Idx n ctx r = (ValidIx n ctx, Idx' (FromLeft ctx n) ctx r)
field :: forall n ctx f r. Idx n ctx r => Lens' (Assignment f ctx) (f r)
natIndex :: forall n ctx r. Idx n ctx r => Index ctx r
natIndexProxy :: forall n ctx r proxy. Idx n ctx r => proxy n -> Index ctx r
type family CurryAssignment (ctx :: Ctx k) (f :: k -> *) (x :: *) :: * where ...
class CurryAssignmentClass (ctx :: Ctx k) where
size1 :: Size (EmptyCtx ::> a)
size2 :: Size ((EmptyCtx ::> a) ::> b)
size3 :: Size (((EmptyCtx ::> a) ::> b) ::> c)
size4 :: Size ((((EmptyCtx ::> a) ::> b) ::> c) ::> d)
size5 :: Size (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e)
size6 :: Size ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f)
i1of2 :: Index ((EmptyCtx ::> a) ::> b) a
i2of2 :: Index ((EmptyCtx ::> a) ::> b) b
i1of3 :: Index (((EmptyCtx ::> a) ::> b) ::> c) a
i2of3 :: Index (((EmptyCtx ::> a) ::> b) ::> c) b
i3of3 :: Index (((EmptyCtx ::> a) ::> b) ::> c) c
i1of4 :: Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) a
i2of4 :: Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) b
i3of4 :: Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) c
i4of4 :: Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) d
i1of5 :: Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) a
i2of5 :: Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) b
i3of5 :: Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) c
i4of5 :: Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) d
i5of5 :: Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) e
i1of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) a
i2of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) b
i3of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) c
i4of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) d
i5of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) e
i6of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) f

Documentation

module Data.Parameterized.Context.Unsafe

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 _ctxeSize :: Size ctx' _ctxeAssignment :: Assignment (Index ctx') ctx

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 #

identityEmbedding :: Size ctx -> CtxEmbedding ctx ctx Source #

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

extendEmbeddingRight :: CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp) Source #

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

ctxeSize :: Simple Lens (CtxEmbedding ctx ctx') (Size ctx') 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.

Instances

CurryAssignmentClass (EmptyCtx :: Ctx k) Source #
Instance details Defined in Data.Parameterized.Context Methods curryAssignment :: (Assignment f EmptyCtx -> x) -> CurryAssignment EmptyCtx f x Source # uncurryAssignment :: CurryAssignment EmptyCtx f x -> Assignment f EmptyCtx -> x Source #
CurryAssignmentClass ctx => CurryAssignmentClass (ctx ::> a :: Ctx k) Source #
Instance details Defined in Data.Parameterized.Context Methods curryAssignment :: (Assignment f (ctx ::> a) -> x) -> CurryAssignment (ctx ::> a) f x Source # uncurryAssignment :: CurryAssignment (ctx ::> a) f x -> Assignment f (ctx ::> a) -> x Source #

Size and Index values

size1 :: Size (EmptyCtx ::> a) Source #

size2 :: Size ((EmptyCtx ::> a) ::> b) Source #

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 #

i1of2 :: Index ((EmptyCtx ::> a) ::> b) a Source #

i2of2 :: Index ((EmptyCtx ::> a) ::> b) b 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 #