Merge pull request #3764 from mtzguido/parser_tweak

Parser: tweak grammar to expose a rule useful to Pulse
FStarLang · Feb 16, 2025 · 1daf467 · 1daf467
2 parents ef85c02 + 80f4c3a
commit 1daf467
Showing 1 changed file with 6 additions and 2 deletions.
diff --git a/src/ml/FStarC_Parser_Parse.mly b/src/ml/FStarC_Parser_Parse.mly
@@ -1302,7 +1302,8 @@ tmEqWith(X):
 %inline recordTerm:
   | LBRACE e=recordExp RBRACE { e }
 
-tmNoEqWith(X):
+%public
+tmNoEqNoRecordWith(X):
   | e1=tmNoEqWith(X) COLON_COLON e2=tmNoEqWith(X)
       { consTerm (rr $loc) e1 e2 }
   | e1=tmNoEqWith(X) AMP e2=tmNoEqWith(X)
@@ -1329,13 +1330,16 @@ tmNoEqWith(X):
       { mkApp op [ e1, Infix; e2, Nothing ] (rr $loc) }
  | e1=tmNoEqWith(X) op=OPINFIX4 e2=tmNoEqWith(X)
       { mk_term (Op(mk_ident(op, rr $loc(op)), [e1; e2])) (rr $loc) Un}
-  | e=recordTerm { e }
   | BACKTICK_PERC e=atomicTerm
       { mk_term (VQuote e) (rr $loc) Un }
   | op=TILDE e=atomicTerm
       { mk_term (Op(mk_ident (op, rr $loc(op)), [e])) (rr $loc) Formula }
   | e=X { e }
 
+tmNoEqWith(X):
+  | e=tmNoEqNoRecordWith(X) { e }
+  | e=recordTerm { e }
+
 binop_name:
   | o=OPINFIX0a              { mk_ident (o, rr $loc) }
   | o=OPINFIX0b              { mk_ident (o, rr $loc) }