Stream: Isabelle/ML

Topic: Full name of binding

view this post on Zulip Jan van Brügge (Nov 03 2021 at 18:55):

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)

view this post on Zulip Dmitriy Traytel (Nov 03 2021 at 20:24):

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).

view this post on Zulip Jan van Brügge (Nov 03 2021 at 20:44):

ok, then i will special case the two

Last updated: Dec 21 2024 at 16:20 UTC