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

Copyright(c) Galois Inc 2015-2019
MaintainerJoe Hendrix <jhendrix@galois.com>
Safe HaskellSafe
LanguageHaskell98

Data.Parameterized.Ctx

Contents

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
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 #

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 #

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 #

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 #

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.