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



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.