Syntax error when parameterized refinement occurs in subscript

[lemmy]

(We recently added better support for parameterized refinement in TLC: tlaplus/tlaplus#687)

----- MODULE Foo -----
EXTENDS Naturals

CONSTANT C

VARIABLE v
vars == v

Init == v = 0

Next == v' \in C

Spec == Init /\ [][Next]_v
=====

We may check that module Bar refines Foo with:

----- MODULE Bar ------
EXTENDS Naturals

VARIABLE v

S == {0, 42}

Spec == v = 0 /\ [][v' \in S]_v

F1 == INSTANCE Foo WITH C <- S
THEOREM A == Spec => F1!Spec
THEOREM B == Spec => F1!Init /\ [][F1!Next]_F1!vars

F2(c) == INSTANCE Foo WITH C <- c
THEOREM C == Spec => F2(S)!Spec
THEOREM D == Spec => F2(S)!Init /\ [][F2(S)!Next]_F2(S)!vars \*  TLAPS doesn't like  F2(S)!vars 
=====

SANY accept A, B, C, and D just fine, but TLAPS' parser reports a syntax error for D:

-> % ~/.opam/5.1.0/bin/tlapm --version
6acb3cb
-> % ~/.opam/5.1.0/bin/tlapm Bar.tla 
File "./Bar.tla", line 16, character 53
Unexpected (
File "<unknown>":
Error: Could not parse "./Bar.tla" successfully.
 tlapm ending abnormally with Failure("Module.Parser.parse_file")
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from Tlapm_lib__M_save.clocking in file "src/module/m_save.ml", line 24, characters 18-22
Called from Tlapm_lib.read_new_modules.(fun) in file "src/tlapm_lib.ml", line 503, characters 8-57
Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
Called from Tlapm_lib.main in file "src/tlapm_lib.ml", line 561, characters 20-43
Called from Tlapm_lib.init in file "src/tlapm_lib.ml", line 589, characters 8-33

-> % tlapm --version
1.5.0
-> % tlapm Bar.tla                    
File "./Bar.tla", line 16, character 53
Unexpected (
File "<unknown>":
Error: Could not parse "./Bar.tla" successfully.
 tlapm ending abnormally with Failure("Module.Parser.parse_file")
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from M_save.clocking in file "m_save.ml", line 25, characters 16-20
Called from Tlapm.read_new_modules.(fun) in file "tlapm.ml", line 455, characters 8-112
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Tlapm.main in file "tlapm.ml", line 490, characters 20-43
Called from Tlapm.init in file "tlapm.ml", line 518, characters 8-33

[ahelwer]

This failure occurs at the syntax parser level; minimized example:

---- MODULE Test ----
op == [A]_M(S)!vars
====