*To*: Jesus Aransay <jesus-maria.aransay at unirioja.es>*Subject*: Re: [isabelle] Problems with code generation for the reals*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Sat, 27 Apr 2013 15:03:15 +0200*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>, Johannes Hoelzl <hoelzl at in.tum.de>*In-reply-to*: <CAL0S8BfPE0=UT6e-zryCwvYqXaL99E7rNnbMZxnHUASJ4tFwig@mail.gmail.com>*Organization*: TU Munich*References*: <CAL0S8BfPE0=UT6e-zryCwvYqXaL99E7rNnbMZxnHUASJ4tFwig@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:17.0) Gecko/20130329 Thunderbird/17.0.5

Hi Jesus, > we were trying to generate code > for matrices of real numbers; we had been doing some experiments with > real numbers represented in SML by fractions of elements of type > "IntInf.int", but doing some profiling we detected that most of the > execution time was spent in computing the functions "gcd", "divmod", > "quotrem", "normalize" and so on, instead of on performing the > operations over matrices that were really interesting for us. > > We thought that giving a chance to Code_Real_Approx_By_Float could be > worth (even if we read about its potential accuracy matters), just to > see if we could reduce computing times of the arithmetic operations. > > Unfortunately, we got some problems with the Library, when generating > code, that we don't know how to avoid. The sort answer: insert the following snippet at the beginning of your example theory: > code_const Ratreal (SML) > > definition Realfract :: "int ⇒ int ⇒ real" > where > "Realfract p q = of_int p / of_int q" > > code_datatype Realfract > > code_const Realfract > (SML "Real.fromInt _/ '// Real.fromInt _") > > lemma [code]: > "Ratreal r = split Realfract (quotient_of r)" > by (cases r) (simp add: Realfract_def quotient_of_Fract of_rat_rat) > > lemma [code, code del]: > "(plus :: real ⇒ real ⇒ real) = plus" > .. > > lemma [code, code del]: > "(times :: real ⇒ real ⇒ real) = times" > .. > > lemma [code, code del]: > "(divide :: real ⇒ real ⇒ real) = divide" > .. > > lemma [code]: > fixes r :: real > shows "inverse r = 1 / r" > by (fact inverse_eq_divide) Code_Real_Approx_By_Float seems indeed to be very approximative since it cannot handle real numerals. This snippet amends this by a specific datatype constructor Realfract which is then mapped to a SML expression. This renders all code equations using the original datatype constructor Ratreal invalid, and they must be dropped explicitly using the funny [code, code del] pattern on reflexive equations. I added only the ones necessary for your examples, their might be more. Inversions seems not be implemented in Code_Real_Approx_By_Float, but it can be easily delegated to division on reals which is. @Johannes: Maybe this stuff should be added to Code_Real_Approx_By_Float? > In the file there can be also found some definitions from the SML > structure "Vector" (or type iarray, in Isabelle); we read your comment > on http://isabelle.in.tum.de/library/HOL/HOL-Library/IArray.html and > thought that the functions might be useful for someone else. This is indeed work by Tobias. I did not experience any problem with it in your examples. To get back to your original observation: > we had been doing some experiments with > real numbers represented in SML by fractions of elements of type > "IntInf.int", but doing some profiling we detected that most of the > execution time was spent in computing the functions "gcd", "divmod", > "quotrem", "normalize" and so on, instead of on performing the > operations over matrices that were really interesting for us. It is indeed questionable whether it is a good idea to normalize quotients always. What do others implementations do here (e.g. Ocaml)? The implementation of rational numbers can be changed in user space using the usual mechanisms of datatype refinement (see the tutorial on code generation and the upcoming ITP paper http://isabelle.in.tum.de/~haftmann/pdf/data_refinement_haftmann_kuncar_krauss_nipkow.pdf). Hope this helps, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Problems with code generation for the reals***From:*Jesus Aransay

- Previous by Date: [isabelle] ACL2 2013 - Call for Participation
- Next by Date: Re: [isabelle] Problems with proof terms
- Previous by Thread: [isabelle] ACL2 2013 - Call for Participation
- Next by Thread: Re: [isabelle] Problems with code generation for the reals
- Cl-isabelle-users April 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list