From bf50102810264a27551d11f212ab952063b5806b Mon Sep 17 00:00:00 2001 From: Christian Rinderknecht Date: Tue, 30 Jul 2019 14:24:26 +0200 Subject: [PATCH 01/14] Fixed expressions annotated with types (they are now allowed everywhere). --- src/parser/pascaligo/Doc/pascaligo_01.bnf | 8 +- src/parser/pascaligo/Doc/pascaligo_02.bnf | 8 +- src/parser/pascaligo/Doc/pascaligo_03.bnf | 8 +- src/parser/pascaligo/Doc/pascaligo_04.bnf | 8 +- src/parser/pascaligo/Doc/pascaligo_05.bnf | 8 +- src/parser/pascaligo/Doc/pascaligo_06.bnf | 8 +- src/parser/pascaligo/Doc/pascaligo_07.bnf | 8 +- src/parser/pascaligo/Doc/pascaligo_08.bnf | 8 +- src/parser/pascaligo/Doc/pascaligo_09.bnf | 8 +- src/parser/pascaligo/Doc/pascaligo_10.bnf | 8 +- src/parser/pascaligo/Doc/pascaligo_11.bnf | 8 +- src/parser/pascaligo/Doc/pascaligo_12.bnf | 30 +- src/parser/pascaligo/Doc/pascaligo_13.bnf | 347 ++++++++++++++++++++++ 13 files changed, 400 insertions(+), 65 deletions(-) create mode 100644 src/parser/pascaligo/Doc/pascaligo_13.bnf diff --git a/src/parser/pascaligo/Doc/pascaligo_01.bnf b/src/parser/pascaligo/Doc/pascaligo_01.bnf index 73babd213..551d23d3e 100644 --- a/src/parser/pascaligo/Doc/pascaligo_01.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_01.bnf @@ -281,10 +281,6 @@ interactive_expr ::= expr ::= case(expr) -| annot_expr - -annot_expr ::= - LPAR disj_expr COLON type_expr RPAR | disj_expr disj_expr ::= @@ -342,6 +338,7 @@ core_expr ::= | C_False | C_True | C_Unit +| annot_expr | tuple_expr | list_expr | C_None @@ -354,6 +351,9 @@ core_expr ::= | Constr | C_Some arguments +annot_expr ::= + LPAR disj_expr COLON type_expr RPAR + set_expr ::= injection(Set,expr) diff --git a/src/parser/pascaligo/Doc/pascaligo_02.bnf b/src/parser/pascaligo/Doc/pascaligo_02.bnf index 26c3add4a..a91bbdaff 100644 --- a/src/parser/pascaligo/Doc/pascaligo_02.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_02.bnf @@ -287,10 +287,6 @@ interactive_expr ::= expr ::= case(expr) -| annot_expr - -annot_expr ::= - LPAR disj_expr COLON type_expr RPAR | disj_expr disj_expr ::= @@ -348,6 +344,7 @@ core_expr ::= | C_False | C_True | C_Unit +| annot_expr | tuple_expr | list_expr | C_None @@ -360,6 +357,9 @@ core_expr ::= | Constr | C_Some arguments +annot_expr ::= + LPAR disj_expr COLON type_expr RPAR + set_expr ::= injection(Set,expr) diff --git a/src/parser/pascaligo/Doc/pascaligo_03.bnf b/src/parser/pascaligo/Doc/pascaligo_03.bnf index 8f4b6114a..8f8f7b9ee 100644 --- a/src/parser/pascaligo/Doc/pascaligo_03.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_03.bnf @@ -266,10 +266,6 @@ interactive_expr ::= expr ::= case(expr) -| annot_expr - -annot_expr ::= - LPAR disj_expr COLON type_expr RPAR | disj_expr disj_expr ::= @@ -327,6 +323,7 @@ core_expr ::= | C_False | C_True | C_Unit +| annot_expr | tuple_expr | list_expr | C_None @@ -339,6 +336,9 @@ core_expr ::= | Constr | C_Some arguments +annot_expr ::= + LPAR disj_expr COLON type_expr RPAR + set_expr ::= injection(Set,expr) diff --git a/src/parser/pascaligo/Doc/pascaligo_04.bnf b/src/parser/pascaligo/Doc/pascaligo_04.bnf index c1fcccc7b..c53d68517 100644 --- a/src/parser/pascaligo/Doc/pascaligo_04.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_04.bnf @@ -244,10 +244,6 @@ interactive_expr ::= expr ::= case(expr) -| annot_expr - -annot_expr ::= - LPAR disj_expr COLON type_expr RPAR | disj_expr disj_expr ::= @@ -305,6 +301,7 @@ core_expr ::= | C_False | C_True | C_Unit +| annot_expr | tuple_expr | list_expr | C_None @@ -317,6 +314,9 @@ core_expr ::= | Constr | C_Some arguments +annot_expr ::= + LPAR disj_expr COLON type_expr RPAR + set_expr ::= injection(Set,expr) diff --git a/src/parser/pascaligo/Doc/pascaligo_05.bnf b/src/parser/pascaligo/Doc/pascaligo_05.bnf index 9ddf65fcd..924a0ca30 100644 --- a/src/parser/pascaligo/Doc/pascaligo_05.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_05.bnf @@ -238,10 +238,6 @@ interactive_expr ::= expr ::= case(expr) -| annot_expr - -annot_expr ::= - LPAR disj_expr COLON type_expr RPAR | disj_expr disj_expr ::= @@ -299,6 +295,7 @@ core_expr ::= | C_False | C_True | C_Unit +| annot_expr | tuple_expr | list_expr | C_None @@ -311,6 +308,9 @@ core_expr ::= | Constr | C_Some arguments +annot_expr ::= + LPAR disj_expr COLON type_expr RPAR + set_expr ::= injection(Set,expr) diff --git a/src/parser/pascaligo/Doc/pascaligo_06.bnf b/src/parser/pascaligo/Doc/pascaligo_06.bnf index 0f8007966..30323f057 100644 --- a/src/parser/pascaligo/Doc/pascaligo_06.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_06.bnf @@ -241,10 +241,6 @@ interactive_expr ::= expr ::= case(expr) -| annot_expr - -annot_expr ::= - LPAR disj_expr COLON type_expr RPAR | disj_expr disj_expr ::= @@ -302,6 +298,7 @@ core_expr ::= | C_False | C_True | C_Unit +| annot_expr | tuple_expr | list_expr | C_None @@ -314,6 +311,9 @@ core_expr ::= | Constr | C_Some arguments +annot_expr ::= + LPAR disj_expr COLON type_expr RPAR + set_expr ::= injection(Set,expr) diff --git a/src/parser/pascaligo/Doc/pascaligo_07.bnf b/src/parser/pascaligo/Doc/pascaligo_07.bnf index 7d4b78f1b..263a64264 100644 --- a/src/parser/pascaligo/Doc/pascaligo_07.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_07.bnf @@ -231,10 +231,6 @@ interactive_expr ::= expr ::= case(expr) -| annot_expr - -annot_expr ::= - LPAR disj_expr COLON type_expr RPAR | disj_expr disj_expr ::= @@ -292,6 +288,7 @@ core_expr ::= | C_False | C_True | C_Unit +| annot_expr | tuple_expr | list_expr | C_None @@ -304,6 +301,9 @@ core_expr ::= | Constr | C_Some arguments +annot_expr ::= + LPAR disj_expr COLON type_expr RPAR + set_expr ::= injection(Set,expr) diff --git a/src/parser/pascaligo/Doc/pascaligo_08.bnf b/src/parser/pascaligo/Doc/pascaligo_08.bnf index b420288bb..524c29d82 100644 --- a/src/parser/pascaligo/Doc/pascaligo_08.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_08.bnf @@ -233,10 +233,6 @@ interactive_expr ::= expr ::= case(expr) -| annot_expr - -annot_expr ::= - LPAR disj_expr COLON type_expr RPAR | disj_expr disj_expr ::= @@ -294,6 +290,7 @@ core_expr ::= | C_False | C_True | C_Unit +| annot_expr | tuple_expr | list_expr | C_None @@ -306,6 +303,9 @@ core_expr ::= | Constr | C_Some arguments +annot_expr ::= + LPAR disj_expr COLON type_expr RPAR + set_expr ::= injection(Set,expr) diff --git a/src/parser/pascaligo/Doc/pascaligo_09.bnf b/src/parser/pascaligo/Doc/pascaligo_09.bnf index b08424594..e74409cb2 100644 --- a/src/parser/pascaligo/Doc/pascaligo_09.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_09.bnf @@ -236,10 +236,6 @@ interactive_expr ::= expr ::= case(expr) -| annot_expr - -annot_expr ::= - LPAR disj_expr COLON type_expr RPAR | disj_expr disj_expr ::= @@ -297,6 +293,7 @@ core_expr ::= | C_False | C_True | C_Unit +| annot_expr | tuple_expr | list_expr | C_None @@ -309,6 +306,9 @@ core_expr ::= | Constr | C_Some arguments +annot_expr ::= + LPAR disj_expr COLON type_expr RPAR + set_expr ::= injection(Set,expr) diff --git a/src/parser/pascaligo/Doc/pascaligo_10.bnf b/src/parser/pascaligo/Doc/pascaligo_10.bnf index b33ff4778..b9b555ba0 100644 --- a/src/parser/pascaligo/Doc/pascaligo_10.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_10.bnf @@ -237,10 +237,6 @@ interactive_expr ::= expr ::= case(expr) -| annot_expr - -annot_expr ::= - LPAR disj_expr COLON type_expr RPAR | disj_expr disj_expr ::= @@ -292,6 +288,7 @@ core_expr ::= | C_False | C_True | C_Unit +| annot_expr | tuple_expr | list_expr | C_None @@ -304,6 +301,9 @@ core_expr ::= | Constr | C_Some arguments +annot_expr ::= + LPAR disj_expr COLON type_expr RPAR + set_expr ::= injection(Set,expr) diff --git a/src/parser/pascaligo/Doc/pascaligo_11.bnf b/src/parser/pascaligo/Doc/pascaligo_11.bnf index 6155fba3b..07e980fb3 100644 --- a/src/parser/pascaligo/Doc/pascaligo_11.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_11.bnf @@ -235,10 +235,6 @@ interactive_expr ::= expr ::= case(expr) -| annot_expr - -annot_expr ::= - LPAR disj_expr COLON type_expr RPAR | disj_expr disj_expr ::= @@ -293,6 +289,7 @@ core_expr ::= | C_False | C_True | C_Unit +| annot_expr | tuple_expr | list_expr | C_None @@ -302,6 +299,9 @@ core_expr ::= | Constr | C_Some arguments +annot_expr ::= + LPAR disj_expr COLON type_expr RPAR + structure ::= injection(Map,binding) | injection(Set,expr) diff --git a/src/parser/pascaligo/Doc/pascaligo_12.bnf b/src/parser/pascaligo/Doc/pascaligo_12.bnf index b4f1972c5..2b959b4cc 100644 --- a/src/parser/pascaligo/Doc/pascaligo_12.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_12.bnf @@ -186,6 +186,10 @@ single_instr ::= | Remove expr From Map path | Remove expr From Set path +path ::= + Ident (* var *) +| Ident (* struct_name *) DOT nsepseq(selection,DOT) + injection(Kind,element) ::= Kind series(element,SEMI,End) | Kind End @@ -235,10 +239,6 @@ interactive_expr ::= expr ::= case(expr) -| annot_expr - -annot_expr ::= - LPAR disj_expr COLON type_expr RPAR | disj_expr disj_expr ::= @@ -296,8 +296,10 @@ core_expr ::= | C_None | C_Some arguments | Constr option(arguments) -| tuple_expr -| list_expr +| LPAR disj_expr COLON type_expr RPAR +| par(nsepseq(expr,COMMA)) +| injection(List,expr) +| Nil | structure structure ::= @@ -305,10 +307,6 @@ structure ::= | injection(Set,expr) | record_expr -path ::= - Ident (* var *) -| Ident (* struct_name *) DOT nsepseq(selection,DOT) - selection ::= Ident (* field_name *) | Int @@ -320,18 +318,8 @@ record_expr ::= field_assignment ::= Ident (* field_name *) EQUAL expr -tuple_expr ::= - tuple_inj - -tuple_inj ::= - par(nsepseq(expr,COMMA)) - arguments ::= - tuple_inj - -list_expr ::= - injection(List,expr) -| Nil + par(nsepseq(expr,COMMA)) (* Patterns *) diff --git a/src/parser/pascaligo/Doc/pascaligo_13.bnf b/src/parser/pascaligo/Doc/pascaligo_13.bnf new file mode 100644 index 000000000..82f22905f --- /dev/null +++ b/src/parser/pascaligo/Doc/pascaligo_13.bnf @@ -0,0 +1,347 @@ +left_assoc(item,op) + +right_assoc(item,op) ::= + item +| item op right_assoc(item,op) + +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 option(SEMI) +| const_decl option(SEMI) +| lambda_decl option(SEMI) + +(* Type declarations *) + +type_decl ::= + Type Ident (* type_name *) Is type_expr + +type_expr ::= + cartesian +| sum_type +| record_type + +cartesian ::= + nsepseq(function_type,TIMES) + +function_type ::= + right_assoc(core_type,ARROW) + +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 ::= + nsepseq(variant,VBAR) +| 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 + +entry_decl ::= + Entrypoint Ident (* fun_name *) entry_params COLON type_expr Is + seq(local_decl) + block + With expr + +entry_params ::= + par(nsepseq(entry_param_decl,SEMI)) + +proc_decl ::= + Procedure Ident (* fun_name *) parameters Is + seq(local_decl) + block + +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 +| data_decl + +data_decl ::= + const_decl +| var_decl + +const_decl ::= + Const unqualified_decl(EQUAL) + +var_decl ::= + Var unqualified_decl(ASS) + +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 ::= + single_instr +| block + +single_instr ::= + If expr Then if_clause option(SEMI) Else if_clause +| case(instruction) +| Ident (* proc_name *) arguments +| Ident ASS expr +| Ident brackets(expr) ASS expr +| Ident DOT nsepseq(selection,DOT) option(brackets(expr)) ASS expr +| loop +| Fail expr +| Skip +| Patch path With structure +| Remove expr From Map path +| Remove expr From Set path + +path ::= + Ident (* var *) +| Ident (* struct_name *) DOT nsepseq(selection,DOT) + +injection(Kind,element) ::= + Kind series(element,SEMI,End) +| Kind End +| Kind LBRACKET bracketed + +bracketed ::= + series(element,SEMI,RBRACKET) +| RBRACKET + +binding ::= + expr ARROW expr + +if_clause ::= + instruction +| LBRACE series(statement,COMMA,RBRACE) + +case(rhs) ::= + Case expr Of cases(rhs) End +| Case expr Of 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_loop +| for_loop + +while_loop ::= + While expr block + +for_loop ::= + For Ident ASS expr option(Down) To expr option(step_clause) block +| For Ident In expr block +| For Ident 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 ::= + core_expr Contains set_membership +| comp_expr + +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 + +core_expr ::= + Int +| Nat +| Mtz +| Ident (* var *) +| Ident (* var *) brackets(expr) (* lookup *) +| Ident (* struct_name *) DOT nsepseq(selection,DOT) option(brackets(expr)) +| Ident (* fun_name *) arguments +| String +| Bytes +| C_False +| C_True +| C_Unit +| C_None +| C_Some arguments +| Constr option(arguments) +| LPAR disj_expr COLON type_expr RPAR +| LPAR nsepseq(expr,COMMA) RPAR +| injection(List,expr) +| Nil +| structure + +structure ::= + injection(Map,binding) +| injection(Set,expr) +| record_expr + +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 + +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(cons_pattern) +| par(nsepseq(core_pattern,COMMA)) +| constr_pattern + +cons_pattern ::= + core_pattern CONS pattern From 50c99ff71dc5baf080898999e372c7c2d3f1bca1 Mon Sep 17 00:00:00 2001 From: Christian Rinderknecht Date: Wed, 31 Jul 2019 10:19:24 +0200 Subject: [PATCH 02/14] I added more transformations. --- src/parser/pascaligo/Doc/pascaligo_09.bnf | 5 +- src/parser/pascaligo/Doc/pascaligo_10.bnf | 5 +- src/parser/pascaligo/Doc/pascaligo_11.bnf | 5 +- src/parser/pascaligo/Doc/pascaligo_12.bnf | 5 +- src/parser/pascaligo/Doc/pascaligo_13.bnf | 6 +- src/parser/pascaligo/Doc/pascaligo_14.bnf | 348 ++++++++++++++++++ src/parser/pascaligo/Doc/pascaligo_15.bnf | 350 ++++++++++++++++++ src/parser/pascaligo/Doc/pascaligo_16.bnf | 353 ++++++++++++++++++ src/parser/pascaligo/Doc/pascaligo_17.bnf | 353 ++++++++++++++++++ src/parser/pascaligo/Doc/pascaligo_18.bnf | 356 +++++++++++++++++++ src/parser/pascaligo/Doc/pascaligo_19.bnf | 354 ++++++++++++++++++ src/parser/pascaligo/Parser.mly | 3 +- src/parser/pascaligo/Tests/crowdfunding.ligo | 16 +- 13 files changed, 2143 insertions(+), 16 deletions(-) create mode 100644 src/parser/pascaligo/Doc/pascaligo_14.bnf create mode 100644 src/parser/pascaligo/Doc/pascaligo_15.bnf create mode 100644 src/parser/pascaligo/Doc/pascaligo_16.bnf create mode 100644 src/parser/pascaligo/Doc/pascaligo_17.bnf create mode 100644 src/parser/pascaligo/Doc/pascaligo_18.bnf create mode 100644 src/parser/pascaligo/Doc/pascaligo_19.bnf diff --git a/src/parser/pascaligo/Doc/pascaligo_09.bnf b/src/parser/pascaligo/Doc/pascaligo_09.bnf index e74409cb2..dd10222dd 100644 --- a/src/parser/pascaligo/Doc/pascaligo_09.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_09.bnf @@ -1,9 +1,10 @@ -left_assoc(item,op) - right_assoc(item,op) ::= item | item op right_assoc(item,op) +left_assoc(item,op) ::= + right_assoc(item,op) + option(X) := (**) | X diff --git a/src/parser/pascaligo/Doc/pascaligo_10.bnf b/src/parser/pascaligo/Doc/pascaligo_10.bnf index b9b555ba0..90c390108 100644 --- a/src/parser/pascaligo/Doc/pascaligo_10.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_10.bnf @@ -1,9 +1,10 @@ -left_assoc(item,op) - right_assoc(item,op) ::= item | item op right_assoc(item,op) +left_assoc(item,op) ::= + right_assoc(item,op) + option(X) := (**) | X diff --git a/src/parser/pascaligo/Doc/pascaligo_11.bnf b/src/parser/pascaligo/Doc/pascaligo_11.bnf index 07e980fb3..d0ddeaee5 100644 --- a/src/parser/pascaligo/Doc/pascaligo_11.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_11.bnf @@ -1,9 +1,10 @@ -left_assoc(item,op) - right_assoc(item,op) ::= item | item op right_assoc(item,op) +left_assoc(item,op) ::= + right_assoc(item,op) + option(X) := (**) | X diff --git a/src/parser/pascaligo/Doc/pascaligo_12.bnf b/src/parser/pascaligo/Doc/pascaligo_12.bnf index 2b959b4cc..29711cd62 100644 --- a/src/parser/pascaligo/Doc/pascaligo_12.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_12.bnf @@ -1,9 +1,10 @@ -left_assoc(item,op) - right_assoc(item,op) ::= item | item op right_assoc(item,op) +left_assoc(item,op) ::= + right_assoc(item,op) + option(X) := (**) | X diff --git a/src/parser/pascaligo/Doc/pascaligo_13.bnf b/src/parser/pascaligo/Doc/pascaligo_13.bnf index 82f22905f..7a9c840ec 100644 --- a/src/parser/pascaligo/Doc/pascaligo_13.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_13.bnf @@ -1,9 +1,10 @@ -left_assoc(item,op) - right_assoc(item,op) ::= item | item op right_assoc(item,op) +left_assoc(item,op) ::= + right_assoc(item,op) + option(X) := (**) | X @@ -341,7 +342,6 @@ core_pattern ::= | Nil | par(cons_pattern) | par(nsepseq(core_pattern,COMMA)) -| constr_pattern cons_pattern ::= core_pattern CONS pattern diff --git a/src/parser/pascaligo/Doc/pascaligo_14.bnf b/src/parser/pascaligo/Doc/pascaligo_14.bnf new file mode 100644 index 000000000..0bea4fd14 --- /dev/null +++ b/src/parser/pascaligo/Doc/pascaligo_14.bnf @@ -0,0 +1,348 @@ +right_assoc(item,op) ::= + item +| item op right_assoc(item,op) + +left_assoc(item,op) ::= + right_assoc(item,op) + +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 option(SEMI) +| const_decl option(SEMI) +| lambda_decl option(SEMI) + +(* Type declarations *) + +type_decl ::= + Type Ident (* type_name *) Is type_expr + +type_expr ::= + cartesian +| sum_type +| record_type + +cartesian ::= + nsepseq(function_type,TIMES) + +function_type ::= + right_assoc(core_type,ARROW) + +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 ::= + nsepseq(variant,VBAR) +| 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 + +entry_decl ::= + Entrypoint Ident (* fun_name *) entry_params COLON type_expr Is + seq(local_decl) + block + With expr + +entry_params ::= + par(nsepseq(entry_param_decl,SEMI)) + +proc_decl ::= + Procedure Ident (* fun_name *) parameters Is + seq(local_decl) + block + +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 +| data_decl + +data_decl ::= + const_decl +| var_decl + +const_decl ::= + Const unqualified_decl(EQUAL) + +var_decl ::= + Var unqualified_decl(ASS) + +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 ::= + single_instr +| block + +single_instr ::= + If expr Then if_clause option(SEMI) Else if_clause +| case(instruction) +| Ident (* proc_name *) arguments +| Ident ASS expr +| Ident brackets(expr) ASS expr +| Ident DOT nsepseq(selection,DOT) option(brackets(expr)) ASS expr +| loop +| Fail expr +| Skip +| Patch path With structure +| Remove expr From Map path +| Remove expr From Set path + +path ::= + Ident (* var *) +| Ident (* struct_name *) DOT nsepseq(selection,DOT) + +injection(Kind,element) ::= + Kind series(element,SEMI,End) +| Kind End +| Kind LBRACKET bracketed + +bracketed ::= + series(element,SEMI,RBRACKET) +| RBRACKET + +binding ::= + expr ARROW expr + +if_clause ::= + instruction +| LBRACE series(statement,COMMA,RBRACE) + +case(rhs) ::= + Case expr Of cases(rhs) End +| Case expr Of 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_loop +| for_loop + +while_loop ::= + While expr block + +for_loop ::= + For Ident ASS expr option(Down) To expr option(step_clause) block +| For Ident In expr block +| For Ident 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 ::= + core_expr Contains set_membership +| comp_expr + +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 + +core_expr ::= + Int +| Nat +| Mtz +| Ident (* var *) +| Ident (* var *) brackets(expr) (* lookup *) +| Ident (* struct_name *) DOT nsepseq(selection,DOT) option(brackets(expr)) +| Ident (* fun_name *) arguments +| String +| Bytes +| C_False +| C_True +| C_Unit +| C_None +| C_Some arguments +| Constr option(arguments) +| LPAR disj_expr COLON type_expr RPAR +| LPAR expr RPAR +| LPAR expr COMMA nsepseq(expr,COMMA) RPAR +| injection(List,expr) +| Nil +| structure + +structure ::= + injection(Map,binding) +| injection(Set,expr) +| record_expr + +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 + +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(cons_pattern) +| par(nsepseq(core_pattern,COMMA)) + +cons_pattern ::= + core_pattern CONS pattern diff --git a/src/parser/pascaligo/Doc/pascaligo_15.bnf b/src/parser/pascaligo/Doc/pascaligo_15.bnf new file mode 100644 index 000000000..7984d91f0 --- /dev/null +++ b/src/parser/pascaligo/Doc/pascaligo_15.bnf @@ -0,0 +1,350 @@ +right_assoc(item,op) ::= + item +| item op right_assoc(item,op) + +left_assoc(item,op) ::= + right_assoc(item,op) + +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 option(SEMI) +| const_decl option(SEMI) +| lambda_decl option(SEMI) + +(* Type declarations *) + +type_decl ::= + Type Ident (* type_name *) Is type_expr + +type_expr ::= + cartesian +| sum_type +| record_type + +cartesian ::= + nsepseq(function_type,TIMES) + +function_type ::= + right_assoc(core_type,ARROW) + +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 ::= + nsepseq(variant,VBAR) +| 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 + +entry_decl ::= + Entrypoint Ident (* fun_name *) entry_params COLON type_expr Is + seq(local_decl) + block + With expr + +entry_params ::= + par(nsepseq(entry_param_decl,SEMI)) + +proc_decl ::= + Procedure Ident (* fun_name *) parameters Is + seq(local_decl) + block + +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 +| data_decl + +data_decl ::= + const_decl +| var_decl + +const_decl ::= + Const unqualified_decl(EQUAL) + +var_decl ::= + Var unqualified_decl(ASS) + +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 ::= + single_instr +| block + +single_instr ::= + If expr Then if_clause option(SEMI) Else if_clause +| case(instruction) +| Ident (* proc_name *) arguments +| Ident ASS expr +| Ident brackets(expr) ASS expr +| Ident DOT nsepseq(selection,DOT) option(brackets(expr)) ASS expr +| loop +| Fail expr +| Skip +| Patch path With structure +| Remove expr From Map path +| Remove expr From Set path + +path ::= + Ident (* var *) +| Ident (* struct_name *) DOT nsepseq(selection,DOT) + +injection(Kind,element) ::= + Kind series(element,SEMI,End) +| Kind End +| Kind LBRACKET bracketed + +bracketed ::= + series(element,SEMI,RBRACKET) +| RBRACKET + +binding ::= + expr ARROW expr + +if_clause ::= + instruction +| LBRACE series(statement,COMMA,RBRACE) + +case(rhs) ::= + Case expr Of cases(rhs) End +| Case expr Of 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_loop +| for_loop + +while_loop ::= + While expr block + +for_loop ::= + For Ident ASS expr option(Down) To expr option(step_clause) block +| For Ident In expr block +| For Ident 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 ::= + core_expr Contains set_membership +| comp_expr + +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 + +core_expr ::= + Int +| Nat +| Mtz +| Ident (* var *) +| Ident (* var *) brackets(expr) (* lookup *) +| Ident (* struct_name *) DOT nsepseq(selection,DOT) option(brackets(expr)) +| Ident (* fun_name *) arguments +| String +| Bytes +| C_False +| C_True +| C_Unit +| C_None +| C_Some arguments +| Constr option(arguments) +| LPAR disj_expr COLON type_expr RPAR +| LPAR case(expr) RPAR +| LPAR disj_expr RPAR +| LPAR case(expr) COMMA nsepseq(expr,COMMA) RPAR +| LPAR disj_expr COMMA nsepseq(expr,COMMA) RPAR +| injection(List,expr) +| Nil +| structure + +structure ::= + injection(Map,binding) +| injection(Set,expr) +| record_expr + +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 + +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(cons_pattern) +| par(nsepseq(core_pattern,COMMA)) + +cons_pattern ::= + core_pattern CONS pattern diff --git a/src/parser/pascaligo/Doc/pascaligo_16.bnf b/src/parser/pascaligo/Doc/pascaligo_16.bnf new file mode 100644 index 000000000..e1429f350 --- /dev/null +++ b/src/parser/pascaligo/Doc/pascaligo_16.bnf @@ -0,0 +1,353 @@ +right_assoc(item,op) ::= + item +| item op right_assoc(item,op) + +left_assoc(item,op) ::= + right_assoc(item,op) + +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 option(SEMI) +| const_decl option(SEMI) +| lambda_decl option(SEMI) + +(* Type declarations *) + +type_decl ::= + Type Ident (* type_name *) Is type_expr + +type_expr ::= + cartesian +| sum_type +| record_type + +cartesian ::= + nsepseq(function_type,TIMES) + +function_type ::= + right_assoc(core_type,ARROW) + +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 ::= + nsepseq(variant,VBAR) +| 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 + +entry_decl ::= + Entrypoint Ident (* fun_name *) entry_params COLON type_expr Is + seq(local_decl) + block + With expr + +entry_params ::= + par(nsepseq(entry_param_decl,SEMI)) + +proc_decl ::= + Procedure Ident (* fun_name *) parameters Is + seq(local_decl) + block + +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 +| data_decl + +data_decl ::= + const_decl +| var_decl + +const_decl ::= + Const unqualified_decl(EQUAL) + +var_decl ::= + Var unqualified_decl(ASS) + +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 ::= + single_instr +| block + +single_instr ::= + If expr Then if_clause option(SEMI) Else if_clause +| case(instruction) +| Ident (* proc_name *) arguments +| Ident ASS expr +| Ident brackets(expr) ASS expr +| Ident DOT nsepseq(selection,DOT) option(brackets(expr)) ASS expr +| loop +| Fail expr +| Skip +| Patch path With structure +| Remove expr From Map path +| Remove expr From Set path + +path ::= + Ident (* var *) +| Ident (* struct_name *) DOT nsepseq(selection,DOT) + +injection(Kind,element) ::= + Kind series(element,SEMI,End) +| Kind End +| Kind LBRACKET bracketed + +bracketed ::= + series(element,SEMI,RBRACKET) +| RBRACKET + +binding ::= + expr ARROW expr + +if_clause ::= + instruction +| LBRACE series(statement,COMMA,RBRACE) + +case(rhs) ::= + Case expr Of cases(rhs) End +| Case expr Of 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_loop +| for_loop + +while_loop ::= + While expr block + +for_loop ::= + For Ident ASS expr option(Down) To expr option(step_clause) block +| For Ident In expr block +| For Ident 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 ::= + core_expr Contains set_membership +| comp_expr + +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 + +core_expr ::= + Int +| Nat +| Mtz +| Ident (* var *) +| Ident (* var *) brackets(expr) (* lookup *) +| Ident (* struct_name *) DOT nsepseq(selection,DOT) option(brackets(expr)) +| Ident (* fun_name *) arguments +| String +| Bytes +| C_False +| C_True +| C_Unit +| C_None +| C_Some arguments +| Constr option(arguments) +| LPAR paren_expr RPAR +| injection(List,expr) +| Nil +| structure + +paren_expr ::= + disj_expr COLON type_expr +| disj_expr +| disj_expr COMMA nsepseq(expr,COMMA) +| case(expr) +| case(expr) COMMA nsepseq(expr,COMMA) + +structure ::= + injection(Map,binding) +| injection(Set,expr) +| record_expr + +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 + +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(cons_pattern) +| par(nsepseq(core_pattern,COMMA)) + +cons_pattern ::= + core_pattern CONS pattern diff --git a/src/parser/pascaligo/Doc/pascaligo_17.bnf b/src/parser/pascaligo/Doc/pascaligo_17.bnf new file mode 100644 index 000000000..ae8a73add --- /dev/null +++ b/src/parser/pascaligo/Doc/pascaligo_17.bnf @@ -0,0 +1,353 @@ +right_assoc(item,op) ::= + item +| item op right_assoc(item,op) + +left_assoc(item,op) ::= + right_assoc(item,op) + +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 option(SEMI) +| const_decl option(SEMI) +| lambda_decl option(SEMI) + +(* Type declarations *) + +type_decl ::= + Type Ident (* type_name *) Is type_expr + +type_expr ::= + cartesian +| sum_type +| record_type + +cartesian ::= + nsepseq(function_type,TIMES) + +function_type ::= + right_assoc(core_type,ARROW) + +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 ::= + nsepseq(variant,VBAR) +| 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 + +entry_decl ::= + Entrypoint Ident (* fun_name *) entry_params COLON type_expr Is + seq(local_decl) + block + With expr + +entry_params ::= + par(nsepseq(entry_param_decl,SEMI)) + +proc_decl ::= + Procedure Ident (* fun_name *) parameters Is + seq(local_decl) + block + +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 +| data_decl + +data_decl ::= + const_decl +| var_decl + +const_decl ::= + Const unqualified_decl(EQUAL) + +var_decl ::= + Var unqualified_decl(ASS) + +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 ::= + single_instr +| block + +single_instr ::= + If expr Then if_clause option(SEMI) Else if_clause +| case(instruction) +| Ident (* proc_name *) arguments +| Ident ASS expr +| Ident brackets(expr) ASS expr +| Ident DOT nsepseq(selection,DOT) option(brackets(expr)) ASS expr +| loop +| Fail expr +| Skip +| Patch path With structure +| Remove expr From Map path +| Remove expr From Set path + +path ::= + Ident (* var *) +| Ident (* struct_name *) DOT nsepseq(selection,DOT) + +injection(Kind,element) ::= + Kind series(element,SEMI,End) +| Kind End +| Kind LBRACKET bracketed + +bracketed ::= + series(element,SEMI,RBRACKET) +| RBRACKET + +binding ::= + expr ARROW expr + +if_clause ::= + instruction +| LBRACE series(statement,COMMA,RBRACE) + +case(rhs) ::= + Case expr Of cases(rhs) End +| Case expr Of 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_loop +| for_loop + +while_loop ::= + While expr block + +for_loop ::= + For Ident ASS expr option(Down) To expr option(step_clause) block +| For Ident In expr block +| For Ident 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 ::= + core_expr Contains set_membership +| comp_expr + +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 + +core_expr ::= + Int +| Nat +| Mtz +| Ident (* var *) +| Ident (* var *) brackets(expr) (* lookup *) +| Ident (* struct_name *) DOT nsepseq(selection,DOT) option(brackets(expr)) +| Ident (* fun_name *) arguments +| String +| Bytes +| C_False +| C_True +| C_Unit +| C_None +| C_Some arguments +| Constr option(arguments) +| LPAR paren_expr RPAR +| injection(List,expr) +| Nil +| structure + +paren_expr ::= + disj_expr COLON type_expr +| disj_expr +| disj_expr COMMA nsepseq(expr,COMMA) +| case(expr) +| case(expr) COMMA nsepseq(expr,COMMA) + +structure ::= + injection(Map,binding) +| injection(Set,expr) +| record_expr + +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 + +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 +| LPAR cons_pattern RPAR +| LPAR nsepseq(core_pattern,COMMA) RPAR + +cons_pattern ::= + core_pattern CONS pattern diff --git a/src/parser/pascaligo/Doc/pascaligo_18.bnf b/src/parser/pascaligo/Doc/pascaligo_18.bnf new file mode 100644 index 000000000..f98ac4cf5 --- /dev/null +++ b/src/parser/pascaligo/Doc/pascaligo_18.bnf @@ -0,0 +1,356 @@ +right_assoc(item,op) ::= + item +| item op right_assoc(item,op) + +left_assoc(item,op) ::= + right_assoc(item,op) + +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 option(SEMI) +| const_decl option(SEMI) +| lambda_decl option(SEMI) + +(* Type declarations *) + +type_decl ::= + Type Ident (* type_name *) Is type_expr + +type_expr ::= + cartesian +| sum_type +| record_type + +cartesian ::= + nsepseq(function_type,TIMES) + +function_type ::= + right_assoc(core_type,ARROW) + +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 ::= + nsepseq(variant,VBAR) +| 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 + +entry_decl ::= + Entrypoint Ident (* fun_name *) entry_params COLON type_expr Is + seq(local_decl) + block + With expr + +entry_params ::= + par(nsepseq(entry_param_decl,SEMI)) + +proc_decl ::= + Procedure Ident (* fun_name *) parameters Is + seq(local_decl) + block + +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 +| data_decl + +data_decl ::= + const_decl +| var_decl + +const_decl ::= + Const unqualified_decl(EQUAL) + +var_decl ::= + Var unqualified_decl(ASS) + +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 ::= + single_instr +| block + +single_instr ::= + If expr Then if_clause option(SEMI) Else if_clause +| case(instruction) +| Ident (* proc_name *) arguments +| Ident ASS expr +| Ident brackets(expr) ASS expr +| Ident DOT nsepseq(selection,DOT) option(brackets(expr)) ASS expr +| loop +| Fail expr +| Skip +| Patch path With structure +| Remove expr From Map path +| Remove expr From Set path + +path ::= + Ident (* var *) +| Ident (* struct_name *) DOT nsepseq(selection,DOT) + +injection(Kind,element) ::= + Kind series(element,SEMI,End) +| Kind End +| Kind LBRACKET bracketed + +bracketed ::= + series(element,SEMI,RBRACKET) +| RBRACKET + +binding ::= + expr ARROW expr + +if_clause ::= + instruction +| LBRACE series(statement,COMMA,RBRACE) + +case(rhs) ::= + Case expr Of cases(rhs) End +| Case expr Of 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_loop +| for_loop + +while_loop ::= + While expr block + +for_loop ::= + For Ident ASS expr option(Down) To expr option(step_clause) block +| For Ident In expr block +| For Ident 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 ::= + core_expr Contains set_membership +| comp_expr + +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 + +core_expr ::= + Int +| Nat +| Mtz +| Ident (* var *) +| Ident (* var *) brackets(expr) (* lookup *) +| Ident (* struct_name *) DOT nsepseq(selection,DOT) option(brackets(expr)) +| Ident (* fun_name *) arguments +| String +| Bytes +| C_False +| C_True +| C_Unit +| C_None +| C_Some arguments +| Constr option(arguments) +| LPAR paren_expr RPAR +| injection(List,expr) +| Nil +| structure + +paren_expr ::= + disj_expr COLON type_expr +| disj_expr +| disj_expr COMMA nsepseq(expr,COMMA) +| case(expr) +| case(expr) COMMA nsepseq(expr,COMMA) + +structure ::= + injection(Map,binding) +| injection(Set,expr) +| record_expr + +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 + +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 +| LPAR paren_pattern RPAR + +paren_pattern ::= + cons_pattern +| nsepseq(core_pattern,COMMA) + +cons_pattern ::= + core_pattern CONS pattern diff --git a/src/parser/pascaligo/Doc/pascaligo_19.bnf b/src/parser/pascaligo/Doc/pascaligo_19.bnf new file mode 100644 index 000000000..52916e821 --- /dev/null +++ b/src/parser/pascaligo/Doc/pascaligo_19.bnf @@ -0,0 +1,354 @@ +right_assoc(item,op) ::= + item +| item op right_assoc(item,op) + +left_assoc(item,op) ::= + right_assoc(item,op) + +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 option(SEMI) +| const_decl option(SEMI) +| lambda_decl option(SEMI) + +(* Type declarations *) + +type_decl ::= + Type Ident (* type_name *) Is type_expr + +type_expr ::= + cartesian +| sum_type +| record_type + +cartesian ::= + nsepseq(function_type,TIMES) + +function_type ::= + right_assoc(core_type,ARROW) + +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 ::= + nsepseq(variant,VBAR) +| 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 + +entry_decl ::= + Entrypoint Ident (* fun_name *) entry_params COLON type_expr Is + seq(local_decl) + block + With expr + +entry_params ::= + par(nsepseq(entry_param_decl,SEMI)) + +proc_decl ::= + Procedure Ident (* fun_name *) parameters Is + seq(local_decl) + block + +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 +| data_decl + +data_decl ::= + const_decl +| var_decl + +const_decl ::= + Const unqualified_decl(EQUAL) + +var_decl ::= + Var unqualified_decl(ASS) + +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 ::= + single_instr +| block + +single_instr ::= + If expr Then if_clause option(SEMI) Else if_clause +| case(instruction) +| Ident (* proc_name *) arguments +| Ident ASS expr +| Ident brackets(expr) ASS expr +| Ident DOT nsepseq(selection,DOT) option(brackets(expr)) ASS expr +| loop +| Fail expr +| Skip +| Patch path With structure +| Remove expr From Map path +| Remove expr From Set path + +path ::= + Ident (* var *) +| Ident (* struct_name *) DOT nsepseq(selection,DOT) + +injection(Kind,element) ::= + Kind series(element,SEMI,End) +| Kind End +| Kind LBRACKET bracketed + +bracketed ::= + series(element,SEMI,RBRACKET) +| RBRACKET + +binding ::= + expr ARROW expr + +if_clause ::= + instruction +| LBRACE series(statement,COMMA,RBRACE) + +case(rhs) ::= + Case expr Of cases(rhs) End +| Case expr Of 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_loop +| for_loop + +while_loop ::= + While expr block + +for_loop ::= + For Ident ASS expr option(Down) To expr option(step_clause) block +| For Ident In expr block +| For Ident 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 ::= + core_expr Contains set_membership +| comp_expr + +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 + +core_expr ::= + Int +| Nat +| Mtz +| Ident (* var *) +| Ident (* var *) brackets(expr) (* lookup *) +| Ident (* struct_name *) DOT nsepseq(selection,DOT) option(brackets(expr)) +| Ident (* fun_name *) arguments +| String +| Bytes +| C_False +| C_True +| C_Unit +| C_None +| C_Some arguments +| Constr option(arguments) +| LPAR paren_expr RPAR +| injection(List,expr) +| Nil +| structure + +paren_expr ::= + disj_expr COLON type_expr +| disj_expr +| disj_expr COMMA nsepseq(expr,COMMA) +| case(expr) +| case(expr) COMMA nsepseq(expr,COMMA) + +structure ::= + injection(Map,binding) +| injection(Set,expr) +| record_expr + +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 + +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 +| LPAR paren_pattern RPAR + +paren_pattern ::= + core_pattern CONS pattern +| core_pattern +| core_pattern COMMA nsepseq(core_pattern,COMMA) diff --git a/src/parser/pascaligo/Parser.mly b/src/parser/pascaligo/Parser.mly index 96647a5ca..34b4db971 100644 --- a/src/parser/pascaligo/Parser.mly +++ b/src/parser/pascaligo/Parser.mly @@ -703,8 +703,7 @@ interactive_expr: expr: case(expr) { ECase ($1 expr_to_region) } - (*| annot_expr { $1 }*) -| disj_expr { $1 } +| disj_expr { $1 } disj_expr: disj_expr Or conj_expr { diff --git a/src/parser/pascaligo/Tests/crowdfunding.ligo b/src/parser/pascaligo/Tests/crowdfunding.ligo index bbd42dad7..662fe4cc0 100644 --- a/src/parser/pascaligo/Tests/crowdfunding.ligo +++ b/src/parser/pascaligo/Tests/crowdfunding.ligo @@ -1,3 +1,13 @@ +const cmp_check : bool = 0 < 1 + +(* +const cmp_check : bool = ("1970-01-01T00:00:00Z" : timestamp) < ("1970-01-01T00:01:00Z" : timestamp)) +*) + +const x : int = (3 : int) + + + type store is record [ goal : nat; @@ -11,14 +21,14 @@ entrypoint contribute (storage store : store; const amount : mutez) : store * list (operation) is var operations : list (operation) := nil - // const s : list (int) = list [1; 2; 3] -//const t : set (int) = set [] + // const s : list (int) = list [1; 2; 3] + // const t : set (int) = set [] begin if now (Unit) > store.deadline then fail "Deadline passed"; else case store.backers[sender] of [ - None -> store.backers[sender] := Some (amount); + None -> store.backers[sender] := Some (amount) // None -> patch store.backers with map sender -> amount end | _ -> skip ] From 5bc43fa430eb7dde7b7da6f02299b72e70676394 Mon Sep 17 00:00:00 2001 From: Christian Rinderknecht Date: Wed, 31 Jul 2019 10:45:19 +0200 Subject: [PATCH 03/14] Changed the definition of the compound constructs so they use "option". --- src/parser/pascaligo/Doc/pascaligo_01.bnf | 30 +++++++++++------------ src/parser/pascaligo/Doc/pascaligo_02.bnf | 26 ++++++++++---------- src/parser/pascaligo/Doc/pascaligo_03.bnf | 25 ++++++++++--------- src/parser/pascaligo/Doc/pascaligo_04.bnf | 25 ++++++++++--------- src/parser/pascaligo/Doc/pascaligo_05.bnf | 25 ++++++++++--------- src/parser/pascaligo/Doc/pascaligo_06.bnf | 25 ++++++++++--------- src/parser/pascaligo/Doc/pascaligo_07.bnf | 6 ++--- src/parser/pascaligo/Doc/pascaligo_08.bnf | 25 ++++++++++--------- src/parser/pascaligo/Doc/pascaligo_09.bnf | 25 ++++++++++--------- src/parser/pascaligo/Doc/pascaligo_10.bnf | 25 ++++++++++--------- src/parser/pascaligo/Doc/pascaligo_11.bnf | 25 ++++++++++--------- src/parser/pascaligo/Doc/pascaligo_12.bnf | 25 ++++++++++--------- src/parser/pascaligo/Doc/pascaligo_13.bnf | 25 ++++++++++--------- src/parser/pascaligo/Doc/pascaligo_14.bnf | 25 ++++++++++--------- src/parser/pascaligo/Doc/pascaligo_15.bnf | 25 ++++++++++--------- src/parser/pascaligo/Doc/pascaligo_16.bnf | 25 ++++++++++--------- src/parser/pascaligo/Doc/pascaligo_17.bnf | 25 ++++++++++--------- src/parser/pascaligo/Doc/pascaligo_18.bnf | 25 ++++++++++--------- src/parser/pascaligo/Doc/pascaligo_19.bnf | 25 ++++++++++--------- 19 files changed, 238 insertions(+), 224 deletions(-) diff --git a/src/parser/pascaligo/Doc/pascaligo_01.bnf b/src/parser/pascaligo/Doc/pascaligo_01.bnf index 551d23d3e..7eeb63c1b 100644 --- a/src/parser/pascaligo/Doc/pascaligo_01.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_01.bnf @@ -1,6 +1,6 @@ -option(X) := +option(item) := (**) -| X +| item sep_or_term_list(item,sep) ::= nsepseq(item,sep) @@ -8,34 +8,34 @@ sep_or_term_list(item,sep) ::= (* Compound constructs *) -par(X) ::= LPAR X RPAR +par(item) ::= + LPAR item RPAR -brackets(X) ::= LBRACKET X RBRACKET +brackets(item) ::= + LBRACKET item RBRACKET (* Sequences *) (* Possibly empty sequence of items *) -seq(X) ::= - (**) -| X seq(X) +seq(item) ::= + option(nseq(item)) (* Non-empty sequence of items *) -nseq(X) ::= X seq(X) +nseq(item) ::= + item seq(item) (* Non-empty separated sequence of items *) -nsepseq(X,Sep) ::= - X -| X Sep nsepseq(X,Sep) +nsepseq(item,Sep) ::= + item +| item Sep nsepseq(item,Sep) (* Possibly empy separated sequence of items *) -sepseq(X,Sep) ::= - (**) -| nsepseq(X,Sep) - +sepseq(item,Sep) ::= + option(nsepseq(item,Sep)) (* Inlines *) diff --git a/src/parser/pascaligo/Doc/pascaligo_02.bnf b/src/parser/pascaligo/Doc/pascaligo_02.bnf index a91bbdaff..dd410f63c 100644 --- a/src/parser/pascaligo/Doc/pascaligo_02.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_02.bnf @@ -15,34 +15,34 @@ item_or_closing(item,sep,term) ::= (* Compound constructs *) -par(X) ::= LPAR X RPAR +par(item) ::= + LPAR item RPAR -brackets(X) ::= LBRACKET X RBRACKET +brackets(item) ::= + LBRACKET item RBRACKET (* Sequences *) (* Possibly empty sequence of items *) -seq(X) ::= - (**) -| X seq(X) +seq(item) ::= + option(nseq(item)) (* Non-empty sequence of items *) -nseq(X) ::= X seq(X) +nseq(item) ::= + item seq(item) (* Non-empty separated sequence of items *) -nsepseq(X,Sep) ::= - X -| X Sep nsepseq(X,Sep) +nsepseq(item,Sep) ::= + item +| item Sep nsepseq(item,Sep) (* Possibly empy separated sequence of items *) -sepseq(X,Sep) ::= - (**) -| nsepseq(X,Sep) - +sepseq(item,Sep) ::= + option(nsepseq(item,Sep)) (* Inlines *) diff --git a/src/parser/pascaligo/Doc/pascaligo_03.bnf b/src/parser/pascaligo/Doc/pascaligo_03.bnf index 8f8f7b9ee..1f39f9dba 100644 --- a/src/parser/pascaligo/Doc/pascaligo_03.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_03.bnf @@ -15,33 +15,34 @@ item_or_closing(item,sep,term) ::= (* Compound constructs *) -par(X) ::= LPAR X RPAR +par(item) ::= + LPAR item RPAR -brackets(X) ::= LBRACKET X RBRACKET +brackets(item) ::= + LBRACKET item RBRACKET (* Sequences *) (* Possibly empty sequence of items *) -seq(X) ::= - (**) -| X seq(X) +seq(item) ::= + option(nseq(item)) (* Non-empty sequence of items *) -nseq(X) ::= X seq(X) +nseq(item) ::= + item seq(item) (* Non-empty separated sequence of items *) -nsepseq(X,Sep) ::= - X -| X Sep nsepseq(X,Sep) +nsepseq(item,Sep) ::= + item +| item Sep nsepseq(item,Sep) (* Possibly empy separated sequence of items *) -sepseq(X,Sep) ::= - (**) -| nsepseq(X,Sep) +sepseq(item,Sep) ::= + option(nsepseq(item,Sep)) (* Main *) diff --git a/src/parser/pascaligo/Doc/pascaligo_04.bnf b/src/parser/pascaligo/Doc/pascaligo_04.bnf index c53d68517..9b5b9cc66 100644 --- a/src/parser/pascaligo/Doc/pascaligo_04.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_04.bnf @@ -15,33 +15,34 @@ item_or_closing(item,sep,term) ::= (* Compound constructs *) -par(X) ::= LPAR X RPAR +par(item) ::= + LPAR item RPAR -brackets(X) ::= LBRACKET X RBRACKET +brackets(item) ::= + LBRACKET item RBRACKET (* Sequences *) (* Possibly empty sequence of items *) -seq(X) ::= - (**) -| X seq(X) +seq(item) ::= + option(nseq(item)) (* Non-empty sequence of items *) -nseq(X) ::= X seq(X) +nseq(item) ::= + item seq(item) (* Non-empty separated sequence of items *) -nsepseq(X,Sep) ::= - X -| X Sep nsepseq(X,Sep) +nsepseq(item,Sep) ::= + item +| item Sep nsepseq(item,Sep) (* Possibly empy separated sequence of items *) -sepseq(X,Sep) ::= - (**) -| nsepseq(X,Sep) +sepseq(item,Sep) ::= + option(nsepseq(item,Sep)) (* Main *) diff --git a/src/parser/pascaligo/Doc/pascaligo_05.bnf b/src/parser/pascaligo/Doc/pascaligo_05.bnf index 924a0ca30..1461f2a4c 100644 --- a/src/parser/pascaligo/Doc/pascaligo_05.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_05.bnf @@ -15,33 +15,34 @@ item_or_closing(item,sep,term) ::= (* Compound constructs *) -par(X) ::= LPAR X RPAR +par(item) ::= + LPAR item RPAR -brackets(X) ::= LBRACKET X RBRACKET +brackets(item) ::= + LBRACKET item RBRACKET (* Sequences *) (* Possibly empty sequence of items *) -seq(X) ::= - (**) -| X seq(X) +seq(item) ::= + option(nseq(item)) (* Non-empty sequence of items *) -nseq(X) ::= X seq(X) +nseq(item) ::= + item seq(item) (* Non-empty separated sequence of items *) -nsepseq(X,Sep) ::= - X -| X Sep nsepseq(X,Sep) +nsepseq(item,Sep) ::= + item +| item Sep nsepseq(item,Sep) (* Possibly empy separated sequence of items *) -sepseq(X,Sep) ::= - (**) -| nsepseq(X,Sep) +sepseq(item,Sep) ::= + option(nsepseq(item,Sep)) (* Main *) diff --git a/src/parser/pascaligo/Doc/pascaligo_06.bnf b/src/parser/pascaligo/Doc/pascaligo_06.bnf index 30323f057..caced433f 100644 --- a/src/parser/pascaligo/Doc/pascaligo_06.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_06.bnf @@ -15,33 +15,34 @@ item_or_closing(item,sep,term) ::= (* Compound constructs *) -par(X) ::= LPAR X RPAR +par(item) ::= + LPAR item RPAR -brackets(X) ::= LBRACKET X RBRACKET +brackets(item) ::= + LBRACKET item RBRACKET (* Sequences *) (* Possibly empty sequence of items *) -seq(X) ::= - (**) -| X seq(X) +seq(item) ::= + option(nseq(item)) (* Non-empty sequence of items *) -nseq(X) ::= X seq(X) +nseq(item) ::= + item seq(item) (* Non-empty separated sequence of items *) -nsepseq(X,Sep) ::= - X -| X Sep nsepseq(X,Sep) +nsepseq(item,Sep) ::= + item +| item Sep nsepseq(item,Sep) (* Possibly empy separated sequence of items *) -sepseq(X,Sep) ::= - (**) -| nsepseq(X,Sep) +sepseq(item,Sep) ::= + option(nsepseq(item,Sep)) (* Main *) diff --git a/src/parser/pascaligo/Doc/pascaligo_07.bnf b/src/parser/pascaligo/Doc/pascaligo_07.bnf index 263a64264..95d1be77a 100644 --- a/src/parser/pascaligo/Doc/pascaligo_07.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_07.bnf @@ -24,8 +24,7 @@ brackets(X) ::= LBRACKET X RBRACKET (* Possibly empty sequence of items *) seq(X) ::= - (**) -| X seq(X) + option(nseq(X)) (* Non-empty sequence of items *) @@ -40,8 +39,7 @@ nsepseq(X,Sep) ::= (* Possibly empy separated sequence of items *) sepseq(X,Sep) ::= - (**) -| nsepseq(X,Sep) + option(nsepseq(X,Sep)) (* Main *) diff --git a/src/parser/pascaligo/Doc/pascaligo_08.bnf b/src/parser/pascaligo/Doc/pascaligo_08.bnf index 524c29d82..953341d69 100644 --- a/src/parser/pascaligo/Doc/pascaligo_08.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_08.bnf @@ -15,33 +15,34 @@ item_or_closing(item,sep,term) ::= (* Compound constructs *) -par(X) ::= LPAR X RPAR +par(item) ::= + LPAR item RPAR -brackets(X) ::= LBRACKET X RBRACKET +brackets(item) ::= + LBRACKET item RBRACKET (* Sequences *) (* Possibly empty sequence of items *) -seq(X) ::= - (**) -| X seq(X) +seq(item) ::= + option(nseq(item)) (* Non-empty sequence of items *) -nseq(X) ::= X seq(X) +nseq(item) ::= + item seq(item) (* Non-empty separated sequence of items *) -nsepseq(X,Sep) ::= - X -| X Sep nsepseq(X,Sep) +nsepseq(item,Sep) ::= + item +| item Sep nsepseq(item,Sep) (* Possibly empy separated sequence of items *) -sepseq(X,Sep) ::= - (**) -| nsepseq(X,Sep) +sepseq(item,Sep) ::= + option(nsepseq(item,Sep)) (* Main *) diff --git a/src/parser/pascaligo/Doc/pascaligo_09.bnf b/src/parser/pascaligo/Doc/pascaligo_09.bnf index dd10222dd..e570609c7 100644 --- a/src/parser/pascaligo/Doc/pascaligo_09.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_09.bnf @@ -22,33 +22,34 @@ item_or_closing(item,sep,term) ::= (* Compound constructs *) -par(X) ::= LPAR X RPAR +par(item) ::= + LPAR item RPAR -brackets(X) ::= LBRACKET X RBRACKET +brackets(item) ::= + LBRACKET item RBRACKET (* Sequences *) (* Possibly empty sequence of items *) -seq(X) ::= - (**) -| X seq(X) +seq(item) ::= + option(nseq(item)) (* Non-empty sequence of items *) -nseq(X) ::= X seq(X) +nseq(item) ::= + item seq(item) (* Non-empty separated sequence of items *) -nsepseq(X,Sep) ::= - X -| X Sep nsepseq(X,Sep) +nsepseq(item,Sep) ::= + item +| item Sep nsepseq(item,Sep) (* Possibly empy separated sequence of items *) -sepseq(X,Sep) ::= - (**) -| nsepseq(X,Sep) +sepseq(item,Sep) ::= + option(nsepseq(item,Sep)) (* Main *) diff --git a/src/parser/pascaligo/Doc/pascaligo_10.bnf b/src/parser/pascaligo/Doc/pascaligo_10.bnf index 90c390108..33fbe18f6 100644 --- a/src/parser/pascaligo/Doc/pascaligo_10.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_10.bnf @@ -22,33 +22,34 @@ item_or_closing(item,sep,term) ::= (* Compound constructs *) -par(X) ::= LPAR X RPAR +par(item) ::= + LPAR item RPAR -brackets(X) ::= LBRACKET X RBRACKET +brackets(item) ::= + LBRACKET item RBRACKET (* Sequences *) (* Possibly empty sequence of items *) -seq(X) ::= - (**) -| X seq(X) +seq(item) ::= + option(nseq(item)) (* Non-empty sequence of items *) -nseq(X) ::= X seq(X) +nseq(item) ::= + item seq(item) (* Non-empty separated sequence of items *) -nsepseq(X,Sep) ::= - X -| X Sep nsepseq(X,Sep) +nsepseq(item,Sep) ::= + item +| item Sep nsepseq(item,Sep) (* Possibly empy separated sequence of items *) -sepseq(X,Sep) ::= - (**) -| nsepseq(X,Sep) +sepseq(item,Sep) ::= + option(nsepseq(item,Sep)) (* Main *) diff --git a/src/parser/pascaligo/Doc/pascaligo_11.bnf b/src/parser/pascaligo/Doc/pascaligo_11.bnf index d0ddeaee5..0995cb0e7 100644 --- a/src/parser/pascaligo/Doc/pascaligo_11.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_11.bnf @@ -22,33 +22,34 @@ item_or_closing(item,sep,term) ::= (* Compound constructs *) -par(X) ::= LPAR X RPAR +par(item) ::= + LPAR item RPAR -brackets(X) ::= LBRACKET X RBRACKET +brackets(item) ::= + LBRACKET item RBRACKET (* Sequences *) (* Possibly empty sequence of items *) -seq(X) ::= - (**) -| X seq(X) +seq(item) ::= + option(nseq(item)) (* Non-empty sequence of items *) -nseq(X) ::= X seq(X) +nseq(item) ::= + item seq(item) (* Non-empty separated sequence of items *) -nsepseq(X,Sep) ::= - X -| X Sep nsepseq(X,Sep) +nsepseq(item,Sep) ::= + item +| item Sep nsepseq(item,Sep) (* Possibly empy separated sequence of items *) -sepseq(X,Sep) ::= - (**) -| nsepseq(X,Sep) +sepseq(item,Sep) ::= + option(nsepseq(item,Sep)) (* Main *) diff --git a/src/parser/pascaligo/Doc/pascaligo_12.bnf b/src/parser/pascaligo/Doc/pascaligo_12.bnf index 29711cd62..a69689f8d 100644 --- a/src/parser/pascaligo/Doc/pascaligo_12.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_12.bnf @@ -22,33 +22,34 @@ item_or_closing(item,sep,term) ::= (* Compound constructs *) -par(X) ::= LPAR X RPAR +par(item) ::= + LPAR item RPAR -brackets(X) ::= LBRACKET X RBRACKET +brackets(item) ::= + LBRACKET item RBRACKET (* Sequences *) (* Possibly empty sequence of items *) -seq(X) ::= - (**) -| X seq(X) +seq(item) ::= + option(nseq(item)) (* Non-empty sequence of items *) -nseq(X) ::= X seq(X) +nseq(item) ::= + item seq(item) (* Non-empty separated sequence of items *) -nsepseq(X,Sep) ::= - X -| X Sep nsepseq(X,Sep) +nsepseq(item,Sep) ::= + item +| item Sep nsepseq(item,Sep) (* Possibly empy separated sequence of items *) -sepseq(X,Sep) ::= - (**) -| nsepseq(X,Sep) +sepseq(item,Sep) ::= + option(nsepseq(item,Sep)) (* Main *) diff --git a/src/parser/pascaligo/Doc/pascaligo_13.bnf b/src/parser/pascaligo/Doc/pascaligo_13.bnf index 7a9c840ec..7bf49f9c4 100644 --- a/src/parser/pascaligo/Doc/pascaligo_13.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_13.bnf @@ -22,33 +22,34 @@ item_or_closing(item,sep,term) ::= (* Compound constructs *) -par(X) ::= LPAR X RPAR +par(item) ::= + LPAR item RPAR -brackets(X) ::= LBRACKET X RBRACKET +brackets(item) ::= + LBRACKET item RBRACKET (* Sequences *) (* Possibly empty sequence of items *) -seq(X) ::= - (**) -| X seq(X) +seq(item) ::= + option(nseq(item)) (* Non-empty sequence of items *) -nseq(X) ::= X seq(X) +nseq(item) ::= + item seq(item) (* Non-empty separated sequence of items *) -nsepseq(X,Sep) ::= - X -| X Sep nsepseq(X,Sep) +nsepseq(item,Sep) ::= + item +| item Sep nsepseq(item,Sep) (* Possibly empy separated sequence of items *) -sepseq(X,Sep) ::= - (**) -| nsepseq(X,Sep) +sepseq(item,Sep) ::= + option(nsepseq(item,Sep)) (* Main *) diff --git a/src/parser/pascaligo/Doc/pascaligo_14.bnf b/src/parser/pascaligo/Doc/pascaligo_14.bnf index 0bea4fd14..748bddb41 100644 --- a/src/parser/pascaligo/Doc/pascaligo_14.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_14.bnf @@ -22,33 +22,34 @@ item_or_closing(item,sep,term) ::= (* Compound constructs *) -par(X) ::= LPAR X RPAR +par(item) ::= + LPAR item RPAR -brackets(X) ::= LBRACKET X RBRACKET +brackets(item) ::= + LBRACKET item RBRACKET (* Sequences *) (* Possibly empty sequence of items *) -seq(X) ::= - (**) -| X seq(X) +seq(item) ::= + option(nseq(item)) (* Non-empty sequence of items *) -nseq(X) ::= X seq(X) +nseq(item) ::= + item seq(item) (* Non-empty separated sequence of items *) -nsepseq(X,Sep) ::= - X -| X Sep nsepseq(X,Sep) +nsepseq(item,Sep) ::= + item +| item Sep nsepseq(item,Sep) (* Possibly empy separated sequence of items *) -sepseq(X,Sep) ::= - (**) -| nsepseq(X,Sep) +sepseq(item,Sep) ::= + option(nsepseq(item,Sep)) (* Main *) diff --git a/src/parser/pascaligo/Doc/pascaligo_15.bnf b/src/parser/pascaligo/Doc/pascaligo_15.bnf index 7984d91f0..700ee4058 100644 --- a/src/parser/pascaligo/Doc/pascaligo_15.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_15.bnf @@ -22,33 +22,34 @@ item_or_closing(item,sep,term) ::= (* Compound constructs *) -par(X) ::= LPAR X RPAR +par(item) ::= + LPAR item RPAR -brackets(X) ::= LBRACKET X RBRACKET +brackets(item) ::= + LBRACKET item RBRACKET (* Sequences *) (* Possibly empty sequence of items *) -seq(X) ::= - (**) -| X seq(X) +seq(item) ::= + option(nseq(item)) (* Non-empty sequence of items *) -nseq(X) ::= X seq(X) +nseq(item) ::= + item seq(item) (* Non-empty separated sequence of items *) -nsepseq(X,Sep) ::= - X -| X Sep nsepseq(X,Sep) +nsepseq(item,Sep) ::= + item +| item Sep nsepseq(item,Sep) (* Possibly empy separated sequence of items *) -sepseq(X,Sep) ::= - (**) -| nsepseq(X,Sep) +sepseq(item,Sep) ::= + option(nsepseq(item,Sep)) (* Main *) diff --git a/src/parser/pascaligo/Doc/pascaligo_16.bnf b/src/parser/pascaligo/Doc/pascaligo_16.bnf index e1429f350..d826edc34 100644 --- a/src/parser/pascaligo/Doc/pascaligo_16.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_16.bnf @@ -22,33 +22,34 @@ item_or_closing(item,sep,term) ::= (* Compound constructs *) -par(X) ::= LPAR X RPAR +par(item) ::= + LPAR item RPAR -brackets(X) ::= LBRACKET X RBRACKET +brackets(item) ::= + LBRACKET item RBRACKET (* Sequences *) (* Possibly empty sequence of items *) -seq(X) ::= - (**) -| X seq(X) +seq(item) ::= + option(nseq(item)) (* Non-empty sequence of items *) -nseq(X) ::= X seq(X) +nseq(item) ::= + item seq(item) (* Non-empty separated sequence of items *) -nsepseq(X,Sep) ::= - X -| X Sep nsepseq(X,Sep) +nsepseq(item,Sep) ::= + item +| item Sep nsepseq(item,Sep) (* Possibly empy separated sequence of items *) -sepseq(X,Sep) ::= - (**) -| nsepseq(X,Sep) +sepseq(item,Sep) ::= + option(nsepseq(item,Sep)) (* Main *) diff --git a/src/parser/pascaligo/Doc/pascaligo_17.bnf b/src/parser/pascaligo/Doc/pascaligo_17.bnf index ae8a73add..af6dd9531 100644 --- a/src/parser/pascaligo/Doc/pascaligo_17.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_17.bnf @@ -22,33 +22,34 @@ item_or_closing(item,sep,term) ::= (* Compound constructs *) -par(X) ::= LPAR X RPAR +par(item) ::= + LPAR item RPAR -brackets(X) ::= LBRACKET X RBRACKET +brackets(item) ::= + LBRACKET item RBRACKET (* Sequences *) (* Possibly empty sequence of items *) -seq(X) ::= - (**) -| X seq(X) +seq(item) ::= + option(nseq(item)) (* Non-empty sequence of items *) -nseq(X) ::= X seq(X) +nseq(item) ::= + item seq(item) (* Non-empty separated sequence of items *) -nsepseq(X,Sep) ::= - X -| X Sep nsepseq(X,Sep) +nsepseq(item,Sep) ::= + item +| item Sep nsepseq(item,Sep) (* Possibly empy separated sequence of items *) -sepseq(X,Sep) ::= - (**) -| nsepseq(X,Sep) +sepseq(item,Sep) ::= + option(nsepseq(item,Sep)) (* Main *) diff --git a/src/parser/pascaligo/Doc/pascaligo_18.bnf b/src/parser/pascaligo/Doc/pascaligo_18.bnf index f98ac4cf5..7ad433713 100644 --- a/src/parser/pascaligo/Doc/pascaligo_18.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_18.bnf @@ -22,33 +22,34 @@ item_or_closing(item,sep,term) ::= (* Compound constructs *) -par(X) ::= LPAR X RPAR +par(item) ::= + LPAR item RPAR -brackets(X) ::= LBRACKET X RBRACKET +brackets(item) ::= + LBRACKET item RBRACKET (* Sequences *) (* Possibly empty sequence of items *) -seq(X) ::= - (**) -| X seq(X) +seq(item) ::= + option(nseq(item)) (* Non-empty sequence of items *) -nseq(X) ::= X seq(X) +nseq(item) ::= + item seq(item) (* Non-empty separated sequence of items *) -nsepseq(X,Sep) ::= - X -| X Sep nsepseq(X,Sep) +nsepseq(item,Sep) ::= + item +| item Sep nsepseq(item,Sep) (* Possibly empy separated sequence of items *) -sepseq(X,Sep) ::= - (**) -| nsepseq(X,Sep) +sepseq(item,Sep) ::= + option(nsepseq(item,Sep)) (* Main *) diff --git a/src/parser/pascaligo/Doc/pascaligo_19.bnf b/src/parser/pascaligo/Doc/pascaligo_19.bnf index 52916e821..ae1219062 100644 --- a/src/parser/pascaligo/Doc/pascaligo_19.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_19.bnf @@ -22,33 +22,34 @@ item_or_closing(item,sep,term) ::= (* Compound constructs *) -par(X) ::= LPAR X RPAR +par(item) ::= + LPAR item RPAR -brackets(X) ::= LBRACKET X RBRACKET +brackets(item) ::= + LBRACKET item RBRACKET (* Sequences *) (* Possibly empty sequence of items *) -seq(X) ::= - (**) -| X seq(X) +seq(item) ::= + option(nseq(item)) (* Non-empty sequence of items *) -nseq(X) ::= X seq(X) +nseq(item) ::= + item seq(item) (* Non-empty separated sequence of items *) -nsepseq(X,Sep) ::= - X -| X Sep nsepseq(X,Sep) +nsepseq(item,Sep) ::= + item +| item Sep nsepseq(item,Sep) (* Possibly empy separated sequence of items *) -sepseq(X,Sep) ::= - (**) -| nsepseq(X,Sep) +sepseq(item,Sep) ::= + option(nsepseq(item,Sep)) (* Main *) From 6c818567fad72c5895f31e98ff0bd7220b3f72eb Mon Sep 17 00:00:00 2001 From: Christian Rinderknecht Date: Wed, 31 Jul 2019 14:43:04 +0200 Subject: [PATCH 04/14] Fixed comment. --- src/parser/pascaligo/Doc/pascaligo_01.bnf | 2 +- src/parser/pascaligo/Doc/pascaligo_02.bnf | 2 +- src/parser/pascaligo/Doc/pascaligo_03.bnf | 2 +- src/parser/pascaligo/Doc/pascaligo_04.bnf | 2 +- src/parser/pascaligo/Doc/pascaligo_05.bnf | 2 +- src/parser/pascaligo/Doc/pascaligo_06.bnf | 2 +- src/parser/pascaligo/Doc/pascaligo_07.bnf | 2 +- src/parser/pascaligo/Doc/pascaligo_08.bnf | 2 +- src/parser/pascaligo/Doc/pascaligo_09.bnf | 2 +- src/parser/pascaligo/Doc/pascaligo_10.bnf | 2 +- src/parser/pascaligo/Doc/pascaligo_11.bnf | 2 +- src/parser/pascaligo/Doc/pascaligo_12.bnf | 2 +- src/parser/pascaligo/Doc/pascaligo_13.bnf | 2 +- src/parser/pascaligo/Doc/pascaligo_14.bnf | 2 +- src/parser/pascaligo/Doc/pascaligo_15.bnf | 2 +- src/parser/pascaligo/Doc/pascaligo_16.bnf | 2 +- src/parser/pascaligo/Doc/pascaligo_17.bnf | 2 +- src/parser/pascaligo/Doc/pascaligo_18.bnf | 2 +- src/parser/pascaligo/Doc/pascaligo_19.bnf | 2 +- src/parser/pascaligo/Doc/pascaligo_20.bnf | 340 ++++++++++++++++++++++ 20 files changed, 359 insertions(+), 19 deletions(-) create mode 100644 src/parser/pascaligo/Doc/pascaligo_20.bnf diff --git a/src/parser/pascaligo/Doc/pascaligo_01.bnf b/src/parser/pascaligo/Doc/pascaligo_01.bnf index 7eeb63c1b..d7c05f76d 100644 --- a/src/parser/pascaligo/Doc/pascaligo_01.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_01.bnf @@ -32,7 +32,7 @@ nsepseq(item,Sep) ::= item | item Sep nsepseq(item,Sep) -(* Possibly empy separated sequence of items *) +(* Possibly empty separated sequence of items *) sepseq(item,Sep) ::= option(nsepseq(item,Sep)) diff --git a/src/parser/pascaligo/Doc/pascaligo_02.bnf b/src/parser/pascaligo/Doc/pascaligo_02.bnf index dd410f63c..aa116d906 100644 --- a/src/parser/pascaligo/Doc/pascaligo_02.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_02.bnf @@ -39,7 +39,7 @@ nsepseq(item,Sep) ::= item | item Sep nsepseq(item,Sep) -(* Possibly empy separated sequence of items *) +(* Possibly empty separated sequence of items *) sepseq(item,Sep) ::= option(nsepseq(item,Sep)) diff --git a/src/parser/pascaligo/Doc/pascaligo_03.bnf b/src/parser/pascaligo/Doc/pascaligo_03.bnf index 1f39f9dba..dedd68a84 100644 --- a/src/parser/pascaligo/Doc/pascaligo_03.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_03.bnf @@ -39,7 +39,7 @@ nsepseq(item,Sep) ::= item | item Sep nsepseq(item,Sep) -(* Possibly empy separated sequence of items *) +(* Possibly empty separated sequence of items *) sepseq(item,Sep) ::= option(nsepseq(item,Sep)) diff --git a/src/parser/pascaligo/Doc/pascaligo_04.bnf b/src/parser/pascaligo/Doc/pascaligo_04.bnf index 9b5b9cc66..c223129f7 100644 --- a/src/parser/pascaligo/Doc/pascaligo_04.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_04.bnf @@ -39,7 +39,7 @@ nsepseq(item,Sep) ::= item | item Sep nsepseq(item,Sep) -(* Possibly empy separated sequence of items *) +(* Possibly empty separated sequence of items *) sepseq(item,Sep) ::= option(nsepseq(item,Sep)) diff --git a/src/parser/pascaligo/Doc/pascaligo_05.bnf b/src/parser/pascaligo/Doc/pascaligo_05.bnf index 1461f2a4c..926e1244d 100644 --- a/src/parser/pascaligo/Doc/pascaligo_05.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_05.bnf @@ -39,7 +39,7 @@ nsepseq(item,Sep) ::= item | item Sep nsepseq(item,Sep) -(* Possibly empy separated sequence of items *) +(* Possibly empty separated sequence of items *) sepseq(item,Sep) ::= option(nsepseq(item,Sep)) diff --git a/src/parser/pascaligo/Doc/pascaligo_06.bnf b/src/parser/pascaligo/Doc/pascaligo_06.bnf index caced433f..e62db26aa 100644 --- a/src/parser/pascaligo/Doc/pascaligo_06.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_06.bnf @@ -39,7 +39,7 @@ nsepseq(item,Sep) ::= item | item Sep nsepseq(item,Sep) -(* Possibly empy separated sequence of items *) +(* Possibly empty separated sequence of items *) sepseq(item,Sep) ::= option(nsepseq(item,Sep)) diff --git a/src/parser/pascaligo/Doc/pascaligo_07.bnf b/src/parser/pascaligo/Doc/pascaligo_07.bnf index 95d1be77a..f9ad66fb4 100644 --- a/src/parser/pascaligo/Doc/pascaligo_07.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_07.bnf @@ -36,7 +36,7 @@ nsepseq(X,Sep) ::= X | X Sep nsepseq(X,Sep) -(* Possibly empy separated sequence of items *) +(* Possibly empty separated sequence of items *) sepseq(X,Sep) ::= option(nsepseq(X,Sep)) diff --git a/src/parser/pascaligo/Doc/pascaligo_08.bnf b/src/parser/pascaligo/Doc/pascaligo_08.bnf index 953341d69..4944ba91b 100644 --- a/src/parser/pascaligo/Doc/pascaligo_08.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_08.bnf @@ -39,7 +39,7 @@ nsepseq(item,Sep) ::= item | item Sep nsepseq(item,Sep) -(* Possibly empy separated sequence of items *) +(* Possibly empty separated sequence of items *) sepseq(item,Sep) ::= option(nsepseq(item,Sep)) diff --git a/src/parser/pascaligo/Doc/pascaligo_09.bnf b/src/parser/pascaligo/Doc/pascaligo_09.bnf index e570609c7..acd43171a 100644 --- a/src/parser/pascaligo/Doc/pascaligo_09.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_09.bnf @@ -46,7 +46,7 @@ nsepseq(item,Sep) ::= item | item Sep nsepseq(item,Sep) -(* Possibly empy separated sequence of items *) +(* Possibly empty separated sequence of items *) sepseq(item,Sep) ::= option(nsepseq(item,Sep)) diff --git a/src/parser/pascaligo/Doc/pascaligo_10.bnf b/src/parser/pascaligo/Doc/pascaligo_10.bnf index 33fbe18f6..d0e2f14b9 100644 --- a/src/parser/pascaligo/Doc/pascaligo_10.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_10.bnf @@ -46,7 +46,7 @@ nsepseq(item,Sep) ::= item | item Sep nsepseq(item,Sep) -(* Possibly empy separated sequence of items *) +(* Possibly empty separated sequence of items *) sepseq(item,Sep) ::= option(nsepseq(item,Sep)) diff --git a/src/parser/pascaligo/Doc/pascaligo_11.bnf b/src/parser/pascaligo/Doc/pascaligo_11.bnf index 0995cb0e7..6c9cbf461 100644 --- a/src/parser/pascaligo/Doc/pascaligo_11.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_11.bnf @@ -46,7 +46,7 @@ nsepseq(item,Sep) ::= item | item Sep nsepseq(item,Sep) -(* Possibly empy separated sequence of items *) +(* Possibly empty separated sequence of items *) sepseq(item,Sep) ::= option(nsepseq(item,Sep)) diff --git a/src/parser/pascaligo/Doc/pascaligo_12.bnf b/src/parser/pascaligo/Doc/pascaligo_12.bnf index a69689f8d..b213b230a 100644 --- a/src/parser/pascaligo/Doc/pascaligo_12.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_12.bnf @@ -46,7 +46,7 @@ nsepseq(item,Sep) ::= item | item Sep nsepseq(item,Sep) -(* Possibly empy separated sequence of items *) +(* Possibly empty separated sequence of items *) sepseq(item,Sep) ::= option(nsepseq(item,Sep)) diff --git a/src/parser/pascaligo/Doc/pascaligo_13.bnf b/src/parser/pascaligo/Doc/pascaligo_13.bnf index 7bf49f9c4..135e0052b 100644 --- a/src/parser/pascaligo/Doc/pascaligo_13.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_13.bnf @@ -46,7 +46,7 @@ nsepseq(item,Sep) ::= item | item Sep nsepseq(item,Sep) -(* Possibly empy separated sequence of items *) +(* Possibly empty separated sequence of items *) sepseq(item,Sep) ::= option(nsepseq(item,Sep)) diff --git a/src/parser/pascaligo/Doc/pascaligo_14.bnf b/src/parser/pascaligo/Doc/pascaligo_14.bnf index 748bddb41..23718d06b 100644 --- a/src/parser/pascaligo/Doc/pascaligo_14.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_14.bnf @@ -46,7 +46,7 @@ nsepseq(item,Sep) ::= item | item Sep nsepseq(item,Sep) -(* Possibly empy separated sequence of items *) +(* Possibly empty separated sequence of items *) sepseq(item,Sep) ::= option(nsepseq(item,Sep)) diff --git a/src/parser/pascaligo/Doc/pascaligo_15.bnf b/src/parser/pascaligo/Doc/pascaligo_15.bnf index 700ee4058..0cc9c2070 100644 --- a/src/parser/pascaligo/Doc/pascaligo_15.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_15.bnf @@ -46,7 +46,7 @@ nsepseq(item,Sep) ::= item | item Sep nsepseq(item,Sep) -(* Possibly empy separated sequence of items *) +(* Possibly empty separated sequence of items *) sepseq(item,Sep) ::= option(nsepseq(item,Sep)) diff --git a/src/parser/pascaligo/Doc/pascaligo_16.bnf b/src/parser/pascaligo/Doc/pascaligo_16.bnf index d826edc34..fcf25c03c 100644 --- a/src/parser/pascaligo/Doc/pascaligo_16.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_16.bnf @@ -46,7 +46,7 @@ nsepseq(item,Sep) ::= item | item Sep nsepseq(item,Sep) -(* Possibly empy separated sequence of items *) +(* Possibly empty separated sequence of items *) sepseq(item,Sep) ::= option(nsepseq(item,Sep)) diff --git a/src/parser/pascaligo/Doc/pascaligo_17.bnf b/src/parser/pascaligo/Doc/pascaligo_17.bnf index af6dd9531..245c2988c 100644 --- a/src/parser/pascaligo/Doc/pascaligo_17.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_17.bnf @@ -46,7 +46,7 @@ nsepseq(item,Sep) ::= item | item Sep nsepseq(item,Sep) -(* Possibly empy separated sequence of items *) +(* Possibly empty separated sequence of items *) sepseq(item,Sep) ::= option(nsepseq(item,Sep)) diff --git a/src/parser/pascaligo/Doc/pascaligo_18.bnf b/src/parser/pascaligo/Doc/pascaligo_18.bnf index 7ad433713..d8b378645 100644 --- a/src/parser/pascaligo/Doc/pascaligo_18.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_18.bnf @@ -46,7 +46,7 @@ nsepseq(item,Sep) ::= item | item Sep nsepseq(item,Sep) -(* Possibly empy separated sequence of items *) +(* Possibly empty separated sequence of items *) sepseq(item,Sep) ::= option(nsepseq(item,Sep)) diff --git a/src/parser/pascaligo/Doc/pascaligo_19.bnf b/src/parser/pascaligo/Doc/pascaligo_19.bnf index ae1219062..a3e90d99e 100644 --- a/src/parser/pascaligo/Doc/pascaligo_19.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_19.bnf @@ -46,7 +46,7 @@ nsepseq(item,Sep) ::= item | item Sep nsepseq(item,Sep) -(* Possibly empy separated sequence of items *) +(* Possibly empty separated sequence of items *) sepseq(item,Sep) ::= option(nsepseq(item,Sep)) diff --git a/src/parser/pascaligo/Doc/pascaligo_20.bnf b/src/parser/pascaligo/Doc/pascaligo_20.bnf new file mode 100644 index 000000000..1d2f84afb --- /dev/null +++ b/src/parser/pascaligo/Doc/pascaligo_20.bnf @@ -0,0 +1,340 @@ +right_assoc(item,op) ::= + item +| item op right_assoc(item,op) + +left_assoc(item,op) ::= + right_assoc(item,op) + +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(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 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 series(field_decl,SEMI,End) +| Record LBRACKET series(field_decl,SEMI,RBRACKET) + +variant ::= + Constr Of cartesian +| Constr + +cartesian ::= + nsepseq(function_type,TIMES) + +function_type ::= + right_assoc(core_type,ARROW) + +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)) + +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) + +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 (* proc_name *) arguments +| Ident ASS expr +| Ident brackets(expr) ASS expr +| Ident DOT nsepseq(selection,DOT) option(brackets(expr)) ASS expr +| loop +| Fail expr +| Skip +| Patch path With structure +| Remove expr From Map path +| Remove expr From Set path + +path ::= + Ident (* var *) +| Ident (* struct_name *) DOT nsepseq(selection,DOT) + +injection(Kind,element) ::= + Kind series(element,SEMI,End) +| Kind End +| Kind LBRACKET bracketed + +bracketed ::= + series(element,SEMI,RBRACKET) +| RBRACKET + +binding ::= + expr ARROW expr + +if_clause ::= + instruction +| LBRACE series(statement,COMMA,RBRACE) + +case(rhs) ::= + Case expr Of cases(rhs) End +| Case expr Of 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 ASS expr option(Down) To expr option(step_clause) block +| For Ident In expr block +| For Ident 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 ::= + core_expr Contains set_membership +| comp_expr + +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 + +core_expr ::= + Int +| Nat +| Mtz +| Ident (* var *) +| Ident (* var *) brackets(expr) (* lookup *) +| Ident (* struct_name *) DOT nsepseq(selection,DOT) option(brackets(expr)) +| Ident (* fun_name *) arguments +| String +| Bytes +| C_False +| C_True +| C_Unit +| C_None +| C_Some arguments +| Constr option(arguments) +| LPAR paren_expr RPAR +| injection(List,expr) +| Nil +| structure + +paren_expr ::= + disj_expr COLON type_expr +| disj_expr +| disj_expr COMMA nsepseq(expr,COMMA) +| case(expr) +| case(expr) COMMA nsepseq(expr,COMMA) + +structure ::= + injection(Map,binding) +| injection(Set,expr) +| record_expr + +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 + +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 +| LPAR paren_pattern RPAR + +paren_pattern ::= + core_pattern CONS pattern +| core_pattern +| core_pattern COMMA nsepseq(core_pattern,COMMA) From ce31bc25727cfc340c2a4e1c4c87de433a9602a1 Mon Sep 17 00:00:00 2001 From: Christian Rinderknecht Date: Sun, 4 Aug 2019 18:02:56 +0200 Subject: [PATCH 05/14] Fixes. --- src/parser/pascaligo/Doc/pascaligo_02.bnf | 4 ++-- src/parser/pascaligo/Doc/pascaligo_03.bnf | 4 ++-- src/parser/pascaligo/Doc/pascaligo_04.bnf | 4 ++-- src/parser/pascaligo/Doc/pascaligo_05.bnf | 4 ++-- src/parser/pascaligo/Doc/pascaligo_06.bnf | 8 +++---- src/parser/pascaligo/Doc/pascaligo_07.bnf | 28 +++++++++++------------ src/parser/pascaligo/Doc/pascaligo_08.bnf | 8 +++---- src/parser/pascaligo/Doc/pascaligo_09.bnf | 8 +++---- src/parser/pascaligo/Doc/pascaligo_10.bnf | 8 +++---- src/parser/pascaligo/Doc/pascaligo_11.bnf | 8 +++---- src/parser/pascaligo/Doc/pascaligo_12.bnf | 8 +++---- src/parser/pascaligo/Doc/pascaligo_13.bnf | 11 +++++---- src/parser/pascaligo/Doc/pascaligo_14.bnf | 11 +++++---- src/parser/pascaligo/Doc/pascaligo_15.bnf | 11 +++++---- src/parser/pascaligo/Doc/pascaligo_16.bnf | 11 +++++---- src/parser/pascaligo/Doc/pascaligo_17.bnf | 11 +++++---- src/parser/pascaligo/Doc/pascaligo_18.bnf | 11 +++++---- src/parser/pascaligo/Doc/pascaligo_19.bnf | 11 +++++---- src/parser/pascaligo/Doc/pascaligo_20.bnf | 15 +++++++----- 19 files changed, 104 insertions(+), 80 deletions(-) diff --git a/src/parser/pascaligo/Doc/pascaligo_02.bnf b/src/parser/pascaligo/Doc/pascaligo_02.bnf index aa116d906..a8fd7f688 100644 --- a/src/parser/pascaligo/Doc/pascaligo_02.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_02.bnf @@ -1,6 +1,6 @@ -option(X) := +option(item) := (**) -| X +| item series(item,sep,term) ::= item after_item(item,sep,term) diff --git a/src/parser/pascaligo/Doc/pascaligo_03.bnf b/src/parser/pascaligo/Doc/pascaligo_03.bnf index dedd68a84..f7893cf6d 100644 --- a/src/parser/pascaligo/Doc/pascaligo_03.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_03.bnf @@ -1,6 +1,6 @@ -option(X) := +option(item) := (**) -| X +| item series(item,sep,term) ::= item after_item(item,sep,term) diff --git a/src/parser/pascaligo/Doc/pascaligo_04.bnf b/src/parser/pascaligo/Doc/pascaligo_04.bnf index c223129f7..5f344787a 100644 --- a/src/parser/pascaligo/Doc/pascaligo_04.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_04.bnf @@ -1,6 +1,6 @@ -option(X) := +option(item) := (**) -| X +| item series(item,sep,term) ::= item after_item(item,sep,term) diff --git a/src/parser/pascaligo/Doc/pascaligo_05.bnf b/src/parser/pascaligo/Doc/pascaligo_05.bnf index 926e1244d..d88b74f78 100644 --- a/src/parser/pascaligo/Doc/pascaligo_05.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_05.bnf @@ -1,6 +1,6 @@ -option(X) := +option(item) := (**) -| X +| item series(item,sep,term) ::= item after_item(item,sep,term) diff --git a/src/parser/pascaligo/Doc/pascaligo_06.bnf b/src/parser/pascaligo/Doc/pascaligo_06.bnf index e62db26aa..f16a91dba 100644 --- a/src/parser/pascaligo/Doc/pascaligo_06.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_06.bnf @@ -1,6 +1,6 @@ -option(X) := +option(item) := (**) -| X +| item series(item,sep,term) ::= item after_item(item,sep,term) @@ -195,9 +195,9 @@ single_instr ::= injection(Kind,element) ::= Kind series(element,SEMI,End) | Kind End -| Kind LBRACKET bracketed +| Kind LBRACKET bracketed(element) -bracketed ::= +bracketed(element) ::= series(element,SEMI,RBRACKET) | RBRACKET diff --git a/src/parser/pascaligo/Doc/pascaligo_07.bnf b/src/parser/pascaligo/Doc/pascaligo_07.bnf index f9ad66fb4..a6d801368 100644 --- a/src/parser/pascaligo/Doc/pascaligo_07.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_07.bnf @@ -1,6 +1,6 @@ -option(X) := +option(item) := (**) -| X +| item series(item,sep,term) ::= item after_item(item,sep,term) @@ -15,31 +15,31 @@ item_or_closing(item,sep,term) ::= (* Compound constructs *) -par(X) ::= LPAR X RPAR +par(item) ::= LPAR item RPAR -brackets(X) ::= LBRACKET X RBRACKET +brackets(item) ::= LBRACKET item RBRACKET (* Sequences *) (* Possibly empty sequence of items *) -seq(X) ::= - option(nseq(X)) +seq(item) ::= + option(nseq(item)) (* Non-empty sequence of items *) -nseq(X) ::= X seq(X) +nseq(item) ::= item seq(item) (* Non-empty separated sequence of items *) -nsepseq(X,Sep) ::= - X -| X Sep nsepseq(X,Sep) +nsepseq(item,Sep) ::= + item +| item Sep nsepseq(item,Sep) (* Possibly empty separated sequence of items *) -sepseq(X,Sep) ::= - option(nsepseq(X,Sep)) +sepseq(item,Sep) ::= + option(nsepseq(item,Sep)) (* Main *) @@ -182,9 +182,9 @@ single_instr ::= injection(Kind,element) ::= Kind series(element,SEMI,End) | Kind End -| Kind LBRACKET bracketed +| Kind LBRACKET bracketed(element) -bracketed ::= +bracketed(element) ::= series(element,SEMI,RBRACKET) | RBRACKET diff --git a/src/parser/pascaligo/Doc/pascaligo_08.bnf b/src/parser/pascaligo/Doc/pascaligo_08.bnf index 4944ba91b..f459f2193 100644 --- a/src/parser/pascaligo/Doc/pascaligo_08.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_08.bnf @@ -1,6 +1,6 @@ -option(X) := +option(item) := (**) -| X +| item series(item,sep,term) ::= item after_item(item,sep,term) @@ -187,9 +187,9 @@ single_instr ::= injection(Kind,element) ::= Kind series(element,SEMI,End) | Kind End -| Kind LBRACKET bracketed +| Kind LBRACKET bracketed(element) -bracketed ::= +bracketed(element) ::= series(element,SEMI,RBRACKET) | RBRACKET diff --git a/src/parser/pascaligo/Doc/pascaligo_09.bnf b/src/parser/pascaligo/Doc/pascaligo_09.bnf index acd43171a..0b15db3ac 100644 --- a/src/parser/pascaligo/Doc/pascaligo_09.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_09.bnf @@ -5,9 +5,9 @@ right_assoc(item,op) ::= left_assoc(item,op) ::= right_assoc(item,op) -option(X) := +option(item) := (**) -| X +| item series(item,sep,term) ::= item after_item(item,sep,term) @@ -193,9 +193,9 @@ single_instr ::= injection(Kind,element) ::= Kind series(element,SEMI,End) | Kind End -| Kind LBRACKET bracketed +| Kind LBRACKET bracketed(element) -bracketed ::= +bracketed(element) ::= series(element,SEMI,RBRACKET) | RBRACKET diff --git a/src/parser/pascaligo/Doc/pascaligo_10.bnf b/src/parser/pascaligo/Doc/pascaligo_10.bnf index d0e2f14b9..ae956b3c7 100644 --- a/src/parser/pascaligo/Doc/pascaligo_10.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_10.bnf @@ -5,9 +5,9 @@ right_assoc(item,op) ::= left_assoc(item,op) ::= right_assoc(item,op) -option(X) := +option(item) := (**) -| X +| item series(item,sep,term) ::= item after_item(item,sep,term) @@ -193,9 +193,9 @@ single_instr ::= injection(Kind,element) ::= Kind series(element,SEMI,End) | Kind End -| Kind LBRACKET bracketed +| Kind LBRACKET bracketed(element) -bracketed ::= +bracketed(element) ::= series(element,SEMI,RBRACKET) | RBRACKET diff --git a/src/parser/pascaligo/Doc/pascaligo_11.bnf b/src/parser/pascaligo/Doc/pascaligo_11.bnf index 6c9cbf461..569b16392 100644 --- a/src/parser/pascaligo/Doc/pascaligo_11.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_11.bnf @@ -5,9 +5,9 @@ right_assoc(item,op) ::= left_assoc(item,op) ::= right_assoc(item,op) -option(X) := +option(item) := (**) -| X +| item series(item,sep,term) ::= item after_item(item,sep,term) @@ -191,9 +191,9 @@ single_instr ::= injection(Kind,element) ::= Kind series(element,SEMI,End) | Kind End -| Kind LBRACKET bracketed +| Kind LBRACKET bracketed(element) -bracketed ::= +bracketed(element) ::= series(element,SEMI,RBRACKET) | RBRACKET diff --git a/src/parser/pascaligo/Doc/pascaligo_12.bnf b/src/parser/pascaligo/Doc/pascaligo_12.bnf index b213b230a..47c399337 100644 --- a/src/parser/pascaligo/Doc/pascaligo_12.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_12.bnf @@ -5,9 +5,9 @@ right_assoc(item,op) ::= left_assoc(item,op) ::= right_assoc(item,op) -option(X) := +option(item) := (**) -| X +| item series(item,sep,term) ::= item after_item(item,sep,term) @@ -195,9 +195,9 @@ path ::= injection(Kind,element) ::= Kind series(element,SEMI,End) | Kind End -| Kind LBRACKET bracketed +| Kind LBRACKET bracketed(element) -bracketed ::= +bracketed(element) ::= series(element,SEMI,RBRACKET) | RBRACKET diff --git a/src/parser/pascaligo/Doc/pascaligo_13.bnf b/src/parser/pascaligo/Doc/pascaligo_13.bnf index 135e0052b..7b8146e1c 100644 --- a/src/parser/pascaligo/Doc/pascaligo_13.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_13.bnf @@ -5,9 +5,9 @@ right_assoc(item,op) ::= left_assoc(item,op) ::= right_assoc(item,op) -option(X) := +option(item) := (**) -| X +| item series(item,sep,term) ::= item after_item(item,sep,term) @@ -195,9 +195,9 @@ path ::= injection(Kind,element) ::= Kind series(element,SEMI,End) | Kind End -| Kind LBRACKET bracketed +| Kind LBRACKET bracketed(element) -bracketed ::= +bracketed(element) ::= series(element,SEMI,RBRACKET) | RBRACKET @@ -344,5 +344,8 @@ core_pattern ::= | par(cons_pattern) | par(nsepseq(core_pattern,COMMA)) +tuple_pattern ::= + par(nsepseq(core_pattern,COMMA)) + cons_pattern ::= core_pattern CONS pattern diff --git a/src/parser/pascaligo/Doc/pascaligo_14.bnf b/src/parser/pascaligo/Doc/pascaligo_14.bnf index 23718d06b..4973e59b6 100644 --- a/src/parser/pascaligo/Doc/pascaligo_14.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_14.bnf @@ -5,9 +5,9 @@ right_assoc(item,op) ::= left_assoc(item,op) ::= right_assoc(item,op) -option(X) := +option(item) := (**) -| X +| item series(item,sep,term) ::= item after_item(item,sep,term) @@ -195,9 +195,9 @@ path ::= injection(Kind,element) ::= Kind series(element,SEMI,End) | Kind End -| Kind LBRACKET bracketed +| Kind LBRACKET bracketed(element) -bracketed ::= +bracketed(element) ::= series(element,SEMI,RBRACKET) | RBRACKET @@ -345,5 +345,8 @@ core_pattern ::= | par(cons_pattern) | par(nsepseq(core_pattern,COMMA)) +tuple_pattern ::= + par(nsepseq(core_pattern,COMMA)) + cons_pattern ::= core_pattern CONS pattern diff --git a/src/parser/pascaligo/Doc/pascaligo_15.bnf b/src/parser/pascaligo/Doc/pascaligo_15.bnf index 0cc9c2070..3f26f6494 100644 --- a/src/parser/pascaligo/Doc/pascaligo_15.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_15.bnf @@ -5,9 +5,9 @@ right_assoc(item,op) ::= left_assoc(item,op) ::= right_assoc(item,op) -option(X) := +option(item) := (**) -| X +| item series(item,sep,term) ::= item after_item(item,sep,term) @@ -195,9 +195,9 @@ path ::= injection(Kind,element) ::= Kind series(element,SEMI,End) | Kind End -| Kind LBRACKET bracketed +| Kind LBRACKET bracketed(element) -bracketed ::= +bracketed(element) ::= series(element,SEMI,RBRACKET) | RBRACKET @@ -347,5 +347,8 @@ core_pattern ::= | par(cons_pattern) | par(nsepseq(core_pattern,COMMA)) +tuple_pattern ::= + par(nsepseq(core_pattern,COMMA)) + cons_pattern ::= core_pattern CONS pattern diff --git a/src/parser/pascaligo/Doc/pascaligo_16.bnf b/src/parser/pascaligo/Doc/pascaligo_16.bnf index fcf25c03c..ab6844335 100644 --- a/src/parser/pascaligo/Doc/pascaligo_16.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_16.bnf @@ -5,9 +5,9 @@ right_assoc(item,op) ::= left_assoc(item,op) ::= right_assoc(item,op) -option(X) := +option(item) := (**) -| X +| item series(item,sep,term) ::= item after_item(item,sep,term) @@ -195,9 +195,9 @@ path ::= injection(Kind,element) ::= Kind series(element,SEMI,End) | Kind End -| Kind LBRACKET bracketed +| Kind LBRACKET bracketed(element) -bracketed ::= +bracketed(element) ::= series(element,SEMI,RBRACKET) | RBRACKET @@ -350,5 +350,8 @@ core_pattern ::= | par(cons_pattern) | par(nsepseq(core_pattern,COMMA)) +tuple_pattern ::= + par(nsepseq(core_pattern,COMMA)) + cons_pattern ::= core_pattern CONS pattern diff --git a/src/parser/pascaligo/Doc/pascaligo_17.bnf b/src/parser/pascaligo/Doc/pascaligo_17.bnf index 245c2988c..7a1f4c926 100644 --- a/src/parser/pascaligo/Doc/pascaligo_17.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_17.bnf @@ -5,9 +5,9 @@ right_assoc(item,op) ::= left_assoc(item,op) ::= right_assoc(item,op) -option(X) := +option(item) := (**) -| X +| item series(item,sep,term) ::= item after_item(item,sep,term) @@ -195,9 +195,9 @@ path ::= injection(Kind,element) ::= Kind series(element,SEMI,End) | Kind End -| Kind LBRACKET bracketed +| Kind LBRACKET bracketed(element) -bracketed ::= +bracketed(element) ::= series(element,SEMI,RBRACKET) | RBRACKET @@ -350,5 +350,8 @@ core_pattern ::= | LPAR cons_pattern RPAR | LPAR nsepseq(core_pattern,COMMA) RPAR +tuple_pattern ::= + par(nsepseq(core_pattern,COMMA)) + cons_pattern ::= core_pattern CONS pattern diff --git a/src/parser/pascaligo/Doc/pascaligo_18.bnf b/src/parser/pascaligo/Doc/pascaligo_18.bnf index d8b378645..6d7911a23 100644 --- a/src/parser/pascaligo/Doc/pascaligo_18.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_18.bnf @@ -5,9 +5,9 @@ right_assoc(item,op) ::= left_assoc(item,op) ::= right_assoc(item,op) -option(X) := +option(item) := (**) -| X +| item series(item,sep,term) ::= item after_item(item,sep,term) @@ -195,9 +195,9 @@ path ::= injection(Kind,element) ::= Kind series(element,SEMI,End) | Kind End -| Kind LBRACKET bracketed +| Kind LBRACKET bracketed(element) -bracketed ::= +bracketed(element) ::= series(element,SEMI,RBRACKET) | RBRACKET @@ -353,5 +353,8 @@ paren_pattern ::= cons_pattern | nsepseq(core_pattern,COMMA) +tuple_pattern ::= + par(nsepseq(core_pattern,COMMA)) + cons_pattern ::= core_pattern CONS pattern diff --git a/src/parser/pascaligo/Doc/pascaligo_19.bnf b/src/parser/pascaligo/Doc/pascaligo_19.bnf index a3e90d99e..937290d18 100644 --- a/src/parser/pascaligo/Doc/pascaligo_19.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_19.bnf @@ -5,9 +5,9 @@ right_assoc(item,op) ::= left_assoc(item,op) ::= right_assoc(item,op) -option(X) := +option(item) := (**) -| X +| item series(item,sep,term) ::= item after_item(item,sep,term) @@ -195,9 +195,9 @@ path ::= injection(Kind,element) ::= Kind series(element,SEMI,End) | Kind End -| Kind LBRACKET bracketed +| Kind LBRACKET bracketed(element) -bracketed ::= +bracketed(element) ::= series(element,SEMI,RBRACKET) | RBRACKET @@ -353,3 +353,6 @@ paren_pattern ::= core_pattern CONS pattern | core_pattern | core_pattern COMMA nsepseq(core_pattern,COMMA) + +tuple_pattern ::= + par(nsepseq(core_pattern,COMMA)) diff --git a/src/parser/pascaligo/Doc/pascaligo_20.bnf b/src/parser/pascaligo/Doc/pascaligo_20.bnf index 1d2f84afb..3afe57b98 100644 --- a/src/parser/pascaligo/Doc/pascaligo_20.bnf +++ b/src/parser/pascaligo/Doc/pascaligo_20.bnf @@ -5,9 +5,9 @@ right_assoc(item,op) ::= left_assoc(item,op) ::= right_assoc(item,op) -option(X) := +option(item) := (**) -| X +| item series(item,sep,term) ::= item after_item(item,sep,term) @@ -186,9 +186,9 @@ path ::= injection(Kind,element) ::= Kind series(element,SEMI,End) | Kind End -| Kind LBRACKET bracketed +| Kind LBRACKET bracketed(element) -bracketed ::= +bracketed(element) ::= series(element,SEMI,RBRACKET) | RBRACKET @@ -283,7 +283,7 @@ core_expr ::= | C_None | C_Some arguments | Constr option(arguments) -| LPAR paren_expr RPAR +| par(paren_expr) | injection(List,expr) | Nil | structure @@ -332,9 +332,12 @@ core_pattern ::= | Constr option(tuple_pattern) | injection(List,core_pattern) | Nil -| LPAR paren_pattern RPAR +| par(paren_pattern) paren_pattern ::= core_pattern CONS pattern | core_pattern | core_pattern COMMA nsepseq(core_pattern,COMMA) + +tuple_pattern ::= + par(nsepseq(core_pattern,COMMA)) From fddce3257a9fc8894bdd4f1308dc33b7412c44ab Mon Sep 17 00:00:00 2001 From: Christian Rinderknecht Date: Sun, 4 Aug 2019 18:03:54 +0200 Subject: [PATCH 06/14] First draft of the PascaLIGO parser using streams. --- src/parser/pascaligo/.SParser.ml.tag | 2 + src/parser/pascaligo/.SParserMain.tag | 0 src/parser/pascaligo/SParser.ml | 377 ++++++++++++++++++++++++++ src/parser/pascaligo/SParserMain.ml | 124 +++++++++ 4 files changed, 503 insertions(+) create mode 100644 src/parser/pascaligo/.SParser.ml.tag create mode 100644 src/parser/pascaligo/.SParserMain.tag create mode 100644 src/parser/pascaligo/SParser.ml create mode 100644 src/parser/pascaligo/SParserMain.ml diff --git a/src/parser/pascaligo/.SParser.ml.tag b/src/parser/pascaligo/.SParser.ml.tag new file mode 100644 index 000000000..ea961256f --- /dev/null +++ b/src/parser/pascaligo/.SParser.ml.tag @@ -0,0 +1,2 @@ +ocamldep: -pp camlp5o +ocamlc: -pp camlp5o \ No newline at end of file diff --git a/src/parser/pascaligo/.SParserMain.tag b/src/parser/pascaligo/.SParserMain.tag new file mode 100644 index 000000000..e69de29bb diff --git a/src/parser/pascaligo/SParser.ml b/src/parser/pascaligo/SParser.ml new file mode 100644 index 000000000..94fb6ca81 --- /dev/null +++ b/src/parser/pascaligo/SParser.ml @@ -0,0 +1,377 @@ +open LexToken + +let semi = parser [< 'SEMI _ >] -> () +let vbar = parser [< 'VBAR _ >] -> () +let end_ = parser [< 'End _ >] -> () +let rbracket = parser [< 'RBRACKET _ >] -> () +let times = parser [< 'TIMES _ >] -> () +let arrow = parser [< 'ARROW _ >] -> fun _ _ -> () +let comma = parser [< 'COMMA _ >] -> () +let rbrace = parser [< 'RBRACE _ >] -> () +let equal = parser [< 'EQUAL _ >] -> () +let ass = parser [< 'ASS _ >] -> () +let dot = parser [< 'DOT _ >] -> () +let down = parser [< 'Down _ >] -> () +let or_ = parser [< 'Or _ >] -> fun _ _ -> () +let and_ = parser [< 'And _ >] -> fun _ _ -> () +let cat = parser [< 'CAT _ >] -> fun _ _ -> () +let cons = parser [< 'CONS _ >] -> () +let cons' = parser [< 'CONS _ >] -> fun _ _ -> () +let list = parser [< 'List _ >] -> () +let map = parser [< 'Map _ >] -> () +let set = parser [< 'Set _ >] -> () + +let left_assoc item op = + let rec op_elem i = parser + [< f=op; j=item; r = op_elem (f i j) ?! >] -> r + | [< >] -> i + in parser [< i=item; r = op_elem i >] -> r + +let rec right_assoc item op = parser + [< i=item >] -> i +| [< i=item; f=op; j = right_assoc item op ?! >] -> f i j + +let opt item = parser + [< i=item >] -> Some i +| [< >] -> None + +let rec series item sep term = parser + [< i=item; l = after_item item sep term >] -> i,l + +and after_item item sep term = parser + [< t=term >] -> + [], None, t +| [< s=sep; io = item_or_closing item sep term >] -> + match io with + `Some (item, items, term, closing) -> + (s, item)::items, term, closing + | `Closing closing -> + [], Some s, closing + +and item_or_closing item sep term = parser + [< t=term >] -> + `Closing t +| [< s = series item sep term >] -> + let item, (items, term, closing) = s + in `Some (item, items, term, closing) + +(* Compound constructs *) + +let par item = parser + [< 'LPAR _; _=item; 'RPAR _ >] -> () + +let brackets item = parser + [< 'LBRACKET _; _=item; 'RBRACKET _ >] -> () + +(* Sequences *) + +(* Possibly empty sequence of items *) + +let rec seq item = parser + [< h,t = nseq item >] -> h::t + +(* Non-empty sequence of items *) + +and nseq item = parser + [< i=item; l = seq item >] -> i,l + +(* Non-empty separated sequence of items *) + +and nsepseq item sep = parser + [< i=item >] -> i, [] +| [< i=item; s=sep; h,t = nsepseq item sep ?! >] -> i, (s,h)::t + +(* Possibly empty separated sequence of items *) + +and sepseq item sep = opt (nsepseq item sep) + +(* Main *) + +let rec contract = parser + [< _ = nseq declaration; 'EOF _ >] -> () + +and declaration = parser + [< _ = type_decl; _ = opt semi >] -> () +| [< _ = const_decl; _ = opt semi >] -> () +| [< _ = lambda_decl; _ = opt semi >] -> () + +and type_decl = parser + [< 'Type _; 'Ident _; 'Is _; _=type_expr >] -> () + +and type_expr = parser + [< _=cartesian >] -> () +| [< _=nsepseq variant vbar >] -> () +| [< 'VBAR _; _ = nsepseq variant vbar >] -> () +| [< 'Record _; _ = series field_decl semi end_ >] -> () +| [< 'Record _; 'LBRACKET _; _ = series field_decl semi rbracket >] -> () + +and variant = parser + [< 'Constr _; 'Of _; _=cartesian >] -> () +| [< 'Constr _ >] -> () + +and cartesian = parser + [< _ = nsepseq function_type times >] -> () + +and function_type strm = right_assoc core_type arrow strm + +and core_type = parser + [< 'Ident _ >] -> () +| [< 'Ident _; _=type_tuple >] -> () +| [< 'Map _; _=type_tuple >] -> () +| [< 'Set _; _ = par type_expr >] -> () +| [< 'List _; _ = par type_expr >] -> () +| [< _ = par type_expr >] -> () + +and type_tuple = parser + [< _ = par (nsepseq type_expr comma) >] -> () + +and field_decl = parser + [< 'Ident _; 'COLON _; _=type_expr >] -> () + +(* Function and procedure declarations *) + +and lambda_decl = parser + [< _=fun_decl >] -> () +| [< _=proc_decl >] -> () +| [< _=entry_decl >] -> () + +and fun_decl = parser + [< 'Function _; 'Ident _; _=parameters; 'COLON _; + _=type_expr; 'Is _; _ = seq local_decl; _=block; + 'With _; _=expr >] -> () + +and entry_decl = parser + [< 'Entrypoint _; 'Ident _; _=entry_params; + 'COLON _; _ = type_expr; 'Is _; _ = seq local_decl; + _=block; 'With _; _=expr >] -> () + +and entry_params = parser + [< p = par (nsepseq entry_param_decl semi) >] -> p + +and proc_decl = parser + [< 'Procedure _; 'Ident _; _parameters; 'Is _; + _ = seq local_decl; _=block >] -> () + +and parameters = parser + [< p = par (nsepseq param_decl semi) >] -> p + +and param_decl = parser + [< 'Var _; 'Ident _; 'COLON _; _=param_type >] -> () +| [< 'Const _; 'Ident _; 'COLON _; _=param_type >] -> () + +and entry_param_decl = parser + [< _ = param_decl >] -> () +| [< 'Storage _; 'Ident _; 'COLON _; _=param_type >] -> () + +and param_type = parser [< c = cartesian >] -> c + +and block = parser + [< 'Begin _; _ = series statement semi end_ >] -> () +| [< 'Block _; 'LBRACE _; _ = series statement semi rbrace >] -> () + +and statement = parser + [< _=instruction >] -> () +| [< _=data_decl >] -> () + +and data_decl = parser + [< _=const_decl >] -> () +| [< _=var_decl >] -> () + +and const_decl = parser + [< 'Const _; _ = unqualified_decl equal >] -> () + +and var_decl = parser + [< 'Var _; _ = unqualified_decl ass >] -> () + +and local_decl = parser + [< _=fun_decl; _ = opt semi >] -> () +| [< _=proc_decl; _ = opt semi >] -> () +| [< _=data_decl; _ = opt semi >] -> () + +and unqualified_decl op = parser + [< 'Ident _; 'COLON _; _=type_expr; _=op; _=expr >] -> () + +and instruction = parser + [< _=block >] -> () +| [< 'If _; _=expr; 'Then _; _=if_clause; _ = opt semi; + 'Else _; _=if_clause >] -> () +| [< _ = case instruction >] -> () +| [< 'Ident _; _=arguments >] -> () +| [< 'Ident _; 'ASS _; _=expr >] -> () +| [< 'Ident _; _ = brackets expr; 'ASS _; _=expr >] -> () +| [< 'Ident _; 'DOT _; _ = nsepseq selection dot; + _ = opt (brackets expr); 'ASS _; _=expr >] -> () +| [< _=loop >] -> () +| [< 'Fail _; _=expr >] -> () +| [< 'Skip _ >] -> () +| [< 'Patch _; _=expr; 'From _; 'Map _; _=path >] -> () +| [< 'Patch _; _=expr; 'From _; 'Set _; _=path >] -> () + +and path = parser + [< 'Ident _ >] -> () +| [< 'Ident _; 'DOT _; _ = nsepseq selection dot >] -> () + +and injection kind element = parser + [< _=kind; _ = series element semi end_ >] -> () +| [< _=kind; 'End _ >] -> () +| [< _=kind; 'LBRACKET _; _ = bracketed element >] -> () + +and bracketed element = parser + [< _ = series element semi rbracket >] -> () +| [< 'RBRACKET _ >] -> () + +and binding = parser + [< _=expr; 'ARROW _; _=expr >] -> () + +and if_clause = parser + [< _=instruction >] -> () +| [< 'LBRACE _; _ = series statement comma rbrace >] -> () + +and case rhs = parser + [< 'Case _; _=expr; 'Of _; _ = cases rhs; 'End _ >] -> () +| [< 'Case _; _=expr; 'Of _; 'LBRACKET _; _ = cases rhs; + 'RBRACKET _ >] -> () + +and cases rhs = parser + [< _ = nsepseq (case_clause rhs) vbar >] -> () +| [< 'VBAR _; _ = nsepseq (case_clause rhs) vbar >] -> () + +and case_clause rhs = parser + [< _=pattern; 'ARROW _; _=rhs >] -> () + +and loop = parser + [< 'While _; _=expr; _=block >] -> () +| [< 'For _; 'Ident _; 'ASS _; _=expr; _ = opt down; + 'To _; _=expr; _ = opt step_clause >] -> () +| [< 'For _; 'Ident _; 'In _; _=expr; _=block >] -> () +| [< 'For _; 'Ident _; 'ARROW _; 'Ident _; 'In _; + _=expr; _=block >] -> () + +and step_clause = parser + [< 'Step _; _=expr >] -> () + +(* Expressions *) + +and interactive = parser + [< _=expr; 'EOF _ >] -> () + +and expr = parser + [< _ = case expr >] -> () +| [< _=disj_expr >] -> () + +and disj_expr strm = left_assoc conj_expr or_ strm + +and conj_expr strm = left_assoc set_membership and_ strm + +and set_membership = parser + [< _ = core_expr; 'Contains _; _=set_membership >] -> () +| [< _ = comp_expr >] -> () + +and comp_expr strm = left_assoc cat_expr op_comp strm + +and op_comp = parser + [< 'LT _ >] -> fun _ _ -> () +| [< 'LEQ _ >] -> fun _ _ -> () +| [< 'GT _ >] -> fun _ _ -> () +| [< 'GEQ _ >] -> fun _ _ -> () +| [< 'EQUAL _ >] -> fun _ _ -> () +| [< 'NEQ _ >] -> fun _ _ -> () + +and cat_expr strm = right_assoc cons_expr cat strm + +and cons_expr strm = left_assoc add_expr cons' strm + +and add_expr strm = left_assoc mult_expr add_op strm + +and add_op = parser + [< 'PLUS _ >] -> fun _ _ -> () +| [< 'MINUS _ >] -> fun _ _ -> () + +and mult_expr strm = left_assoc unary_expr mult_op strm + +and mult_op = parser + [< 'TIMES _ >] -> fun _ _ -> () +| [< 'SLASH _ >] -> fun _ _ -> () +| [< 'Mod _ >] -> fun _ _ -> () + +and unary_expr = parser + [< 'MINUS _; _=core_expr >] -> () +| [< 'Not _; _=core_expr >] -> () +| [< _=core_expr >] -> () + +and core_expr = parser + [< 'Int _ >] -> () +| [< 'Nat _ >] -> () +| [< 'Mtz _ >] -> () +| [< 'Ident _ >] -> () +| [< 'Ident _; _ = brackets expr >] -> () +| [< 'Ident _; 'DOT _; _ = nsepseq selection dot; + _ = opt (brackets expr) >] -> () +| [< 'Ident _; _=arguments >] -> () +| [< 'String _ >] -> () +| [< 'Bytes _ >] -> () +| [< 'C_False _ >] -> () +| [< 'C_True _ >] -> () +| [< 'C_Unit _ >] -> () +| [< 'C_None _ >] -> () +| [< 'C_Some _; _=arguments >] -> () +| [< 'Constr _; _ = opt arguments >] -> () +| [< _ = par paren_expr >] -> () +| [< _ = injection list expr >] -> () +| [< 'Nil _ >] -> () +| [< _=structure >] -> () + +and paren_expr = parser + [< _=disj_expr; 'COLON _; _=type_expr >] -> () +| [< _=disj_expr >] -> () +| [< _=disj_expr; 'COMMA _; _ = nsepseq expr comma >] -> () +| [< _ = case expr >] -> () +| [< _ = case expr; 'COMMA _; _ = nsepseq expr comma >] -> () + +and structure = parser + [< _ = injection map binding >] -> () +| [< _ = injection set expr >] -> () +| [< _=record_expr >] -> () + +and selection = parser + [< 'Ident _ >] -> () +| [< 'Int _ >] -> () + +and record_expr = parser + [< 'Record _; _ = series field_assignment semi end_ >] -> () +| [< 'Record _; 'LBRACKET _; + _ = series field_assignment semi rbracket >] -> () + +and field_assignment = parser + [< 'Ident _; 'EQUAL _; _=expr >] -> () + +and arguments = parser + [< _ = par (nsepseq expr comma) >] -> () + +(* Patterns *) + +and pattern = parser + [< _ = nsepseq core_pattern cons >] -> () + +and core_pattern = parser + [< 'Ident _ >] -> () +| [< 'WILD _ >] -> () +| [< 'Int _ >] -> () +| [< 'String _ >] -> () +| [< 'C_Unit _ >] -> () +| [< 'C_False _ >] -> () +| [< 'C_True _ >] -> () +| [< 'C_None _ >] -> () +| [< 'C_Some _; _ = par core_pattern >] -> () +| [< 'Constr _; _ = opt tuple_pattern >] -> () +| [< _ = injection list core_pattern >] -> () +| [< 'Nil _ >] -> () +| [< _ = par paren_pattern >] -> () + +and paren_pattern = parser + [< _=core_pattern; 'CONS _; _=pattern >] -> () +| [< _=core_pattern >] -> () +| [< _=core_pattern; 'COMMA _; _ = nsepseq core_pattern comma >] -> () + +and tuple_pattern = parser + [< _ = par (nsepseq core_pattern comma) >] -> () diff --git a/src/parser/pascaligo/SParserMain.ml b/src/parser/pascaligo/SParserMain.ml new file mode 100644 index 000000000..d6b91d0f1 --- /dev/null +++ b/src/parser/pascaligo/SParserMain.ml @@ -0,0 +1,124 @@ +(* Driver for the parser of PascaLIGO *) + +open SParser (* TEMPORARY *) + +(* Error printing and exception tracing *) + +let () = Printexc.record_backtrace true + +(* Reading the command-line options *) + +let options = EvalOpt.read () + +open EvalOpt + +(* Auxiliary functions *) + +let sprintf = Printf.sprintf + +(* Extracting the input file *) + +let file = + match options.input with + None | Some "-" -> false + | Some _ -> true + +(* Error printing and exception tracing *) + +let () = Printexc.record_backtrace true + +let external_ text = + Utils.highlight (Printf.sprintf "External error: %s" text); exit 1;; + +type Error.t += ParseError + +let error_to_string = function + ParseError -> "Syntax error.\n" +| _ -> assert false + +let print_error ?(offsets=true) mode Region.{region; value} ~file = + let msg = error_to_string value in + let reg = region#to_string ~file ~offsets mode in + Utils.highlight (sprintf "Parse error %s:\n%s%!" reg msg) + +(* Path for CPP inclusions (#include) *) + +let lib_path = + match options.libs with + [] -> "" + | libs -> let mk_I dir path = Printf.sprintf " -I %s%s" dir path + in List.fold_right mk_I libs "" + +(* Preprocessing the input source and opening the input channels *) + +let prefix = + match options.input with + None | Some "-" -> "temp" + | Some file -> Filename.(file |> basename |> remove_extension) + +let suffix = ".pp.ligo" + +let pp_input = + if Utils.String.Set.mem "cpp" options.verbose + then prefix ^ suffix + else let pp_input, pp_out = Filename.open_temp_file prefix suffix + in close_out pp_out; pp_input + +let cpp_cmd = + match options.input with + None | Some "-" -> + Printf.sprintf "cpp -traditional-cpp%s - > %s" + lib_path pp_input + | Some file -> + Printf.sprintf "cpp -traditional-cpp%s %s > %s" + lib_path file pp_input + +let () = + if Utils.String.Set.mem "cpp" options.verbose + then Printf.eprintf "%s\n%!" cpp_cmd; + if Sys.command cpp_cmd <> 0 then + external_ (Printf.sprintf "the command \"%s\" failed." cpp_cmd) + +(* Instanciating the lexer *) + +module Lexer = Lexer.Make (LexToken) + +module Log = LexerLog.Make (Lexer) + +let Lexer.{read; buffer; get_pos; get_last; close} = + Lexer.open_token_stream (Some pp_input) + +and cout = stdout + +let log = Log.output_token ~offsets:options.offsets + options.mode options.cmd cout + +and close_all () = close (); close_out cout + +(* Tokeniser *) + +let tokeniser = read ~log + +(* Main *) + +let () = + try + let ast = Parser.contract tokeniser buffer in + if Utils.String.Set.mem "ast" options.verbose + then begin + ParserLog.offsets := options.offsets; + ParserLog.mode := options.mode; + ParserLog.print_tokens ast + end + with + Lexer.Error err -> + close_all (); + Lexer.print_error ~offsets:options.offsets + options.mode err ~file + | Parser.Error -> + let region = get_last () in + let error = Region.{region; value=ParseError} in + let () = close_all () in + print_error ~offsets:options.offsets + options.mode error ~file + | Sys_error msg -> Utils.highlight msg From f99bd0d1df33c99028448814c05751b09a528644 Mon Sep 17 00:00:00 2001 From: Christian Rinderknecht Date: Thu, 29 Aug 2019 17:06:16 +0200 Subject: [PATCH 07/14] More rewrites of the grammar for stream parsing. Fixed code in the internal documentation of PascaLIGO. --- src/parser/pascaligo/Doc/pascaligo.txt | 14 +- src/parser/pascaligo/Doc/pascaligo_21.bnf | 375 +++++++++++++++++++ src/parser/pascaligo/Doc/pascaligo_22.bnf | 433 ++++++++++++++++++++++ 3 files changed, 815 insertions(+), 7 deletions(-) create mode 100644 src/parser/pascaligo/Doc/pascaligo_21.bnf create mode 100644 src/parser/pascaligo/Doc/pascaligo_22.bnf diff --git a/src/parser/pascaligo/Doc/pascaligo.txt b/src/parser/pascaligo/Doc/pascaligo.txt index 5b6b78696..53c4d79fc 100644 --- a/src/parser/pascaligo/Doc/pascaligo.txt +++ b/src/parser/pascaligo/Doc/pascaligo.txt @@ -190,15 +190,15 @@ the latter can be reassigned. The syntax is slightly different for both. For example, the variables "x" and "y" above could have been declared as follows: -var x : nat := 0; -var y : nat := 0; +var x : nat := 0n; +var y : nat := 0n; It is possible to specify that the value of a variable will not change (the name "variable" is misleading in that context), that is, they remain constant: -const ten : nat = 10; -const eleven : nat = ten + 1; +const ten : nat = 10n; +const eleven : nat = ten + 1n; Similarly, function declarations have their parameters and return value annotated with their types. For instance, @@ -214,10 +214,10 @@ the result of calling the function is given after the keyword "with". A another example would be function factorial (const n : nat) : nat is - var m : nat := 0; - var f : nat := 1; + var m : nat := 0n; + var f : nat := 1n; begin - if n <= 0 then f := 1 + if n <= 0n then f := 1n else for m := 1 to n begin diff --git a/src/parser/pascaligo/Doc/pascaligo_21.bnf b/src/parser/pascaligo/Doc/pascaligo_21.bnf new file mode 100644 index 000000000..d99ef835b --- /dev/null +++ b/src/parser/pascaligo/Doc/pascaligo_21.bnf @@ -0,0 +1,375 @@ +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 *) + +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 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) + +variant ::= + Constr option(of_cartesian) + +of_cartesian ::= + Of cartesian + +cartesian ::= + nsepseq(function_type,TIMES) + +function_type ::= + right_assoc(core_type,ARROW) + +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) + +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 + +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 ::= + core_expr Contains set_membership +| comp_expr + +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 + +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)) diff --git a/src/parser/pascaligo/Doc/pascaligo_22.bnf b/src/parser/pascaligo/Doc/pascaligo_22.bnf new file mode 100644 index 000000000..6eb0e8dc1 --- /dev/null +++ b/src/parser/pascaligo/Doc/pascaligo_22.bnf @@ -0,0 +1,433 @@ +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)) From fbbff496c7ed40da7df030d70cecf9b617183c63 Mon Sep 17 00:00:00 2001 From: Christian Rinderknecht Date: Thu, 29 Aug 2019 17:07:23 +0200 Subject: [PATCH 08/14] Cosmetics. --- src/parser/pascaligo/Lexer.mll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/parser/pascaligo/Lexer.mll b/src/parser/pascaligo/Lexer.mll index 90be90ff9..c0e5283c1 100644 --- a/src/parser/pascaligo/Lexer.mll +++ b/src/parser/pascaligo/Lexer.mll @@ -502,7 +502,7 @@ and scan state = parse | constr { mk_constr state lexbuf |> enqueue } | bytes { (mk_bytes seq) state lexbuf |> enqueue } | natural 'n' { mk_nat state lexbuf |> enqueue } -| natural "mtz" { mk_mtz state lexbuf |> enqueue } +| natural "mtz" { mk_mtz state lexbuf |> enqueue } | integer { mk_int state lexbuf |> enqueue } | symbol { mk_sym state lexbuf |> enqueue } | eof { mk_eof state lexbuf |> enqueue } From 95b2111a8bccadb6dd43141038cac93b2926cfaf Mon Sep 17 00:00:00 2001 From: Christian Rinderknecht Date: Thu, 29 Aug 2019 17:08:23 +0200 Subject: [PATCH 09/14] Left factoring of productions to get closer to LL. --- src/parser/pascaligo/SParser.ml | 121 ++++++++++++++++++++------------ 1 file changed, 76 insertions(+), 45 deletions(-) diff --git a/src/parser/pascaligo/SParser.ml b/src/parser/pascaligo/SParser.ml index 94fb6ca81..c76903659 100644 --- a/src/parser/pascaligo/SParser.ml +++ b/src/parser/pascaligo/SParser.ml @@ -82,8 +82,9 @@ and nsepseq item sep = parser | [< i=item; s=sep; h,t = nsepseq item sep ?! >] -> i, (s,h)::t (* Possibly empty separated sequence of items *) - +(* and sepseq item sep = opt (nsepseq item sep) +*) (* Main *) @@ -102,12 +103,17 @@ and type_expr = parser [< _=cartesian >] -> () | [< _=nsepseq variant vbar >] -> () | [< 'VBAR _; _ = nsepseq variant vbar >] -> () -| [< 'Record _; _ = series field_decl semi end_ >] -> () -| [< 'Record _; 'LBRACKET _; _ = series field_decl semi rbracket >] -> () +| [< 'Record _; _=record_type_expr >] -> () + +and record_type_expr = parser + [< _ = series field_decl semi end_ >] -> () +| [< 'LBRACKET _; _ = series field_decl semi rbracket >] -> () and variant = parser - [< 'Constr _; 'Of _; _=cartesian >] -> () -| [< 'Constr _ >] -> () + [< 'Constr _; _ = opt of_cartesian >] -> () + +and of_cartesian = parser + [< 'Of _; _=cartesian >] -> () and cartesian = parser [< _ = nsepseq function_type times >] -> () @@ -115,8 +121,7 @@ and cartesian = parser and function_type strm = right_assoc core_type arrow strm and core_type = parser - [< 'Ident _ >] -> () -| [< 'Ident _; _=type_tuple >] -> () + [< 'Ident _; _ = opt type_tuple >] -> () | [< 'Map _; _=type_tuple >] -> () | [< 'Set _; _ = par type_expr >] -> () | [< 'List _; _ = par type_expr >] -> () @@ -196,25 +201,37 @@ and instruction = parser | [< 'If _; _=expr; 'Then _; _=if_clause; _ = opt semi; 'Else _; _=if_clause >] -> () | [< _ = case instruction >] -> () -| [< 'Ident _; _=arguments >] -> () -| [< 'Ident _; 'ASS _; _=expr >] -> () -| [< 'Ident _; _ = brackets expr; 'ASS _; _=expr >] -> () -| [< 'Ident _; 'DOT _; _ = nsepseq selection dot; - _ = opt (brackets expr); 'ASS _; _=expr >] -> () +| [< 'Ident _; _=instruction_1 >] -> () | [< _=loop >] -> () | [< 'Fail _; _=expr >] -> () | [< 'Skip _ >] -> () -| [< 'Patch _; _=expr; 'From _; 'Map _; _=path >] -> () -| [< 'Patch _; _=expr; 'From _; 'Set _; _=path >] -> () +| [< 'Patch _; _=path; 'With _; _=structure >] -> () +| [< 'Remove _; _=expr; 'From _; _=remove_suffix >] -> () + +and remove_suffix = parser + [< 'Map _; _=path >] -> () +| [< 'Set _; _=path >] -> () + +and instruction_1 = parser + [< _=arguments >] -> () +| [< 'ASS _; _=expr >] -> () +| [< _ = brackets expr; 'ASS _; _=expr >] -> () +| [< _=selections; + _ = opt (brackets expr); 'ASS _; _=expr >] -> () and path = parser - [< 'Ident _ >] -> () -| [< 'Ident _; 'DOT _; _ = nsepseq selection dot >] -> () + [< 'Ident _; _ = opt selections >] -> () + +and selections = parser + [< 'DOT _; _ = nsepseq selection dot >] -> () and injection kind element = parser - [< _=kind; _ = series element semi end_ >] -> () -| [< _=kind; 'End _ >] -> () -| [< _=kind; 'LBRACKET _; _ = bracketed element >] -> () + [< _=kind; _ = inj_suffix element >] -> () + +and inj_suffix element = parser + [< _ = series element semi end_ >] -> () +| [< 'End _ >] -> () +| [< 'LBRACKET _; _ = bracketed element >] -> () and bracketed element = parser [< _ = series element semi rbracket >] -> () @@ -228,9 +245,11 @@ and if_clause = parser | [< 'LBRACE _; _ = series statement comma rbrace >] -> () and case rhs = parser - [< 'Case _; _=expr; 'Of _; _ = cases rhs; 'End _ >] -> () -| [< 'Case _; _=expr; 'Of _; 'LBRACKET _; _ = cases rhs; - 'RBRACKET _ >] -> () + [< 'Case _; _=expr; 'Of _; _ = case_suffix rhs >] -> () + +and case_suffix rhs = parser + [< _ = cases rhs; 'End _ >] -> () +| [< 'LBRACKET _; _ = cases rhs; 'RBRACKET _ >] -> () and cases rhs = parser [< _ = nsepseq (case_clause rhs) vbar >] -> () @@ -241,11 +260,13 @@ and case_clause rhs = parser and loop = parser [< 'While _; _=expr; _=block >] -> () -| [< 'For _; 'Ident _; 'ASS _; _=expr; _ = opt down; - 'To _; _=expr; _ = opt step_clause >] -> () -| [< 'For _; 'Ident _; 'In _; _=expr; _=block >] -> () -| [< 'For _; 'Ident _; 'ARROW _; 'Ident _; 'In _; - _=expr; _=block >] -> () +| [< 'For _; 'Ident _; _=for_suffix >] -> () + +and for_suffix = parser + [< 'ASS _; _=expr; _ = opt down; + 'To _; _=expr; _ = opt step_clause; _=block >] -> () +| [< 'In _; _=expr; _=block >] -> () +| [< 'ARROW _; 'Ident _; 'In _; _=expr; _=block >] -> () and step_clause = parser [< 'Step _; _=expr >] -> () @@ -264,8 +285,10 @@ and disj_expr strm = left_assoc conj_expr or_ strm and conj_expr strm = left_assoc set_membership and_ strm and set_membership = parser - [< _ = core_expr; 'Contains _; _=set_membership >] -> () -| [< _ = comp_expr >] -> () + [< _ = comp_expr; _ = opt contains_clause >] -> () + +and contains_clause = parser + [< 'Contains _; _=set_membership >] -> () and comp_expr strm = left_assoc cat_expr op_comp strm @@ -303,11 +326,7 @@ and core_expr = parser [< 'Int _ >] -> () | [< 'Nat _ >] -> () | [< 'Mtz _ >] -> () -| [< 'Ident _ >] -> () -| [< 'Ident _; _ = brackets expr >] -> () -| [< 'Ident _; 'DOT _; _ = nsepseq selection dot; - _ = opt (brackets expr) >] -> () -| [< 'Ident _; _=arguments >] -> () +| [< 'Ident _; _ = opt core_suffix >] -> () | [< 'String _ >] -> () | [< 'Bytes _ >] -> () | [< 'C_False _ >] -> () @@ -321,12 +340,22 @@ and core_expr = parser | [< 'Nil _ >] -> () | [< _=structure >] -> () +and core_suffix = parser + [< _ = brackets expr >] -> () +| [< 'DOT _; _ = nsepseq selection dot; + _ = opt (brackets expr) >] -> () +| [< _=arguments >] -> () + and paren_expr = parser - [< _=disj_expr; 'COLON _; _=type_expr >] -> () -| [< _=disj_expr >] -> () -| [< _=disj_expr; 'COMMA _; _ = nsepseq expr comma >] -> () -| [< _ = case expr >] -> () -| [< _ = case expr; 'COMMA _; _ = nsepseq expr comma >] -> () + [< _=disj_expr; _ = opt paren_expr_1 >] -> () +| [< _ = case expr; _ = opt paren_expr_2 >] -> () + +and paren_expr_1 = parser + [< 'COLON _; _=type_expr >] -> () +| [< 'COMMA _; _ = nsepseq expr comma >] -> () + +and paren_expr_2 = parser + [< 'COMMA _; _ = nsepseq expr comma >] -> () and structure = parser [< _ = injection map binding >] -> () @@ -338,8 +367,11 @@ and selection = parser | [< 'Int _ >] -> () and record_expr = parser - [< 'Record _; _ = series field_assignment semi end_ >] -> () -| [< 'Record _; 'LBRACKET _; + [< 'Record _; _=record_expr_suffix >] -> () + +and record_expr_suffix = parser + [< _ = series field_assignment semi end_ >] -> () +| [< 'LBRACKET _; _ = series field_assignment semi rbracket >] -> () and field_assignment = parser @@ -366,12 +398,11 @@ and core_pattern = parser | [< 'Constr _; _ = opt tuple_pattern >] -> () | [< _ = injection list core_pattern >] -> () | [< 'Nil _ >] -> () -| [< _ = par paren_pattern >] -> () +| [< _ = par (opt paren_pattern) >] -> () and paren_pattern = parser - [< _=core_pattern; 'CONS _; _=pattern >] -> () -| [< _=core_pattern >] -> () -| [< _=core_pattern; 'COMMA _; _ = nsepseq core_pattern comma >] -> () + [< 'CONS _; _=pattern >] -> () +| [< 'COMMA _; _ = nsepseq core_pattern comma >] -> () and tuple_pattern = parser [< _ = par (nsepseq core_pattern comma) >] -> () From 3f47bb2e857b17df581c50196dccfa09a29eefeb Mon Sep 17 00:00:00 2001 From: Christian Rinderknecht Date: Thu, 29 Aug 2019 17:09:43 +0200 Subject: [PATCH 10/14] Recording as miscellaneous the old way to do series of items. --- src/parser/pascaligo/Doc/misc.txt | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 src/parser/pascaligo/Doc/misc.txt diff --git a/src/parser/pascaligo/Doc/misc.txt b/src/parser/pascaligo/Doc/misc.txt new file mode 100644 index 000000000..49fb5b8bd --- /dev/null +++ b/src/parser/pascaligo/Doc/misc.txt @@ -0,0 +1,27 @@ +(* The rule [series(Item,TERM)] parses a non-empty list of [Item] + separated by semicolons and optionally terminated by a semicolon, + then the terminal TERM. *) + +series(Item,TERM): + Item after_item(Item,TERM) { $1,$2 } + +after_item(Item,TERM): + SEMI item_or_closing(Item,TERM) { + match $2 with + `Some (item, items, term, closing) -> + ($1, item)::items, term, closing + | `Closing closing -> + [], Some $1, closing + } +| TERM { + [], None, $1 + } + +item_or_closing(Item,TERM): + TERM { + `Closing $1 + } +| series(Item,TERM) { + let item, (items, term, closing) = $1 + in `Some (item, items, term, closing) + } From 57b1d39b6ea72b688026197747a55438259a18bf Mon Sep 17 00:00:00 2001 From: Christian Rinderknecht Date: Thu, 29 Aug 2019 17:25:35 +0200 Subject: [PATCH 11/14] New contract in CameLIGO, based on the tutorial. (Not called from the CI.) --- src/contracts/incr_decr.mligo | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 src/contracts/incr_decr.mligo diff --git a/src/contracts/incr_decr.mligo b/src/contracts/incr_decr.mligo new file mode 100644 index 000000000..6e2f7e8f9 --- /dev/null +++ b/src/contracts/incr_decr.mligo @@ -0,0 +1,20 @@ +type storage = int + +(* variant defining pseudo multi-entrypoint actions *) + +type action = +| Increment of int +| Decrement of int + +let add (a : int) (b : int) : int = a + b + +let subtract (a : int) (b : int) : int = a - b + +(* real entrypoint that re-routes the flow based on the action provided *) + +let%entry main (p : action) storage = + let storage = + match p with + | Increment n -> add s n + | Decrement n -> subtract s n + in ([] : operation list), storage From 10469818c12729feb271f6029e806f1bcbe8450e Mon Sep 17 00:00:00 2001 From: Christian Rinderknecht Date: Thu, 26 Sep 2019 16:35:16 +0200 Subject: [PATCH 12/14] Removed `entrypoint` and `storage` as keywords. Bug fix: `n-1` was scanned as `n` and `-1`, which was rejected by a style constraint. I removed useless style constraints in the lexer. I removed dead code in `pascaligo.ml`. I added my first draft for the reference manual of PascaLIGO: DO NOT EDIT. Edit the website instead. About the bug fix: This was an awkward attempt at rejecting at lexing time negative integer literals whose sign is separated from the digits, like `- 1`. The fix was simple: remove the `integer` regular expression and use `natural`. --- src/parser/pascaligo/.links | 1 - src/parser/pascaligo/AST.ml | 31 - src/parser/pascaligo/AST.mli | 31 - src/parser/pascaligo/Doc/pascaligo.md | 1350 ++++++++++++++++++ src/parser/pascaligo/LexToken.mli | 2 - src/parser/pascaligo/LexToken.mll | 10 - src/parser/pascaligo/ParToken.mly | 2 - src/parser/pascaligo/Parser.mly | 44 - src/parser/pascaligo/ParserLog.ml | 35 - src/parser/pascaligo/SParser.ml | 13 - src/parser/pascaligo/Tests/crowdfunding.ligo | 77 +- src/parser/shared/Lexer.mli | 10 +- src/parser/shared/Lexer.mll | 24 +- src/simplify/pascaligo.ml | 22 - 14 files changed, 1395 insertions(+), 257 deletions(-) create mode 100644 src/parser/pascaligo/Doc/pascaligo.md diff --git a/src/parser/pascaligo/.links b/src/parser/pascaligo/.links index 1f30004d4..eff63d2f8 100644 --- a/src/parser/pascaligo/.links +++ b/src/parser/pascaligo/.links @@ -17,5 +17,4 @@ $HOME/git/ligo/src/parser/shared/Markup.ml $HOME/git/ligo/src/parser/shared/Markup.mli $HOME/git/ligo/src/parser/shared/Utils.mli $HOME/git/ligo/src/parser/shared/Utils.ml -$HOME/git/ligo/src/parser/shared/Version.ml Stubs/Simple_utils.ml diff --git a/src/parser/pascaligo/AST.ml b/src/parser/pascaligo/AST.ml index a94f3f869..1a45b6929 100644 --- a/src/parser/pascaligo/AST.ml +++ b/src/parser/pascaligo/AST.ml @@ -49,7 +49,6 @@ type kwd_contains = Region.t type kwd_down = Region.t type kwd_else = Region.t type kwd_end = Region.t -type kwd_entrypoint = Region.t type kwd_fail = Region.t type kwd_for = Region.t type kwd_from = Region.t @@ -71,7 +70,6 @@ type kwd_remove = Region.t type kwd_set = Region.t type kwd_skip = Region.t type kwd_step = Region.t -type kwd_storage = Region.t type kwd_then = Region.t type kwd_to = Region.t type kwd_type = Region.t @@ -219,7 +217,6 @@ and type_tuple = (type_expr, comma) nsepseq par reg and lambda_decl = FunDecl of fun_decl reg | ProcDecl of proc_decl reg -| EntryDecl of entry_decl reg and fun_decl = { kwd_function : kwd_function; @@ -245,36 +242,8 @@ and proc_decl = { terminator : semi option } -and entry_decl = { - kwd_entrypoint : kwd_entrypoint; - name : variable; - param : entry_params; - colon : colon; - ret_type : type_expr; - kwd_is : kwd_is; - local_decls : local_decl list; - block : block reg; - kwd_with : kwd_with; - return : expr; - terminator : semi option -} - and parameters = (param_decl, semi) nsepseq par reg -and entry_params = (entry_param_decl, semi) nsepseq par reg - -and entry_param_decl = - EntryConst of param_const reg -| EntryVar of param_var reg -| EntryStore of storage reg - -and storage = { - kwd_storage : kwd_storage; - var : variable; - colon : colon; - storage_type : type_expr -} - and param_decl = ParamConst of param_const reg | ParamVar of param_var reg diff --git a/src/parser/pascaligo/AST.mli b/src/parser/pascaligo/AST.mli index b9c7693cb..d3d848e91 100644 --- a/src/parser/pascaligo/AST.mli +++ b/src/parser/pascaligo/AST.mli @@ -33,7 +33,6 @@ type kwd_contains = Region.t type kwd_down = Region.t type kwd_else = Region.t type kwd_end = Region.t -type kwd_entrypoint = Region.t type kwd_fail = Region.t type kwd_for = Region.t type kwd_from = Region.t @@ -55,7 +54,6 @@ type kwd_remove = Region.t type kwd_set = Region.t type kwd_skip = Region.t type kwd_step = Region.t -type kwd_storage = Region.t type kwd_then = Region.t type kwd_to = Region.t type kwd_type = Region.t @@ -203,7 +201,6 @@ and type_tuple = (type_expr, comma) nsepseq par reg and lambda_decl = FunDecl of fun_decl reg | ProcDecl of proc_decl reg -| EntryDecl of entry_decl reg and fun_decl = { kwd_function : kwd_function; @@ -229,36 +226,8 @@ and proc_decl = { terminator : semi option } -and entry_decl = { - kwd_entrypoint : kwd_entrypoint; - name : variable; - param : entry_params; - colon : colon; - ret_type : type_expr; - kwd_is : kwd_is; - local_decls : local_decl list; - block : block reg; - kwd_with : kwd_with; - return : expr; - terminator : semi option -} - and parameters = (param_decl, semi) nsepseq par reg -and entry_params = (entry_param_decl, semi) nsepseq par reg - -and entry_param_decl = - EntryConst of param_const reg -| EntryVar of param_var reg -| EntryStore of storage reg - -and storage = { - kwd_storage : kwd_storage; - var : variable; - colon : colon; - storage_type : type_expr -} - and param_decl = ParamConst of param_const reg | ParamVar of param_var reg diff --git a/src/parser/pascaligo/Doc/pascaligo.md b/src/parser/pascaligo/Doc/pascaligo.md new file mode 100644 index 000000000..5f1b54a96 --- /dev/null +++ b/src/parser/pascaligo/Doc/pascaligo.md @@ -0,0 +1,1350 @@ +<# Documentation of PascaLIGO + +## A Walkthrough for the Impatient + +PascaLIGO is an imperative language for writing smart contracts on the +Tezos blockchain. As such, it is compiled to Michelson, the native +language of the Tezos blockchain. Its design is inspired by Pascal, +OCaml and Michelson. + + Why Pascal? One quality of Pascal is that its syntax is supported by +many, unabbreviated keywords and compound constructs are opened and +closed by those keywords, making Pascal programs easily readable and +unambiguous, albeit verbose, a desirable property of smart +contracts. In order to reduce the verbosity, PascaLIGO comes in two +flavours: _verbose_ and _terse_. Roughly speaking, this means that +some keywords can be replaced, in some contexts, by symbols. Those +styles are specified on the command line, for a whole contract, and +the default is "verbose". (See below for examples.) Pascal will not be +your only option though: LIGO offers multiple concrete syntaxes, one +of which is based on Pascal, but another one is based on OCaml --- and +more to come. + +If you're coming to LIGO from another language, chances are it is an +imperative language like C++ or Java. In an imperative language, +variables can change value over time through repeated assignment; as +opposed to functional languages like OCaml or Haskell where variables +tend to take one value during their lifetime. Formally, code that +changes the value of a variable is considered *mutating* or to have +*side effects*. An imperative language uses side effects in loops and +other control structures to change the contents of the memory. + +For example, here is how the integer value associated to the variable +`x` is incremented: + + x := x + 1; + +A loop computing the sum of all integers from 1 to 10 would be written +as follows: + + y := 0; + for x := 1 to 10 + begin + y := y + x + end + + In PascaLIGO, expressions and instructions are +distinguished. Expressions are evaluated and yield values, whilst +instructions are evaluated but do not yield values. Instructions are +meant to perform side-effects, like changing the value of a variable, +whereas expressions are purely computational. For instance, an +expression could be used to calculate an arithmetic mean. Instructions +and expressions can be compounded, and instructions can evaluate +expressions as a means to perform side-effects. + + PascaLIGO is _strongly and statically typed_, which means that the +composition of data and functions is contrained so the compiler can +check that no such composition can fail at run-time, e.g., because of +a meaningless expression. PascaLIGO requires that variables are +declared together with their type and an initial value. + + Declarations of values come in two kinds: either constants or +variables. The former are assigned only once at their declaration, and +the latter can be reassigned. The syntax is slightly different for +both. For example, the variables `x` and `y` above could have been +declared as follows: + + var x : nat := 0n; + var y : nat := 0n; + for x := 1n to 10n + begin + y := y + x + end + +You may have noticed that the literal `0n` has a letter attached to +the number, this is to disambiguate its type from the integer 0: `n` +stands for 'nat' and '0n' is a number of type nat (natural number) +whose value is zero. + +It is possible to define constant variables using the `const` keyword. + + const ten : nat = 10n; + const eleven : nat = ten + 1n; + +These variables have fixed value during their lifetime and **in future +versions of LIGO** will raise an error if code attempts to change +them: + + ten := 0n // Will raise an error in a future version! + +Note that the assignment operator for constants is `=`, but `:=` for +mutable variables (that is, annotated by `var` at their +declaration). + + Similarly, function declarations have their parameters and return +value annotated with their types. For instance, + + function sum (const n : nat; const m : nat) : nat is + begin + skip + end with n + m; + +declares a function `sum` that takes as argument two constant natural +numbers and returns their sum. The expression whose value is the +result of calling the function is given after the keyword `with`. Note +that to avoid forgetting a single instruction in a block, you need to +use the non-operation `skip`. + + A another familiar example would be + + function factorial (const n : nat) : nat is + var m : nat := 0n; + var f : nat := 1n; + begin + if n <= 0n then f := 1n + else + for m := 1n to n + begin + f := f * m + end + end with f + + Like Pascal, PascaLIGO offers procedures, as well as functions. The +difference follows the divide between expressions and instructions: +function calls are expressions, procedure calls are instructions. + + In order for a function to be a candidate to be an entrypoint to the +contract, it needs to return a specific type: `list (operation) * +store`, where `list (operation)` is the type for lists of operations +(see below, predefined types) and `store` is the type of the internal +storage of the contract. + + PascaLIGO features predefined types, like integers, natural numbers, +mutez (millionth of a tez), strings, maps, lists etc. and constructs +to combine those into structured types. Amongst those constructs are +the _records_, which group and map names (_fields_) to values of +potentially different types. For instance, + + type point is + record + x : int; + y : int + end + +defines a record type `point` with two fields, each made of a name +and a type. Values of record types are made by assigning a value to +each field (in any order). Like so: + + const origin : point = + record + x = 0; + y = 0 + end + + At this point it is perhaps useful to recall that there are actually +two styles, or flavours, of PascaLIGO: one is "verbose" and the other +is "terse". Those styles differ in the manner compound constructs are +delimited. For example, the type `point` above could have been +alternatively defined as follows in the terse style: + + type point is + record [ + x : int; + y : int + ] + +and the value as + + const origin : point = record [x = 0; y = 0]; + + When updating the fields of a record, PascaLIGO offers some +syntactic support. If you're only updating a small subset of +fields there is a shorthand: the _record patch_, which corresponds +to a functional update in OCaml. For example, + + var p : point := origin; + patch p with record y = 10 end; + +will update only the field `y` of `p`, leaving `x` unchanged. +Of course, this example is not impressive, but imagine that +one has to update a small number of fields in a large record. + + An alternative syntax, in terse style, is + + patch p with record [y = 10]; + + Another way to combine types are the _disjunctive types_ (also +called _algebraic data types_), which are a generalisation of +enumerated types, and found in OCaml. They can be interpreted as being +a disjoint partition of value sets, each being disinguished by a +unique tag, or _data constructor_. For example, + + type u = unit + type t = A | B of u | C of int * string + +See OCaml and, as in OCaml, their values can be matched against +patterns: + + match some_value_of_type_t with + A -> "A" + | B (Unit) -> "B" + | C (_, s) -> s + +Note also how type `u` is just another name for the predefined type +`unit`. This is an instance of a _type alias_. + + Another useful data abstraction, native to PascaLIGO, is the _map_, +which relates values of a given type to values of another given +type. For example, the type of maps from addresses to natural number +is written `map (address, nat)`. The address data type comes from Michelson. + + PascaLIGO is inspired by OCaml, where semicolons are separators, but +they can be used as terminators as well. For example + + type store is + record + goal : nat; (* Separator *) + deadline : timestamp; (* Separator *) + backers : map (address, nat); (* Separator *) + funded : bool + end + +can alternatively be written + + type store is + record + goal : nat; (* Separator *) + deadline : timestamp; (* Separator *) + backers : map (address, nat); (* Separator *) + funded : bool; (* Terminator *) + end + + PascaLIGO has predefined types that cannot be defined by the +contract programmer. Some of those types are specific to the Tezos +blockchain, like `timestamp` and `address` above. Others are the types +`list` and `map` above, but also `set` (sets of comparable +values). The rationale for the latter is not only that they are native +to Michelson, but also that PascaLIGO does not allow the programmer to +define neither recursive types, nor parametric types. In other words, +_user-defined types are monomorphic and non-recursive_. (Monomorphic +means a unique type.) For example, this limitation precludes defining +lists of values, as the type of lists is an inductive data type: a +list is either empty or a pair made of an item (the first item) and +another list (the remaining items). That is why PascaLIGO features a +_native polymorphic list type_, with the condition that all lists of +values must constrain the type of its values to be monomorphic. For +example, we saw above the type `list (operation)`. This reads as the +type constructor `list` being instantiated with the type +`operation`. A type constructor is like a function from types to +types. Note how the syntax reminds us of the analogy of applying data +constructors, or calling functions. + + As an example of list expression, a non-empty list starts with the +keyword `list` and contains its elements separated by semicolons +(definition by extension): + + list 1; 2; 3 end + +Accordingly, the empty list is + + list end + +but also has a shorthand in the manner of a keyword, because it is +quite common: + + nil + +Note that the use of `nil` is acceptable in both verbose and terse +style. + + To push an element in an existing list (an operation called +_consing_ in functional languages), the infix operator to use is +`#`. It takes on the left the element and on the right the list. For +example, the list containing `1`, then `2` and then all items of list +`l` is written: + + 1#(2#l) + +or, simply (because the `#` operator is right-associative): + + 1#2#l + + All user-definable values in PascaLIGO are monomorphic and must be +annotated with their types at declaration (since their type is +given in the left-hand side). Arithmetic or boolean expressions do not +need to be annotated, but empty lists need to be, like so: + + 1#(nil : list (int)) + +But + + var l : list (int) := nil + +is also accepted because the type of `nil` here is available in the +left-hand side. + +## Comments + +PascaLIGO features comments as blocks, that is, spanning one or more +lines, and inline, that is, spanning the end of a line. The syntax of +the former is based on Pascal: + + (* This is + a block comment *) + +The latter is inspired from C++: + + // This is a line comment + +## Predefined types and values + +### Primitive types + +The predefined types of PascaLIGO are lifted from Michelson, so the +programmer knows that they map exactly to their counterpart in the +generated Michelson, which, in turn, help in assessing the gas cost. Some +of those types are specific to the Tezos blockchain, and, when used, +make PascalLIGO a Domain-Specific Language (DSL). + +#### Unit + +The predefined type `unit` has a unique value `Unit`. It is useful +when no logical value, that is, information, can be deduced from an +expression, typically performing a side effect. + +#### Numerical types + +There are three kinds of native numerical types in PascaLIGO: `int`, +`nat` and `tez`. + + * The first is the type of signed integers, e.g., `-4`, `0` or +`13`. Note that the value zero has a canonical form, `0`, and no +other, for example `00` is invalid. Also, for the sake of convenience, +underscores are allowed in the literals, like `1_000_000`. + + * The second numerical type is the type of the natural numbers, +e.g., `0n` or `13n`. Note that the `nat` literals must be annotated +with the suffix `n`, which distinguishes them from `int` literals. The +same convenient use of underscores as with integer literals is allowed +too and the canonical form of zero is `0n`. + + * The last kind of native numerical type is `tez`, which is a unit +of measure of the amounts (fees, accounts). Beware: the literals of +the type `tez` are annotated with the suffix `mtz`, which stands for +millionth of Tez, for instance, `0mtz` or `1200000mtz`. The same handy +use of underscores as in natural literals help in the writing, like +`1_200_000mtz`. + +To see how numerical types can be used in expressions see the sections +"Predefined operators" and "Predefined values". + +#### Bytes + +Bytes have the same type as in Michelson and the same notation for the +literals. The type `bytes` denotes the arrays of hexadecimal numbers +of even length, prefixed by `0x`. For example, `0xA5` or `0xEFFF`. It +is possible to use underscores to make long bytes more readable, like +so: `0x00_A5_EF`. Odd-lengthed or negative bytes are invalid. + +#### Booleans + +The type of the booleans is `bool`. The only two boolean values are +`True` and `False`. Note the upper case of the first letters, showing +that those are data constructors. (See variant types below.) + +#### Strings + +The type of the strings is `string`. String values are a contiguous +series of characters enclosed between double quotes, e.g., `"A +string."`. Control characters (including line breaks) are not allowed +unless they are escaped with a preceding backslash, like `"\n"`. + +#### Blockchain-specific types + +PascaLIGO features predefined types that are specific to the Tezos +blockchain: `operation`, `address`, `key`, `key_hash`, `signature` and +`timestamp`. + +#### Options + +When the need for an optional value arises, the programmer can use the +predefined type constructor `option`. It applies to a PascaLIGO type +to make it optional, for example, the type of an optional integer is +`option (int)`. All instances of `option` are variant types. Given a +type `foo`, the values of the type `option (foo)` are either `None` or +`Some (v)` where `v` has type `foo`. For example, `Some (4)` is a +value of type `option (int)`. + +Options are an instance of a variant type. See section "Variants". + +#### Lists + +The type constructor `list` is used to create types of lists. For +example, the type of lists of integers is `list (int)`. All instances +of `list` are variant types with two kinds of values. A list is either +empty, denoted by `nil` or `list end`, or non-empty, in which case the +values it contains are written in order separated by semicolons and +between the keywords `list` and `end`. For example, the list +containing the integers `1`, `2` and `3` is written + + list 1; 2; 3 end + + or + + list 1; 2; 3; end + +(terminating semicolon). A complete declaration of the constant list +above would be: + + const my_list : list (int) = list 1; 2; 3 end + +The _terse style_ of writing PascaLIGO allows the programmer to write + + list [1;2;3] + +instead of `list 1; 2; 3 end` (_verbose style_). For readability's +sake, both styles cannot be mixed in the same contract. + +To see what operations are available on lists, see the section +"Predefined operators" and "Predefined functions". + +#### Sets + +The type constructor `set` is used to create ordered sets of +(comparable) values. For example, the type of sets of integers is `set +(int)`. Set values follow the same convention as lists, e.g., + + set 3; 1; 2 end + +(a terminating semicolon is possible) which is the same value as + + set 1; 2; 3 end + +because elements of a set are unordered (even though they have to be +comparable). A complete declaration of the constant map above would +be: + + const my_set : set (int) = set 3; 1; 2 end + +The _terse style_ of writing PascaLIGO allows the programmer to write + + list [1;2;3] + +instead of `list 1; 2; 3 end` (verbose style). For readability's sake, +both styles cannot be mixed in the same contract. + +To see how to update a given set, see the section "Instructions/Set +updates". + +#### Maps + +The type constructor `map` is used to create mappings between +values. A map can be modelled as a set of _bindings_, and each binding +is a pair of values with the convention that the first component of +the pair is the source, or _key_, and the second is the destination, +or _value_. As such, `map` requires a pair of type arguments, for +example, `map (int, string)` is the type of the maps from integers +(the keys) to strings (the values). A constant map containing a +binding from `1` to `"one"` would be declared as follows: + + const my_map : map (int, string) = map 1 -> "one" end + +(A terminating semicolon is possible.) Another example is a map that +denotes a permutation of the set of integers `1`, `2` and `3`: + + const perm : map (int, int) = map 1 -> 3; 2 -> 1; 3 -> 2 end + +The _terse style_ of writing PascaLIGO allows the programmer to write + + map [1 -> 3; 2 -> 1; 3 -> 2] + +instead of `map 1 -> 3; 2 -> 1; 3 -> 2 end` (_verbose style_). For +readability's sake, both styles cannot be mixed in the same contract. + +To see how to update a given map, see the section "Instructions/Map +updates". + +#### Big maps + +Big maps is a type lifted from Michelson, and called `big_map`. As far +as the language itself is concerned, there is no syntactic difference +between maps and big maps. The interpretation of big maps is specified +by the command-line of the LIGO compiler. + +### Predefined operators + +#### Numeric values + +Values of the same given numerical type (integers, naturals, mutez) +can be used in arithmetic expressions. The comparison operators on +numerical types are: `=`, `<`, `<=`, `>`, `>=`, and, notably, the +difference operator is written `=/=`. The arithmetic operators are the +usual ones: `+`, `-` (binary and unary), `/` and `*` are _overloaded_, +which means that they can apply to arguments of different types. For +example, the following expression is valid: + + 3 * 4 + +as well as + + 3n * 4n + +#### Booleans + +Boolean values can be compared with the predefined operators `=` and +`=/=` (inequality). See the section "Instructions/Conditional" to see +the implicit equality in the tests of conditionals. The dedicated +boolean operators are `and` (logical conjunction), `or` (logical +disjunction) and `not` (logical negation). + +#### Strings + +Strings can be compared for equality and inequality by means of the +predefined operators `=` and `=/=`. They can be concatenated by means +of the operator right-associative predefined operator `^`, like so: + + "This is a prefix" ^ " and " ^ "this is a suffix." + +### Lists + +Lists can be augmented by adding an item (as their new head) with the +operator `#`, like so: + + (1,"one")#(2,"two")#nil + +which is the list containing the pair `(1,"one")` as first item (head) +and `(2,"two")` as the second and last item. This is the same list as + + list [(1,"one"); (2,"two")] + +in terse style (see section "Predefined types and values/Lists"). + +#### Tuples + +Given a tuple `t` with _n_ components, the `i`th component is + + t.(i) + +where `t.(0)` is the first component. For example, given the +declaration + + const t : int * string = (4, "four") + +the expression `t.(1)` has the value `"four"`. + +#### Records + +Record values can be projected, that is, their fields can be selected, +by means of the dot operator: if a record `r` has a field `f`, then +`r.f` has the value associated to the field `f` in `r`. For example, +given the declarations (in verbose style) + + type rec_t = record f : int end + const r : rec_t = record f = 4 end + +then the value of `r.f` is `4`. + +### Predefined functions, procedures and instructions + +Beyond a few operators, PascaLIGO features some predefined values and +functions. + +#### Tezos-specific + +The following are predefined values lifted from Michelson: +`get_force`, `transaction`, `get_contract`, `amount`, `now`, `source`, +and `sender`. + +#### Numeric types + +It is always safe to cast a natural number (that is, a value of type +`nat`) to an integer. This is done by calling the predefined function +`int`, like so: + + const m : nat = 7n + const n : int = int (m) + +The absolute value of an integer is a natural number, which provides a +way to cast positive integers into natural numbers, like so: + + const m : int = 6 + const n : nat = abs (m) + +#### Strings + +The call `string_slice (offset, length, string)` to the predefined +function `string_slice` evaluates in the substring of `string` +starting at the offset `offset` (included, first character being at +offset 0) and of length `length`. The result is actually an optional +string: if `offset + length` is greater than the length of `string`, +the result is `None`, otherwise `Some (substring)`. See section +"Options". + +#### Lists + +PascaLIGO offers two kinds of iterators on lists. + +The first applies a given function to all the items of a given list, +each call returning the predefined value `Unit`. If the function name +is `f` and the list is `l`, this is expressed as + + list_iter (l, f); + +Note: `list_iter` is a predefined _procedure_. Procedures are +functions that return `Unit` and whose calls are instructions, not +expressions. The same holds for the iterated function `f` here. See +section "Declarations/Procedures". + +For an iterator like `list_iter` to be useful, it needs to be able to +perform a side effect, which user-defined procedures and functions +cannot do. Like so: + + function iter (const delta : int; const l : list (int)) : int is + var acc : int := 0 + procedure aggregate (const i : int) is + begin + acc := acc + i + end + begin + aggregate (delta); // Has no effect on acc + list_iter (l, aggregate) // Has an effect on acc + end with acc + +The other predefined iterator on lists is `list_map`. It is useful +when we need to apply a function to all the items of a list and gather +them into another list, in the same order as the original items. (In +mathematical terms, `list_map` builds the list of the images through +the function.) For instance, the function `iter` + + function iter (const l : list (int)) : list (int) is + function incr (const i : int) : int is + begin + skip + end with i+1 + begin + skip + end with list_map (l, incr) + +will take a list of integers as a parameter and return a list with the +integers all incremented, e.g., `iter (list [1;2;3])` evaluates in +`list [2;3;4]`. + +#### Sets + +Sets have no built-in operators. Instead, PascaLIGO offers predefined +functions to update sets. + + - The function `set_mem` tests for membership in a set. It is the + same as the boolean expression + + my_set contains my_value + + which is `True` is the set `my_set` contains the value `my_value`, + otherwise `False`. In functional form: + + set_mem (my_value, my_set) + + - The function `set_add` adds an element to a set: + + set_add (my_value, my_set) + + evaluates into a set that contains all the elements of the set + `my_set`, plus the element `my_value` (the original set `my_set` + is unchanged because there are no side effects on the context of a + function call). If `my_value` was already present in `my_set`, + then the returned set is the same as `my_set` (mathematical set). + + PascaLIGO also enables the addition of elements by means of a side + effect. This is when a mutable variable, that is, a variable + annotated with `var` at its declaration, needs to be modified by + an instruction. When that variable is a set, for example, in terse + style: + + var s : set (int) := set [1;4;2] + + PascaLIGO offers the "patch" instruction to add elements to + `s`. It takes the mutable set `s` and a set constant (that is, a + set defined by listing all its elements) and adds all the elements + of the latter to the former, with a side effect. For example, let + us add the elements `5`, `3` and `4`, all at once, to `s` (in + terse style): + + patch s with set [5; 3; 4]; + + After that instruction, the value of `s` is `set [1;2;3;4;5]` + --- which is the same as `set [4;2;1;5;3]`, of course. + + - The function `set_remove` builds a set by taking a set and + removing a given value from it: + + set_remove (my_value, my_set) + + is a set containing all the elements of the set `my_set`, except + the element `my_value`. In particular, if `my_value` was not in + `my_set`, the resulting set is identical to `my_set`. + + There is also a special instruction (as opposed to an expression + like `set_remove (my_value, my_set)`) to remove elements from a + set: + + remove my_value from set my_set + + In this case, `my_set` must have been declared with the `var` + annotation of mutable variables. + + - The function `size` returns the cardinal of a set. For instance, + the expression (in terse style) + + size (set ["a"; "a"; "b"; "c"]) + + has value `3`. + + + - The iterator `set_iter` is similar to `list_iter`: it takes a set + and a procedure (or function returning `Unit`) and applies it in + turn to all the elements of the set. + + - Another form of complete iteration on sets is performed by + loops. See section "Loops". + +#### Maps + +Currently, maps have less support than sets. PascaLIGO offers the +following functions and procedures on maps: + + - Adding bindings to a map is only possible if the map is mutable, + that is, if it was declared with the annotation `var`, like so, in + terse style: + + var m : map (int, string) := map [2 -> "deux"; 3 -> "three"] + + Then, a destructive update can be performed with a patch, as with + sets (in terse style), For example, the instruction + + patch m with map [1 -> "one"; 2 -> "two"]; + + modifies the value of `m` to be the same as + + map [1 -> "one"; 2 -> "two"; 3 -> "three"] + + - When exactly one binding is added or modified, PascaLIGO offers a + shorter syntax by reusing the assignement operator like so: + + my_map[my_key] := my_value; + + That instruction addes the binding from `my_key` to `my_value` + into the map `my_map` (hiding any previous binding for the key + `my_key`). + + - To check for the existence of a binding in a map for a given key, + the programmer should simply reuse the `case` instruction. For + example, to check whether there is a binding for the key `2` in + the map `m` above, one would write + + case m[2] with + Some (value) -> ... // The value is "two", here. + | None -> ... // Should only happen if 2 is not a key. + end + + (See the section "Instructions/Pattern matching".) + + Generally speaking, the type of `m[k]` is `option (value)` if the + type of `m` is `map (key, value)` and `k` is of type `key`. + + - Removing a binding from a map requires a special instruction, like + + remove sender from map backers + + where `sender` is a key and `backers` is a map. If the key is + absent in the map, this instruction is a non-operation. + + - The iterator `map_iter` is similar to `list_iter`: it takes a set + and a procedure (or function returning `Unit`) and applies it in + turn to all the bindings of the map. The type of the iterated + procedure/function is expected to be `key * value -> unit`. + + - The iterator `map_map` is similar to `list_map`: it takes a map + and a function and builds a new map by applying the function to + all the bindings. In particular, this means that the expected + return type of the iterated function must be the type of the + values in the map. + + - Another form of complete iteration on maps is performed by + loops. See section "Loops". + +#### Failures + +When an invariant is not satisfied in a contract, it can fail by using +the keyword `fail` followed by a string as a parameter, like so: + + fail "This is an error message." + +Note that, were `fail` a function name, we would write instead + + fail ("This is an error message.") + +and, indeed, you can do so, but `fail` is a keyword, like `if`, so you +can chose. + + +## Declarations + +There are several kinds of declarations: types, mutable variables, +constants, functions, procedures, fields. Depending on the syntactic +context, only some of those declarations will be allowed. Declarations +may be separated by a semicolon. (Because each declaration starts with a +keyword they can be parsed without separators.) + + +### Types + +Type declarations are found only at top-level, that is, outside any +function or procedure. They associate a type name to a type +expression. The general syntax is + + type some_type_name is some_type_expression + +where `type` and `is` are keywords. + +#### Tuples + +Tuples are a nameless product of types, as usually found in +mathematics. A particularly useful case is the _pair_, to wit, `(3, +"three")` is a value of a pair type. A corresponding type could be +declared as follows: + + type my_pair is nat * string + +The operators `*` is the product on types. + +Surprisingly, few programming languages support a notation for tuples, +counter-examples being found mostly amongst functional languages. An +example of a _triple value_ is: `(-3, True, "whatever")`. The only +possible type expression for it is `int * bool * string`. + +#### Records + +A record is the product of types (called _field types_) indexed by +names (called _field names_). They are called "struct" in C/C++. For +example, in verbose style: + + type store is + record + goal : mutez; // Millionth of a tez + deadline : timestamp; + backers : map (address, nat); + funded : bool + end + +A value of that type could be + + record + goal = 10mtz; + deadline = "..."; + backers = map end; + funded = False + end + +#### Variants + +The dual type of product types (that is, record and tuple types) are +the sum types, also called here _variant types_. We have seen an +example above in the option type. For example, the type `option (int)` +has two kinds of values: `None` to mean that there is no integer, and +`Some (n)`, where `n` is an integer. This partioning of the values +(`None` vs. `Some`) is what makes it a variant: a value is either of +one shape or the other. + +We can imagine that there are more cases too. Consider: + + type suit is Heart | Spade | Club | Diamond + +The type `suit` has exactly four values, each with a unique name. Note +that, just as with the `option` type, those names are not variables: +they are the value itself, and, as such, they are called _data +constructors_. + +This kind of definition is found in mainstream programming languages +as _enumerated types_. Similarly, we would declare + + type rank is + Ace | Two | Three | Four | Five | Six | Seven | Eight + | Nine | Ten | Jack | Queen | King + +And a card could be defined as a pair of a suit and a rank, like so: + + type card is suit * rank + +Actually, variant types are more general than enumerated types, +whereby a value is associated to each data constructor, and we have +seen that with the `option` type when we write `Some (4)` (the piece +of data here is `4`). For instance, here is an alternative definition +for the cards: + + type card is + Heart of rank + | Spade of rank + | Club of rank + | Diamond of rank + +so `Heart (Ace)` is a value of type `card` now. We recommend the +reader to read about variant types in OCaml to become acquainted with +their possibilities. (They are also called _algebraic data types_.) + +See the section "Instructions/Pattern matching". + +#### Aliases + +Type aliases are simply another name given to an existing type that +has a name. In other words, the type expression in the declaration is +a type name, like + + type trump is card + +### Values + +Value declarations are of two kinds: mutable variables and constants. + +#### Constants + +Constant declarations bind the value of an expression to a value name +and that value cannot be changed. Another way to put it is to say that +these are singly assigned variables. The general shape of the +declaration is + + const my_name : my_type = my_expression + +Note the `const` keyword and the constant assignment operator `=` (not +`:=`). For example, given the declaration + + const three : nat = 1n + 2n + +the following assignment + + three := three + 2n + +_will be invalid in a future version of LIGO_. Remember also that +`three = three + 2n` is valid but is a boolean expression whose value +is `False` (the symbol `=` means "is, by definition" when used in a +declaration, and "equals to" in an expression). + +#### Mutable variables + +Like constant declarations, declarations of mutable variables bind a +name to a value, but that value can be reassignment after the +declaration. The general shape is + + var my_name : my_type := my_expression + +Note the keyword `var` and the assignment operator `:=` (not `=`). For +example, given the declaration + + var counter : nat := 1n + +the following assignment + + counter := counter + 2n + +is valid and changes the value of the mutable variable `counter` to be +`3n`. This is the semantics found in all imperative languages. + +IMPORTANT: Mutable variables cannot be declared at top-level, but only +in the scope of function and procedure bodies. This is to avoid global +side effects that hide the control flow and makes static analysis +extremely difficult. + +### Functions + +Function declarations can occur both at top-level and inside functions +and procedures (in the tradition of Pascal). We saw an example +earlier: + + function iter (const l : list (int)) : list (int) is + function incr (const i : int) : int is + begin + skip + end with i+1 + begin + skip + end with list_map (l, incr) + +Here, the function `incr` is declared inside the declaration of the +function `iter`. The general shape of a function declaration is + + function my_name ( ... (* parameters here *)) : return_type is + ... // local declarations here + begin + ... // instructions here + end with ... // return expression here + +where `function`, `is`, `begin`, `end` and `with` are keywords. For +example, + + function sum (const n : nat; const m : nat) : nat is + begin + skip + end with n + m; + +declares a function `sum` that takes as argument two constant natural +numbers and returns their sum. The expression whose value is the +result of calling the function is given after the keyword `with`. Note +that to avoid forgetting a single instruction in a block, you need to +use the non-operation `skip`. + +A another familiar example would be + + function factorial (const n : nat) : nat is + var m : nat := 0n; + var f : nat := 1n; + begin + if n <= 0n then f := 1n + else + for m := 1n to n + begin + f := f * m + end + end with f + +IMPORTANT: The semantics of function calls is particular in PascaLIGO: +_the arguments are always copied_, even if the corresponding parameter +is annotated with `var`. So, given the declarations + + function foo (var n : int) : unit is + begin + n := n + 1 + end with Unit + +and + + var m : int := 5 + +the call `foo (m)` will leave the value of `m` invariant. + +Moreover, _the environment at the call site is also always +copied_. This is perhaps the most puzzling feature of PascaLIGO +functions (in fact, they should be called _quotations_, not functions, +for that very reason). The environment at a point in the program is +the set of variables in scope (that is, variables we can refer +to). The point here is that if it does not matter if those variables +in the environment have been declared `const` or `var`: they will all +be copied, so the body of the called function will deal with +copies. Let us copy an example seen above: + + function iter (const delta : int; const l : list (int)) : int is + var acc : int := 0 + procedure aggregate (const i : int) is + begin + acc := acc + i // acc is part of the copied environment + end + begin + aggregate (delta); // Has no effect on acc + end with acc + +Another spin on this topic consists in declaring that functions are +pure for the caller, that is, _the environment is left unchanged by +function calls_. The only way to observe a change is to receive a +value in return. + +IMPORTANT: _Functions cannot be recursive in PascaLIGO_, that is why +loops or iterators are needed. + +### Procedures + +WARNING: Procedures are not implemented in the current version of LIGO, they +will appear in a future version with these semantics but cannot currently be +used. + +Procedures are a special kind of functions that return `Unit`. They +are declared as follows: + + procedure my_name ( ... (* parameters here *)) is + ... // local declarations here + begin + ... // instructions here + end + +Since function calls (see section "Functions") leave the environment +invariant, one may wonder what use there is to procedures. As we have +seen in the section about "Lists" and their iterators, the exception +to this rule are predefined iterators, like `list_iter`. They actually +allow the iterated function to perform side effects. Here is the +example again: + + function iter (const delta : int; const l : list (int)) : int is + var acc : int := 0 + procedure aggregate (const i : int) is + begin + acc := acc + i + end + begin + aggregate (delta); // Has no effect on acc + list_iter (l, aggregate) // Has an effect on acc + end with acc + +(For the keen reader, this is because the iterated function is inlined +by the compiler.) + +## Instructions + +In PascaLIGO distinguishes between expressions and instructions. The +former have values, whilst the latter do not. The latter may perform +side effects, whilst the former cannot. + +### Assignments + +The most obvious kind of instruction is the assignment: + + i := i + 1 + +### Loops + +There are two kinds of loops in PascaLIGO: bounded and +conditioned. The former is often called a _for_ loop, and the latter a +_while_ loop. The most general is the latter, as is well known, has +has the form + + while my_expression + begin + ... // instructions here + end + +in verbose style, or + + while my_expression + block { + ... // instructions here + } + +in terse style. + +The semantics is the usual: the block (body) of the loop is executed +as long as the value of `my_expression` is `True`. + +WARNING: The for loop is not implemented in the current version of LIGO. It will +be added with these semantics in future versions, but cannot be used in programs yet. + +The syntax for the _for_ loops is more complex because it used to +iterated on collections like sets and maps. Let us start with a simple +case of iteration on integers: A loop computing the sum of all +integers from 1 to 10 would be written as follows: + + y := 0; + for x := 1 to 10 + begin + y := y + x + end + +(Note that this is useless in practice, as a closed-form formula +exists for that computation.) + +To iterate on a set `s`, we would write, for instance, + + for e in s + begin + ... // instructions + end + +where `e` is bound in turn in increasing orde to each element of the +set `s`. For example, given the declarations + + const s : set (int) = set 3; 1; 2 end + var sum : int := 0 + +the instruction + + for n in s + begin + sum := sum + n + end + +has the side effect of storing `6` (`1+2+3`) in `sum`. + +To iterate on maps, the syntax is + + for key -> value in m + begin + ... // instructions + end + +Here, the variables `key` and `value` will be bound in increasing +order to each key and value of each binding before the block is +executed. + +### Conditionals + +Conditionals in PascaLIGO are instructions made of a conditional +expression (that is, a boolean expression), and two clauses. The +general shape is + + if my_condition then true_expression else false_expression + +We have seen a familiar example above: + + function factorial (const n : nat) : nat is + var m : nat := 0n; + var f : nat := 1n; + begin + if n <= 0n then f := 1n + else + for m := 1n to n + begin + f := f * m + end + end with f + +### Pattern matching + +Pattern matching is a generalisation of some constructs found in +mainstream imperative languages, like `switch` in Java, or `case` in +Pascal, those, in turn, being a generalisation of conditionals. They +provide a way to destructure compounded values without the need to +write a cascade of embedded conditionals. The general syntax is + + case my_expression of + my_pattern_1 -> my_instruction_1 + | my_pattern_2 -> my_instruction_2 + ... + | my_pattern_n -> my_instruction_n + end + +First, the `case` construct is an instruction, not an expression, and +this can be seen from the fact that we find instructions on the +right-hand sides of the arrows. The informal meaning is this: evaluate +the expression `my_expression`, then "match" the resulting value with +the pattern `my_pattern_1`. If there is a match (we will define this +later), then `my_instruction_1` is executed; otherwise, try matching +`my_pattern_2` etc. In PascaLIGO, the compiler checks that pattern +matchings are complete, so there is no need for a catch-all pattern: +one will have to match. + +Let us consider the a function that receives a pair of integers and +returns their sum, except if any of those is zero, in which case it +returns zero: + + function pair_sum (const p : int * int) : int is + var res : int := 0 + begin + case p of + (0,_) -> skip + | (_,0) -> skip + | (m,n) -> res := m + n + end + end with res + +We can see that the last pattern contains the variables, `m` and `n`, +thus matches any pair of values: conditionals can only evaluate +boolean expressions as their test, whereas pattern matching can bind +variables. The binding is evident here because `m` and `n` are used on +the right-hand side of the arrow of the last case: `m + n`. The +underscores `_` in the first two patterns stand for a unique and +unknown variable. + +Here is the logical disjunction: + + function logical_or (const p : bool * bool) : bool is + var res : bool := True + begin + case p of + (False, False) -> res := False + | _ -> skip + end + end with res + +The values that are usually destructured are of variant types, for +which there are many cases. Let us revisit the card game above: + + type suit is Heart | Spade | Club | Diamond + type face is Ace | King | Queen | Jack + type pip is + Two | Three | Four | Five | Six | Seven | Eight | Nine | Ten + type rank is + Face of face + | Pip of pip + type card is + Ordinary of suit * rank + | Joker + +Individual cards can be declared as follows: + + const jack_of_spade : card = Ordinary (Space, Jack) + +A function returning the numerical value of a card could be declared +as follows: + + function val_of_face (const f : face) : nat is + var val : nat := 0n + begin + case f of + Ace -> val := 14n + | King -> val := 13n + | Queen -> val := 12n + | Jack -> val := 11n + end + end with val + + function val_of_pip (const p : pip) : nat is + var val : nat := 0n + begin + case p of + Ten -> val := 10n + | Nine -> val := 9n + | Eight -> val := 8n + | Seven -> val := 7n + | Six -> val := 6n + | Five -> val := 5n + | Four -> val := 4n + | Three -> val := 3n + | Two -> val := 2n + end + end with val + + function value (const c : card) : nat is + var val : nat := 0n + begin + case c of + Ordinary (_, Face (f)) -> val := val_of_face (f) + | Ordinary (_, Pip (p)) -> val := val_of_pip (p) + | Joker -> val := 15n + end + end with val + +### Non-operation + +PascaLIGO has an explicit keyword for the non-operation: `skip`. Using +`skip` makes it clear that there was no omission. + +## Unsupported Functionalities + +### Major Functionalities + +- The `for` loop is not supported yet. + +- Procedures are not supported yet. + +- Nested code blocks are not supported yet. + +### Minor Functionalities + +- The value `None` cannot be assigned to a variable. + +- Assignments to nested maps are not currently supported. + +- You cannot patch an empty record. + +- Map patches are not supported yet. + +- Set patches are not supported yet. + +- Removal of bindings in nested maps is not supported yet. + +- Elements cannot be removed from a set using the `remove` keyword. diff --git a/src/parser/pascaligo/LexToken.mli b/src/parser/pascaligo/LexToken.mli index aee80d628..fd79652d8 100644 --- a/src/parser/pascaligo/LexToken.mli +++ b/src/parser/pascaligo/LexToken.mli @@ -79,7 +79,6 @@ type t = | Down of Region.t (* "down" *) | Else of Region.t (* "else" *) | End of Region.t (* "end" *) -| Entrypoint of Region.t (* "entrypoint" *) | Fail of Region.t (* "fail" *) | For of Region.t (* "for" *) | From of Region.t (* "from" *) @@ -101,7 +100,6 @@ type t = | Set of Region.t (* "set" *) | Skip of Region.t (* "skip" *) | Step of Region.t (* "step" *) -| Storage of Region.t (* "storage" *) | Then of Region.t (* "then" *) | To of Region.t (* "to" *) | Type of Region.t (* "type" *) diff --git a/src/parser/pascaligo/LexToken.mll b/src/parser/pascaligo/LexToken.mll index 989e9fbec..e08ea56eb 100644 --- a/src/parser/pascaligo/LexToken.mll +++ b/src/parser/pascaligo/LexToken.mll @@ -77,7 +77,6 @@ type t = | Down of Region.t (* "down" *) | Else of Region.t (* "else" *) | End of Region.t (* "end" *) -| Entrypoint of Region.t (* "entrypoint" *) | Fail of Region.t (* "fail" *) | For of Region.t (* "for" *) | From of Region.t (* "from" *) @@ -99,7 +98,6 @@ type t = | Set of Region.t (* "set" *) | Skip of Region.t (* "skip" *) | Step of Region.t (* "step" *) -| Storage of Region.t (* "storage" *) | Then of Region.t (* "then" *) | To of Region.t (* "to" *) | Type of Region.t (* "type" *) @@ -210,7 +208,6 @@ let proj_token = function | Down region -> region, "Down" | Else region -> region, "Else" | End region -> region, "End" -| Entrypoint region -> region, "Entrypoint" | Fail region -> region, "Fail" | For region -> region, "For" | From region -> region, "From" @@ -232,7 +229,6 @@ let proj_token = function | Set region -> region, "Set" | Skip region -> region, "Skip" | Step region -> region, "Step" -| Storage region -> region, "Storage" | Then region -> region, "Then" | To region -> region, "To" | Type region -> region, "Type" @@ -304,7 +300,6 @@ let to_lexeme = function | Down _ -> "down" | Else _ -> "else" | End _ -> "end" -| Entrypoint _ -> "entrypoint" | Fail _ -> "fail" | For _ -> "for" | From _ -> "from" @@ -326,7 +321,6 @@ let to_lexeme = function | Set _ -> "set" | Skip _ -> "skip" | Step _ -> "step" -| Storage _ -> "storage" | Then _ -> "then" | To _ -> "to" | Type _ -> "type" @@ -366,7 +360,6 @@ let keywords = [ (fun reg -> Down reg); (fun reg -> Else reg); (fun reg -> End reg); - (fun reg -> Entrypoint reg); (fun reg -> For reg); (fun reg -> From reg); (fun reg -> Function reg); @@ -388,7 +381,6 @@ let keywords = [ (fun reg -> Set reg); (fun reg -> Skip reg); (fun reg -> Step reg); - (fun reg -> Storage reg); (fun reg -> Then reg); (fun reg -> To reg); (fun reg -> Type reg); @@ -576,7 +568,6 @@ let is_kwd = function | Down _ | Else _ | End _ -| Entrypoint _ | Fail _ | For _ | From _ @@ -598,7 +589,6 @@ let is_kwd = function | Set _ | Skip _ | Step _ -| Storage _ | Then _ | To _ | Type _ diff --git a/src/parser/pascaligo/ParToken.mly b/src/parser/pascaligo/ParToken.mly index 67dbaeb25..e62d3d583 100644 --- a/src/parser/pascaligo/ParToken.mly +++ b/src/parser/pascaligo/ParToken.mly @@ -53,7 +53,6 @@ %token Down (* "down" *) %token Else (* "else" *) %token End (* "end" *) -%token Entrypoint (* "entrypoint" *) %token Fail (* "fail" *) %token For (* "for" *) %token Function (* "function" *) @@ -75,7 +74,6 @@ %token Set (* "set" *) %token Skip (* "skip" *) %token Step (* "step" *) -%token Storage (* "storage" *) %token Then (* "then" *) %token To (* "to" *) %token Type (* "type" *) diff --git a/src/parser/pascaligo/Parser.mly b/src/parser/pascaligo/Parser.mly index 34b4db971..6f36586bb 100644 --- a/src/parser/pascaligo/Parser.mly +++ b/src/parser/pascaligo/Parser.mly @@ -234,7 +234,6 @@ field_decl: lambda_decl: fun_decl { FunDecl $1 } | proc_decl { ProcDecl $1 } -| entry_decl { EntryDecl $1 } fun_decl: Function fun_name parameters COLON type_expr Is @@ -260,33 +259,6 @@ fun_decl: terminator = $11} in {region; value}} -entry_decl: - Entrypoint fun_name entry_params COLON type_expr Is - seq(local_decl) - block - With expr option(SEMI) { - let stop = - match $11 with - Some region -> region - | None -> expr_to_region $10 in - let region = cover $1 stop - and value = { - kwd_entrypoint = $1; - name = $2; - param = $3; - colon = $4; - ret_type = $5; - kwd_is = $6; - local_decls = $7; - block = $8; - kwd_with = $9; - return = $10; - terminator = $11} - in {region; value}} - -entry_params: - par(nsepseq(entry_param_decl,SEMI)) { $1 } - proc_decl: Procedure fun_name parameters Is seq(local_decl) @@ -331,22 +303,6 @@ param_decl: param_type = $4} in ParamConst {region; value}} -entry_param_decl: - param_decl { - match $1 with - ParamConst const -> EntryConst const - | ParamVar var -> EntryVar var - } -| Storage var COLON param_type { - let stop = type_expr_to_region $4 in - let region = cover $1 stop - and value = { - kwd_storage = $1; - var = $2; - colon = $3; - storage_type = $4} - in EntryStore {region; value}} - param_type: cartesian { TProd $1 } diff --git a/src/parser/pascaligo/ParserLog.ml b/src/parser/pascaligo/ParserLog.ml index 46341e800..c6feea777 100644 --- a/src/parser/pascaligo/ParserLog.ml +++ b/src/parser/pascaligo/ParserLog.ml @@ -144,7 +144,6 @@ and print_type_tuple {value; _} = and print_lambda_decl = function FunDecl fun_decl -> print_fun_decl fun_decl | ProcDecl proc_decl -> print_proc_decl proc_decl -| EntryDecl entry_decl -> print_entry_decl entry_decl and print_fun_decl {value; _} = let {kwd_function; name; param; colon; @@ -173,40 +172,6 @@ and print_proc_decl {value; _} = print_block block; print_terminator terminator -and print_entry_decl {value; _} = - let {kwd_entrypoint; name; param; colon; - ret_type; kwd_is; local_decls; - block; kwd_with; return; terminator} = value in - print_token kwd_entrypoint "entrypoint"; - print_var name; - print_entry_params param; - print_token colon ":"; - print_type_expr ret_type; - print_token kwd_is "is"; - print_local_decls local_decls; - print_block block; - print_token kwd_with "with"; - print_expr return; - print_terminator terminator - -and print_entry_params {value; _} = - let {lpar; inside; rpar} = value in - print_token lpar "("; - print_nsepseq ";" print_entry_param_decl inside; - print_token rpar ")" - -and print_entry_param_decl = function - EntryConst param_const -> print_param_const param_const -| EntryVar param_var -> print_param_var param_var -| EntryStore param_store -> print_storage param_store - -and print_storage {value; _} = - let {kwd_storage; var; colon; storage_type} = value in - print_token kwd_storage "storage"; - print_var var; - print_token colon ":"; - print_type_expr storage_type - and print_parameters {value; _} = let {lpar; inside; rpar} = value in print_token lpar "("; diff --git a/src/parser/pascaligo/SParser.ml b/src/parser/pascaligo/SParser.ml index c76903659..faa9780ed 100644 --- a/src/parser/pascaligo/SParser.ml +++ b/src/parser/pascaligo/SParser.ml @@ -138,21 +138,12 @@ and field_decl = parser and lambda_decl = parser [< _=fun_decl >] -> () | [< _=proc_decl >] -> () -| [< _=entry_decl >] -> () and fun_decl = parser [< 'Function _; 'Ident _; _=parameters; 'COLON _; _=type_expr; 'Is _; _ = seq local_decl; _=block; 'With _; _=expr >] -> () -and entry_decl = parser - [< 'Entrypoint _; 'Ident _; _=entry_params; - 'COLON _; _ = type_expr; 'Is _; _ = seq local_decl; - _=block; 'With _; _=expr >] -> () - -and entry_params = parser - [< p = par (nsepseq entry_param_decl semi) >] -> p - and proc_decl = parser [< 'Procedure _; 'Ident _; _parameters; 'Is _; _ = seq local_decl; _=block >] -> () @@ -164,10 +155,6 @@ and param_decl = parser [< 'Var _; 'Ident _; 'COLON _; _=param_type >] -> () | [< 'Const _; 'Ident _; 'COLON _; _=param_type >] -> () -and entry_param_decl = parser - [< _ = param_decl >] -> () -| [< 'Storage _; 'Ident _; 'COLON _; _=param_type >] -> () - and param_type = parser [< c = cartesian >] -> c and block = parser diff --git a/src/parser/pascaligo/Tests/crowdfunding.ligo b/src/parser/pascaligo/Tests/crowdfunding.ligo index 662fe4cc0..5d649d2ca 100644 --- a/src/parser/pascaligo/Tests/crowdfunding.ligo +++ b/src/parser/pascaligo/Tests/crowdfunding.ligo @@ -1,74 +1,55 @@ -const cmp_check : bool = 0 < 1 - -(* -const cmp_check : bool = ("1970-01-01T00:00:00Z" : timestamp) < ("1970-01-01T00:01:00Z" : timestamp)) -*) - -const x : int = (3 : int) - - - type store is record [ - goal : nat; + goal : mutez; deadline : timestamp; backers : map (address, nat); funded : bool; ] -entrypoint contribute (storage store : store; - const sender : address; - const amount : mutez) - : store * list (operation) is - var operations : list (operation) := nil - // const s : list (int) = list [1; 2; 3] - // const t : set (int) = set [] +function back (var store : store) : list (operation) * store is + var operations : list (operation) := list [] begin - if now (Unit) > store.deadline then + if now > store.deadline then fail "Deadline passed"; else case store.backers[sender] of [ - None -> store.backers[sender] := Some (amount) -// None -> patch store.backers with map sender -> amount end + None -> store.backers[sender] := amount + // or: None -> patch store.backers with map sender -> amount end | _ -> skip ] - end with (store, operations) + end with (operations, store) -entrypoint withdraw (storage store : store; const sender : address) - : store * list (operation) is - var operations : list (operation) := list end - begin -// if set ["a"; "b"] contains x then skip else skip; - if sender = owner then - if now (Unit) >= store.deadline then - if balance >= store.goal then { - store.funded := True; -// patch store with record funded = True end; - operations := list [Transfer (owner, balance)]; - }; - else fail "Below target" - else block { fail "Too soon"; } - else skip - end with (store, operations) - -entrypoint claim (storage store : store; const sender : address) - : store * list (operation) is - var operations : list (operation) := list [] - var amount : mutez := 0 +function claim (var store : store) : list (operation) * store is + var operations : list (operation) := nil begin if now <= store.deadline then - fail "Too soon" + fail "Too soon." else case store.backers[sender] of None -> - fail "Not a backer" + fail "Not a backer." | Some (amount) -> if balance >= store.goal or store.funded then - fail "Cannot refund" + fail "Goal reached: no refund." else begin - operations := list [Transfer (sender, amount)]; + operations := list [transaction (unit, sender, amount)]; remove sender from map store.backers end end - end with (store, operations) + end with (operations, store) + +function withdraw (var store : store) : list (operation) * store is + var operations : list (operation) := list end + begin + if sender = owner then + if now >= store.deadline then + if balance >= store.goal then { + store.funded := True; + // or: patch store with record funded = True end; + operations := list [Transfer (owner, balance)]; + }; + else fail "Below target." + else fail "Too soon."; + else skip + end with (operations, store) diff --git a/src/parser/shared/Lexer.mli b/src/parser/shared/Lexer.mli index 639894aa5..029275ac1 100644 --- a/src/parser/shared/Lexer.mli +++ b/src/parser/shared/Lexer.mli @@ -28,11 +28,11 @@ source regions, so useful error messages can be printed, therefore they are part of the signature [TOKEN] that parameterises the functor generated here. For instance, if, in a future release of - LIGO, new tokens may be added, and the recognition of their lexemes - may entail new errors, the signature [TOKEN] will have to be - augmented and the lexer specification changed. However, in - practice, it is more likely that instructions or types are added, - instead of new kinds of tokens. + LIGO, new tokens are added, and the recognition of their lexemes + entails new errors, the signature [TOKEN] will have to be augmented + and this lexer specification changed. However, in practice, it is + more likely that instructions or types will be added, instead of + new kinds of tokens. *) module Region = Simple_utils.Region diff --git a/src/parser/shared/Lexer.mll b/src/parser/shared/Lexer.mll index c0e5283c1..6a6f156ef 100644 --- a/src/parser/shared/Lexer.mll +++ b/src/parser/shared/Lexer.mll @@ -461,7 +461,6 @@ let nl = ['\n' '\r'] | "\r\n" let blank = ' ' | '\t' let digit = ['0'-'9'] let natural = digit | digit (digit | '_')* digit -let integer = '-'? natural let small = ['a'-'z'] let capital = ['A'-'Z'] let letter = small | capital @@ -503,7 +502,7 @@ and scan state = parse | bytes { (mk_bytes seq) state lexbuf |> enqueue } | natural 'n' { mk_nat state lexbuf |> enqueue } | natural "mtz" { mk_mtz state lexbuf |> enqueue } -| integer { mk_int state lexbuf |> enqueue } +| natural { mk_int state lexbuf |> enqueue } | symbol { mk_sym state lexbuf |> enqueue } | eof { mk_eof state lexbuf |> enqueue } @@ -546,7 +545,7 @@ and scan state = parse processed). *) -| '#' blank* ("line" blank+)? (integer as line) blank+ +| '#' blank* ("line" blank+)? (natural as line) blank+ '"' (string as file) '"' { let _, _, state = sync state lexbuf in let flags, state = scan_flags state [] lexbuf in @@ -562,7 +561,7 @@ and scan state = parse Some special errors are recognised in the semantic actions of the following regular expressions. The first error is a minus sign - separated from the integer it modifies by some markup (space or + separated from the integer it applies by some markup (space or tabs). The second is a minus sign immediately followed by anything else than a natural number (matched above) or markup and a number (previous error). The third is the strange occurrence of @@ -581,7 +580,7 @@ and scan state = parse fail region Orphan_minus | _ -> fail region Unterminated_integer } -| '-' "0x" byte_seq? +| "-0x" byte_seq? { let region, _, _ = sync state lexbuf in fail region Negative_byte_sequence } @@ -593,7 +592,7 @@ and scan state = parse and scan_flags state acc = parse blank+ { let _, _, state = sync state lexbuf in scan_flags state acc lexbuf } -| integer as code { let _, _, state = sync state lexbuf in +| natural as code { let _, _, state = sync state lexbuf in let acc = int_of_string code :: acc in scan_flags state acc lexbuf } | nl { List.rev acc, push_newline state lexbuf } @@ -699,7 +698,7 @@ and scan_utf8 thread state = parse report special error patterns), we need to keep a hidden reference to a queue of recognised lexical units (that is, tokens and markup) that acts as a mutable state between the calls to - [read_token]. When [read_token] is called, that queue is consulted + [read_token]. When [read_token] is called, that queue is examined first and, if it contains at least one token, that token is returned; otherwise, the lexing buffer is scanned for at least one more new token. That is the general principle: we put a high-level @@ -794,19 +793,18 @@ let open_token_stream file_path_opt = Some ([], next) -> let pos = (Token.to_region token)#stop in let region = Region.make ~start:pos ~stop:pos in - if is_bytes token && is_int next then + if is_int next then fail region Odd_lengthed_bytes else - if is_ident next || is_string next - || is_bytes next || is_int next then + if is_ident next || is_string next || is_bytes next then fail region Missing_break | _ -> () else - if Token.is_ident token || Token.is_string token then + if is_ident token || is_string token then match next_token buffer with Some ([], next) -> - if Token.is_ident next || Token.is_string next - || Token.is_bytes next || Token.is_int next + if is_ident next || is_string next + || is_bytes next || is_int next then let pos = (Token.to_region token)#stop in let region = Region.make ~start:pos ~stop:pos diff --git a/src/simplify/pascaligo.ml b/src/simplify/pascaligo.ml index c7d803f1f..cb9bd46cb 100644 --- a/src/simplify/pascaligo.ml +++ b/src/simplify/pascaligo.ml @@ -100,28 +100,6 @@ module Errors = struct ] in error ~data title message - let unsupported_string_catenation expr = - let title () = "string expressions" in - let message () = - Format.asprintf "string concatenation is not supported yet" in - let expr_loc = Raw.expr_to_region expr in - let data = [ - ("expr_loc", - fun () -> Format.asprintf "%a" Location.pp_lift @@ expr_loc) - ] in - error ~data title message - - let unsupported_set_expr expr = - let title () = "set expressions" in - let message () = - Format.asprintf "the set type is not supported yet" in - let expr_loc = Raw.expr_to_region expr in - let data = [ - ("expr_loc", - fun () -> Format.asprintf "%a" Location.pp_lift @@ expr_loc) - ] in - error ~data title message - let unsupported_proc_calls call = let title () = "procedure calls" in let message () = From fa4a7cecdfdba722095249dee797e06165c3a28b Mon Sep 17 00:00:00 2001 From: Christian Rinderknecht Date: Fri, 27 Sep 2019 13:44:29 +0200 Subject: [PATCH 13/14] Removed entrypoint. Added back missing error message (string cat). --- src/passes/2-simplify/pascaligo.ml | 24 +++++++++++------------- 1 file changed, 11 insertions(+), 13 deletions(-) diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index 90d87ea0c..de0b82aa7 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -46,17 +46,6 @@ module Errors = struct ] in error ~data title message - let unsupported_entry_decl decl = - let title () = "entry point declarations" in - let message () = - Format.asprintf "entry points within the contract \ - are not supported yet" in - let data = [ - ("declaration", - fun () -> Format.asprintf "%a" Location.pp_lift @@ decl.Region.region) - ] in - error ~data title message - let unsupported_proc_decl decl = let title () = "procedure declarations" in let message () = @@ -110,6 +99,17 @@ module Errors = struct ] in error ~data title message + let unsupported_string_catenation expr = + let title () = "string expressions" in + let message () = + Format.asprintf "string concatenation is not supported yet" in + let expr_loc = Raw.expr_to_region expr in + let data = [ + ("expr_loc", + fun () -> Format.asprintf "%a" Location.pp_lift @@ expr_loc) + ] in + error ~data title message + let unsupported_proc_calls call = let title () = "procedure calls" in let message () = @@ -740,8 +740,6 @@ and simpl_declaration : Raw.declaration -> declaration Location.wrap result = ) | LambdaDecl (ProcDecl decl) -> fail @@ unsupported_proc_decl decl - | LambdaDecl (EntryDecl decl) -> - fail @@ unsupported_entry_decl decl and simpl_statement : Raw.statement -> (_ -> expression result) result = fun s -> From 889a4d643dc3f8c250ef8717932a833caf57562a Mon Sep 17 00:00:00 2001 From: Christian Rinderknecht Date: Fri, 27 Sep 2019 17:08:07 +0200 Subject: [PATCH 14/14] Forgot to fully resolved conflict due to removal of keyword `fail`. --- src/passes/1-parser/pascaligo/AST.ml | 4 ---- src/passes/1-parser/pascaligo/AST.mli | 4 ---- src/passes/1-parser/pascaligo/ParToken.mly | 4 ---- src/passes/1-parser/pascaligo/Tests/crowdfunding.ligo | 10 +++++----- 4 files changed, 5 insertions(+), 17 deletions(-) diff --git a/src/passes/1-parser/pascaligo/AST.ml b/src/passes/1-parser/pascaligo/AST.ml index a39c2bec7..214daaafe 100644 --- a/src/passes/1-parser/pascaligo/AST.ml +++ b/src/passes/1-parser/pascaligo/AST.ml @@ -49,10 +49,6 @@ type kwd_contains = Region.t type kwd_down = Region.t type kwd_else = Region.t type kwd_end = Region.t -<<<<<<< HEAD -======= -type kwd_fail = Region.t ->>>>>>> e5e9fb8e2faa1a67595553ab83279d3eb2b64470 type kwd_for = Region.t type kwd_from = Region.t type kwd_function = Region.t diff --git a/src/passes/1-parser/pascaligo/AST.mli b/src/passes/1-parser/pascaligo/AST.mli index f5a09536e..15e7e9883 100644 --- a/src/passes/1-parser/pascaligo/AST.mli +++ b/src/passes/1-parser/pascaligo/AST.mli @@ -33,10 +33,6 @@ type kwd_contains = Region.t type kwd_down = Region.t type kwd_else = Region.t type kwd_end = Region.t -<<<<<<< HEAD -======= -type kwd_fail = Region.t ->>>>>>> e5e9fb8e2faa1a67595553ab83279d3eb2b64470 type kwd_for = Region.t type kwd_from = Region.t type kwd_function = Region.t diff --git a/src/passes/1-parser/pascaligo/ParToken.mly b/src/passes/1-parser/pascaligo/ParToken.mly index 4f0a70cf3..e400947cb 100644 --- a/src/passes/1-parser/pascaligo/ParToken.mly +++ b/src/passes/1-parser/pascaligo/ParToken.mly @@ -53,10 +53,6 @@ %token Down (* "down" *) %token Else (* "else" *) %token End (* "end" *) -<<<<<<< HEAD -======= -%token Fail (* "fail" *) ->>>>>>> e5e9fb8e2faa1a67595553ab83279d3eb2b64470 %token For (* "for" *) %token Function (* "function" *) %token From (* "from" *) diff --git a/src/passes/1-parser/pascaligo/Tests/crowdfunding.ligo b/src/passes/1-parser/pascaligo/Tests/crowdfunding.ligo index 5d649d2ca..12e516534 100644 --- a/src/passes/1-parser/pascaligo/Tests/crowdfunding.ligo +++ b/src/passes/1-parser/pascaligo/Tests/crowdfunding.ligo @@ -10,7 +10,7 @@ function back (var store : store) : list (operation) * store is var operations : list (operation) := list [] begin if now > store.deadline then - fail "Deadline passed"; + failwith ("Deadline passed"); else case store.backers[sender] of [ None -> store.backers[sender] := amount @@ -23,14 +23,14 @@ function claim (var store : store) : list (operation) * store is var operations : list (operation) := nil begin if now <= store.deadline then - fail "Too soon." + failwith ("Too soon.") else case store.backers[sender] of None -> - fail "Not a backer." + failwith ("Not a backer.") | Some (amount) -> if balance >= store.goal or store.funded then - fail "Goal reached: no refund." + failwith ("Goal reached: no refund.") else begin operations := list [transaction (unit, sender, amount)]; @@ -49,7 +49,7 @@ function withdraw (var store : store) : list (operation) * store is // or: patch store with record funded = True end; operations := list [Transfer (owner, balance)]; }; - else fail "Below target." + else failwith ("Below target.") else fail "Too soon."; else skip end with (operations, store)