From c94c9293542cb5f481edd03c12a04b054dbf06f0 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Mon, 30 Mar 2020 09:35:00 -0700 Subject: [PATCH] Comment tweaks --- src/Cryptol/Eval/Backend.hs | 4 ++-- src/Cryptol/Eval/Generic.hs | 2 +- src/Cryptol/Eval/SBV.hs | 2 -- 3 files changed, 3 insertions(+), 5 deletions(-) diff --git a/src/Cryptol/Eval/Backend.hs b/src/Cryptol/Eval/Backend.hs index a505cef9..26a40595 100644 --- a/src/Cryptol/Eval/Backend.hs +++ b/src/Cryptol/Eval/Backend.hs @@ -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 -} -> diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs index d9695d6a..9f58768c 100644 --- a/src/Cryptol/Eval/Generic.hs +++ b/src/Cryptol/Eval/Generic.hs @@ -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 diff --git a/src/Cryptol/Eval/SBV.hs b/src/Cryptol/Eval/SBV.hs index 11fcf3a8..e5a32ddc 100644 --- a/src/Cryptol/Eval/SBV.hs +++ b/src/Cryptol/Eval/SBV.hs @@ -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 =