diff --git a/src/parser/pascaligo/Doc/pascaligo1.bnf b/src/parser/pascaligo/Doc/pascaligo1.bnf new file mode 100644 index 000000000..2ca145d99 --- /dev/null +++ b/src/parser/pascaligo/Doc/pascaligo1.bnf @@ -0,0 +1,436 @@ +option(X) := + (**) +| X + +sep_or_term_list(item,sep) ::= + nsepseq(item,sep) +| nseq(item sep) + +(* Compound constructs *) + +par(X) ::= LPAR X RPAR + +brackets(X) ::= LBRACKET X RBRACKET + +(* Sequences *) + +(* Possibly empty sequence of items *) + +seq(X) ::= + (**) +| X seq(X) + +(* Non-empty sequence of items *) + +nseq(X) ::= X seq(X) + +(* Non-empty separated sequence of items *) + +nsepseq(X,Sep) ::= + X +| X Sep nsepseq(X,Sep) + +(* Possibly empy separated sequence of items *) + +sepseq(X,Sep) ::= + (**) +| nsepseq(X,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 extended_expr + +const_decl ::= + open_const_decl SEMI +| open_const_decl + +var_decl ::= + open_var_decl SEMI +| open_var_decl + +extended_expr ::= + expr + +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) +| annot_expr + +annot_expr ::= + LPAR disj_expr COLON type_expr RPAR +| 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 +| var +| String +| Bytes +| C_False +| C_True +| C_Unit +| tuple_expr +| list_expr +| C_None +| fun_call +| map_expr +| set_expr +| record_expr +| projection +| Constr arguments +| Constr +| C_Some arguments + +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 diff --git a/src/parser/pascaligo/Doc/pascaligo2.bnf b/src/parser/pascaligo/Doc/pascaligo2.bnf new file mode 100644 index 000000000..0508b4409 --- /dev/null +++ b/src/parser/pascaligo/Doc/pascaligo2.bnf @@ -0,0 +1,442 @@ +option(X) := + (**) +| X + +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(X) ::= LPAR X RPAR + +brackets(X) ::= LBRACKET X RBRACKET + +(* Sequences *) + +(* Possibly empty sequence of items *) + +seq(X) ::= + (**) +| X seq(X) + +(* Non-empty sequence of items *) + +nseq(X) ::= X seq(X) + +(* Non-empty separated sequence of items *) + +nsepseq(X,Sep) ::= + X +| X Sep nsepseq(X,Sep) + +(* Possibly empy separated sequence of items *) + +sepseq(X,Sep) ::= + (**) +| nsepseq(X,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 series(field_decl,SEMI,End) +| Record LBRACKET series(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 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) ::= + var COLON type_expr OP extended_expr + +const_decl ::= + open_const_decl SEMI +| open_const_decl + +var_decl ::= + open_var_decl option(SEMI) + +extended_expr ::= + expr + +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 series(element,SEMI,End) +| Kind End +| Kind LBRACKET series(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 series(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) +| annot_expr + +annot_expr ::= + LPAR disj_expr COLON type_expr RPAR +| 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 +| var +| String +| Bytes +| C_False +| C_True +| C_Unit +| tuple_expr +| list_expr +| C_None +| fun_call +| map_expr +| set_expr +| record_expr +| projection +| Constr arguments +| Constr +| C_Some arguments + +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 series(field_assignment,SEMI,End) +| Record LBRACKET series(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 diff --git a/src/parser/pascaligo/Doc/pascaligo3.bnf b/src/parser/pascaligo/Doc/pascaligo3.bnf new file mode 100644 index 000000000..c75e7605e --- /dev/null +++ b/src/parser/pascaligo/Doc/pascaligo3.bnf @@ -0,0 +1,421 @@ +option(X) := + (**) +| X + +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(X) ::= LPAR X RPAR + +brackets(X) ::= LBRACKET X RBRACKET + +(* Sequences *) + +(* Possibly empty sequence of items *) + +seq(X) ::= + (**) +| X seq(X) + +(* Non-empty sequence of items *) + +nseq(X) ::= X seq(X) + +(* Non-empty separated sequence of items *) + +nsepseq(X,Sep) ::= + X +| X Sep nsepseq(X,Sep) + +(* Possibly empy separated sequence of items *) + +sepseq(X,Sep) ::= + (**) +| nsepseq(X,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 extended_expr + +const_decl ::= + open_const_decl SEMI +| open_const_decl + +var_decl ::= + open_var_decl option(SEMI) + +extended_expr ::= + expr + +instruction ::= + single_instr +| block + +single_instr ::= + conditional +| case_instr +| assignment +| loop +| proc_call +| fail_instr +| Skip +| record_patch +| 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 + +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 series(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 Ident (* var *) option(arrow_clause) In expr block + +var_assign ::= + Ident (* var *) ASS expr + +step_clause ::= + Step expr + +arrow_clause ::= + ARROW Ident (* var *) + +(* Expressions *) + +interactive_expr ::= + expr EOF + +expr ::= + case(expr) +| annot_expr + +annot_expr ::= + LPAR disj_expr COLON type_expr RPAR +| 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 +| tuple_expr +| list_expr +| C_None +| fun_call +| map_expr +| set_expr +| record_expr +| projection +| Constr arguments +| Constr +| C_Some arguments + +set_expr ::= + injection(Set,expr) + +map_expr ::= + map_lookup +| injection(Map,binding) + +map_lookup ::= + path brackets(expr) + +path ::= + Ident (* var *) +| projection + +projection ::= + 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 diff --git a/src/parser/pascaligo/Doc/pascaligo4.bnf b/src/parser/pascaligo/Doc/pascaligo4.bnf new file mode 100644 index 000000000..960dc9737 --- /dev/null +++ b/src/parser/pascaligo/Doc/pascaligo4.bnf @@ -0,0 +1,396 @@ +option(X) := + (**) +| X + +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(X) ::= LPAR X RPAR + +brackets(X) ::= LBRACKET X RBRACKET + +(* Sequences *) + +(* Possibly empty sequence of items *) + +seq(X) ::= + (**) +| X seq(X) + +(* Non-empty sequence of items *) + +nseq(X) ::= X seq(X) + +(* Non-empty separated sequence of items *) + +nsepseq(X,Sep) ::= + X +| X Sep nsepseq(X,Sep) + +(* Possibly empy separated sequence of items *) + +sepseq(X,Sep) ::= + (**) +| nsepseq(X,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 extended_expr + +const_decl ::= + open_const_decl option(SEMI) + +var_decl ::= + open_var_decl option(SEMI) + +extended_expr ::= + expr + +instruction ::= + single_instr +| block + +single_instr ::= + If expr Then if_clause option(SEMI) Else if_clause +| case(instruction) +| path ASS expr +| path brackets(expr) (* map_lookup *) ASS expr +| loop +| proc_call +| 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 + +proc_call ::= + fun_call + +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 var_assign option(Down) To expr option(step_clause) block +| For Ident (* var *) option(arrow_clause) In expr block + +var_assign ::= + Ident (* var *) ASS expr + +step_clause ::= + Step expr + +arrow_clause ::= + ARROW Ident (* var *) + +(* Expressions *) + +interactive_expr ::= + expr EOF + +expr ::= + case(expr) +| annot_expr + +annot_expr ::= + LPAR disj_expr COLON type_expr RPAR +| 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 +| 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 + +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 diff --git a/src/parser/pascaligo/Doc/pascaligo5.bnf b/src/parser/pascaligo/Doc/pascaligo5.bnf new file mode 100644 index 000000000..5f3da6828 --- /dev/null +++ b/src/parser/pascaligo/Doc/pascaligo5.bnf @@ -0,0 +1,390 @@ +option(X) := + (**) +| X + +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(X) ::= LPAR X RPAR + +brackets(X) ::= LBRACKET X RBRACKET + +(* Sequences *) + +(* Possibly empty sequence of items *) + +seq(X) ::= + (**) +| X seq(X) + +(* Non-empty sequence of items *) + +nseq(X) ::= X seq(X) + +(* Non-empty separated sequence of items *) + +nsepseq(X,Sep) ::= + X +| X Sep nsepseq(X,Sep) + +(* Possibly empy separated sequence of items *) + +sepseq(X,Sep) ::= + (**) +| nsepseq(X,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 extended_expr + +const_decl ::= + open_const_decl option(SEMI) + +var_decl ::= + open_var_decl option(SEMI) + +extended_expr ::= + expr + +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) +| annot_expr + +annot_expr ::= + LPAR disj_expr COLON type_expr RPAR +| 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 +| 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 + +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