Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Formula with same variable bound by different quantifiers and using XPath expressions not parseable #17

Open
rindPHI opened this issue Sep 29, 2022 · 0 comments
Assignees
Labels
bug Something isn't working minor Bugs/issues of minor importance parser ISLa-Parser related issues

Comments

@rindPHI
Copy link
Owner

rindPHI commented Sep 29, 2022

The formula

forall <internal_reference> ref in start:
   exists <labeled_paragraph> lpar in start:
     ref.<id> = lpar.<label>.<id> and
 forall <internal_reference_nospace> fref in start:
   exists <labeled_paragraph> lpar in start:
     fref.<id> = lpar.<label>.<id>

cannot be parsed with the REST_GRAMMAR; code to reproduce:

from isla.language import parse_isla
from isla_formalizations.rest import REST_GRAMMAR

parse_isla(
    """
forall <internal_reference> ref in start:
   exists <labeled_paragraph> lpar in start:
     ref.<id> = lpar.<label>.<id> and
 forall <internal_reference_nospace> fref in start:
   exists <labeled_paragraph> lpar in start:
     fref.<id> = lpar.<label>.<id>
""",
    REST_GRAMMAR,
)

Output is:

SyntaxError: Unbound variables: id_0 in formula
(forall <internal_reference> ref in start:
   exists <labeled_paragraph> lpar in start:
     (= id id_0) and
forall <internal_reference_nospace> fref in start:
  exists <labeled_paragraph> lpar_0 in start:
    (= id_1 id_0))

Using ISLa v1.2.0, commit id 0d5ab32.

@rindPHI rindPHI added bug Something isn't working minor Bugs/issues of minor importance parser ISLa-Parser related issues labels Sep 29, 2022
@rindPHI rindPHI self-assigned this Sep 29, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working minor Bugs/issues of minor importance parser ISLa-Parser related issues
Projects
None yet
Development

No branches or pull requests

1 participant