[isabelle-dev] BNF: number of dead variables

[Christian Sternagel]

Hi Jasmin,

thanks for the quick reply. Your suggestion works fine!

cheers

chris

On 12/03/2014 03:46 PM, Jasmin Christian Blanchette wrote:
> 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
>