*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Efficient_Nat and Imperative-HOL, strange import-order dependent bug*From*: Peter Lammich <lammich at in.tum.de>*Date*: Mon, 24 Jun 2013 18:02:54 +0200*In-reply-to*: <51C85D3A.5000709@inf.ethz.ch>*References*: <1372077392.2370.13.camel@lapbroy33> <51C85D3A.5000709@inf.ethz.ch>

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 > > > >

**Follow-Ups**:**Re: [isabelle] Efficient_Nat and Imperative-HOL, strange import-order dependent bug***From:*Florian Haftmann

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

**References**:**[isabelle] Efficient_Nat and Imperative-HOL, strange import-order dependent bug***From:*Peter Lammich

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

- Previous by Date: Re: [isabelle] Efficient_Nat and Imperative-HOL, strange import-order dependent bug
- Next by Date: Re: [isabelle] Efficient_Nat and Imperative-HOL, strange import-order dependent bug
- Previous by Thread: Re: [isabelle] Efficient_Nat and Imperative-HOL, strange import-order dependent bug
- Next by Thread: Re: [isabelle] Efficient_Nat and Imperative-HOL, strange import-order dependent bug
- Cl-isabelle-users June 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list