From: "Max W. Haslbeck" <max.haslbeck@gmx.de>

Hi,

Consider the following .thy file (I’m using Isabelle2020 and an up to date AFP-2020 (rev: c645808bafa7)):

```
theory Scratch
imports
"HOL-Library.Numeral_Type"
"Containers.Containers"
begin
definition card_test :: "'a set ⇒ nat" where
"card_test = card"
export_code card_test in Haskell module_name Test
end
```

The generated Haskell module Test.hs contains the following code equations:

```
…
card :: forall a. (Card_UNIV a) => Set a -> Nat;
card = card;
card_test :: Set Nat -> Nat;
card_test = card;
...
```

The programming language chosen in the `export_code`

command doesn’t seem to matter. You will get also get a broken definition of `card`

. Removing one of the two imports leads to working exported code. Importing `HOL-Library.Cardinality`

(which is the only import of `HOL-Library.Numeral_Type`

) instead of `HOL-Library.Numeral_Type`

also leads to working code equations.

This problem came up when working with IsaFoR. IsaFoR uses Containers for code export and imports `HOL-Library.Numeral_Type`

[1,2] at some point by importing AFP/Collections.

Any help or pointers on what’s going on here would be appreciated.

Gruß

Max

[1]: http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/e4b1e20b0880/thys/Proof_Checker/Container_Setup.thy <http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/e4b1e20b0880/thys/Proof_Checker/Container_Setup.thy>

[2]: Container_Setup -> TA.Tree_Automata_Det_Container -> TA.Tree_Automata_Det_Impl -> TA.Tree_Automata_Wit_Impl -> TA.Tree_Automata_Autoref_Setup -> Collections.Refine_Dflt -> Collections.GenCF -> Collections.Impl_Array_Hash_Map -> "Collections.HashCode" -> "Native_Word.Uint32" -> "Native_Word.Code_Target_Word_Base" -> "HOL-Word.Word" -> "HOL-Library.Type_Length" -> "HOL-Library.Numeral_Type"

From: "Max W. Haslbeck" <max.haslbeck@gmx.de>

Hi,

Consider the following .thy file (I’m using Isabelle2020 and an up to date AFP-2020 (rev: c645808bafa7)):

```
theory Scratch
imports
"HOL-Library.Numeral_Type"
"Containers.Containers"
begin
definition card_test :: "'a set ⇒ nat" where
"card_test = card"
export_code card_test in Haskell module_name Test
end
```

The generated Haskell module Test.hs contains the following code equations:

```
…
card :: forall a. (Card_UNIV a) => Set a -> Nat;
card = card;
card_test :: Set Nat -> Nat;
card_test = card;
...
```

The programming language chosen in the `export_code`

command doesn’t seem to matter. You will get also get a broken definition of `card`

. Removing one of the two imports leads to working exported code. Importing `HOL-Library.Cardinality`

(which is the only import of `HOL-Library.Numeral_Type`

) instead of `HOL-Library.Numeral_Type`

also leads to working code equations.

This problem came up when working with IsaFoR. IsaFoR uses Containers for code export and imports `HOL-Library.Numeral_Type`

[1,2] at some point by importing AFP/Collections.

Any help or pointers on what’s going on here would be appreciated.

Gruß

Max

[1]: http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/e4b1e20b0880/thys/Proof_Checker/Container_Setup.thy <http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/e4b1e20b0880/thys/Proof_Checker/Container_Setup.thy>

[2]: Container_Setup -> TA.Tree_Automata_Det_Container -> TA.Tree_Automata_Det_Impl -> TA.Tree_Automata_Wit_Impl -> TA.Tree_Automata_Autoref_Setup -> Collections.Refine_Dflt -> Collections.GenCF -> Collections.Impl_Array_Hash_Map -> "Collections.HashCode" -> "Native_Word.Uint32" -> "Native_Word.Code_Target_Word_Base" -> "HOL-Word.Word" -> "HOL-Library.Type_Length" -> "HOL-Library.Numeral_Type"

From: Andreas Lochbihler <mail@andreas-lochbihler.de>

Dear Max,

Thanks for the report. Containers non-monotonically changes the code setup for card,

finite and Set.member. However, HOL-Library.Numeral_Type imports HOL-Library.Cardinality

and therefore all the code declarations from Cardinality are back in place. You'd have to

manually remove the offending declarations after the theories have been joined, e.g. with

the following

lemma [code_unfold del, symmetric, code_post del]:

"x ∈ set xs ≡ List.member xs x"

by(simp add: List.member_def)

lemma [code_unfold del, symmetric, code_post del]:

"finite ≡ Cardinality.finite'" by(simp)

lemma [code_unfold del, symmetric, code_post del]:

"card ≡ Cardinality.card'" by simp

Unfortunately, there's not much I can do about this right now due to how code equations

are merged when theories are joined. You'll just have remove those equations again and again.

Hope this helps

Andreas

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>

If your applications needs both those sessions with a conflicting code

setup, it's best to provide your individual theory within your

application session which joins the code setup as seen above and base

your application entirely on that theory.

Hope this helps,

Florian

signature.asc

Last updated: Dec 05 2021 at 23:19 UTC