Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] code_datatype and theory merges

Email Gateway (Aug 18 2022 at 17:37):

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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

Email Gateway (Aug 18 2022 at 17:40):

From: Lukas Bulwahn <bulwahn@in.tum.de>
On 04/21/2011 02:43 PM, Andreas Lochbihler wrote:

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.

This issue has been resolved by 42d607a9ae65 in the development version.

Lukas

Andreas

Last updated: Apr 26 2024 at 20:16 UTC