Email Gateway (Aug 18 2022 at 15:55): Email Gateway (Aug 18 2022 at 15:55):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all.
We have some theory A, that defines, among others, the functions:
foldl, foldr, insert
Inside A, and inside theories extending A, these names make perfectly
sense, and we do not want to change them to, say, "A_foldl".
However, some theories based on A are now to be used a bigger context,
where the details of A (including foldl, etc.) are no longer important.
Nevertheless, the constants remain defined and overwrite the standard
constants from List.thy and Set.thy, which is embarrassing.
What's the right solution to this problem?
I know the hide_const (open) construct, however, its annoying to
explicitly having to list all constants of the theory again (and perhaps
forgetting one).
Moreover, if the constants are hidden "too early", its impossible to use
them by unqualified names in theories extending A.
Alternatively, I thought of defining a locale:
locale A_loc begin
definition foldl, foldr, insert, ...
end
interpretation A: A_loc .
And proving extensions to A inside the locale.
The interpretation is required for code generation, as the code generator
seems not to generate code for "A_loc.foldl", etc.
Am I on the right track? Is there a simpler solution?
Best,
Peter
Email Gateway (Aug 18 2022 at 15:56):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Peter,
However, some theories based on A are now to be used a bigger context,
where the details of A (including foldl, etc.) are no longer important.
Nevertheless, the constants remain defined and overwrite the standard
constants from List.thy and Set.thy, which is embarrassing.
This sounds like the theory A and some of its descendents form some kind of
module, so I would suggest to set up a theory file of its own which specifies
the canonical entry point. Inside this "interface" theory, you can hide all
"internal" constants as with hide_const (open). If you want to access the
constants unqualified, you just have to do this in a theory whose imports bypass
the interface theory. However, this does not solve the problem of having to
explicitly hide every internal constant.
Alternatively, I thought of defining a locale:
locale A_loc begin
definition foldl, foldr, insert, ...
end
interpretation A: A_loc .And proving extensions to A inside the locale.
The interpretation is required for code generation, as the code generator
seems not to generate code for "A_loc.foldl", etc.
Note that the interpretation is executed only once, i.e. if you later add
definitions/code equations to locale A, they will not be carried through the
interpretation automatically. And, AFAIK, there is no way to force a
re-interpretation of A. If you want to go that way, I recommend that you do your
code generator setup manually by declaring all necessary equations OUTSIDE the
locale context as [code].
Am I on the right track? Is there a simpler solution?
If the constant that gets hidden is not visible at the point where the other
constant of the same name is defined, you could exploit the order of theory
merges. But this can make your developments very fragile and possibly hard to
maintain. Here is an example:
theory Foo imports Plain begin
definition foldl :: "nat" where "foldl = 0"
end
theory Bar imports Main Foo begin
-- "foldl now refers to Foo.foldl"
end
theory Bar2 imports Foo Main begin
-- "foldl now refers to List.foldl"
end
Another option is to abuse notation, which also allows to unhide the constant again:
theory Foo imports Main begin
definition foldl :: "nat" where "foldl = 0"
notation List.foldl ("foldl")
term "foldl" -- "List.foldl"
no_notation List.fold ("foldl")
term "foldl" -- "Foo.foldl"
end
Best,
Andreas
Email Gateway (Aug 18 2022 at 15:56):From: Makarius <makarius@sketis.net>
For tricks like this I recommend using 'abbreviation' instead, since it
does not spoil the token table of the syntax with literal "foldl" etc.
More hardcore manipulations can be done with name space aliases in
Isabelle2009-2, e.g. like this:
setup {* Sign.const_alias @{binding fold} @{const_name List.foldr} *}
hide_const List.foldr
term fold
term foldr -- "free variable"
Workarounds with aliases are not much worse than 'hide_const' etc. Of
course, we are all waiting for proper name space management at the level
of theory "modules", "packages", whatever. After a few more rounds of
"localization" of old packages we are getting closer and closer to that.
Makarius
Last updated: Apr 26 2024 at 08:19 UTC