Cryptol.Backend.SeqMap

Sequence Maps

data SeqMap sym a

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

Instances

Backend sym => Functor (SeqMap sym)

Defined in Cryptol.Backend.SeqMap

Methods

fmap :: (a -> b) -> SeqMap sym a -> SeqMap sym b

(<$) :: a -> SeqMap sym b -> 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

Generate a finite sequence map from a list of values

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

Generate an infinite sequence map from a stream of values

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

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]

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

reverseSeqMap

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

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

Drop the first n elements of the given SeqMap.

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

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)

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)

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)

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

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)

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

barrelShifter

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

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

Constructors

BitIndexSegment (SBit sym)

WordIndexSegment (SWord sym)