Re: [isabelle] datatype_compat in Isabelle2018-RC0
> On 21 Jun 2018, at 19:07, Gerwin.Klein at data61.csiro.au wrote:
>> On 21 Jun 2018, at 18:22, Jasmin Blanchette <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:
> fold_td' :: "(typ_name => ('a * field_name) list => 'a) * 'a typ_desc => 'a"
> 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.
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 typ_desc typ_struct
fold_td' :: "(typ_name => ('a * field_name) list => 'a) * 'a typ_desc => 'a"
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