Dear Florian,
On 05/30/2013 06:03 AM, Florian Haftmann wrote:
Hi Christian,
- 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.
I think Adhoc_Overloading.setup should stay theory -> theory: this is
the installation of the necessary syntax check phases, which is done
once globally on import of the corresponding theory – unlike the dynamic
addition via add_overloaded and add_variant
Sorry, my question should have been: how to apply a function of type
"Generic.context -> Generic.context" in a situation where "theory ->
theory" is expected (the former type comes from using Generic_Data, and
the latter is what "setup" should have). In the meanwhile I found
Context.theory_map: (Context.generic -> Context.generic) -> theory ->
theory
Alternatively, use Context.>> directly in the body of the ML file
(which, I guess, is nowadays preferred over explicit setup in the
surrounding theory).
Thanks for the hint. I'm now using "Context.>>" instead of a setup
function called from a thy-file.
- 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:
It depends how far you want to push the game.
* The simplest one I can imagine is to stay on the »constant as string«
level, but have declarations within local theories; if these would be
morphed e.g. due to interpretation, they would only be kept if their
resulting shape is again a constant.
* Treat one component as general term appropriately (maybe the variant?).
* Treat both components as general term appropriately.
My naive approach was to just turn the previous Symtabs into Termtabs,
i.e., previously:
internalize : (string * typ) list Symtab.table
(*maps overloaded constants to lists of variants (together with their
type)*)
externalize : string Symtab.table
(*maps variants to corresponding overloaded constants*)
(An aside: I'm leaning towards renaming those two tables and related
functions as follows:
internalize ~> variant_tab
externalize ~> oconst_tab
which would make more sense to me, but maybe the old naming has a
Isabelle-specific reason I'm not aware of?)
As a first attempt I just changed this into
variant_tab : term list Termtab.table (*we can get the type of a term*)
oconst_tab : term Termtab.table
But of course that is not what I intended, since types are now also
inspected when looking up a key in a table, but at least for overloaded
constants only their name is important. This seems to point towards one
of your first two suggestions. The first one, would require the least
amount of changes (and would allow to print readable error messages).
The question is whether I'm asking for problems, when I treat "Free"
variables (i.e., "constants" in local theories) and "Const"s both as
strings? Any opinions?
A related question. Until now I can only register overloaded constants
and variants via the ML interface, since the "adhoc_overloading" command
I implemented does not seem to effect the surrounding theory. I will
have a look at "notation" again to see how functions of type
"local_theory -> local_theory" are able to make "non-local" changes
persistent, i.e., update the tables in my Generic_Data. Maybe somebody
does already have suggestions in that respect?
cheers
chris
* 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)
Good question. Note that most »fully localized« data store prefer
Item_Net.T as store index, where merge always seems to prefer on branch
(I only did skim over the sources, so this conclusion might be erroneous).
* 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?
It should work, with the usual problems on the theory level that things
deleted in one theory come up again after merge with another theory with
partly shared but different ancestry.
- 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?
Maybe \<rightharpoonup> / => similar to existing syntax things=
- 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?
I have no particular idea about that.
Cheers,
Florian
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
