Re: [isabelle-dev] NEWS: Rat in Isabelle/ML
Very good! This is very convenient.
On 01/06/16 21:42, Makarius wrote:
*** ML ***
* Structure Rat for rational numbers is now an integral part of
Isabelle/ML, with special notation @int/nat or @int for numerals (an
abbreviation for antiquotation @{Pure.rat argument}) and ML pretty
printing. Standard operations on type Rat.rat are provided via ad-hoc
overloading of + - * / < <= > >= ~ abs. INCOMPATIBILITY, need to
use + instead of +/ etc. Moreover, exception Rat.DIVZERO has been
superseded by General.Div.
This refers to Isabelle/c7de5b311909, which also contains the updated
documentation.
The antiquotation syntax @int/nat for @{Pure.rat argument} is stretching
the existing syntax very little, see 921a5be54132. Further changesets in
the vicinity clean up rat.ML is various repects -- it is surprising how
many details can be missing in such a small module.
I have compared it with the MyRat implementation by Manuel Eberl
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2016-April/msg2.html
as well as rat.ML in https://bitbucket.org/lcpaulson/metitarski
b11e8139b880 (where a comment says that it goes back to John Harrison).
Further comments? Anything missing?
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Rat in Isabelle/ML
On 01/06/16 21:47, Lawrence Paulson wrote: > Doesn’t Poly/ML include an option to support GCDs (if not rationals) > efficiently? Do you mean PolyML.IntInf.gcd and PolyML.IntInf.lcm? That is already used (da38571dd5bd). These operations normally use GNU MP, but on Mac OS X only the old builtin bigints of Poly/ML. (I still don't know how to compile Poly/ML with libgmp such that the binary becomes self-contained.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Rat in Isabelle/ML
On 01/06/16 21:58, Florian Haftmann wrote: > > One could regard the dedicated literal syntax for rationals a little bit > oversophisticated; maybe an infix // for Rat.make would serve better. > Or we could A matter of personal taste, though. There is a delicate point here: our antiquotation infrastructure distinguishes inlined text from compile-time values. @a/b is the latter, so it is always guaranteed to be pre-evaluated, independently of other code inline options of Poly/ML. This is also the reason why I have removed Rat.zero, Rat.one, Rat.two and used @0, @1, @2 everywhere. Makarius signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Rat in Isabelle/ML
> * Structure Rat for rational numbers is now an integral part of
> Isabelle/ML, with special notation @int/nat or @int for numerals (an
> abbreviation for antiquotation @{Pure.rat argument}) and ML pretty
> printing. Standard operations on type Rat.rat are provided via ad-hoc
> overloading of + - * / < <= > >= ~ abs. INCOMPATIBILITY, need to
> use + instead of +/ etc. Moreover, exception Rat.DIVZERO has been
> superseded by General.Div.
>
>
> This refers to Isabelle/c7de5b311909, which also contains the updated
> documentation.
>
> The antiquotation syntax @int/nat for @{Pure.rat argument} is stretching
> the existing syntax very little, see 921a5be54132. Further changesets in
> the vicinity clean up rat.ML is various repects -- it is surprising how
> many details can be missing in such a small module.
>
> I have compared it with the MyRat implementation by Manuel Eberl
> https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2016-April/msg2.html
> as well as rat.ML in https://bitbucket.org/lcpaulson/metitarski
> b11e8139b880 (where a comment says that it goes back to John Harrison).
>
>
> Further comments? Anything missing?
Very fine. Indeed rat.ML has been one of my first Isabelle playgrounds,
and I did not have much experience then.
One could regard the dedicated literal syntax for rationals a little bit
oversophisticated; maybe an infix // for Rat.make would serve better.
Or we could A matter of personal taste, though.
Cheers,
Florian
--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: Rat in Isabelle/ML
*** ML ***
* Structure Rat for rational numbers is now an integral part of
Isabelle/ML, with special notation @int/nat or @int for numerals (an
abbreviation for antiquotation @{Pure.rat argument}) and ML pretty
printing. Standard operations on type Rat.rat are provided via ad-hoc
overloading of + - * / < <= > >= ~ abs. INCOMPATIBILITY, need to
use + instead of +/ etc. Moreover, exception Rat.DIVZERO has been
superseded by General.Div.
This refers to Isabelle/c7de5b311909, which also contains the updated
documentation.
The antiquotation syntax @int/nat for @{Pure.rat argument} is stretching
the existing syntax very little, see 921a5be54132. Further changesets in
the vicinity clean up rat.ML is various repects -- it is surprising how
many details can be missing in such a small module.
I have compared it with the MyRat implementation by Manuel Eberl
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2016-April/msg2.html
as well as rat.ML in https://bitbucket.org/lcpaulson/metitarski
b11e8139b880 (where a comment says that it goes back to John Harrison).
Further comments? Anything missing?
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
