tree-sitter-lean.ebnf

//
// From tree-sitter-lean/src/grammar.json
//
//
// EBNF to generate railroad diagram at 
//      (IPV6) https://www.bottlecaps.de/rr/ui
//      (IPV4) https://rr.red-dove.com/ui
//

module ::=
	 prelude? import* _command*

prelude ::=
	 'prelude'

import ::=
	 'import' identifier

parameters ::=
	 ( identifier | hole | _bracketed_binder | anonymous_constructor )+

_expression ::=
	 apply
	| comparison
	| let
	| tactics
	| binary_expression
	| neg
	| quoted_tactic
	| fun
	| _term
	| do
	| unless

let ::=
	 'let' identifier parameters? ( ':' _expression )? ':=' _expression ( _newline | ';' ) _expression?

_do_seq ::=
	 _do_element ( _newline _do_element )* _newline?

do ::=
	 'do' _do_seq

conditional_when ::=
	 'if' _expression 'then' _do_element

for_in ::=
	 'for' ( identifier | anonymous_constructor ) 'in' _expression do

assign ::=
	 identifier ':=' _expression

let_mut ::=
	 'let' 'mut' parameters ( _left_arrow | ':=' ) _expression

let_bind ::=
	 'let' identifier _left_arrow _expression

unless ::=
	 'unless' _expression do

try ::=
	 'try' _do_element ( _newline _do_element )* _newline? ( catch finally? | finally )

catch ::=
	 'catch' _expression '=>' _do_element ( _newline _do_element )* _newline?

finally ::=
	 'finally' _do_element ( _newline _do_element )* _newline?

fun ::=
	 ( 'fun' | 'λ' ) ( parameters '=>' _expression | ( '|' ( _expression ( ',' _expression )* ) '=>' _expression )* )

apply ::=
	 _apply
	| _dollar

_apply ::=
	 ( identifier | number | float | string | char | hole | synthetic_hole | sorry | cdot | parenthesized | anonymous_constructor | structure_instance | explicit | forall | true | false | borrowed | quoted_name | double_quoted_name | have | proj | arrow | _do_term | _command_term | _notation_term | _notation_extra_term | array | subarray | range | interpolated_string ) _argument+

_dollar ::=
	 _expression '$' _expression

neg ::=
	 '-' _expression

binary_expression ::=
	 _expression '^' _expression
	| _expression '*' _expression
	| _expression '/' _expression
	| _expression '%' _expression
	| _expression '+' _expression
	| _expression '-' _expression
	| _expression '∘' _expression
	| _expression '∧' _expression
	| _expression '∨' _expression
	| _expression '/\' _expression
	| _expression '\/' _expression
	| _expression '↔' _expression
	| _expression '||' _expression
	| _expression '&&' _expression
	| _expression '==' _expression
	| _expression '++' _expression
	| _expression '::' _expression
	| _expression '|>' _expression
	| _expression '|>.' _expression
	| _expression '<|' _expression
	| _expression '<|>' _expression
	| _expression '>>' _expression
	| _expression '>>=' _expression
	| _expression '<*>' _expression
	| _expression '<*' _expression
	| _expression '*>' _expression
	| _expression '<$>' _expression
	| _expression '=' _expression
	| _expression '≠' _expression

comparison ::=
	 _expression ( '<' | '>' | '≤' | '≥' | '<=' | '>=' ) _expression

comment ::=
	 ( '--' '.'* | '/-' ( [^-] | '-'[^/] )* '-/' )

_identifier ::=
	 [_a-zA-ZͰ-ϿĀ-ſ\U0001D400-\U0001D7FF][_`'`a-zA-Z0-9Ͱ-ϿĀ-ſ∇!?\u2070-\u209F\U0001D400-\U0001D7FF]*

_escaped_identifier ::=
	 '«'[^»]*'»'

_attribute ::=
	 _simple_attribute
	| _extern_attribute

_simple_attribute ::=
	 ( identifier identifier? )

_extern_entry ::=
	 identifier? 'inline'? string

_extern_attribute ::=
	 'extern' number? _extern_entry*

_visibility ::=
	 'private'
	| 'protected'

_decl_modifiers ::=
	 ( attributes ( 'noncomputable' | 'partial' | _visibility | 'unsafe' )+? | attributes? ( 'noncomputable' | 'partial' | _visibility | 'unsafe' )+ )

_decl_id ::=
	 identifier

_decl_sig ::=
	 _simple_binder_without_type | _bracketed_binder* _type_spec

_opt_decl_sig ::=
	 _simple_binder_without_type | _bracketed_binder+ _type_spec? | _simple_binder_without_type | _bracketed_binder+? _type_spec

_decl_val_simple ::=
	 ':=' _expression

_decl_val_equations ::=
	 _match_alts_where_decls

_decl_val ::=
	 ( _decl_val_simple | _decl_val_equations | _where_decls )

abbrev ::=
	 'abbrev' _decl_id _opt_decl_sig? _decl_val

def ::=
	 'def' _decl_id _opt_decl_sig? _decl_val

theorem ::=
	 'theorem' _decl_id _decl_sig _decl_val

constant ::=
	 'constant' _decl_id _decl_sig _decl_val_simple?

instance ::=
	 'instance' _decl_id? _decl_sig _decl_val

axiom ::=
	 'axiom' _decl_id _decl_sig

example ::=
	 'example' _decl_sig _decl_val

constructor ::=
	 '|' identifier _opt_decl_sig?

_deriving ::=
	 ( 'deriving' identifier ( ',' identifier )* )

inductive ::=
	 'inductive' _decl_id _opt_decl_sig? ( ':=' | 'where' )? constructor+? _deriving?

class_inductive ::=
	 'class' 'inductive' _decl_id _opt_decl_sig? ( ':=' | 'where' )? constructor+? _deriving?

_struct_explicit_binder ::=
	 '(' identifier+ _opt_decl_sig? _binder_default? ')'

_struct_implicit_binder ::=
	 '{' identifier+ _decl_sig '}'

_struct_instance_binder ::=
	 '[' identifier+ _decl_sig ']'

_struct_simple_binder ::=
	 identifier _opt_decl_sig? _binder_default?

_struct_field ::=
	 ( _struct_explicit_binder | _struct_implicit_binder | _struct_instance_binder | _struct_simple_binder )

_struct_constructor ::=
	 identifier '::'

_extends ::=
	 ( 'extends' _expression ( ',' _expression )* )

structure ::=
	 ( 'structure' | 'class' ) _decl_id _bracketed_binder* _extends? _type_spec? ( ( ':=' | 'where' ) _struct_constructor? _struct_field* )? _deriving?

declaration ::=
	 _decl_modifiers? ( abbrev | def | theorem | constant | instance | axiom | example | inductive | class_inductive | structure )

section ::=
	 'section' identifier? _command* 'end' identifier?

namespace ::=
	 'namespace' identifier _command* 'end' identifier

variable ::=
	 'variable' _bracketed_binder+

universe ::=
	 'universe' identifier+

hash_command ::=
	 ( '#check' | '#check_failure' | '#eval' | '#print' | '#reduce' ) _expression

attribute ::=
	 'attribute' '[' ( _attribute | '-' _attribute ) ( ',' ( _attribute | '-' _attribute ) )* ']' identifier

export ::=
	 'export' identifier '(' identifier+ ')'

open ::=
	 'open' identifier+ ( 'in' _command )?

quoted ::=
	 '`(' ( _term | _command+ ) ')'

_command_term ::=
	 quoted

builtin_initialize ::=
	 _visibility? 'builtin_initialize' ( identifier _type_spec _left_arrow )? _do_seq

_command ::=
	 declaration
	| section
	| namespace
	| variable
	| universe
	| hash_command
	| attribute
	| export
	| open
	| builtin_initialize
	| mixfix
	| notation
	| macro_rules
	| syntax
	| macro
	| elab

_precedence ::=
	 ':' ( number | 'max' | 'arg' | 'lead' | 'min' | 'min1' )

_syntax_cat ::=
	 identifier

_syntax_atom ::=
	 string

_syntax ::=
	 _syntax_cat
	| _syntax_atom

mixfix ::=
	 _attr_kind? ( 'prefix' | 'infix' | 'infixl' | 'infixr' | 'postfix' ) _precedence string '=>' _term

notation ::=
	 _attr_kind? 'notation' _expression '=>' _expression

macro_rules ::=
	 _attr_kind? 'macro_rules' _match_alts

syntax ::=
	 _attr_kind? 'syntax' _syntax+ ':' identifier

_macro_arg ::=
	 ( identifier ':' )? _syntax

_macro_tail_tactic ::=
	 ' : ' 'tactic' '=>' '`(' _tactic+ ')'

_macro_tail_command ::=
	 ' : ' 'command' '=>' '`(' _command+ ')'

_macro_tail_default ::=
	 ' : ' identifier '=>' '`(' ( _tactic | _command )+ ')'

_macro_tail ::=
	 _macro_tail_tactic
	| _macro_tail_command

macro ::=
	 _attr_kind? 'macro' _precedence? _macro_arg+ _macro_tail

_elab_arg ::=
	 _macro_arg

_elab_tail ::=
	 ':' identifier ( '<=' identifier )? '=>' _expression

elab ::=
	 _attr_kind? 'elab' _precedence? _elab_arg+ _elab_tail

tactics ::=
	 'by' _tactic ( ';'? _newline _tactic )* ( ';'? _newline )?

apply_tactic ::=
	 'apply' _expression

rewrite ::=
	 ( 'rewrite' | 'rw' ) _expression

term ::=
	 'exact' _expression

simp ::=
	 'simp' list?

trivial ::=
	 'trivial'

intro ::=
	 'intro' _expression*

rfl ::=
	 'rfl'

_user_tactic ::=
	 _expression

_tactic ::=
	 apply_tactic
	| rewrite
	| simp
	| term
	| trivial
	| intro
	| rfl
	| _user_tactic

quoted_char ::=
	 ( '\\'  ( 'u'[a-fA-F0-9]'{4}' | 'x'[a-fA-F0-9]'{2}' | [\"'rnt] ) )

_left_arrow ::=
	 '<-'
	| '←'

do_return ::=
	 'return' _expression?

_do_expression ::=
	 _expression

_do_element ::=
	 _do_expression
	| assign
	| for_in
	| let_bind
	| let_mut
	| do_return

identifier ::=
	 _identifier ( '.' _identifier )*
	| _identifier
	| _escaped_identifier

number ::=
	 [0-9]+

float ::=
	 [0-9]+'.'[0-9]*

string ::=
	 '"'  ( quoted_char | [^"#x0A\]+ )* '"' 

char ::=
	 "'"  ( quoted_char | [^'] ) "'" 

hole ::=
	 '_'

synthetic_hole ::=
	 '?' ( identifier | hole )

sorry ::=
	 'sorry'

cdot ::=
	 '.'
	| '·'

type_ascription ::=
	 ':' _expression

tuple_tail ::=
	 ',' _expression ( ',' _expression )*

parenthesized ::=
	 '(' ( _expression ( tuple_tail | type_ascription )? )? ')'

anonymous_constructor ::=
	 '⟨' ( _expression ( ',' _expression )* )? '⟩'

_structure_instance_field ::=
	 identifier ':=' _expression

structure_instance ::=
	 '{' ( _expression 'with' )? ( _structure_instance_field ( ',' _structure_instance_field )* ','? )? _type_spec? '}'

_type_spec ::=
	 ( ':' _expression )

explicit ::=
	 '@' _term

_binder_ident ::=
	 identifier
	| hole

_binder_default ::=
	 ( ':=' _expression )

explicit_binder ::=
	 '(' _binder_ident+ _type_spec? ( _binder_default )? ')'

implicit_binder ::=
	 '{' _binder_ident+ _type_spec? '}'

instance_binder ::=
	 '[' ( identifier ':' )? _expression ']'

_bracketed_binder ::=
	 explicit_binder
	| implicit_binder
	| instance_binder

proj ::=
	 _term '.' ( identifier | number )

arrow ::=
	 _term ( '->' | '→' ) _expression

forall ::=
	 '∀' ( _simple_binder | _bracketed_binder )+ ',' _expression

_simple_binder ::=
	 _binder_ident+ _type_spec?

match_alt ::=
	 '|' ( _expression ( ',' _expression )* ) '=>' _expression

_match_alts ::=
	 match_alt+

_match_discr ::=
	 ( identifier ':' )? _expression

true ::=
	 'true'

false ::=
	 'false'

match ::=
	 'match' ( _match_discr ( ', ' _match_discr )* ) _type_spec? 'with' _match_alts

borrowed ::=
	 '@&' _term

quoted_name ::=
	 '`' identifier

double_quoted_name ::=
	 '``' identifier

_simple_binder_without_type ::=
	 _binder_ident+

_let_id_lhs ::=
	 identifier ( _simple_binder_without_type | _bracketed_binder )* _type_spec?

_let_id_decl ::=
	 _let_id_lhs ':=' _expression

_let_pattern_decl ::=
	 _term _type_spec? ':=' _expression

_let_equations_decl ::=
	 _let_id_lhs _match_alts

_let_decl ::=
	 _let_id_decl
	| _let_pattern_decl
	| _let_equations_decl

_have_id_lhs ::=
	 identifier ( _simple_binder_without_type | _bracketed_binder )* _type_spec?
	| ( identifier ( _simple_binder_without_type | _bracketed_binder )* )? _type_spec

_have_id_decl ::=
	 _have_id_lhs? ':=' _term

_have_eqns_decl ::=
	 _have_id_lhs? _match_alts

_have_decl ::=
	 _have_id_decl
	| _let_pattern_decl
	| _have_eqns_decl

have ::=
	 'have' _have_decl ';'? _term

_attr_kind ::=
	 'scoped'
	| 'local'

_attr_instance ::=
	 _attr_kind? _attribute

attributes ::=
	 '@[' _attr_instance ( ',' _attr_instance )* ']'

_let_rec_decl ::=
	 _let_decl

_where_decls ::=
	 'where' ( _let_rec_decl )+

_match_alts_where_decls ::=
	 _match_alts _where_decls?

named_argument ::=
	 '(' identifier ':=' _expression ')'

ellipsis ::=
	 '..'

_argument ::=
	 named_argument
	| ellipsis
	| _expression

quoted_tactic ::=
	 '`(tactic|' _tactic ')'

_term ::=
	 identifier
	| number
	| float
	| string
	| char
	| hole
	| synthetic_hole
	| sorry
	| cdot
	| parenthesized
	| anonymous_constructor
	| structure_instance
	| explicit
	| forall
	| true
	| false
	| match
	| borrowed
	| quoted_name
	| double_quoted_name
	| have
	| proj
	| arrow
	| _do_term
	| _command_term
	| _notation_term
	| _notation_extra_term
	| array
	| subarray
	| range
	| interpolated_string

lift_method ::=
	 _left_arrow _term

_do_term ::=
	 lift_method

product ::=
	 _term '×' _term

unary_expression ::=
	 ( '¬' | '!' ) _term

subtype ::=
	 '{' identifier ( ':' _term )? '//' _expression '}'

list ::=
	 '[' ( _expression ( ',' _expression )* )? ']'

assumption_literal ::=
	 '‹' _term '›'

if_then_else ::=
	 'if' _expression 'then' _expression 'else' _expression

_notation_term ::=
	 product
	| unary_expression
	| subtype
	| if_then_else
	| list
	| assumption_literal

exists ::=
	 '∃' ( _simple_binder | _bracketed_binder )+ ',' _expression

_notation_extra_term ::=
	 exists

array ::=
	 '#[' ( _expression ( ',' _expression )* )? ']'

subarray ::=
	 _expression '[' ( _expression | _expression? ':' _expression | _expression ':' _expression? ) ']'

range ::=
	 '[' _expression? ':' _expression ( ':' _expression )? ']'

interpolated_string ::=
	 's!"' ( [^"] | quoted_char | interpolation )* '"' 

interpolation ::=
	 '{' _expression '}'