Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] How does Int31 "underlying mechanism for hardware-efficient computations" work?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How does Int31 "underlying mechanism for hardware-efficient computations" work?


Chronological Thread 
  • From: Laurent Thery <Laurent.Thery AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] How does Int31 "underlying mechanism for hardware-efficient computations" work?
  • Date: Fri, 1 Jul 2016 08:29:17 +0200



On 06/30/2016 12:04 PM, Soegtrop, Michael wrote:
Dear Laurent,

as it looks I might need 4 number libraries, one for reasonably efficient
safe computation in Coq, one for fast not so safe computation in Coq, another
one optimized for OCaml export and maybe yet another one which concentrates
on simplicity to help beginners to understand the interface.

E.g. an Int32 type is probably best mapped to an OCaml Int32 and not to a
BigN using Int31.

I guess the easiest way to switch libraries is to have an NumbersSafe,
NumbersFast, NumbersOcaml and NumbersSimpl folder with identical interfaces
and use the -Q option to map one of these to Numbers. I will look into this
and do some experiments.

If someone wants to review results from time to time, please let me know - I
plan to publish this as extension to the standard library.

Best regards,

That sounds really great.

For the NumberOcaml I guess if you are not really interested in modular arithmetic, you should just map it to an arbitary precision library.

--
Laurent




  • Re: [Coq-Club] How does Int31 "underlying mechanism for hardware-efficient computations" work?, Laurent Thery, 07/01/2016

Archive powered by MHonArc 2.6.18.

Top of Page