Email Gateway (Jul 25 2022 at 08:21): Email Gateway (Jul 25 2022 at 08:21):From: "Achim D. Brucker" <adbrucker@0x5f.org>
Dear all,
I do not fully understand the behaviour of the theory
HOL-Library.Code_Real_Approx_By_Float. Consider the following
two theories:
theory ExampleDef imports Complex_Main begin
definition f:: "real => real" where "f x = exp(x) * 2.0"
end
and
theory ExampleCode imports
"HOL-Library.Code_Real_Approx_By_Float" ExampleDef
begin
definition g:: "real => real" where "g x = exp(x) * 2.0"
export_code g checking SML (* only works w/o importing ExampleDef *)
export_code f checking SML (* does not work *)
end
The first export_code (of the locally defined constant g) in the
theory ExampleCode only works the theory ExampleDef is not
included. The second export_code (of the constant f defined in the
imported theory ExampleDef) does not work at all.
I had a closer look at the theory HOL-Library.Code_Real_Approx_By_Float
and the problem seems to be two-fold:
1) the type "unwrapping" if integers (from Arith.int to IntInf.int) is
missing in the code printing of Realfract
2) the ML structure Real is overwritten by the generated code
The following patch seems to solve the problem:
https://hg.logicalhacking.com/isabelle/rev/91cdf474b64d
The patch declares Real as reserved word for the code generator and
introduces a "wrapper" Realfract' for the actual Realfract, which seems
sufficient to convince the code generator to generate the necessary type
conversions.
Best,
Achim
PS: I am fully aware of the risks of approximating reals by machine floats
but having a working code generator (and value) has proven to be
a key success factor in introducing Isabelle to students with little to
no previous exposure to theory ...
Last updated: Oct 30 2025 at 20:23 UTC