More rewrites of the grammar for stream parsing.
Fixed code in the internal documentation of PascaLIGO.
This commit is contained in:
Christian Rinderknecht
parent
fddce3257a
commit
f99bd0d1df
@ -190,15 +190,15 @@ the latter can be reassigned. The syntax is slightly different for
|
|||||||
both. For example, the variables "x" and "y" above could have been
|
both. For example, the variables "x" and "y" above could have been
|
||||||
declared as follows:
|
declared as follows:
|
||||||
|
|
||||||
var x : nat := 0;
|
var x : nat := 0n;
|
||||||
var y : nat := 0;
|
var y : nat := 0n;
|
||||||
|
|
||||||
It is possible to specify that the value of a variable will not change
|
It is possible to specify that the value of a variable will not change
|
||||||
(the name "variable" is misleading in that context), that is, they
|
(the name "variable" is misleading in that context), that is, they
|
||||||
remain constant:
|
remain constant:
|
||||||
|
|
||||||
const ten : nat = 10;
|
const ten : nat = 10n;
|
||||||
const eleven : nat = ten + 1;
|
const eleven : nat = ten + 1n;
|
||||||
|
|
||||||
Similarly, function declarations have their parameters and return
|
Similarly, function declarations have their parameters and return
|
||||||
value annotated with their types. For instance,
|
value annotated with their types. For instance,
|
||||||
@ -214,10 +214,10 @@ the result of calling the function is given after the keyword "with".
|
|||||||
A another example would be
|
A another example would be
|
||||||
|
|
||||||
function factorial (const n : nat) : nat is
|
function factorial (const n : nat) : nat is
|
||||||
var m : nat := 0;
|
var m : nat := 0n;
|
||||||
var f : nat := 1;
|
var f : nat := 1n;
|
||||||
begin
|
begin
|
||||||
if n <= 0 then f := 1
|
if n <= 0n then f := 1n
|
||||||
else
|
else
|
||||||
for m := 1 to n
|
for m := 1 to n
|
||||||
begin
|
begin
|
||||||
|
|||||||
375
src/parser/pascaligo/Doc/pascaligo_21.bnf
Normal file
375
src/parser/pascaligo/Doc/pascaligo_21.bnf
Normal file
@ -0,0 +1,375 @@
|
|||||||
|
right_assoc(item,op) ::=
|
||||||
|
item
|
||||||
|
| item op right_assoc(item,op)
|
||||||
|
|
||||||
|
left_assoc(item,op) ::=
|
||||||
|
right_assoc(item,op)
|
||||||
|
|
||||||
|
option(item) :=
|
||||||
|
(**)
|
||||||
|
| item
|
||||||
|
|
||||||
|
series(item,sep,term) ::=
|
||||||
|
item after_item(item,sep,term)
|
||||||
|
|
||||||
|
after_item(item,sep,term) ::=
|
||||||
|
sep item_or_closing(item,sep,term)
|
||||||
|
| term
|
||||||
|
|
||||||
|
item_or_closing(item,sep,term) ::=
|
||||||
|
term
|
||||||
|
| series(item,sep,term)
|
||||||
|
|
||||||
|
(* Compound constructs *)
|
||||||
|
|
||||||
|
par(item) ::=
|
||||||
|
LPAR item RPAR
|
||||||
|
|
||||||
|
brackets(item) ::=
|
||||||
|
LBRACKET item RBRACKET
|
||||||
|
|
||||||
|
(* Sequences *)
|
||||||
|
|
||||||
|
(* Possibly empty sequence of items *)
|
||||||
|
|
||||||
|
seq(item) ::=
|
||||||
|
option(nseq(item))
|
||||||
|
|
||||||
|
(* Non-empty sequence of items *)
|
||||||
|
|
||||||
|
nseq(item) ::=
|
||||||
|
item seq(item)
|
||||||
|
|
||||||
|
(* Non-empty separated sequence of items *)
|
||||||
|
|
||||||
|
nsepseq(item,Sep) ::=
|
||||||
|
item
|
||||||
|
| item Sep nsepseq(item,Sep)
|
||||||
|
|
||||||
|
(* Possibly empty separated sequence of items *)
|
||||||
|
|
||||||
|
sepseq(item,Sep) ::=
|
||||||
|
option(nsepseq(item,Sep))
|
||||||
|
|
||||||
|
(* Main *)
|
||||||
|
|
||||||
|
contract ::=
|
||||||
|
nseq(declaration) EOF
|
||||||
|
|
||||||
|
declaration ::=
|
||||||
|
type_decl option(SEMI)
|
||||||
|
| const_decl option(SEMI)
|
||||||
|
| lambda_decl option(SEMI)
|
||||||
|
|
||||||
|
(* Type declarations *)
|
||||||
|
|
||||||
|
type_decl ::=
|
||||||
|
Type Ident Is type_expr
|
||||||
|
|
||||||
|
type_expr ::=
|
||||||
|
cartesian
|
||||||
|
| nsepseq(variant,VBAR)
|
||||||
|
| VBAR nsepseq(variant,VBAR)
|
||||||
|
| Record record_type_expr
|
||||||
|
|
||||||
|
record_type_expr ::=
|
||||||
|
series(field_decl,SEMI,End)
|
||||||
|
| LBRACKET series(field_decl,SEMI,RBRACKET)
|
||||||
|
|
||||||
|
variant ::=
|
||||||
|
Constr option(of_cartesian)
|
||||||
|
|
||||||
|
of_cartesian ::=
|
||||||
|
Of cartesian
|
||||||
|
|
||||||
|
cartesian ::=
|
||||||
|
nsepseq(function_type,TIMES)
|
||||||
|
|
||||||
|
function_type ::=
|
||||||
|
right_assoc(core_type,ARROW)
|
||||||
|
|
||||||
|
core_type ::=
|
||||||
|
Ident (* type_name *) option(type_tuple)
|
||||||
|
| Map type_tuple
|
||||||
|
| Set par(type_expr)
|
||||||
|
| List par(type_expr)
|
||||||
|
| par(type_expr)
|
||||||
|
|
||||||
|
type_tuple ::=
|
||||||
|
par(nsepseq(type_expr,COMMA))
|
||||||
|
|
||||||
|
field_decl ::=
|
||||||
|
Ident (* field_name *) COLON type_expr
|
||||||
|
|
||||||
|
(* Function and procedure declarations *)
|
||||||
|
|
||||||
|
lambda_decl ::=
|
||||||
|
fun_decl
|
||||||
|
| proc_decl
|
||||||
|
| entry_decl
|
||||||
|
|
||||||
|
fun_decl ::=
|
||||||
|
Function Ident parameters COLON type_expr Is
|
||||||
|
seq(local_decl)
|
||||||
|
block
|
||||||
|
With expr
|
||||||
|
|
||||||
|
entry_decl ::=
|
||||||
|
Entrypoint Ident entry_params COLON type_expr Is
|
||||||
|
seq(local_decl)
|
||||||
|
block
|
||||||
|
With expr
|
||||||
|
|
||||||
|
entry_params ::=
|
||||||
|
par(nsepseq(entry_param_decl,SEMI))
|
||||||
|
|
||||||
|
proc_decl ::=
|
||||||
|
Procedure Ident parameters Is
|
||||||
|
seq(local_decl)
|
||||||
|
block
|
||||||
|
|
||||||
|
parameters ::=
|
||||||
|
par(nsepseq(param_decl,SEMI))
|
||||||
|
|
||||||
|
param_decl ::=
|
||||||
|
Var Ident COLON param_type
|
||||||
|
| Const Ident COLON param_type
|
||||||
|
|
||||||
|
entry_param_decl ::=
|
||||||
|
param_decl
|
||||||
|
| Storage Ident COLON param_type
|
||||||
|
|
||||||
|
param_type ::=
|
||||||
|
cartesian
|
||||||
|
|
||||||
|
block ::=
|
||||||
|
Begin series(statement,SEMI,End)
|
||||||
|
| Block LBRACE series(statement,SEMI,RBRACE)
|
||||||
|
|
||||||
|
statement ::=
|
||||||
|
instruction
|
||||||
|
| data_decl
|
||||||
|
|
||||||
|
data_decl ::=
|
||||||
|
const_decl
|
||||||
|
| var_decl
|
||||||
|
|
||||||
|
const_decl ::=
|
||||||
|
Const unqualified_decl(EQUAL)
|
||||||
|
|
||||||
|
var_decl ::=
|
||||||
|
Var unqualified_decl(ASS)
|
||||||
|
|
||||||
|
local_decl ::=
|
||||||
|
fun_decl option(SEMI)
|
||||||
|
| proc_decl option(SEMI)
|
||||||
|
| data_decl option(SEMI)
|
||||||
|
|
||||||
|
unqualified_decl(op) ::=
|
||||||
|
Ident (* var *) COLON type_expr op expr
|
||||||
|
|
||||||
|
instruction ::=
|
||||||
|
block
|
||||||
|
| If expr Then if_clause option(SEMI) Else if_clause
|
||||||
|
| case(instruction)
|
||||||
|
| Ident instruction_1
|
||||||
|
| loop
|
||||||
|
| Fail expr
|
||||||
|
| Skip
|
||||||
|
| Patch path With structure
|
||||||
|
| Remove expr From remove_suffix
|
||||||
|
|
||||||
|
remove_suffix ::=
|
||||||
|
Map path
|
||||||
|
| Set path
|
||||||
|
|
||||||
|
instruction_1 ::=
|
||||||
|
arguments
|
||||||
|
| ASS expr
|
||||||
|
| brackets(expr) ASS expr
|
||||||
|
| selections option(brackets(expr)) ASS expr
|
||||||
|
|
||||||
|
path ::=
|
||||||
|
Ident option(selections)
|
||||||
|
|
||||||
|
selections ::=
|
||||||
|
DOT nsepseq(selection,DOT)
|
||||||
|
|
||||||
|
injection(Kind,element) ::=
|
||||||
|
Kind inj_sufffix(element)
|
||||||
|
|
||||||
|
inj_suffix(element) ::=
|
||||||
|
series(element,SEMI,End)
|
||||||
|
| End
|
||||||
|
| LBRACKET bracketed(element)
|
||||||
|
|
||||||
|
bracketed(element) ::=
|
||||||
|
series(element,SEMI,RBRACKET)
|
||||||
|
| RBRACKET
|
||||||
|
|
||||||
|
binding ::=
|
||||||
|
expr ARROW expr
|
||||||
|
|
||||||
|
if_clause ::=
|
||||||
|
instruction
|
||||||
|
| LBRACE series(statement,COMMA,RBRACE)
|
||||||
|
|
||||||
|
case(rhs) ::=
|
||||||
|
Case expr Of case_suffix(rhs)
|
||||||
|
|
||||||
|
case_suffix(rhs) ::=
|
||||||
|
cases(rhs) End
|
||||||
|
| LBRACKET cases(rhs) RBRACKET
|
||||||
|
|
||||||
|
cases(rhs) ::=
|
||||||
|
nsepseq(case_clause(rhs),VBAR)
|
||||||
|
| VBAR nsepseq(case_clause(rhs),VBAR)
|
||||||
|
|
||||||
|
case_clause(rhs) ::=
|
||||||
|
pattern ARROW rhs
|
||||||
|
|
||||||
|
loop ::=
|
||||||
|
While expr block
|
||||||
|
| For Ident for_suffix
|
||||||
|
|
||||||
|
for_suffix ::=
|
||||||
|
ASS expr option(Down) To expr option(step_clause) block
|
||||||
|
| In expr block
|
||||||
|
| ARROW Ident In expr block
|
||||||
|
|
||||||
|
step_clause ::=
|
||||||
|
Step expr
|
||||||
|
|
||||||
|
(* Expressions *)
|
||||||
|
|
||||||
|
interactive_expr ::=
|
||||||
|
expr EOF
|
||||||
|
|
||||||
|
expr ::=
|
||||||
|
case(expr)
|
||||||
|
| disj_expr
|
||||||
|
|
||||||
|
disj_expr ::=
|
||||||
|
left_assoc(conj_expr,Or)
|
||||||
|
|
||||||
|
conj_expr ::=
|
||||||
|
left_assoc(set_membership,And)
|
||||||
|
|
||||||
|
set_membership ::=
|
||||||
|
core_expr Contains set_membership
|
||||||
|
| comp_expr
|
||||||
|
|
||||||
|
comp_expr ::=
|
||||||
|
left_assoc(cat_expr,op_comp)
|
||||||
|
|
||||||
|
op_comp ::=
|
||||||
|
LT | LEQ | GT | GEQ | EQUAL | NEQ
|
||||||
|
|
||||||
|
cat_expr ::=
|
||||||
|
right_assoc(cons_expr,CAT)
|
||||||
|
|
||||||
|
cons_expr ::=
|
||||||
|
left_assoc(add_expr,CONS)
|
||||||
|
|
||||||
|
add_expr ::=
|
||||||
|
left_assoc(mult_expr,add_op)
|
||||||
|
|
||||||
|
add_op ::=
|
||||||
|
PLUS | MINUS
|
||||||
|
|
||||||
|
mult_expr ::=
|
||||||
|
left_assoc(unary_expr,mult_op)
|
||||||
|
|
||||||
|
mult_op ::=
|
||||||
|
TIMES | SLASH | Mod
|
||||||
|
|
||||||
|
unary_expr ::=
|
||||||
|
MINUS core_expr
|
||||||
|
| Not core_expr
|
||||||
|
| core_expr
|
||||||
|
|
||||||
|
core_expr ::=
|
||||||
|
Int
|
||||||
|
| Nat
|
||||||
|
| Mtz
|
||||||
|
| Ident option(core_suffix)
|
||||||
|
| String
|
||||||
|
| Bytes
|
||||||
|
| C_False
|
||||||
|
| C_True
|
||||||
|
| C_Unit
|
||||||
|
| C_None
|
||||||
|
| C_Some arguments
|
||||||
|
| Constr option(arguments)
|
||||||
|
| par(paren_expr)
|
||||||
|
| injection(List,expr)
|
||||||
|
| Nil
|
||||||
|
| structure
|
||||||
|
|
||||||
|
core_suffix ::=
|
||||||
|
brackets(expr) (* lookup *)
|
||||||
|
| DOT nsepseq(selection,DOT) option(brackets(expr))
|
||||||
|
| arguments
|
||||||
|
|
||||||
|
paren_expr ::=
|
||||||
|
disj_expr option(paren_expr_1)
|
||||||
|
| case(expr) option(paren_expr_2)
|
||||||
|
|
||||||
|
paren_expr_1 ::=
|
||||||
|
COLON type_expr
|
||||||
|
| COMMA nsepseq(expr,COMMA)
|
||||||
|
|
||||||
|
paren_expr_2 ::=
|
||||||
|
COMMA nsepseq(expr,COMMA)
|
||||||
|
|
||||||
|
structure ::=
|
||||||
|
injection(Map,binding)
|
||||||
|
| injection(Set,expr)
|
||||||
|
| record_expr
|
||||||
|
|
||||||
|
selection ::=
|
||||||
|
Ident (* field_name *)
|
||||||
|
| Int
|
||||||
|
|
||||||
|
record_expr ::=
|
||||||
|
Record record_expr_suffix
|
||||||
|
|
||||||
|
record_expr_suffix ::=
|
||||||
|
series(field_assignment,SEMI,End)
|
||||||
|
| LBRACKET series(field_assignment,SEMI,RBRACKET)
|
||||||
|
|
||||||
|
field_assignment ::=
|
||||||
|
Ident (* field_name *) EQUAL expr
|
||||||
|
|
||||||
|
arguments ::=
|
||||||
|
par(nsepseq(expr,COMMA))
|
||||||
|
|
||||||
|
(* Patterns *)
|
||||||
|
|
||||||
|
pattern ::=
|
||||||
|
nsepseq(core_pattern,CONS)
|
||||||
|
|
||||||
|
core_pattern ::=
|
||||||
|
Ident (* var *)
|
||||||
|
| WILD
|
||||||
|
| Int
|
||||||
|
| String
|
||||||
|
| C_Unit
|
||||||
|
| C_False
|
||||||
|
| C_True
|
||||||
|
| C_None
|
||||||
|
| C_Some par(core_pattern)
|
||||||
|
| Constr option(tuple_pattern)
|
||||||
|
| injection(List,core_pattern)
|
||||||
|
| Nil
|
||||||
|
| par(option(paren_pattern))
|
||||||
|
|
||||||
|
paren_pattern ::=
|
||||||
|
core_pattern paren_pattern_suffix
|
||||||
|
|
||||||
|
paren_pattern_suffix ::=
|
||||||
|
CONS pattern
|
||||||
|
| COMMA nsepseq(core_pattern,COMMA)
|
||||||
|
|
||||||
|
tuple_pattern ::=
|
||||||
|
par(nsepseq(core_pattern,COMMA))
|
||||||
433
src/parser/pascaligo/Doc/pascaligo_22.bnf
Normal file
433
src/parser/pascaligo/Doc/pascaligo_22.bnf
Normal file
@ -0,0 +1,433 @@
|
|||||||
|
right_assoc(item,op) ::=
|
||||||
|
item
|
||||||
|
| item op right_assoc(item,op)
|
||||||
|
|
||||||
|
left_assoc(item,op) ::=
|
||||||
|
right_assoc(item,op)
|
||||||
|
|
||||||
|
option(item) :=
|
||||||
|
(**)
|
||||||
|
| item
|
||||||
|
|
||||||
|
series(item,sep,term) ::=
|
||||||
|
item after_item(item,sep,term)
|
||||||
|
|
||||||
|
after_item(item,sep,term) ::=
|
||||||
|
sep item_or_closing(item,sep,term)
|
||||||
|
| term
|
||||||
|
|
||||||
|
item_or_closing(item,sep,term) ::=
|
||||||
|
term
|
||||||
|
| series(item,sep,term)
|
||||||
|
|
||||||
|
(* Compound constructs *)
|
||||||
|
|
||||||
|
par(item) ::=
|
||||||
|
LPAR item RPAR
|
||||||
|
|
||||||
|
brackets(item) ::=
|
||||||
|
LBRACKET item RBRACKET
|
||||||
|
|
||||||
|
(* Sequences *)
|
||||||
|
|
||||||
|
(* Possibly empty sequence of items
|
||||||
|
|
||||||
|
LL(1) constraint: item not in Follow(seq), where
|
||||||
|
Follow(seq) = Follow(nseq) = {EOF, Begin, Block}
|
||||||
|
*)
|
||||||
|
|
||||||
|
seq(item) ::=
|
||||||
|
option(nseq(item))
|
||||||
|
|
||||||
|
(* Non-empty sequence of items *)
|
||||||
|
|
||||||
|
nseq(item) ::=
|
||||||
|
item seq(item)
|
||||||
|
|
||||||
|
(* Non-empty separated sequence of items *)
|
||||||
|
|
||||||
|
nsepseq(item,Sep) ::=
|
||||||
|
item
|
||||||
|
| item Sep nsepseq(item,Sep)
|
||||||
|
|
||||||
|
(* Main *)
|
||||||
|
|
||||||
|
contract ::=
|
||||||
|
nseq(declaration) EOF
|
||||||
|
|
||||||
|
(* LL(1) constraint: SEMI not in Follow(declaration), where
|
||||||
|
Follow(declaration)
|
||||||
|
= {EOF} U First(declaration)
|
||||||
|
= {EOF} U First(type_decl)
|
||||||
|
U First(const_decl) U First(lambda_decl)
|
||||||
|
= {EOF} U {Type} U {Const} U First(fun_decl)
|
||||||
|
U First(proc_decl) U First(entry_decl)
|
||||||
|
= {EOF,Type,Const,Function,Procedure,Entrypoint}.
|
||||||
|
*)
|
||||||
|
|
||||||
|
declaration ::=
|
||||||
|
type_decl option(SEMI)
|
||||||
|
| const_decl option(SEMI)
|
||||||
|
| lambda_decl option(SEMI)
|
||||||
|
|
||||||
|
(* Type declarations *)
|
||||||
|
|
||||||
|
type_decl ::=
|
||||||
|
Type Ident Is type_expr
|
||||||
|
|
||||||
|
type_expr ::=
|
||||||
|
cartesian
|
||||||
|
| nsepseq(variant,VBAR)
|
||||||
|
| VBAR nsepseq(variant,VBAR)
|
||||||
|
| Record record_type_expr
|
||||||
|
|
||||||
|
record_type_expr ::=
|
||||||
|
series(field_decl,SEMI,End)
|
||||||
|
| LBRACKET series(field_decl,SEMI,RBRACKET)
|
||||||
|
|
||||||
|
(* LL(1) constraint: Of not in Follow(variant).
|
||||||
|
"Of" only occurs after {Constr, expr}. *)
|
||||||
|
|
||||||
|
variant ::=
|
||||||
|
Constr option(of_cartesian)
|
||||||
|
|
||||||
|
of_cartesian ::=
|
||||||
|
Of cartesian
|
||||||
|
|
||||||
|
cartesian ::=
|
||||||
|
nsepseq(function_type,TIMES)
|
||||||
|
|
||||||
|
function_type ::=
|
||||||
|
right_assoc(core_type,ARROW)
|
||||||
|
|
||||||
|
(* LL(1) constraint: LPAR not in Follow(core_type), where
|
||||||
|
Follow(core_type)
|
||||||
|
= {ARROW} U Follow(function_type)
|
||||||
|
= {ARROW} U {TIMES} U Follow(cartesian)
|
||||||
|
= {ARROW,TIMES} U Follow(of_cartesian) U Follow(type_expr)
|
||||||
|
U Follow(param_type)
|
||||||
|
= {ARROW,TIMES} U Follow(variant)
|
||||||
|
U {RPAR,COMMA,Is,EQUAL,ASS} U Follow(field_decl)
|
||||||
|
U Follow(paren_expr_1) U Follow(type_decl)
|
||||||
|
U Follow(param_decl) U Follow(entry_param_decl)
|
||||||
|
= {ARROW,TIMES,RPAR,COMMA,Is,EQUAL,ASS,VBAR,
|
||||||
|
SEMI,End,RBRACKET} U Follow(paren_expr)
|
||||||
|
U {SEMI} U Follow(declaration)
|
||||||
|
= {ARROW,TIMES,RPAR,COMMA,Is,EQUAL,ASS,VBAR,
|
||||||
|
SEMI,End,RBRACKET,EOF,Type,Const,
|
||||||
|
Function,Procedure,Entrypoint}.
|
||||||
|
*)
|
||||||
|
|
||||||
|
core_type ::=
|
||||||
|
Ident (* type_name *) option(type_tuple)
|
||||||
|
| Map type_tuple
|
||||||
|
| Set par(type_expr)
|
||||||
|
| List par(type_expr)
|
||||||
|
| par(type_expr)
|
||||||
|
|
||||||
|
type_tuple ::=
|
||||||
|
par(nsepseq(type_expr,COMMA))
|
||||||
|
|
||||||
|
field_decl ::=
|
||||||
|
Ident (* field_name *) COLON type_expr
|
||||||
|
|
||||||
|
(* Function and procedure declarations *)
|
||||||
|
|
||||||
|
lambda_decl ::=
|
||||||
|
fun_decl
|
||||||
|
| proc_decl
|
||||||
|
| entry_decl
|
||||||
|
|
||||||
|
fun_decl ::=
|
||||||
|
Function Ident parameters COLON type_expr Is
|
||||||
|
seq(local_decl)
|
||||||
|
block
|
||||||
|
With expr
|
||||||
|
|
||||||
|
entry_decl ::=
|
||||||
|
Entrypoint Ident entry_params COLON type_expr Is
|
||||||
|
seq(local_decl)
|
||||||
|
block
|
||||||
|
With expr
|
||||||
|
|
||||||
|
entry_params ::=
|
||||||
|
par(nsepseq(entry_param_decl,SEMI))
|
||||||
|
|
||||||
|
proc_decl ::=
|
||||||
|
Procedure Ident parameters Is
|
||||||
|
seq(local_decl)
|
||||||
|
block
|
||||||
|
|
||||||
|
parameters ::=
|
||||||
|
par(nsepseq(param_decl,SEMI))
|
||||||
|
|
||||||
|
param_decl ::=
|
||||||
|
Var Ident COLON param_type
|
||||||
|
| Const Ident COLON param_type
|
||||||
|
|
||||||
|
entry_param_decl ::=
|
||||||
|
param_decl
|
||||||
|
| Storage Ident COLON param_type
|
||||||
|
|
||||||
|
param_type ::=
|
||||||
|
cartesian
|
||||||
|
|
||||||
|
block ::=
|
||||||
|
Begin series(statement,SEMI,End)
|
||||||
|
| Block LBRACE series(statement,SEMI,RBRACE)
|
||||||
|
|
||||||
|
statement ::=
|
||||||
|
instruction
|
||||||
|
| data_decl
|
||||||
|
|
||||||
|
data_decl ::=
|
||||||
|
const_decl
|
||||||
|
| var_decl
|
||||||
|
|
||||||
|
const_decl ::=
|
||||||
|
Const unqualified_decl(EQUAL)
|
||||||
|
|
||||||
|
var_decl ::=
|
||||||
|
Var unqualified_decl(ASS)
|
||||||
|
|
||||||
|
(* LL(1) constraint: SEMI not in Follow(local_decl), where
|
||||||
|
Follow(local_decl)
|
||||||
|
= First(local_decl) U First(block)
|
||||||
|
= First(fun_decl) U First(proc_decl) U First(data_decl)
|
||||||
|
U {BEGIN,Block}
|
||||||
|
= {Function,Procedure,BEGIN,Block} U First(const_decl)
|
||||||
|
U First(var_decl)
|
||||||
|
= {Function,Procedure,BEGIN,Block,Const,Var}.
|
||||||
|
*)
|
||||||
|
|
||||||
|
local_decl ::=
|
||||||
|
fun_decl option(SEMI)
|
||||||
|
| proc_decl option(SEMI)
|
||||||
|
| data_decl option(SEMI)
|
||||||
|
|
||||||
|
unqualified_decl(op) ::=
|
||||||
|
Ident (* var *) COLON type_expr op expr
|
||||||
|
|
||||||
|
instruction ::=
|
||||||
|
block
|
||||||
|
| If expr Then if_clause option(SEMI) Else if_clause
|
||||||
|
| case(instruction)
|
||||||
|
| Ident instruction_1
|
||||||
|
| loop
|
||||||
|
| Fail expr
|
||||||
|
| Skip
|
||||||
|
| Patch path With structure
|
||||||
|
| Remove expr From remove_suffix
|
||||||
|
|
||||||
|
remove_suffix ::=
|
||||||
|
Map path
|
||||||
|
| Set path
|
||||||
|
|
||||||
|
instruction_1 ::=
|
||||||
|
arguments
|
||||||
|
| ASS expr
|
||||||
|
| brackets(expr) ASS expr
|
||||||
|
| selections option(brackets(expr)) ASS expr
|
||||||
|
|
||||||
|
(* LL(1) constraint: First(selections) not in Follow(path), where
|
||||||
|
First(selections) = {DOT} and
|
||||||
|
Follow(path)
|
||||||
|
= {With} U Follow(remove_suffix)
|
||||||
|
= {With} U Follow(instruction)
|
||||||
|
= {With} U Follow(statement) U Follow(if_clause)
|
||||||
|
U Follow(case_clause(instruction))
|
||||||
|
= {With,SEMI,End,Else,VBAR} U Follow(cases(instruction))
|
||||||
|
= {With,SEMI,End,Else,VBAR,RBRACKET}.
|
||||||
|
*)
|
||||||
|
|
||||||
|
path ::=
|
||||||
|
Ident option(selections)
|
||||||
|
|
||||||
|
selections ::=
|
||||||
|
DOT nsepseq(selection,DOT)
|
||||||
|
|
||||||
|
injection(Kind,element) ::=
|
||||||
|
Kind inj_sufffix(element)
|
||||||
|
|
||||||
|
inj_suffix(element) ::=
|
||||||
|
series(element,SEMI,End)
|
||||||
|
| End
|
||||||
|
| LBRACKET bracketed(element)
|
||||||
|
|
||||||
|
bracketed(element) ::=
|
||||||
|
series(element,SEMI,RBRACKET)
|
||||||
|
| RBRACKET
|
||||||
|
|
||||||
|
binding ::=
|
||||||
|
expr ARROW expr
|
||||||
|
|
||||||
|
if_clause ::=
|
||||||
|
instruction
|
||||||
|
| LBRACE series(statement,COMMA,RBRACE)
|
||||||
|
|
||||||
|
case(rhs) ::=
|
||||||
|
Case expr Of case_suffix(rhs)
|
||||||
|
|
||||||
|
case_suffix(rhs) ::=
|
||||||
|
cases(rhs) End
|
||||||
|
| LBRACKET cases(rhs) RBRACKET
|
||||||
|
|
||||||
|
cases(rhs) ::=
|
||||||
|
nsepseq(case_clause(rhs),VBAR)
|
||||||
|
| VBAR nsepseq(case_clause(rhs),VBAR)
|
||||||
|
|
||||||
|
case_clause(rhs) ::=
|
||||||
|
pattern ARROW rhs
|
||||||
|
|
||||||
|
loop ::=
|
||||||
|
While expr block
|
||||||
|
| For Ident for_suffix
|
||||||
|
|
||||||
|
for_suffix ::=
|
||||||
|
ASS expr option(Down) To expr option(step_clause) block
|
||||||
|
| In expr block
|
||||||
|
| ARROW Ident In expr block
|
||||||
|
|
||||||
|
step_clause ::=
|
||||||
|
Step expr
|
||||||
|
|
||||||
|
(* Expressions *)
|
||||||
|
|
||||||
|
interactive_expr ::=
|
||||||
|
expr EOF
|
||||||
|
|
||||||
|
expr ::=
|
||||||
|
case(expr)
|
||||||
|
| disj_expr
|
||||||
|
|
||||||
|
disj_expr ::=
|
||||||
|
left_assoc(conj_expr,Or)
|
||||||
|
|
||||||
|
conj_expr ::=
|
||||||
|
left_assoc(set_membership,And)
|
||||||
|
|
||||||
|
set_membership ::=
|
||||||
|
comp_expr option(contains_clause) (* Enlarged the language *)
|
||||||
|
|
||||||
|
contains_clause ::=
|
||||||
|
Contains set_membership
|
||||||
|
|
||||||
|
comp_expr ::=
|
||||||
|
left_assoc(cat_expr,op_comp)
|
||||||
|
|
||||||
|
op_comp ::=
|
||||||
|
LT | LEQ | GT | GEQ | EQUAL | NEQ
|
||||||
|
|
||||||
|
cat_expr ::=
|
||||||
|
right_assoc(cons_expr,CAT)
|
||||||
|
|
||||||
|
cons_expr ::=
|
||||||
|
left_assoc(add_expr,CONS)
|
||||||
|
|
||||||
|
add_expr ::=
|
||||||
|
left_assoc(mult_expr,add_op)
|
||||||
|
|
||||||
|
add_op ::=
|
||||||
|
PLUS | MINUS
|
||||||
|
|
||||||
|
mult_expr ::=
|
||||||
|
left_assoc(unary_expr,mult_op)
|
||||||
|
|
||||||
|
mult_op ::=
|
||||||
|
TIMES | SLASH | Mod
|
||||||
|
|
||||||
|
unary_expr ::=
|
||||||
|
MINUS core_expr
|
||||||
|
| Not core_expr
|
||||||
|
| core_expr
|
||||||
|
|
||||||
|
(* LL(1) constraint: First(core_suffix) not in Follow(core_expr)
|
||||||
|
First(core_suffix) =
|
||||||
|
|
||||||
|
XXX
|
||||||
|
*)
|
||||||
|
core_expr ::=
|
||||||
|
Int
|
||||||
|
| Nat
|
||||||
|
| Mtz
|
||||||
|
| Ident option(core_suffix)
|
||||||
|
| String
|
||||||
|
| Bytes
|
||||||
|
| C_False
|
||||||
|
| C_True
|
||||||
|
| C_Unit
|
||||||
|
| C_None
|
||||||
|
| C_Some arguments
|
||||||
|
| Constr option(arguments)
|
||||||
|
| par(paren_expr)
|
||||||
|
| injection(List,expr)
|
||||||
|
| Nil
|
||||||
|
| structure
|
||||||
|
|
||||||
|
core_suffix ::=
|
||||||
|
brackets(expr) (* lookup *)
|
||||||
|
| DOT nsepseq(selection,DOT) option(brackets(expr))
|
||||||
|
| arguments
|
||||||
|
|
||||||
|
paren_expr ::=
|
||||||
|
disj_expr option(paren_expr_1)
|
||||||
|
| case(expr) option(paren_expr_2)
|
||||||
|
|
||||||
|
paren_expr_1 ::=
|
||||||
|
COLON type_expr
|
||||||
|
| COMMA nsepseq(expr,COMMA)
|
||||||
|
|
||||||
|
paren_expr_2 ::=
|
||||||
|
COMMA nsepseq(expr,COMMA)
|
||||||
|
|
||||||
|
structure ::=
|
||||||
|
injection(Map,binding)
|
||||||
|
| injection(Set,expr)
|
||||||
|
| record_expr
|
||||||
|
|
||||||
|
selection ::=
|
||||||
|
Ident (* field_name *)
|
||||||
|
| Int
|
||||||
|
|
||||||
|
record_expr ::=
|
||||||
|
Record record_expr_suffix
|
||||||
|
|
||||||
|
record_expr_suffix ::=
|
||||||
|
series(field_assignment,SEMI,End)
|
||||||
|
| LBRACKET series(field_assignment,SEMI,RBRACKET)
|
||||||
|
|
||||||
|
field_assignment ::=
|
||||||
|
Ident (* field_name *) EQUAL expr
|
||||||
|
|
||||||
|
arguments ::=
|
||||||
|
par(nsepseq(expr,COMMA))
|
||||||
|
|
||||||
|
(* Patterns *)
|
||||||
|
|
||||||
|
pattern ::=
|
||||||
|
nsepseq(core_pattern,CONS)
|
||||||
|
|
||||||
|
core_pattern ::=
|
||||||
|
Ident (* var *)
|
||||||
|
| WILD
|
||||||
|
| Int
|
||||||
|
| String
|
||||||
|
| C_Unit
|
||||||
|
| C_False
|
||||||
|
| C_True
|
||||||
|
| C_None
|
||||||
|
| C_Some par(core_pattern)
|
||||||
|
| Constr option(tuple_pattern)
|
||||||
|
| injection(List,core_pattern)
|
||||||
|
| Nil
|
||||||
|
| par(option(paren_pattern))
|
||||||
|
|
||||||
|
paren_pattern ::=
|
||||||
|
core_pattern paren_pattern_suffix
|
||||||
|
|
||||||
|
paren_pattern_suffix ::=
|
||||||
|
CONS pattern
|
||||||
|
| COMMA nsepseq(core_pattern,COMMA)
|
||||||
|
|
||||||
|
tuple_pattern ::=
|
||||||
|
par(nsepseq(core_pattern,COMMA))
|
||||||
Loading…
Reference in New Issue
Block a user