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):
Composition.DEADID
Composition.Sum_Type.sum
I want:
BNF_Composition.DEADID
Sum_Type.sum
(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 2024 at 16:22 UTC