isla icon indicating copy to clipboard operation
isla copied to clipboard

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

Open rindPHI opened this issue 2 years ago • 0 comments

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 0d5ab32ec43a35def151035026983555c6da146f.

rindPHI avatar Sep 29 '22 13:09 rindPHI