Skip to content

Commit 421d0ff

Browse files
mtzguidomtzguido
authored
Merge pull request #3984 from mtzguido/starstar
Lexer: make `**` actually right-associative, but keep its precedence
2 parents 8288c84 + 7c79a4b commit 421d0ff

File tree

6 files changed

+83
-16
lines changed

6 files changed

+83
-16
lines changed

‎src/ml/FStarC_Parser_LexFStar.ml

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -209,10 +209,10 @@ let () =
209209
"¬", TILDE "~";
210210
"⸬", COLON_COLON;
211211
"▹", PIPE_RIGHT;
212-
"÷", OPINFIX3 "÷";
212+
"÷", OPINFIX3L "÷";
213213
"‖", OPINFIX0a "||";
214214
"×", IDENT "op_Multiply";
215-
"∗", OPINFIX3 "*";
215+
"∗", OPINFIX3L "*";
216216
"⇒", OPINFIX0c "=>";
217217
"≥", OPINFIX0c ">=";
218218
"≤", OPINFIX0c "<=";
@@ -611,6 +611,8 @@ match%sedlex lexbuf with
611611
| _ -> assert false end
612612

613613
(* Operators. *)
614+
| "**" , Star symbolchar -> ensure_no_comment lexbuf (fun s -> OPINFIX3R s)
615+
| "|->" , Star symbolchar -> ensure_no_comment lexbuf (fun s -> OPINFIX4 s)
614616
| op_prefix, Star symbolchar -> ensure_no_comment lexbuf (fun s -> OPPREFIX s)
615617
| op_infix0a, Star symbolchar -> ensure_no_comment lexbuf (fun s -> OPINFIX0a s)
616618
| op_infix0b, Star symbolchar -> ensure_no_comment lexbuf (fun s -> OPINFIX0b s)
@@ -620,9 +622,8 @@ match%sedlex lexbuf with
620622
| op_infix2, Star symbolchar -> ensure_no_comment lexbuf (fun s -> OPINFIX2 s)
621623
| op_infix3, Star symbolchar -> ensure_no_comment lexbuf (function
622624
| "" -> one_line_comment "" lexbuf
623-
| s -> OPINFIX3 s
625+
| s -> OPINFIX3L s
624626
)
625-
| "**" , Star symbolchar -> ensure_no_comment lexbuf (fun s -> OPINFIX4 s)
626627

627628
(* Unicode Operators *)
628629
| uoperator -> let id = L.lexeme lexbuf in

‎src/ml/FStarC_Parser_Parse.mly

Lines changed: 10 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -138,7 +138,7 @@ type tc_constraint = {
138138
%token BACKTICK UNIV_HASH
139139
%token BACKTICK_PERC
140140

141-
%token<string> OPPREFIX OPINFIX0a OPINFIX0b OPINFIX0c OPINFIX0d OPINFIX1 OPINFIX2 OPINFIX3 OPINFIX4
141+
%token<string> OPPREFIX OPINFIX0a OPINFIX0b OPINFIX0c OPINFIX0d OPINFIX1 OPINFIX2 OPINFIX3L OPINFIX3R OPINFIX4
142142
%token<string> OP_MIXFIX_ASSIGNMENT OP_MIXFIX_ACCESS
143143
%token<string * string * Lexing.position * FStarC_Sedlexing.snap> BLOB
144144
%token<string * string * Lexing.position * FStarC_Sedlexing.snap> USE_LANG_BLOB
@@ -166,7 +166,8 @@ type tc_constraint = {
166166
%right PIPE_LEFT
167167
%right OPINFIX1
168168
%left OPINFIX2 MINUS QUOTE
169-
%left OPINFIX3
169+
%left OPINFIX3L
170+
%right OPINFIX3R
170171
%left BACKTICK
171172
%right OPINFIX4
172173

@@ -1346,12 +1347,14 @@ tmNoEqNoRecordWith(X):
13461347
in
13471348
mk_term (Sum(dom, res)) (rr2 $loc(e1) $loc(e2)) Type_level
13481349
}
1349-
| e1=tmNoEqWith(X) op=OPINFIX3 e2=tmNoEqWith(X)
1350+
1351+
| e1=tmNoEqWith(X) op=OPINFIX3L e2=tmNoEqWith(X)
1352+
| e1=tmNoEqWith(X) op=OPINFIX3R e2=tmNoEqWith(X)
1353+
| e1=tmNoEqWith(X) op=OPINFIX4 e2=tmNoEqWith(X)
13501354
{ mk_term (Op(mk_ident(op, rr $loc(op)), [e1; e2])) (rr $loc) Un}
1355+
13511356
| e1=tmNoEqWith(X) BACKTICK op=tmNoEqWith(X) BACKTICK e2=tmNoEqWith(X)
13521357
{ mkApp op [ e1, Infix; e2, Nothing ] (rr $loc) }
1353-
| e1=tmNoEqWith(X) op=OPINFIX4 e2=tmNoEqWith(X)
1354-
{ mk_term (Op(mk_ident(op, rr $loc(op)), [e1; e2])) (rr $loc) Un}
13551358
| BACKTICK_PERC e=atomicTerm
13561359
{ mk_term (VQuote e) (rr $loc) Un }
13571360
| op=TILDE e=atomicTerm
@@ -1370,7 +1373,8 @@ binop_name:
13701373
| o=OPINFIX0d { mk_ident (o, rr $loc) }
13711374
| o=OPINFIX1 { mk_ident (o, rr $loc) }
13721375
| o=OPINFIX2 { mk_ident (o, rr $loc) }
1373-
| o=OPINFIX3 { mk_ident (o, rr $loc) }
1376+
| o=OPINFIX3L { mk_ident (o, rr $loc) }
1377+
| o=OPINFIX3R { mk_ident (o, rr $loc) }
13741378
| o=OPINFIX4 { mk_ident (o, rr $loc) }
13751379
| o=IMPLIES { mk_ident ("==>", rr $loc) }
13761380
| o=CONJUNCTION { mk_ident ("/\\", rr $loc) }

‎src/ml/FStarC_Parser_ParseIt.ml

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -461,7 +461,8 @@ let string_of_token =
461461
| OPINFIX0d s -> "OPINFIX0d " ^ s
462462
| OPINFIX1 s -> "OPINFIX1 " ^ s
463463
| OPINFIX2 s -> "OPINFIX2 " ^ s
464-
| OPINFIX3 s -> "OPINFIX3 " ^ s
464+
| OPINFIX3L s -> "OPINFIX3L " ^ s
465+
| OPINFIX3R s -> "OPINFIX3R " ^ s
465466
| OPINFIX4 s -> "OPINFIX4 " ^ s
466467
| OP_MIXFIX_ASSIGNMENT s -> "OP_MIXFIX_ASSIGNMENT " ^ s
467468
| OP_MIXFIX_ACCESS s -> "OP_MIXFIX_ACCESS " ^ s

‎src/parser/FStarC.Parser.ToDocument.fst

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -312,9 +312,10 @@ let matches_level s (assoc_levels, tokens) =
312312
// GM 05/10/18, TODO: This still needs to be heavily annotated with the new unifier:
313313
314314
(* Precedence and associativity levels, taken from ../src/parse.mly *)
315-
let opinfix4 : associativity_level = Right, [Exact "**"; UnicodeOperator]
315+
let opinfix4 : associativity_level = Right, [Exact "|->"; UnicodeOperator]
316316
// level backtick won't be used here
317-
let opinfix3 : associativity_level = Left, [StartsWith '*' ; StartsWith '/' ; StartsWith '%']
317+
let opinfix3l : associativity_level = Left, [StartsWith '*' ; StartsWith '/' ; StartsWith '%']
318+
let opinfix3r : associativity_level = Right, [Exact "**"]
318319
let opinfix2 : associativity_level = Left, [StartsWith '+' ; StartsWith '-' ]
319320
let minus_lvl : associativity_level = Left, [Exact "-"] // Sublevel of opinfix2, not a level on its own !!!
320321
let opinfix1 : associativity_level = Right, [StartsWith '@' ; StartsWith '^']
@@ -332,7 +333,8 @@ let colon_colon : associativity_level = Right, [Exact "::"]
332333
let level_associativity_spec : list associativity_level =
333334
[
334335
opinfix4 ;
335-
opinfix3 ;
336+
opinfix3r ;
337+
opinfix3l ;
336338
opinfix2 ;
337339
opinfix1 ;
338340
pipe_right ;
@@ -389,7 +391,7 @@ let is_operatorInfix0ad12 op =
389391
List.tryFind (matches_level <| Ident.string_of_id op) operatorInfix0ad12 <> None
390392
391393
let is_operatorInfix34 =
392-
let opinfix34 = [ opinfix3 ; opinfix4 ] in
394+
let opinfix34 = [ opinfix3l ; opinfix3r; opinfix4 ] in
393395
fun op -> List.tryFind (matches_level <| Ident.string_of_id op) opinfix34 <> None
394396
395397
let handleable_args_length (op:ident) =
@@ -1948,7 +1950,7 @@ and p_tmEqWith' p_X curr e = match e.tm with
19481950
19491951
and p_tmNoEqWith p_X e =
19501952
(* TODO : this should be precomputed but F* complains about a potential ML effect *)
1951-
let n = max_level [colon_colon ; amp ; opinfix3 ; opinfix4] in
1953+
let n = max_level [colon_colon ; amp ; opinfix3l ; opinfix3r ; opinfix4] in
19521954
p_tmNoEqWith' false p_X n e
19531955
19541956
and p_tmNoEqWith' inside_tuple p_X curr e = match e.tm with

‎tests/bug-reports/closed/Bug3980.fst

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
module Bug3980
2+
3+
assume
4+
val slprop : Type
5+
6+
assume
7+
val p : int -> slprop
8+
9+
assume
10+
val ( ** ) : slprop -> slprop -> slprop
11+
12+
let a = p 1 ** p 2 ** p 3
13+
let b = p 1 ** (p 2 ** p 3)
14+
let c = (p 1 ** p 2) ** p 3
15+
16+
#check p 1 ** p 2 ** p 3
17+
#check (p 1 ** p 2) ** p 3
18+
#check p 1 ** (p 2 ** p 3)
19+
20+
let _ = assert (a == b)
21+
22+
[@@expect_failure]
23+
let _ = assert (a == c)
24+
[@@expect_failure]
25+
let _ = assert (b == c)
26+
27+
assume
28+
val ( |-> ) : string -> int -> slprop
29+
30+
let _ = "a" |-> 1 ** "b" |-> 2
31+
32+
33+
#check "a" |-> 1 ** "b" |-> 2

‎tests/bug-reports/closed/Bug3980.fst.output.expected

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
* Info at Bug3980.fst(16,0-16,24):
2+
- Term Bug3980.p 1 ** Bug3980.p 2 ** Bug3980.p 3 has type Bug3980.slprop
3+
4+
* Info at Bug3980.fst(17,0-17,26):
5+
- Term (Bug3980.p 1 ** Bug3980.p 2) ** Bug3980.p 3 has type Bug3980.slprop
6+
7+
* Info at Bug3980.fst(18,0-18,26):
8+
- Term Bug3980.p 1 ** Bug3980.p 2 ** Bug3980.p 3 has type Bug3980.slprop
9+
10+
* Info at Bug3980.fst(23,8-23,14):
11+
- Expected failure:
12+
- Assertion failed
13+
- The SMT solver could not prove the query. Use --query_stats for more
14+
details.
15+
- See also Bug3980.fst(23,15-23,23)
16+
17+
* Info at Bug3980.fst(25,8-25,14):
18+
- Expected failure:
19+
- Assertion failed
20+
- The SMT solver could not prove the query. Use --query_stats for more
21+
details.
22+
- See also Bug3980.fst(25,15-25,23)
23+
24+
* Info at Bug3980.fst(33,0-33,29):
25+
- Term "a" |-> 1 ** "b" |-> 2 has type Bug3980.slprop
26+

0 commit comments

Comments
 (0)