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

Merge pull request #720 from GaloisInc/fromInteger

Browse Source 
Avoid using `fromInteger`.
This commit is contained in:
brianhuffman 2020-05-27 10:56:28 -07:00 committed by GitHub
commit 63bfdb2c06
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
8 changed files with 21 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Cryptol/Eval.hs
View File

@ -358,7 +358,7 @@ etaWord ::
etaWord sym n val = do
w <- sDelay sym Nothing (fromWordVal "during eta-expansion" =<< val)
xs <- memoMap $ IndexSeqMap $ \i ->
do w' <- w; VBit <$> indexWordValue sym w' (toInteger i)
do w' <- w; VBit <$> indexWordValue sym w' i
pure $ LargeBitsVal n xs
{-# SPECIALIZE etaDelay ::

4
src/Cryptol/Eval/Generic.hs
View File

@ -708,7 +708,7 @@ joinSeq sym (Nat parts) each TVBit xs
= do let zs = IndexSeqMap $ \i ->
do let (q,r) = divMod i each
ys <- fromWordVal "join seq" =<< lookupSeqMap xs q
VBit <$> indexWordValue sym ys (fromInteger r)
VBit <$> indexWordValue sym ys r
return $ VWord (parts * each) $ pure $ LargeBitsVal (parts * each) zs
-- infinite sequence of words
@ -716,7 +716,7 @@ joinSeq sym Inf each TVBit xs
= return $ VStream $ IndexSeqMap $ \i ->
do let (q,r) = divMod i each
ys <- fromWordVal "join seq" =<< lookupSeqMap xs q
VBit <$> indexWordValue sym ys (fromInteger r)
VBit <$> indexWordValue sym ys r
-- finite or infinite sequence of non-words
joinSeq _sym parts each _a xs

5
src/Cryptol/Parser.y
View File

@ -484,7 +484,7 @@ no_sel_aexpr :: { Expr PName }
| NUM { at $1 $ numLit (tokenType (thing $1)) }
| STRLIT { at $1 $ ELit $ ECString $ getStr $1 }
| CHARLIT { at $1 $ ELit $ ECNum (getNum $1) CharLit }
| CHARLIT { at $1 $ ELit $ ECChar $ getChr $1 }
| '_' { at $1 $ EVar $ mkUnqual $ mkIdent "_" }
| '(' expr ')' { at ($1,$3) $ EParens $2 }
@ -672,8 +672,7 @@ atype :: { Type PName }
: qname { at $1 $ TUser (thing $1) [] }
| '(' qop ')' { at $1 $ TUser (thing $2) [] }
| NUM { at $1 $ TNum (getNum $1) }
| CHARLIT { at $1 $ TChar (toEnum $ fromInteger
$ getNum $1) }
| CHARLIT { at $1 $ TChar (getChr $1) }
| '[' type ']' { at ($1,$3) $ TSeq $2 TBit }
| '(' type ')' { at ($1,$3) $ TParens $2 }
| '(' ')' { at ($1,$2) $ TTuple [] }

4
src/Cryptol/Parser/AST.hs
View File

@ -277,12 +277,12 @@ data NumInfo = BinLit Int -- ^ n-digit binary literal
| OctLit Int -- ^ n-digit octal literal
| DecLit -- ^ overloaded decimal literal
| HexLit Int -- ^ n-digit hex literal
| CharLit -- ^ character literal
| PolyLit Int -- ^ polynomial literal
deriving (Eq, Show, Generic, NFData)
-- | Literals.
data Literal = ECNum Integer NumInfo -- ^ @0x10@ (HexLit 2)
| ECChar Char -- ^ @'a'@
| ECString String -- ^ @\"hello\"@
deriving (Eq, Show, Generic, NFData)
@ -623,6 +623,7 @@ instance PP Literal where
ppPrec _ lit =
case lit of
ECNum n i -> ppNumLit n i
ECChar c -> text (show c)
ECString s -> text (show s)
@ -630,7 +631,6 @@ ppNumLit :: Integer -> NumInfo -> Doc
ppNumLit n info =
case info of
DecLit -> integer n
CharLit -> text (show (toEnum (fromInteger n) :: Char))
BinLit w -> pad 2 "0b" w
OctLit w -> pad 8 "0o" w
HexLit w -> pad 16 "0x" w

6
src/Cryptol/Parser/LexerUtils.hs
View File

@ -213,11 +213,11 @@ splitQual t =
--------------------------------------------------------------------------------
numToken :: Integer -> Text -> TokenT
numToken rad ds = Num (toVal ds') (fromInteger rad) (T.length ds')
numToken :: Int {- ^ base -} -> Text -> TokenT
numToken rad ds = Num (toVal ds') rad (T.length ds')
where
ds' = T.filter (/= '_') ds
toVal = T.foldl' (\x c -> rad * x + fromDigit c) 0
toVal = T.foldl' (\x c -> toInteger rad * x + fromDigit c) 0
fromDigit :: Char -> Integer
fromDigit x'

5
src/Cryptol/Parser/ParserUtils.hs
View File

@ -190,6 +190,11 @@ getNum l = case thing l of
Token (ChrLit x) _ -> toInteger (fromEnum x)
_ -> panic "[Parser] getNum" ["not a number:", show l]
getChr :: Located Token -> Char
getChr l = case thing l of
Token (ChrLit x) _ -> x
_ -> panic "[Parser] getChr" ["not a char:", show l]
getStr :: Located Token -> String
getStr l = case thing l of
Token (StrLit x) _ -> x

2
src/Cryptol/Parser/Utils.hs
View File

@ -53,6 +53,6 @@ translateExprToNumT expr =
TUser f ts -> return (TUser f (ts ++ [t]))
_ -> Nothing
cvtLit (ECNum n CharLit) = return (TChar $ toEnum $ fromInteger n)
cvtLit (ECNum n _) = return (TNum n)
cvtLit (ECChar c) = return (TChar c)
cvtLit (ECString _) = Nothing

8
src/Cryptol/TypeCheck/Infer.hs
View File

@ -115,7 +115,6 @@ desugarLiteral fixDec lit =
P.BinLit n -> [ ("rep", tBits (1 * toInteger n)) ]
P.OctLit n -> [ ("rep", tBits (3 * toInteger n)) ]
P.HexLit n -> [ ("rep", tBits (4 * toInteger n)) ]
P.CharLit -> [ ("rep", tBits (8 :: Integer)) ]
P.DecLit
| fixDec -> if num == 0
then [ ("rep", tBits 0)]
@ -125,9 +124,12 @@ desugarLiteral fixDec lit =
| otherwise -> [ ]
P.PolyLit _n -> [ ("rep", P.TSeq P.TWild P.TBit) ]
P.ECChar c ->
number [ ("val", P.TNum (toInteger (fromEnum c)))
, ("rep", tBits (8 :: Integer)) ]
P.ECString s ->
P.ETyped (P.EList [ P.ELit (P.ECNum (toInteger (fromEnum c))
P.CharLit) | c <- s ])
P.ETyped (P.EList [ P.ELit (P.ECChar c) | c <- s ])
(P.TSeq P.TWild (P.TSeq (P.TNum 8) P.TBit))