Skip to content

Commit

Permalink
Merge pull request #2921 from FStarLang/_nik_menhir
Browse files Browse the repository at this point in the history
Marking some symbols public in the menhir grammar
  • Loading branch information
nikswamy authored May 10, 2023
2 parents 1904d9a + 2ff1be4 commit 347bae4
Showing 1 changed file with 10 additions and 1 deletion.
11 changes: 10 additions & 1 deletion ocaml/fstar-lib/FStar_Parser_Parse.mly
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,8 @@
there are S-R conflicts with dangling elses, with a non-delimited match where
the BAR is dangling etc.
Note: Some symbols are marked public, so that we can reuse this parser from
the parser for the Pulse DSL in FStarLang/steel.
*)
(* (c) Microsoft Corporation. All rights reserved *)
Expand Down Expand Up @@ -586,6 +587,7 @@ binderAttributes:
disjunctivePattern:
| pats=separated_nonempty_list(BAR, tuplePattern) { pats }

%public
tuplePattern:
| pats=separated_nonempty_list(COMMA, constructorPattern)
{ match pats with | [x] -> x | l -> mk_pattern (PatTuple (l, false)) (rr $loc) }
Expand Down Expand Up @@ -710,6 +712,7 @@ aqualifiedWithAttrs(X):
qlident:
| ids=path(lident) { lid_of_ids ids }

%public
quident:
| ids=path(uident) { lid_of_ids ids }

Expand Down Expand Up @@ -739,10 +742,12 @@ ifMaybeOp:
| IF {None}
| op=IF_OP { Some (mk_ident ("let" ^ op, rr $loc(op))) }

%public
lidentOrUnderscore:
| id=IDENT { mk_ident(id, rr $loc(id))}
| UNDERSCORE { gen (rr $loc) }

%public
lident:
| id=IDENT { mk_ident(id, rr $loc(id))}

Expand Down Expand Up @@ -805,6 +810,7 @@ match_returning:
| as_opt=option(AS i=lident {i}) RETURNS t=tmIff {as_opt,t,false}
| as_opt=option(AS i=lident {i}) RETURNS_EQ t=tmIff {as_opt,t,true}

%public
noSeqTerm:
| t=typ { t }
| e=tmIff SUBTYPE t=tmIff tactic_opt=option(BY tactic=thunk(typ) {tactic})
Expand Down Expand Up @@ -1248,9 +1254,11 @@ simpleDef:
| head=indexingTerm args=list(argTerm)
{ mkApp head (map (fun (x,y) -> (y,x)) args) (rr2 $loc(head) $loc(args)) }

%public
appTerm:
| t=appTermCommon(t=argTerm {t} | h=maybeHash LBRACE t=recordExp RBRACE {h, t}) {t}

%public
appTermNoRecordExp:
| t=appTermCommon(argTerm) {t}

Expand All @@ -1262,6 +1270,7 @@ argTerm:
| { Nothing }
| HASH { Hash }

%public
indexingTerm:
| e1=atomicTermNotQUident op_exprs=nonempty_list(dotOperator)
{
Expand Down

0 comments on commit 347bae4

Please sign in to comment.