Email Gateway (Aug 18 2022 at 17:36): Email Gateway (Aug 18 2022 at 17:36):From: Lukas Bulwahn <bulwahn@in.tum.de>
Hi everyone,
in a private discussion with Andreas Lochbihler and Florian Haftmann, we
have noticed that we should split the theories for data structures in
HOL-Library (currently: RBT_Impl, RBT, AssocList, DList, CSet, Mapping)
into more fine-grained theories.
If you require the implementation of one data structure, but you want to
connect an abstract type with other data structure,
the code equations must be manually deleted for one and added for the
other because implementation and their connection to abstract type are
within the same theory you would import from the Library.
Therefore, we propose the following naming scheme:
-- theories name of the representation types would end on "Impl", short
for implementation.
-- theories that define the invariant-ensuring type and lift operations
have no suffix in its theory name.
-- theories that connect the invariant-ensuring type and the abstract
type are named by the scheme <invariant-ensuring type>_<abstract type>.
This would result in the following renamings:
for Red-Black trees: RBT_Impl remains RBT_Impl. RBT is split into RBT
and RBT_Mapping.
for association lists: AssocList is split into AssocList_Impl and
AssocList_Mapping. [AssocList is removed because AssocList has no
invariant-ensuring type (yet).]
for distinct lists: DList is split into DList_Impl, DList, and DList_Cset.
for computable sets: Cset is split into Cset and List_Cset.
This way, the different layers are clearly separated in different theories.
For most users, this would mainly be noticed one would have to import,
e.g., RBT_Mapping, instead of RBT to get executable Mappings based on
red-black trees.
Any thoughts?
Lukas
Last updated: Apr 25 2024 at 16:19 UTC