search

edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris
https://idris-lang.org/
Other
902 stars 58 forks source link

Integers > 2^31-1 getting mangled during parsing/compiling #345

Closed cypheon closed 4 years ago

cypheon commented 4 years ago

It seems large (>31 bits) integers somehow get mangled.

Steps to Reproduce

module Main

main : IO ()
main = do
  putStrLn $ show 2147483647
  putStrLn $ show 2147483648
  putStrLn $ show 2147483649
  putStrLn $ show 3518437212345678901234567890123

idris2 --exec main Integers.idr

Expected Behavior

2147483647
2147483648
2147483649
3518437212345678901234567890123

Observed Behavior

2147483647
-2147483648
-2147483647
3518437212327232157160858338507

This behavior seems to be present for a while, since the test chez015 verifies that:

  3518437212345678901234567890123
                            + 437
= 3518437212327232157160858338944

Which is only working, because 351...123 becomes 351...507

The problem does not occur in the REPL:

Main> show 3518437212345678901234567890123
"3518437212345678901234567890123"

(From my naïve point of view, it looks like the (Big)Integer is at some point interpreted as or casted to a signed int32).

Checked on macOS with Idris2 master@409357c and on Linux with Idris2 v0.1.0

cypheon commented 4 years ago

One thing I forgot to mention: I suspect this to be a problem with parsing / compiling, because the negative integers also appear in the generated Scheme source file. So it's probably not a runtime issue.

cypheon commented 4 years ago

I managed to track down the issue to a TTC file (un)marshalling bug, which explains, why it did not occur in the REPL. The linked PR fixes this.