Discrepancy between terminal and single-match regex terminal

Open
#4,082 1 comment 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Assessment

Difficulty
4/5
Estimated time
3-5 days
Newbie friendliness
25/100
Issue type
Bug
Clarity
Needs clarification
Activity status
Stale
Domain
compilers

Research direction

Reproduce the examples in lexical.k, comparing the plain terminal and regex-terminal cases, and trace the inner parser and compiler diagnostics reported for each. Determine the intended handling of regex terminals and the token/format attributes; done means the discrepancy is resolved or its behavior is clearly documented with coverage for both cases.

Written by the indexing model from the issue text.

Description

question

Consider the following definitions.

1. With terminal

module LEXICAL
    syntax Foo ::= "foo"
    rule <k> foo => .K ... </k>
endmodule

This works as expected.

2. With regex terminal

Let's change the symbol to a regex terminal.

syntax Foo ::= r"foo"

This defines the same set of valid tokens for Foo as the previous definition. But now there's a parse error:

[Error] Inner Parser: Parse error: unexpected token '=>' following token 'foo'.
        Source(/home/ttoth/git/pyk/lexical.k)
        Location(3,18,3,20)
        3 |         rule <k> foo => .K ... </k>
          .                      ^~
[Error] Compiler: Had 1 parsing errors.

3. Fix potential lexical conflicts

Speculatively, let's change the token to be disjoint from other lexicals in the prelude.

module LEXICAL
    syntax Foo ::= r"@foo"
    rule <k> @foo => .K ... </k>
endmodule

Now the error is something different:

[Error] Compiler: Expected format attribute on production with regular
expression terminal. Did you forget the 'token' attribute?
        Source(/home/ttoth/git/pyk/lexical.k)
        Location(2,20,2,27)
        2 |         syntax Foo ::= r"@foo"
          .                        ^~~~~~~
[Error] Compiler: Had 1 structural errors.

4. Add the format attribute

After adding the format attribute, kompilation works.

syntax Foo ::= r"@foo" [format(@foo)]

Questions

This raises a few questions.

  1. Why doesn't (2) work if (1) does?
  2. Why does the kompiler ask for the format attribute for (3) if for (2) it does not?
Dominant language
Python
Stars
591
Forks
163
No merged PRs in 30d

Contributor guide

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from runtimeverification/k

All issues in runtimeverification/k

Similar issues

More Python issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.