cryptol-3.0.0: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2021 Galois Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | Safe-Inferred
Language | Haskell2010

Cryptol.Backend.SeqMap

Contents

- Sequence Maps

Description

Synopsis

- data SeqMap sym a
- indexSeqMap :: (Integer -> SEval sym a) -> SeqMap sym a
- lookupSeqMap :: Backend sym => SeqMap sym a -> Integer -> SEval sym a
- finiteSeqMap :: Backend sym => sym -> [SEval sym a] -> SeqMap sym a
- infiniteSeqMap :: Backend sym => sym -> [SEval sym a] -> SEval sym (SeqMap sym a)
- enumerateSeqMap :: (Backend sym, Integral n) => n -> SeqMap sym a -> [SEval sym a]
- streamSeqMap :: Backend sym => SeqMap sym a -> [SEval sym a]
- reverseSeqMap :: Backend sym => Integer -> SeqMap sym a -> SeqMap sym a
- updateSeqMap :: SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
- dropSeqMap :: Backend sym => Integer -> SeqMap sym a -> SeqMap sym a
- concatSeqMap :: Backend sym => Integer -> SeqMap sym a -> SeqMap sym a -> SeqMap sym a
- splitSeqMap :: Backend sym => Integer -> SeqMap sym a -> (SeqMap sym a, SeqMap sym a)
- memoMap :: Backend sym => sym -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a)
- delaySeqMap :: Backend sym => sym -> SEval sym (SeqMap sym a) -> SEval sym (SeqMap sym a)
- zipSeqMap :: Backend sym => sym -> (a -> a -> SEval sym a) -> Nat' -> SeqMap sym a -> SeqMap sym a -> SEval sym (SeqMap sym a)
- mapSeqMap :: Backend sym => sym -> (a -> SEval sym a) -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a)
- mergeSeqMap :: Backend sym => sym -> (SBit sym -> a -> a -> SEval sym a) -> SBit sym -> SeqMap sym a -> SeqMap sym a -> SeqMap sym a
- barrelShifter :: Backend sym => sym -> (SBit sym -> a -> a -> SEval sym a) -> (SeqMap sym a -> Integer -> SEval sym (SeqMap sym a)) -> Nat' -> SeqMap sym a -> Integer -> [IndexSegment sym] -> SEval sym (SeqMap sym a)
- shiftSeqByInteger :: Backend sym => sym -> (SBit sym -> a -> a -> SEval sym a) -> (Integer -> Integer -> Maybe Integer) -> SEval sym a -> Nat' -> SeqMap sym a -> SInteger sym -> SEval sym (SeqMap sym a)
- data IndexSegment sym
  - = BitIndexSegment (SBit sym)
  - | WordIndexSegment (SWord sym)

# Sequence Maps

data SeqMap sym a Source #

A sequence map represents a mapping from nonnegative integer indices to values. These are used to represent both finite and infinite sequences.

#### Instances

Instances details

Backend sym => Functor (SeqMap sym) Source # |
Instance details Defined in Cryptol.Backend.SeqMap Methods fmap :: (a -> b) -> SeqMap sym a -> SeqMap sym b Source # (<$) :: a -> SeqMap sym b -> SeqMap sym a Source #

indexSeqMap :: (Integer -> SEval sym a) -> SeqMap sym a Source #

lookupSeqMap :: Backend sym => SeqMap sym a -> Integer -> SEval sym a Source #

finiteSeqMap :: Backend sym => sym -> [SEval sym a] -> SeqMap sym a Source #

Generate a finite sequence map from a list of values

infiniteSeqMap :: Backend sym => sym -> [SEval sym a] -> SEval sym (SeqMap sym a) Source #

Generate an infinite sequence map from a stream of values

enumerateSeqMap :: (Backend sym, Integral n) => n -> SeqMap sym a -> [SEval sym a] Source #

Create a finite list of length `n` of the values from `[0..n-1]` in the given the sequence emap.

streamSeqMap :: Backend sym => SeqMap sym a -> [SEval sym a] Source #

Create an infinite stream of all the values in a sequence map

reverseSeqMap Source #

Arguments

:: Backend sym |
=> Integer | Size of the sequence map
-> SeqMap sym a |
-> SeqMap sym a |

Reverse the order of a finite sequence map

updateSeqMap :: SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a Source #

dropSeqMap :: Backend sym => Integer -> SeqMap sym a -> SeqMap sym a Source #

Drop the first `n` elements of the given `SeqMap`.

concatSeqMap :: Backend sym => Integer -> SeqMap sym a -> SeqMap sym a -> SeqMap sym a Source #

Concatenate the first `n` values of the first sequence map onto the beginning of the second sequence map.

splitSeqMap :: Backend sym => Integer -> SeqMap sym a -> (SeqMap sym a, SeqMap sym a) Source #

Given a number `n` and a sequence map, return two new sequence maps: the first containing the values from `[0..n-1]` and the next containing the values from `n` onward.

memoMap :: Backend sym => sym -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a) Source #

Given a sequence map, return a new sequence map that is memoized using a finite map memo table.

delaySeqMap :: Backend sym => sym -> SEval sym (SeqMap sym a) -> SEval sym (SeqMap sym a) Source #

zipSeqMap :: Backend sym => sym -> (a -> a -> SEval sym a) -> Nat' -> SeqMap sym a -> SeqMap sym a -> SEval sym (SeqMap sym a) Source #

Apply the given evaluation function pointwise to the two given sequence maps.

mapSeqMap :: Backend sym => sym -> (a -> SEval sym a) -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a) Source #

Apply the given function to each value in the given sequence map

mergeSeqMap :: Backend sym => sym -> (SBit sym -> a -> a -> SEval sym a) -> SBit sym -> SeqMap sym a -> SeqMap sym a -> SeqMap sym a Source #

barrelShifter Source #

Arguments

:: Backend sym |
=> sym |
-> (SBit sym -> a -> a -> SEval sym a) | ifthenelse operation of values
-> (SeqMap sym a -> Integer -> SEval sym (SeqMap sym a)) | concrete shifting operation
-> Nat' | Size of the map being shifted
-> SeqMap sym a | initial value
-> Integer |
-> [IndexSegment sym] | segments of the shift amount, in big-endian order
-> SEval sym (SeqMap sym a) |

shiftSeqByInteger Source #

Arguments

:: Backend sym |
=> sym |
-> (SBit sym -> a -> a -> SEval sym a) | ifthenelse operation of values
-> (Integer -> Integer -> Maybe Integer) | reindexing operation
-> SEval sym a | zero value
-> Nat' | size of the sequence
-> SeqMap sym a | sequence to shift
-> SInteger sym | shift amount, assumed to be in range [0,len]
-> SEval sym (SeqMap sym a) |

data IndexSegment sym Source #

Constructors

BitIndexSegment (SBit sym) |
WordIndexSegment (SWord sym) |