Email Gateway (Aug 22 2022 at 14:44): Email Gateway (Aug 22 2022 at 14:44):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi all,
The "datatype" command and the "smt" proof method were reimplemented in Isabelle2014. For compatibility, the old constructs are provided by "/src/HOL/Library/Old_Datatype.thy" and "/src/HOL/Library/Old_SMT.thy", as "old_datatype" and "old_smt".
Do you depend on either of these constructs?
If so, why?
Would you be sorry if "old_datatype", "old_smt", or both were to be missing in the next release (presumably Isabelle2017)?
If the answer to question 3 is yes, please reply.
Jasmin
Email Gateway (Aug 22 2022 at 14:44):From: "Urban, Christian" <christian.urban@kcl.ac.uk>
Dear Jasmin,
I am not sure what the latest states of Nominal1 (in the distribution) and Nominal2 (in the AFP) are? If I remember correctly, they depend internally
on old_datatype (heavily). I am not sure how easy it would be to port
them to (new)datatype. It would certainly be desirable.
Best wishes,
Christian
Email Gateway (Aug 22 2022 at 14:44):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Christian,
I am not sure what the latest states of Nominal1 (in the distribution) and Nominal2 (in the AFP) are?
I ported Nominal1 to the new datatypes back in 2014, using the compatibility interfaces (which are almost one-to-one with the old interfaces). As for Nominal2, I had run into a limitation in my code back then and didn't investigate further, but I could easily give it a new try (a lot of bugs were fixed since then). In any case, it's on my radar. I'm more worried about users in the non-Isabelle, non-AFP world.
Jasmin
Email Gateway (Aug 22 2022 at 14:55):From: Burkhart Wolff <Burkhart.Wolff@lri.fr>
Dear all,
we use indeed in a rather critical way the "~~/src/HOL/Library/Old_Datatype.thy”
package - we need a uniform way to extract splitting rules for arbitrary data-types
and a kind of abstract syntax for data-types to compute cycles in (indirect) type
dependencies. Neither of this is really existing in the 2016 version of the new-datatype
package, although I tried quite hard to reconstruct this information (implicitly
depending on naming conventions for theorems and the like.)
bu
Email Gateway (Aug 22 2022 at 14:57):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Burkhart,
Thanks for answering my email.
You wrote:
we use indeed in a rather critical way the "~~/src/HOL/Library/Old_Datatype.thy”
package
The old datatype package consists of several layers of .ML and .thy files. My email concerns only the last layer -- mainly, the "old_datatype" command provided by "Old_Datatype.thy" or the corresponding "Old_Datatype.add_datatype" ML command.
In particular, excluded from the scope of my email are all the ML functions provided by modules called "Old_Datatype_Xxx" (for some nonempty "Xxx", e.g. "Aux"). For these, reform should also come some day, but let's proceed one step at a time.
- we need a uniform way to extract splitting rules for arbitrary data-types
The new package certainly offers an interface for doing so:
ML {*
Ctr_Sugar.ctr_sugar_of @{context} @{type_name list}
|> the
|> #split
*}
And if you're porting old code, or are prone to nostalgia, you can use the compatibility interfaces:
ML {*
BNF_LFP_Compat.the_info @{theory} [] @{type_name list}
|> #split
*}
and a kind of abstract syntax for data-types to compute cycles in (indirect) type
dependencies.
This is too abstract for me to understand what you want. Which old interface do you rely on exactly?
Neither of this is really existing in the 2016 version of the new-datatype package,
I can't judge for the "kind of abstract syntax", but for splitting rules they have been around since 2014.
The compatibility interfaces were designed to be comprehensive and allowed us to port Isabelle's own tools and the AFP, and they themselves only use public APIs such as "Ctr_Sugar.ctr_sugar_of" and "BNF_FP_Def_Sugar.fp_sugar_of". Almost everything we know about a datatype is recorded somewhere in there.
although I tried quite hard to reconstruct this information (implicitly
depending on naming conventions for theorems and the like.)
Could you tell us concretely what information about, say, "list", you cannot access using the public APIs? This would interest me a lot.
Isabelle's interfaces are not perfect, but we've worked hard to make the new (co)datatype interfaces complete, and we use them ourselves for many tools, so I'm really puzzled by your comments.
Cheers,
Jasmin
Last updated: Apr 25 2024 at 08:20 UTC