Email Gateway (Aug 22 2022 at 14:59): Email Gateway (Aug 22 2022 at 14:59):From: Manfred Kerber <mnfrd.krbr@gmail.com>
Dear All,
I use the type real in Isabelle and extract code to Scala. In an easy
example with
definition c1 :: real
where "c1 = 1.2"
I get in Isabelle with value c something that I can read immediately, namely
"6/5" :: "real".
However, when printing the extracted value in Scala via
println(c) I get something quite unreadable:
Ratreal(Frct((Pos(Bit0(Bit1(One()))),Pos(Bit1(Bit0(One()))))))
Is there an easy way to transform it to either 6/5 or to 1.2?
Many thanks,
Manfred
Email Gateway (Aug 22 2022 at 15:00):From: Tobias Nipkow <nipkow@in.tum.de>
On 27/01/2017 10:27, Manfred Kerber wrote:
Dear All,
I use the type real in Isabelle and extract code to Scala. In an easy
example withdefinition c1 :: real
where "c1 = 1.2"
Floating point numbers are just notation. When you look at the definition
thm c1_def
you'll see that 1.2 became 12/10.
I get in Isabelle with value c something that I can read immediately, namely
"6/5" :: "real".However, when printing the extracted value in Scala via
println(c) I get something quite unreadable:Ratreal(Frct((Pos(Bit0(Bit1(One()))),Pos(Bit1(Bit0(One()))))))
This is because reals are defined on top of nat and int and you inherit the
default binary notation. You can improve matters by importing
"~~/src/HOL/Library/Code_Target_Int". The Scala code now becomes
def c1: Real.real =
Real.divide_real(Real.Ratreal(Rat.of_int(Int.int_of_integer(BigInt(12)))),
Real.Ratreal(Rat.of_int(Int.int_of_integer(BigInt(10)))))
If you are brave, you could import
"~~/src/HOL/Library/Code_Real_Approx_By_Float" which sets up a logicallt unsound
translation to floats in the target language. Unfortunately, it has not been set
up for Scala, although that should be easy to add.
Tobias
Is there an easy way to transform it to either 6/5 or to 1.2?
Many thanks,
Manfred
Last updated: Apr 19 2024 at 12:27 UTC