K-user mailing list

["Park, Daejun" <dpark69 AT illinois.edu>]

Hi Mihály,

I suggest to organize your language definition as follows:

----

module A-COMMON

// put your language syntax except for program variables

syntax Variable // declare only sort for the program variables

endmodule

module A-SYNTAX

import A-COMMON

syntax Variable ::= r"[A-Z][_a-zA-Z0-9@]*" [token] // define the sort for the program variables

endmodule

module A

import A-COMMON

// put your language semantics

endmodule

----

The idea is to put the syntax for the program variables apart from the language semantics, so that you can avoid any unnecessary parsing ambiguities. In most cases, you will not need to mention a specific (program) variable name in your semantics.

In case you want to mention a specific program variable name, e.g., "main", you can do it by extending the variable sort:

syntax Variable ::= "main" [token]

Best,

Daejun

On Dec 5, 2016, at 11:05 AM, Mihály Palenik <palenik.mihaly AT gmail.com> wrote:

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