Am 26.05.2014 um 14:28 schrieb Andrei Popescu <uuo...@yahoo.com>:
> I have the following proposal:
>
> (1) Hide all the extra structure from the user if it is not required
> explicitly.
>
> (2) Make parts of this structure visible upon request by "get" commands that
> specify the target datatype and the desired
> components, which can be issued at any time (not necessarily immediately)
> after the datatype definition. Something like:
>
> datatype 'a list = Nil | Cons 'a "'a list"
>
> ...
>
> getSelector isNil for Nil[list]
>
> Then novices will first get a chance to experiment with defining their own
> selectors, set, map, etc. before they are shown
> how to get them for free.
Do I understand you correctly that you are volunteering to implement this?? I
wish you good luck, to derive theorems like "sel_map" etc. on a per-need basis.
It's certainly doable, but would be an architectural nightmare.
Seriously: We've had a discussion after lunch. We haven't agreed on a concrete
syntax, but some elements have emerged:
1. The squiggles (-: and =:) are easy to get rid of, and we'll kill them. This
has been discussed before.
2. We'll try to move (map: ... rel: ...) out of the way, e.g. by putting them
after the definition rather than before.
3. Similar story for the set function (set: 'a), even though it's a bit painful
in the general case (with, say, ten type variables and five mutually recursive
types -- cf. IsaFoR).
4. The selector syntax seems acceptable to most of not all parties. Some of us
even love it. Also important is that readers are usually smart enough to infer,
from the names of the things, what is meant (e.g. "hd" and "tl" for a list have
to be the selectors).
5. The discriminators are a bit more iffy, and could perhaps be labeled more
clearly, e.g. with a pseudo-keyword "discriminator". On the other hand, they're
not needed for "list" and "option", and the default name (is_C for constructor
C) is good.
6. The default values for, e.g. "tl [] = []", could be specified as equations
after the definition (e.g. in a "where" clause), as suggested one year ago by
Andreas L.
One scheme that appeared promising as a compromise is to specify replacement
names at the end of the definition, e.g.
with
map := map_list
set := set_list
list_all2 := rel (* ugly name BTW -- maybe*)
This scales gracefully to the mutual case.
I'll do step 1 now, and we can give ourselves more time to think about 2 to 6.
Jasmin
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
