diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index 2cc632f95..8b10197b7 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/src/Idris/IDEMode/REPL.idr @@ -129,7 +129,7 @@ getInput f do rest <- getFLine f pure (pack x ++ rest) Just num => - do inp <- getNChars f (integerToNat (cast num)) + do inp <- getNChars f (integerToNat num) pure (pack inp) ||| Do nothing and tell the user to wait for us to implmement this (or join the effort!) diff --git a/src/Libraries/Utils/Hex.idr b/src/Libraries/Utils/Hex.idr index 7b2e9642d..2551dc111 100644 --- a/src/Libraries/Utils/Hex.idr +++ b/src/Libraries/Utils/Hex.idr @@ -66,13 +66,16 @@ fromHexDigit 'f' = Just 15 fromHexDigit _ = Nothing export -fromHexChars : List Char -> Maybe Int +fromHexChars : List Char -> Maybe Integer fromHexChars = fromHexChars' 1 where - fromHexChars' : Int -> List Char -> Maybe Int + fromHexChars' : Integer -> List Char -> Maybe Integer fromHexChars' _ [] = Just 0 - fromHexChars' m (d :: ds) = pure $ !(fromHexDigit (toLower d)) * m + !(fromHexChars' (m*16) ds) + fromHexChars' m (d :: ds) + = do digit <- fromHexDigit (toLower d) + digits <- fromHexChars' (m*16) ds + pure $ cast digit * m + digits export -fromHex : String -> Maybe Int +fromHex : String -> Maybe Integer fromHex = fromHexChars . unpack diff --git a/src/Libraries/Utils/Octal.idr b/src/Libraries/Utils/Octal.idr index 8153961ad..ba2b88659 100644 --- a/src/Libraries/Utils/Octal.idr +++ b/src/Libraries/Utils/Octal.idr @@ -39,13 +39,16 @@ fromOctDigit '7' = Just 7 fromOctDigit _ = Nothing export -fromOctChars : List Char -> Maybe Int +fromOctChars : List Char -> Maybe Integer fromOctChars = fromOctChars' 1 where - fromOctChars' : Int -> List Char -> Maybe Int + fromOctChars' : Integer -> List Char -> Maybe Integer fromOctChars' _ [] = Just 0 - fromOctChars' m (d :: ds) = pure $ !(fromOctDigit (toLower d)) * m + !(fromOctChars' (m*8) ds) + fromOctChars' m (d :: ds) + = do digit <- fromOctDigit (toLower d) + digits <- fromOctChars' (m*8) ds + pure $ cast digit * m + digits export -fromOct : String -> Maybe Int +fromOct : String -> Maybe Integer fromOct = fromOctChars . unpack diff --git a/src/Parser/Lexer/Source.idr b/src/Parser/Lexer/Source.idr index a1c49bf9a..1bf101ffb 100644 --- a/src/Parser/Lexer/Source.idr +++ b/src/Parser/Lexer/Source.idr @@ -4,6 +4,7 @@ import public Parser.Lexer.Common import Data.List1 import Data.List +import Data.Maybe import Data.Strings import Libraries.Data.String.Extra import public Libraries.Text.Bounded @@ -234,18 +235,16 @@ fromHexLit str = if length str <= 2 then 0 else let num = assert_total (strTail (strTail str)) in - case fromHex (reverse num) of - Nothing => 0 -- can't happen if the literal lexed correctly - Just n => cast n + fromMaybe 0 (fromHex (reverse num)) + -- ^-- can't happen if the literal was lexed correctly fromOctLit : String -> Integer fromOctLit str = if length str <= 2 then 0 else let num = assert_total (strTail (strTail str)) in - case fromOct (reverse num) of - Nothing => 0 -- can't happen if the literal lexed correctly - Just n => cast n + fromMaybe 0 (fromOct (reverse num)) + -- ^-- can't happen if the literal lexed correctly rawTokens : TokenMap Token rawTokens = diff --git a/tests/Main.idr b/tests/Main.idr index 70ad75d61..564ad0231 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -45,7 +45,7 @@ idrisTestsBasic = MkTestPool [] "basic036", "basic037", "basic038", "basic039", "basic040", "basic041", "basic042", "basic043", "basic044", "basic045", "basic046", "basic047", "basic048", "basic049", "basic050", - "basic051", "basic052", "basic053"] + "basic051", "basic052", "basic053", "basic054"] idrisTestsCoverage : TestPool idrisTestsCoverage = MkTestPool [] diff --git a/tests/idris2/basic054/Issue1023.idr b/tests/idris2/basic054/Issue1023.idr new file mode 100644 index 000000000..3726b47e5 --- /dev/null +++ b/tests/idris2/basic054/Issue1023.idr @@ -0,0 +1,4 @@ +main : IO () +main = do + putStrLn $ show (the Bits64 0xffffffffffffffff) + putStrLn $ show (the Bits64 0x8000000000000000) diff --git a/tests/idris2/basic054/expected b/tests/idris2/basic054/expected new file mode 100644 index 000000000..c9f1c1ae7 --- /dev/null +++ b/tests/idris2/basic054/expected @@ -0,0 +1,2 @@ +18446744073709551615 +9223372036854775808 diff --git a/tests/idris2/basic054/run b/tests/idris2/basic054/run new file mode 100755 index 000000000..525bfcd47 --- /dev/null +++ b/tests/idris2/basic054/run @@ -0,0 +1,3 @@ +$1 --no-color --console-width 0 --no-banner Issue1023.idr --exec main + +rm -rf build