Safe Haskell | Safe-Inferred |
---|---|

Language | Haskell2010 |

Very strong types for working with indices, counts, etc within sequences.

## Synopsis

- newtype Count (base ∷ Type) (elem ∷ kelem) (which ∷ kwhich) = Count Int
- forgetBase ∷ Count base elem which → Forgotten (Count () elem which)
- forgetElem ∷ Count base elem which → Forgotten (Count base () which)
- getCount ∷ Count base elem which → Int
- (+) ∷ Count base elem which → Int → Count base elem which
- (-) ∷ Count base elem which → Int → Count base elem which
- type Index base elem = Count base elem Preds
- data Preds
- type Size base elem = Count base elem Total
- data Total
- forRange_ ∷ Applicative f ⇒ Size base elem → (Index base elem → f a) → f ()
- lastIndex ∷ Size base elem → Index base elem
- range ∷ Size base elem → [Index base elem]
- uniformIndex ∷ StatefulGen g m ⇒ Size base elem → g → m (Index base elem)
- data Contains (elem ∷ kelem) (outer ∷ Type) (inner ∷ Type) where
- data Lbl lbl = Lbl
- data SomeWindow (lbl ∷ klbl) (outer ∷ Type) (elem ∷ kelem) = ∀ (skolem ∷ Type). SomeWindow !(Proxy skolem) !(Contains elem outer (Win lbl skolem))
- data Win (lbl ∷ klbl) (skolem ∷ Type)
- forgetWindow ∷ Contains elem outer inner → Forgotten (Index outer elem, Index outer elem)
- fromWindow ∷ Contains elem outer inner → Index inner elem → Index outer elem
- fromWindowVar ∷ Contains elem outer inner → Var inner x → Var outer x
- joinWin ∷ Contains elem outer mid → Contains elem mid inner → Contains elem outer inner
- toWindow ∷ Contains elem outer inner → Index outer elem → Maybe (Index inner elem)
- toWindowVar ∷ Contains elem outer inner → Var outer x → Var inner x
- truncateWin ∷ Contains elem outer inner → Size inner elem → Contains elem outer inner
- windowLast ∷ Contains elem outer inner → Index outer elem
- windowSize ∷ Contains elem outer inner → Size inner elem
- windowStart ∷ Contains elem outer inner → Index outer elem
- withSuffixWindow ∷ Size outer elem → Lbl lbl → Index outer elem → SomeWindow lbl outer elem
- withTopWindow ∷ Lbl lbl → Int → (∀ base. Proxy base → SomeWindow lbl base elem → ans) → ans
- withWindow ∷ Size outer elem → Lbl lbl → Index outer elem → Size x elem → SomeWindow lbl outer elem
- withWindowBetween ∷ Size outer elem → Lbl lbl → Index outer elem → Index outer elem → SomeWindow lbl outer elem
- newtype MVector base elem s a = MVector (MVector s a)
- newtype Vector base elem a = Vector (Vector a)
- createV ∷ Unbox a ⇒ (∀ s. ST s (MVector base elem s a)) → Vector base elem a
- getMVector ∷ MVector base elem s a → MVector s a
- getVector ∷ Vector base elem a → Vector a
- lengthMV ∷ Unbox a ⇒ MVector base elem s a → Size base elem
- lengthV ∷ Unbox a ⇒ Vector base elem a → Size base elem
- modifyMV ∷ Unbox a ⇒ MVector base elem s a → (a → a) → Index base elem → ST s ()
- readMV ∷ Unbox a ⇒ MVector base elem s a → Index base elem → ST s a
- readV ∷ Unbox a ⇒ Vector base elem a → Index base elem → a
- replicateMV ∷ Unbox a ⇒ Size base elem → ST s a → ST s (MVector base elem s a)
- sliceMV ∷ Unbox a ⇒ Contains elem outer inner → MVector outer elem s a → MVector inner elem s a
- sliceV ∷ Unbox a ⇒ Contains elem outer inner → Vector outer elem a → Vector inner elem a
- unsafeThawV ∷ Unbox a ⇒ Vector base elem a → ST s (MVector base elem s a)
- writeMV ∷ Unbox a ⇒ MVector base elem s a → Index base elem → a → ST s ()
- data Other
- type Var base elem = Count base elem Other
- joinVar ∷ MVector base elem s a → Var a x → Var base x
- toIndex ∷ Var base elem → Index base elem
- toSize ∷ Var base elem → Size base elem
- toVar ∷ Count base elem which → Var base elem

# general counts

newtype Count (base ∷ Type) (elem ∷ kelem) (which ∷ kwhich) Source #

A type-indexed Int to represent counts of elements in containers

`base`

is the type-level name of the container in which we are counting (e.g.`Win (Lbl HonestLbl) skolem1`

)`elem`

is the type-level name of the elements in the container (e.g.`SlotE`

)`which`

is the type-level name of some property that identifies the particular elements that we are counting (e.g.`Pred`

,`Total`

, or`Other`

)

TODO: rename `base`

to `container`

#### Instances

Arbitrary (Count base elem which) Source # | |

which ~~ Other ⇒ Enum (Count base elem which) Source # | |

Defined in Test.Ouroboros.Consensus.ChainGenerator.Counting succ ∷ Count base elem which → Count base elem which # pred ∷ Count base elem which → Count base elem which # toEnum ∷ Int → Count base elem which # fromEnum ∷ Count base elem which → Int # enumFrom ∷ Count base elem which → [Count base elem which] # enumFromThen ∷ Count base elem which → Count base elem which → [Count base elem which] # enumFromTo ∷ Count base elem which → Count base elem which → [Count base elem which] # enumFromThenTo ∷ Count base elem which → Count base elem which → Count base elem which → [Count base elem which] # | |

which ~~ Other ⇒ Num (Count base elem which) Source # | |

Defined in Test.Ouroboros.Consensus.ChainGenerator.Counting (+) ∷ Count base elem which → Count base elem which → Count base elem which # (-) ∷ Count base elem which → Count base elem which → Count base elem which # (*) ∷ Count base elem which → Count base elem which → Count base elem which # negate ∷ Count base elem which → Count base elem which # abs ∷ Count base elem which → Count base elem which # signum ∷ Count base elem which → Count base elem which # fromInteger ∷ Integer → Count base elem which # | |

Read (Count base elem which) Source # | |

Show (Count base elem which) Source # | |

Eq (Count base elem which) Source # | |

Ord (Count base elem which) Source # | |

Defined in Test.Ouroboros.Consensus.ChainGenerator.Counting compare ∷ Count base elem which → Count base elem which → Ordering # (<) ∷ Count base elem which → Count base elem which → Bool # (<=) ∷ Count base elem which → Count base elem which → Bool # (>) ∷ Count base elem which → Count base elem which → Bool # (>=) ∷ Count base elem which → Count base elem which → Bool # max ∷ Count base elem which → Count base elem which → Count base elem which # min ∷ Count base elem which → Count base elem which → Count base elem which # |

# indices and sizes

uniformIndex ∷ StatefulGen g m ⇒ Size base elem → g → m (Index base elem) Source #

# windows

data Contains (elem ∷ kelem) (outer ∷ Type) (inner ∷ Type) Source #

Values of this type describe a window in a sequence of elements.

A window is an infix of the sequence, and it is described with an offset and a length or size (the number of elements in the window).

`elem`

is a type-level name of the elements in the containing sequence (e.g.`SlotE`

)`outer`

is a type-level name identifying the containing sequence (e.g.`Win (Lbl HonestLbl) skolem1`

)`inner`

is a type-level name for the window that the value describes (e.g.`Win (Lbl ScgLbl) skolem2`

)

Note that nothing is said about the containing sequence other than its type name.

TODO: rename Contains to Window

A human-readable label for a `Win`

data SomeWindow (lbl ∷ klbl) (outer ∷ Type) (elem ∷ kelem) Source #

∀ (skolem ∷ Type). SomeWindow !(Proxy skolem) !(Contains elem outer (Win lbl skolem)) |

#### Instances

Read (SomeWindow lbl outer elem) Source # | |

Defined in Test.Ouroboros.Consensus.ChainGenerator.Counting readsPrec ∷ Int → ReadS (SomeWindow lbl outer elem) # readList ∷ ReadS [SomeWindow lbl outer elem] # readPrec ∷ ReadPrec (SomeWindow lbl outer elem) # readListPrec ∷ ReadPrec [SomeWindow lbl outer elem] # | |

Show (SomeWindow lbl outer elem) Source # | |

Defined in Test.Ouroboros.Consensus.ChainGenerator.Counting showsPrec ∷ Int → SomeWindow lbl outer elem → ShowS # show ∷ SomeWindow lbl outer elem → String # showList ∷ [SomeWindow lbl outer elem] → ShowS # | |

Eq (SomeWindow lbl outer elem) Source # | |

Defined in Test.Ouroboros.Consensus.ChainGenerator.Counting (==) ∷ SomeWindow lbl outer elem → SomeWindow lbl outer elem → Bool # (/=) ∷ SomeWindow lbl outer elem → SomeWindow lbl outer elem → Bool # |

data Win (lbl ∷ klbl) (skolem ∷ Type) Source #

A type-level name for a window within some containing sequence

`lbl`

is a name component that can be used in multiple names`skolem`

is a component to differentiate between names which use the same`lbl`

TODO: rename Win to WinLabel

fromWindow ∷ Contains elem outer inner → Index inner elem → Index outer elem Source #

Converts an index of a window into an index in the containing sequence.

fromWindowVar ∷ Contains elem outer inner → Var inner x → Var outer x Source #

Converts a count of elements in a window to a count of elements in the containing sequence.

joinWin ∷ Contains elem outer mid → Contains elem mid inner → Contains elem outer inner Source #

`Contains`

is a `Semigroupoid`

windowLast ∷ Contains elem outer inner → Index outer elem Source #

windowSize ∷ Contains elem outer inner → Size inner elem Source #

windowStart ∷ Contains elem outer inner → Index outer elem Source #

withSuffixWindow ∷ Size outer elem → Lbl lbl → Index outer elem → SomeWindow lbl outer elem Source #

`withSuffixWindow outerSz lbl i`

is the window between indices `i`

and the
end of the containing sequence of length `outerSz`

with name `lbl`

.

withTopWindow ∷ Lbl lbl → Int → (∀ base. Proxy base → SomeWindow lbl base elem → ans) → ans Source #

`withTopWindow lbl sz k`

passes to `k`

a window of size `sz`

with name
`lbl`

at offset `0`

of some containing sequence with a unique name `base`

.

withWindow ∷ Size outer elem → Lbl lbl → Index outer elem → Size x elem → SomeWindow lbl outer elem Source #

`withWindow outerSz lbl offset innerSz`

is a window of length `innerSz`

with name `lbl`

starting at `offset`

in a sequence with length `outerSz`

.

If the window doesn't fit in the containing sequence, it is clipped so the resulting (possibly empty) window is contained.

Note that the window can spill either on the right if `i + innerSz > outerSz`

,
or it can spill on the left if `i < 0`

, or it can spill on both sides
simultaneously.

withWindowBetween ∷ Size outer elem → Lbl lbl → Index outer elem → Index outer elem → SomeWindow lbl outer elem Source #

`withWindowBetween outerSz lbl i j`

is the window between indices `i`

and `j`

with name `lbl`

in a containing sequence of length `outerSz`

.

# vectors

newtype MVector base elem s a Source #

A type-indexed vector carrying values of a container

`base`

is a type-level name identifying the container (e.g.`Win (Lbl HonestLbl) skolem1`

)`elem`

is a type-level name of the elements in the container (e.g.`SlotE`

)

getMVector ∷ MVector base elem s a → MVector s a Source #

sliceMV ∷ Unbox a ⇒ Contains elem outer inner → MVector outer elem s a → MVector inner elem s a Source #