*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] Target language bindings for rat*From*: Jose DivasÃn <jose.divasonm at unirioja.es>*Date*: Fri, 18 Dec 2015 13:56:16 +0100*Cc*: Jose DivasÃn <jose.divasonm at unirioja.es>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <5673EC8F.6050708@inf.ethz.ch>*References*: <mailman.3044.1450352332.9047.cl-isabelle-users@lists.cam.ac.uk> <82F0C6E8-11A1-4904-9FBD-6E4604F380BD@email.gwu.edu> <C386445D0EDF694D9093DF78925C0ABA3714C2FC@MBX23.d.ethz.ch> <5673C404.4090301@in.tum.de> <5673D45F.5010808@inf.ethz.ch> <CA+MUZ5utu6KHOYbMjT3+MR7aLRUpPdesW=R-S81R_mgj_RYyMw@mail.gmail.com> <5673EC8F.6050708@inf.ethz.ch>*Sender*: jose.divason at gmail.com

> I was also a bit surprised by your comparison of serialisation options for > divmod_integer in Code_Generation_IArrays_SML. In SML, quotRem and divMod > behave differently when it comes to negative numbers. In that respect, > quotRem is the wrong choice. For example, > quotRem (~10, 6) evaluates to (~4, ~6) and divMod (~10, 6) to (~2, 2). In > Isabelle/HOL, > value [nbe] "divmod_integer (-10, 6)" gives (-2, 2). So the generated code > may actually return a different result than what you have proved. (I do not > know whether such negative numbers can occur in your application). > I think it works for my concrete case (integer numbers are only used for representing rational numbers), however for a general integer manipulation this is not a correct serialisation. In my exported code, quot is only used when nomalising rational numbers (by means of the Rat.normalise definition). If I am not wrong, for such a function it is the same using "div" as using "quot". So, "-20 div 6" would return different results (as expected), but normalize (-20,6) the same: code_printing constant "op div :: integer => _ => _" â (SML) "(IntInf.div ((_), (_)))" | constant "op mod :: integer => _ => _" â (SML) "(IntInf.mod ((_), (_)))" value[code] "-20 div 6::int" (*Result: - 4*) value[code] "Rat.normalize (-20,6)" (*Result: (-10,3) :: "int Ã int"*) code_printing constant "op div :: integer => _ => _" â (SML) "(IntInf.quot ((_), (_)))" | constant "op mod :: integer => _ => _" â (SML) "(IntInf.rem ((_), (_)))" value[code] "-20 div 6::int" (*Result: - 3 :: "int"*) value[code] "Rat.normalize (-20,6)" (*Result: (-10,3) :: "int Ã int"*) Then, I took advantage of it and decided to use quot, since it is supposed to be faster. Nevertheless, I have to study it carefully again because maybe I am wrong. Best, Jose

**Follow-Ups**:**Re: [isabelle] Target language bindings for rat***From:*Andreas Lochbihler

**References**:**Re: [isabelle] Target language bindings for rat***From:*W. Douglas Maurer

**Re: [isabelle] Target language bindings for rat***From:*Lochbihler Andreas

**Re: [isabelle] Target language bindings for rat***From:*Manuel Eberl

**Re: [isabelle] Target language bindings for rat***From:*Andreas Lochbihler

**Re: [isabelle] Target language bindings for rat***From:*Jose DivasÃn

**Re: [isabelle] Target language bindings for rat***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Target language bindings for rat
- Next by Date: Re: [isabelle] Target language bindings for rat
- Previous by Thread: Re: [isabelle] Target language bindings for rat
- Next by Thread: Re: [isabelle] Target language bindings for rat
- Cl-isabelle-users December 2015 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