[ fix #1023 ] Hexadecimal literals can be pretty big

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!)

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

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

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 =

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 []

tests/idris2/basic054/Issue1023.idr

@@ -0,0 +1,4 @@
+main : IO ()
+main = do
+  putStrLn $ show (the Bits64 0xffffffffffffffff)
+  putStrLn $ show (the Bits64 0x8000000000000000)

tests/idris2/basic054/expected

@@ -0,0 +1,2 @@
+18446744073709551615
+9223372036854775808

tests/idris2/basic054/run

@@ -0,0 +1,3 @@
+$1 --no-color --console-width 0 --no-banner Issue1023.idr --exec main
+
+rm -rf build