[isabelle] AFP/Containers, "HOL-Library.Numeral_Type", co... · Mirror: Isabelle Users Mailing List

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] AFP/Containers, "HOL-Library.Numeral_Type", co...

Email Gateway (Aug 12 2020 at 12:00):

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"

Email Gateway (Aug 12 2020 at 12:04):

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;
...

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

Email Gateway (Aug 16 2020 at 12:15):

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

Email Gateway (Aug 16 2020 at 13:57):

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: Apr 19 2024 at 04:17 UTC