Data.Parameterized.Context

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.

Documentation

module Data.Parameterized.Context.Unsafe

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

Create a single element context.

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

Convert the assignment to a vector.

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

Pattern synonym for extending an assignment on the right

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

Pattern synonym for the empty assignment

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

null :: Assignment f ctx -> Bool

Return true if assignment is empty.

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

Return assignment with all but the last block.

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

Return the last element in the assignment.

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

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

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

take :: forall f ctx ctx'. Size ctx -> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx

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

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

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

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))

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

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

Create an assignment from a list of values.

traverseAndCollect :: (Monoid w, Applicative m) => (forall tp. Index ctx tp -> f tp -> m w) -> Assignment f ctx -> m w

Visit each of the elements in an Assignment in order from left to right and collect the results using the provided Monoid.

Context extension and embedding utilities

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

This datastructure contains a proof that the first context is embeddable in the second. This is useful if we want to add extend an existing term under a larger context.

Constructors

CtxEmbedding

Fields

• _ctxeSize :: Size ctx'
• _ctxeAssignment :: Assignment (Index ctx') ctx

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

Methods

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

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

Methods

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

Instances

ExtendContext' (Index :: Ctx k' -> k' -> Type)

Defined in Data.Parameterized.Context

Methods

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

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

Methods

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

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

Methods

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

Instances

ApplyEmbedding' (Index :: Ctx k' -> k' -> Type)

Defined in Data.Parameterized.Context

Methods

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

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)

appendEmbedding :: Size ctx -> Size ctx' -> CtxEmbedding ctx (ctx <+> ctx')

ctxeSize :: Simple Lens (CtxEmbedding ctx ctx') (Size ctx')

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

Static indexing and lenses for assignments

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

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)

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

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

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 ...

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

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

Methods

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

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

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

Instances

CurryAssignmentClass (EmptyCtx :: Ctx k)

Defined in Data.Parameterized.Context

Methods

curryAssignment :: (Assignment f EmptyCtx -> x) -> CurryAssignment EmptyCtx f x

uncurryAssignment :: CurryAssignment EmptyCtx f x -> Assignment f EmptyCtx -> x

CurryAssignmentClass ctx => CurryAssignmentClass (ctx ::> a :: Ctx k)

Defined in Data.Parameterized.Context

Methods

curryAssignment :: (Assignment f (ctx ::> a) -> x) -> CurryAssignment (ctx ::> a) f x

uncurryAssignment :: CurryAssignment (ctx ::> a) f x -> Assignment f (ctx ::> a) -> x

Size and Index values

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