nikswamy
commented
1 year ago Thanks! This is an interesting way to visualize the grammar. How would you suggest we use it?
Open mingodad opened 1 year ago
nikswamy
commented
1 year ago Thanks! This is an interesting way to visualize the grammar. How would you suggest we use it?
mingodad
commented
1 year ago As a supplemental documentation ! You can generate it for offline usage (saving the online rendering or using the offline tool https://www.bottlecaps.de/rr/download/rr-2.0-java11.zip).
nikswamy
commented
1 year ago Thanks @mingodad! Already last week I think @amosr mentioned that such documentation is useful and would be a great way to explore and learn F*'s syntax. So, this would be great to include in our docs.
But, do you have any suggestions for how to maintain it? For example, we recently had some changes to the menhir grammar. Is there an easy way to regenerate the BNF for input to the railroad diagram tool?
mingodad
commented
1 year ago Probably if the changes are small then manually updating the EBNF shown above would do, otherwise a bit of thinkering would be needed.
See bellow the update EBNF using this sequence:
menhir --only-preprocess ocaml/fstar-lib/FStar_Parser_Parse.mly > fstar-pp.mly
squilu "test-menhir.nut" fstar-pp.mly > fstar-pp-0.ebnf
# manually move the top macros `option___anonymous_0_ ...` to the bottom then add the `tokens` manually extracted from ocaml/fstar-lib/FStar_Parser_LexFStar.mlinputFragment ::= list_decl_ EOF
oneDeclOrEOF ::= EOF
| idecl
idecl ::= decl startOfNextDeclToken
startOfNextDeclToken ::= EOF
| pragmaStartToken
| LBRACK_AT
| LBRACK_AT_AT
| qualifier
| CLASS
| INSTANCE
| OPEN
| FRIEND
| INCLUDE
| MODULE
| TYPE
| EFFECT
| LET
| VAL
| SPLICE
| SPLICET
| EXCEPTION
| NEW_EFFECT
| LAYERED_EFFECT
| SUB_EFFECT
| POLYMONADIC_BIND
| POLYMONADIC_SUBCOMP
pragmaStartToken ::= PRAGMA_SET_OPTIONS
| PRAGMA_RESET_OPTIONS
| PRAGMA_PUSH_OPTIONS
| PRAGMA_POP_OPTIONS
| PRAGMA_RESTART_SOLVER
| PRAGMA_PRINT_EFFECTS_GRAPH
pragma ::= PRAGMA_SET_OPTIONS string
| PRAGMA_RESET_OPTIONS option_string_
| PRAGMA_PUSH_OPTIONS option_string_
| PRAGMA_POP_OPTIONS
| PRAGMA_RESTART_SOLVER
| PRAGMA_PRINT_EFFECTS_GRAPH
attribute ::= LBRACK_AT list_atomicTerm_ RBRACK
| LBRACK_AT_AT right_flexible_list_SEMICOLON_noSeqTerm_ RBRACK
decoration ::= attribute
| qualifier
decl ::= ASSUME uident COLON noSeqTerm
| list_decoration_ rawDecl
| list_decoration_ typeclassDecl
typeclassDecl ::= CLASS typeDecl
| INSTANCE letqualifier letbinding
rawDecl ::= pragma
| OPEN quident
| FRIEND quident
| INCLUDE quident
| MODULE uident EQUALS quident
| MODULE qlident
| MODULE quident
| TYPE separated_nonempty_list_AND_typeDecl_
| EFFECT uident typars EQUALS typ
| LET letqualifier separated_nonempty_list_AND_letbinding_
| VAL constant
| VAL lident list_multiBinder_ COLON typ
| VAL LPAREN OPPREFIX RPAREN list_multiBinder_ COLON typ
| VAL LPAREN binop_name RPAREN list_multiBinder_ COLON typ
| VAL LPAREN TILDE RPAREN list_multiBinder_ COLON typ
| VAL LPAREN AND_OP RPAREN list_multiBinder_ COLON typ
| VAL LPAREN LET_OP RPAREN list_multiBinder_ COLON typ
| SPLICE LBRACK loption_separated_nonempty_list_SEMICOLON_ident__ RBRACK thunk_atomicTerm_
| SPLICET LBRACK loption_separated_nonempty_list_SEMICOLON_ident__ RBRACK atomicTerm
| EXCEPTION uident option___anonymous_0_
| NEW_EFFECT newEffect
| LAYERED_EFFECT effectDefinition
| EFFECT layeredEffectDefinition
| SUB_EFFECT subEffect
| POLYMONADIC_BIND polymonadic_bind
| POLYMONADIC_SUBCOMP polymonadic_subcomp
| BLOB
typeDecl ::= ident typars option_ascribeKind_ typeDefinition
typars ::= tvarinsts
| binders
tvarinsts ::= TYP_APP_LESS separated_nonempty_list_COMMA_tvar_ TYP_APP_GREATER
typeDefinition ::= /* empty */
| EQUALS typ
| EQUALS LBRACE right_flexible_nonempty_list_SEMICOLON_recordFieldDecl_ RBRACE
| EQUALS binderAttributes LBRACE right_flexible_nonempty_list_SEMICOLON_recordFieldDecl_ RBRACE
| EQUALS list_constructorDecl_
recordFieldDecl ::= aqualifiedWithAttrs_lidentOrOperator_ COLON typ
constructorPayload ::= COLON typ
| OF typ
| LBRACE right_flexible_nonempty_list_SEMICOLON_recordFieldDecl_ RBRACE option___anonymous_1_
constructorDecl ::= BAR uident option_constructorPayload_
| BAR binderAttributes uident option_constructorPayload_
attr_letbinding ::= AND letbinding
| attribute AND letbinding
letoperatorbinding ::= tuplePattern option_ascribeTyp_ option___anonymous_2_
letbinding ::= maybeFocus lident nonempty_list_patternOrMultibinder_ option_ascribeTyp_ EQUALS term
| maybeFocus LPAREN OPPREFIX RPAREN nonempty_list_patternOrMultibinder_ option_ascribeTyp_ EQUALS term
| maybeFocus LPAREN binop_name RPAREN nonempty_list_patternOrMultibinder_ option_ascribeTyp_ EQUALS term
| maybeFocus LPAREN TILDE RPAREN nonempty_list_patternOrMultibinder_ option_ascribeTyp_ EQUALS term
| maybeFocus LPAREN AND_OP RPAREN nonempty_list_patternOrMultibinder_ option_ascribeTyp_ EQUALS term
| maybeFocus LPAREN LET_OP RPAREN nonempty_list_patternOrMultibinder_ option_ascribeTyp_ EQUALS term
| maybeFocus tuplePattern ascribeTyp EQUALS term
| maybeFocus tuplePattern EQUALS term
newEffect ::= effectRedefinition
| effectDefinition
effectRedefinition ::= uident EQUALS simpleTerm
effectDefinition ::= LBRACE uident binders COLON tmArrow_tmNoEq_ WITH separated_nonempty_list_SEMICOLON_effectDecl_ RBRACE
layeredEffectDefinition ::= LBRACE uident binders WITH tmNoEq RBRACE
effectDecl ::= lident binders EQUALS simpleTerm
subEffect ::= quident SQUIGGLY_RARROW quident EQUALS simpleTerm
| quident SQUIGGLY_RARROW quident LBRACE IDENT EQUALS simpleTerm RBRACE
| quident SQUIGGLY_RARROW quident LBRACE IDENT EQUALS simpleTerm SEMICOLON IDENT EQUALS simpleTerm RBRACE
polymonadic_bind ::= LPAREN quident COMMA quident RPAREN PIPE_RIGHT quident EQUALS simpleTerm
polymonadic_subcomp ::= quident SUBTYPE quident EQUALS simpleTerm
qualifier ::= ASSUME
| INLINE
| UNFOLDABLE
| INLINE_FOR_EXTRACTION
| UNFOLD
| IRREDUCIBLE
| NOEXTRACT
| DEFAULT
| TOTAL
| PRIVATE
| NOEQUALITY
| UNOPTEQUALITY
| NEW
| LOGIC
| OPAQUE
| REIFIABLE
| REFLECTABLE
maybeFocus ::= boption_SQUIGGLY_RARROW_
letqualifier ::= REC
| /* empty */
aqual ::= HASH LBRACK thunk_tmNoEq_ RBRACK
| HASH
| DOLLAR
binderAttributes ::= LBRACK_AT_AT_AT right_flexible_list_SEMICOLON_noSeqTerm_ RBRACK
disjunctivePattern ::= separated_nonempty_list_BAR_tuplePattern_
tuplePattern ::= separated_nonempty_list_COMMA_constructorPattern_
constructorPattern ::= constructorPattern COLON_COLON constructorPattern
| quident nonempty_list_atomicPattern_
| atomicPattern
atomicPattern ::= LPAREN tuplePattern COLON simpleArrow refineOpt RPAREN
| LBRACK loption_separated_nonempty_list_SEMICOLON_tuplePattern__ RBRACK
| LBRACE right_flexible_nonempty_list_SEMICOLON_fieldPattern_ RBRACE
| LENS_PAREN_LEFT constructorPattern COMMA separated_nonempty_list_COMMA_constructorPattern_ LENS_PAREN_RIGHT
| LPAREN tuplePattern RPAREN
| tvar
| LPAREN OPPREFIX RPAREN
| LPAREN binop_name RPAREN
| LPAREN TILDE RPAREN
| LPAREN AND_OP RPAREN
| LPAREN LET_OP RPAREN
| UNDERSCORE
| HASH UNDERSCORE
| constant
| BACKTICK_PERC atomicTerm
| aqualifiedWithAttrs_lident_
| quident
fieldPattern ::= qlident EQUALS tuplePattern
| qlident
patternOrMultibinder ::= LBRACE_BAR lidentOrUnderscore COLON simpleArrow BAR_RBRACE
| LBRACE_BAR simpleArrow BAR_RBRACE
| atomicPattern
| LPAREN aqualifiedWithAttrs_lident_ nonempty_list_aqualifiedWithAttrs_lident__ COLON simpleArrow refineOpt RPAREN
binder ::= aqualifiedWithAttrs_lidentOrUnderscore_
| tvar
multiBinder ::= LBRACE_BAR lidentOrUnderscore COLON simpleArrow BAR_RBRACE
| LBRACE_BAR simpleArrow BAR_RBRACE
| LPAREN nonempty_list_aqualifiedWithAttrs_lidentOrUnderscore__ COLON simpleArrow refineOpt RPAREN
binders ::= list___anonymous_4_
aqualifiedWithAttrs_lident_ ::= aqual binderAttributes lident
| aqual lident
| binderAttributes lident
| lident
aqualifiedWithAttrs_lidentOrOperator_ ::= aqual binderAttributes lident
| aqual binderAttributes LPAREN OPPREFIX RPAREN
| aqual binderAttributes LPAREN binop_name RPAREN
| aqual binderAttributes LPAREN TILDE RPAREN
| aqual binderAttributes LPAREN AND_OP RPAREN
| aqual binderAttributes LPAREN LET_OP RPAREN
| aqual lident
| aqual LPAREN OPPREFIX RPAREN
| aqual LPAREN binop_name RPAREN
| aqual LPAREN TILDE RPAREN
| aqual LPAREN AND_OP RPAREN
| aqual LPAREN LET_OP RPAREN
| binderAttributes lident
| binderAttributes LPAREN OPPREFIX RPAREN
| binderAttributes LPAREN binop_name RPAREN
| binderAttributes LPAREN TILDE RPAREN
| binderAttributes LPAREN AND_OP RPAREN
| binderAttributes LPAREN LET_OP RPAREN
| lident
| LPAREN OPPREFIX RPAREN
| LPAREN binop_name RPAREN
| LPAREN TILDE RPAREN
| LPAREN AND_OP RPAREN
| LPAREN LET_OP RPAREN
aqualifiedWithAttrs_lidentOrUnderscore_ ::= aqual binderAttributes lidentOrUnderscore
| aqual lidentOrUnderscore
| binderAttributes lidentOrUnderscore
| lidentOrUnderscore
qlident ::= path_lident_
quident ::= path_uident_
path_lident_ ::= lident
| uident DOT path_lident_
path_uident_ ::= uident
| uident DOT path_uident_
ident ::= lident
| uident
qlidentOrOperator ::= qlident
| LPAREN OPPREFIX RPAREN
| LPAREN binop_name RPAREN
| LPAREN TILDE RPAREN
| LPAREN AND_OP RPAREN
| LPAREN LET_OP RPAREN
matchMaybeOp ::= MATCH
| MATCH_OP
ifMaybeOp ::= IF
| IF_OP
lidentOrUnderscore ::= IDENT
| UNDERSCORE
lident ::= IDENT
uident ::= NAME
tvar ::= TVAR
thunk_atomicTerm_ ::= atomicTerm
thunk_tmNoEq_ ::= tmNoEq
thunk_typ_ ::= typ
thunk2_typ_ ::= typ
ascribeTyp ::= COLON tmArrow_tmNoEq_ option___anonymous_5_
ascribeKind ::= COLON kind
kind ::= tmArrow_tmNoEq_
term ::= noSeqTerm
| noSeqTerm SEMICOLON term
| noSeqTerm SEMICOLON_OP term
| lidentOrUnderscore LONG_LEFT_ARROW noSeqTerm SEMICOLON term
match_returning ::= option___anonymous_6_ RETURNS tmIff
| option___anonymous_7_ RETURNS_EQ tmIff
noSeqTerm ::= typ
| tmIff SUBTYPE tmIff option___anonymous_8_
| tmIff EQUALTYPE tmIff option___anonymous_9_
| atomicTermNotQUident DOT_LPAREN term RPAREN LARROW noSeqTerm
| atomicTermNotQUident DOT_LBRACK term RBRACK LARROW noSeqTerm
| atomicTermNotQUident DOT_LBRACK_BAR term BAR_RBRACK LARROW noSeqTerm
| atomicTermNotQUident DOT_LENS_PAREN_LEFT term LENS_PAREN_RIGHT LARROW noSeqTerm
| REQUIRES typ
| ENSURES typ
| DECREASES typ
| DECREASES LBRACE_COLON_WELL_FOUNDED noSeqTerm RBRACE
| ATTRIBUTES nonempty_list_atomicTerm_
| ifMaybeOp noSeqTerm option_match_returning_ THEN noSeqTerm ELSE noSeqTerm
| ifMaybeOp noSeqTerm option_match_returning_ THEN noSeqTerm
| TRY term WITH reverse_left_flexible_nonempty_list_BAR_patternBranch_
| matchMaybeOp term option_match_returning_ WITH reverse_left_flexible_list_BAR___anonymous_10_
| LET OPEN term IN term
| LET letqualifier letbinding list_attr_letbinding_ IN term
| attribute LET letqualifier letbinding list_attr_letbinding_ IN term
| LET_OP letoperatorbinding list___anonymous_11_ IN term
| FUNCTION reverse_left_flexible_nonempty_list_BAR_patternBranch_
| ASSUME atomicTerm
| ASSERT atomicTerm option___anonymous_12_
| UNDERSCORE BY thunk_atomicTerm_
| SYNTH atomicTerm
| CALC atomicTerm LBRACE noSeqTerm SEMICOLON list_calcStep_ RBRACE
| INTRO FORALL binders DOT noSeqTerm WITH noSeqTerm
| INTRO EXISTS binders DOT noSeqTerm WITH list_atomicTerm_ AND noSeqTerm
| INTRO tmFormula IMPLIES tmFormula WITH singleBinder DOT noSeqTerm
| INTRO tmFormula DISJUNCTION tmConjunction WITH NAME noSeqTerm
| INTRO tmConjunction CONJUNCTION tmTuple WITH noSeqTerm AND noSeqTerm
| ELIM FORALL binders DOT noSeqTerm WITH list_atomicTerm_
| ELIM EXISTS binders DOT noSeqTerm RETURNS noSeqTerm WITH singleBinder DOT noSeqTerm
| ELIM tmFormula IMPLIES tmFormula WITH noSeqTerm
| ELIM tmFormula DISJUNCTION tmConjunction RETURNS noSeqTerm WITH singleBinder DOT noSeqTerm AND singleBinder DOT noSeqTerm
| ELIM tmConjunction CONJUNCTION tmTuple RETURNS noSeqTerm WITH binders DOT noSeqTerm
singleBinder ::= binders
calcRel ::= binop_name
| BACKTICK qlident BACKTICK
| atomicTerm
calcStep ::= calcRel LBRACE option_term_ RBRACE noSeqTerm SEMICOLON
typ ::= simpleTerm
| FORALL binders DOT trigger noSeqTerm
| EXISTS binders DOT trigger noSeqTerm
trigger ::= /* empty */
| LBRACE_COLON_PATTERN disjunctivePats RBRACE
disjunctivePats ::= separated_nonempty_list_DISJUNCTION_conjunctivePat_
conjunctivePat ::= separated_nonempty_list_SEMICOLON_appTerm_
simpleTerm ::= tmIff
| FUN nonempty_list_patternOrMultibinder_ RARROW term
maybeFocusArrow ::= RARROW
| SQUIGGLY_RARROW
patternBranch ::= disjunctivePattern maybeFocusArrow term
| disjunctivePattern WHEN tmFormula maybeFocusArrow term
tmIff ::= tmImplies IFF tmIff
| tmImplies
tmImplies ::= tmArrow_tmFormula_ IMPLIES tmImplies
| tmArrow_tmFormula_
tmArrow_tmFormula_ ::= LBRACE_BAR tmFormula BAR_RBRACE RARROW tmArrow_tmFormula_
| LPAREN aqual tmFormula RPAREN RARROW tmArrow_tmFormula_
| LPAREN aqual binderAttributes tmFormula RPAREN RARROW tmArrow_tmFormula_
| tmFormula RARROW tmArrow_tmFormula_
| binderAttributes tmFormula RARROW tmArrow_tmFormula_
| aqual tmFormula RARROW tmArrow_tmFormula_
| aqual binderAttributes tmFormula RARROW tmArrow_tmFormula_
| tmFormula
tmArrow_tmNoEq_ ::= LBRACE_BAR tmNoEq BAR_RBRACE RARROW tmArrow_tmNoEq_
| LPAREN aqual tmNoEq RPAREN RARROW tmArrow_tmNoEq_
| LPAREN aqual binderAttributes tmNoEq RPAREN RARROW tmArrow_tmNoEq_
| tmNoEq RARROW tmArrow_tmNoEq_
| binderAttributes tmNoEq RARROW tmArrow_tmNoEq_
| aqual tmNoEq RARROW tmArrow_tmNoEq_
| aqual binderAttributes tmNoEq RARROW tmArrow_tmNoEq_
| tmNoEq
simpleArrow ::= simpleArrowDomain RARROW simpleArrow
| tmEqNoRefinement
simpleArrowDomain ::= LBRACE_BAR tmEqNoRefinement BAR_RBRACE
| tmEqNoRefinement
| binderAttributes tmEqNoRefinement
| aqual tmEqNoRefinement
| aqual binderAttributes tmEqNoRefinement
tmFormula ::= tmFormula DISJUNCTION tmConjunction
| tmConjunction
tmConjunction ::= tmConjunction CONJUNCTION tmTuple
| tmTuple
tmTuple ::= separated_nonempty_list_COMMA_tmEq_
tmEqWith_appTermNoRecordExp_ ::= tmEqWith_appTermNoRecordExp_ EQUALS tmEqWith_appTermNoRecordExp_
| tmEqWith_appTermNoRecordExp_ COLON_EQUALS tmEqWith_appTermNoRecordExp_
| tmEqWith_appTermNoRecordExp_ PIPE_RIGHT tmEqWith_appTermNoRecordExp_
| tmEqWith_appTermNoRecordExp_ OPINFIX0a tmEqWith_appTermNoRecordExp_
| tmEqWith_appTermNoRecordExp_ OPINFIX0b tmEqWith_appTermNoRecordExp_
| tmEqWith_appTermNoRecordExp_ OPINFIX0c tmEqWith_appTermNoRecordExp_
| tmEqWith_appTermNoRecordExp_ OPINFIX0d tmEqWith_appTermNoRecordExp_
| tmEqWith_appTermNoRecordExp_ OPINFIX1 tmEqWith_appTermNoRecordExp_
| tmEqWith_appTermNoRecordExp_ OPINFIX2 tmEqWith_appTermNoRecordExp_
| tmEqWith_appTermNoRecordExp_ MINUS tmEqWith_appTermNoRecordExp_
| MINUS tmEqWith_appTermNoRecordExp_
| QUOTE tmEqWith_appTermNoRecordExp_
| BACKTICK tmEqWith_appTermNoRecordExp_
| BACKTICK_AT atomicTerm
| BACKTICK_HASH atomicTerm
| tmNoEqWith_appTermNoRecordExp_
tmEqWith_tmRefinement_ ::= tmEqWith_tmRefinement_ EQUALS tmEqWith_tmRefinement_
| tmEqWith_tmRefinement_ COLON_EQUALS tmEqWith_tmRefinement_
| tmEqWith_tmRefinement_ PIPE_RIGHT tmEqWith_tmRefinement_
| tmEqWith_tmRefinement_ OPINFIX0a tmEqWith_tmRefinement_
| tmEqWith_tmRefinement_ OPINFIX0b tmEqWith_tmRefinement_
| tmEqWith_tmRefinement_ OPINFIX0c tmEqWith_tmRefinement_
| tmEqWith_tmRefinement_ OPINFIX0d tmEqWith_tmRefinement_
| tmEqWith_tmRefinement_ OPINFIX1 tmEqWith_tmRefinement_
| tmEqWith_tmRefinement_ OPINFIX2 tmEqWith_tmRefinement_
| tmEqWith_tmRefinement_ MINUS tmEqWith_tmRefinement_
| MINUS tmEqWith_tmRefinement_
| QUOTE tmEqWith_tmRefinement_
| BACKTICK tmEqWith_tmRefinement_
| BACKTICK_AT atomicTerm
| BACKTICK_HASH atomicTerm
| tmNoEqWith_tmRefinement_
tmNoEqWith_appTermNoRecordExp_ ::= tmNoEqWith_appTermNoRecordExp_ COLON_COLON tmNoEqWith_appTermNoRecordExp_
| tmNoEqWith_appTermNoRecordExp_ AMP tmNoEqWith_appTermNoRecordExp_
| tmNoEqWith_appTermNoRecordExp_ OPINFIX3 tmNoEqWith_appTermNoRecordExp_
| tmNoEqWith_appTermNoRecordExp_ BACKTICK tmNoEqWith_appTermNoRecordExp_ BACKTICK tmNoEqWith_appTermNoRecordExp_
| tmNoEqWith_appTermNoRecordExp_ OPINFIX4 tmNoEqWith_appTermNoRecordExp_
| LBRACE recordExp RBRACE
| BACKTICK_PERC atomicTerm
| TILDE atomicTerm
| appTermNoRecordExp
tmNoEqWith_tmRefinement_ ::= tmNoEqWith_tmRefinement_ COLON_COLON tmNoEqWith_tmRefinement_
| tmNoEqWith_tmRefinement_ AMP tmNoEqWith_tmRefinement_
| tmNoEqWith_tmRefinement_ OPINFIX3 tmNoEqWith_tmRefinement_
| tmNoEqWith_tmRefinement_ BACKTICK tmNoEqWith_tmRefinement_ BACKTICK tmNoEqWith_tmRefinement_
| tmNoEqWith_tmRefinement_ OPINFIX4 tmNoEqWith_tmRefinement_
| LBRACE recordExp RBRACE
| BACKTICK_PERC atomicTerm
| TILDE atomicTerm
| tmRefinement
binop_name ::= OPINFIX0a
| OPINFIX0b
| OPINFIX0c
| EQUALS
| OPINFIX0d
| OPINFIX1
| OPINFIX2
| OPINFIX3
| OPINFIX4
| IMPLIES
| CONJUNCTION
| DISJUNCTION
| IFF
| PIPE_RIGHT
| COLON_EQUALS
| COLON_COLON
| OP_MIXFIX_ASSIGNMENT
| OP_MIXFIX_ACCESS
tmEqNoRefinement ::= tmEqWith_appTermNoRecordExp_
tmEq ::= tmEqWith_tmRefinement_
tmNoEq ::= tmNoEqWith_tmRefinement_
tmRefinement ::= lidentOrUnderscore COLON appTermNoRecordExp refineOpt
| appTerm
refineOpt ::= option___anonymous_13_
recordExp ::= right_flexible_nonempty_list_SEMICOLON_simpleDef_
| appTerm WITH right_flexible_nonempty_list_SEMICOLON_simpleDef_
simpleDef ::= qlidentOrOperator EQUALS noSeqTerm
| qlidentOrOperator
appTerm ::= indexingTerm list___anonymous_14_
appTermNoRecordExp ::= indexingTerm list_argTerm_
argTerm ::= indexingTerm
| HASH indexingTerm
| universe
indexingTerm ::= atomicTermNotQUident nonempty_list_dotOperator_
| atomicTerm
atomicTerm ::= atomicTermNotQUident
| atomicTermQUident
| opPrefixTerm_atomicTermQUident_
atomicTermQUident ::= quident
| quident DOT_LPAREN term RPAREN
atomicTermNotQUident ::= UNDERSCORE
| tvar
| constant
| opPrefixTerm_atomicTermNotQUident_
| LPAREN OPPREFIX RPAREN
| LPAREN binop_name RPAREN
| LPAREN TILDE RPAREN
| LPAREN AND_OP RPAREN
| LPAREN LET_OP RPAREN
| LENS_PAREN_LEFT tmEq COMMA separated_nonempty_list_COMMA_tmEq_ LENS_PAREN_RIGHT
| projectionLHS list___anonymous_15_
| BEGIN term END
opPrefixTerm_atomicTermNotQUident_ ::= OPPREFIX atomicTermNotQUident
opPrefixTerm_atomicTermQUident_ ::= OPPREFIX atomicTermQUident
projectionLHS ::= qidentWithTypeArgs_qlident_option_fsTypeArgs__
| qidentWithTypeArgs_quident_some_fsTypeArgs__
| LPAREN term option_pair_hasSort_simpleTerm__ RPAREN
| LBRACK_BAR right_flexible_list_SEMICOLON_noSeqTerm_ BAR_RBRACK
| LBRACK right_flexible_list_SEMICOLON_noSeqTerm_ RBRACK
| PERCENT_LBRACK right_flexible_list_SEMICOLON_noSeqTerm_ RBRACK
| BANG_LBRACE loption_separated_nonempty_list_COMMA_appTerm__ RBRACE
| quident QMARK_DOT lident
| quident QMARK
fsTypeArgs ::= TYP_APP_LESS separated_nonempty_list_COMMA_atomicTerm_ TYP_APP_GREATER
qidentWithTypeArgs_qlident_option_fsTypeArgs__ ::= qlident option_fsTypeArgs_
qidentWithTypeArgs_quident_some_fsTypeArgs__ ::= quident some_fsTypeArgs_
hasSort ::= SUBKIND
constant ::= LPAREN_RPAREN
| INT
| CHAR
| STRING
| TRUE
| FALSE
| REAL
| UINT8
| INT8
| UINT16
| INT16
| UINT32
| INT32
| UINT64
| INT64
| SIZET
| REIFY
| RANGE_OF
| SET_RANGE_OF
universe ::= UNIV_HASH atomicUniverse
universeFrom ::= atomicUniverse
| universeFrom OPINFIX2 universeFrom
| ident nonempty_list_atomicUniverse_
atomicUniverse ::= UNDERSCORE
| INT
| lident
| LPAREN universeFrom RPAREN
warn_error_list ::= warn_error EOF
warn_error ::= flag range
| flag range warn_error
flag ::= OPINFIX1
| OPINFIX2
| MINUS
range ::= INT
| RANGE
string ::= STRING
some_fsTypeArgs_ ::= fsTypeArgs
right_flexible_list_SEMICOLON_fieldPattern_ ::= /* empty */
| fieldPattern
| fieldPattern SEMICOLON right_flexible_list_SEMICOLON_fieldPattern_
right_flexible_list_SEMICOLON_noSeqTerm_ ::= /* empty */
| noSeqTerm
| noSeqTerm SEMICOLON right_flexible_list_SEMICOLON_noSeqTerm_
right_flexible_list_SEMICOLON_recordFieldDecl_ ::= /* empty */
| recordFieldDecl
| recordFieldDecl SEMICOLON right_flexible_list_SEMICOLON_recordFieldDecl_
right_flexible_list_SEMICOLON_simpleDef_ ::= /* empty */
| simpleDef
| simpleDef SEMICOLON right_flexible_list_SEMICOLON_simpleDef_
right_flexible_nonempty_list_SEMICOLON_fieldPattern_ ::= fieldPattern
| fieldPattern SEMICOLON right_flexible_list_SEMICOLON_fieldPattern_
right_flexible_nonempty_list_SEMICOLON_recordFieldDecl_ ::= recordFieldDecl
| recordFieldDecl SEMICOLON right_flexible_list_SEMICOLON_recordFieldDecl_
right_flexible_nonempty_list_SEMICOLON_simpleDef_ ::= simpleDef
| simpleDef SEMICOLON right_flexible_list_SEMICOLON_simpleDef_
reverse_left_flexible_list_BAR___anonymous_10_ ::= /* empty */
| patternBranch
| reverse_left_flexible_list_BAR___anonymous_10_ BAR patternBranch
reverse_left_flexible_nonempty_list_BAR_patternBranch_ ::= patternBranch
| BAR patternBranch
| reverse_left_flexible_nonempty_list_BAR_patternBranch_ BAR patternBranch
option___anonymous_0_ ::= /* empty */
| OF typ
option___anonymous_1_ ::= /* empty */
| COLON typ
option___anonymous_12_ ::= /* empty */
| BY thunk2_typ_
option___anonymous_13_ ::= /* empty */
| LBRACE noSeqTerm RBRACE
option___anonymous_2_ ::= /* empty */
| EQUALS term
option___anonymous_5_ ::= /* empty */
| BY thunk_atomicTerm_
option___anonymous_6_ ::= /* empty */
| AS lident
option___anonymous_7_ ::= /* empty */
| AS lident
option___anonymous_8_ ::= /* empty */
| BY thunk_typ_
option___anonymous_9_ ::= /* empty */
| BY thunk_typ_
option_ascribeKind_ ::= /* empty */
| ascribeKind
option_ascribeTyp_ ::= /* empty */
| ascribeTyp
option_constructorPayload_ ::= /* empty */
| constructorPayload
option_fsTypeArgs_ ::= /* empty */
| fsTypeArgs
option_match_returning_ ::= /* empty */
| match_returning
option_pair_hasSort_simpleTerm__ ::= /* empty */
| hasSort simpleTerm
option_string_ ::= /* empty */
| string
option_term_ ::= /* empty */
| term
boption_SQUIGGLY_RARROW_ ::= /* empty */
| SQUIGGLY_RARROW
loption_separated_nonempty_list_COMMA_appTerm__ ::= /* empty */
| separated_nonempty_list_COMMA_appTerm_
loption_separated_nonempty_list_SEMICOLON_ident__ ::= /* empty */
| separated_nonempty_list_SEMICOLON_ident_
loption_separated_nonempty_list_SEMICOLON_tuplePattern__ ::= /* empty */
| separated_nonempty_list_SEMICOLON_tuplePattern_
list___anonymous_11_ ::= /* empty */
| AND_OP letoperatorbinding list___anonymous_11_
list___anonymous_14_ ::= /* empty */
| argTerm list___anonymous_14_
| LBRACE recordExp RBRACE list___anonymous_14_
| HASH LBRACE recordExp RBRACE list___anonymous_14_
list___anonymous_15_ ::= /* empty */
| DOT qlident list___anonymous_15_
list___anonymous_4_ ::= /* empty */
| binder list___anonymous_4_
| multiBinder list___anonymous_4_
list_argTerm_ ::= /* empty */
| argTerm list_argTerm_
list_atomicTerm_ ::= /* empty */
| atomicTerm list_atomicTerm_
list_attr_letbinding_ ::= /* empty */
| attr_letbinding list_attr_letbinding_
list_calcStep_ ::= /* empty */
| calcStep list_calcStep_
list_constructorDecl_ ::= /* empty */
| constructorDecl list_constructorDecl_
list_decl_ ::= /* empty */
| decl list_decl_
list_decoration_ ::= /* empty */
| decoration list_decoration_
list_multiBinder_ ::= /* empty */
| multiBinder list_multiBinder_
nonempty_list_aqualifiedWithAttrs_lident__ ::= aqualifiedWithAttrs_lident_
| aqualifiedWithAttrs_lident_ nonempty_list_aqualifiedWithAttrs_lident__
nonempty_list_aqualifiedWithAttrs_lidentOrUnderscore__ ::= aqualifiedWithAttrs_lidentOrUnderscore_
| aqualifiedWithAttrs_lidentOrUnderscore_ nonempty_list_aqualifiedWithAttrs_lidentOrUnderscore__
nonempty_list_atomicPattern_ ::= atomicPattern
| atomicPattern nonempty_list_atomicPattern_
nonempty_list_atomicTerm_ ::= atomicTerm
| atomicTerm nonempty_list_atomicTerm_
nonempty_list_atomicUniverse_ ::= atomicUniverse
| atomicUniverse nonempty_list_atomicUniverse_
nonempty_list_dotOperator_ ::= DOT_LPAREN term RPAREN
| DOT_LBRACK term RBRACK
| DOT_LBRACK_BAR term BAR_RBRACK
| DOT_LENS_PAREN_LEFT term LENS_PAREN_RIGHT
| DOT_LPAREN term RPAREN nonempty_list_dotOperator_
| DOT_LBRACK term RBRACK nonempty_list_dotOperator_
| DOT_LBRACK_BAR term BAR_RBRACK nonempty_list_dotOperator_
| DOT_LENS_PAREN_LEFT term LENS_PAREN_RIGHT nonempty_list_dotOperator_
nonempty_list_patternOrMultibinder_ ::= patternOrMultibinder
| patternOrMultibinder nonempty_list_patternOrMultibinder_
separated_nonempty_list_AND_letbinding_ ::= letbinding
| letbinding AND separated_nonempty_list_AND_letbinding_
separated_nonempty_list_AND_typeDecl_ ::= typeDecl
| typeDecl AND separated_nonempty_list_AND_typeDecl_
separated_nonempty_list_BAR_tuplePattern_ ::= tuplePattern
| tuplePattern BAR separated_nonempty_list_BAR_tuplePattern_
separated_nonempty_list_COMMA_appTerm_ ::= appTerm
| appTerm COMMA separated_nonempty_list_COMMA_appTerm_
separated_nonempty_list_COMMA_atomicTerm_ ::= atomicTerm
| atomicTerm COMMA separated_nonempty_list_COMMA_atomicTerm_
separated_nonempty_list_COMMA_constructorPattern_ ::= constructorPattern
| constructorPattern COMMA separated_nonempty_list_COMMA_constructorPattern_
separated_nonempty_list_COMMA_tmEq_ ::= tmEq
| tmEq COMMA separated_nonempty_list_COMMA_tmEq_
separated_nonempty_list_COMMA_tvar_ ::= tvar
| tvar COMMA separated_nonempty_list_COMMA_tvar_
separated_nonempty_list_DISJUNCTION_conjunctivePat_ ::= conjunctivePat
| conjunctivePat DISJUNCTION separated_nonempty_list_DISJUNCTION_conjunctivePat_
separated_nonempty_list_SEMICOLON_appTerm_ ::= appTerm
| appTerm SEMICOLON separated_nonempty_list_SEMICOLON_appTerm_
separated_nonempty_list_SEMICOLON_effectDecl_ ::= effectDecl
| effectDecl SEMICOLON separated_nonempty_list_SEMICOLON_effectDecl_
separated_nonempty_list_SEMICOLON_ident_ ::= ident
| ident SEMICOLON separated_nonempty_list_SEMICOLON_ident_
separated_nonempty_list_SEMICOLON_tuplePattern_ ::= tuplePattern
| tuplePattern SEMICOLON separated_nonempty_list_SEMICOLON_tuplePattern_
// Tokens
//Hashtbl.add keywords \("[^"]+"\)\s+\(\S+\)\s+;
ATTRIBUTES ::= "attributes"
NOEQUALITY ::= "noeq"
UNOPTEQUALITY ::= "unopteq"
AND ::= "and"
ASSERT ::= "assert"
ASSUME ::= "assume"
BEGIN ::= "begin"
BY ::= "by"
CALC ::= "calc"
CLASS ::= "class"
DEFAULT ::= "default"
DECREASES ::= "decreases"
EFFECT ::= "effect"
ELIM ::= "eliminate"
ELSE ::= "else"
END ::= "end"
ENSURES ::= "ensures"
EXCEPTION ::= "exception"
EXISTS ::= "exists"
FALSE ::= "false"
FRIEND ::= "friend"
FORALL ::= "forall"
FUN ::= "fun"
FUN ::= "λ"
FUNCTION ::= "function"
IF ::= "if"
IN ::= "in"
INCLUDE ::= "include"
INLINE ::= "inline"
INLINE_FOR_EXTRACTION ::= "inline_for_extraction"
INSTANCE ::= "instance"
INTRO ::= "introduce"
IRREDUCIBLE ::= "irreducible"
LET ::= "let" // (LET false) ;
LOGIC ::= "logic"
MATCH ::= "match"
RETURNS ::= "returns"
AS ::= "as"
MODULE ::= "module"
NEW ::= "new"
NEW_EFFECT ::= "new_effect"
LAYERED_EFFECT ::= "layered_effect"
POLYMONADIC_BIND ::= "polymonadic_bind"
POLYMONADIC_SUBCOMP ::= "polymonadic_subcomp"
NOEXTRACT ::= "noextract"
OF ::= "of"
OPEN ::= "open"
OPAQUE ::= "opaque"
PRIVATE ::= "private"
QUOTE ::= "quote"
RANGE_OF ::= "range_of"
REC ::= "rec"
REIFIABLE ::= "reifiable"
REIFY ::= "reify"
REFLECTABLE ::= "reflectable"
REQUIRES ::= "requires"
SET_RANGE_OF ::= s "set_range_of"
SUB_EFFECT ::= "sub_effect"
SYNTH ::= "synth"
THEN ::= "then"
TOTAL ::= "total"
TRUE ::= "true"
TRY ::= "try"
TYPE ::= "type"
UNFOLD ::= "unfold"
UNFOLDABLE ::= "unfoldable"
VAL ::= "val"
WHEN ::= "when"
WITH ::= "with"
UNDERSCORE ::= "_"
//\("[^"]+"\),\s+\(\S+\)\s*;
TILDE::= "~"
MINUS ::= "-"
CONJUNCTION ::= "/\\"
DISJUNCTION ::= "\\/"
SUBTYPE ::= "<:"
EQUALTYPE ::= "$:"
SUBKIND ::= "<@"
LENS_PAREN_LEFT ::= "(|"
LENS_PAREN_RIGHT ::= "|)"
HASH ::= "#"
UNIV_HASH ::= "u#"
AMP ::= "&"
LPAREN_RPAREN ::= "()"
LPAREN ::= "("
RPAREN ::= ")"
COMMA ::= ","
SQUIGGLY_RARROW ::= "~>"
RARROW ::= "->"
LONG_LEFT_ARROW ::= "<--"
LARROW ::= "<-"
IFF ::= "<==>"
IMPLIES ::= "==>"
DOT ::= "."
QMARK_DOT ::= "?."
QMARK ::= "?"
DOT_LBRACK ::= ".["
DOT_LENS_PAREN_LEFT ::= ".(|"
DOT_LPAREN ::= ".("
DOT_LBRACK_BAR ::= ".[|"
LBRACE_COLON_PATTERN ::= "{:pattern"
LBRACE_COLON_WELL_FOUNDED ::= "{:well-founded"
RETURNS_EQ ::= "returns$"
COLON ::= ":"
COLON_COLON ::= "::"
COLON_EQUALS ::= ":="
SEMICOLON ::= ";"
EQUALS ::= "="
PERCENT_LBRACK ::= "%["
BANG_LBRACE ::= "!{"
LBRACK_AT_AT_AT ::= "[@@@"
LBRACK_AT_AT ::= "[@@"
LBRACK_AT ::= "[@"
LBRACK ::= "["
LBRACK_BAR ::= "[|"
LBRACE_BAR ::= "{|"
PIPE_RIGHT ::= "|>"
RBRACK ::= "]"
BAR_RBRACK ::= "|]"
BAR_RBRACE ::= "|}"
LBRACE ::= "{"
BAR ::= "|"
RBRACE ::= "}"
DOLLAR ::= "$"
//(* New Unicode equivalents *)
FORALL ::= "∀"
EXISTS ::= "∃"
//"⊤", NAME "True";
//"⊥", NAME "False";
IMPLIES ::= "⟹"
IFF ::= "⟺"
RARROW ::= "→"
LARROW ::= "←"
LONG_LEFT_ARROW ::= "⟵"
SQUIGGLY_RARROW ::= "↝"
COLON_EQUALS ::= "≔"
CONJUNCTION ::= "∧"
DISJUNCTION ::= "∨"
TILDE ::= "¬"
COLON_COLON ::= "⸬"
PIPE_RIGHT ::= "▹"
Using a custom parser for menhir grammars and applying it to
src/parser/parse.mlyand manually adding the tokens fromocaml/fstar-lib/FStar_Parser_LexFStar.mlwe can see a nice navigable railroad diagram .Copy and paste the EBNF shown bellow on https://www.bottlecaps.de/rr/ui in the tab
Edit Grammarthen switching to the tabView Diagram.