Re: [isabelle-dev] Notes on datatype_new list

2014-05-28 Thread Jasmin Christian Blanchette
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) =

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Tobias Nipkow
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

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Tobias Nipkow
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

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Jasmin Christian Blanchette
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

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Tobias Nipkow
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

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread 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. set rel_list vs. forall_list2 un_Cons1 vs. hd

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Dmitriy Traytel
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.

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Makarius
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

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Thomas Sewell
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 #

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Dmitriy Traytel
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

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Tobias Nipkow
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

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread 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. The other funky syntax we have is -:.

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Jasmin Christian Blanchette
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

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Dmitriy Traytel
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.

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Lawrence Paulson
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

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread 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 repository. So it's not a rare add-on, but

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Dmitriy Traytel
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

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Jasmin Blanchette
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

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Jasmin Blanchette
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

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Andrei Popescu
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:

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Jasmin Christian Blanchette
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

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Makarius
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

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Jasmin Blanchette
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

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Makarius
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

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Makarius
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

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Makarius
On Mon, 26 May 2014, Andrei Popescu wrote: getSelector isNil for Nil[list] BTW, camelCaseIsNotUsedInIsabelleSourcesToImproveReadability. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Jasmin Christian Blanchette
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

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Tobias Nipkow
On 26/05/2014 16:13, Jasmin Christian Blanchette wrote: 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

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Makarius
On Mon, 26 May 2014, Jasmin Christian Blanchette wrote: 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

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Florian Haftmann
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

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Florian Haftmann
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

Re: [isabelle-dev] Notes on datatype_new list

2014-05-25 Thread Jasmin Christian Blanchette
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

Re: [isabelle-dev] Notes on datatype_new list

2014-05-24 Thread Andrei Popescu
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

[isabelle-dev] Notes on datatype_new list

2014-05-23 Thread Makarius
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