Re: [isabelle] Efficient_Nat and Imperative-HOL, strange import-order dependent bug



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

On Mo, 2013-06-24 at 16:52 +0200, Andreas Lochbihler wrote:
> 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
> 
> 
> 
> 
> On 24/06/13 14:36, Peter Lammich wrote:
> > There seems to be a strange dependency between
> > Efficient_Nat and the import order of totally unrelated theories.
> >
> > As an example, consider the following theories:
> >
> >
> > theory A
> > imports Main
> > begin
> > end
> >
> > theory Scratch
> > imports
> >    "~~/src/HOL/Library/Efficient_Nat"
> >    "~~/src/HOL/Imperative_HOL/Imperative_HOL"
> >    A
> > begin
> >
> >    export_code Unity Array.len in Scala_imp file -
> >
> >
> > Produces:
> >
> >    [...]
> > def len[A : Heapa.heap](a: collection.mutable.ArraySeq[A]): Unit => Nat =
> >    (b: Unit) =>
> >      {
> >        val (): Unit = b
> >        val i: BigInt = ((_: Unit) => Array.len(a)).apply(());
> >        Nat(i.as_BigInt)
> >      }
> >
> >    [...]
> >
> >
> > which is a type-error, as Array.len returns a "Natural", not a "BigInt".
> >
> > However, when removing the import of A, or moving it up, the generated
> > code correctly becomes:
> >
> >
> >
> >    def len[A : Heapa.heap](a: collection.mutable.ArraySeq[A]): Unit => Nat =
> >    (b: Unit) =>
> >      {
> >        val (): Unit = b
> >        val i: Natural = ((_: Unit) => Array.len(a)).apply(());
> >        Nat(i.as_BigInt)
> >      }
> >
> >
> > For Scala code generation, this is a real showstopper! Fortunately, this
> > problem seems not to occur for SML.
> >
> > What is happening here. Why does the import order wrt an *empty* theory
> > change the output of the code generator?
> > And how to fix the problem, which rules for imports do I have to follow
> > in order to avoid this problem?
> >
> >
> > Best,
> >    Peter
> >
> >






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.