right_assoc(item,op) ::=
  item
| item op right_assoc(item,op)

left_assoc(item,op) ::=
  right_assoc(item,op)

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

   LL(1) constraint: item not in Follow(seq), where
   Follow(seq) = Follow(nseq) = {EOF, Begin, Block}
*)

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)

(* Main *)

contract ::=
  nseq(declaration) EOF

(* LL(1) constraint: SEMI not in Follow(declaration), where
   Follow(declaration)
      = {EOF} U First(declaration)
      = {EOF} U First(type_decl)
        U First(const_decl) U First(lambda_decl)
      = {EOF} U {Type} U {Const} U First(fun_decl)
        U First(proc_decl) U First(entry_decl)
      = {EOF,Type,Const,Function,Procedure,Entrypoint}.
*)

declaration ::=
  type_decl   option(SEMI)
| const_decl  option(SEMI)
| lambda_decl option(SEMI)

(* Type declarations *)

type_decl ::=
  Type Ident Is type_expr

type_expr ::=
  cartesian
| nsepseq(variant,VBAR)
| VBAR nsepseq(variant,VBAR)
| Record record_type_expr

record_type_expr ::=
  series(field_decl,SEMI,End)
| LBRACKET series(field_decl,SEMI,RBRACKET)

(* LL(1) constraint: Of not in Follow(variant).
   "Of" only occurs after {Constr, expr}. *)

variant ::=
  Constr option(of_cartesian)

of_cartesian ::=
  Of cartesian

cartesian ::=
  nsepseq(function_type,TIMES)

function_type ::=
  right_assoc(core_type,ARROW)

(* LL(1) constraint: LPAR not in Follow(core_type), where
   Follow(core_type)
     = {ARROW} U Follow(function_type)
     = {ARROW} U {TIMES} U Follow(cartesian)
     = {ARROW,TIMES} U Follow(of_cartesian) U Follow(type_expr)
       U Follow(param_type)
     = {ARROW,TIMES} U Follow(variant)
       U {RPAR,COMMA,Is,EQUAL,ASS} U Follow(field_decl)
       U Follow(paren_expr_1) U Follow(type_decl)
       U Follow(param_decl) U Follow(entry_param_decl)
     = {ARROW,TIMES,RPAR,COMMA,Is,EQUAL,ASS,VBAR,
        SEMI,End,RBRACKET} U Follow(paren_expr)
        U {SEMI} U Follow(declaration)
     = {ARROW,TIMES,RPAR,COMMA,Is,EQUAL,ASS,VBAR,
        SEMI,End,RBRACKET,EOF,Type,Const,
        Function,Procedure,Entrypoint}.
*)

core_type ::=
  Ident (* type_name *) option(type_tuple)
| Map type_tuple
| Set par(type_expr)
| List par(type_expr)
| par(type_expr)

type_tuple ::=
  par(nsepseq(type_expr,COMMA))

field_decl ::=
  Ident (* field_name *) COLON type_expr

(* Function and procedure declarations *)

lambda_decl ::=
  fun_decl
| proc_decl
| entry_decl

fun_decl ::=
  Function Ident parameters COLON type_expr Is
    seq(local_decl)
    block
  With expr

entry_decl ::=
  Entrypoint Ident entry_params COLON type_expr Is
    seq(local_decl)
    block
  With expr

entry_params ::=
  par(nsepseq(entry_param_decl,SEMI))

proc_decl ::=
  Procedure Ident parameters Is
    seq(local_decl)
    block

parameters ::=
  par(nsepseq(param_decl,SEMI))

param_decl ::=
  Var   Ident COLON param_type
| Const Ident COLON param_type

entry_param_decl ::=
  param_decl
| Storage Ident COLON param_type

param_type ::=
  cartesian

block ::=
  Begin series(statement,SEMI,End)
| Block LBRACE series(statement,SEMI,RBRACE)

statement ::=
  instruction
| data_decl

data_decl ::=
  const_decl
| var_decl

const_decl ::=
  Const unqualified_decl(EQUAL)

var_decl ::=
  Var unqualified_decl(ASS)

(* LL(1) constraint: SEMI not in Follow(local_decl), where
   Follow(local_decl)
     = First(local_decl) U First(block)
     = First(fun_decl) U First(proc_decl) U First(data_decl)
       U {BEGIN,Block}
     = {Function,Procedure,BEGIN,Block} U First(const_decl)
       U First(var_decl)
     = {Function,Procedure,BEGIN,Block,Const,Var}.
*)

local_decl ::=
  fun_decl  option(SEMI)
| proc_decl option(SEMI)
| data_decl option(SEMI)

unqualified_decl(op) ::=
  Ident (* var *) COLON type_expr op expr

instruction ::=
  block
| If expr Then if_clause option(SEMI) Else if_clause
| case(instruction)
| Ident instruction_1
| loop
| Fail expr
| Skip
| Patch path With structure
| Remove expr From remove_suffix

remove_suffix ::=
  Map path
| Set path

instruction_1 ::=
  arguments
| ASS expr
| brackets(expr) ASS expr
| selections option(brackets(expr)) ASS expr

(* LL(1) constraint: First(selections) not in Follow(path), where
   First(selections) = {DOT} and
   Follow(path)
     = {With} U Follow(remove_suffix)
     = {With} U Follow(instruction)
     = {With} U Follow(statement) U Follow(if_clause)
       U Follow(case_clause(instruction))
     = {With,SEMI,End,Else,VBAR} U Follow(cases(instruction))
     = {With,SEMI,End,Else,VBAR,RBRACKET}.
*)

path ::=
  Ident option(selections)

selections ::=
  DOT nsepseq(selection,DOT)

injection(Kind,element) ::=
  Kind inj_sufffix(element)

inj_suffix(element) ::=
  series(element,SEMI,End)
| End
| LBRACKET bracketed(element)

bracketed(element) ::=
  series(element,SEMI,RBRACKET)
| RBRACKET

binding ::=
  expr ARROW expr

if_clause ::=
  instruction
| LBRACE series(statement,COMMA,RBRACE)

case(rhs) ::=
  Case expr Of case_suffix(rhs)

case_suffix(rhs) ::=
  cases(rhs) End
| LBRACKET cases(rhs) RBRACKET

cases(rhs) ::=
  nsepseq(case_clause(rhs),VBAR)
| VBAR nsepseq(case_clause(rhs),VBAR)

case_clause(rhs) ::=
  pattern ARROW rhs

loop ::=
  While expr block
| For Ident for_suffix

for_suffix ::=
  ASS expr option(Down) To expr option(step_clause) block
| In expr block
| ARROW Ident In expr block

step_clause ::=
  Step expr

(* Expressions *)

interactive_expr ::=
  expr EOF

expr ::=
  case(expr)
| disj_expr

disj_expr ::=
  left_assoc(conj_expr,Or)

conj_expr ::=
  left_assoc(set_membership,And)

set_membership ::=
  comp_expr option(contains_clause)  (* Enlarged the language *)

contains_clause ::=
  Contains set_membership

comp_expr ::=
  left_assoc(cat_expr,op_comp)

op_comp ::=
  LT | LEQ | GT | GEQ | EQUAL | NEQ

cat_expr ::=
  right_assoc(cons_expr,CAT)

cons_expr ::=
  left_assoc(add_expr,CONS)

add_expr ::=
  left_assoc(mult_expr,add_op)

add_op ::=
  PLUS | MINUS

mult_expr ::=
  left_assoc(unary_expr,mult_op)

mult_op ::=
  TIMES | SLASH | Mod

unary_expr ::=
  MINUS core_expr
| Not core_expr
| core_expr

(* LL(1) constraint: First(core_suffix) not in Follow(core_expr)
   First(core_suffix) =

XXX
*)
core_expr ::=
  Int
| Nat
| Mtz
| Ident option(core_suffix)
| String
| Bytes
| C_False
| C_True
| C_Unit
| C_None
| C_Some arguments
| Constr option(arguments)
| par(paren_expr)
| injection(List,expr)
| Nil
| structure

core_suffix ::=
  brackets(expr) (* lookup *)
| DOT nsepseq(selection,DOT) option(brackets(expr))
| arguments

paren_expr ::=
  disj_expr option(paren_expr_1)
| case(expr) option(paren_expr_2)

paren_expr_1 ::=
  COLON type_expr
| COMMA nsepseq(expr,COMMA)

paren_expr_2 ::=
  COMMA nsepseq(expr,COMMA)

structure ::=
  injection(Map,binding)
| injection(Set,expr)
| record_expr

selection ::=
  Ident (* field_name *)
| Int

record_expr ::=
  Record record_expr_suffix

record_expr_suffix ::=
  series(field_assignment,SEMI,End)
| LBRACKET series(field_assignment,SEMI,RBRACKET)

field_assignment ::=
  Ident (* field_name *) EQUAL expr

arguments ::=
  par(nsepseq(expr,COMMA))

(* Patterns *)

pattern ::=
  nsepseq(core_pattern,CONS)

core_pattern ::=
  Ident (* var *)
| WILD
| Int
| String
| C_Unit
| C_False
| C_True
| C_None
| C_Some par(core_pattern)
| Constr option(tuple_pattern)
| injection(List,core_pattern)
| Nil
| par(option(paren_pattern))

paren_pattern ::=
  core_pattern paren_pattern_suffix

paren_pattern_suffix ::=
  CONS pattern
| COMMA nsepseq(core_pattern,COMMA)

tuple_pattern ::=
  par(nsepseq(core_pattern,COMMA))