Re: [isabelle] datatype_compat in Isabelle2018-RC0




> 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:

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))”

With the old size definition, fun find as lexicographic termination order, with the new size definitions it fails (and I couldn’t figure out one within 20min, which might have more to do with the state of my mind than anything).

Originals (for 2017) at
https://github.com/seL4/l4v/blob/a837d380126ae06765353bcd6af90e5546e8e946/tools/c-parser/umm_heap/CTypesDefs.thy#L34
https://github.com/seL4/l4v/blob/a837d380126ae06765353bcd6af90e5546e8e946/tools/c-parser/umm_heap/CTypesDefs.thy#L756

This is not the nicest way to define things, but again, lots of later ugly proofs depend on the structure of these functions, so I am loathe to touch them if not necessary.

Cheers,
Gerwin



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