| Copyright | (c) Galois Inc 2014-16 |
|---|---|
| Maintainer | Joe Hendrix <jhendrix@galois.com> |
| Safe Haskell | Trustworthy |
| Language | Haskell98 |
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.
- 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
- 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)
- getCtx :: forall n ctx f r. Idx n ctx r => Assignment f ctx -> f r
- setCtx :: forall n ctx f r. Idx n ctx r => f r -> Assignment f ctx -> Assignment f ctx
- 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
Documentation
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
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
Methods
extendContext :: Diff ctx ctx' -> f ctx -> f ctx' Source #
class ExtendContext' (f :: Ctx k -> k' -> *) where Source #
Minimal complete definition
Methods
extendContext' :: Diff ctx ctx' -> f ctx v -> f ctx' v Source #
Instances
| ExtendContext' k' k' (Index k') Source # | |
class ApplyEmbedding (f :: Ctx k -> *) where Source #
Minimal complete definition
Methods
applyEmbedding :: CtxEmbedding ctx ctx' -> f ctx -> f ctx' Source #
class ApplyEmbedding' (f :: Ctx k -> k' -> *) where Source #
Minimal complete definition
Methods
applyEmbedding' :: CtxEmbedding ctx ctx' -> f ctx v -> f ctx' v Source #
Instances
| ApplyEmbedding' k' k' (Index k') 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 #
ctxeAssignment :: Lens (CtxEmbedding ctx1 ctx') (CtxEmbedding ctx2 ctx') (Assignment (Index ctx') ctx1) (Assignment (Index ctx') ctx2) Source #
Static indexing and lenses for assignments
getCtx :: forall n ctx f r. Idx n ctx r => Assignment f ctx -> f r Source #
Get an element from an Assignment by zero-based, left-to-right position.
The position must be specified using TypeApplications for the n parameter.
setCtx :: forall n ctx f r. Idx n ctx r => f r -> Assignment f ctx -> Assignment f ctx Source #
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.
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
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 k (EmptyCtx k) Source # | |
| CurryAssignmentClass k ctx => CurryAssignmentClass k ((::>) k ctx a) Source # | |