First rewrites of the PascaLIGO grammar to make it suitbale for stream
parsing.
This commit is contained in:
Christian Rinderknecht
parent
9b34b13e15
commit
100bf1119a
436
src/parser/pascaligo/Doc/pascaligo1.bnf
Normal file
436
src/parser/pascaligo/Doc/pascaligo1.bnf
Normal file
@ -0,0 +1,436 @@
|
|||||||
|
option(X) :=
|
||||||
|
(**)
|
||||||
|
| X
|
||||||
|
|
||||||
|
sep_or_term_list(item,sep) ::=
|
||||||
|
nsepseq(item,sep)
|
||||||
|
| nseq(item sep)
|
||||||
|
|
||||||
|
(* Compound constructs *)
|
||||||
|
|
||||||
|
par(X) ::= LPAR X RPAR
|
||||||
|
|
||||||
|
brackets(X) ::= LBRACKET X RBRACKET
|
||||||
|
|
||||||
|
(* Sequences *)
|
||||||
|
|
||||||
|
(* Possibly empty sequence of items *)
|
||||||
|
|
||||||
|
seq(X) ::=
|
||||||
|
(**)
|
||||||
|
| X seq(X)
|
||||||
|
|
||||||
|
(* Non-empty sequence of items *)
|
||||||
|
|
||||||
|
nseq(X) ::= X seq(X)
|
||||||
|
|
||||||
|
(* Non-empty separated sequence of items *)
|
||||||
|
|
||||||
|
nsepseq(X,Sep) ::=
|
||||||
|
X
|
||||||
|
| X Sep nsepseq(X,Sep)
|
||||||
|
|
||||||
|
(* Possibly empy separated sequence of items *)
|
||||||
|
|
||||||
|
sepseq(X,Sep) ::=
|
||||||
|
(**)
|
||||||
|
| nsepseq(X,Sep)
|
||||||
|
|
||||||
|
|
||||||
|
(* Inlines *)
|
||||||
|
|
||||||
|
var ::= Ident
|
||||||
|
type_name ::= Ident
|
||||||
|
fun_name ::= Ident
|
||||||
|
field_name ::= Ident
|
||||||
|
struct_name ::= Ident
|
||||||
|
|
||||||
|
(* Main *)
|
||||||
|
|
||||||
|
contract ::=
|
||||||
|
nseq(declaration) EOF
|
||||||
|
|
||||||
|
declaration ::=
|
||||||
|
type_decl
|
||||||
|
| const_decl
|
||||||
|
| lambda_decl
|
||||||
|
|
||||||
|
(* Type declarations *)
|
||||||
|
|
||||||
|
type_decl ::=
|
||||||
|
Type type_name Is type_expr option(SEMI)
|
||||||
|
|
||||||
|
type_expr ::=
|
||||||
|
cartesian
|
||||||
|
| sum_type
|
||||||
|
| record_type
|
||||||
|
|
||||||
|
cartesian ::=
|
||||||
|
nsepseq(function_type,TIMES)
|
||||||
|
|
||||||
|
function_type ::=
|
||||||
|
core_type
|
||||||
|
| core_type ARROW function_type
|
||||||
|
|
||||||
|
core_type ::=
|
||||||
|
type_name
|
||||||
|
| type_name type_tuple
|
||||||
|
| Map type_tuple
|
||||||
|
| Set par(type_expr)
|
||||||
|
| List par(type_expr)
|
||||||
|
| par(type_expr)
|
||||||
|
|
||||||
|
type_tuple ::=
|
||||||
|
par(nsepseq(type_expr,COMMA))
|
||||||
|
|
||||||
|
sum_type ::=
|
||||||
|
option(VBAR) nsepseq(variant,VBAR)
|
||||||
|
|
||||||
|
variant ::=
|
||||||
|
Constr Of cartesian
|
||||||
|
| Constr
|
||||||
|
|
||||||
|
record_type ::=
|
||||||
|
Record sep_or_term_list(field_decl,SEMI) End
|
||||||
|
| Record LBRACKET sep_or_term_list(field_decl,SEMI) RBRACKET
|
||||||
|
|
||||||
|
field_decl ::=
|
||||||
|
field_name COLON type_expr
|
||||||
|
|
||||||
|
(* Function and procedure declarations *)
|
||||||
|
|
||||||
|
lambda_decl ::=
|
||||||
|
fun_decl
|
||||||
|
| proc_decl
|
||||||
|
| entry_decl
|
||||||
|
|
||||||
|
fun_decl ::=
|
||||||
|
Function fun_name parameters COLON type_expr Is
|
||||||
|
seq(local_decl)
|
||||||
|
block
|
||||||
|
With expr option(SEMI)
|
||||||
|
|
||||||
|
entry_decl ::=
|
||||||
|
Entrypoint fun_name entry_params COLON type_expr Is
|
||||||
|
seq(local_decl)
|
||||||
|
block
|
||||||
|
With expr option(SEMI)
|
||||||
|
|
||||||
|
entry_params ::=
|
||||||
|
par(nsepseq(entry_param_decl,SEMI))
|
||||||
|
|
||||||
|
proc_decl ::=
|
||||||
|
Procedure fun_name parameters Is
|
||||||
|
seq(local_decl)
|
||||||
|
block option(SEMI)
|
||||||
|
|
||||||
|
parameters ::=
|
||||||
|
par(nsepseq(param_decl,SEMI))
|
||||||
|
|
||||||
|
param_decl ::=
|
||||||
|
Var var COLON param_type
|
||||||
|
| Const var COLON param_type
|
||||||
|
|
||||||
|
entry_param_decl ::=
|
||||||
|
param_decl
|
||||||
|
| Storage var COLON param_type
|
||||||
|
|
||||||
|
param_type ::=
|
||||||
|
cartesian
|
||||||
|
|
||||||
|
block ::=
|
||||||
|
Begin sep_or_term_list(statement,SEMI) End
|
||||||
|
| Block LBRACE sep_or_term_list(statement,SEMI) RBRACE
|
||||||
|
|
||||||
|
statement ::=
|
||||||
|
instruction
|
||||||
|
| open_data_decl
|
||||||
|
|
||||||
|
open_data_decl ::=
|
||||||
|
open_const_decl
|
||||||
|
| open_var_decl
|
||||||
|
|
||||||
|
open_const_decl ::=
|
||||||
|
Const unqualified_decl(EQUAL)
|
||||||
|
|
||||||
|
open_var_decl ::=
|
||||||
|
Var unqualified_decl(ASS)
|
||||||
|
|
||||||
|
local_decl ::=
|
||||||
|
fun_decl
|
||||||
|
| proc_decl
|
||||||
|
| data_decl
|
||||||
|
|
||||||
|
data_decl ::=
|
||||||
|
const_decl
|
||||||
|
| var_decl
|
||||||
|
|
||||||
|
unqualified_decl(OP) ::=
|
||||||
|
var COLON type_expr OP extended_expr
|
||||||
|
|
||||||
|
const_decl ::=
|
||||||
|
open_const_decl SEMI
|
||||||
|
| open_const_decl
|
||||||
|
|
||||||
|
var_decl ::=
|
||||||
|
open_var_decl SEMI
|
||||||
|
| open_var_decl
|
||||||
|
|
||||||
|
extended_expr ::=
|
||||||
|
expr
|
||||||
|
|
||||||
|
instruction ::=
|
||||||
|
single_instr
|
||||||
|
| block
|
||||||
|
|
||||||
|
single_instr ::=
|
||||||
|
conditional
|
||||||
|
| case_instr
|
||||||
|
| assignment
|
||||||
|
| loop
|
||||||
|
| proc_call
|
||||||
|
| fail_instr
|
||||||
|
| Skip
|
||||||
|
| record_patch
|
||||||
|
| map_patch
|
||||||
|
| set_patch
|
||||||
|
| map_remove
|
||||||
|
| set_remove
|
||||||
|
|
||||||
|
set_remove ::=
|
||||||
|
Remove expr From Set path
|
||||||
|
|
||||||
|
map_remove ::=
|
||||||
|
Remove expr From Map path
|
||||||
|
|
||||||
|
set_patch ::=
|
||||||
|
Patch path With injection(Set,expr)
|
||||||
|
|
||||||
|
map_patch ::=
|
||||||
|
Patch path With injection(Map,binding)
|
||||||
|
|
||||||
|
injection(Kind,element) ::=
|
||||||
|
Kind sep_or_term_list(element,SEMI) End
|
||||||
|
| Kind End
|
||||||
|
| Kind LBRACKET sep_or_term_list(element,SEMI) RBRACKET
|
||||||
|
| Kind LBRACKET RBRACKET
|
||||||
|
|
||||||
|
binding ::=
|
||||||
|
expr ARROW expr
|
||||||
|
|
||||||
|
record_patch ::=
|
||||||
|
Patch path With record_expr
|
||||||
|
|
||||||
|
fail_instr ::=
|
||||||
|
Fail expr
|
||||||
|
|
||||||
|
proc_call ::=
|
||||||
|
fun_call
|
||||||
|
|
||||||
|
conditional ::=
|
||||||
|
If expr Then if_clause option(SEMI) Else if_clause
|
||||||
|
|
||||||
|
if_clause ::=
|
||||||
|
instruction
|
||||||
|
| LBRACE sep_or_term_list(statement,COMMA) RBRACE
|
||||||
|
|
||||||
|
case_instr ::=
|
||||||
|
case(instruction)
|
||||||
|
|
||||||
|
case(rhs) ::=
|
||||||
|
Case expr Of option(VBAR) cases(rhs) End
|
||||||
|
| Case expr Of LBRACKET option(VBAR) cases(rhs) RBRACKET
|
||||||
|
|
||||||
|
cases(rhs) ::=
|
||||||
|
nsepseq(case_clause(rhs),VBAR)
|
||||||
|
|
||||||
|
case_clause(rhs) ::=
|
||||||
|
pattern ARROW rhs
|
||||||
|
|
||||||
|
assignment ::=
|
||||||
|
lhs ASS rhs
|
||||||
|
|
||||||
|
rhs ::=
|
||||||
|
expr
|
||||||
|
|
||||||
|
lhs ::=
|
||||||
|
path
|
||||||
|
| map_lookup
|
||||||
|
|
||||||
|
loop ::=
|
||||||
|
while_loop
|
||||||
|
| for_loop
|
||||||
|
|
||||||
|
while_loop ::=
|
||||||
|
While expr block
|
||||||
|
|
||||||
|
for_loop ::=
|
||||||
|
For var_assign option(Down) To expr option(step_clause) block
|
||||||
|
| For var option(arrow_clause) In expr block
|
||||||
|
|
||||||
|
var_assign ::=
|
||||||
|
var ASS expr
|
||||||
|
|
||||||
|
step_clause ::=
|
||||||
|
Step expr
|
||||||
|
|
||||||
|
arrow_clause ::=
|
||||||
|
ARROW var
|
||||||
|
|
||||||
|
(* Expressions *)
|
||||||
|
|
||||||
|
interactive_expr ::=
|
||||||
|
expr EOF
|
||||||
|
|
||||||
|
expr ::=
|
||||||
|
case(expr)
|
||||||
|
| annot_expr
|
||||||
|
|
||||||
|
annot_expr ::=
|
||||||
|
LPAR disj_expr COLON type_expr RPAR
|
||||||
|
| disj_expr
|
||||||
|
|
||||||
|
disj_expr ::=
|
||||||
|
disj_expr Or conj_expr
|
||||||
|
| conj_expr
|
||||||
|
|
||||||
|
conj_expr ::=
|
||||||
|
conj_expr And set_membership
|
||||||
|
| set_membership
|
||||||
|
|
||||||
|
set_membership ::=
|
||||||
|
core_expr Contains set_membership
|
||||||
|
| comp_expr
|
||||||
|
|
||||||
|
comp_expr ::=
|
||||||
|
comp_expr LT cat_expr
|
||||||
|
| comp_expr LEQ cat_expr
|
||||||
|
| comp_expr GT cat_expr
|
||||||
|
| comp_expr GEQ cat_expr
|
||||||
|
| comp_expr EQUAL cat_expr
|
||||||
|
| comp_expr NEQ cat_expr
|
||||||
|
| cat_expr
|
||||||
|
|
||||||
|
cat_expr ::=
|
||||||
|
cons_expr CAT cat_expr
|
||||||
|
| cons_expr
|
||||||
|
|
||||||
|
cons_expr ::=
|
||||||
|
add_expr CONS cons_expr
|
||||||
|
| add_expr
|
||||||
|
|
||||||
|
add_expr ::=
|
||||||
|
add_expr PLUS mult_expr
|
||||||
|
| add_expr MINUS mult_expr
|
||||||
|
| mult_expr
|
||||||
|
|
||||||
|
mult_expr ::=
|
||||||
|
mult_expr TIMES unary_expr
|
||||||
|
| mult_expr SLASH unary_expr
|
||||||
|
| mult_expr Mod unary_expr
|
||||||
|
| unary_expr
|
||||||
|
|
||||||
|
unary_expr ::=
|
||||||
|
MINUS core_expr
|
||||||
|
| Not core_expr
|
||||||
|
| core_expr
|
||||||
|
|
||||||
|
core_expr ::=
|
||||||
|
Int
|
||||||
|
| Nat
|
||||||
|
| Mtz
|
||||||
|
| var
|
||||||
|
| String
|
||||||
|
| Bytes
|
||||||
|
| C_False
|
||||||
|
| C_True
|
||||||
|
| C_Unit
|
||||||
|
| tuple_expr
|
||||||
|
| list_expr
|
||||||
|
| C_None
|
||||||
|
| fun_call
|
||||||
|
| map_expr
|
||||||
|
| set_expr
|
||||||
|
| record_expr
|
||||||
|
| projection
|
||||||
|
| Constr arguments
|
||||||
|
| Constr
|
||||||
|
| C_Some arguments
|
||||||
|
|
||||||
|
set_expr ::=
|
||||||
|
injection(Set,expr)
|
||||||
|
|
||||||
|
map_expr ::=
|
||||||
|
map_lookup
|
||||||
|
| injection(Map,binding)
|
||||||
|
|
||||||
|
map_lookup ::=
|
||||||
|
path brackets(expr)
|
||||||
|
|
||||||
|
path ::=
|
||||||
|
var
|
||||||
|
| projection
|
||||||
|
|
||||||
|
projection ::=
|
||||||
|
struct_name DOT nsepseq(selection,DOT)
|
||||||
|
|
||||||
|
selection ::=
|
||||||
|
field_name
|
||||||
|
| Int
|
||||||
|
|
||||||
|
record_expr ::=
|
||||||
|
Record sep_or_term_list(field_assignment,SEMI) End
|
||||||
|
| Record LBRACKET sep_or_term_list(field_assignment,SEMI) RBRACKET
|
||||||
|
|
||||||
|
field_assignment ::=
|
||||||
|
field_name EQUAL expr
|
||||||
|
|
||||||
|
fun_call ::=
|
||||||
|
fun_name arguments
|
||||||
|
|
||||||
|
tuple_expr ::=
|
||||||
|
tuple_inj
|
||||||
|
|
||||||
|
tuple_inj ::=
|
||||||
|
par(nsepseq(expr,COMMA))
|
||||||
|
|
||||||
|
arguments ::=
|
||||||
|
tuple_inj
|
||||||
|
|
||||||
|
list_expr ::=
|
||||||
|
injection(List,expr)
|
||||||
|
| Nil
|
||||||
|
|
||||||
|
(* Patterns *)
|
||||||
|
|
||||||
|
pattern ::=
|
||||||
|
nsepseq(core_pattern,CONS)
|
||||||
|
|
||||||
|
core_pattern ::=
|
||||||
|
var
|
||||||
|
| WILD
|
||||||
|
| Int
|
||||||
|
| String
|
||||||
|
| C_Unit
|
||||||
|
| C_False
|
||||||
|
| C_True
|
||||||
|
| C_None
|
||||||
|
| list_pattern
|
||||||
|
| tuple_pattern
|
||||||
|
| constr_pattern
|
||||||
|
| C_Some par(core_pattern)
|
||||||
|
|
||||||
|
list_pattern ::=
|
||||||
|
injection(List,core_pattern)
|
||||||
|
| Nil
|
||||||
|
| par(cons_pattern)
|
||||||
|
|
||||||
|
cons_pattern ::=
|
||||||
|
core_pattern CONS pattern
|
||||||
|
|
||||||
|
tuple_pattern ::=
|
||||||
|
par(nsepseq(core_pattern,COMMA))
|
||||||
|
|
||||||
|
constr_pattern ::=
|
||||||
|
Constr tuple_pattern
|
||||||
|
| Constr
|
||||||
442
src/parser/pascaligo/Doc/pascaligo2.bnf
Normal file
442
src/parser/pascaligo/Doc/pascaligo2.bnf
Normal file
@ -0,0 +1,442 @@
|
|||||||
|
option(X) :=
|
||||||
|
(**)
|
||||||
|
| X
|
||||||
|
|
||||||
|
series(item,sep,term) ::=
|
||||||
|
item after_item(item,sep,term)
|
||||||
|
|
||||||
|
after_item(item,sep,term) ::=
|
||||||
|
sep item_or_closing(item,sep,term)
|
||||||
|
| term
|
||||||
|
|
||||||
|
item_or_closing(item,sep,term) ::=
|
||||||
|
term
|
||||||
|
| series(item,sep,term)
|
||||||
|
|
||||||
|
(* Compound constructs *)
|
||||||
|
|
||||||
|
par(X) ::= LPAR X RPAR
|
||||||
|
|
||||||
|
brackets(X) ::= LBRACKET X RBRACKET
|
||||||
|
|
||||||
|
(* Sequences *)
|
||||||
|
|
||||||
|
(* Possibly empty sequence of items *)
|
||||||
|
|
||||||
|
seq(X) ::=
|
||||||
|
(**)
|
||||||
|
| X seq(X)
|
||||||
|
|
||||||
|
(* Non-empty sequence of items *)
|
||||||
|
|
||||||
|
nseq(X) ::= X seq(X)
|
||||||
|
|
||||||
|
(* Non-empty separated sequence of items *)
|
||||||
|
|
||||||
|
nsepseq(X,Sep) ::=
|
||||||
|
X
|
||||||
|
| X Sep nsepseq(X,Sep)
|
||||||
|
|
||||||
|
(* Possibly empy separated sequence of items *)
|
||||||
|
|
||||||
|
sepseq(X,Sep) ::=
|
||||||
|
(**)
|
||||||
|
| nsepseq(X,Sep)
|
||||||
|
|
||||||
|
|
||||||
|
(* Inlines *)
|
||||||
|
|
||||||
|
var ::= Ident
|
||||||
|
type_name ::= Ident
|
||||||
|
fun_name ::= Ident
|
||||||
|
field_name ::= Ident
|
||||||
|
struct_name ::= Ident
|
||||||
|
|
||||||
|
(* Main *)
|
||||||
|
|
||||||
|
contract ::=
|
||||||
|
nseq(declaration) EOF
|
||||||
|
|
||||||
|
declaration ::=
|
||||||
|
type_decl
|
||||||
|
| const_decl
|
||||||
|
| lambda_decl
|
||||||
|
|
||||||
|
(* Type declarations *)
|
||||||
|
|
||||||
|
type_decl ::=
|
||||||
|
Type type_name Is type_expr option(SEMI)
|
||||||
|
|
||||||
|
type_expr ::=
|
||||||
|
cartesian
|
||||||
|
| sum_type
|
||||||
|
| record_type
|
||||||
|
|
||||||
|
cartesian ::=
|
||||||
|
nsepseq(function_type,TIMES)
|
||||||
|
|
||||||
|
function_type ::=
|
||||||
|
core_type
|
||||||
|
| core_type ARROW function_type
|
||||||
|
|
||||||
|
core_type ::=
|
||||||
|
type_name
|
||||||
|
| type_name type_tuple
|
||||||
|
| Map type_tuple
|
||||||
|
| Set par(type_expr)
|
||||||
|
| List par(type_expr)
|
||||||
|
| par(type_expr)
|
||||||
|
|
||||||
|
type_tuple ::=
|
||||||
|
par(nsepseq(type_expr,COMMA))
|
||||||
|
|
||||||
|
sum_type ::=
|
||||||
|
option(VBAR) nsepseq(variant,VBAR)
|
||||||
|
|
||||||
|
variant ::=
|
||||||
|
Constr Of cartesian
|
||||||
|
| Constr
|
||||||
|
|
||||||
|
record_type ::=
|
||||||
|
Record series(field_decl,SEMI,End)
|
||||||
|
| Record LBRACKET series(field_decl,SEMI,RBRACKET)
|
||||||
|
|
||||||
|
field_decl ::=
|
||||||
|
field_name COLON type_expr
|
||||||
|
|
||||||
|
(* Function and procedure declarations *)
|
||||||
|
|
||||||
|
lambda_decl ::=
|
||||||
|
fun_decl
|
||||||
|
| proc_decl
|
||||||
|
| entry_decl
|
||||||
|
|
||||||
|
fun_decl ::=
|
||||||
|
Function fun_name parameters COLON type_expr Is
|
||||||
|
seq(local_decl)
|
||||||
|
block
|
||||||
|
With expr option(SEMI)
|
||||||
|
|
||||||
|
entry_decl ::=
|
||||||
|
Entrypoint fun_name entry_params COLON type_expr Is
|
||||||
|
seq(local_decl)
|
||||||
|
block
|
||||||
|
With expr option(SEMI)
|
||||||
|
|
||||||
|
entry_params ::=
|
||||||
|
par(nsepseq(entry_param_decl,SEMI))
|
||||||
|
|
||||||
|
proc_decl ::=
|
||||||
|
Procedure fun_name parameters Is
|
||||||
|
seq(local_decl)
|
||||||
|
block option(SEMI)
|
||||||
|
|
||||||
|
parameters ::=
|
||||||
|
par(nsepseq(param_decl,SEMI))
|
||||||
|
|
||||||
|
param_decl ::=
|
||||||
|
Var var COLON param_type
|
||||||
|
| Const var COLON param_type
|
||||||
|
|
||||||
|
entry_param_decl ::=
|
||||||
|
param_decl
|
||||||
|
| Storage var COLON param_type
|
||||||
|
|
||||||
|
param_type ::=
|
||||||
|
cartesian
|
||||||
|
|
||||||
|
block ::=
|
||||||
|
Begin series(statement,SEMI,End)
|
||||||
|
| Block LBRACE series(statement,SEMI,RBRACE)
|
||||||
|
|
||||||
|
statement ::=
|
||||||
|
instruction
|
||||||
|
| open_data_decl
|
||||||
|
|
||||||
|
open_data_decl ::=
|
||||||
|
open_const_decl
|
||||||
|
| open_var_decl
|
||||||
|
|
||||||
|
open_const_decl ::=
|
||||||
|
Const unqualified_decl(EQUAL)
|
||||||
|
|
||||||
|
open_var_decl ::=
|
||||||
|
Var unqualified_decl(ASS)
|
||||||
|
|
||||||
|
local_decl ::=
|
||||||
|
fun_decl
|
||||||
|
| proc_decl
|
||||||
|
| data_decl
|
||||||
|
|
||||||
|
data_decl ::=
|
||||||
|
const_decl
|
||||||
|
| var_decl
|
||||||
|
|
||||||
|
unqualified_decl(OP) ::=
|
||||||
|
var COLON type_expr OP extended_expr
|
||||||
|
|
||||||
|
const_decl ::=
|
||||||
|
open_const_decl SEMI
|
||||||
|
| open_const_decl
|
||||||
|
|
||||||
|
var_decl ::=
|
||||||
|
open_var_decl option(SEMI)
|
||||||
|
|
||||||
|
extended_expr ::=
|
||||||
|
expr
|
||||||
|
|
||||||
|
instruction ::=
|
||||||
|
single_instr
|
||||||
|
| block
|
||||||
|
|
||||||
|
single_instr ::=
|
||||||
|
conditional
|
||||||
|
| case_instr
|
||||||
|
| assignment
|
||||||
|
| loop
|
||||||
|
| proc_call
|
||||||
|
| fail_instr
|
||||||
|
| Skip
|
||||||
|
| record_patch
|
||||||
|
| map_patch
|
||||||
|
| set_patch
|
||||||
|
| map_remove
|
||||||
|
| set_remove
|
||||||
|
|
||||||
|
set_remove ::=
|
||||||
|
Remove expr From Set path
|
||||||
|
|
||||||
|
map_remove ::=
|
||||||
|
Remove expr From Map path
|
||||||
|
|
||||||
|
set_patch ::=
|
||||||
|
Patch path With injection(Set,expr)
|
||||||
|
|
||||||
|
map_patch ::=
|
||||||
|
Patch path With injection(Map,binding)
|
||||||
|
|
||||||
|
injection(Kind,element) ::=
|
||||||
|
Kind series(element,SEMI,End)
|
||||||
|
| Kind End
|
||||||
|
| Kind LBRACKET series(element,SEMI,RBRACKET)
|
||||||
|
| Kind LBRACKET RBRACKET
|
||||||
|
|
||||||
|
binding ::=
|
||||||
|
expr ARROW expr
|
||||||
|
|
||||||
|
record_patch ::=
|
||||||
|
Patch path With record_expr
|
||||||
|
|
||||||
|
fail_instr ::=
|
||||||
|
Fail expr
|
||||||
|
|
||||||
|
proc_call ::=
|
||||||
|
fun_call
|
||||||
|
|
||||||
|
conditional ::=
|
||||||
|
If expr Then if_clause option(SEMI) Else if_clause
|
||||||
|
|
||||||
|
if_clause ::=
|
||||||
|
instruction
|
||||||
|
| LBRACE series(statement,COMMA,RBRACE)
|
||||||
|
|
||||||
|
case_instr ::=
|
||||||
|
case(instruction)
|
||||||
|
|
||||||
|
case(rhs) ::=
|
||||||
|
Case expr Of option(VBAR) cases(rhs) End
|
||||||
|
| Case expr Of LBRACKET option(VBAR) cases(rhs) RBRACKET
|
||||||
|
|
||||||
|
cases(rhs) ::=
|
||||||
|
nsepseq(case_clause(rhs),VBAR)
|
||||||
|
|
||||||
|
case_clause(rhs) ::=
|
||||||
|
pattern ARROW rhs
|
||||||
|
|
||||||
|
assignment ::=
|
||||||
|
lhs ASS rhs
|
||||||
|
|
||||||
|
rhs ::=
|
||||||
|
expr
|
||||||
|
|
||||||
|
lhs ::=
|
||||||
|
path
|
||||||
|
| map_lookup
|
||||||
|
|
||||||
|
loop ::=
|
||||||
|
while_loop
|
||||||
|
| for_loop
|
||||||
|
|
||||||
|
while_loop ::=
|
||||||
|
While expr block
|
||||||
|
|
||||||
|
for_loop ::=
|
||||||
|
For var_assign option(Down) To expr option(step_clause) block
|
||||||
|
| For var option(arrow_clause) In expr block
|
||||||
|
|
||||||
|
var_assign ::=
|
||||||
|
var ASS expr
|
||||||
|
|
||||||
|
step_clause ::=
|
||||||
|
Step expr
|
||||||
|
|
||||||
|
arrow_clause ::=
|
||||||
|
ARROW var
|
||||||
|
|
||||||
|
(* Expressions *)
|
||||||
|
|
||||||
|
interactive_expr ::=
|
||||||
|
expr EOF
|
||||||
|
|
||||||
|
expr ::=
|
||||||
|
case(expr)
|
||||||
|
| annot_expr
|
||||||
|
|
||||||
|
annot_expr ::=
|
||||||
|
LPAR disj_expr COLON type_expr RPAR
|
||||||
|
| disj_expr
|
||||||
|
|
||||||
|
disj_expr ::=
|
||||||
|
disj_expr Or conj_expr
|
||||||
|
| conj_expr
|
||||||
|
|
||||||
|
conj_expr ::=
|
||||||
|
conj_expr And set_membership
|
||||||
|
| set_membership
|
||||||
|
|
||||||
|
set_membership ::=
|
||||||
|
core_expr Contains set_membership
|
||||||
|
| comp_expr
|
||||||
|
|
||||||
|
comp_expr ::=
|
||||||
|
comp_expr LT cat_expr
|
||||||
|
| comp_expr LEQ cat_expr
|
||||||
|
| comp_expr GT cat_expr
|
||||||
|
| comp_expr GEQ cat_expr
|
||||||
|
| comp_expr EQUAL cat_expr
|
||||||
|
| comp_expr NEQ cat_expr
|
||||||
|
| cat_expr
|
||||||
|
|
||||||
|
cat_expr ::=
|
||||||
|
cons_expr CAT cat_expr
|
||||||
|
| cons_expr
|
||||||
|
|
||||||
|
cons_expr ::=
|
||||||
|
add_expr CONS cons_expr
|
||||||
|
| add_expr
|
||||||
|
|
||||||
|
add_expr ::=
|
||||||
|
add_expr PLUS mult_expr
|
||||||
|
| add_expr MINUS mult_expr
|
||||||
|
| mult_expr
|
||||||
|
|
||||||
|
mult_expr ::=
|
||||||
|
mult_expr TIMES unary_expr
|
||||||
|
| mult_expr SLASH unary_expr
|
||||||
|
| mult_expr Mod unary_expr
|
||||||
|
| unary_expr
|
||||||
|
|
||||||
|
unary_expr ::=
|
||||||
|
MINUS core_expr
|
||||||
|
| Not core_expr
|
||||||
|
| core_expr
|
||||||
|
|
||||||
|
core_expr ::=
|
||||||
|
Int
|
||||||
|
| Nat
|
||||||
|
| Mtz
|
||||||
|
| var
|
||||||
|
| String
|
||||||
|
| Bytes
|
||||||
|
| C_False
|
||||||
|
| C_True
|
||||||
|
| C_Unit
|
||||||
|
| tuple_expr
|
||||||
|
| list_expr
|
||||||
|
| C_None
|
||||||
|
| fun_call
|
||||||
|
| map_expr
|
||||||
|
| set_expr
|
||||||
|
| record_expr
|
||||||
|
| projection
|
||||||
|
| Constr arguments
|
||||||
|
| Constr
|
||||||
|
| C_Some arguments
|
||||||
|
|
||||||
|
set_expr ::=
|
||||||
|
injection(Set,expr)
|
||||||
|
|
||||||
|
map_expr ::=
|
||||||
|
map_lookup
|
||||||
|
| injection(Map,binding)
|
||||||
|
|
||||||
|
map_lookup ::=
|
||||||
|
path brackets(expr)
|
||||||
|
|
||||||
|
path ::=
|
||||||
|
var
|
||||||
|
| projection
|
||||||
|
|
||||||
|
projection ::=
|
||||||
|
struct_name DOT nsepseq(selection,DOT)
|
||||||
|
|
||||||
|
selection ::=
|
||||||
|
field_name
|
||||||
|
| Int
|
||||||
|
|
||||||
|
record_expr ::=
|
||||||
|
Record series(field_assignment,SEMI,End)
|
||||||
|
| Record LBRACKET series(field_assignment,SEMI,RBRACKET)
|
||||||
|
|
||||||
|
field_assignment ::=
|
||||||
|
field_name EQUAL expr
|
||||||
|
|
||||||
|
fun_call ::=
|
||||||
|
fun_name arguments
|
||||||
|
|
||||||
|
tuple_expr ::=
|
||||||
|
tuple_inj
|
||||||
|
|
||||||
|
tuple_inj ::=
|
||||||
|
par(nsepseq(expr,COMMA))
|
||||||
|
|
||||||
|
arguments ::=
|
||||||
|
tuple_inj
|
||||||
|
|
||||||
|
list_expr ::=
|
||||||
|
injection(List,expr)
|
||||||
|
| Nil
|
||||||
|
|
||||||
|
(* Patterns *)
|
||||||
|
|
||||||
|
pattern ::=
|
||||||
|
nsepseq(core_pattern,CONS)
|
||||||
|
|
||||||
|
core_pattern ::=
|
||||||
|
var
|
||||||
|
| WILD
|
||||||
|
| Int
|
||||||
|
| String
|
||||||
|
| C_Unit
|
||||||
|
| C_False
|
||||||
|
| C_True
|
||||||
|
| C_None
|
||||||
|
| list_pattern
|
||||||
|
| tuple_pattern
|
||||||
|
| constr_pattern
|
||||||
|
| C_Some par(core_pattern)
|
||||||
|
|
||||||
|
list_pattern ::=
|
||||||
|
injection(List,core_pattern)
|
||||||
|
| Nil
|
||||||
|
| par(cons_pattern)
|
||||||
|
|
||||||
|
cons_pattern ::=
|
||||||
|
core_pattern CONS pattern
|
||||||
|
|
||||||
|
tuple_pattern ::=
|
||||||
|
par(nsepseq(core_pattern,COMMA))
|
||||||
|
|
||||||
|
constr_pattern ::=
|
||||||
|
Constr tuple_pattern
|
||||||
|
| Constr
|
||||||
421
src/parser/pascaligo/Doc/pascaligo3.bnf
Normal file
421
src/parser/pascaligo/Doc/pascaligo3.bnf
Normal file
@ -0,0 +1,421 @@
|
|||||||
|
option(X) :=
|
||||||
|
(**)
|
||||||
|
| X
|
||||||
|
|
||||||
|
series(item,sep,term) ::=
|
||||||
|
item after_item(item,sep,term)
|
||||||
|
|
||||||
|
after_item(item,sep,term) ::=
|
||||||
|
sep item_or_closing(item,sep,term)
|
||||||
|
| term
|
||||||
|
|
||||||
|
item_or_closing(item,sep,term) ::=
|
||||||
|
term
|
||||||
|
| series(item,sep,term)
|
||||||
|
|
||||||
|
(* Compound constructs *)
|
||||||
|
|
||||||
|
par(X) ::= LPAR X RPAR
|
||||||
|
|
||||||
|
brackets(X) ::= LBRACKET X RBRACKET
|
||||||
|
|
||||||
|
(* Sequences *)
|
||||||
|
|
||||||
|
(* Possibly empty sequence of items *)
|
||||||
|
|
||||||
|
seq(X) ::=
|
||||||
|
(**)
|
||||||
|
| X seq(X)
|
||||||
|
|
||||||
|
(* Non-empty sequence of items *)
|
||||||
|
|
||||||
|
nseq(X) ::= X seq(X)
|
||||||
|
|
||||||
|
(* Non-empty separated sequence of items *)
|
||||||
|
|
||||||
|
nsepseq(X,Sep) ::=
|
||||||
|
X
|
||||||
|
| X Sep nsepseq(X,Sep)
|
||||||
|
|
||||||
|
(* Possibly empy separated sequence of items *)
|
||||||
|
|
||||||
|
sepseq(X,Sep) ::=
|
||||||
|
(**)
|
||||||
|
| nsepseq(X,Sep)
|
||||||
|
|
||||||
|
(* Main *)
|
||||||
|
|
||||||
|
contract ::=
|
||||||
|
nseq(declaration) EOF
|
||||||
|
|
||||||
|
declaration ::=
|
||||||
|
type_decl
|
||||||
|
| const_decl
|
||||||
|
| lambda_decl
|
||||||
|
|
||||||
|
(* Type declarations *)
|
||||||
|
|
||||||
|
type_decl ::=
|
||||||
|
Type Ident (* type_name *) Is type_expr option(SEMI)
|
||||||
|
|
||||||
|
type_expr ::=
|
||||||
|
cartesian
|
||||||
|
| sum_type
|
||||||
|
| record_type
|
||||||
|
|
||||||
|
cartesian ::=
|
||||||
|
nsepseq(function_type,TIMES)
|
||||||
|
|
||||||
|
function_type ::=
|
||||||
|
core_type
|
||||||
|
| core_type ARROW function_type
|
||||||
|
|
||||||
|
core_type ::=
|
||||||
|
Ident (* type_name *)
|
||||||
|
| Ident (* type_name *) type_tuple
|
||||||
|
| Map type_tuple
|
||||||
|
| Set par(type_expr)
|
||||||
|
| List par(type_expr)
|
||||||
|
| par(type_expr)
|
||||||
|
|
||||||
|
type_tuple ::=
|
||||||
|
par(nsepseq(type_expr,COMMA))
|
||||||
|
|
||||||
|
sum_type ::=
|
||||||
|
option(VBAR) nsepseq(variant,VBAR)
|
||||||
|
|
||||||
|
variant ::=
|
||||||
|
Constr Of cartesian
|
||||||
|
| Constr
|
||||||
|
|
||||||
|
record_type ::=
|
||||||
|
Record series(field_decl,SEMI,End)
|
||||||
|
| Record LBRACKET series(field_decl,SEMI,RBRACKET)
|
||||||
|
|
||||||
|
field_decl ::=
|
||||||
|
Ident (* field_name *) COLON type_expr
|
||||||
|
|
||||||
|
(* Function and procedure declarations *)
|
||||||
|
|
||||||
|
lambda_decl ::=
|
||||||
|
fun_decl
|
||||||
|
| proc_decl
|
||||||
|
| entry_decl
|
||||||
|
|
||||||
|
fun_decl ::=
|
||||||
|
Function Ident (* fun_name *) parameters COLON type_expr Is
|
||||||
|
seq(local_decl)
|
||||||
|
block
|
||||||
|
With expr option(SEMI)
|
||||||
|
|
||||||
|
entry_decl ::=
|
||||||
|
Entrypoint Ident (* fun_name *) entry_params COLON type_expr Is
|
||||||
|
seq(local_decl)
|
||||||
|
block
|
||||||
|
With expr option(SEMI)
|
||||||
|
|
||||||
|
entry_params ::=
|
||||||
|
par(nsepseq(entry_param_decl,SEMI))
|
||||||
|
|
||||||
|
proc_decl ::=
|
||||||
|
Procedure Ident (* fun_name *) parameters Is
|
||||||
|
seq(local_decl)
|
||||||
|
block option(SEMI)
|
||||||
|
|
||||||
|
parameters ::=
|
||||||
|
par(nsepseq(param_decl,SEMI))
|
||||||
|
|
||||||
|
param_decl ::=
|
||||||
|
Var Ident (* var *) COLON param_type
|
||||||
|
| Const Ident (* var *) COLON param_type
|
||||||
|
|
||||||
|
entry_param_decl ::=
|
||||||
|
param_decl
|
||||||
|
| Storage Ident (* var *) COLON param_type
|
||||||
|
|
||||||
|
param_type ::=
|
||||||
|
cartesian
|
||||||
|
|
||||||
|
block ::=
|
||||||
|
Begin series(statement,SEMI,End)
|
||||||
|
| Block LBRACE series(statement,SEMI,RBRACE)
|
||||||
|
|
||||||
|
statement ::=
|
||||||
|
instruction
|
||||||
|
| open_data_decl
|
||||||
|
|
||||||
|
open_data_decl ::=
|
||||||
|
open_const_decl
|
||||||
|
| open_var_decl
|
||||||
|
|
||||||
|
open_const_decl ::=
|
||||||
|
Const unqualified_decl(EQUAL)
|
||||||
|
|
||||||
|
open_var_decl ::=
|
||||||
|
Var unqualified_decl(ASS)
|
||||||
|
|
||||||
|
local_decl ::=
|
||||||
|
fun_decl
|
||||||
|
| proc_decl
|
||||||
|
| data_decl
|
||||||
|
|
||||||
|
data_decl ::=
|
||||||
|
const_decl
|
||||||
|
| var_decl
|
||||||
|
|
||||||
|
unqualified_decl(OP) ::=
|
||||||
|
Ident (* var *) COLON type_expr OP extended_expr
|
||||||
|
|
||||||
|
const_decl ::=
|
||||||
|
open_const_decl SEMI
|
||||||
|
| open_const_decl
|
||||||
|
|
||||||
|
var_decl ::=
|
||||||
|
open_var_decl option(SEMI)
|
||||||
|
|
||||||
|
extended_expr ::=
|
||||||
|
expr
|
||||||
|
|
||||||
|
instruction ::=
|
||||||
|
single_instr
|
||||||
|
| block
|
||||||
|
|
||||||
|
single_instr ::=
|
||||||
|
conditional
|
||||||
|
| case_instr
|
||||||
|
| assignment
|
||||||
|
| loop
|
||||||
|
| proc_call
|
||||||
|
| fail_instr
|
||||||
|
| Skip
|
||||||
|
| record_patch
|
||||||
|
| Patch path With injection(Map,binding)
|
||||||
|
| Patch path With injection(Set,expr)
|
||||||
|
| Remove expr From Map path
|
||||||
|
| Remove expr From Set path
|
||||||
|
|
||||||
|
injection(Kind,element) ::=
|
||||||
|
Kind series(element,SEMI,End)
|
||||||
|
| Kind End
|
||||||
|
| Kind LBRACKET series(element,SEMI,RBRACKET)
|
||||||
|
| Kind LBRACKET RBRACKET
|
||||||
|
|
||||||
|
binding ::=
|
||||||
|
expr ARROW expr
|
||||||
|
|
||||||
|
record_patch ::=
|
||||||
|
Patch path With record_expr
|
||||||
|
|
||||||
|
fail_instr ::=
|
||||||
|
Fail expr
|
||||||
|
|
||||||
|
proc_call ::=
|
||||||
|
fun_call
|
||||||
|
|
||||||
|
conditional ::=
|
||||||
|
If expr Then if_clause option(SEMI) Else if_clause
|
||||||
|
|
||||||
|
if_clause ::=
|
||||||
|
instruction
|
||||||
|
| LBRACE series(statement,COMMA,RBRACE)
|
||||||
|
|
||||||
|
case_instr ::=
|
||||||
|
case(instruction)
|
||||||
|
|
||||||
|
case(rhs) ::=
|
||||||
|
Case expr Of option(VBAR) cases(rhs) End
|
||||||
|
| Case expr Of LBRACKET option(VBAR) cases(rhs) RBRACKET
|
||||||
|
|
||||||
|
cases(rhs) ::=
|
||||||
|
nsepseq(case_clause(rhs),VBAR)
|
||||||
|
|
||||||
|
case_clause(rhs) ::=
|
||||||
|
pattern ARROW rhs
|
||||||
|
|
||||||
|
assignment ::=
|
||||||
|
lhs ASS rhs
|
||||||
|
|
||||||
|
rhs ::=
|
||||||
|
expr
|
||||||
|
|
||||||
|
lhs ::=
|
||||||
|
path
|
||||||
|
| map_lookup
|
||||||
|
|
||||||
|
loop ::=
|
||||||
|
while_loop
|
||||||
|
| for_loop
|
||||||
|
|
||||||
|
while_loop ::=
|
||||||
|
While expr block
|
||||||
|
|
||||||
|
for_loop ::=
|
||||||
|
For var_assign option(Down) To expr option(step_clause) block
|
||||||
|
| For Ident (* var *) option(arrow_clause) In expr block
|
||||||
|
|
||||||
|
var_assign ::=
|
||||||
|
Ident (* var *) ASS expr
|
||||||
|
|
||||||
|
step_clause ::=
|
||||||
|
Step expr
|
||||||
|
|
||||||
|
arrow_clause ::=
|
||||||
|
ARROW Ident (* var *)
|
||||||
|
|
||||||
|
(* Expressions *)
|
||||||
|
|
||||||
|
interactive_expr ::=
|
||||||
|
expr EOF
|
||||||
|
|
||||||
|
expr ::=
|
||||||
|
case(expr)
|
||||||
|
| annot_expr
|
||||||
|
|
||||||
|
annot_expr ::=
|
||||||
|
LPAR disj_expr COLON type_expr RPAR
|
||||||
|
| disj_expr
|
||||||
|
|
||||||
|
disj_expr ::=
|
||||||
|
disj_expr Or conj_expr
|
||||||
|
| conj_expr
|
||||||
|
|
||||||
|
conj_expr ::=
|
||||||
|
conj_expr And set_membership
|
||||||
|
| set_membership
|
||||||
|
|
||||||
|
set_membership ::=
|
||||||
|
core_expr Contains set_membership
|
||||||
|
| comp_expr
|
||||||
|
|
||||||
|
comp_expr ::=
|
||||||
|
comp_expr LT cat_expr
|
||||||
|
| comp_expr LEQ cat_expr
|
||||||
|
| comp_expr GT cat_expr
|
||||||
|
| comp_expr GEQ cat_expr
|
||||||
|
| comp_expr EQUAL cat_expr
|
||||||
|
| comp_expr NEQ cat_expr
|
||||||
|
| cat_expr
|
||||||
|
|
||||||
|
cat_expr ::=
|
||||||
|
cons_expr CAT cat_expr
|
||||||
|
| cons_expr
|
||||||
|
|
||||||
|
cons_expr ::=
|
||||||
|
add_expr CONS cons_expr
|
||||||
|
| add_expr
|
||||||
|
|
||||||
|
add_expr ::=
|
||||||
|
add_expr PLUS mult_expr
|
||||||
|
| add_expr MINUS mult_expr
|
||||||
|
| mult_expr
|
||||||
|
|
||||||
|
mult_expr ::=
|
||||||
|
mult_expr TIMES unary_expr
|
||||||
|
| mult_expr SLASH unary_expr
|
||||||
|
| mult_expr Mod unary_expr
|
||||||
|
| unary_expr
|
||||||
|
|
||||||
|
unary_expr ::=
|
||||||
|
MINUS core_expr
|
||||||
|
| Not core_expr
|
||||||
|
| core_expr
|
||||||
|
|
||||||
|
core_expr ::=
|
||||||
|
Int
|
||||||
|
| Nat
|
||||||
|
| Mtz
|
||||||
|
| Ident (* var *)
|
||||||
|
| String
|
||||||
|
| Bytes
|
||||||
|
| C_False
|
||||||
|
| C_True
|
||||||
|
| C_Unit
|
||||||
|
| tuple_expr
|
||||||
|
| list_expr
|
||||||
|
| C_None
|
||||||
|
| fun_call
|
||||||
|
| map_expr
|
||||||
|
| set_expr
|
||||||
|
| record_expr
|
||||||
|
| projection
|
||||||
|
| Constr arguments
|
||||||
|
| Constr
|
||||||
|
| C_Some arguments
|
||||||
|
|
||||||
|
set_expr ::=
|
||||||
|
injection(Set,expr)
|
||||||
|
|
||||||
|
map_expr ::=
|
||||||
|
map_lookup
|
||||||
|
| injection(Map,binding)
|
||||||
|
|
||||||
|
map_lookup ::=
|
||||||
|
path brackets(expr)
|
||||||
|
|
||||||
|
path ::=
|
||||||
|
Ident (* var *)
|
||||||
|
| projection
|
||||||
|
|
||||||
|
projection ::=
|
||||||
|
Ident (* struct_name *) DOT nsepseq(selection,DOT)
|
||||||
|
|
||||||
|
selection ::=
|
||||||
|
Ident (* field_name *)
|
||||||
|
| Int
|
||||||
|
|
||||||
|
record_expr ::=
|
||||||
|
Record series(field_assignment,SEMI,End)
|
||||||
|
| Record LBRACKET series(field_assignment,SEMI,RBRACKET)
|
||||||
|
|
||||||
|
field_assignment ::=
|
||||||
|
Ident (* field_name *) EQUAL expr
|
||||||
|
|
||||||
|
fun_call ::=
|
||||||
|
Ident (* fun_name *) arguments
|
||||||
|
|
||||||
|
tuple_expr ::=
|
||||||
|
tuple_inj
|
||||||
|
|
||||||
|
tuple_inj ::=
|
||||||
|
par(nsepseq(expr,COMMA))
|
||||||
|
|
||||||
|
arguments ::=
|
||||||
|
tuple_inj
|
||||||
|
|
||||||
|
list_expr ::=
|
||||||
|
injection(List,expr)
|
||||||
|
| Nil
|
||||||
|
|
||||||
|
(* Patterns *)
|
||||||
|
|
||||||
|
pattern ::=
|
||||||
|
nsepseq(core_pattern,CONS)
|
||||||
|
|
||||||
|
core_pattern ::=
|
||||||
|
Ident (* var *)
|
||||||
|
| WILD
|
||||||
|
| Int
|
||||||
|
| String
|
||||||
|
| C_Unit
|
||||||
|
| C_False
|
||||||
|
| C_True
|
||||||
|
| C_None
|
||||||
|
| list_pattern
|
||||||
|
| tuple_pattern
|
||||||
|
| constr_pattern
|
||||||
|
| C_Some par(core_pattern)
|
||||||
|
|
||||||
|
list_pattern ::=
|
||||||
|
injection(List,core_pattern)
|
||||||
|
| Nil
|
||||||
|
| par(cons_pattern)
|
||||||
|
|
||||||
|
cons_pattern ::=
|
||||||
|
core_pattern CONS pattern
|
||||||
|
|
||||||
|
tuple_pattern ::=
|
||||||
|
par(nsepseq(core_pattern,COMMA))
|
||||||
|
|
||||||
|
constr_pattern ::=
|
||||||
|
Constr tuple_pattern
|
||||||
|
| Constr
|
||||||
396
src/parser/pascaligo/Doc/pascaligo4.bnf
Normal file
396
src/parser/pascaligo/Doc/pascaligo4.bnf
Normal file
@ -0,0 +1,396 @@
|
|||||||
|
option(X) :=
|
||||||
|
(**)
|
||||||
|
| X
|
||||||
|
|
||||||
|
series(item,sep,term) ::=
|
||||||
|
item after_item(item,sep,term)
|
||||||
|
|
||||||
|
after_item(item,sep,term) ::=
|
||||||
|
sep item_or_closing(item,sep,term)
|
||||||
|
| term
|
||||||
|
|
||||||
|
item_or_closing(item,sep,term) ::=
|
||||||
|
term
|
||||||
|
| series(item,sep,term)
|
||||||
|
|
||||||
|
(* Compound constructs *)
|
||||||
|
|
||||||
|
par(X) ::= LPAR X RPAR
|
||||||
|
|
||||||
|
brackets(X) ::= LBRACKET X RBRACKET
|
||||||
|
|
||||||
|
(* Sequences *)
|
||||||
|
|
||||||
|
(* Possibly empty sequence of items *)
|
||||||
|
|
||||||
|
seq(X) ::=
|
||||||
|
(**)
|
||||||
|
| X seq(X)
|
||||||
|
|
||||||
|
(* Non-empty sequence of items *)
|
||||||
|
|
||||||
|
nseq(X) ::= X seq(X)
|
||||||
|
|
||||||
|
(* Non-empty separated sequence of items *)
|
||||||
|
|
||||||
|
nsepseq(X,Sep) ::=
|
||||||
|
X
|
||||||
|
| X Sep nsepseq(X,Sep)
|
||||||
|
|
||||||
|
(* Possibly empy separated sequence of items *)
|
||||||
|
|
||||||
|
sepseq(X,Sep) ::=
|
||||||
|
(**)
|
||||||
|
| nsepseq(X,Sep)
|
||||||
|
|
||||||
|
(* Main *)
|
||||||
|
|
||||||
|
contract ::=
|
||||||
|
nseq(declaration) EOF
|
||||||
|
|
||||||
|
declaration ::=
|
||||||
|
type_decl
|
||||||
|
| const_decl
|
||||||
|
| lambda_decl
|
||||||
|
|
||||||
|
(* Type declarations *)
|
||||||
|
|
||||||
|
type_decl ::=
|
||||||
|
Type Ident (* type_name *) Is type_expr option(SEMI)
|
||||||
|
|
||||||
|
type_expr ::=
|
||||||
|
cartesian
|
||||||
|
| sum_type
|
||||||
|
| record_type
|
||||||
|
|
||||||
|
cartesian ::=
|
||||||
|
nsepseq(function_type,TIMES)
|
||||||
|
|
||||||
|
function_type ::=
|
||||||
|
core_type
|
||||||
|
| core_type ARROW function_type
|
||||||
|
|
||||||
|
core_type ::=
|
||||||
|
Ident (* type_name *)
|
||||||
|
| Ident (* type_name *) type_tuple
|
||||||
|
| Map type_tuple
|
||||||
|
| Set par(type_expr)
|
||||||
|
| List par(type_expr)
|
||||||
|
| par(type_expr)
|
||||||
|
|
||||||
|
type_tuple ::=
|
||||||
|
par(nsepseq(type_expr,COMMA))
|
||||||
|
|
||||||
|
sum_type ::=
|
||||||
|
option(VBAR) nsepseq(variant,VBAR)
|
||||||
|
|
||||||
|
variant ::=
|
||||||
|
Constr Of cartesian
|
||||||
|
| Constr
|
||||||
|
|
||||||
|
record_type ::=
|
||||||
|
Record series(field_decl,SEMI,End)
|
||||||
|
| Record LBRACKET series(field_decl,SEMI,RBRACKET)
|
||||||
|
|
||||||
|
field_decl ::=
|
||||||
|
Ident (* field_name *) COLON type_expr
|
||||||
|
|
||||||
|
(* Function and procedure declarations *)
|
||||||
|
|
||||||
|
lambda_decl ::=
|
||||||
|
fun_decl
|
||||||
|
| proc_decl
|
||||||
|
| entry_decl
|
||||||
|
|
||||||
|
fun_decl ::=
|
||||||
|
Function Ident (* fun_name *) parameters COLON type_expr Is
|
||||||
|
seq(local_decl)
|
||||||
|
block
|
||||||
|
With expr option(SEMI)
|
||||||
|
|
||||||
|
entry_decl ::=
|
||||||
|
Entrypoint Ident (* fun_name *) entry_params COLON type_expr Is
|
||||||
|
seq(local_decl)
|
||||||
|
block
|
||||||
|
With expr option(SEMI)
|
||||||
|
|
||||||
|
entry_params ::=
|
||||||
|
par(nsepseq(entry_param_decl,SEMI))
|
||||||
|
|
||||||
|
proc_decl ::=
|
||||||
|
Procedure Ident (* fun_name *) parameters Is
|
||||||
|
seq(local_decl)
|
||||||
|
block option(SEMI)
|
||||||
|
|
||||||
|
parameters ::=
|
||||||
|
par(nsepseq(param_decl,SEMI))
|
||||||
|
|
||||||
|
param_decl ::=
|
||||||
|
Var Ident (* var *) COLON param_type
|
||||||
|
| Const Ident (* var *) COLON param_type
|
||||||
|
|
||||||
|
entry_param_decl ::=
|
||||||
|
param_decl
|
||||||
|
| Storage Ident (* var *) COLON param_type
|
||||||
|
|
||||||
|
param_type ::=
|
||||||
|
cartesian
|
||||||
|
|
||||||
|
block ::=
|
||||||
|
Begin series(statement,SEMI,End)
|
||||||
|
| Block LBRACE series(statement,SEMI,RBRACE)
|
||||||
|
|
||||||
|
statement ::=
|
||||||
|
instruction
|
||||||
|
| open_data_decl
|
||||||
|
|
||||||
|
open_data_decl ::=
|
||||||
|
open_const_decl
|
||||||
|
| open_var_decl
|
||||||
|
|
||||||
|
open_const_decl ::=
|
||||||
|
Const unqualified_decl(EQUAL)
|
||||||
|
|
||||||
|
open_var_decl ::=
|
||||||
|
Var unqualified_decl(ASS)
|
||||||
|
|
||||||
|
local_decl ::=
|
||||||
|
fun_decl
|
||||||
|
| proc_decl
|
||||||
|
| data_decl
|
||||||
|
|
||||||
|
data_decl ::=
|
||||||
|
const_decl
|
||||||
|
| var_decl
|
||||||
|
|
||||||
|
unqualified_decl(OP) ::=
|
||||||
|
Ident (* var *) COLON type_expr OP extended_expr
|
||||||
|
|
||||||
|
const_decl ::=
|
||||||
|
open_const_decl option(SEMI)
|
||||||
|
|
||||||
|
var_decl ::=
|
||||||
|
open_var_decl option(SEMI)
|
||||||
|
|
||||||
|
extended_expr ::=
|
||||||
|
expr
|
||||||
|
|
||||||
|
instruction ::=
|
||||||
|
single_instr
|
||||||
|
| block
|
||||||
|
|
||||||
|
single_instr ::=
|
||||||
|
If expr Then if_clause option(SEMI) Else if_clause
|
||||||
|
| case(instruction)
|
||||||
|
| path ASS expr
|
||||||
|
| path brackets(expr) (* map_lookup *) ASS expr
|
||||||
|
| loop
|
||||||
|
| proc_call
|
||||||
|
| Fail expr
|
||||||
|
| Skip
|
||||||
|
| Patch path With record_expr
|
||||||
|
| Patch path With injection(Map,binding)
|
||||||
|
| Patch path With injection(Set,expr)
|
||||||
|
| Remove expr From Map path
|
||||||
|
| Remove expr From Set path
|
||||||
|
|
||||||
|
injection(Kind,element) ::=
|
||||||
|
Kind series(element,SEMI,End)
|
||||||
|
| Kind End
|
||||||
|
| Kind LBRACKET series(element,SEMI,RBRACKET)
|
||||||
|
| Kind LBRACKET RBRACKET
|
||||||
|
|
||||||
|
binding ::=
|
||||||
|
expr ARROW expr
|
||||||
|
|
||||||
|
proc_call ::=
|
||||||
|
fun_call
|
||||||
|
|
||||||
|
if_clause ::=
|
||||||
|
instruction
|
||||||
|
| LBRACE series(statement,COMMA,RBRACE)
|
||||||
|
|
||||||
|
case(rhs) ::=
|
||||||
|
Case expr Of option(VBAR) cases(rhs) End
|
||||||
|
| Case expr Of LBRACKET option(VBAR) cases(rhs) RBRACKET
|
||||||
|
|
||||||
|
cases(rhs) ::=
|
||||||
|
nsepseq(case_clause(rhs),VBAR)
|
||||||
|
|
||||||
|
case_clause(rhs) ::=
|
||||||
|
pattern ARROW rhs
|
||||||
|
|
||||||
|
loop ::=
|
||||||
|
while_loop
|
||||||
|
| for_loop
|
||||||
|
|
||||||
|
while_loop ::=
|
||||||
|
While expr block
|
||||||
|
|
||||||
|
for_loop ::=
|
||||||
|
For var_assign option(Down) To expr option(step_clause) block
|
||||||
|
| For Ident (* var *) option(arrow_clause) In expr block
|
||||||
|
|
||||||
|
var_assign ::=
|
||||||
|
Ident (* var *) ASS expr
|
||||||
|
|
||||||
|
step_clause ::=
|
||||||
|
Step expr
|
||||||
|
|
||||||
|
arrow_clause ::=
|
||||||
|
ARROW Ident (* var *)
|
||||||
|
|
||||||
|
(* Expressions *)
|
||||||
|
|
||||||
|
interactive_expr ::=
|
||||||
|
expr EOF
|
||||||
|
|
||||||
|
expr ::=
|
||||||
|
case(expr)
|
||||||
|
| annot_expr
|
||||||
|
|
||||||
|
annot_expr ::=
|
||||||
|
LPAR disj_expr COLON type_expr RPAR
|
||||||
|
| disj_expr
|
||||||
|
|
||||||
|
disj_expr ::=
|
||||||
|
disj_expr Or conj_expr
|
||||||
|
| conj_expr
|
||||||
|
|
||||||
|
conj_expr ::=
|
||||||
|
conj_expr And set_membership
|
||||||
|
| set_membership
|
||||||
|
|
||||||
|
set_membership ::=
|
||||||
|
core_expr Contains set_membership
|
||||||
|
| comp_expr
|
||||||
|
|
||||||
|
comp_expr ::=
|
||||||
|
comp_expr LT cat_expr
|
||||||
|
| comp_expr LEQ cat_expr
|
||||||
|
| comp_expr GT cat_expr
|
||||||
|
| comp_expr GEQ cat_expr
|
||||||
|
| comp_expr EQUAL cat_expr
|
||||||
|
| comp_expr NEQ cat_expr
|
||||||
|
| cat_expr
|
||||||
|
|
||||||
|
cat_expr ::=
|
||||||
|
cons_expr CAT cat_expr
|
||||||
|
| cons_expr
|
||||||
|
|
||||||
|
cons_expr ::=
|
||||||
|
add_expr CONS cons_expr
|
||||||
|
| add_expr
|
||||||
|
|
||||||
|
add_expr ::=
|
||||||
|
add_expr PLUS mult_expr
|
||||||
|
| add_expr MINUS mult_expr
|
||||||
|
| mult_expr
|
||||||
|
|
||||||
|
mult_expr ::=
|
||||||
|
mult_expr TIMES unary_expr
|
||||||
|
| mult_expr SLASH unary_expr
|
||||||
|
| mult_expr Mod unary_expr
|
||||||
|
| unary_expr
|
||||||
|
|
||||||
|
unary_expr ::=
|
||||||
|
MINUS core_expr
|
||||||
|
| Not core_expr
|
||||||
|
| core_expr
|
||||||
|
|
||||||
|
core_expr ::=
|
||||||
|
Int
|
||||||
|
| Nat
|
||||||
|
| Mtz
|
||||||
|
| Ident (* var *)
|
||||||
|
| String
|
||||||
|
| Bytes
|
||||||
|
| C_False
|
||||||
|
| C_True
|
||||||
|
| C_Unit
|
||||||
|
| tuple_expr
|
||||||
|
| list_expr
|
||||||
|
| C_None
|
||||||
|
| fun_call
|
||||||
|
| map_expr
|
||||||
|
| set_expr
|
||||||
|
| record_expr
|
||||||
|
| Ident (* struct_name *) DOT nsepseq(selection,DOT)
|
||||||
|
| Constr arguments
|
||||||
|
| Constr
|
||||||
|
| C_Some arguments
|
||||||
|
|
||||||
|
set_expr ::=
|
||||||
|
injection(Set,expr)
|
||||||
|
|
||||||
|
map_expr ::=
|
||||||
|
map_lookup
|
||||||
|
| injection(Map,binding)
|
||||||
|
|
||||||
|
map_lookup ::=
|
||||||
|
path brackets(expr)
|
||||||
|
|
||||||
|
path ::=
|
||||||
|
Ident (* var *)
|
||||||
|
| Ident (* struct_name *) DOT nsepseq(selection,DOT)
|
||||||
|
|
||||||
|
selection ::=
|
||||||
|
Ident (* field_name *)
|
||||||
|
| Int
|
||||||
|
|
||||||
|
record_expr ::=
|
||||||
|
Record series(field_assignment,SEMI,End)
|
||||||
|
| Record LBRACKET series(field_assignment,SEMI,RBRACKET)
|
||||||
|
|
||||||
|
field_assignment ::=
|
||||||
|
Ident (* field_name *) EQUAL expr
|
||||||
|
|
||||||
|
fun_call ::=
|
||||||
|
Ident (* fun_name *) arguments
|
||||||
|
|
||||||
|
tuple_expr ::=
|
||||||
|
tuple_inj
|
||||||
|
|
||||||
|
tuple_inj ::=
|
||||||
|
par(nsepseq(expr,COMMA))
|
||||||
|
|
||||||
|
arguments ::=
|
||||||
|
tuple_inj
|
||||||
|
|
||||||
|
list_expr ::=
|
||||||
|
injection(List,expr)
|
||||||
|
| Nil
|
||||||
|
|
||||||
|
(* Patterns *)
|
||||||
|
|
||||||
|
pattern ::=
|
||||||
|
nsepseq(core_pattern,CONS)
|
||||||
|
|
||||||
|
core_pattern ::=
|
||||||
|
Ident (* var *)
|
||||||
|
| WILD
|
||||||
|
| Int
|
||||||
|
| String
|
||||||
|
| C_Unit
|
||||||
|
| C_False
|
||||||
|
| C_True
|
||||||
|
| C_None
|
||||||
|
| list_pattern
|
||||||
|
| tuple_pattern
|
||||||
|
| constr_pattern
|
||||||
|
| C_Some par(core_pattern)
|
||||||
|
|
||||||
|
list_pattern ::=
|
||||||
|
injection(List,core_pattern)
|
||||||
|
| Nil
|
||||||
|
| par(cons_pattern)
|
||||||
|
|
||||||
|
cons_pattern ::=
|
||||||
|
core_pattern CONS pattern
|
||||||
|
|
||||||
|
tuple_pattern ::=
|
||||||
|
par(nsepseq(core_pattern,COMMA))
|
||||||
|
|
||||||
|
constr_pattern ::=
|
||||||
|
Constr tuple_pattern
|
||||||
|
| Constr
|
||||||
390
src/parser/pascaligo/Doc/pascaligo5.bnf
Normal file
390
src/parser/pascaligo/Doc/pascaligo5.bnf
Normal file
@ -0,0 +1,390 @@
|
|||||||
|
option(X) :=
|
||||||
|
(**)
|
||||||
|
| X
|
||||||
|
|
||||||
|
series(item,sep,term) ::=
|
||||||
|
item after_item(item,sep,term)
|
||||||
|
|
||||||
|
after_item(item,sep,term) ::=
|
||||||
|
sep item_or_closing(item,sep,term)
|
||||||
|
| term
|
||||||
|
|
||||||
|
item_or_closing(item,sep,term) ::=
|
||||||
|
term
|
||||||
|
| series(item,sep,term)
|
||||||
|
|
||||||
|
(* Compound constructs *)
|
||||||
|
|
||||||
|
par(X) ::= LPAR X RPAR
|
||||||
|
|
||||||
|
brackets(X) ::= LBRACKET X RBRACKET
|
||||||
|
|
||||||
|
(* Sequences *)
|
||||||
|
|
||||||
|
(* Possibly empty sequence of items *)
|
||||||
|
|
||||||
|
seq(X) ::=
|
||||||
|
(**)
|
||||||
|
| X seq(X)
|
||||||
|
|
||||||
|
(* Non-empty sequence of items *)
|
||||||
|
|
||||||
|
nseq(X) ::= X seq(X)
|
||||||
|
|
||||||
|
(* Non-empty separated sequence of items *)
|
||||||
|
|
||||||
|
nsepseq(X,Sep) ::=
|
||||||
|
X
|
||||||
|
| X Sep nsepseq(X,Sep)
|
||||||
|
|
||||||
|
(* Possibly empy separated sequence of items *)
|
||||||
|
|
||||||
|
sepseq(X,Sep) ::=
|
||||||
|
(**)
|
||||||
|
| nsepseq(X,Sep)
|
||||||
|
|
||||||
|
(* Main *)
|
||||||
|
|
||||||
|
contract ::=
|
||||||
|
nseq(declaration) EOF
|
||||||
|
|
||||||
|
declaration ::=
|
||||||
|
type_decl
|
||||||
|
| const_decl
|
||||||
|
| lambda_decl
|
||||||
|
|
||||||
|
(* Type declarations *)
|
||||||
|
|
||||||
|
type_decl ::=
|
||||||
|
Type Ident (* type_name *) Is type_expr option(SEMI)
|
||||||
|
|
||||||
|
type_expr ::=
|
||||||
|
cartesian
|
||||||
|
| sum_type
|
||||||
|
| record_type
|
||||||
|
|
||||||
|
cartesian ::=
|
||||||
|
nsepseq(function_type,TIMES)
|
||||||
|
|
||||||
|
function_type ::=
|
||||||
|
core_type
|
||||||
|
| core_type ARROW function_type
|
||||||
|
|
||||||
|
core_type ::=
|
||||||
|
Ident (* type_name *)
|
||||||
|
| Ident (* type_name *) type_tuple
|
||||||
|
| Map type_tuple
|
||||||
|
| Set par(type_expr)
|
||||||
|
| List par(type_expr)
|
||||||
|
| par(type_expr)
|
||||||
|
|
||||||
|
type_tuple ::=
|
||||||
|
par(nsepseq(type_expr,COMMA))
|
||||||
|
|
||||||
|
sum_type ::=
|
||||||
|
option(VBAR) nsepseq(variant,VBAR)
|
||||||
|
|
||||||
|
variant ::=
|
||||||
|
Constr Of cartesian
|
||||||
|
| Constr
|
||||||
|
|
||||||
|
record_type ::=
|
||||||
|
Record series(field_decl,SEMI,End)
|
||||||
|
| Record LBRACKET series(field_decl,SEMI,RBRACKET)
|
||||||
|
|
||||||
|
field_decl ::=
|
||||||
|
Ident (* field_name *) COLON type_expr
|
||||||
|
|
||||||
|
(* Function and procedure declarations *)
|
||||||
|
|
||||||
|
lambda_decl ::=
|
||||||
|
fun_decl
|
||||||
|
| proc_decl
|
||||||
|
| entry_decl
|
||||||
|
|
||||||
|
fun_decl ::=
|
||||||
|
Function Ident (* fun_name *) parameters COLON type_expr Is
|
||||||
|
seq(local_decl)
|
||||||
|
block
|
||||||
|
With expr option(SEMI)
|
||||||
|
|
||||||
|
entry_decl ::=
|
||||||
|
Entrypoint Ident (* fun_name *) entry_params COLON type_expr Is
|
||||||
|
seq(local_decl)
|
||||||
|
block
|
||||||
|
With expr option(SEMI)
|
||||||
|
|
||||||
|
entry_params ::=
|
||||||
|
par(nsepseq(entry_param_decl,SEMI))
|
||||||
|
|
||||||
|
proc_decl ::=
|
||||||
|
Procedure Ident (* fun_name *) parameters Is
|
||||||
|
seq(local_decl)
|
||||||
|
block option(SEMI)
|
||||||
|
|
||||||
|
parameters ::=
|
||||||
|
par(nsepseq(param_decl,SEMI))
|
||||||
|
|
||||||
|
param_decl ::=
|
||||||
|
Var Ident (* var *) COLON param_type
|
||||||
|
| Const Ident (* var *) COLON param_type
|
||||||
|
|
||||||
|
entry_param_decl ::=
|
||||||
|
param_decl
|
||||||
|
| Storage Ident (* var *) COLON param_type
|
||||||
|
|
||||||
|
param_type ::=
|
||||||
|
cartesian
|
||||||
|
|
||||||
|
block ::=
|
||||||
|
Begin series(statement,SEMI,End)
|
||||||
|
| Block LBRACE series(statement,SEMI,RBRACE)
|
||||||
|
|
||||||
|
statement ::=
|
||||||
|
instruction
|
||||||
|
| open_data_decl
|
||||||
|
|
||||||
|
open_data_decl ::=
|
||||||
|
open_const_decl
|
||||||
|
| open_var_decl
|
||||||
|
|
||||||
|
open_const_decl ::=
|
||||||
|
Const unqualified_decl(EQUAL)
|
||||||
|
|
||||||
|
open_var_decl ::=
|
||||||
|
Var unqualified_decl(ASS)
|
||||||
|
|
||||||
|
local_decl ::=
|
||||||
|
fun_decl
|
||||||
|
| proc_decl
|
||||||
|
| data_decl
|
||||||
|
|
||||||
|
data_decl ::=
|
||||||
|
const_decl
|
||||||
|
| var_decl
|
||||||
|
|
||||||
|
unqualified_decl(OP) ::=
|
||||||
|
Ident (* var *) COLON type_expr OP extended_expr
|
||||||
|
|
||||||
|
const_decl ::=
|
||||||
|
open_const_decl option(SEMI)
|
||||||
|
|
||||||
|
var_decl ::=
|
||||||
|
open_var_decl option(SEMI)
|
||||||
|
|
||||||
|
extended_expr ::=
|
||||||
|
expr
|
||||||
|
|
||||||
|
instruction ::=
|
||||||
|
single_instr
|
||||||
|
| block
|
||||||
|
|
||||||
|
single_instr ::=
|
||||||
|
If expr Then if_clause option(SEMI) Else if_clause
|
||||||
|
| case(instruction)
|
||||||
|
| Ident (* proc_name *) arguments
|
||||||
|
| Ident option(brackets(expr)) ASS expr
|
||||||
|
| Ident DOT nsepseq(selection,DOT) option(brackets(expr)) ASS expr
|
||||||
|
| loop
|
||||||
|
| Fail expr
|
||||||
|
| Skip
|
||||||
|
| Patch path With record_expr
|
||||||
|
| Patch path With injection(Map,binding)
|
||||||
|
| Patch path With injection(Set,expr)
|
||||||
|
| Remove expr From Map path
|
||||||
|
| Remove expr From Set path
|
||||||
|
|
||||||
|
injection(Kind,element) ::=
|
||||||
|
Kind series(element,SEMI,End)
|
||||||
|
| Kind End
|
||||||
|
| Kind LBRACKET series(element,SEMI,RBRACKET)
|
||||||
|
| Kind LBRACKET RBRACKET
|
||||||
|
|
||||||
|
binding ::=
|
||||||
|
expr ARROW expr
|
||||||
|
|
||||||
|
if_clause ::=
|
||||||
|
instruction
|
||||||
|
| LBRACE series(statement,COMMA,RBRACE)
|
||||||
|
|
||||||
|
case(rhs) ::=
|
||||||
|
Case expr Of option(VBAR) cases(rhs) End
|
||||||
|
| Case expr Of LBRACKET option(VBAR) cases(rhs) RBRACKET
|
||||||
|
|
||||||
|
cases(rhs) ::=
|
||||||
|
nsepseq(case_clause(rhs),VBAR)
|
||||||
|
|
||||||
|
case_clause(rhs) ::=
|
||||||
|
pattern ARROW rhs
|
||||||
|
|
||||||
|
loop ::=
|
||||||
|
while_loop
|
||||||
|
| for_loop
|
||||||
|
|
||||||
|
while_loop ::=
|
||||||
|
While expr block
|
||||||
|
|
||||||
|
for_loop ::=
|
||||||
|
For Ident (* var *) ASS expr option(Down) To expr option(step_clause) block
|
||||||
|
| For Ident (* var *) option(arrow_clause) In expr block
|
||||||
|
|
||||||
|
step_clause ::=
|
||||||
|
Step expr
|
||||||
|
|
||||||
|
arrow_clause ::=
|
||||||
|
ARROW Ident (* var *)
|
||||||
|
|
||||||
|
(* Expressions *)
|
||||||
|
|
||||||
|
interactive_expr ::=
|
||||||
|
expr EOF
|
||||||
|
|
||||||
|
expr ::=
|
||||||
|
case(expr)
|
||||||
|
| annot_expr
|
||||||
|
|
||||||
|
annot_expr ::=
|
||||||
|
LPAR disj_expr COLON type_expr RPAR
|
||||||
|
| disj_expr
|
||||||
|
|
||||||
|
disj_expr ::=
|
||||||
|
disj_expr Or conj_expr
|
||||||
|
| conj_expr
|
||||||
|
|
||||||
|
conj_expr ::=
|
||||||
|
conj_expr And set_membership
|
||||||
|
| set_membership
|
||||||
|
|
||||||
|
set_membership ::=
|
||||||
|
core_expr Contains set_membership
|
||||||
|
| comp_expr
|
||||||
|
|
||||||
|
comp_expr ::=
|
||||||
|
comp_expr LT cat_expr
|
||||||
|
| comp_expr LEQ cat_expr
|
||||||
|
| comp_expr GT cat_expr
|
||||||
|
| comp_expr GEQ cat_expr
|
||||||
|
| comp_expr EQUAL cat_expr
|
||||||
|
| comp_expr NEQ cat_expr
|
||||||
|
| cat_expr
|
||||||
|
|
||||||
|
cat_expr ::=
|
||||||
|
cons_expr CAT cat_expr
|
||||||
|
| cons_expr
|
||||||
|
|
||||||
|
cons_expr ::=
|
||||||
|
add_expr CONS cons_expr
|
||||||
|
| add_expr
|
||||||
|
|
||||||
|
add_expr ::=
|
||||||
|
add_expr PLUS mult_expr
|
||||||
|
| add_expr MINUS mult_expr
|
||||||
|
| mult_expr
|
||||||
|
|
||||||
|
mult_expr ::=
|
||||||
|
mult_expr TIMES unary_expr
|
||||||
|
| mult_expr SLASH unary_expr
|
||||||
|
| mult_expr Mod unary_expr
|
||||||
|
| unary_expr
|
||||||
|
|
||||||
|
unary_expr ::=
|
||||||
|
MINUS core_expr
|
||||||
|
| Not core_expr
|
||||||
|
| core_expr
|
||||||
|
|
||||||
|
core_expr ::=
|
||||||
|
Int
|
||||||
|
| Nat
|
||||||
|
| Mtz
|
||||||
|
| Ident (* var *)
|
||||||
|
| String
|
||||||
|
| Bytes
|
||||||
|
| C_False
|
||||||
|
| C_True
|
||||||
|
| C_Unit
|
||||||
|
| tuple_expr
|
||||||
|
| list_expr
|
||||||
|
| C_None
|
||||||
|
| fun_call
|
||||||
|
| map_expr
|
||||||
|
| set_expr
|
||||||
|
| record_expr
|
||||||
|
| Ident (* struct_name *) DOT nsepseq(selection,DOT)
|
||||||
|
| Constr arguments
|
||||||
|
| Constr
|
||||||
|
| C_Some arguments
|
||||||
|
|
||||||
|
set_expr ::=
|
||||||
|
injection(Set,expr)
|
||||||
|
|
||||||
|
map_expr ::=
|
||||||
|
map_lookup
|
||||||
|
| injection(Map,binding)
|
||||||
|
|
||||||
|
map_lookup ::=
|
||||||
|
path brackets(expr)
|
||||||
|
|
||||||
|
path ::=
|
||||||
|
Ident (* var *)
|
||||||
|
| Ident (* struct_name *) DOT nsepseq(selection,DOT)
|
||||||
|
|
||||||
|
selection ::=
|
||||||
|
Ident (* field_name *)
|
||||||
|
| Int
|
||||||
|
|
||||||
|
record_expr ::=
|
||||||
|
Record series(field_assignment,SEMI,End)
|
||||||
|
| Record LBRACKET series(field_assignment,SEMI,RBRACKET)
|
||||||
|
|
||||||
|
field_assignment ::=
|
||||||
|
Ident (* field_name *) EQUAL expr
|
||||||
|
|
||||||
|
fun_call ::=
|
||||||
|
Ident (* fun_name *) arguments
|
||||||
|
|
||||||
|
tuple_expr ::=
|
||||||
|
tuple_inj
|
||||||
|
|
||||||
|
tuple_inj ::=
|
||||||
|
par(nsepseq(expr,COMMA))
|
||||||
|
|
||||||
|
arguments ::=
|
||||||
|
tuple_inj
|
||||||
|
|
||||||
|
list_expr ::=
|
||||||
|
injection(List,expr)
|
||||||
|
| Nil
|
||||||
|
|
||||||
|
(* Patterns *)
|
||||||
|
|
||||||
|
pattern ::=
|
||||||
|
nsepseq(core_pattern,CONS)
|
||||||
|
|
||||||
|
core_pattern ::=
|
||||||
|
Ident (* var *)
|
||||||
|
| WILD
|
||||||
|
| Int
|
||||||
|
| String
|
||||||
|
| C_Unit
|
||||||
|
| C_False
|
||||||
|
| C_True
|
||||||
|
| C_None
|
||||||
|
| list_pattern
|
||||||
|
| tuple_pattern
|
||||||
|
| constr_pattern
|
||||||
|
| C_Some par(core_pattern)
|
||||||
|
|
||||||
|
list_pattern ::=
|
||||||
|
injection(List,core_pattern)
|
||||||
|
| Nil
|
||||||
|
| par(cons_pattern)
|
||||||
|
|
||||||
|
cons_pattern ::=
|
||||||
|
core_pattern CONS pattern
|
||||||
|
|
||||||
|
tuple_pattern ::=
|
||||||
|
par(nsepseq(core_pattern,COMMA))
|
||||||
|
|
||||||
|
constr_pattern ::=
|
||||||
|
Constr tuple_pattern
|
||||||
|
| Constr
|
||||||
Loading…
Reference in New Issue
Block a user