parameterized-utils-2.1.2.0: Classes and data structures for working with data-kind indexed types
Copyright(c) Galois Inc 2015-2019
MaintainerJoe Hendrix <jhendrix@galois.com>
Safe HaskellSafe
LanguageHaskell2010

Data.Parameterized.Ctx

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

Documentation

data Ctx k Source #

Kind Ctx k comprises lists of types of kind k.

Constructors

EmptyCtx 
(Ctx k) ::> k 

Instances

Instances details
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 :: 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 :: forall f m. 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 f b. (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 f b. (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 #

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 :: k0). Diff a a #

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

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

Defined in Data.Parameterized.Context.Unsafe

Methods

withShow :: forall p q (tp :: k0) a. p Size -> q tp -> (Show (Size tp) => a) -> a Source #

showF :: forall (tp :: k0). Size tp -> String Source #

showsPrecF :: forall (tp :: k0). 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 :: k0) (b :: k0). 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 :: forall (tp :: k0). Int -> Assignment f tp -> Int Source #

hashF :: forall (tp :: k0). Assignment f tp -> Int Source #

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

Defined in Data.Parameterized.Context.Unsafe

Methods

withShow :: forall p q (tp :: k0) a. p (Assignment f) -> q tp -> (Show (Assignment f tp) => a) -> a Source #

showF :: forall (tp :: k0). Assignment f tp -> String Source #

showsPrecF :: forall (tp :: k0). Int -> Assignment f tp -> String -> String Source #

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

Defined in Data.Parameterized.Context.Unsafe

Methods

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

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

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

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

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

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

Defined in Data.Parameterized.WithRepr

Methods

withRepr :: forall (a :: k0) 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

(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 (::>) (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.