Email Gateway (Aug 23 2022 at 09:15): Email Gateway (Aug 23 2022 at 09:15):From: "Max W. Haslbeck" <max.haslbeck@gmx.de>
Hi,
I have the following two theories in Isabelle/HOL with an up to date AFP-2020.
theory Test_Map1
imports
"HOL-Library.RBT_Mapping"
Containers.Containers
begin
export_code Mapping.ordered_keys
export_code RBT_Mapping in Haskell
end
and
theory Test_Map2
imports
Containers.Containers
"HOL-Library.RBT_Mapping"
begin
export_code Mapping.ordered_keys
export_code RBT_Mapping in Haskell
end
In theory 1 export_code Mapping.ordered_keys fails with
"RBT_Mapping.Mapping" is not a constructor, on left hand side of equation, in theorem:
Mapping.ordered_keys (RBT_Mapping.Mapping ?t) ≡ RBT.keys ?t
```.
In theory 2 `export_code RBT_Mapping in Haskell` fails with
No code equations for RBT_Mapping
The user guide for Containers in AFP [1] says to import Containers.Containers last. I can fix theory 1 by adding
lemma [code]: "Mapping.ordered_keys = sorted_list_of_set o Mapping.keys"
by (auto simp add: Mapping.ordered_keys_def)
before the code export.
So an update to Containers in the AFP could probably fix theory 1.
The problem came up when I wanted to export code in Isabelle/HOL using theories from IsaFoR and the AFP. Some
theories in IsaFoR and the AFP import RBT_Mapping and I use Mapping.ordered_keys in my theories. Therefore I ran
into the above problem.
Gruß
Max
[1]: https://www.isa-afp.org/browser_info/current/AFP/Containers/document.pdf
From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear Max,
Thanks for the report. Indeed, Containers in AFP 2020 doesn't provide an implementation
for the ordered_keys operation. In commit
https://foss.heptapod.net/isa-afp/afp-devel/-/commit/d5c01e7ecb2a098ffd0212b07362e345b31510ae,
I've now added code equations for further operations on mappings. (I didn't find the time
for binary operations like combine and combine_with_key where it is not clear which
implementation should be preferred.) You can probably back-port them to your copy of AFP
2020 or include them in your own theory until the next AFP release.
Best,
Andreas
Last updated: Nov 21 2024 at 12:39 UTC