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
type SingleCtx x = EmptyCtx ::> 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 CheckIx (ctx :: Ctx k) (n :: Nat) (b :: Bool) :: Constraint where ...
type ValidIx (n :: Nat) (ctx :: Ctx k) = CheckIx ctx n ((n + 1) <=? CtxSize ctx)
type FromLeft ctx n = (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

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 Methods knownRepr :: Assignment f EmptyCtx 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 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.