*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes*From*: Jasmin Blanchette <jasmin.blanchette at inria.fr>*Date*: Wed, 18 Nov 2015 13:43:23 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <564C685B.2020203@in.tum.de>*References*: <564B1075.5060706@in.tum.de> <C67DA37B-EEE3-4BBD-9CEE-6AB41FF48ACE@inria.fr> <564B6249.8080603@in.tum.de> <564B6466.4070200@in.tum.de> <564C2743.7080809@inf.ethz.ch> <564C3C4F.9050400@in.tum.de> <9E245509-0BC3-4A1D-A2AE-0D5999744F36@inria.fr> <564C45BA.5000601@in.tum.de> <DB7D90EF-8B43-43AB-B220-ACD633CDF884@inria.fr> <564C685B.2020203@in.tum.de>

>> Returning 1 in both cases would be even less compatible (esp. for list), and returning 0 in both cases is -- well -- precisely the old behavior, which doesn't have the nice "foolproof" property mentioned by Andreas, and for which I can easily construct an example like yours above that exhibits an odd difference in behavior (which is even less regular and intelligible). > > I assume by "exhibits an odd difference in behavior" you mean some term involving both size and size_t? They were never claimed or intended to have a fixed relationship. If you define type U by nesting through type T, the "size" function of U will depend on "size_T" -- hence there is a connection between the two. The lack of uniformity of the old definition is visible in examples such as (* with Isabelle2014 *) datatype 'a x = X 'a thm x.size datatype 'a y = Y "'a y x" | Y' thm y.size value "size (X Y')" -- "returns 0" value "size (Y (X Y'))" -- "returns 2" > But your argument that this feature was not documented and seemed crazy to you and that thus you felt free to change it shows a cavalier attitude towards source code. The tone of some of your emails reveals a cavalier attitude towards the people who work or worked for or with you. We have had instances of passive-aggressive emails from your part regarding minor points of datatypes (minor compared with the scale of the whole BNF entreprise), some of it on-list, some off-list. You will remember how this ended. Because you had the courage to apologize, you came out of the deal as an (even) greater man in my eyes than before. I had reasons to believe this would be the first and last time we would be going into that loop, but alas the same nonconstructive pattern is arising again -- and again in connection with the datatypes. I would greatly appreciate if you could keep your comments -- whether on-list or off-list -- to objective observations, as opposed to a procès d'intention. I don't know what I've done to you to deserve this; clearly, I must have done something to annoy you, but I doubt it has anything to do with the "size" function. I would appreciate if you could tell it to me frankly off-list rather than through insinuations on-list. I'm in Nancy this week. You can also pick up the phone if you think this would be more helpful. The phone number is on my web page. > Let me assume in your favour (No comment on this condescending phrase.) > that the change had no negative effect in the distribution and the AFP It had one negative effect on one AFP entry (Fitting), which was nearly trivial to work around. > and that the problems in IsaFor only showed up later. That's correct. Jasmin

**Follow-Ups**:**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Jasmin Blanchette

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Tobias Nipkow

**References**:**[isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Manuel Eberl

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Jasmin Blanchette

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Manuel Eberl

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Manuel Eberl

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Andreas Lochbihler

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Manuel Eberl

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Jasmin Blanchette

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Tobias Nipkow

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Jasmin Blanchette

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Proving termination of a recursive function
- Next by Date: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
- Previous by Thread: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
- Next by Thread: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
- Cl-isabelle-users November 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list