Skip to content

Commit f99ec90

Browse files
tnelsontnelson
authored
fix: join parsing, regression test, note on 2nd issue (#311)
* fix: join parsing, regression test, note on 2nd issue * add: semantics test * add: tests, no-op change to parser for readability
1 parent c4d6074 commit f99ec90

File tree

2 files changed

+117
-40
lines changed

2 files changed

+117
-40
lines changed

‎forge/lang/alloy-syntax/parser.rkt‎

Lines changed: 59 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -199,49 +199,68 @@ ExprList : NT-Expr
199199
; binary temporal connectives which are not associative."
200200

201201
NT-Expr : @NT-Expr1
202-
| LET-TOK LetDeclList BlockOrBar
203-
| BIND-TOK LetDeclList BlockOrBar
204-
| Quant DISJ-TOK? QuantDeclList BlockOrBar
205-
NT-Expr1 : @NT-Expr1.5 | NT-Expr1 OR-TOK NT-Expr1.5
206-
NT-Expr1.5 : @NT-Expr2 | NT-Expr1.5 XOR-TOK NT-Expr2
207-
NT-Expr2 : @NT-Expr3 | NT-Expr2 IFF-TOK NT-Expr3
202+
| LET-TOK LetDeclList BlockOrBar
203+
| BIND-TOK LetDeclList BlockOrBar
204+
| Quant DISJ-TOK? QuantDeclList BlockOrBar
205+
NT-Expr1 : @NT-Expr1.5
206+
| NT-Expr1 OR-TOK NT-Expr1.5
207+
NT-Expr1.5 : @NT-Expr2
208+
| NT-Expr1.5 XOR-TOK NT-Expr2
209+
NT-Expr2 : @NT-Expr3
210+
| NT-Expr2 IFF-TOK NT-Expr3
208211
;; right assoc
209-
NT-Expr3 : @NT-Expr4 | NT-Expr4 IMP-TOK NT-Expr3 (ELSE-TOK NT-Expr3)?
210-
NT-Expr4 : @NT-Expr4.5 | NT-Expr4 AND-TOK NT-Expr4.5
212+
NT-Expr3 : @NT-Expr4
213+
| NT-Expr4 IMP-TOK NT-Expr3 (ELSE-TOK NT-Expr3)?
214+
;; back to left assoc
215+
NT-Expr4 : @NT-Expr4.5
216+
| NT-Expr4 AND-TOK NT-Expr4.5
211217
; Electrum binary operators (not associative)
212-
NT-Expr4.5 : @NT-Expr5 | NT-Expr5 UNTIL-TOK NT-Expr5
213-
| NT-Expr5 RELEASE-TOK NT-Expr5
214-
| NT-Expr5 SINCE-TOK NT-Expr5
215-
| NT-Expr5 TRIGGERED-TOK NT-Expr5
216-
NT-Expr5 : @NT-Expr6 | NEG-TOK NT-Expr5
217-
| ALWAYS-TOK NT-Expr5
218-
| EVENTUALLY-TOK NT-Expr5
219-
| AFTER-TOK NT-Expr5
220-
| BEFORE-TOK NT-Expr5
221-
| ONCE-TOK NT-Expr5
222-
| HISTORICALLY-TOK NT-Expr5
223-
NT-Expr6 : @NT-Expr7 | NT-Expr6 NEG-TOK? CompareOp NT-Expr7
224-
NT-Expr7 : @NT-Expr8 | (NO-TOK | SOME-TOK | LONE-TOK | ONE-TOK | TWO-TOK | SET-TOK) NT-Expr8
225-
NT-Expr8 : @NT-Expr9 | NT-Expr8 (PLUS-TOK | MINUS-TOK) NT-Expr10
226-
NT-Expr9 : @NT-Expr10 | CARD-TOK NT-Expr9
227-
NT-Expr10 : @NT-Expr11 | NT-Expr10 PPLUS-TOK NT-Expr11
228-
NT-Expr11 : @NT-Expr12 | NT-Expr11 AMP-TOK NT-Expr12
229-
NT-Expr12 : @NT-Expr13 | NT-Expr12 ArrowOp NT-Expr13
230-
NT-Expr13 : @NT-Expr14 | NT-Expr13 (SUBT-TOK | SUPT-TOK) NT-Expr14
231-
NT-Expr14 : @NT-Expr15 | NT-Expr14 LEFT-SQUARE-TOK ExprList RIGHT-SQUARE-TOK
232-
NT-Expr15 : @NT-Expr16 | NT-Expr15 DOT-TOK NT-Expr16
233-
| Name LEFT-SQUARE-TOK ExprList RIGHT-SQUARE-TOK
234-
NT-Expr16 : @NT-Expr17 | NT-Expr16 PRIME-TOK
235-
NT-Expr17 : @NT-Expr18 | (TILDE-TOK | EXP-TOK | STAR-TOK) NT-Expr17
218+
NT-Expr4.5 : @NT-Expr5
219+
| NT-Expr5 UNTIL-TOK NT-Expr5
220+
| NT-Expr5 RELEASE-TOK NT-Expr5
221+
| NT-Expr5 SINCE-TOK NT-Expr5
222+
| NT-Expr5 TRIGGERED-TOK NT-Expr5
223+
NT-Expr5 : @NT-Expr6
224+
| NEG-TOK NT-Expr5
225+
| ALWAYS-TOK NT-Expr5
226+
| EVENTUALLY-TOK NT-Expr5
227+
| AFTER-TOK NT-Expr5
228+
| BEFORE-TOK NT-Expr5
229+
| ONCE-TOK NT-Expr5
230+
| HISTORICALLY-TOK NT-Expr5
231+
NT-Expr6 : @NT-Expr7
232+
| NT-Expr6 NEG-TOK? CompareOp NT-Expr7
233+
NT-Expr7 : @NT-Expr8
234+
| (NO-TOK | SOME-TOK | LONE-TOK | ONE-TOK | TWO-TOK | SET-TOK) NT-Expr8
235+
NT-Expr8 : @NT-Expr9
236+
| NT-Expr8 (PLUS-TOK | MINUS-TOK) NT-Expr10
237+
NT-Expr9 : @NT-Expr10
238+
| CARD-TOK NT-Expr9
239+
NT-Expr10 : @NT-Expr11
240+
| NT-Expr10 PPLUS-TOK NT-Expr11
241+
NT-Expr11 : @NT-Expr12
242+
| NT-Expr11 AMP-TOK NT-Expr12
243+
NT-Expr12 : @NT-Expr13
244+
| NT-Expr12 ArrowOp NT-Expr13
245+
NT-Expr13 : @NT-Expr14
246+
| NT-Expr13 (SUBT-TOK | SUPT-TOK) NT-Expr14
247+
NT-Expr14 : @NT-Expr15
248+
| NT-Expr14 LEFT-SQUARE-TOK ExprList RIGHT-SQUARE-TOK
249+
| NT-Expr14 DOT-TOK NT-Expr15
250+
NT-Expr15 : @NT-Expr16
251+
NT-Expr16 : @NT-Expr17
252+
| NT-Expr16 PRIME-TOK
253+
NT-Expr17 : @NT-Expr18
254+
| (TILDE-TOK | EXP-TOK | STAR-TOK) NT-Expr17
236255
NT-Expr18 : Const
237-
| QualName
238-
| AT-TOK Name
239-
| BACKQUOTE-TOK Name
240-
| THIS-TOK
241-
| LEFT-CURLY-TOK QuantDeclList BlockOrBar RIGHT-CURLY-TOK
242-
| /LEFT-PAREN-TOK @NT-Expr /RIGHT-PAREN-TOK
243-
| NT-Block
244-
| Sexpr
256+
| QualName
257+
| AT-TOK Name
258+
| BACKQUOTE-TOK Name
259+
| THIS-TOK
260+
| LEFT-CURLY-TOK QuantDeclList BlockOrBar RIGHT-CURLY-TOK
261+
| /LEFT-PAREN-TOK @NT-Expr /RIGHT-PAREN-TOK
262+
| NT-Block
263+
| Sexpr
245264

246265
ArrowExpr : QualName
247266
| QualName /ARROW-TOK @ArrowExpr

‎forge/tests/forge/expressions/joinAndQuantAssoc.frg‎

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,58 @@
1+
#lang forge
2+
option run_sterling off
3+
option verbose 0
4+
sig Person { age: one Int }
5+
one sig Solution { people: pfunc Int -> Person }
6+
lone sig Light {}
7+
8+
/** Regression test for join-associativity parser bug.
9+
Previously, this needed to be expressed as (Solution.people[0]).age.
10+
Need to also check semantics. */
11+
pred dotTest { Solution.people[0].age = 0 }
12+
13+
test expect {
14+
{ Solution.people[0].age = 0
15+
iff
16+
((Solution.people)[0]).age = 0} is checked
17+
}
18+
19+
////////////////////////////////////////////////////////////////
20+
21+
// TODO Not yet fixed
22+
/** Regression test for quantifier-precedence parser bug.
23+
Previously, the quantified sub-expression needed parentheses:
24+
some Solution and (some i: Int | no Solution.people[i]) */
25+
// pred qTest { some Solution and some i: Int | no Solution.people[i]} is sat
26+
27+
////////// Test for quantifier semantics after parse. //////////
28+
29+
// This doesn't allow anybody to have a positive age if the light is off.
30+
pred formulation_1 { (some p: Person | p.age > 0) implies (some Light) }
31+
32+
// This allows someone with a positive age even if the light is off.
33+
pred formulation_2 { some p: Person | (p.age > 0 implies some Light) }
34+
35+
// Which does the version without parens parse to? Version 2.
36+
pred formulation_Q { some p: Person | p.age >0 implies some Light }
37+
test expect {
38+
same_Q_2: { formulation_2 iff formulation_Q } is checked
39+
}
40+
// So Alloy's parsing disagrees with Enderton, who says that (paraphrasing)
41+
// "...all and some apply to as little as possible.
42+
// ... all x | A => B is not all x | (A => B)"
43+
44+
45+
////////////////////////////////
46+
// Other potential precedence issues
47+
48+
pred xOrTest1 {some Solution xor some Solution and some Solution}
49+
pred xOrTest2 {some Solution and some Solution xor some Solution}
50+
pred iffTest {some Solution iff some Solution or some Solution}
51+
pred inTest {Solution in Solution and some Solution}
52+
pred unionTest {Solution + Solution = Solution}
53+
54+
////////////////////////////////
55+
// "let" has the same issue as quantifiers
56+
// TODO
57+
// pred qTest { some Solution and let s = Solution | some s}
58+

0 commit comments

Comments
 (0)