I spent way too much time on this now. How does one get the full name off a binding? I tried
Local_Theory.full_name, but not only does it prepend the theory I am working from, it also is not consistent:
local_setup ‹ fn lthy => let val SOME deadid = BNF_Def.bnf_of lthy "BNF_Composition.DEADID" val SOME sum = BNF_Def.bnf_of lthy "Sum_Type.sum" val f = Local_Theory.full_name lthy (BNF_Def.name_of_bnf deadid) val g = Local_Theory.full_name lthy (BNF_Def.name_of_bnf sum) val _ = (writeln f; writeln g) in lthy end ›
This writes (
Composition is the name of the theory the ML snippet is in):
(The two bnfs are only examples, the actual code could get any BNF, so
name_of_bnf it has to be)
You should avoid having to do this. The more low-level variant of Local_Theory.full_name is Name_Space.full_name, but there are not many usages in HOL, which shows that this is not the canonical way to do things.
Getting BNF_Composition.DEADID from the DEADID binding is not realistic: the theory name is not in the qualified path of the binding (Binding.path_of). The theory name is of course stored in the position (Binding.pos_of), but you certainly don't want to fish it from there. I think DEADID and ID will always need to be treated as special cases.
For BNFs corresponding to proper types, you can get the type name from the type (T_of_bnf).
ok, then i will special case the two
Last updated: Dec 07 2023 at 16:21 UTC