option(item) := (**) | item series(item,sep,term) ::= item after_item(item,sep,term) after_item(item,sep,term) ::= sep item_or_closing(item,sep,term) | term item_or_closing(item,sep,term) ::= term | series(item,sep,term) (* 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)) (* Main *) contract ::= nseq(declaration) EOF declaration ::= type_decl | const_decl | lambda_decl (* Type declarations *) type_decl ::= Type Ident (* 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 ::= Ident (* type_name *) | Ident (* 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 series(field_decl,SEMI,End) | Record LBRACKET series(field_decl,SEMI,RBRACKET) field_decl ::= Ident (* field_name *) COLON type_expr (* Function and procedure declarations *) lambda_decl ::= fun_decl | proc_decl | entry_decl fun_decl ::= Function Ident (* fun_name *) parameters COLON type_expr Is seq(local_decl) block With expr option(SEMI) entry_decl ::= Entrypoint Ident (* 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 Ident (* fun_name *) parameters Is seq(local_decl) block option(SEMI) parameters ::= par(nsepseq(param_decl,SEMI)) param_decl ::= Var Ident (* var *) COLON param_type | Const Ident (* var *) COLON param_type entry_param_decl ::= param_decl | Storage Ident (* var *) COLON param_type param_type ::= cartesian block ::= Begin series(statement,SEMI,End) | Block LBRACE series(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) ::= Ident (* var *) COLON type_expr OP expr const_decl ::= open_const_decl option(SEMI) var_decl ::= open_var_decl option(SEMI) instruction ::= single_instr | block single_instr ::= If expr Then if_clause option(SEMI) Else if_clause | case(instruction) | Ident (* proc_name *) arguments | Ident option(brackets(expr)) ASS expr | Ident DOT nsepseq(selection,DOT) option(brackets(expr)) ASS expr | loop | Fail expr | Skip | Patch path With record_expr | Patch path With injection(Map,binding) | Patch path With injection(Set,expr) | Remove expr From Map path | Remove expr From Set path injection(Kind,element) ::= Kind series(element,SEMI,End) | Kind End | Kind LBRACKET series(element,SEMI,RBRACKET) | Kind LBRACKET RBRACKET binding ::= expr ARROW expr if_clause ::= instruction | LBRACE series(statement,COMMA,RBRACE) 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 loop ::= while_loop | for_loop while_loop ::= While expr block for_loop ::= For Ident (* var *) ASS expr option(Down) To expr option(step_clause) block | For Ident (* var *) option(arrow_clause) In expr block step_clause ::= Step expr arrow_clause ::= ARROW Ident (* 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 | Mtz | Ident (* 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 | Ident (* struct_name *) DOT nsepseq(selection,DOT) | 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 ::= Ident (* var *) | Ident (* struct_name *) DOT nsepseq(selection,DOT) selection ::= Ident (* field_name *) | Int record_expr ::= Record series(field_assignment,SEMI,End) | Record LBRACKET series(field_assignment,SEMI,RBRACKET) field_assignment ::= Ident (* field_name *) EQUAL expr fun_call ::= Ident (* 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 ::= Ident (* 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