GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-16 11:22:33 +03:00
Code Issues Projects Releases Wiki Activity

Fix #101 by defining bitSizeMaybe

Browse Source 
intSize was undefined, causing repl terminate.  This is probably because
the incorrect type signature using the scoped type variable (`:: a`
should probably have been `:: SBV a`) either way, bitSize and
bitSizeMaybe should use the same code when the size is finite.
This commit is contained in:
Thomas M. DuBuisson 2014-09-13 01:17:05 -07:00
parent 1cf1e552df
commit 981235118b
2 changed files with 4 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
sbv/Data/SBV/BitVectors/Model.hs
View File

@ -773,7 +773,7 @@ instance ({-Num a,-} Bits a, SymWord a) => Bits (SBV a) where
complement = liftSym1 (mkSymOp1 Not) (noRealUnary "complement") complement (noFloatUnary "complement") (noDoubleUnary "complement")
bitSize x = case kindOf x of KBounded _ w -> w
#if __GLASGOW_HASKELL__ >= 708
bitSizeMaybe _ = Just $ intSizeOf (undefined :: a)
bitSizeMaybe x = Just $ case kindOf x of KBounded _ w -> w
#endif
isSigned x = case kindOf x of KBounded s _ -> s
bit i = 1 `shiftL` i

3
src/Cryptol/Symbolic/BitVector.hs
View File

@ -97,6 +97,9 @@ instance Bits BitVector where
complementBit (BV s m x) i = BV s m (complementBit x i)
testBit (BV _ _ x) i = testBit x i
bitSize (BV _ m _) = m
#if __GLASGOW_HASKELL__ >= 708
bitSizeMaybe (BV _ m _) = Just m
#endif
isSigned (BV s _ _) = s
popCount (BV _ _ x) = popCount x