isla
isla copied to clipboard
Formula with same variable bound by different quantifiers and using XPath expressions not parseable
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.