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

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)