Hi Chris,
> is there a reliable way to check - given the name of a type constructor - how
> many dead type parameters it has?
>
> I tried
>
> (case BNF_FP_Def_Sugar.fp_sugar_of lthy tname of
> SOME sugar =>
> if BNF_Def.dead_of_bnf (#fp_bnf sugar) > 0 then
> error "..."
> ...
>
> However having something like
>
> datatype foo = Foo | Bar
>
> I noticed that
>
> print_bnfs
>
> does not list type "foo",
It doesn't because it's a nullary BNF and all types are trivially nullary BNFs,
so there's no point in storing this pointless information in our databases.
Instead, we store only a single such type, namely 'a, where 'a is dead. This
BNF is called DEADID -- it's listed when you execute "print_bnfs", and you can
grep for it in "src/HOL/*.thy" to find out where it is registered.
So when you look up "foo", you get, somewhat confusingly, the BNF entry for 'a.
A more reliable way to count the number of deads is to use the equation:
num_dead_vars = num_type_vars - num_live_vars
"BNF_Def.live_of_bnf" and "Sign.arity_number" are your friends.
I hope this solves your problem.
Don't hesitate to let us know if you run into issues again. Those interfaces
were never very polished, nor documented (although I might come to add a
section to "isabelle doc datatypes" about the ML functions -- there is an
embryonic, commented out "Using the Standard ML Interface" section already).
Cheers,
Jasmin
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
