[isabelle] code_datatype and theory merges



Dear all,

I stumbled over the following problem with code_datatype and theory merges. It involves 4 theories with diamond inheritance:

1. The first theory defines a type and a refined representation for code generation.

theory Scratch1 imports Main begin

typedef type = "UNIV :: int set"
  morphisms rep_Foo Foo
by blast

definition Bar where [code del]: "Bar n = Foo (n + 1)"
code_datatype Bar

lemma Foo_code [code]: "Foo n = Bar (n - 1)"
by(simp add: Bar_def)

end

2. The next theory Scratch2 changes the refinement such that Foo is the new constructor in the generated code and Bar is implemented in terms of Foo.

theory Scratch2 imports Scratch1 begin
declare Foo_code [code del]
code_datatype Foo
declare Bar_def [code]
end

3. Scratch3 does nothing but introduce an empty theory.

theory Scratch3 imports Scratch1 begin end

4. Scratch4 merges Scratch2 and Scratch3, the order is irrelevant for the following.

theory Scratch4 imports Scratch3 Scratch2 begin

(* This is where the trouble begins: The theory merge imports the code equation Bar_def declared in Scratch2 *and* Foo_code from Scratch, which is visible via Scratch3. *)

code_thms Bar

produces the following error:

*** Constructor as head in equation:
*** Foo ?n ==
*** Bar (minus_int_inst.minus_int ?n
***       (number_int_inst.number_of_int (Int.Bit1 Int.Pls)))
*** At command "code_thms"

Deleting the offending theorem Foo_code is not straight forward:

declare Foo_code [code del]
code_thms Bar

still gives the same error. To me, this looks like a bug in the code generator.
I found a way to get rid of the offending equation in Scratch4, but I don't consider this a reasonable solution:

code_datatype Bar
declare Foo_code [code del]
code_datatype Foo

Although the example is constructed, such weird hiearchies and code_datatype redeclarations do occur in practice. An example: Restore the code generator setup from HOL/Libray/Cset for Cset.set after loading HOL/Library/Dlist. By the way, this has been the reason for Lukas proposing to split the data structure theories in HOL/Library.

I'd be glad if anyone of the developers looked into this issue.

Andreas

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft





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