Fix cast to integral types

[ziman]

@jeetu7 noticed that printLn $ cast {to = Int} 4.2 prints 4.0 rather than 4.

Maybe we could say that it's not defined anywhere how primitives like integers should print but it's probably better to make it less surprising. I changed floor to exact-floor, which I implemented using floor and inexact->exact in non-Racket backends.

It seems that integral division and cast-string-int had the same problem, so I made them use exact-floor, too.

[gallais]

Probably worth adding a test case for these?

[ziman]

I can't say I know what's going on here but chez014 would hang in recv(), unless I switch cast-string-int back to using floor instead of exact-floor. I arrived at this by looking at the source of -p network, where the only code path that could possibly be affected by this change is IP address parsing.

The whole thing is quite strange; for example, chez014 starts working as intended if you put a printLn "A" anywhere, even at the end of the program, i.e. after the call to recv. If I use trace-lambda to trace the calls to cast-string-int, it shows that there are only four calls to this function (for numbers 127, 0, 0, 1), and the output seems to be integral in all four cases. (Debug prints also cause chez014 to work as intended, even with exact-floor.)

Anyway, I give up and I'm leaving cast-string-int unfixed. There are a few test cases commented out in reg016 that print incorrect results for that reason. Once the mysterious bug is fixed, these test cases can be uncommented.

[jeetu7]

Just to add. In REPL it seems creating the correct thing.

~ ➤ idris2                                                                                                                                  
     ____    __     _         ___                                           
    /  _/___/ /____(_)____   |__ \                                          
    / // __  / ___/ / ___/   __/ /     Version 0.1.0-1c4b558b2
  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org           
 /___/\__,_/_/  /_/____/   /____/      Type :? for help                     

Welcome to Idris 2.  Enjoy yourself!
Main> printLn $ cast {to = Int} 4.2
MkIO (prim__putStr "4\n")
Main> printLn $ 4.2
MkIO (prim__putStr "4.2\n")
Main>

[jeetu7]

And here is the gist to reproduce it. Directly printing Int works fine. But cast have some issues. https://gist.github.com/jeetu7/c16b1c2931d74d8f8d04f56626559f74

[abailly]

Seems like the issue with chez014 only happens from the toplevel, running directly in the test directory works fine:

$ ./run ../../../idris2
C:sending hello world!
C:receiving from 7
C:receiving from 5
C:received hello world!
Received: hello world!
C:sending echo: hello world!
C:received echo: hello world!
Received: echo: hello world!
Main> Main> Bye for now!

Wondering if there's not some interaction with stdin/stdout with the way tests are run wrapped from tests/Main.idr...

[ziman]

If you print anything, then recv() will not hang. If I don't put any debug prints in, then I can reliably reproduce the hang using ./run ../../../idris2.

At least that's how it behaves on my machine.

[abailly]

That's funny, because I have put some debugging in the C code, and it now hangs with make test but not when running it directly... -- Arnaud Bailly - @dr_c0d3

On Wed, Apr 15, 2020 at 2:57 PM Matúš Tejiščák notifications@github.com wrote:

If you print anything, then recv() will not hang. If I don't put any debug prints in, then I can reliably reproduce the hang using ./run ../../../idris2.

At least that's how it behaves on my machine.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/edwinb/Idris2/pull/281#issuecomment-614022970, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAAJ2HMDCMNTNWL5KUV73P3RMWVKFANCNFSM4MH7DUAA .

[edwinb]

Oh, I've just noticed something after merging, which is that the test here uses the chez back end. Ideally these should be in a block of tests after the test program has checked that chez is installed. I'll fix this... maybe best to make a category for regressions in the back end.