Email Gateway (Aug 17 2022 at 14:15): Email Gateway (Aug 17 2022 at 14:15):From: Michael Norrish <Michael.Norrish@nicta.com.au>
If I have just defined a constant (using add_constdefs_i, say), and
want to construct a new term including that new constant term, how
should I generate that term?
It seems that using
Sign.intern_const
will give me the correct qualified name for the constant (I do know
its name after all), but I'm worried about the situation when multiple
constants from different theories have the same name. What will
intern_const do then?
Is there a function that will give me the name of the current theory,
so that I can construct the fully-qualified name myself?
Or is there some other way again?
Thanks,
Michael.
Email Gateway (Aug 17 2022 at 14:15):From: Makarius <makarius@sketis.net>
You are right in being worried. Above `intern' only worked by chance,
because a recent declaration is likely to be preferred by name space
lookup.
Name spaces provide 3 key operations:
full -- produce fully qualified name according to the current naming policy
intern -- internalize an external name (partically qualified) according
to the current name space (for reading etc.)
extern -- reverse of intern (for printing etc.)
You want to perform the `full' operation here, ie. mimic what
add_constdefs_i did internally. Do this via Sign.full_name, which uses
the official naming convention of the theory context. Do not refer to
theory_name etc. directly.
Makarius
Last updated: May 03 2024 at 08:18 UTC