Re: [isabelle] Looking up information about new datatypes



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

> On 23 Oct 2017, at 13:58, Stefan Berghofer <berghofe at in.tum.de> wrote:
> 
> 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
> 





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