[isabelle-dev] NEWS: limited name space accesses
* 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
Re: [isabelle-dev] NEWS: limited name space accesses
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
Re: [isabelle-dev] NEWS: limited name space accesses
On 07/04/2015 14:37, Christian Sternagel wrote: (b) qualified That gets my vote because it expresses clearly the description Makarius gave: name space entry that is only accessible by qualified names Tobias smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: limited name space accesses
On Tue, 7 Apr 2015, Tobias Nipkow wrote: On 07/04/2015 14:37, Christian Sternagel wrote: (b) qualified That gets my vote because it expresses clearly the description Makarius gave: name space entry that is only accessible by qualified names It is definitely good to collect keyword candidates from other well-known languages. I had qualified on my list of possibilities at first, but was hesitating to use it, because there is yet another concept (c) that has no Isar notation so far. It is called Binding.qualified in ML and could solve problems like https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2015-February/msg00038.html as follows: locale test begin lemma foo (qualified bar!): ... end In principle there could be a dual-use of 'qualified' as Binding.qualified (with argument) and Name_Space.restricted (without argument), or rather Name_Space.qualified after another tuned signature change. qualified lemma a: ... lemma b (qualified c): ... lemma e (qualified f!): ... This does not work in outer syntax though, since the new command prefix category (keywords that may occur before a command) needs to be disjoint from other minor keywords in the command body. (After the dismissal of Proof General, command spans have become a bit more flexible, but cannot be stretched arbitrarily.) One could try to invent another notation for x (qualified y!) above. Note that the ! is the mandatory flag (like in locale interpretation syntax). We don't have notation for such flags within qualified names themselves. Otherwise one could use c.b directly. A real danger in the whole affair is that we need to proceed towards the Isabelle2015 release very soon, i.e. this week. As a summary, here is the collection of nice keywords so far, without any assignment of meanings yet: private local hidden qualified Anything else? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Local_Theory.open_target instead of Local_Theory.restore
Just a short note on Local_Theory.open_target (for Isabelle/83071f4c8ae6)
versus old uses of Local_Theory.restore.
Local_Theory.open_target is the internal version of context begin, where
Local_Theory.close_target is end. The ML signature is now a bit more
concise form than before. It has already been used successfully in
Eisbach, to lay out a local situation for the internal construction.
Here is a quick example that shows how to get polymorphic constants out of
local theory specifications, with such official context nesting:
context fixes x :: 'a
begin
declare [[show_types]]
ML_val ‹
val lthy = @{context};
val (_, lthy1) = lthy | Local_Theory.open_target;
val ((t, (_, th)), lthy2) = lthy1
| Local_Theory.define ((@{binding c}, NoSyn), (Attrib.empty_binding, @{term
λy. x}));
val lthy3 = lthy2 | Local_Theory.close_target;
val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy3);
val th' = th | singleton (Proof_Context.export lthy2 lthy3);
val th'' = th' | singleton (Proof_Context.export lthy3 thy_ctxt);
writeln (Display.string_of_thm lthy2 th); (*monomorphic*)
writeln (Display.string_of_thm lthy3 th'); (*partly polymorphic*)
writeln (Display.string_of_thm thy_ctxt th''); (*fully polymorphic*)
›
Thus the brute-force Local_Theory.restore is avoided, which only works
properly at the boundary of local theory command transactions anyway.
Eliminating Local_Theory.restore is one of these continuous reform
projects that can be done now or later. Note that it would also achieve
better results for private datatype, because Local_Theory.restore
disrupts the continuity of the naming policy.
It is up to the BNF guys to say if they intend to do something for the
Isabelle2015 release, or just leave the status quo. It is unlikely that
anybody will notice fine points of private datatype definitions before the
next release after Isabelle2015.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Local_Theory.open_target instead of Local_Theory.restore
Hi Makarius,
thanks, this is the hint I was looking for a long time now.
I will do the replacement in the BNF package, but I don't think that I
will have time for it before the approaching release.
Dmitriy
On 07.04.2015 17:47, Makarius wrote:
Just a short note on Local_Theory.open_target (for Isabelle/83071f4c8ae6)
versus old uses of Local_Theory.restore.
Local_Theory.open_target is the internal version of context begin,
where Local_Theory.close_target is end. The ML signature is now a
bit more concise form than before. It has already been used
successfully in Eisbach, to lay out a local situation for the internal
construction.
Here is a quick example that shows how to get polymorphic constants
out of local theory specifications, with such official context nesting:
context fixes x :: 'a
begin
declare [[show_types]]
ML_val ‹
val lthy = @{context};
val (_, lthy1) = lthy | Local_Theory.open_target;
val ((t, (_, th)), lthy2) = lthy1
| Local_Theory.define ((@{binding c}, NoSyn),
(Attrib.empty_binding, @{term λy. x}));
val lthy3 = lthy2 | Local_Theory.close_target;
val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of
lthy3);
val th' = th | singleton (Proof_Context.export lthy2 lthy3);
val th'' = th' | singleton (Proof_Context.export lthy3 thy_ctxt);
writeln (Display.string_of_thm lthy2 th); (*monomorphic*)
writeln (Display.string_of_thm lthy3 th'); (*partly polymorphic*)
writeln (Display.string_of_thm thy_ctxt th''); (*fully polymorphic*)
›
Thus the brute-force Local_Theory.restore is avoided, which only works
properly at the boundary of local theory command transactions anyway.
Eliminating Local_Theory.restore is one of these continuous reform
projects that can be done now or later. Note that it would also
achieve better results for private datatype, because
Local_Theory.restore disrupts the continuity of the naming policy.
It is up to the BNF guys to say if they intend to do something for the
Isabelle2015 release, or just leave the status quo. It is unlikely
that anybody will notice fine points of private datatype definitions
before the next release after Isabelle2015.
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
