Email Gateway (Mar 24 2023 at 08:49): Email Gateway (Mar 24 2023 at 08:49):From: Nicolas Méric <nicolas.meric@lri.fr>
Dear all,
It looks like Syntax.parse_term is not compatible with
long-names starting with a number or an underscore.
For example in the following theory:
theory
"04_RefMan"
imports
Main
begin
record A =
a:: int
find_consts name:"04_Refman.A.make"
value‹04_Refman.A.make›
value‹A.make›
end
The evaluation of value‹04_Refman.A.make› fails
and value‹A.make› succeeds.
The reference manual explains about theory names:
«
A system_name is like name, but it excludes
white-space characters and needs to conform to file-name notation.
Name components that are special on Windows (e.g. CON, PRN, AUX) are
excluded on all platforms.
»
So, is this the expected behavior?
Best regards,
Nicolas Méric
Email Gateway (Apr 24 2023 at 10:51):From: Makarius <makarius@sketis.net>
On 24/03/2023 09:49, Nicolas Méric wrote:
It looks like Syntax.parse_term is not compatible with
long-names starting with a number or an underscore.
That is not a proper long identifier at all. Inner syntax, e.g.
Syntax.parse_term, has stricter rules than outer syntax (where double quotes
allow to produce arbitrary malformed names).
The reference manual explains about theory names:
«
A system_name is like name, but it excludes
white-space characters and needs to conform to file-name notation.
Name components that are special on Windows (e.g. CON, PRN, AUX) are
excluded on all platforms.
»
That is all about outer syntax.
For inner syntax, see the isar-ref manual about syntax category "longid",
which is the same as "long_ident" of outer syntax (but not "name" or
"system_name").
So, is this the expected behavior?
Yes, it is expected. I would say even without reading the documentation,
because such names are rather unreasonable.
Makarius
Email Gateway (Apr 24 2023 at 14:58):From: Nicolas Méric <cl-isabelle-users@lists.cam.ac.uk>
Hi Makarius,
I missed the inner syntax rule for long names in the reference manual,
thanks for pointing that out.
I'll keep in mind that using double quotes to allow malformed names for
theories should really be avoided.
Nicolas Méric
Last updated: Apr 19 2024 at 16:20 UTC