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

Copyright | (c) Galois Inc 2015-2019
Maintainer | Joe Hendrix <jhendrix@galois.com>
Safe Haskell | Safe
Language | Haskell2010

Data.Parameterized.Ctx

Contents

- Type context manipulation

Description

This module defines type-level lists used for representing the type of variables in a context.

A `Ctx` is never intended to be manipulated at the value level; it is used purely as a type-level list, just like `'[]`. To see how it is used, see the module header for Data.Parameterized.Context.

Synopsis

- data Ctx k
  - = EmptyCtx
  - | (Ctx k) ::> k
- type EmptyCtx = 'EmptyCtx :: Ctx k
- type SingleCtx (x :: k) = (EmptyCtx :: Ctx k) ::> x
- type (::>) (c :: Ctx k) (a :: k) = c '::> a
- type family (x :: Ctx k) <+> (y :: Ctx k) :: Ctx k where ...
- type family CtxSize (a :: Ctx k) :: Nat where ...
- type CtxLookup (n :: Nat) (ctx :: Ctx k) = CtxLookupRight (FromLeft ctx n) ctx
- type CtxUpdate (n :: Nat) (x :: k) (ctx :: Ctx k) = CtxUpdateRight (FromLeft ctx n) x ctx
- type family CtxLookupRight (n :: Nat) (ctx :: Ctx k) :: k where ...
- type family CtxUpdateRight (n :: Nat) (x :: k) (ctx :: Ctx k) :: Ctx k where ...
- type family CtxFlatten (ctx :: Ctx (Ctx a)) :: Ctx a where ...
- type family CheckIx (ctx :: Ctx k) (n :: Nat) (b :: Bool) where ...
- type ValidIx (n :: Nat) (ctx :: Ctx k) = CheckIx ctx n ((n + 1) <=? CtxSize ctx)
- type FromLeft (ctx :: Ctx k) (n :: Natural) = (CtxSize ctx - 1) - n

# Documentation

data Ctx k Source #

Kind ``Ctx` k` comprises lists of types of kind `k`.

Constructors

EmptyCtx |
(Ctx k) ::> k |

#### Instances

Instances details

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

Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

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

foldrFC :: (forall (x :: k). f x -> b -> b) -> forall (x :: Ctx k). b -> Assignment f x -> b Source #

foldlFC :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: Ctx k). b -> Assignment f x -> b Source #

foldrFC' :: (forall (x :: k). f x -> b -> b) -> forall (x :: Ctx k). b -> Assignment f x -> b Source #

foldlFC' :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: Ctx k). b -> Assignment f x -> b Source #

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

FunctorFC (Assignment :: (k -> Type) -> Ctx k -> Type) Source # |
Instance details Defined in Data.Parameterized.Context.Unsafe Methods fmapFC :: (forall (x :: k). f x -> g x) -> forall (x :: Ctx k). Assignment f x -> Assignment g x Source #
OrdFC (Assignment :: (k -> Type) -> Ctx k -> Type) Source # |
Instance details Defined in Data.Parameterized.Context.Unsafe Methods compareFC :: (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y) -> forall (x :: Ctx k) (y :: Ctx k). 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 :: k) (y :: k). f x -> f y -> Maybe (x :~: y)) -> forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Maybe (x :~: y) Source #
TraversableFC (Assignment :: (k -> Type) -> Ctx k -> Type) Source # |
Instance details Defined in Data.Parameterized.Context.Unsafe Methods traverseFC :: forall f g m. Applicative m => (forall (x :: k). f x -> m (g x)) -> forall (x :: Ctx k). Assignment f x -> m (Assignment g x) Source #
FoldableFCWithIndex (Assignment :: (k -> Type) -> Ctx k -> Type) Source # |

Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

ifoldMapFC :: forall f m (z :: Ctx k). Monoid m => (forall (x :: k). IndexF (Assignment f z) x -> f x -> m) -> Assignment f z -> m Source #

ifoldrFC :: forall (z :: Ctx k) f b. (forall (x :: k). IndexF (Assignment f z) x -> f x -> b -> b) -> b -> Assignment f z -> b Source #

ifoldlFC :: forall f b (z :: Ctx k). (forall (x :: k). IndexF (Assignment f z) x -> b -> f x -> b) -> b -> Assignment f z -> b Source #

ifoldrFC' :: forall f b (z :: Ctx k). (forall (x :: k). IndexF (Assignment f z) x -> f x -> b -> b) -> b -> Assignment f z -> b Source #

ifoldlFC' :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: Ctx k). b -> Assignment f x -> b Source #

itoListFC :: forall f a (z :: Ctx k). (forall (x :: k). IndexF (Assignment f z) x -> f x -> a) -> Assignment f z -> [a] Source #

FunctorFCWithIndex (Assignment :: (k -> Type) -> Ctx k -> Type) Source # |
Instance details Defined in Data.Parameterized.Context.Unsafe Methods imapFC :: forall f g (z :: Ctx k). (forall (x :: k). IndexF (Assignment f z) x -> f x -> g x) -> Assignment f z -> Assignment g z Source #
TraversableFCWithIndex (Assignment :: (k -> Type) -> Ctx k -> Type) Source # |
Instance details Defined in Data.Parameterized.Context.Unsafe Methods itraverseFC :: forall m (z :: Ctx k) f g. Applicative m => (forall (x :: k). IndexF (Assignment f z) x -> f x -> m (g x)) -> Assignment f z -> m (Assignment g z) Source #
Category (Diff :: Ctx k -> Ctx k -> Type) Source # | Implemented with `noDiff` and `addDiff`
Instance details Defined in Data.Parameterized.Context.Unsafe Methods id :: forall (a :: Ctx k). Diff a a Source # (.) :: forall (b :: Ctx k) (c :: Ctx k) (a :: Ctx k). Diff b c -> Diff a b -> Diff a c Source #
ShowF (Size :: Ctx k -> Type) Source # |
Instance details Defined in Data.Parameterized.Context.Unsafe Methods withShow :: forall p q (tp :: Ctx k) a. p (Size :: Ctx k -> Type) -> q tp -> (Show (Size tp) => a) -> a Source # showF :: forall (tp :: Ctx k). Size tp -> String Source # showsPrecF :: forall (tp :: Ctx k). Int -> Size tp -> String -> String Source #
TestEquality f => TestEquality (Assignment f :: Ctx k -> Type) Source # |
Instance details Defined in Data.Parameterized.Context.Unsafe Methods testEquality :: forall (a :: Ctx k) (b :: Ctx k). Assignment f a -> Assignment f b -> Maybe (a :~: b) Source #
EqF f => EqF (Assignment f :: Ctx k -> Type) Source # |
Instance details Defined in Data.Parameterized.Context.Unsafe Methods eqF :: forall (a :: Ctx k). Assignment f a -> Assignment f a -> Bool Source #
(HashableF f, TestEquality f) => HashableF (Assignment f :: Ctx k -> Type) Source # |
Instance details Defined in Data.Parameterized.Context.Unsafe Methods hashWithSaltF :: forall (tp :: Ctx k). Int -> Assignment f tp -> Int Source # hashF :: forall (tp :: Ctx k). Assignment f tp -> Int Source #
OrdF f => OrdF (Assignment f :: Ctx k -> Type) Source # |

Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

compareF :: forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> OrderingF x y Source #

leqF :: forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Bool Source #

ltF :: forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Bool Source #

geqF :: forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Bool Source #

gtF :: forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Bool Source #

ShowF f => ShowF (Assignment f :: Ctx k -> Type) Source # |
Instance details Defined in Data.Parameterized.Context.Unsafe Methods withShow :: forall p q (tp :: Ctx k) a. p (Assignment f) -> q tp -> (Show (Assignment f tp) => a) -> a Source # showF :: forall (tp :: Ctx k). Assignment f tp -> String Source # showsPrecF :: forall (tp :: Ctx k). Int -> Assignment f tp -> String -> String Source #
IsRepr f => IsRepr (Assignment f :: Ctx k -> Type) Source # |
Instance details Defined in Data.Parameterized.WithRepr Methods withRepr :: forall (a :: Ctx k) r. 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 Methods knownRepr :: Assignment f (EmptyCtx :: Ctx k) Source #
(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 #

type EmptyCtx = 'EmptyCtx :: Ctx k Source #

type SingleCtx (x :: k) = (EmptyCtx :: Ctx k) ::> x Source #

type (::>) (c :: Ctx k) (a :: k) = c '::> a Source #

type family (x :: Ctx k) <+> (y :: Ctx k) :: Ctx k where ... Source #

Append two type-level contexts.

Equations

(x :: Ctx k) <+> (EmptyCtx :: Ctx k) = x |
(x :: Ctx k) <+> (y ::> e :: Ctx k) = (x <+> y) ::> e |

# Type context manipulation

type family CtxSize (a :: Ctx k) :: Nat where ... Source #

This type family computes the number of elements in a `Ctx`

Equations

CtxSize ('EmptyCtx :: Ctx k) = 0 |
CtxSize (xs '::> x :: Ctx k) = 1 + CtxSize xs |

type CtxLookup (n :: Nat) (ctx :: Ctx k) = CtxLookupRight (FromLeft ctx n) ctx Source #

Lookup the value in a context by number, from the left. Produce a type error if the index is out of range.

type CtxUpdate (n :: Nat) (x :: k) (ctx :: Ctx k) = CtxUpdateRight (FromLeft ctx n) x ctx Source #

Update the value in a context by number, from the left. If the index is out of range, the context is unchanged.

type family CtxLookupRight (n :: Nat) (ctx :: Ctx k) :: k where ... Source #

Lookup the value in a context by number, from the right

Equations

CtxLookupRight 0 (ctx '::> r :: Ctx k) = r |
CtxLookupRight n (ctx '::> r :: Ctx k) = CtxLookupRight (n - 1) ctx |

type family CtxUpdateRight (n :: Nat) (x :: k) (ctx :: Ctx k) :: Ctx k where ... Source #

Update the value in a context by number, from the right. If the index is out of range, the context is unchanged.

Equations

CtxUpdateRight n (x :: k) ('EmptyCtx :: Ctx k) = 'EmptyCtx :: Ctx k |
CtxUpdateRight 0 (x :: k) (ctx '::> old :: Ctx k) = ctx '::> x |
CtxUpdateRight n (x :: k) (ctx '::> y :: Ctx k) = CtxUpdateRight (n - 1) x ctx '::> y |

type family CtxFlatten (ctx :: Ctx (Ctx a)) :: Ctx a where ... Source #

Flatten a nested context

Equations

CtxFlatten (EmptyCtx :: Ctx (Ctx a)) = EmptyCtx :: Ctx a |
CtxFlatten (ctxs ::> ctx :: Ctx (Ctx k)) = CtxFlatten ctxs <+> ctx |

type family CheckIx (ctx :: Ctx k) (n :: Nat) (b :: Bool) where ... Source #

Helper type family used to generate descriptive error messages when an index is larger than the length of the `Ctx` being indexed.

Equations

CheckIx (ctx :: Ctx k) n 'True = () |
CheckIx (ctx :: Ctx k) n 'False = TypeError ((('Text "Index " ':<>: 'ShowType n) ':<>: 'Text " out of range in ") ':<>: 'ShowType ctx) :: Constraint |

type ValidIx (n :: Nat) (ctx :: Ctx k) = CheckIx ctx n ((n + 1) <=? CtxSize ctx) Source #

A constraint that checks that the nat `n` is a valid index into the context `ctx`, and raises a type error if not.

type FromLeft (ctx :: Ctx k) (n :: Natural) = (CtxSize ctx - 1) - n Source #

`Ctx` is a snoc-list. In order to use the more intuitive left-to-right ordering of elements the desired index is subtracted from the total number of elements.