option(item) := (**) | item sep_or_term_list(item,sep) ::= nsepseq(item,sep) | nseq(item sep) (* Compound constructs *) par(item) ::= LPAR item RPAR brackets(item) ::= LBRACKET item RBRACKET (* Sequences *) (* Possibly empty sequence of items *) seq(item) ::= option(nseq(item)) (* Non-empty sequence of items *) nseq(item) ::= item seq(item) (* Non-empty separated sequence of items *) nsepseq(item,Sep) ::= item | item Sep nsepseq(item,Sep) (* Possibly empty separated sequence of items *) sepseq(item,Sep) ::= option(nsepseq(item,Sep)) (* Inlines *) var ::= Ident type_name ::= Ident fun_name ::= Ident field_name ::= Ident struct_name ::= Ident (* Main *) contract ::= nseq(declaration) EOF declaration ::= type_decl | const_decl | lambda_decl (* Type declarations *) type_decl ::= Type type_name Is type_expr option(SEMI) type_expr ::= cartesian | sum_type | record_type cartesian ::= nsepseq(function_type,TIMES) function_type ::= core_type | core_type ARROW function_type core_type ::= type_name | type_name type_tuple | Map type_tuple | Set par(type_expr) | List par(type_expr) | par(type_expr) type_tuple ::= par(nsepseq(type_expr,COMMA)) sum_type ::= option(VBAR) nsepseq(variant,VBAR) variant ::= Constr Of cartesian | Constr record_type ::= Record sep_or_term_list(field_decl,SEMI) End | Record LBRACKET sep_or_term_list(field_decl,SEMI) RBRACKET field_decl ::= field_name COLON type_expr (* Function and procedure declarations *) lambda_decl ::= fun_decl | proc_decl | entry_decl fun_decl ::= Function fun_name parameters COLON type_expr Is seq(local_decl) block With expr option(SEMI) entry_decl ::= Entrypoint fun_name entry_params COLON type_expr Is seq(local_decl) block With expr option(SEMI) entry_params ::= par(nsepseq(entry_param_decl,SEMI)) proc_decl ::= Procedure fun_name parameters Is seq(local_decl) block option(SEMI) parameters ::= par(nsepseq(param_decl,SEMI)) param_decl ::= Var var COLON param_type | Const var COLON param_type entry_param_decl ::= param_decl | Storage var COLON param_type param_type ::= cartesian block ::= Begin sep_or_term_list(statement,SEMI) End | Block LBRACE sep_or_term_list(statement,SEMI) RBRACE statement ::= instruction | open_data_decl open_data_decl ::= open_const_decl | open_var_decl open_const_decl ::= Const unqualified_decl(EQUAL) open_var_decl ::= Var unqualified_decl(ASS) local_decl ::= fun_decl | proc_decl | data_decl data_decl ::= const_decl | var_decl unqualified_decl(OP) ::= var COLON type_expr OP expr const_decl ::= open_const_decl SEMI | open_const_decl var_decl ::= open_var_decl SEMI | open_var_decl instruction ::= single_instr | block single_instr ::= conditional | case_instr | assignment | loop | proc_call | fail_instr | Skip | record_patch | map_patch | set_patch | map_remove | set_remove set_remove ::= Remove expr From Set path map_remove ::= Remove expr From Map path set_patch ::= Patch path With injection(Set,expr) map_patch ::= Patch path With injection(Map,binding) injection(Kind,element) ::= Kind sep_or_term_list(element,SEMI) End | Kind End | Kind LBRACKET sep_or_term_list(element,SEMI) RBRACKET | Kind LBRACKET RBRACKET binding ::= expr ARROW expr record_patch ::= Patch path With record_expr fail_instr ::= Fail expr proc_call ::= fun_call conditional ::= If expr Then if_clause option(SEMI) Else if_clause if_clause ::= instruction | LBRACE sep_or_term_list(statement,COMMA) RBRACE case_instr ::= case(instruction) case(rhs) ::= Case expr Of option(VBAR) cases(rhs) End | Case expr Of LBRACKET option(VBAR) cases(rhs) RBRACKET cases(rhs) ::= nsepseq(case_clause(rhs),VBAR) case_clause(rhs) ::= pattern ARROW rhs assignment ::= lhs ASS rhs rhs ::= expr lhs ::= path | map_lookup loop ::= while_loop | for_loop while_loop ::= While expr block for_loop ::= For var_assign option(Down) To expr option(step_clause) block | For var option(arrow_clause) In expr block var_assign ::= var ASS expr step_clause ::= Step expr arrow_clause ::= ARROW var (* Expressions *) interactive_expr ::= expr EOF expr ::= case(expr) | disj_expr disj_expr ::= disj_expr Or conj_expr | conj_expr conj_expr ::= conj_expr And set_membership | set_membership set_membership ::= core_expr Contains set_membership | comp_expr comp_expr ::= comp_expr LT cat_expr | comp_expr LEQ cat_expr | comp_expr GT cat_expr | comp_expr GEQ cat_expr | comp_expr EQUAL cat_expr | comp_expr NEQ cat_expr | cat_expr cat_expr ::= cons_expr CAT cat_expr | cons_expr cons_expr ::= add_expr CONS cons_expr | add_expr add_expr ::= add_expr PLUS mult_expr | add_expr MINUS mult_expr | mult_expr mult_expr ::= mult_expr TIMES unary_expr | mult_expr SLASH unary_expr | mult_expr Mod unary_expr | unary_expr unary_expr ::= MINUS core_expr | Not core_expr | core_expr core_expr ::= Int | Nat | Mutez | var | String | Bytes | C_False | C_True | C_Unit | annot_expr | tuple_expr | list_expr | C_None | fun_call | map_expr | set_expr | record_expr | projection | Constr arguments | Constr | C_Some arguments annot_expr ::= LPAR disj_expr COLON type_expr RPAR set_expr ::= injection(Set,expr) map_expr ::= map_lookup | injection(Map,binding) map_lookup ::= path brackets(expr) path ::= var | projection projection ::= struct_name DOT nsepseq(selection,DOT) selection ::= field_name | Int record_expr ::= Record sep_or_term_list(field_assignment,SEMI) End | Record LBRACKET sep_or_term_list(field_assignment,SEMI) RBRACKET field_assignment ::= field_name EQUAL expr fun_call ::= fun_name arguments tuple_expr ::= tuple_inj tuple_inj ::= par(nsepseq(expr,COMMA)) arguments ::= tuple_inj list_expr ::= injection(List,expr) | Nil (* Patterns *) pattern ::= nsepseq(core_pattern,CONS) core_pattern ::= var | WILD | Int | String | C_Unit | C_False | C_True | C_None | list_pattern | tuple_pattern | constr_pattern | C_Some par(core_pattern) list_pattern ::= injection(List,core_pattern) | Nil | par(cons_pattern) cons_pattern ::= core_pattern CONS pattern tuple_pattern ::= par(nsepseq(core_pattern,COMMA)) constr_pattern ::= Constr tuple_pattern | Constr