Comment tweaks

This commit is contained in:
Rob Dockins 2020-03-30 09:35:00 -07:00
parent ffdf11d202
commit c94c929354
3 changed files with 3 additions and 5 deletions

View File

@ -507,7 +507,7 @@ class MonadIO (SEval sym) => Backend sym where
-- | Division of integers modulo n, for a concrete positive integer n.
-- NOTE: this is integer division on the initial segement of Z,
-- and not the multiplictitive inverse in Z_p.
-- and not the multiplicative inverse in Z_p.
znDiv ::
sym ->
Integer {- ^ modulus -} ->
@ -521,7 +521,7 @@ class MonadIO (SEval sym) => Backend sym where
-- | Modulus of integers modulo n, for a concrete positive integer n.
-- NOTE: this is the modulus corresponding to integer division on the initial
-- segement of Z, and not related to multiplictitive inverse in Z_p.
-- segement of Z, and not related to multiplicative inverse in Z_p.
znMod ::
sym ->
Integer {- ^ modulus -} ->

View File

@ -1288,7 +1288,7 @@ errorV sym ty msg = case ty of
TVAbstract {} -> cryUserError sym msg
-- | Expect a word value. Mask it an 8-bits ASCII value
-- | Expect a word value. Mask it to an 8-bits ASCII value
-- and return the associated character, if it is concrete.
-- Otherwise, return a '?' character
valueToChar :: Backend sym => sym -> GenValue sym -> SEval sym Char

View File

@ -320,14 +320,12 @@ instance Backend SBV where
znMult _ m a b = sModMult m a b
znNegate _ m a = sModNegate m a
-- TODO: implement this properly in SBV using "bv2int"
svToInteger :: SWord SBV -> SInteger SBV
svToInteger w =
case svAsInteger w of
Nothing -> svFromIntegral KUnbounded w
Just x -> svInteger KUnbounded x
-- TODO: implement this properly in SBV using "int2bv"
svFromInteger :: Integer -> SInteger SBV -> SWord SBV
svFromInteger 0 _ = literalSWord 0 0
svFromInteger n i =