GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-24 06:52:44 +03:00
Code Issues Projects Releases Wiki Activity

fixed replicateV during symbolic simulation

Browse Source 
Previously this function would always produce a sequence with the
"isWord" bit set to False. It now takes a type argument so that it can
properly set it to True when the elements are Bits.
This commit is contained in:
Adam C. Foltzer 2015-06-01 12:33:07 -07:00
parent d5988338be
commit 28960c1b68
1 changed files with 11 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
src/Cryptol/Symbolic/Prims.hs
View File

@ -106,8 +106,8 @@ evalECon econ =
shl i =
case numTValue m of
Inf -> dropV i xs
Nat j | i >= j -> replicateV j (zeroV a)
| otherwise -> catV (dropV i xs) (replicateV i (zeroV a))
Nat j | i >= j -> replicateV j a (zeroV a)
| otherwise -> catV (dropV i xs) (replicateV i a (zeroV a))
ECShiftR -> -- {m,n,a} (fin n) => [m] a -> [n] -> [m] a
tlam $ \m ->
@ -122,9 +122,9 @@ evalECon econ =
shr :: Integer -> Value
shr i =
case numTValue m of
Inf -> catV (replicateV i (zeroV a)) xs
Nat j | i >= j -> replicateV j (zeroV a)
| otherwise -> catV (replicateV i (zeroV a)) (takeV (j - i) xs)
Inf -> catV (replicateV i a (zeroV a)) xs
Nat j | i >= j -> replicateV j a (zeroV a)
| otherwise -> catV (replicateV i a (zeroV a)) (takeV (j - i) xs)
ECRotL -> -- {m,n,a} (fin m, fin n) => [m] a -> [n] -> [m] a
tlam $ \m ->
@ -298,8 +298,12 @@ selectV f v = sel 0 bits
where m1 = sel (offset + 2 ^ length bs) bs
m2 = sel offset bs
replicateV :: Integer -> Value -> Value
replicateV n x = VSeq False (genericReplicate n x)
replicateV :: Integer -- ^ number of elements
-> TValue -- ^ type of element
-> Value -- ^ element
-> Value
replicateV n (toTypeVal -> TVBit) x = VSeq True (genericReplicate n x)
replicateV n _ x = VSeq False (genericReplicate n x)
nth :: a -> [a] -> Int -> a
nth def [] _ = def