GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-17 04:44:39 +03:00
Code Issues Projects Releases Wiki Activity

generalize the 'zero' operation

Browse Source
This commit is contained in:
Rob Dockins 2016-05-15 22:34:06 -07:00
parent da4a458aed
commit 1b51f0edf4
1 changed files with 6 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
src/Cryptol/Prims/Eval.hs
View File

@ -473,17 +473,20 @@ funCmp op =
-- Logic -----------------------------------------------------------------------
zeroV :: TValue -> Value
zeroV :: forall b w
. BitWord b w
=> TValue
-> GenValue b w
zeroV ty
-- bits
| isTBit ty =
VBit False
VBit (bitLit False)
-- sequences
| Just (n,ety) <- isTSeq ty =
case numTValue n of
Nat w | isTBit ety -> word w 0
Nat w | isTBit ety -> VWord $ wordLit w 0
| otherwise -> mkSeq n ety (SeqMap $ \_ -> ready $ zeroV ety)
Inf -> mkSeq n ety (SeqMap $ \_ -> ready $ zeroV ety)