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

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

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.

The Assignment type is isomorphic to the List type, except Assignments construct lists from the right-hand side, and instead of using type-level '[]-style lists, an Assignment is indexed by a type-level Ctx. The implementation of Assignments is also more efficent than List for lists of many elements, as it uses a balanced binary tree representation rather than a linear-time list. For a motivating example, see List.

Synopsis

Documentation

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

A context that can be determined statically at compiler time.

Methods

knownSize :: Size ctx Source #

Instances
KnownContext (EmptyCtx :: Ctx k) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

KnownContext ctx => KnownContext (ctx ::> tp :: Ctx k) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

knownSize :: Size (ctx ::> tp) Source #

Size

data Size (ctx :: Ctx k) Source #

Represents the size of a context.

Instances
ShowF (Size :: Ctx k -> Type) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

withShow :: p Size -> q tp -> (Show (Size tp) -> a) -> a Source #

showF :: Size tp -> String Source #

showsPrecF :: Int -> Size tp -> String -> String Source #

Show (Size ctx) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

showsPrec :: Int -> Size ctx -> ShowS #

show :: Size ctx -> String #

showList :: [Size ctx] -> ShowS #

sizeInt :: Size ctx -> Int Source #

Convert a context size to an Int.

zeroSize :: Size EmptyCtx Source #

The size of an empty context.

incSize :: Size ctx -> Size (ctx ::> tp) Source #

Increment the size to the next value.

decSize :: Size (ctx ::> tp) -> Size ctx Source #

extSize :: Size l -> Diff l r -> Size r Source #

Extend the size by a given difference.

addSize :: Size x -> Size y -> Size (x <+> y) Source #

The total size of two concatenated contexts.

data SizeView (ctx :: Ctx k) where Source #

Allows interpreting a size.

Constructors

ZeroSize :: SizeView EmptyCtx 
IncSize :: !(Size ctx) -> SizeView (ctx ::> tp) 

viewSize :: Size ctx -> SizeView ctx Source #

Project a size

Diff

data Diff (l :: Ctx k) (r :: Ctx k) Source #

Difference in number of elements between two contexts. The first context must be a sub-context of the other.

Instances
Category (Diff :: Ctx k -> Ctx k -> Type) Source #

Implemented with noDiff and addDiff

Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

id :: Diff a a #

(.) :: Diff b c -> Diff a b -> Diff a c #

noDiff :: Diff l l Source #

The identity difference. Identity element of Category instance.

addDiff :: Diff a b -> Diff b c -> Diff a c Source #

The addition of differences. Flipped binary operation of Category instance.

extendRight :: Diff l r -> Diff l (r ::> tp) Source #

Extend the difference to a sub-context of the right side.

appendDiff :: Size r -> Diff l (l <+> r) Source #

data DiffView a b where Source #

Constructors

NoDiff :: DiffView a a 
ExtendRightDiff :: Diff a b -> DiffView a (b ::> r) 

viewDiff :: Diff a b -> DiffView a b Source #

class KnownDiff (l :: Ctx k) (r :: Ctx k) where Source #

A difference that can be automatically inferred at compile time.

Methods

knownDiff :: Diff l r Source #

Instances
KnownDiff (l :: Ctx k) (l :: Ctx k) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

knownDiff :: Diff l l Source #

KnownDiff l r => KnownDiff (l :: Ctx k) (r ::> tp :: Ctx k) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

knownDiff :: Diff l (r ::> tp) Source #

data IsAppend l r where Source #

Proof that r = l + app for some app

Constructors

IsAppend :: Size app -> IsAppend l (l <+> app) 

diffIsAppend :: Diff l r -> IsAppend l r Source #

If l is a sub-context of r then extract out their "contextual difference", i.e., the app such that r = l + app

Indexing

data Index (ctx :: Ctx k) (tp :: k) Source #

An index is a reference to a position with a particular type in a context.

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

Defined in Data.Parameterized.Context

Methods

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

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

Defined in Data.Parameterized.Context

Methods

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

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

Defined in Data.Parameterized.Context.Unsafe

Methods

testEquality :: Index ctx a -> Index ctx b -> Maybe (a :~: b) #

HashableF (Index ctx :: k -> Type) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

hashWithSaltF :: Int -> Index ctx tp -> Int Source #

hashF :: Index ctx tp -> Int Source #

ShowF (Index ctx :: k -> Type) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

withShow :: p (Index ctx) -> q tp -> (Show (Index ctx tp) -> a) -> a Source #

showF :: Index ctx tp -> String Source #

showsPrecF :: Int -> Index ctx tp -> String -> String Source #

OrdF (Index ctx :: k -> Type) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

compareF :: Index ctx x -> Index ctx y -> OrderingF x y Source #

leqF :: Index ctx x -> Index ctx y -> Bool Source #

ltF :: Index ctx x -> Index ctx y -> Bool Source #

geqF :: Index ctx x -> Index ctx y -> Bool Source #

gtF :: Index ctx x -> Index ctx y -> Bool Source #

Eq (Index ctx tp) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

(==) :: Index ctx tp -> Index ctx tp -> Bool #

(/=) :: Index ctx tp -> Index ctx tp -> Bool #

Ord (Index ctx tp) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

compare :: Index ctx tp -> Index ctx tp -> Ordering #

(<) :: Index ctx tp -> Index ctx tp -> Bool #

(<=) :: Index ctx tp -> Index ctx tp -> Bool #

(>) :: Index ctx tp -> Index ctx tp -> Bool #

(>=) :: Index ctx tp -> Index ctx tp -> Bool #

max :: Index ctx tp -> Index ctx tp -> Index ctx tp #

min :: Index ctx tp -> Index ctx tp -> Index ctx tp #

Show (Index ctx tp) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

showsPrec :: Int -> Index ctx tp -> ShowS #

show :: Index ctx tp -> String #

showList :: [Index ctx tp] -> ShowS #

Hashable (Index ctx tp) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

hashWithSalt :: Int -> Index ctx tp -> Int #

hash :: Index ctx tp -> Int #

indexVal :: Index ctx tp -> Int Source #

baseIndex :: Index (EmptyCtx ::> tp) tp Source #

Index for first element in context.

skipIndex :: Index ctx x -> Index (ctx ::> y) x Source #

Increase context while staying at same index.

lastIndex :: Size (ctx ::> tp) -> Index (ctx ::> tp) tp Source #

Return the last index of a element.

nextIndex :: Size ctx -> Index (ctx ::> tp) tp Source #

Return the index of a element one past the size.

extendIndex :: KnownDiff l r => Index l tp -> Index r tp Source #

extendIndex' :: Diff l r -> Index l tp -> Index r tp Source #

forIndex :: forall ctx r. Size ctx -> (forall tp. r -> Index ctx tp -> r) -> r -> r Source #

Given a size n, an initial value v0, and a function f, the expression forIndex n v0 f is equivalent to v0 when n is zero, and f (forIndex (n-1) v0) (n-1) otherwise.

forIndexRange :: forall ctx r. Int -> Size ctx -> (forall tp. Index ctx tp -> r -> r) -> r -> r Source #

Given an index i, size n, a function f, value v, and a function f, the expression forIndex i n f v is equivalent to v when i >= sizeInt n, and f i (forIndexRange (i+1) n v) otherwise.

intIndex :: Int -> Size ctx -> Maybe (Some (Index ctx)) Source #

Return index at given integer or nothing if integer is out of bounds.

data IndexView ctx tp where Source #

View of indexes as pointing to the last element in the index range or pointing to an earlier element in a smaller range.

Constructors

IndexViewLast :: !(Size ctx) -> IndexView (ctx ::> t) t 
IndexViewInit :: !(Index ctx t) -> IndexView (ctx ::> u) t 
Instances
ShowF (IndexView ctx :: k -> Type) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

withShow :: p (IndexView ctx) -> q tp -> (Show (IndexView ctx tp) -> a) -> a Source #

showF :: IndexView ctx tp -> String Source #

showsPrecF :: Int -> IndexView ctx tp -> String -> String Source #

Show (IndexView ctx tp) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

showsPrec :: Int -> IndexView ctx tp -> ShowS #

show :: IndexView ctx tp -> String #

showList :: [IndexView ctx tp] -> ShowS #

viewIndex :: Size ctx -> Index ctx tp -> IndexView ctx tp Source #

Project an index

IndexRange

data IndexRange (ctx :: Ctx k) (sub :: Ctx k) Source #

This represents a contiguous range of indices.

allRange :: Size ctx -> IndexRange ctx ctx Source #

Return a range containing all indices in the context.

indexOfRange :: IndexRange ctx (EmptyCtx ::> e) -> Index ctx e Source #

indexOfRange returns the only index in a range.

dropHeadRange :: IndexRange ctx (x <+> y) -> Size x -> IndexRange ctx y Source #

dropHeadRange r n drops the first n elements in r.

dropTailRange :: IndexRange ctx (x <+> y) -> Size y -> IndexRange ctx x Source #

dropTailRange r n drops the last n elements in r.

Assignments

data Assignment (f :: k -> Type) (ctx :: Ctx k) Source #

An assignment is a sequence that maps each index with type tp to a value of type f tp.

This assignment implementation uses a binomial tree implementation that offers lookups and updates in time and space logarithmic with respect to the number of elements in the context.

Instances
TraversableFC (Assignment :: (k -> Type) -> Ctx k -> Type) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

traverseFC :: Applicative m => (forall (x :: k0). f x -> m (g x)) -> forall (x :: l). Assignment f x -> m (Assignment g x) Source #

FoldableFC (Assignment :: (k -> Type) -> Ctx k -> Type) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

foldMapFC :: Monoid m => (forall (x :: k0). f x -> m) -> forall (x :: l). Assignment f x -> m Source #

foldrFC :: (forall (x :: k0). f x -> b -> b) -> forall (x :: l). b -> Assignment f x -> b Source #

foldlFC :: (forall (x :: k0). b -> f x -> b) -> forall (x :: l). b -> Assignment f x -> b Source #

foldrFC' :: (forall (x :: k0). f x -> b -> b) -> forall (x :: l). b -> Assignment f x -> b Source #

foldlFC' :: (forall (x :: k0). b -> f x -> b) -> forall (x :: l). b -> Assignment f x -> b Source #

toListFC :: (forall (x :: k0). f x -> a) -> forall (x :: l). Assignment f x -> [a] Source #

OrdFC (Assignment :: (k -> Type) -> Ctx k -> Type) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

compareFC :: (forall (x :: k0) (y :: k0). f x -> f y -> OrderingF x y) -> forall (x :: l) (y :: l). Assignment f x -> Assignment f y -> OrderingF x y Source #

TestEqualityFC (Assignment :: (k -> Type) -> Ctx k -> Type) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

testEqualityFC :: (forall (x :: k0) (y :: k0). f x -> f y -> Maybe (x :~: y)) -> forall (x :: l) (y :: l). Assignment f x -> Assignment f y -> Maybe (x :~: y) Source #

FunctorFC (Assignment :: (k -> Type) -> Ctx k -> Type) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

fmapFC :: (forall (x :: k0). f x -> g x) -> forall (x :: l). Assignment f x -> Assignment g x Source #

IxedF' k (Assignment f ctx) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

ixF' :: IndexF (Assignment f ctx) x -> Lens' (Assignment f ctx) (IxValueF (Assignment f ctx) x) Source #

IxedF k (Assignment f ctx) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

ixF :: IndexF (Assignment f ctx) x -> Traversal' (Assignment f ctx) (IxValueF (Assignment f ctx) x) Source #

TestEquality f => TestEquality (Assignment f :: Ctx k -> Type) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

testEquality :: Assignment f a -> Assignment f b -> Maybe (a :~: b) #

HashableF f => HashableF (Assignment f :: Ctx k -> Type) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

hashWithSaltF :: Int -> Assignment f tp -> Int Source #

hashF :: Assignment f tp -> Int Source #

ShowF f => ShowF (Assignment f :: Ctx k -> Type) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

withShow :: p (Assignment f) -> q tp -> (Show (Assignment f tp) -> a) -> a Source #

showF :: Assignment f tp -> String Source #

showsPrecF :: Int -> Assignment f tp -> String -> String Source #

OrdF f => OrdF (Assignment f :: Ctx k -> Type) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

IsRepr f => IsRepr (Assignment f :: Ctx k -> Type) Source # 
Instance details

Defined in Data.Parameterized.WithRepr

Methods

withRepr :: Assignment f a -> (KnownRepr (Assignment f) a -> r) -> r Source #

KnownRepr (Assignment f :: Ctx k -> Type) (EmptyCtx :: Ctx k) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

(KnownRepr (Assignment f) ctx, KnownRepr f bt) => KnownRepr (Assignment f :: Ctx k -> Type) (ctx ::> bt :: Ctx k) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

knownRepr :: Assignment f (ctx ::> bt) Source #

TestEquality f => Eq (Assignment f ctx) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

(==) :: Assignment f ctx -> Assignment f ctx -> Bool #

(/=) :: Assignment f ctx -> Assignment f ctx -> Bool #

OrdF f => Ord (Assignment f ctx) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

compare :: Assignment f ctx -> Assignment f ctx -> Ordering #

(<) :: Assignment f ctx -> Assignment f ctx -> Bool #

(<=) :: Assignment f ctx -> Assignment f ctx -> Bool #

(>) :: Assignment f ctx -> Assignment f ctx -> Bool #

(>=) :: Assignment f ctx -> Assignment f ctx -> Bool #

max :: Assignment f ctx -> Assignment f ctx -> Assignment f ctx #

min :: Assignment f ctx -> Assignment f ctx -> Assignment f ctx #

ShowF f => Show (Assignment f ctx) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

showsPrec :: Int -> Assignment f ctx -> ShowS #

show :: Assignment f ctx -> String #

showList :: [Assignment f ctx] -> ShowS #

NFData (Assignment f ctx) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

rnf :: Assignment f ctx -> () #

HashableF f => Hashable (Assignment f ctx) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

hashWithSalt :: Int -> Assignment f ctx -> Int #

hash :: Assignment f ctx -> Int #

type IxValueF (Assignment f ctx) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

type IxValueF (Assignment f ctx) = f
type IndexF (Assignment f ctx) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

type IndexF (Assignment f ctx) = Index ctx

size :: Assignment f ctx -> Size ctx Source #

Return number of elements in assignment.

replicate :: Size ctx -> (forall tp. f tp) -> Assignment f ctx Source #

replicate n make a context with different copies of the same polymorphic value.

generate :: Size ctx -> (forall tp. Index ctx tp -> f tp) -> Assignment f ctx Source #

Generate an assignment

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

Generate an assignment in an Applicative context

empty :: Assignment f EmptyCtx Source #

Return empty assignment

extend :: Assignment f ctx -> f x -> Assignment f (ctx ::> x) Source #

adjust :: (f tp -> f tp) -> Index ctx tp -> Assignment f ctx -> Assignment f ctx Source #

Deprecated: Replace 'adjust f i asgn' with 'Lens.over (ixF i) f asgn' instead.

update :: Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx Source #

Deprecated: Replace 'update idx val asgn' with 'Lens.set (ixF idx) val asgn' instead.

adjustM :: Functor m => (f tp -> m (f tp)) -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx) Source #

Modify the value of an assignment at a particular index.

data AssignView f ctx where Source #

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

Constructors

AssignEmpty :: AssignView f EmptyCtx 
AssignExtend :: Assignment f ctx -> f tp -> AssignView f (ctx ::> tp) 

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

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

(!) :: Assignment f ctx -> Index ctx tp -> f tp Source #

Return value of assignment.

(!^) :: KnownDiff l r => Assignment f r -> Index l tp -> f tp Source #

Return value of assignment, where the index is into an initial sequence of the assignment.

zipWith :: (forall x. f x -> g x -> h x) -> Assignment f a -> Assignment g a -> Assignment h a Source #

zipWithM :: Applicative m => (forall x. f x -> g x -> m (h x)) -> Assignment f a -> Assignment g a -> m (Assignment h a) Source #

(<++>) :: Assignment f x -> Assignment f y -> Assignment f (x <+> y) Source #

traverseWithIndex :: Applicative m => (forall tp. Index ctx tp -> f tp -> m (g tp)) -> Assignment f ctx -> m (Assignment g ctx) Source #

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 #

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.

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

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.

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

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

traverseWithIndex_ :: Applicative m => (forall tp. Index ctx tp -> f tp -> m ()) -> Assignment f ctx -> m () Source #

Visit each of the elements in an Assignment in order from left to right, executing an action with each.

dropPrefix Source #

Arguments

:: TestEquality f 
=> Assignment f xs

Assignment to split

-> Assignment f prefix

Expected prefix

-> a

error continuation

-> (forall addl. xs ~ (prefix <+> addl) => Assignment f addl -> a)

success continuation

-> a 

Utility function for testing if xs is an assignment with prefix as a prefix, and computing the tail of xs not in the prefix, if so.

Context extension and embedding utilities

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

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

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

Methods

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

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

Methods

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

Instances
ExtendContext' (Index :: Ctx k' -> k' -> Type) 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 #

Methods

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

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

Methods

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

Instances
ApplyEmbedding' (Index :: Ctx k' -> k' -> Type) 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 #

appendEmbedding :: Size ctx -> Size ctx' -> CtxEmbedding ctx (ctx <+> 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.

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 #