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

Data.Parameterized.Ctx

Contents

Type context manipulation

Description

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

Synopsis

Documentation

data Ctx k Source #

Kind Ctx k comprises lists of types of kind k.

Constructors

EmptyCtx
(Ctx k) ::> k

Instances

TraversableFC k (Ctx k) (Assignment k) Source #
Methods traverseFC :: Applicative m => (forall (s :: Assignment k). e s -> m (f s)) -> t e c -> m (t f c) Source #
TraversableFC k (Ctx k) (Assignment k) Source #
Methods traverseFC :: Applicative m => (forall (s :: Assignment k). e s -> m (f s)) -> t e c -> m (t f c) Source #
FoldableFC k (Ctx k) (Assignment k) Source #
Methods foldMapFC :: Monoid m => (forall (s :: Assignment k). e s -> m) -> t e c -> m Source # foldrFC :: (forall (s :: Assignment k). e s -> b -> b) -> b -> t e c -> b Source # foldlFC :: (forall (s :: Assignment k). b -> e s -> b) -> b -> t e c -> b Source # foldrFC' :: (forall (s :: Assignment k). e s -> b -> b) -> b -> t e c -> b Source # foldlFC' :: (forall (s :: Assignment k). b -> e s -> b) -> b -> t e c -> b Source # toListFC :: (forall (tp :: Assignment k). f tp -> a) -> t f c -> [a] Source #
FoldableFC k (Ctx k) (Assignment k) Source #
Methods foldMapFC :: Monoid m => (forall (s :: Assignment k). e s -> m) -> t e c -> m Source # foldrFC :: (forall (s :: Assignment k). e s -> b -> b) -> b -> t e c -> b Source # foldlFC :: (forall (s :: Assignment k). b -> e s -> b) -> b -> t e c -> b Source # foldrFC' :: (forall (s :: Assignment k). e s -> b -> b) -> b -> t e c -> b Source # foldlFC' :: (forall (s :: Assignment k). b -> e s -> b) -> b -> t e c -> b Source # toListFC :: (forall (tp :: Assignment k). f tp -> a) -> t f c -> [a] Source #
OrdFC k (Ctx k) (Assignment k) Source #
Methods compareFC :: (forall (x :: Assignment k) (y :: Assignment k). f x -> f y -> OrderingF (Assignment k) x y) -> forall (x :: l) (y :: l). t f x -> t f y -> OrderingF l x y Source #
OrdFC k (Ctx k) (Assignment k) Source #
Methods compareFC :: (forall (x :: Assignment k) (y :: Assignment k). f x -> f y -> OrderingF (Assignment k) x y) -> forall (x :: l) (y :: l). t f x -> t f y -> OrderingF l x y Source #
TestEqualityFC k (Ctx k) (Assignment k) Source #
Methods testEqualityFC :: (forall (x :: Assignment k) (y :: Assignment k). f x -> f y -> Maybe ((Assignment k :~: x) y)) -> forall (x :: l) (y :: l). t f x -> t f y -> Maybe ((l :~: x) y) Source #
TestEqualityFC k (Ctx k) (Assignment k) Source #
Methods testEqualityFC :: (forall (x :: Assignment k) (y :: Assignment k). f x -> f y -> Maybe ((Assignment k :~: x) y)) -> forall (x :: l) (y :: l). t f x -> t f y -> Maybe ((l :~: x) y) Source #
FunctorFC k (Ctx k) (Assignment k) Source #
Methods fmapFC :: (forall (x :: Assignment k). f x -> g x) -> forall (x :: k). m f x -> m g x Source #
FunctorFC k (Ctx k) (Assignment k) Source #
Methods fmapFC :: (forall (x :: Assignment k). f x -> g x) -> forall (x :: k). m f x -> m g x Source #
Category (Ctx k) (Diff k) #
Methods id :: cat a a # (.) :: cat b c -> cat a b -> cat a c #
Category (Ctx k) (Diff k) #
Methods id :: cat a a # (.) :: cat b c -> cat a b -> cat a c #
TestEquality k f => TestEquality (Ctx k) (Assignment k f) #
Methods testEquality :: f a -> f b -> Maybe ((Assignment k f :~: a) b) #
TestEquality k f => TestEquality (Ctx k) (Assignment k f) #
Methods testEquality :: f a -> f b -> Maybe ((Assignment k f :~: a) b) #
HashableF k f => HashableF (Ctx k) (Assignment k f) Source #
Methods hashWithSaltF :: Int -> f tp -> Int Source # hashF :: f tp -> Int Source #
HashableF k f => HashableF (Ctx k) (Assignment k f) Source #
Methods hashWithSaltF :: Int -> f tp -> Int Source # hashF :: f tp -> Int Source #
ShowF k f => ShowF (Ctx k) (Assignment k f) Source #
Methods withShow :: p f -> q tp -> (Show (f tp) -> a) -> a Source # showF :: f tp -> String Source # showsF :: f tp -> String -> String Source #
ShowF k f => ShowF (Ctx k) (Assignment k f) Source #
Methods withShow :: p f -> q tp -> (Show (f tp) -> a) -> a Source # showF :: f tp -> String Source # showsF :: f tp -> String -> String Source #
OrdF k f => OrdF (Ctx k) (Assignment k f) Source #
Methods compareF :: ktp x -> ktp y -> OrderingF (Assignment k f) x y Source # leqF :: ktp x -> ktp y -> Bool Source # ltF :: ktp x -> ktp y -> Bool Source # geqF :: ktp x -> ktp y -> Bool Source # gtF :: ktp x -> ktp y -> Bool Source #
OrdF k f => OrdF (Ctx k) (Assignment k f) Source #
Methods compareF :: ktp x -> ktp y -> OrderingF (Assignment k f) x y Source # leqF :: ktp x -> ktp y -> Bool Source # ltF :: ktp x -> ktp y -> Bool Source # geqF :: ktp x -> ktp y -> Bool Source # gtF :: ktp x -> ktp y -> Bool Source #
KnownRepr (Ctx k) (Assignment k f) (EmptyCtx k) Source #
Methods knownRepr :: EmptyCtx k ctx Source #
KnownRepr (Ctx k) (Assignment k f) (EmptyCtx k) Source #
Methods knownRepr :: EmptyCtx k ctx Source #
(KnownRepr (Ctx k) (Assignment k f) ctx, KnownRepr k f bt) => KnownRepr (Ctx k) (Assignment k f) ((::>) k ctx bt) Source #
Methods knownRepr :: (k ::> ctx) bt ctx Source #
(KnownRepr (Ctx k) (Assignment k f) ctx, KnownRepr k f bt) => KnownRepr (Ctx k) (Assignment k f) ((::>) k ctx bt) Source #
Methods knownRepr :: (k ::> ctx) bt ctx Source #

type EmptyCtx = EmptyCtx Source #

type SingleCtx x = EmptyCtx ::> 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 <+> EmptyCtx = x
x <+> (y ::> e) = (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 = 0
CtxSize (xs ::> x) = 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) = r
CtxLookupRight n (ctx ::> r) = 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 EmptyCtx = EmptyCtx
CtxUpdateRight 0 x (ctx ::> old) = ctx ::> x
CtxUpdateRight n x (ctx ::> y) = CtxUpdateRight (n - 1) x ctx ::> y

type family CheckIx (ctx :: Ctx k) (n :: Nat) (b :: Bool) :: Constraint 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 n True = ()
CheckIx ctx n False = TypeError (((Text "Index " :<>: ShowType n) :<>: Text " out of range in ") :<>: ShowType ctx)

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 n = (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.