Email Gateway (Aug 22 2022 at 16:18): Email Gateway (Aug 22 2022 at 16:18):From: Stefan Berghofer <berghofe@in.tum.de>
Hi all,
I am looking for an ML API for looking up information about new datatypes. In particular, from the name of
a datatype, I would like to find out the names (and types) of the selector functions corresponding to the
arguments of a constructor. I am aware of the get_info function from BNF_LFP_Compat, but this does not give
me any information about selector functions, since they were not supported by the old datatype package.
If I have understood the code correctly, get_info is based on the fp_sugar_of function from BNF_FP_Def_Sugar,
but this function mainly seems to return low-level internal information about the datatype. Is there a
function returning more high-level information, including the selector functions?
Greetings,
Stefan
Email Gateway (Aug 22 2022 at 16:18):From: Lars Hupel <hupel@in.tum.de>
Hi Stefan,
you might want to look at "Ctr_Sugar.ctr_sugar_of". The resulting record
contains fields for selectors, discriminators etc.
Cheers
Lars
Email Gateway (Aug 22 2022 at 16:18):From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Stefan,
fp_sugar_of returns pretty much everything that we know about the datatype (high- and low-level stuff).
The selectors are part of the "constructor sugar" abstraction. Lars gave a reference how to query that interface. But this info (and a bit more) is also contained in the returned fp_sugar record. See e.g.
ML ‹BNF_FP_Def_Sugar.fp_sugar_of @{context} @{type_name list} |> the |> #fp_ctr_sugar›
ML ‹BNF_FP_Def_Sugar.fp_sugar_of @{context} @{type_name list} |> the |> #fp_ctr_sugar |> #ctr_sugar›
Please also note that for datatype declarations the selectors are turned off by default. To get the command to generate them one has either to give a name to at least one selector or pass the discs_sels option (c.f. isabelle doc datatypes for details).
Cheers,
Dmitriy
Email Gateway (Aug 22 2022 at 16:19):From: Stefan Berghofer <berghofe@in.tum.de>
Dear Dmitriy and Lars,
thanks a lot for your quick and helpful replies. The Ctr_Sugar.ctr_sugar_of function was exactly what I was looking for.
Greetings,
Stefan
Last updated: Apr 25 2024 at 08:20 UTC