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

Data.Parameterized.Context.Safe

Contents

Size
Diff
Indexing
Assignments

Description

This module defines type contexts as a data-kind that consists of a list of types. Indexes are defined with respect to these contexts. In addition, finite dependent products (Assignments) are defined over type contexts. The elements of an assignment can be accessed using appropriately-typed indexes.

This module is intended to export exactly the same API as module Data.Parameterized.Context.Unsafe, so that they can be used interchangeably.

This implementation is entirely typesafe, and provides a proof that the signature implemented by this module is consistent. Contexts, indexes, and assignments are represented naively by linear sequences.

Compared to the implementation in Data.Parameterized.Context.Unsafe, this one suffers from the fact that the operation of extending an the context of an index is not a no-op. We therefore cannot use coerce to understand indexes in a new context without actually breaking things.

Synopsis

module Data.Parameterized.Ctx
data Size (ctx :: Ctx k)
sizeInt :: Size ctx -> Int
zeroSize :: Size EmptyCtx
incSize :: Size ctx -> Size (ctx ::> tp)
decSize :: Size (ctx ::> tp) -> Size ctx
extSize :: Size l -> Diff l r -> Size r
addSize :: Size x -> Size y -> Size (x <+> y)
data SizeView (ctx :: Ctx k) where
- ZeroSize :: SizeView EmptyCtx
- IncSize :: !(Size ctx) -> SizeView (ctx ::> tp)
viewSize :: Size ctx -> SizeView ctx
class KnownContext (ctx :: Ctx k) where
- knownSize :: Size ctx
data Diff (l :: Ctx k) (r :: Ctx k)
noDiff :: Diff l l
extendRight :: Diff l r -> Diff l (r ::> tp)
appendDiff :: Size r -> Diff l (l <+> r)
data DiffView a b where
- NoDiff :: DiffView a a
- ExtendRightDiff :: Diff a b -> DiffView a (b ::> r)
viewDiff :: Diff a b -> DiffView a b
class KnownDiff (l :: Ctx k) (r :: Ctx k) where
- knownDiff :: Diff l r
data IsAppend l r where
- IsAppend :: Size app -> IsAppend l (l <+> app)
diffIsAppend :: Diff l r -> IsAppend l r
data Index (ctx :: Ctx k) (tp :: k)
indexVal :: Index ctx tp -> Int
baseIndex :: Index (EmptyCtx ::> tp) tp
skipIndex :: Index ctx x -> Index (ctx ::> y) x
lastIndex :: Size (ctx ::> tp) -> Index (ctx ::> tp) tp
nextIndex :: Size ctx -> Index (ctx ::> tp) tp
extendIndex :: KnownDiff l r => Index l tp -> Index r tp
extendIndex' :: Diff l r -> Index l tp -> Index r tp
forIndex :: forall ctx r. Size ctx -> (forall tp. r -> Index ctx tp -> r) -> r -> r
forIndexRange :: Int -> Size ctx -> (forall tp. Index ctx tp -> r -> r) -> r -> r
intIndex :: Int -> Size ctx -> Maybe (Some (Index ctx))
data Assignment (f :: k -> Type) (ctx :: Ctx k)
size :: Assignment f ctx -> Size ctx
replicate :: Size ctx -> (forall tp. f tp) -> Assignment f ctx
generate :: forall ctx f. Size ctx -> (forall tp. Index ctx tp -> f tp) -> Assignment f ctx
generateM :: forall ctx m f. Applicative m => Size ctx -> (forall tp. Index ctx tp -> m (f tp)) -> m (Assignment f ctx)
empty :: Assignment f EmptyCtx
extend :: Assignment f ctx -> f tp -> Assignment f (ctx ::> tp)
adjust :: forall f ctx tp. (f tp -> f tp) -> Index ctx tp -> Assignment f ctx -> Assignment f ctx
update :: forall f ctx tp. Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx
adjustM :: forall m f ctx tp. Functor m => (f tp -> m (f tp)) -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)
data AssignView (f :: k -> Type) (ctx :: Ctx k) where
- AssignEmpty :: AssignView f EmptyCtx
- AssignExtend :: Assignment f ctx -> f tp -> AssignView f (ctx ::> tp)
viewAssign :: forall f ctx. Assignment f ctx -> AssignView f ctx
(!) :: Assignment f ctx -> Index ctx tp -> f tp
(!^) :: KnownDiff l r => Assignment f r -> Index l tp -> f tp
zipWith :: (forall x. f x -> g x -> h x) -> Assignment f a -> Assignment g a -> Assignment h a
zipWithM :: Applicative m => (forall tp. f tp -> g tp -> m (h tp)) -> Assignment f c -> Assignment g c -> m (Assignment h c)
(<++>) :: Assignment f x -> Assignment f y -> Assignment f (x <+> y)
traverseWithIndex :: Applicative m => (forall tp. Index ctx tp -> f tp -> m (g tp)) -> Assignment f ctx -> m (Assignment g ctx)

Documentation

module Data.Parameterized.Ctx

Size

data Size (ctx :: Ctx k) Source #

An indexed singleton type representing the size of a context.

sizeInt :: Size ctx -> Int Source #

Convert a context size to an Int.

zeroSize :: Size EmptyCtx Source #

The size of an empty context.

incSize :: Size ctx -> Size (ctx ::> tp) Source #

Increment the size to the next value.

decSize :: Size (ctx ::> tp) -> Size ctx Source #

extSize :: Size l -> Diff l r -> Size r Source #

Extend the size by a given difference.

addSize :: Size x -> Size y -> Size (x <+> y) Source #

The total size of two concatenated contexts.

data SizeView (ctx :: Ctx k) where Source #

Allows interpreting a size.

Constructors

ZeroSize :: SizeView EmptyCtx
IncSize :: !(Size ctx) -> SizeView (ctx ::> tp)

viewSize :: Size ctx -> SizeView ctx Source #

View a size as either zero or a smaller size plus one.

class KnownContext (ctx :: Ctx k) where Source #

A context that can be determined statically at compiler time.

Methods

knownSize :: Size ctx Source #

Instances

KnownContext (EmptyCtx :: Ctx k) Source #
Instance details Defined in Data.Parameterized.Context.Safe Methods knownSize :: Size EmptyCtx Source #
KnownContext ctx => KnownContext (ctx ::> tp :: Ctx k) Source #
Instance details Defined in Data.Parameterized.Context.Safe Methods knownSize :: Size (ctx ::> tp) Source #

Diff

data Diff (l :: Ctx k) (r :: Ctx k) Source #

Difference in number of elements between two contexts. The first context must be a sub-context of the other.

Instances

Category (Diff :: Ctx k -> Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Safe Methods id :: Diff a a # (.) :: Diff b c -> Diff a b -> Diff a c #

noDiff :: Diff l l Source #

The identity difference.

extendRight :: Diff l r -> Diff l (r ::> tp) Source #

Extend the difference to a sub-context of the right side.

appendDiff :: Size r -> Diff l (l <+> r) Source #

data DiffView a b where Source #

Constructors

NoDiff :: DiffView a a
ExtendRightDiff :: Diff a b -> DiffView a (b ::> r)

viewDiff :: Diff a b -> DiffView a b Source #

class KnownDiff (l :: Ctx k) (r :: Ctx k) where Source #

A difference that can be automatically inferred at compile time.

Methods

knownDiff :: Diff l r Source #

Instances

KnownDiff (l :: Ctx k) (l :: Ctx k) Source #
Instance details Defined in Data.Parameterized.Context.Safe Methods knownDiff :: Diff l l Source #
KnownDiff l r => KnownDiff (l :: Ctx k) (r ::> tp :: Ctx k) Source #
Instance details Defined in Data.Parameterized.Context.Safe Methods knownDiff :: Diff l (r ::> tp) Source #

data IsAppend l r where Source #

Proof that r = l + app for some app

Constructors

IsAppend :: Size app -> IsAppend l (l <+> app)

diffIsAppend :: Diff l r -> IsAppend l r Source #

If l is a sub-context of r then extract out their "contextual difference", i.e., the app such that r = l + app

Indexing

data Index (ctx :: Ctx k) (tp :: k) Source #

An index is a reference to a position with a particular type in a context.

Instances

TestEquality (Index ctx :: k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Safe Methods testEquality :: Index ctx a -> Index ctx b -> Maybe (a :~: b) #
HashableF (Index ctx :: k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Safe Methods hashWithSaltF :: Int -> Index ctx tp -> Int Source # hashF :: Index ctx tp -> Int Source #
ShowF (Index ctx :: k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Safe Methods withShow :: p (Index ctx) -> q tp -> (Show (Index ctx tp) -> a) -> a Source # showF :: Index ctx tp -> String Source # showsPrecF :: Int -> Index ctx tp -> String -> String Source #
OrdF (Index ctx :: k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Safe Methods compareF :: Index ctx x -> Index ctx y -> OrderingF x y Source # leqF :: Index ctx x -> Index ctx y -> Bool Source # ltF :: Index ctx x -> Index ctx y -> Bool Source # geqF :: Index ctx x -> Index ctx y -> Bool Source # gtF :: Index ctx x -> Index ctx y -> Bool Source #
Eq (Index ctx tp) Source #
Instance details Defined in Data.Parameterized.Context.Safe Methods (==) :: Index ctx tp -> Index ctx tp -> Bool # (/=) :: Index ctx tp -> Index ctx tp -> Bool #
Ord (Index ctx tp) Source #
Instance details Defined in Data.Parameterized.Context.Safe Methods compare :: Index ctx tp -> Index ctx tp -> Ordering # (<) :: Index ctx tp -> Index ctx tp -> Bool # (<=) :: Index ctx tp -> Index ctx tp -> Bool # (>) :: Index ctx tp -> Index ctx tp -> Bool # (>=) :: Index ctx tp -> Index ctx tp -> Bool # max :: Index ctx tp -> Index ctx tp -> Index ctx tp # min :: Index ctx tp -> Index ctx tp -> Index ctx tp #
Show (Index ctx tp) Source #
Instance details Defined in Data.Parameterized.Context.Safe Methods showsPrec :: Int -> Index ctx tp -> ShowS # show :: Index ctx tp -> String # showList :: [Index ctx tp] -> ShowS #
Hashable (Index ctx tp) Source #
Instance details Defined in Data.Parameterized.Context.Safe Methods hashWithSalt :: Int -> Index ctx tp -> Int # hash :: Index ctx tp -> Int #

indexVal :: Index ctx tp -> Int Source #

Convert an index to an Int, where the index of the left-most type in the context is 0.

baseIndex :: Index (EmptyCtx ::> tp) tp Source #

Index for first element in context.

skipIndex :: Index ctx x -> Index (ctx ::> y) x Source #

Increase context while staying at same index.

lastIndex :: Size (ctx ::> tp) -> Index (ctx ::> tp) tp Source #

Return the last index of a element.

nextIndex :: Size ctx -> Index (ctx ::> tp) tp Source #

Return the index of an element one past the size.

extendIndex :: KnownDiff l r => Index l tp -> Index r tp Source #

extendIndex' :: Diff l r -> Index l tp -> Index r tp Source #

forIndex :: forall ctx r. Size ctx -> (forall tp. r -> Index ctx tp -> r) -> r -> r Source #

Given a size n, an initial value v0, and a function f, the expression forIndex n v0 f calls f on each index less than n starting from 0 and v0, with the value v obtained from the last call.

forIndexRange :: Int -> Size ctx -> (forall tp. Index ctx tp -> r -> r) -> r -> r Source #

Given an index i, size n, a function f, value v, and a function f, the expression forIndexRange i n f v is equivalent to v when i >= sizeInt n, and f i (forIndexRange (i+1) n v) otherwise.

intIndex :: Int -> Size ctx -> Maybe (Some (Index ctx)) Source #

Return index at given integer or nothing if integer is out of bounds.

Assignments

data Assignment (f :: k -> Type) (ctx :: Ctx k) Source #

An assignment is a sequence that maps each index with type tp to a value of type 'f tp'.

Instances

TraversableFC (Assignment :: (k -> Type) -> Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Safe 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.Safe 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.Safe 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.Safe 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.Safe Methods fmapFC :: (forall (x :: k0). f x -> g x) -> forall (x :: l). Assignment f x -> Assignment g x Source #
IxedF' k (Assignment f ctx) Source #
Instance details Defined in Data.Parameterized.Context.Safe Methods ixF' :: IndexF (Assignment f ctx) x -> Lens' (Assignment f ctx) (IxValueF (Assignment f ctx) x) Source #
IxedF k (Assignment f ctx) Source #
Instance details Defined in Data.Parameterized.Context.Safe Methods ixF :: IndexF (Assignment f ctx) x -> Traversal' (Assignment f ctx) (IxValueF (Assignment f ctx) x) Source #
TestEquality f => TestEquality (Assignment f :: Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Safe 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.Safe 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.Safe 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.Safe Methods compareF :: Assignment f x -> Assignment f y -> OrderingF x y Source # leqF :: Assignment f x -> Assignment f y -> Bool Source # ltF :: Assignment f x -> Assignment f y -> Bool Source # geqF :: Assignment f x -> Assignment f y -> Bool Source # gtF :: Assignment f x -> Assignment f y -> Bool Source #
KnownRepr (Assignment f :: Ctx k -> Type) (EmptyCtx :: Ctx k) Source #
Instance details Defined in Data.Parameterized.Context.Safe 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.Safe Methods knownRepr :: Assignment f (ctx ::> bt) Source #
TestEquality f => Eq (Assignment f ctx) Source #
Instance details Defined in Data.Parameterized.Context.Safe Methods (==) :: Assignment f ctx -> Assignment f ctx -> Bool # (/=) :: Assignment f ctx -> Assignment f ctx -> Bool #
OrdF f => Ord (Assignment f ctx) Source #
Instance details Defined in Data.Parameterized.Context.Safe Methods compare :: Assignment f ctx -> Assignment f ctx -> Ordering # (<) :: Assignment f ctx -> Assignment f ctx -> Bool # (<=) :: Assignment f ctx -> Assignment f ctx -> Bool # (>) :: Assignment f ctx -> Assignment f ctx -> Bool # (>=) :: Assignment f ctx -> Assignment f ctx -> Bool # max :: Assignment f ctx -> Assignment f ctx -> Assignment f ctx # min :: Assignment f ctx -> Assignment f ctx -> Assignment f ctx #
ShowF f => Show (Assignment f ctx) Source #
Instance details Defined in Data.Parameterized.Context.Safe Methods showsPrec :: Int -> Assignment f ctx -> ShowS # show :: Assignment f ctx -> String # showList :: [Assignment f ctx] -> ShowS #
NFData (Assignment f ctx) Source #
Instance details Defined in Data.Parameterized.Context.Safe Methods rnf :: Assignment f ctx -> () #
HashableF f => Hashable (Assignment f ctx) Source #
Instance details Defined in Data.Parameterized.Context.Safe Methods hashWithSalt :: Int -> Assignment f ctx -> Int # hash :: Assignment f ctx -> Int #
TestEquality f => PolyEq (Assignment f x) (Assignment f y) Source #
Instance details Defined in Data.Parameterized.Context.Safe Methods polyEqF :: Assignment f x -> Assignment f y -> Maybe (Assignment f x :~: Assignment f y) Source # polyEq :: Assignment f x -> Assignment f y -> Bool Source #
type IxValueF (Assignment f ctx) Source #
Instance details Defined in Data.Parameterized.Context.Safe type IxValueF (Assignment f ctx) = f
type IndexF (Assignment f ctx) Source #
Instance details Defined in Data.Parameterized.Context.Safe type IndexF (Assignment f ctx) = Index ctx

size :: Assignment f ctx -> Size ctx Source #

Return number of elements in assignment.

replicate :: Size ctx -> (forall tp. f tp) -> Assignment f ctx Source #

replicate n make a context with different copies of the same polymorphic value.

generate :: forall ctx f. Size ctx -> (forall tp. Index ctx tp -> f tp) -> Assignment f ctx Source #

Generate an assignment

generateM :: forall ctx m f. Applicative m => Size ctx -> (forall tp. Index ctx tp -> m (f tp)) -> m (Assignment f ctx) Source #

Generate an assignment

empty :: Assignment f EmptyCtx Source #

Create empty indexed vector.

extend :: Assignment f ctx -> f tp -> Assignment f (ctx ::> tp) Source #

adjust :: forall f ctx tp. (f tp -> f tp) -> Index ctx tp -> Assignment f ctx -> Assignment f ctx Source #

Deprecated: Replace 'adjust f i asgn' with 'Lens.over (ixF i) f asgn' instead.

update :: forall f ctx tp. Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx Source #

Deprecated: Replace 'update idx val asgn' with 'Lens.set (ixF idx) val asgn' instead.

adjustM :: forall m f ctx tp. Functor m => (f tp -> m (f tp)) -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx) Source #

data AssignView (f :: k -> Type) (ctx :: Ctx k) where Source #

View an assignment as either empty or an assignment with one appended.

Constructors

AssignEmpty :: AssignView f EmptyCtx
AssignExtend :: Assignment f ctx -> f tp -> AssignView f (ctx ::> tp)

viewAssign :: forall f ctx. Assignment f ctx -> AssignView f ctx Source #

(!) :: Assignment f ctx -> Index ctx tp -> f tp Source #

Return value of assignment.

(!^) :: KnownDiff l r => Assignment f r -> Index l tp -> f tp Source #

Return value of assignment, where the index is into an initial sequence of the assignment.

zipWith :: (forall x. f x -> g x -> h x) -> Assignment f a -> Assignment g a -> Assignment h a Source #

zipWithM :: Applicative m => (forall tp. f tp -> g tp -> m (h tp)) -> Assignment f c -> Assignment g c -> m (Assignment h c) Source #

(<++>) :: Assignment f x -> Assignment f y -> Assignment f (x <+> y) Source #

traverseWithIndex :: Applicative m => (forall tp. Index ctx tp -> f tp -> m (g tp)) -> Assignment f ctx -> m (Assignment g ctx) Source #