[isabelle-dev] Acces to internal interfaces ...

[Jasmin Blanchette]

Dear Burkhart,

> in Isabelle 2016, certain traditional interfaces to data-type packages
> do no longer exist, for example Datatype.get_info thy typename or
> its homologue on records. This function yielded for a given typename 
> the list of constructors together with their types, and other information.
> 
> This change is, as I assume, a consequence of the new layer of type-related
> packages of more recent isabelle versions.
> 
> One can, of course, extract this information from the type-exhaustion schemes.
> Is there another recommended way ?

Yes. You basically have two options: the compatibility layer and the new interfaces. The compatibility layer is provided by "~~/src/HOL/Tools/BNF/bnf_lfp_compat.ML", e.g.

	BNF_LFP_Compat.get_info

This is what we used to port big parts of the Isabelle code and the AFP. The argument list is almost identical to before.

With the new interfaces, you have to look into "ctr_sugar_of" and "fp_sugar_of" in "~~/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML" and "~~/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML". The "ctr_sugar" part is shared by datatypes, codatatypes, and other types with freely generated constructors. The "fp_sugar" contains a "ctr_sugar" and complements it with things like (co)induction, (co)recursors, etc.

> By the way, the necessary pre-requisite for doing this would be to have access 
> to the “fast reference” operation:
> 
>     ML_Thms.thm_binding kind is_single thms txt 
> 
> which is at the moment not exported.
> Again, what is the recommended way of doing this
> (searching for a theorem in a local or global context) by its long name ?

You won't need any of that.

> [And please, don’t tell me it’s Eisbach.]

Ditto.

Cheers,

Jasmin