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) =
I can only agree with what Makarius has observed but would go one step further:
the new definition of list is truly baroque and unsuitable for beginners, but
beginners are bound to look at it. Sometimes languages have to reduce complexity
to cater for novices. The three types bool, nat and list
On 26/05/2014 10:30, Tobias Nipkow wrote:
The three types bool, nat and list should be defined in
the plain standard manner.
Ignore the bit about bool and nat.
Tobias
___
isabelle-dev mailing list
isabelle-...@in.tum.de
Am 26.05.2014 um 10:30 schrieb Tobias Nipkow nip...@in.tum.de:
I can only agree with what Makarius has observed but would go one step
further:
the new definition of list is truly baroque and unsuitable for beginners, but
beginners are bound to look at it. Sometimes languages have to reduce
The definition of list should look like before.
Tobias
On 26/05/2014 10:59, Jasmin Christian Blanchette wrote:
Am 26.05.2014 um 10:30 schrieb Tobias Nipkow nip...@in.tum.de:
I can only agree with what Makarius has observed but would go one step
further:
the new definition of list is
Am 26.05.2014 um 11:02 schrieb Tobias Nipkow nip...@in.tum.de:
The definition of list should look like before.
I don't see how this is an option. This would result in the following duplicate
constants:
map_list vs. map
set_list vs. set
rel_list vs. forall_list2
un_Cons1 vs. hd
Am 26.05.2014 11:07, schrieb Jasmin Blanchette:
Am 26.05.2014 um 11:02 schrieb Tobias Nipkow nip...@in.tum.de:
The definition of list should look like before.
I don't see how this is an option. This would result in the following duplicate
constants:
map_list vs. map
set_list vs.
On Sun, 25 May 2014, Jasmin Christian Blanchette wrote:
(3) A genuine name space problem: list is concealed, and thus cannot
be completed in semantic completion.
I presume you are referring to the fact that
@{const_name Cons} = List.list.Cons
@{const_name hd} = List.list.hd
I have no particular stake in this issue, but I would think there was an
option (c) which is to do the *opposite* of what Jasmin said about
bringing the additional constant names etc as close as possible to
wherever they fit:
datatype_new 'a list =
Nil ([])
| Cons 'a 'a list (infixr #
Am 26.05.2014 11:46, schrieb Tobias Nipkow:
On 26/05/2014 11:07, Jasmin Blanchette wrote:
Am 26.05.2014 um 11:02 schrieb Tobias Nipkow nip...@in.tum.de:
The definition of list should look like before.
I don't see how this is an option. This would result in the following duplicate
Just to be clear on this: the ability to get all of these functions for free is
marvellous! We are now discussion only the syntactic interface to that
marvellous functionality, how much is exposed by default, and in particular in
the defn of list.
Tobias
On 26/05/2014 12:14, Dmitriy Traytel
On Sun, 25 May 2014, Jasmin Christian Blanchette wrote:
The = as the name for Nil's discriminator deserves an explanation.
[...] So I introduced this weird = syntax, which suggests that
equality is used for discriminating. I am open to other suggestions.
The other funky syntax we have is -:.
Let's distinguish between A = {hd, tl} and B = {map, set, rel}. The constants
from B are an integral part of the package---they form together with the type
a BNF. Thus, they will always be generated. The question is whether they
are exposed to the user.
Well, they necessarily need to be
Am 26.05.2014 12:25, schrieb Makarius:
On Sun, 25 May 2014, Jasmin Christian Blanchette wrote:
The = as the name for Nil's discriminator deserves an explanation.
[...] So I introduced this weird = syntax, which suggests that
equality is used for discriminating. I am open to other suggestions.
What new users see when they look at the actual definition of lists is not that
important. There are many, many situations where the actual definition of
something is much more complicated than the idealised version that one would
use for teaching. What is necessary is that simple-looking
On Mon, 26 May 2014, Dmitriy Traytel wrote:
Just on the squiggles in isolation: if these are rare add-on options one
could invent long / explicit keywords for them (or Parse.literal items).
grep gives 371 occurences of -: in IsaFoR's development repository. So
it's not a rare add-on, but
Am 26.05.2014 12:53, schrieb Makarius:
On Mon, 26 May 2014, Dmitriy Traytel wrote:
Just on the squiggles in isolation: if these are rare add-on
options one
could invent long / explicit keywords for them (or Parse.literal
items).
grep gives 371 occurences of -: in IsaFoR's development
Am 26.05.2014 um 12:25 schrieb Makarius makar...@sketis.net:
On Sun, 25 May 2014, Jasmin Christian Blanchette wrote:
The = as the name for Nil's discriminator deserves an explanation. [...]
So I introduced this weird = syntax, which suggests that equality is used
for discriminating. I am
Am 26.05.2014 um 12:05 schrieb Makarius makar...@sketis.net:
The observed here problem is different: the type constructor list somehow
ends up in the name space with a concealed flag. There might be one or
more Binding.conceal too many in the BNF sources.
Ah, now I get it. Of course this
I have a comment followed by a suggestion.
Three years ago when I introduced the concept of BNF, I initially called it
enriched type constructor.
Then people suggested that this name is too unspecific and I came up with BNF
(bounded natural functor),
which summarizes the main components:
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
On Mon, 26 May 2014, Jasmin Blanchette wrote:
Am 26.05.2014 um 13:41 schrieb Dmitriy Traytel tray...@in.tum.de:
Yes, we have considered this naming earlier. It was discarded, because
it looks like one is giving the name dead to a set function. The same
holds for any other identifier (not
Am 26.05.2014 um 15:24 schrieb Makarius makar...@sketis.net:
I think you could afford an actual keyword for the dead modifier and use it
without colon, like lazy in HOLCF/domain. That would substract dead from
the normal identifier space, but merely means its very few occurrences on
On Mon, 26 May 2014, Andrei Popescu wrote:
Then people suggested that this name is too unspecific and I came up
with BNF (bounded natural functor), which summarizes the main
components: a natural transformation set, a cardinal bound, and a
functor.
This more specific name however loses an
On Mon, 26 May 2014, Jasmin Blanchette wrote:
Am 26.05.2014 um 15:24 schrieb Makarius makar...@sketis.net:
I think you could afford an actual keyword for the dead modifier and
use it without colon, like lazy in HOLCF/domain. That would
substract dead from the normal identifier space, but
On Mon, 26 May 2014, Andrei Popescu wrote:
getSelector isNil for Nil[list]
BTW, camelCaseIsNotUsedInIsabelleSourcesToImproveReadability.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
Am 26.05.2014 um 12:34 schrieb Lawrence Paulson l...@cam.ac.uk:
What new users see when they look at the actual definition of lists is not
that important. There are many, many situations where the actual definition
of something is much more complicated than the idealised version that one
Hi all,
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.
1. The squiggles (-: and =:) are easy to get rid of, and we'll kill
them. This has been discussed before.
OK. No need to discuss this
Hi again,
datatype_new 'a list =
Nil (defaults un_Cons2: []) ([])
| Cons 'a 'a list (infixr # 65)
abbreviation map ≡ map_list
abbreviation set ≡ set_list
abbreviation list_all2 ≡ rel_list
abbreviation hd ≡ un_Cons1
abbreviation tl ≡ un_Cons2
this would make sense if you were to abandon
Hi Makarius,
For the new high-end BNF version of 'a list there were a few funny effects.
(1) Its definition looks terrific:
datatype_new (set: 'a) list (map: map rel: list_all2) =
=: Nil (defaults tl: []) ([])
| Cons (hd: 'a) (tl: 'a list) (infixr # 65)
It means it can no longer
datatype_new (set: 'a) list (map: map rel: list_all2) =
=: Nil (defaults tl: []) ([])
| Cons (hd: 'a) (tl: 'a list) (infixr # 65)
Can you explain the squiggle =: above? I did not find it in the manual
nor in the sources so far. It seems to be special to main HOL datatypes.
what it
The following is relevant to the BNF guys, with continously growing team
strength (according to Isabelle/aa7f051ba6ab).
Today we've had a tutorial with mostly fresh users, which is always useful
to see remaining snags. There were also 2-3 experienced Coq users, who
have the usual problems of
32 matches
Mail list logo
