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: Jul 15 2022 at 23:21 UTC