Add functions for rounding rationals to integers

[barrettj12]

Implements functions for rounding rationals to integers, thereby solving #1063.

[MatthewDaggitt]

Thanks for the great PR! I've added a few minor comments about library style, feel free to check out the style guide for more detail.

On the more major questions side, these don't have any particularly fancy import requirements so I think they could probably go in Data.Rational.Base?

It'd also be good to add their counter-parts to Data.Rational.Unnormalised while you're here? As an aside that might help you prove some properties around them as well, as the standard proof style is first to prove properties of the unnormalised operations, then prove they're isomorphic to the normalised versions and then transfer the proofs across.

[gallais]

Can we add some test cases to https://github.com/agda/agda-stdlib/tree/master/tests/data
to make sure we're getting the appropriate behaviour on edge cases?

[barrettj12]

Can we add some test cases to https://github.com/agda/agda-stdlib/tree/master/tests/data
to make sure we're getting the appropriate behaviour on edge cases?

Sure, that sounds like a good idea. Is there a guide on how to do this? I don't have any experience with that.

[gallais]

Not really: it's a fairly new addition to the stdlib.
The easiest way is probably to:

1. cp -R an existing directory
2. Edit the main agda file to add your tests [1]
3. Add the new test case to the the appropriate pool in the test runner
4. Run the test suite and accept the update expected file
5. Commit all of that

[1] They get run using the run file in the directory so you could have unit tests
of the form

_ : a \== b
_ = refl

and run would just make sure the file typechecks or you could have full blown
programs that get compiled & run. As you want.

[barrettj12]

Side note: what should the fractional part of -3.7 be? I reckon 0.7.

[JacquesCarette]

I'm sure there are coherent ways of making it 0.7, -0.7, 0.3 or -0.3. To me, it all depends on what relations with ceil, floor and/or round and addition you want to hold.

[barrettj12]

Yeah, there doesn't seem to be a convention, so I will redefine round and fracPart to get symmetry, i.e.

round p = round (- p)
fracPart p = fracPart (- p)

[barrettj12]

@gallais I've put in the new test cases under tests/data/rational. I think I've done it right.
@MatthewDaggitt I've implemented the changes you suggested, except I still haven't been able to prove anything useful about these functions. I'm happy to open a new issue for proving the properties.

[gallais]

Looks like you happen to have a trailing newline in your expected file.

[barrettj12]

Looks like you happen to have a trailing newline in your expected file.

No, it appears that I didn't have a trailing newline, but now I've added one to match the other expected files. Now the tests are passing fine, but it doesn't want to play nice with GHC. The error was

Cannot add PPA: 'ppa:~hvr/ubuntu/ghc'.
ERROR: '~hvr' user or team does not exist.

which might have been caused by a faulty internet connection. Can we re-run those checks?

EDIT: The checks all look fine now.

[MatthewDaggitt]

Looks good! Thanks for the PR!