*To*: Peter Lammich <lammich at in.tum.de>*Subject*: Re: [isabelle] Efficient_Nat and Imperative-HOL, strange import-order dependent bug*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Mon, 24 Jun 2013 16:52:42 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*In-reply-to*: <1372077392.2370.13.camel@lapbroy33>*References*: <1372077392.2370.13.camel@lapbroy33>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130510 Thunderbird/17.0.6

Hi Peter,

code_type code_numeral (Scala "Natural")

code_type code_numeral (Scala "BigInt")

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

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

- Previous by Date: Re: [isabelle] Latex without proofs
- Next by Date: Re: [isabelle] Efficient_Nat and Imperative-HOL, strange import-order dependent bug
- Previous by Thread: [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