K-user mailing list

[Radu Mereuta <headness13 AT gmail.com>]

Hi Mihály,

That's the point, you don't want to access what is in A-SYNTAX from A, because it will taint the rule parser and create ambiguities.

You are fine putting in A-SYNTAX only those productions which create ambiguities. They will reach the program parser, so you can still parse programs correctly.

module A-COMMON

  syntax Variable

  syntax Exp ::= Exp "+" Exp

                       | Variable

endmodule

module A-SYNTAX

  import A-COMMON

  syntax Variable ::= r"[A-Z][_a-zA-Z0-9@]*" [token, autoReject] // ambiguous with KVariable from kast.k. Should be avoided in modules where you have rules

endmodule

module A

  import A-COMMON

  syntax Variable ::= "Main" [token] // this is fine, since it's a single word, and the tool can reserve the name for sort Variable

  rule A + B => Main // A,B - meta variable from K of sort Exp, Main - token of sort Variable from the user language

endmodule

Radu

On Tue, Dec 6, 2016 at 7:12 PM, Mihály Palenik <palenik.mihaly AT gmail.com> wrote:

Hello,

Thank you your answer.

I try to organize my module structure like you mentioned above before your email. If I know well A-COMMON for parsing, A for semantic and A-SYNTAX is additional syntax for semantic?

In A module you import A-COMMON, so how can I reach stuff in A-SYNTAX in my A module?

Thank you your help in advance!

Best regards

Mihály Palenik

On Tue, Dec 6, 2016 at 1:20 AM, Park, Daejun <dpark69 AT illinois.edu> wrote:

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