Email Gateway (Aug 18 2022 at 19:06): Email Gateway (Aug 18 2022 at 19:06):From: Thomas Genet <Thomas.Genet@irisa.fr>
Dear Isabelle Users,
I am looking for the equivalent of "Efficient_nat" but for integers,
leading to exported code that uses machine integers rather than a term
representation.
Best regards,
Thomas
Email Gateway (Aug 18 2022 at 19:06):From: Tobias Nipkow <nipkow@in.tum.de>
I believe Library/Code_Integer is what you need to load.
Tobias
Email Gateway (Aug 18 2022 at 19:06):From: Tobias Nipkow <nipkow@in.tum.de>
PS No, you don't get machine integers, that would be unsound. You get
big integers, which are language specific. I assume that in most of the
languages we support big integers are like machine integers plus some
fixed overhead, as long as you stay in the machine integer range.
Email Gateway (Aug 18 2022 at 19:06):From: Thomas Genet <Thomas.Genet@irisa.fr>
Thanks a lot Tobias, this is even better that what I expected!
Thomas
Email Gateway (Aug 18 2022 at 19:07):From: Filip Maric <filip@matf.bg.ac.rs>
Hello,
although it is generally unsound, is there still a simple way to get
machine integers?
I have an application that uses only positive integers between 0 and 2^12
and the only operation performed on these numbers is bitwise disjunction
(which leaves them in this range). In the logic, I used the nat type and
define the bit-or using div/mod, but, of course, this is very slow when
executed (proof checking takes almost half an hour since there is a lot
computation involved). Since the range is bounded, there is a
"meta-theoretic" argument that machine integers would not introduce
unsoundness, so I wonder if it is possible to "cheat" and use them and
instruct the code generator to call the target-language bit-or in place of
my div/mod defined bit-or (I tried something like code_const "bitor" (SML
"IntInf.orb ((_), (_))") (Haskell infixl 6 "(.|.)"), but it did not give
expected efficiency since big integers are used). Evaluations are used
within a "proof-by-evaluation" paradigm and I use the method "by eval".
I suppose the other option would be not to use nats but machine words in
the logic level, but then the formalization would be a bit more
complicated, and I not sure what theory I should start from (I assume
there is such a formalization in the Library)?
Thank you very much,
Filip
Email Gateway (Aug 18 2022 at 19:07):From: Tobias Nipkow <nipkow@in.tum.de>
You can do anything you want, at your own risk, if you modify what the
code generator turns a certain type into. See the code generation
documentation and see what Code_Integer does.
Tobias
Email Gateway (Aug 18 2022 at 19:07):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Filip,
if you really only need disjunction, I would recommend the following:
define your own type for positive integers between 0 and 2^12;
HOL/Library/Dlist.thy (among others) is a helpful example to glimpse from
setup code generation for that type as sketched above.
There is a formalization of bit-arithmetic in HOL/Word, but it is not
very suitable to setup a customary code generation for specific target
languages because the bit length is encoded into a type argument, a
concept which cannot be mapped straighforwardly to target languages.
Hope this helps,
Florian
signature.asc
Last updated: May 06 2024 at 12:29 UTC