Re: [isabelle] datatype_compat in Isabelle2018-RC0



Hm, I had tried that before and it failed. Let me get back to you.

Cheers,
Gerwin

On 21 Jun 2018, at 19:33, Traytel Dmitriy <traytel at inf.ethz.ch<mailto:traytel at inf.ethz.ch>> wrote:

Hi Gerwin,

On 21 Jun 2018, at 19:07, Gerwin.Klein at data61.csiro.au<mailto:Gerwin.Klein at data61.csiro.au> wrote:



On 21 Jun 2018, at 18:22, Jasmin Blanchette <jasmin.blanchette at inria.fr<mailto:jasmin.blanchette at inria.fr>> wrote:
[..]
The reason why the old-style definitions were supported for so long at all was for the benefit of the "old_datatype" command. The thread "Any users of 'Old_Datatype.thy' or 'Old_SMT.thy'?" (started in December 2017) didn't reveal any users, so when I removed the legacy "old_datatype", I also removed the old-style size infrastructure (which itself is an important step towards removing the last left-overs from the old datatype package from Isabelle, to keep the Isabelle code in a not too messy state).

Ha, I did see that query, but did not realise its implication :-)


I’m using this a few times — not very often, but it’s annoying enough to recreate manually (see email thread on that around Isabelle2017..) that it’s worth checking at least.

I would like to know more about your use case. It seems like you found a corner case of the datatype package -- namely, you're presumably disabling "size" first, then invoking "datatype_compat" to produce an old-style "size". Is your main motivation for the use of old-style "size" definitions compatibility (i.e. no need to port old scripts), or do you find the old definitions intrinsically better?

The reason I'm asking is that there are advantages and disadvantages to both schemes, and it may be worthwhile to just support both, e.g. via an option.

This case is so far the only one I have encountered that showed a real difference between the two.

It is precisely as you guessed:

datatype (plugins del: size)
       'a typ_desc   = TypDesc "'a typ_struct" typ_name
  and  'a typ_struct = TypScalar nat nat "'a" |
                       TypAggregate "('a typ_desc,field_name) dt_pair list"

datatype_compat dt_pair
datatype_compat typ_desc typ_struct

then a bunch of rules recreating exactly the old induct rules, so I don’t have to dig into old and messy proofs, and then at some point:

fun
fold_td' :: "(typ_name => ('a * field_name) list => 'a) * 'a typ_desc => 'a"
where
fot0: "fold_td' (f,TypDesc st nm) = (case st of
         TypScalar n algn d => d |
         TypAggregate ts => f nm (map (\<lambda>x. case x of DTPair t n => (fold_td' (f,t),n)) ts))”

The following works for me out of the box. Note that I also have removed "(plugins del: size)" from dt_pair.

Cheers,
Dmitriy


type_synonym field_name = string
type_synonym typ_name = string

datatype ('a,'b) dt_pair = DTPair 'a 'b

datatype 'a typ_desc   = TypDesc "'a typ_struct" typ_name
  and   'a typ_struct = TypScalar nat nat "'a" |
                        TypAggregate "('a typ_desc,field_name) dt_pair list"

datatype_compat dt_pair
datatype_compat typ_desc typ_struct

fun
fold_td' :: "(typ_name => ('a * field_name) list => 'a) * 'a typ_desc => 'a"
where
fot0: "fold_td' (f,TypDesc st nm) = (case st of
         TypScalar n algn d => d |
         TypAggregate ts => f nm (map (λx. case x of DTPair t n => (fold_td' (f,t),n)) ts))"



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.