Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code export, Conflict between HOL-Library and ...


view this post on Zulip 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

view this post on Zulip Email Gateway (Aug 23 2022 at 09:18):

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: Mar 29 2024 at 01:04 UTC