K-user mailing list

[Mihály Palenik <palenik.mihaly AT gmail.com>]

Hello,

I found a strange warning message and I don't know what is the problem.

I have Variable sort:
syntax Variable ::= r"[A-Z][_a-zA-Z0-9@]*"      [token, autoReject]

syntax Exp ::= Variable

which always has parsing ambiguity with #KVariable. That's why is use :: sort annotation which eliminate it.

I have a function called matching
syntax Map ::= matching(Exp, Exp, Map) [function]
I'd like to write matching rule where second Exp is always different subsort of Exp (e.g Atom, Variable...).
For the Variable I write this:
rule matching(E::Exp, P:Variable, M) => do_something

I got the above mention warning:

[Warning] Inner Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: syntax Variable ::= r"[A-Z][_a-zA-Z0-9@]*"
[Location(...)
Source(#token("...",KString))
autoReject(#token("",AttributeValue)) klabel(#token("",KString))
token(#token("",AttributeValue))]
    #token(Variable,"P")
2: syntax #KVariable ::=
r"(?<![A-Za-z0-9_\\$!\\?])(\\!|\\?)?([A-Z][A-Za-z0-9'_]*|_)"
[Location(#token("62",Int),#token("25",Int),#token("62",Int),#token("143",Int))
Source(#token("../include/builtin/kast.k",KString))
autoReject(#token("",AttributeValue))
hook(#token("org.kframework.kore.KVariable",AttributeValue))
klabel(#token("",KString)) token(#token("",AttributeValue))]
    #token(#KVariable,"P")
    Source(...)
    Location(...)

If I try with :: then:

rule matching(E::Exp, P::Variable, M) => do_something

[Warning] Inner Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: syntax Variable ::= r"[A-Z][_a-zA-Z0-9@]*"
[Location(...)
Source(#token("...",KString))
autoReject(#token("",AttributeValue)) klabel(#token("",KString))
token(#token("",AttributeValue))]
    #token(Variable,"P")
2: syntax Variable ::= Variable ":Variable"
[klabel(#token("#SemanticCastToVariable",KString))
sort(#token("Variable",KString))]
    #SemanticCastToVariable(#token(#KVariable,"P"))
    Source(...)
    Location(...)

I don't know the second syntax Variable where come from. Maybe second is a #KVariable which is cast to Variable. But how can I fix it?

I read in CHANGELOG.md that I can edit k-distribution/include/builtin/kast.k (where is #KVariable) but I'm not professional with K and don't want to change it.

Thank you your answers in advance.

Best regards,

Mihály Palenik