Email Gateway (Aug 22 2022 at 17:24): Email Gateway (Aug 22 2022 at 17:24):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Gerwin,
The datatype_compat command used to generate the old-style definition of the “size” constant in Isabelle2017 (potentially only when size did not yet exist). This no longer seems to be the case.
Is this intentional? I couldn’t find anything relevant in NEWS.
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).
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.
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 17:24):From: Gerwin.Klein@data61.csiro.au
On 21 Jun 2018, at 18:22, Jasmin Blanchette <jasmin.blanchette@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
Email Gateway (Aug 22 2022 at 17:24):From: Traytel Dmitriy <traytel@inf.ethz.ch>
Hi Gerwin,
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))"
Email Gateway (Aug 22 2022 at 17:24):From: Gerwin.Klein@data61.csiro.au
Hm, I had tried that before and it failed. Let me get back to you.
Cheers,
Gerwin
Email Gateway (Aug 22 2022 at 17:24):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Gerwin,
Hm, I had tried that before and it failed. Let me get back to you.
Your type has very few constructors. Another option, which is always available, is to define the "size" instance yourself. The "size" plugin (old or new) is doing very little.
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 17:24):From: Gerwin.Klein@data61.csiro.au
That would have been my fall-back solution, yes.
Cheers,
Gerwin
Email Gateway (Aug 22 2022 at 17:40):From: Gerwin.Klein@data61.csiro.au
The datatype_compat command used to generate the old-style definition of the “size” constant in Isabelle2017 (potentially only when size did not yet exist). This no longer seems to be the case.
Is this intentional? I couldn’t find anything relevant in NEWS.
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.
Cheers,
Gerwin
Last updated: Apr 18 2024 at 16:19 UTC