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

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

Data.Parameterized.Context.Safe

Contents

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

Documentation

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

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

KnownRepr (Assignment f :: Ctx k -> Type) (EmptyCtx :: Ctx k) Source # 
Instance details

Defined in Data.Parameterized.Context.Safe

(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

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 #