mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-14 17:51:43 +03:00
Replace fromIntegral
with fromInteger
or toInteger
where possible.
See #637.
This commit is contained in:
parent
484f9fc631
commit
2e72a7387c
@ -461,7 +461,7 @@ evalSetSel e x v =
|
||||
case x of
|
||||
TupleSel n _ -> setTuple n
|
||||
RecordSel n _ -> setRecord n
|
||||
ListSel ix _ -> setList (fromIntegral ix)
|
||||
ListSel ix _ -> setList (toInteger ix)
|
||||
|
||||
where
|
||||
bad msg =
|
||||
|
@ -245,7 +245,7 @@ primLexer cfg cs = run inp Normal
|
||||
, alexPos i')
|
||||
AlexSkip i' _ -> run i' s
|
||||
AlexToken i' l act ->
|
||||
let txt = Text.take (fromIntegral l) (input i)
|
||||
let txt = Text.take l (input i)
|
||||
(mtok,s') = act cfg (alexPos i) txt s
|
||||
(rest,pos) = run i' $! s'
|
||||
in case mtok of
|
||||
|
@ -214,15 +214,15 @@ splitQual t =
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
numToken :: Integer -> Text -> TokenT
|
||||
numToken rad ds = Num (toVal ds') (fromInteger rad) (fromIntegral (T.length ds'))
|
||||
numToken rad ds = Num (toVal ds') (fromInteger rad) (T.length ds')
|
||||
where
|
||||
ds' = T.filter (/= '_') ds
|
||||
toVal = T.foldl' (\x c -> rad * x + fromDigit c) 0
|
||||
|
||||
fromDigit :: Char -> Integer
|
||||
fromDigit x'
|
||||
| 'a' <= x && x <= 'z' = fromIntegral (10 + fromEnum x - fromEnum 'a')
|
||||
| otherwise = fromIntegral (fromEnum x - fromEnum '0')
|
||||
| 'a' <= x && x <= 'z' = toInteger (10 + fromEnum x - fromEnum 'a')
|
||||
| otherwise = toInteger (fromEnum x - fromEnum '0')
|
||||
where x = toLower x'
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
|
@ -96,7 +96,7 @@ noPat pat =
|
||||
x <- newName
|
||||
r <- getRange
|
||||
let len = length ps
|
||||
ty = TSeq (TNum (fromIntegral len)) TWild
|
||||
ty = TSeq (TNum (toInteger len)) TWild
|
||||
getN a n = sel a x (ListSel n (Just len))
|
||||
return (pTy r x ty, zipWith getN as [0..] ++ concat dss)
|
||||
|
||||
|
@ -184,7 +184,7 @@ getName l = case thing l of
|
||||
getNum :: Located Token -> Integer
|
||||
getNum l = case thing l of
|
||||
Token (Num x _ _) _ -> x
|
||||
Token (ChrLit x) _ -> fromIntegral (fromEnum x)
|
||||
Token (ChrLit x) _ -> toInteger (fromEnum x)
|
||||
_ -> panic "[Parser] getNum" ["not a number:", show l]
|
||||
|
||||
getStr :: Located Token -> String
|
||||
|
@ -660,7 +660,7 @@ signedBV :: BV -> Integer
|
||||
signedBV (BV i x) = signedValue i x
|
||||
|
||||
signedValue :: Integer -> Integer -> Integer
|
||||
signedValue i x = if testBit x (fromIntegral (i-1)) then x - (1 `shiftL` (fromIntegral i)) else x
|
||||
signedValue i x = if testBit x (fromInteger (i-1)) then x - (1 `shiftL` (fromInteger i)) else x
|
||||
|
||||
bvSlt :: Integer -> Integer -> Integer -> Eval Value
|
||||
bvSlt _sz x y = return . VBit $! (x < y)
|
||||
@ -679,7 +679,7 @@ sshrV =
|
||||
nlam $ \_k ->
|
||||
wlam $ \(BV i x) -> return $
|
||||
wlam $ \y ->
|
||||
let signx = testBit x (fromIntegral (i-1))
|
||||
let signx = testBit x (fromInteger (i-1))
|
||||
amt = fromInteger (bvVal y)
|
||||
negv = (((-1) `shiftL` amt) .|. x) `shiftR` amt
|
||||
posv = x `shiftR` amt
|
||||
@ -1481,7 +1481,7 @@ randomV ty seed =
|
||||
Just gen ->
|
||||
-- unpack the seed into four Word64s
|
||||
let mask64 = 0xFFFFFFFFFFFFFFFF
|
||||
unpack s = fromIntegral (s .&. mask64) : unpack (s `shiftR` 64)
|
||||
unpack s = fromInteger (s .&. mask64) : unpack (s `shiftR` 64)
|
||||
[a, b, c, d] = take 4 (unpack seed)
|
||||
in fst $ gen 100 $ seedTFGen (a, b, c, d)
|
||||
|
||||
|
@ -425,7 +425,7 @@ qcCmd qcMode str =
|
||||
lg2 :: Integer -> Integer
|
||||
lg2 x | x >= 2^(1024::Int) = 1024 + lg2 (x `div` 2^(1024::Int))
|
||||
| x == 0 = 0
|
||||
| otherwise = let valNumD = fromIntegral x :: Double
|
||||
| otherwise = let valNumD = fromInteger x :: Double
|
||||
in round $ logBase 2 valNumD :: Integer
|
||||
|
||||
prt msg = rPutStr msg >> io (hFlush stdout)
|
||||
|
@ -793,7 +793,7 @@ userOptions = mkOptionMap
|
||||
"Enable type-checker debugging output." $
|
||||
\case EnvNum n -> do me <- getModuleEnv
|
||||
let cfg = M.meSolverConfig me
|
||||
setModuleEnv me { M.meSolverConfig = cfg{ T.solverVerbose = fromIntegral n } }
|
||||
setModuleEnv me { M.meSolverConfig = cfg{ T.solverVerbose = n } }
|
||||
_ -> return ()
|
||||
, OptionDescr "core-lint" (EnvBool False)
|
||||
noCheck
|
||||
|
@ -193,7 +193,7 @@ instance BitWord SBool SWord SInteger where
|
||||
wordLit n x = svInteger (KBounded False (fromInteger n)) x
|
||||
integerLit x = svInteger KUnbounded x
|
||||
|
||||
wordBit x idx = svTestBit x (intSizeOf x - 1 - fromIntegral idx)
|
||||
wordBit x idx = svTestBit x (intSizeOf x - 1 - fromInteger idx)
|
||||
|
||||
wordUpdate x idx b = svSymbolicMerge (kindOf x) False b wtrue wfalse
|
||||
where
|
||||
|
@ -126,7 +126,7 @@ desugarLiteral fixDec lit =
|
||||
P.PolyLit _n -> [ ("rep", P.TSeq P.TWild P.TBit) ]
|
||||
|
||||
P.ECString s ->
|
||||
P.ETyped (P.EList [ P.ELit (P.ECNum (fromIntegral (fromEnum c))
|
||||
P.ETyped (P.EList [ P.ELit (P.ECNum (toInteger (fromEnum c))
|
||||
P.CharLit) | c <- s ])
|
||||
(P.TSeq P.TWild (P.TSeq (P.TNum 8) P.TBit))
|
||||
|
||||
|
@ -372,7 +372,7 @@ doCheckType ty k =
|
||||
P.TSeq t1 t2 -> tcon (TC TCSeq) [t1,t2] k
|
||||
P.TBit -> tcon (TC TCBit) [] k
|
||||
P.TNum n -> tcon (TC (TCNum n)) [] k
|
||||
P.TChar n -> tcon (TC (TCNum $ fromIntegral $ fromEnum n)) [] k
|
||||
P.TChar n -> tcon (TC (TCNum $ toInteger $ fromEnum n)) [] k
|
||||
|
||||
P.TTuple ts -> tcon (TC (TCTuple (length ts))) ts k
|
||||
|
||||
|
@ -326,7 +326,7 @@ checkHas t sel =
|
||||
Just len ->
|
||||
case tNoUser n of
|
||||
TCon (TC (TCNum m)) []
|
||||
| m == fromIntegral len -> return ()
|
||||
| m == toInteger len -> return ()
|
||||
_ -> reportError $ UnexpectedSequenceShape len n
|
||||
|
||||
return elT
|
||||
|
@ -449,7 +449,7 @@ pIsWidth ty = case tNoUser ty of
|
||||
|
||||
|
||||
tNum :: Integral a => a -> Type
|
||||
tNum n = TCon (TC (TCNum (fromIntegral n))) []
|
||||
tNum n = TCon (TC (TCNum (toInteger n))) []
|
||||
|
||||
tZero :: Type
|
||||
tZero = tNum (0 :: Int)
|
||||
|
Loading…
Reference in New Issue
Block a user