Very nice!
I'll wait until the naming issue is settled before replacing my many
uses of "hide_const (open) ...".
A further naming suggestion:
(a) private/hidden
(b) qualified
the latter is akin to Haskell's "qualified" import.
cheers
chris
PS: I'm still waiting for
isabelle build -n -a -d '$AFP' -k qualified
to finish (but I guess proper checking, taking semantics into account,
is just expensive). Oops, while writing this email I obtained:
*** java.lang.OutOfMemoryError: Java heap space
0:03:32 elapsed time, 0:05:46 cpu time, factor 1.63
(Maybe because in parallel I am still waiting on
isabelle build -v -n -a -d '$AFP' -k hidden -k private
? Which seems to "hangs" at "Session Pure/RAW" now for several minutes.)
On 04/07/2015 02:07 PM, Makarius wrote:
* Local theory specification commands may have a 'private' or
'restricted' modifier to limit name space accesses to the local scope,
as provided by some "context begin ... end" block. For example:
context
begin
private definition ...
private definition ...
private lemma ...
lemma ...
lemma ...
theorem ...
end
This refers to Isabelle/83071f4c8ae6.
After more than 10 years in the pipeline, and never-ending efforts to
localize almost all tools, there is now the long anticipated limitation
of name space accesses. There are presently two example applications:
(1) Local tool setup with some auxiliary constants: "induct_forall" etc.
in
http://isabelle.in.tum.de/repos/isabelle/file/83071f4c8ae6/src/HOL/HOL.thy#l1377
(2) Plain specifications that are meant to produce theory-qualified
names: AList.update etc. in
http://isabelle.in.tum.de/repos/isabelle/file/e83ecf0a0ee1/src/HOL/Library/AList.thy#l11
I am still not 100% sure about the choice of keywords. There are two
concepts that are supported: (a) totally inaccessible name space entry,
(b) name space entry that is only accessible by qualified names, not the
base name.
Presently we have:
(a) 'private'
(b) 'restricted'
I first started out implementing 'private' for the sake of Eisbach,
which really needs that. Then I noticed that in practice one mostly
uses 'restricted' to eliminated old "hide (open)", but this keyword is a
bit awkward.
Here are some possible alternatives:
(a) 'hidden' (like Long_Name.hidden according to Isabelle/ML
terminology)
(b) 'private' (like 'private' in Java/Scala, in non-serious mode)
or:
(a) 'private' (like 'private' on Java/Scala in serious mode)
(b) 'local' (like an ancient Isabelle command of that name)
By non-serious mode I mean the rather easy way to bypass 'private'
declarations on the JVM via reflection. Likewise our logical
environment always allows to access inaccessible names, after some
tweaking of the name space, e.g. via aliases. This could justify the
use of 'private' for what is now 'restricted', or it might be just too
confusing to users.
Note that it is now releatively easy to test feasibility of new keywords
like this:
$ isabelle build -n -a -d '$AFP' -k hidden -k local
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
