Email Gateway (Aug 19 2022 at 11:47): Email Gateway (Aug 19 2022 at 11:47):From: Peter Lammich <lammich@in.tum.de>
Referring to Isabelle_12_Sep_2013:
When using Code_Target_Numeral instead of the old Efficient_Nat, the
code generator wraps some funny dummy-datatype (nat = Nat of int) around
my natural numbers. For one of my benchmarks (heavy use of arrays in
Imperative-HOL) this results in doubling the runtime under PolyML. Under
mlton, its only around 15% slower.
What was the reason behind this change, and is there a way to produce
code working with plain IntInf?
Email Gateway (Aug 19 2022 at 11:47):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Peter,
Until Isabelle2013, Code_Numeral.thy defined a type copy of the naturals and translated
them to arbitrary-precision integers in the target languages. As the latter also include
the negative numbers, this is not a perfect fit. Florian changed this: now, Code_Numeral
defines the type integer as a type copy of int and maps it to the target language integers
-- and Code_Target_Nat implements the nat type as a sub-type of integer. So, the
motivation was to get a cleaner setup of the code generator.
In many cases, such type copies do not affect performance, because the compiler can get
rid of such type copies after type checking. However, when they are nested into some other
polymorphic type, this is not always possible. Maybe, arrays fall into that class.
If you are free to choose which number to use, use Code_Numeral.integer instead of
Nat.nat. That will always be mapped to IntInf in SML. Alternatively, you can roll your own
setup following Isabelle2013's Code_Numeral and Efficient_Nat.
Best,
Andreas
Last updated: Apr 25 2024 at 01:08 UTC