Email Gateway (Aug 19 2022 at 11:19): Email Gateway (Aug 19 2022 at 11:19):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Peter,
the code generator tutorial tells you that you should list theories at the end of the
imports list if they are adaptation theories for code generation like Efficient_Nat. Upon
processing the import list, Isabelle merges the theory data of all the imports in the
given list according to the merge operation of the theory data. If you now look at the
merge operation in src/Tools/Code/code_target.ML, you see that it always prefers later
imports. If you add the empty theory A at the end of the import list, all the imports that
A inherits from Main will overwrite those from Efficient_Nat and Imperative_HOL.
The code setup in Imperative_HOL requires that the type nat be mapped to Natural in Scala;
Heap_Monad therefore imports Code_Natural, which contains the following declaration:
code_type code_numeral (Scala "Natural")
This conflicts with the declaration from Code_Numeral that is valid in A (via the Main
import):
code_type code_numeral (Scala "BigInt")
Now, if you import A after Imperative_HOL and Efficient_Nat, the former's declaration wins
over the latter's and the type error manifests itself.
The whole trouble arises from a sloppy handling of target numerals in Isabelle2013. The
type code_numeral is isomorphic to nat, but implemented by arbitrary precision integers of
the target language (which also contain negative numbers). Code_Natural wraps these
target-language integers in a new type Natural for Haskell and Scala, but I don't know
why. In the development version, Florian has renovated the whole business with target
language numerals such that there are now separate types for all integers and non-negative
integers. This hopefully solves your problem in the next release although I have not tried
it yet.
Hope this helps,
Andreas
Email Gateway (Aug 19 2022 at 11:19):From: Peter Lammich <lammich@in.tum.de>
Hi.
Thanks, this helps understanding the problem.
It probably means that I have to restructure my theory tree such that
export_code is only performed in leave-theories, where I can safely
import Efficient_Nat. I only hope that Imperative_HOL does not make
changes that get overwritten, too, as this would mean that no non-leaf
theory could be based on Imperative_HOL.
Cheers,
Peter
Email Gateway (Aug 19 2022 at 11:19):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
This should not be the case.
Florian
signature.asc
Email Gateway (Aug 19 2022 at 11:20):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Peter,
It probably means that I have to restructure my theory tree such that
export_code is only performed in leave-theories, where I can safely
import Efficient_Nat.
No, you don't. For this particular case, just make sure that every theory with an
export_code imports Efficient_Nat at the end of its imports list. AFAIK, the merge is
performed even if some anchestor theory has already imported Efficient_Nat, so you can
always force the declarations from Efficient_Nat again.
I only hope that Imperative_HOL does not make
changes that get overwritten, too, as this would mean that no non-leaf
theory could be based on Imperative_HOL.
Efficient_Nat violates the locality principle, because it changes some setup of Isabelle
that can be accessed in other ways. Such non-monotonic changes result in non-trivial
merges and often cause trouble sooner or later. IIRC, Imperative_HOL respects locality in
that the whole setup is declared once and for all, so if everything is based on the single
entry point Imperative_HOL.thy, everything should be fine.
Andreas
Last updated: Apr 26 2024 at 08:19 UTC