Backtracking Not Working After "in" Keyword

[viper-admin]

Created by bitbucket user nilsbecker_ on 2017-09-06 22:14
Last updated on 2019-07-31 09:29

in can either be parsed as a set operation or as part of a let, unfolding or applying expression in Viper. The rule for applying is defined as

#!scala

keyword("applying") ~/ "(" ~ magicWandExp ~ ")" ~ "in" ~ exp

Without the parentheses, in is parsed as a set operation and the in of the applying expression cannot be found. The parser should at that point backtrack and parse the expression correctly. This does not work.

A similar issue occurs for let expressions. As a work around parentheses are inserted as shown above.

[viper-admin]

@alexanderjsummers commented on 2017-11-28 18:01

This is quite confusing in practice. We should try to improve the grammar.

[viper-admin]

@alexanderjsummers on 2017-11-28 18:01:

• changed priority from minor to major

[viper-admin]

@fabiopakk commented on 2018-10-10 09:24

Could you provide examples that show how it is today and how would it preferably be instead? Both for 'in' and 'let', please.

[viper-admin]

Bitbucket user nilsbecker_ commented on 2018-10-15 14:32

For a simple let expression like

#!

let x == (2) in x == 2

it is my understanding that if you remove the parentheses around the 2 (in the parser rule and the expression) it is parsed as

#!

let x == (2 in x == 2)

i.e. x bound to the boolean value indicating whether 2 is in the set x == 2 which would obviously give a type error later on. The parser then produces an error since it cannot find the in keyword that is required for parsing the let expression. At this point the parser should backtrack and try to split the expression before the in keyword.

A similar example could be constructed for magic wands:

#!

applying (true --* acc(x.f) && x.f == 2) in x.f == 2

would be parsed as

#!

applying true --* (acc(x.f) && x.f == 2 in x.f == 2)

without the parentheses.

[viper-admin]

@fabiopakk on 2018-10-17 12:24:

• changed the assignee from (none) to @fabiopakk

[viper-admin]

@fabiopakk on 2018-10-17 15:08:

• changed the assignee from @fabiopakk to (none)

[viper-admin]

@fabiopakk on 2018-10-17 15:15:

• changed the assignee from (none) to @fabiopakk

[viper-admin]

@fabiopakk on 2018-10-17 15:28:

• changed the assignee from @fabiopakk to (none)

[viper-admin]

@fabiopakk commented on 2019-05-20 09:09

in can either be parsed as a set operation or as part of a let, unfolding or applying expression in Viper. The rule for applying is defined as

#!scala

keyword("applying") ~/ "(" ~ magicWandExp ~ ")" ~ "in" ~ exp

Without the parentheses, in is parsed as a set operation and the in of the applying expression cannot be found. The parser should at that point backtrack and parse the expression correctly. This does not work.

A similar issue occurs for let expressions. As a work around parentheses are inserted as shown above.

[viper-admin]

@fabiopakk on 2019-05-20 09:09:

• changed the assignee from (none) to bitbucket user krantikiran

[viper-admin]

@fabiopakk commented on 2019-07-31 09:29

Although good progress was made in branch krantikiran_issue_216_bactrack_after_in, no solution that is general enough was reached yet, as we cannot limit expressions to proper subsets of expressions, depending on where it occurs, just to avoid ambiguity in the parser.

[viper-admin]

@fabiopakk on 2019-07-31 09:29:

• changed the assignee from bitbucket user krantikiran to (none)