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



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.