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
