I added more transformations.
This commit is contained in:
parent
bf50102810
commit
50c99ff71d
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
348
src/parser/pascaligo/Doc/pascaligo_14.bnf
Normal file
348
src/parser/pascaligo/Doc/pascaligo_14.bnf
Normal file
@ -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
|
350
src/parser/pascaligo/Doc/pascaligo_15.bnf
Normal file
350
src/parser/pascaligo/Doc/pascaligo_15.bnf
Normal file
@ -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
|
353
src/parser/pascaligo/Doc/pascaligo_16.bnf
Normal file
353
src/parser/pascaligo/Doc/pascaligo_16.bnf
Normal file
@ -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
|
353
src/parser/pascaligo/Doc/pascaligo_17.bnf
Normal file
353
src/parser/pascaligo/Doc/pascaligo_17.bnf
Normal file
@ -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
|
356
src/parser/pascaligo/Doc/pascaligo_18.bnf
Normal file
356
src/parser/pascaligo/Doc/pascaligo_18.bnf
Normal file
@ -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
|
354
src/parser/pascaligo/Doc/pascaligo_19.bnf
Normal file
354
src/parser/pascaligo/Doc/pascaligo_19.bnf
Normal file
@ -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)
|
@ -703,7 +703,6 @@ interactive_expr:
|
||||
|
||||
expr:
|
||||
case(expr) { ECase ($1 expr_to_region) }
|
||||
(*| annot_expr { $1 }*)
|
||||
| disj_expr { $1 }
|
||||
|
||||
disj_expr:
|
||||
|
@ -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;
|
||||
@ -18,7 +28,7 @@ entrypoint contribute (storage store : store;
|
||||
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
|
||||
]
|
||||
|
Loading…
Reference in New Issue
Block a user