In the meanwhile I had a first look at the implementation of the
"notation" command. Some things I noted w.r.t. localizing ad-hoc
overloading (please correct me if I'm wrong):
- For Overload_Data instead of Theory_Data, I should use Generic_Data
(such that it is available in top-level theories and local theories).
Currently that means that I do the following in the setup (where
Adhoc_Overloading.setup is now of type "Context.generic ->
Context.generic").
setup {* fn thy =>
Adhoc_Overloading.setup (Context.Theory thy)
Context.theory_of *}
This looks strange, I'm sure I'm doing something wrong / non-canonical.
- Apparently "constants" (in the sense of locally fixed variables of a
local theory) are represented as "term"s rather than "string"s (in the
notation command). In adhoc_overloading.ML, until now we used "string"s
to represent top-level constants. A change (if really necessary) implies
the following questions:
* How to print a "constant" represented as "term" in the error
messages inside Overload_Data (I do not see how I could access the
context here)
* I also would like to add the possibility to remove overloading and
variants again. Is that against some monotonicity requirement I'm not
aware of?
- Concerning syntax, I thought about providing commands like:
adhoc_overloading
bind bind_list bind_option and
permute permute_list permute_option
(which would declare "bind" and "permute" as ad-hoc overloaded and add
the variants "bind_list" and "bind_option", and "permute_list" and
"permute_option", respectively.) Maybe some punctuation between the
overloaded constant and its variant would increase readability?
Similarly there could be
no_adhoc_overloading
...
Any comments?
- In the check and uncheck functions I now would have to unify typed
terms instead of mere constants. Could that be too expensive to be
practicable?
Would anybody be interested in "formally" discussing and implementing
necessary changes to the existing implementation in a dedicated
mercurial repo on bitbucket?
cheers
chris
On 05/25/2013 03:28 AM, Makarius wrote:
On Fri, 24 May 2013, Christian Sternagel wrote:
Since I'm not too sure about the internals of local contexts, would
that make sense in principle?
Yes. According to the "local everything approach" from 2006, locality
is the normal situation unless there are very strong reasons against
it. In practice, non-locality is merely historic in most cases, and the
effort to get things to the normal local state is called "localization".
For the declarations of Adhoc_Overloading (add_overloaded, add_variant)
you merely need to address the usual questions what it means to
transform them via a morphism, and then apply the result to concrete
contexts in the applications. A usual starting point is to look how
existing similar mechanism do that, lets say notation that is associated
with "constant" terms.
A related question: what is the difference between
Syntax_Phases.term_check and Syntax_Phases.term_check'? Why does the
latter expect a function returning an option but not the former?
Syntax_Phases.term_check' allows full generality, with a functions that
indicates a stable situation by NONE, to represent identity explicitly.
The more common Syntax_Phases.term_check merely applies the given total
function and compares the visible part of the result (the types/terms)
to see if stability was achieved.
You need the "'" version in particular, when the context changes and not
just the types/term material, e.g. setting some flags that you have
"seen" a certain situation already.
And another one: assume we could do
consts FOO :: ... (<some syntax>)
setup {* Adhoc_Overloading.add_overloaded @{const_name FOO} *}
locale foo =
fixes foo :: ...
assumes ...
begin
local_setup {*
Adhoc_Overloading.add_variant @{const_name FOO} @{const_name foo}
*}
would the overloading only be active inside foo or would it also have
effects outside of this context (that are impossible to avoid due to
technical reasons)? Does it make sense at all to use the locally fixed
foo as a constant in the call to add_overloaded?
The local_setup above is technically a 'declaration' within the local
theory context (or other application contexts). The morphism that
transforms your original data from the immediate auxiliary context of
the local definition to the application context gives you some clues
about what to do, and when to give up the update of the context at hand.
(The latter needs to be done gracefully, without an error.)
As a start, I recommend to imitate 'notation' to some extent. (That is
itself not beyond reform, but that is another story.)
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
