Hi Florian,
many issues have been touched in this thread, but I would like to get
back to the proposals made by Jasmin which IMHO point into the right
direction.
Thanks for your comments. The current syntax (as per dc0b4f50e288) is
datatype_new (set: 'a) list (map: map rel: list_all2) =
Nil (defaults tl: []) ([])
| Cons (hd: 'a) (tl: 'a list) (infixr # 65)
Moving things to the end could yield something like
datatype_new 'a list =
Nil ([])
| Cons (hd: 'a) (tl: 'a list) (infixr # 65)
where
hd [] = []
sets: set
map: map
rel: list_all2
(I got the OK from Tobias for keeping the selectors in there.)
For mutually recursive types, there could be one where per type -- but I
doubt that where and mutual recursions will often need to be combined anyway.
In the heat of the discussion, we might have forgotten that most datatypes
actually look quite good today, e.g.
datatype_new 'a option =
None
| Some (the: 'a)
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.
I have a slight feeling that syntax for selectors and discriminators
should be corresponding.
Good point. And since the default is reasonable (= C for nullary constructors
C, is_C otherwise), the syntax is rarely needed. (Andreas uses it for lnull
:: 'a llist = bool, though.)
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.
This is more verbose to parse, but it also quite common in Isar to
require propostions of a certain shape instead of (conceptually
isomorphic) fragments. A similar example are mixin equations in
interpretation statements.
Right. It is also easier to parse (and to get right as an author) for
constructors with arguments. See the example right at the end of Section 3 of
http://www21.in.tum.de/~blanchet/co-data-impl.pdf
if you want a taste of how unnatural default values can get. The default for
mid (Node2 x l r) is %x l r. r.
Actually, here I did not need much convincing. My main objection with the
equational scheme was that someone would need to implement it...
Jasmin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
