Merge branch 'rinderknecht-dev' into 'dev'

Fixing scanning of integers, removing keywords `storage` and `entrypoint` from PascaLIGO

See merge request ligolang/ligo!94
This commit is contained in:
Sander 2019-09-27 15:47:56 +00:00
commit 210bd665c0
42 changed files with 5885 additions and 520 deletions

View File

@ -0,0 +1,20 @@
type storage = int
(* variant defining pseudo multi-entrypoint actions *)
type action =
| Increment of int
| Decrement of int
let add (a : int) (b : int) : int = a + b
let subtract (a : int) (b : int) : int = a - b
(* real entrypoint that re-routes the flow based on the action provided *)
let%entry main (p : action) storage =
let storage =
match p with
| Increment n -> add s n
| Decrement n -> subtract s n
in ([] : operation list), storage

View File

@ -0,0 +1,2 @@
ocamldep: -pp camlp5o
ocamlc: -pp camlp5o

View File

@ -17,5 +17,4 @@ $HOME/git/ligo/src/parser/shared/Markup.ml
$HOME/git/ligo/src/parser/shared/Markup.mli
$HOME/git/ligo/src/parser/shared/Utils.mli
$HOME/git/ligo/src/parser/shared/Utils.ml
$HOME/git/ligo/src/parser/shared/Version.ml
Stubs/Simple_utils.ml

View File

@ -49,7 +49,6 @@ type kwd_contains = Region.t
type kwd_down = Region.t
type kwd_else = Region.t
type kwd_end = Region.t
type kwd_entrypoint = Region.t
type kwd_for = Region.t
type kwd_from = Region.t
type kwd_function = Region.t
@ -70,7 +69,6 @@ type kwd_remove = Region.t
type kwd_set = Region.t
type kwd_skip = Region.t
type kwd_step = Region.t
type kwd_storage = Region.t
type kwd_then = Region.t
type kwd_to = Region.t
type kwd_type = Region.t
@ -218,7 +216,6 @@ and type_tuple = (type_expr, comma) nsepseq par reg
and lambda_decl =
FunDecl of fun_decl reg
| ProcDecl of proc_decl reg
| EntryDecl of entry_decl reg
and fun_decl = {
kwd_function : kwd_function;
@ -244,36 +241,8 @@ and proc_decl = {
terminator : semi option
}
and entry_decl = {
kwd_entrypoint : kwd_entrypoint;
name : variable;
param : entry_params;
colon : colon;
ret_type : type_expr;
kwd_is : kwd_is;
local_decls : local_decl list;
block : block reg;
kwd_with : kwd_with;
return : expr;
terminator : semi option
}
and parameters = (param_decl, semi) nsepseq par reg
and entry_params = (entry_param_decl, semi) nsepseq par reg
and entry_param_decl =
EntryConst of param_const reg
| EntryVar of param_var reg
| EntryStore of storage reg
and storage = {
kwd_storage : kwd_storage;
var : variable;
colon : colon;
storage_type : type_expr
}
and param_decl =
ParamConst of param_const reg
| ParamVar of param_var reg

View File

@ -33,7 +33,6 @@ type kwd_contains = Region.t
type kwd_down = Region.t
type kwd_else = Region.t
type kwd_end = Region.t
type kwd_entrypoint = Region.t
type kwd_for = Region.t
type kwd_from = Region.t
type kwd_function = Region.t
@ -54,7 +53,6 @@ type kwd_remove = Region.t
type kwd_set = Region.t
type kwd_skip = Region.t
type kwd_step = Region.t
type kwd_storage = Region.t
type kwd_then = Region.t
type kwd_to = Region.t
type kwd_type = Region.t
@ -202,7 +200,6 @@ and type_tuple = (type_expr, comma) nsepseq par reg
and lambda_decl =
FunDecl of fun_decl reg
| ProcDecl of proc_decl reg
| EntryDecl of entry_decl reg
and fun_decl = {
kwd_function : kwd_function;
@ -228,36 +225,8 @@ and proc_decl = {
terminator : semi option
}
and entry_decl = {
kwd_entrypoint : kwd_entrypoint;
name : variable;
param : entry_params;
colon : colon;
ret_type : type_expr;
kwd_is : kwd_is;
local_decls : local_decl list;
block : block reg;
kwd_with : kwd_with;
return : expr;
terminator : semi option
}
and parameters = (param_decl, semi) nsepseq par reg
and entry_params = (entry_param_decl, semi) nsepseq par reg
and entry_param_decl =
EntryConst of param_const reg
| EntryVar of param_var reg
| EntryStore of storage reg
and storage = {
kwd_storage : kwd_storage;
var : variable;
colon : colon;
storage_type : type_expr
}
and param_decl =
ParamConst of param_const reg
| ParamVar of param_var reg

View File

@ -0,0 +1,27 @@
(* The rule [series(Item,TERM)] parses a non-empty list of [Item]
separated by semicolons and optionally terminated by a semicolon,
then the terminal TERM. *)
series(Item,TERM):
Item after_item(Item,TERM) { $1,$2 }
after_item(Item,TERM):
SEMI item_or_closing(Item,TERM) {
match $2 with
`Some (item, items, term, closing) ->
($1, item)::items, term, closing
| `Closing closing ->
[], Some $1, closing
}
| TERM {
[], None, $1
}
item_or_closing(Item,TERM):
TERM {
`Closing $1
}
| series(Item,TERM) {
let item, (items, term, closing) = $1
in `Some (item, items, term, closing)
}

File diff suppressed because it is too large Load Diff

View File

@ -136,15 +136,15 @@ the latter can be reassigned. The syntax is slightly different for
both. For example, the variables "x" and "y" above could have been
declared as follows:
var x : nat := 0;
var y : nat := 0;
var x : nat := 0n;
var y : nat := 0n;
It is possible to specify that the value of a variable will not change
(the name "variable" is misleading in that context), that is, they
remain constant:
const ten : nat = 10;
const eleven : nat = ten + 1;
const ten : nat = 10n;
const eleven : nat = ten + 1n;
Similarly, function declarations have their parameters and return
value annotated with their types. For instance,
@ -160,10 +160,10 @@ the result of calling the function is given after the keyword "with".
A another example would be
function factorial (const n : nat) : nat is
var m : nat := 0;
var f : nat := 1;
var m : nat := 0n;
var f : nat := 1n;
begin
if n <= 0 then f := 1
if n <= 0n then f := 1n
else
for m := 1 to n
begin

View File

@ -1,6 +1,6 @@
option(X) :=
option(item) :=
(**)
| X
| item
sep_or_term_list(item,sep) ::=
nsepseq(item,sep)
@ -8,34 +8,34 @@ sep_or_term_list(item,sep) ::=
(* Compound constructs *)
par(X) ::= LPAR X RPAR
par(item) ::=
LPAR item RPAR
brackets(X) ::= LBRACKET X RBRACKET
brackets(item) ::=
LBRACKET item RBRACKET
(* Sequences *)
(* Possibly empty sequence of items *)
seq(X) ::=
(**)
| X seq(X)
seq(item) ::=
option(nseq(item))
(* Non-empty sequence of items *)
nseq(X) ::= X seq(X)
nseq(item) ::=
item seq(item)
(* Non-empty separated sequence of items *)
nsepseq(X,Sep) ::=
X
| X Sep nsepseq(X,Sep)
nsepseq(item,Sep) ::=
item
| item Sep nsepseq(item,Sep)
(* Possibly empy separated sequence of items *)
sepseq(X,Sep) ::=
(**)
| nsepseq(X,Sep)
(* Possibly empty separated sequence of items *)
sepseq(item,Sep) ::=
option(nsepseq(item,Sep))
(* Inlines *)
@ -281,10 +281,6 @@ interactive_expr ::=
expr ::=
case(expr)
| annot_expr
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
| disj_expr
disj_expr ::=
@ -342,6 +338,7 @@ core_expr ::=
| C_False
| C_True
| C_Unit
| annot_expr
| tuple_expr
| list_expr
| C_None
@ -354,6 +351,9 @@ core_expr ::=
| Constr
| C_Some arguments
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
set_expr ::=
injection(Set,expr)

View File

@ -1,6 +1,6 @@
option(X) :=
option(item) :=
(**)
| X
| item
series(item,sep,term) ::=
item after_item(item,sep,term)
@ -15,34 +15,34 @@ item_or_closing(item,sep,term) ::=
(* Compound constructs *)
par(X) ::= LPAR X RPAR
par(item) ::=
LPAR item RPAR
brackets(X) ::= LBRACKET X RBRACKET
brackets(item) ::=
LBRACKET item RBRACKET
(* Sequences *)
(* Possibly empty sequence of items *)
seq(X) ::=
(**)
| X seq(X)
seq(item) ::=
option(nseq(item))
(* Non-empty sequence of items *)
nseq(X) ::= X seq(X)
nseq(item) ::=
item seq(item)
(* Non-empty separated sequence of items *)
nsepseq(X,Sep) ::=
X
| X Sep nsepseq(X,Sep)
nsepseq(item,Sep) ::=
item
| item Sep nsepseq(item,Sep)
(* Possibly empy separated sequence of items *)
sepseq(X,Sep) ::=
(**)
| nsepseq(X,Sep)
(* Possibly empty separated sequence of items *)
sepseq(item,Sep) ::=
option(nsepseq(item,Sep))
(* Inlines *)
@ -287,10 +287,6 @@ interactive_expr ::=
expr ::=
case(expr)
| annot_expr
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
| disj_expr
disj_expr ::=
@ -348,6 +344,7 @@ core_expr ::=
| C_False
| C_True
| C_Unit
| annot_expr
| tuple_expr
| list_expr
| C_None
@ -360,6 +357,9 @@ core_expr ::=
| Constr
| C_Some arguments
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
set_expr ::=
injection(Set,expr)

View File

@ -1,6 +1,6 @@
option(X) :=
option(item) :=
(**)
| X
| item
series(item,sep,term) ::=
item after_item(item,sep,term)
@ -15,33 +15,34 @@ item_or_closing(item,sep,term) ::=
(* Compound constructs *)
par(X) ::= LPAR X RPAR
par(item) ::=
LPAR item RPAR
brackets(X) ::= LBRACKET X RBRACKET
brackets(item) ::=
LBRACKET item RBRACKET
(* Sequences *)
(* Possibly empty sequence of items *)
seq(X) ::=
(**)
| X seq(X)
seq(item) ::=
option(nseq(item))
(* Non-empty sequence of items *)
nseq(X) ::= X seq(X)
nseq(item) ::=
item seq(item)
(* Non-empty separated sequence of items *)
nsepseq(X,Sep) ::=
X
| X Sep nsepseq(X,Sep)
nsepseq(item,Sep) ::=
item
| item Sep nsepseq(item,Sep)
(* Possibly empy separated sequence of items *)
(* Possibly empty separated sequence of items *)
sepseq(X,Sep) ::=
(**)
| nsepseq(X,Sep)
sepseq(item,Sep) ::=
option(nsepseq(item,Sep))
(* Main *)
@ -266,10 +267,6 @@ interactive_expr ::=
expr ::=
case(expr)
| annot_expr
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
| disj_expr
disj_expr ::=
@ -327,6 +324,7 @@ core_expr ::=
| C_False
| C_True
| C_Unit
| annot_expr
| tuple_expr
| list_expr
| C_None
@ -339,6 +337,9 @@ core_expr ::=
| Constr
| C_Some arguments
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
set_expr ::=
injection(Set,expr)

View File

@ -1,6 +1,6 @@
option(X) :=
option(item) :=
(**)
| X
| item
series(item,sep,term) ::=
item after_item(item,sep,term)
@ -15,33 +15,34 @@ item_or_closing(item,sep,term) ::=
(* Compound constructs *)
par(X) ::= LPAR X RPAR
par(item) ::=
LPAR item RPAR
brackets(X) ::= LBRACKET X RBRACKET
brackets(item) ::=
LBRACKET item RBRACKET
(* Sequences *)
(* Possibly empty sequence of items *)
seq(X) ::=
(**)
| X seq(X)
seq(item) ::=
option(nseq(item))
(* Non-empty sequence of items *)
nseq(X) ::= X seq(X)
nseq(item) ::=
item seq(item)
(* Non-empty separated sequence of items *)
nsepseq(X,Sep) ::=
X
| X Sep nsepseq(X,Sep)
nsepseq(item,Sep) ::=
item
| item Sep nsepseq(item,Sep)
(* Possibly empy separated sequence of items *)
(* Possibly empty separated sequence of items *)
sepseq(X,Sep) ::=
(**)
| nsepseq(X,Sep)
sepseq(item,Sep) ::=
option(nsepseq(item,Sep))
(* Main *)
@ -244,10 +245,6 @@ interactive_expr ::=
expr ::=
case(expr)
| annot_expr
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
| disj_expr
disj_expr ::=
@ -305,6 +302,7 @@ core_expr ::=
| C_False
| C_True
| C_Unit
| annot_expr
| tuple_expr
| list_expr
| C_None
@ -317,6 +315,9 @@ core_expr ::=
| Constr
| C_Some arguments
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
set_expr ::=
injection(Set,expr)

View File

@ -1,6 +1,6 @@
option(X) :=
option(item) :=
(**)
| X
| item
series(item,sep,term) ::=
item after_item(item,sep,term)
@ -15,33 +15,34 @@ item_or_closing(item,sep,term) ::=
(* Compound constructs *)
par(X) ::= LPAR X RPAR
par(item) ::=
LPAR item RPAR
brackets(X) ::= LBRACKET X RBRACKET
brackets(item) ::=
LBRACKET item RBRACKET
(* Sequences *)
(* Possibly empty sequence of items *)
seq(X) ::=
(**)
| X seq(X)
seq(item) ::=
option(nseq(item))
(* Non-empty sequence of items *)
nseq(X) ::= X seq(X)
nseq(item) ::=
item seq(item)
(* Non-empty separated sequence of items *)
nsepseq(X,Sep) ::=
X
| X Sep nsepseq(X,Sep)
nsepseq(item,Sep) ::=
item
| item Sep nsepseq(item,Sep)
(* Possibly empy separated sequence of items *)
(* Possibly empty separated sequence of items *)
sepseq(X,Sep) ::=
(**)
| nsepseq(X,Sep)
sepseq(item,Sep) ::=
option(nsepseq(item,Sep))
(* Main *)
@ -238,10 +239,6 @@ interactive_expr ::=
expr ::=
case(expr)
| annot_expr
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
| disj_expr
disj_expr ::=
@ -299,6 +296,7 @@ core_expr ::=
| C_False
| C_True
| C_Unit
| annot_expr
| tuple_expr
| list_expr
| C_None
@ -311,6 +309,9 @@ core_expr ::=
| Constr
| C_Some arguments
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
set_expr ::=
injection(Set,expr)

View File

@ -1,6 +1,6 @@
option(X) :=
option(item) :=
(**)
| X
| item
series(item,sep,term) ::=
item after_item(item,sep,term)
@ -15,33 +15,34 @@ item_or_closing(item,sep,term) ::=
(* Compound constructs *)
par(X) ::= LPAR X RPAR
par(item) ::=
LPAR item RPAR
brackets(X) ::= LBRACKET X RBRACKET
brackets(item) ::=
LBRACKET item RBRACKET
(* Sequences *)
(* Possibly empty sequence of items *)
seq(X) ::=
(**)
| X seq(X)
seq(item) ::=
option(nseq(item))
(* Non-empty sequence of items *)
nseq(X) ::= X seq(X)
nseq(item) ::=
item seq(item)
(* Non-empty separated sequence of items *)
nsepseq(X,Sep) ::=
X
| X Sep nsepseq(X,Sep)
nsepseq(item,Sep) ::=
item
| item Sep nsepseq(item,Sep)
(* Possibly empy separated sequence of items *)
(* Possibly empty separated sequence of items *)
sepseq(X,Sep) ::=
(**)
| nsepseq(X,Sep)
sepseq(item,Sep) ::=
option(nsepseq(item,Sep))
(* Main *)
@ -194,9 +195,9 @@ single_instr ::=
injection(Kind,element) ::=
Kind series(element,SEMI,End)
| Kind End
| Kind LBRACKET bracketed
| Kind LBRACKET bracketed(element)
bracketed ::=
bracketed(element) ::=
series(element,SEMI,RBRACKET)
| RBRACKET
@ -241,10 +242,6 @@ interactive_expr ::=
expr ::=
case(expr)
| annot_expr
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
| disj_expr
disj_expr ::=
@ -302,6 +299,7 @@ core_expr ::=
| C_False
| C_True
| C_Unit
| annot_expr
| tuple_expr
| list_expr
| C_None
@ -314,6 +312,9 @@ core_expr ::=
| Constr
| C_Some arguments
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
set_expr ::=
injection(Set,expr)

View File

@ -1,6 +1,6 @@
option(X) :=
option(item) :=
(**)
| X
| item
series(item,sep,term) ::=
item after_item(item,sep,term)
@ -15,33 +15,31 @@ item_or_closing(item,sep,term) ::=
(* Compound constructs *)
par(X) ::= LPAR X RPAR
par(item) ::= LPAR item RPAR
brackets(X) ::= LBRACKET X RBRACKET
brackets(item) ::= LBRACKET item RBRACKET
(* Sequences *)
(* Possibly empty sequence of items *)
seq(X) ::=
(**)
| X seq(X)
seq(item) ::=
option(nseq(item))
(* Non-empty sequence of items *)
nseq(X) ::= X seq(X)
nseq(item) ::= item seq(item)
(* Non-empty separated sequence of items *)
nsepseq(X,Sep) ::=
X
| X Sep nsepseq(X,Sep)
nsepseq(item,Sep) ::=
item
| item Sep nsepseq(item,Sep)
(* Possibly empy separated sequence of items *)
(* Possibly empty separated sequence of items *)
sepseq(X,Sep) ::=
(**)
| nsepseq(X,Sep)
sepseq(item,Sep) ::=
option(nsepseq(item,Sep))
(* Main *)
@ -184,9 +182,9 @@ single_instr ::=
injection(Kind,element) ::=
Kind series(element,SEMI,End)
| Kind End
| Kind LBRACKET bracketed
| Kind LBRACKET bracketed(element)
bracketed ::=
bracketed(element) ::=
series(element,SEMI,RBRACKET)
| RBRACKET
@ -231,10 +229,6 @@ interactive_expr ::=
expr ::=
case(expr)
| annot_expr
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
| disj_expr
disj_expr ::=
@ -292,6 +286,7 @@ core_expr ::=
| C_False
| C_True
| C_Unit
| annot_expr
| tuple_expr
| list_expr
| C_None
@ -304,6 +299,9 @@ core_expr ::=
| Constr
| C_Some arguments
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
set_expr ::=
injection(Set,expr)

View File

@ -1,6 +1,6 @@
option(X) :=
option(item) :=
(**)
| X
| item
series(item,sep,term) ::=
item after_item(item,sep,term)
@ -15,33 +15,34 @@ item_or_closing(item,sep,term) ::=
(* Compound constructs *)
par(X) ::= LPAR X RPAR
par(item) ::=
LPAR item RPAR
brackets(X) ::= LBRACKET X RBRACKET
brackets(item) ::=
LBRACKET item RBRACKET
(* Sequences *)
(* Possibly empty sequence of items *)
seq(X) ::=
(**)
| X seq(X)
seq(item) ::=
option(nseq(item))
(* Non-empty sequence of items *)
nseq(X) ::= X seq(X)
nseq(item) ::=
item seq(item)
(* Non-empty separated sequence of items *)
nsepseq(X,Sep) ::=
X
| X Sep nsepseq(X,Sep)
nsepseq(item,Sep) ::=
item
| item Sep nsepseq(item,Sep)
(* Possibly empy separated sequence of items *)
(* Possibly empty separated sequence of items *)
sepseq(X,Sep) ::=
(**)
| nsepseq(X,Sep)
sepseq(item,Sep) ::=
option(nsepseq(item,Sep))
(* Main *)
@ -186,9 +187,9 @@ single_instr ::=
injection(Kind,element) ::=
Kind series(element,SEMI,End)
| Kind End
| Kind LBRACKET bracketed
| Kind LBRACKET bracketed(element)
bracketed ::=
bracketed(element) ::=
series(element,SEMI,RBRACKET)
| RBRACKET
@ -233,10 +234,6 @@ interactive_expr ::=
expr ::=
case(expr)
| annot_expr
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
| disj_expr
disj_expr ::=
@ -294,6 +291,7 @@ core_expr ::=
| C_False
| C_True
| C_Unit
| annot_expr
| tuple_expr
| list_expr
| C_None
@ -306,6 +304,9 @@ core_expr ::=
| Constr
| C_Some arguments
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
set_expr ::=
injection(Set,expr)

View File

@ -1,12 +1,13 @@
left_assoc(item,op)
right_assoc(item,op) ::=
item
| item op right_assoc(item,op)
option(X) :=
left_assoc(item,op) ::=
right_assoc(item,op)
option(item) :=
(**)
| X
| item
series(item,sep,term) ::=
item after_item(item,sep,term)
@ -21,33 +22,34 @@ item_or_closing(item,sep,term) ::=
(* Compound constructs *)
par(X) ::= LPAR X RPAR
par(item) ::=
LPAR item RPAR
brackets(X) ::= LBRACKET X RBRACKET
brackets(item) ::=
LBRACKET item RBRACKET
(* Sequences *)
(* Possibly empty sequence of items *)
seq(X) ::=
(**)
| X seq(X)
seq(item) ::=
option(nseq(item))
(* Non-empty sequence of items *)
nseq(X) ::= X seq(X)
nseq(item) ::=
item seq(item)
(* Non-empty separated sequence of items *)
nsepseq(X,Sep) ::=
X
| X Sep nsepseq(X,Sep)
nsepseq(item,Sep) ::=
item
| item Sep nsepseq(item,Sep)
(* Possibly empy separated sequence of items *)
(* Possibly empty separated sequence of items *)
sepseq(X,Sep) ::=
(**)
| nsepseq(X,Sep)
sepseq(item,Sep) ::=
option(nsepseq(item,Sep))
(* Main *)
@ -191,9 +193,9 @@ single_instr ::=
injection(Kind,element) ::=
Kind series(element,SEMI,End)
| Kind End
| Kind LBRACKET bracketed
| Kind LBRACKET bracketed(element)
bracketed ::=
bracketed(element) ::=
series(element,SEMI,RBRACKET)
| RBRACKET
@ -236,10 +238,6 @@ interactive_expr ::=
expr ::=
case(expr)
| annot_expr
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
| disj_expr
disj_expr ::=
@ -297,6 +295,7 @@ core_expr ::=
| C_False
| C_True
| C_Unit
| annot_expr
| tuple_expr
| list_expr
| C_None
@ -309,6 +308,9 @@ core_expr ::=
| Constr
| C_Some arguments
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
set_expr ::=
injection(Set,expr)

View File

@ -1,12 +1,13 @@
left_assoc(item,op)
right_assoc(item,op) ::=
item
| item op right_assoc(item,op)
option(X) :=
left_assoc(item,op) ::=
right_assoc(item,op)
option(item) :=
(**)
| X
| item
series(item,sep,term) ::=
item after_item(item,sep,term)
@ -21,33 +22,34 @@ item_or_closing(item,sep,term) ::=
(* Compound constructs *)
par(X) ::= LPAR X RPAR
par(item) ::=
LPAR item RPAR
brackets(X) ::= LBRACKET X RBRACKET
brackets(item) ::=
LBRACKET item RBRACKET
(* Sequences *)
(* Possibly empty sequence of items *)
seq(X) ::=
(**)
| X seq(X)
seq(item) ::=
option(nseq(item))
(* Non-empty sequence of items *)
nseq(X) ::= X seq(X)
nseq(item) ::=
item seq(item)
(* Non-empty separated sequence of items *)
nsepseq(X,Sep) ::=
X
| X Sep nsepseq(X,Sep)
nsepseq(item,Sep) ::=
item
| item Sep nsepseq(item,Sep)
(* Possibly empy separated sequence of items *)
(* Possibly empty separated sequence of items *)
sepseq(X,Sep) ::=
(**)
| nsepseq(X,Sep)
sepseq(item,Sep) ::=
option(nsepseq(item,Sep))
(* Main *)
@ -191,9 +193,9 @@ single_instr ::=
injection(Kind,element) ::=
Kind series(element,SEMI,End)
| Kind End
| Kind LBRACKET bracketed
| Kind LBRACKET bracketed(element)
bracketed ::=
bracketed(element) ::=
series(element,SEMI,RBRACKET)
| RBRACKET
@ -237,10 +239,6 @@ interactive_expr ::=
expr ::=
case(expr)
| annot_expr
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
| disj_expr
disj_expr ::=
@ -292,6 +290,7 @@ core_expr ::=
| C_False
| C_True
| C_Unit
| annot_expr
| tuple_expr
| list_expr
| C_None
@ -304,6 +303,9 @@ core_expr ::=
| Constr
| C_Some arguments
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
set_expr ::=
injection(Set,expr)

View File

@ -1,12 +1,13 @@
left_assoc(item,op)
right_assoc(item,op) ::=
item
| item op right_assoc(item,op)
option(X) :=
left_assoc(item,op) ::=
right_assoc(item,op)
option(item) :=
(**)
| X
| item
series(item,sep,term) ::=
item after_item(item,sep,term)
@ -21,33 +22,34 @@ item_or_closing(item,sep,term) ::=
(* Compound constructs *)
par(X) ::= LPAR X RPAR
par(item) ::=
LPAR item RPAR
brackets(X) ::= LBRACKET X RBRACKET
brackets(item) ::=
LBRACKET item RBRACKET
(* Sequences *)
(* Possibly empty sequence of items *)
seq(X) ::=
(**)
| X seq(X)
seq(item) ::=
option(nseq(item))
(* Non-empty sequence of items *)
nseq(X) ::= X seq(X)
nseq(item) ::=
item seq(item)
(* Non-empty separated sequence of items *)
nsepseq(X,Sep) ::=
X
| X Sep nsepseq(X,Sep)
nsepseq(item,Sep) ::=
item
| item Sep nsepseq(item,Sep)
(* Possibly empy separated sequence of items *)
(* Possibly empty separated sequence of items *)
sepseq(X,Sep) ::=
(**)
| nsepseq(X,Sep)
sepseq(item,Sep) ::=
option(nsepseq(item,Sep))
(* Main *)
@ -189,9 +191,9 @@ single_instr ::=
injection(Kind,element) ::=
Kind series(element,SEMI,End)
| Kind End
| Kind LBRACKET bracketed
| Kind LBRACKET bracketed(element)
bracketed ::=
bracketed(element) ::=
series(element,SEMI,RBRACKET)
| RBRACKET
@ -235,10 +237,6 @@ interactive_expr ::=
expr ::=
case(expr)
| annot_expr
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
| disj_expr
disj_expr ::=
@ -293,6 +291,7 @@ core_expr ::=
| C_False
| C_True
| C_Unit
| annot_expr
| tuple_expr
| list_expr
| C_None
@ -302,6 +301,9 @@ core_expr ::=
| Constr
| C_Some arguments
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
structure ::=
injection(Map,binding)
| injection(Set,expr)

View File

@ -1,12 +1,13 @@
left_assoc(item,op)
right_assoc(item,op) ::=
item
| item op right_assoc(item,op)
option(X) :=
left_assoc(item,op) ::=
right_assoc(item,op)
option(item) :=
(**)
| X
| item
series(item,sep,term) ::=
item after_item(item,sep,term)
@ -21,33 +22,34 @@ item_or_closing(item,sep,term) ::=
(* Compound constructs *)
par(X) ::= LPAR X RPAR
par(item) ::=
LPAR item RPAR
brackets(X) ::= LBRACKET X RBRACKET
brackets(item) ::=
LBRACKET item RBRACKET
(* Sequences *)
(* Possibly empty sequence of items *)
seq(X) ::=
(**)
| X seq(X)
seq(item) ::=
option(nseq(item))
(* Non-empty sequence of items *)
nseq(X) ::= X seq(X)
nseq(item) ::=
item seq(item)
(* Non-empty separated sequence of items *)
nsepseq(X,Sep) ::=
X
| X Sep nsepseq(X,Sep)
nsepseq(item,Sep) ::=
item
| item Sep nsepseq(item,Sep)
(* Possibly empy separated sequence of items *)
(* Possibly empty separated sequence of items *)
sepseq(X,Sep) ::=
(**)
| nsepseq(X,Sep)
sepseq(item,Sep) ::=
option(nsepseq(item,Sep))
(* Main *)
@ -186,12 +188,16 @@ single_instr ::=
| Remove expr From Map path
| Remove expr From Set path
path ::=
Ident (* var *)
| Ident (* struct_name *) DOT nsepseq(selection,DOT)
injection(Kind,element) ::=
Kind series(element,SEMI,End)
| Kind End
| Kind LBRACKET bracketed
| Kind LBRACKET bracketed(element)
bracketed ::=
bracketed(element) ::=
series(element,SEMI,RBRACKET)
| RBRACKET
@ -235,10 +241,6 @@ interactive_expr ::=
expr ::=
case(expr)
| annot_expr
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
| disj_expr
disj_expr ::=
@ -296,8 +298,10 @@ core_expr ::=
| C_None
| C_Some arguments
| Constr option(arguments)
| tuple_expr
| list_expr
| LPAR disj_expr COLON type_expr RPAR
| par(nsepseq(expr,COMMA))
| injection(List,expr)
| Nil
| structure
structure ::=
@ -305,10 +309,6 @@ structure ::=
| injection(Set,expr)
| record_expr
path ::=
Ident (* var *)
| Ident (* struct_name *) DOT nsepseq(selection,DOT)
selection ::=
Ident (* field_name *)
| Int
@ -320,18 +320,8 @@ record_expr ::=
field_assignment ::=
Ident (* field_name *) EQUAL expr
tuple_expr ::=
tuple_inj
tuple_inj ::=
par(nsepseq(expr,COMMA))
arguments ::=
tuple_inj
list_expr ::=
injection(List,expr)
| Nil
par(nsepseq(expr,COMMA))
(* Patterns *)

View File

@ -0,0 +1,351 @@
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 (* 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(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 cases(rhs) End
| Case expr Of LBRACKET cases(rhs) RBRACKET
cases(rhs) ::=
nsepseq(case_clause(rhs),VBAR)
| VBAR nsepseq(case_clause(rhs),VBAR)
case_clause(rhs) ::=
pattern ARROW rhs
loop ::=
while_loop
| for_loop
while_loop ::=
While expr block
for_loop ::=
For Ident ASS expr option(Down) To expr option(step_clause) block
| For Ident In expr block
| For Ident ARROW Ident In expr block
step_clause ::=
Step expr
(* Expressions *)
interactive_expr ::=
expr EOF
expr ::=
case(expr)
| disj_expr
disj_expr ::=
left_assoc(conj_expr,Or)
conj_expr ::=
left_assoc(set_membership,And)
set_membership ::=
core_expr Contains set_membership
| comp_expr
comp_expr ::=
left_assoc(cat_expr,op_comp)
op_comp ::=
LT | LEQ | GT | GEQ | EQUAL | NEQ
cat_expr ::=
right_assoc(cons_expr,CAT)
cons_expr ::=
left_assoc(add_expr,CONS)
add_expr ::=
left_assoc(mult_expr,add_op)
add_op ::=
PLUS | MINUS
mult_expr ::=
left_assoc(unary_expr,mult_op)
mult_op ::=
TIMES | SLASH | Mod
unary_expr ::=
MINUS core_expr
| Not core_expr
| core_expr
core_expr ::=
Int
| Nat
| Mtz
| Ident (* var *)
| Ident (* var *) brackets(expr) (* lookup *)
| Ident (* struct_name *) DOT nsepseq(selection,DOT) option(brackets(expr))
| Ident (* fun_name *) arguments
| String
| Bytes
| C_False
| C_True
| C_Unit
| C_None
| C_Some arguments
| Constr option(arguments)
| LPAR disj_expr COLON type_expr RPAR
| LPAR nsepseq(expr,COMMA) RPAR
| injection(List,expr)
| Nil
| structure
structure ::=
injection(Map,binding)
| injection(Set,expr)
| record_expr
selection ::=
Ident (* field_name *)
| Int
record_expr ::=
Record series(field_assignment,SEMI,End)
| Record LBRACKET series(field_assignment,SEMI,RBRACKET)
field_assignment ::=
Ident (* field_name *) EQUAL expr
arguments ::=
par(nsepseq(expr,COMMA))
(* Patterns *)
pattern ::=
nsepseq(core_pattern,CONS)
core_pattern ::=
Ident (* var *)
| WILD
| Int
| String
| C_Unit
| C_False
| C_True
| C_None
| C_Some par(core_pattern)
| Constr option(tuple_pattern)
| injection(List,core_pattern)
| Nil
| par(cons_pattern)
| par(nsepseq(core_pattern,COMMA))
tuple_pattern ::=
par(nsepseq(core_pattern,COMMA))
cons_pattern ::=
core_pattern CONS pattern

View File

@ -0,0 +1,352 @@
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 (* 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(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 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))
tuple_pattern ::=
par(nsepseq(core_pattern,COMMA))
cons_pattern ::=
core_pattern CONS pattern

View 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(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 (* 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(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 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))
tuple_pattern ::=
par(nsepseq(core_pattern,COMMA))
cons_pattern ::=
core_pattern CONS pattern

View File

@ -0,0 +1,357 @@
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 (* 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(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 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))
tuple_pattern ::=
par(nsepseq(core_pattern,COMMA))
cons_pattern ::=
core_pattern CONS pattern

View File

@ -0,0 +1,357 @@
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 (* 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(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 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
tuple_pattern ::=
par(nsepseq(core_pattern,COMMA))
cons_pattern ::=
core_pattern CONS pattern

View File

@ -0,0 +1,360 @@
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 (* 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(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 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)
tuple_pattern ::=
par(nsepseq(core_pattern,COMMA))
cons_pattern ::=
core_pattern CONS pattern

View File

@ -0,0 +1,358 @@
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 (* 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(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 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)
tuple_pattern ::=
par(nsepseq(core_pattern,COMMA))

View File

@ -0,0 +1,343 @@
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 series(field_decl,SEMI,End)
| Record LBRACKET series(field_decl,SEMI,RBRACKET)
variant ::=
Constr Of cartesian
| Constr
cartesian ::=
nsepseq(function_type,TIMES)
function_type ::=
right_assoc(core_type,ARROW)
core_type ::=
Ident (* type_name *)
| Ident (* type_name *) type_tuple
| Map type_tuple
| Set par(type_expr)
| List par(type_expr)
| par(type_expr)
type_tuple ::=
par(nsepseq(type_expr,COMMA))
field_decl ::=
Ident (* field_name *) COLON type_expr
(* Function and procedure declarations *)
lambda_decl ::=
fun_decl
| proc_decl
| entry_decl
fun_decl ::=
Function Ident parameters COLON type_expr Is
seq(local_decl)
block
With expr
entry_decl ::=
Entrypoint Ident entry_params COLON type_expr Is
seq(local_decl)
block
With expr
entry_params ::=
par(nsepseq(entry_param_decl,SEMI))
proc_decl ::=
Procedure Ident parameters Is
seq(local_decl)
block
parameters ::=
par(nsepseq(param_decl,SEMI))
param_decl ::=
Var Ident COLON param_type
| Const Ident COLON param_type
entry_param_decl ::=
param_decl
| Storage Ident COLON param_type
param_type ::=
cartesian
block ::=
Begin series(statement,SEMI,End)
| Block LBRACE series(statement,SEMI,RBRACE)
statement ::=
instruction
| data_decl
data_decl ::=
const_decl
| var_decl
const_decl ::=
Const unqualified_decl(EQUAL)
var_decl ::=
Var unqualified_decl(ASS)
local_decl ::=
fun_decl option(SEMI)
| proc_decl option(SEMI)
| data_decl option(SEMI)
unqualified_decl(op) ::=
Ident (* var *) COLON type_expr op expr
instruction ::=
block
| If expr Then if_clause option(SEMI) Else if_clause
| case(instruction)
| Ident (* proc_name *) arguments
| Ident ASS expr
| Ident brackets(expr) ASS expr
| Ident DOT nsepseq(selection,DOT) option(brackets(expr)) ASS expr
| loop
| Fail expr
| Skip
| Patch path With structure
| Remove expr From Map path
| Remove expr From Set path
path ::=
Ident (* var *)
| Ident (* struct_name *) DOT nsepseq(selection,DOT)
injection(Kind,element) ::=
Kind series(element,SEMI,End)
| Kind End
| Kind LBRACKET bracketed(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 cases(rhs) End
| Case expr Of LBRACKET cases(rhs) RBRACKET
cases(rhs) ::=
nsepseq(case_clause(rhs),VBAR)
| VBAR nsepseq(case_clause(rhs),VBAR)
case_clause(rhs) ::=
pattern ARROW rhs
loop ::=
While expr block
| For Ident ASS expr option(Down) To expr option(step_clause) block
| For Ident In expr block
| For Ident ARROW Ident In expr block
step_clause ::=
Step expr
(* Expressions *)
interactive_expr ::=
expr EOF
expr ::=
case(expr)
| disj_expr
disj_expr ::=
left_assoc(conj_expr,Or)
conj_expr ::=
left_assoc(set_membership,And)
set_membership ::=
core_expr Contains set_membership
| comp_expr
comp_expr ::=
left_assoc(cat_expr,op_comp)
op_comp ::=
LT | LEQ | GT | GEQ | EQUAL | NEQ
cat_expr ::=
right_assoc(cons_expr,CAT)
cons_expr ::=
left_assoc(add_expr,CONS)
add_expr ::=
left_assoc(mult_expr,add_op)
add_op ::=
PLUS | MINUS
mult_expr ::=
left_assoc(unary_expr,mult_op)
mult_op ::=
TIMES | SLASH | Mod
unary_expr ::=
MINUS core_expr
| Not core_expr
| core_expr
core_expr ::=
Int
| Nat
| Mtz
| Ident (* var *)
| Ident (* var *) brackets(expr) (* lookup *)
| Ident (* struct_name *) DOT nsepseq(selection,DOT) option(brackets(expr))
| Ident (* fun_name *) arguments
| String
| Bytes
| C_False
| C_True
| C_Unit
| C_None
| C_Some arguments
| Constr option(arguments)
| par(paren_expr)
| 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(paren_pattern)
paren_pattern ::=
core_pattern CONS pattern
| core_pattern
| core_pattern COMMA nsepseq(core_pattern,COMMA)
tuple_pattern ::=
par(nsepseq(core_pattern,COMMA))

View 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))

View 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))

View File

@ -79,7 +79,6 @@ type t =
| Down of Region.t (* "down" *)
| Else of Region.t (* "else" *)
| End of Region.t (* "end" *)
| Entrypoint of Region.t (* "entrypoint" *)
| Fail of Region.t (* "fail" *)
| For of Region.t (* "for" *)
| From of Region.t (* "from" *)
@ -101,7 +100,6 @@ type t =
| Set of Region.t (* "set" *)
| Skip of Region.t (* "skip" *)
| Step of Region.t (* "step" *)
| Storage of Region.t (* "storage" *)
| Then of Region.t (* "then" *)
| To of Region.t (* "to" *)
| Type of Region.t (* "type" *)

View File

@ -77,7 +77,6 @@ type t =
| Down of Region.t (* "down" *)
| Else of Region.t (* "else" *)
| End of Region.t (* "end" *)
| Entrypoint of Region.t (* "entrypoint" *)
| Fail of Region.t (* "fail" *)
| For of Region.t (* "for" *)
| From of Region.t (* "from" *)
@ -99,7 +98,6 @@ type t =
| Set of Region.t (* "set" *)
| Skip of Region.t (* "skip" *)
| Step of Region.t (* "step" *)
| Storage of Region.t (* "storage" *)
| Then of Region.t (* "then" *)
| To of Region.t (* "to" *)
| Type of Region.t (* "type" *)
@ -210,7 +208,6 @@ let proj_token = function
| Down region -> region, "Down"
| Else region -> region, "Else"
| End region -> region, "End"
| Entrypoint region -> region, "Entrypoint"
| Fail region -> region, "Fail"
| For region -> region, "For"
| From region -> region, "From"
@ -232,7 +229,6 @@ let proj_token = function
| Set region -> region, "Set"
| Skip region -> region, "Skip"
| Step region -> region, "Step"
| Storage region -> region, "Storage"
| Then region -> region, "Then"
| To region -> region, "To"
| Type region -> region, "Type"
@ -304,7 +300,6 @@ let to_lexeme = function
| Down _ -> "down"
| Else _ -> "else"
| End _ -> "end"
| Entrypoint _ -> "entrypoint"
| Fail _ -> "fail"
| For _ -> "for"
| From _ -> "from"
@ -326,7 +321,6 @@ let to_lexeme = function
| Set _ -> "set"
| Skip _ -> "skip"
| Step _ -> "step"
| Storage _ -> "storage"
| Then _ -> "then"
| To _ -> "to"
| Type _ -> "type"
@ -366,7 +360,6 @@ let keywords = [
(fun reg -> Down reg);
(fun reg -> Else reg);
(fun reg -> End reg);
(fun reg -> Entrypoint reg);
(fun reg -> For reg);
(fun reg -> From reg);
(fun reg -> Function reg);
@ -388,7 +381,6 @@ let keywords = [
(fun reg -> Set reg);
(fun reg -> Skip reg);
(fun reg -> Step reg);
(fun reg -> Storage reg);
(fun reg -> Then reg);
(fun reg -> To reg);
(fun reg -> Type reg);
@ -584,7 +576,6 @@ let is_kwd = function
| Down _
| Else _
| End _
| Entrypoint _
| Fail _
| For _
| From _
@ -606,7 +597,6 @@ let is_kwd = function
| Set _
| Skip _
| Step _
| Storage _
| Then _
| To _
| Type _

View File

@ -53,7 +53,6 @@
%token <Region.t> Down (* "down" *)
%token <Region.t> Else (* "else" *)
%token <Region.t> End (* "end" *)
%token <Region.t> Entrypoint (* "entrypoint" *)
%token <Region.t> For (* "for" *)
%token <Region.t> Function (* "function" *)
%token <Region.t> From (* "from" *)
@ -74,7 +73,6 @@
%token <Region.t> Set (* "set" *)
%token <Region.t> Skip (* "skip" *)
%token <Region.t> Step (* "step" *)
%token <Region.t> Storage (* "storage" *)
%token <Region.t> Then (* "then" *)
%token <Region.t> To (* "to" *)
%token <Region.t> Type (* "type" *)

View File

@ -235,7 +235,6 @@ field_decl:
lambda_decl:
fun_decl { FunDecl $1 }
| proc_decl { ProcDecl $1 }
| entry_decl { EntryDecl $1 }
fun_decl:
Function fun_name parameters COLON type_expr Is
@ -261,33 +260,6 @@ fun_decl:
terminator = $11}
in {region; value}}
entry_decl:
Entrypoint fun_name entry_params COLON type_expr Is
seq(local_decl)
block
With expr option(SEMI) {
let stop =
match $11 with
Some region -> region
| None -> expr_to_region $10 in
let region = cover $1 stop
and value = {
kwd_entrypoint = $1;
name = $2;
param = $3;
colon = $4;
ret_type = $5;
kwd_is = $6;
local_decls = $7;
block = $8;
kwd_with = $9;
return = $10;
terminator = $11}
in {region; value}}
entry_params:
par(nsepseq(entry_param_decl,SEMI)) { $1 }
proc_decl:
Procedure fun_name parameters Is
seq(local_decl)
@ -332,22 +304,6 @@ param_decl:
param_type = $4}
in ParamConst {region; value}}
entry_param_decl:
param_decl {
match $1 with
ParamConst const -> EntryConst const
| ParamVar var -> EntryVar var
}
| Storage var COLON param_type {
let stop = type_expr_to_region $4 in
let region = cover $1 stop
and value = {
kwd_storage = $1;
var = $2;
colon = $3;
storage_type = $4}
in EntryStore {region; value}}
param_type:
cartesian { TProd $1 }
@ -697,8 +653,7 @@ interactive_expr:
expr:
case(expr) { ECase ($1 expr_to_region) }
(*| annot_expr { $1 }*)
| disj_expr { $1 }
| disj_expr { $1 }
disj_expr:
disj_expr Or conj_expr {

View File

@ -144,7 +144,6 @@ and print_type_tuple {value; _} =
and print_lambda_decl = function
FunDecl fun_decl -> print_fun_decl fun_decl
| ProcDecl proc_decl -> print_proc_decl proc_decl
| EntryDecl entry_decl -> print_entry_decl entry_decl
and print_fun_decl {value; _} =
let {kwd_function; name; param; colon;
@ -173,40 +172,6 @@ and print_proc_decl {value; _} =
print_block block;
print_terminator terminator
and print_entry_decl {value; _} =
let {kwd_entrypoint; name; param; colon;
ret_type; kwd_is; local_decls;
block; kwd_with; return; terminator} = value in
print_token kwd_entrypoint "entrypoint";
print_var name;
print_entry_params param;
print_token colon ":";
print_type_expr ret_type;
print_token kwd_is "is";
print_local_decls local_decls;
print_block block;
print_token kwd_with "with";
print_expr return;
print_terminator terminator
and print_entry_params {value; _} =
let {lpar; inside; rpar} = value in
print_token lpar "(";
print_nsepseq ";" print_entry_param_decl inside;
print_token rpar ")"
and print_entry_param_decl = function
EntryConst param_const -> print_param_const param_const
| EntryVar param_var -> print_param_var param_var
| EntryStore param_store -> print_storage param_store
and print_storage {value; _} =
let {kwd_storage; var; colon; storage_type} = value in
print_token kwd_storage "storage";
print_var var;
print_token colon ":";
print_type_expr storage_type
and print_parameters {value; _} =
let {lpar; inside; rpar} = value in
print_token lpar "(";

View File

@ -0,0 +1,395 @@
open LexToken
let semi = parser [< 'SEMI _ >] -> ()
let vbar = parser [< 'VBAR _ >] -> ()
let end_ = parser [< 'End _ >] -> ()
let rbracket = parser [< 'RBRACKET _ >] -> ()
let times = parser [< 'TIMES _ >] -> ()
let arrow = parser [< 'ARROW _ >] -> fun _ _ -> ()
let comma = parser [< 'COMMA _ >] -> ()
let rbrace = parser [< 'RBRACE _ >] -> ()
let equal = parser [< 'EQUAL _ >] -> ()
let ass = parser [< 'ASS _ >] -> ()
let dot = parser [< 'DOT _ >] -> ()
let down = parser [< 'Down _ >] -> ()
let or_ = parser [< 'Or _ >] -> fun _ _ -> ()
let and_ = parser [< 'And _ >] -> fun _ _ -> ()
let cat = parser [< 'CAT _ >] -> fun _ _ -> ()
let cons = parser [< 'CONS _ >] -> ()
let cons' = parser [< 'CONS _ >] -> fun _ _ -> ()
let list = parser [< 'List _ >] -> ()
let map = parser [< 'Map _ >] -> ()
let set = parser [< 'Set _ >] -> ()
let left_assoc item op =
let rec op_elem i = parser
[< f=op; j=item; r = op_elem (f i j) ?! >] -> r
| [< >] -> i
in parser [< i=item; r = op_elem i >] -> r
let rec right_assoc item op = parser
[< i=item >] -> i
| [< i=item; f=op; j = right_assoc item op ?! >] -> f i j
let opt item = parser
[< i=item >] -> Some i
| [< >] -> None
let rec series item sep term = parser
[< i=item; l = after_item item sep term >] -> i,l
and after_item item sep term = parser
[< t=term >] ->
[], None, t
| [< s=sep; io = item_or_closing item sep term >] ->
match io with
`Some (item, items, term, closing) ->
(s, item)::items, term, closing
| `Closing closing ->
[], Some s, closing
and item_or_closing item sep term = parser
[< t=term >] ->
`Closing t
| [< s = series item sep term >] ->
let item, (items, term, closing) = s
in `Some (item, items, term, closing)
(* Compound constructs *)
let par item = parser
[< 'LPAR _; _=item; 'RPAR _ >] -> ()
let brackets item = parser
[< 'LBRACKET _; _=item; 'RBRACKET _ >] -> ()
(* Sequences *)
(* Possibly empty sequence of items *)
let rec seq item = parser
[< h,t = nseq item >] -> h::t
(* Non-empty sequence of items *)
and nseq item = parser
[< i=item; l = seq item >] -> i,l
(* Non-empty separated sequence of items *)
and nsepseq item sep = parser
[< i=item >] -> i, []
| [< i=item; s=sep; h,t = nsepseq item sep ?! >] -> i, (s,h)::t
(* Possibly empty separated sequence of items *)
(*
and sepseq item sep = opt (nsepseq item sep)
*)
(* Main *)
let rec contract = parser
[< _ = nseq declaration; 'EOF _ >] -> ()
and declaration = parser
[< _ = type_decl; _ = opt semi >] -> ()
| [< _ = const_decl; _ = opt semi >] -> ()
| [< _ = lambda_decl; _ = opt semi >] -> ()
and type_decl = parser
[< 'Type _; 'Ident _; 'Is _; _=type_expr >] -> ()
and type_expr = parser
[< _=cartesian >] -> ()
| [< _=nsepseq variant vbar >] -> ()
| [< 'VBAR _; _ = nsepseq variant vbar >] -> ()
| [< 'Record _; _=record_type_expr >] -> ()
and record_type_expr = parser
[< _ = series field_decl semi end_ >] -> ()
| [< 'LBRACKET _; _ = series field_decl semi rbracket >] -> ()
and variant = parser
[< 'Constr _; _ = opt of_cartesian >] -> ()
and of_cartesian = parser
[< 'Of _; _=cartesian >] -> ()
and cartesian = parser
[< _ = nsepseq function_type times >] -> ()
and function_type strm = right_assoc core_type arrow strm
and core_type = parser
[< 'Ident _; _ = opt type_tuple >] -> ()
| [< 'Map _; _=type_tuple >] -> ()
| [< 'Set _; _ = par type_expr >] -> ()
| [< 'List _; _ = par type_expr >] -> ()
| [< _ = par type_expr >] -> ()
and type_tuple = parser
[< _ = par (nsepseq type_expr comma) >] -> ()
and field_decl = parser
[< 'Ident _; 'COLON _; _=type_expr >] -> ()
(* Function and procedure declarations *)
and lambda_decl = parser
[< _=fun_decl >] -> ()
| [< _=proc_decl >] -> ()
and fun_decl = parser
[< 'Function _; 'Ident _; _=parameters; 'COLON _;
_=type_expr; 'Is _; _ = seq local_decl; _=block;
'With _; _=expr >] -> ()
and proc_decl = parser
[< 'Procedure _; 'Ident _; _parameters; 'Is _;
_ = seq local_decl; _=block >] -> ()
and parameters = parser
[< p = par (nsepseq param_decl semi) >] -> p
and param_decl = parser
[< 'Var _; 'Ident _; 'COLON _; _=param_type >] -> ()
| [< 'Const _; 'Ident _; 'COLON _; _=param_type >] -> ()
and param_type = parser [< c = cartesian >] -> c
and block = parser
[< 'Begin _; _ = series statement semi end_ >] -> ()
| [< 'Block _; 'LBRACE _; _ = series statement semi rbrace >] -> ()
and statement = parser
[< _=instruction >] -> ()
| [< _=data_decl >] -> ()
and data_decl = parser
[< _=const_decl >] -> ()
| [< _=var_decl >] -> ()
and const_decl = parser
[< 'Const _; _ = unqualified_decl equal >] -> ()
and var_decl = parser
[< 'Var _; _ = unqualified_decl ass >] -> ()
and local_decl = parser
[< _=fun_decl; _ = opt semi >] -> ()
| [< _=proc_decl; _ = opt semi >] -> ()
| [< _=data_decl; _ = opt semi >] -> ()
and unqualified_decl op = parser
[< 'Ident _; 'COLON _; _=type_expr; _=op; _=expr >] -> ()
and instruction = parser
[< _=block >] -> ()
| [< 'If _; _=expr; 'Then _; _=if_clause; _ = opt semi;
'Else _; _=if_clause >] -> ()
| [< _ = case instruction >] -> ()
| [< 'Ident _; _=instruction_1 >] -> ()
| [< _=loop >] -> ()
| [< 'Fail _; _=expr >] -> ()
| [< 'Skip _ >] -> ()
| [< 'Patch _; _=path; 'With _; _=structure >] -> ()
| [< 'Remove _; _=expr; 'From _; _=remove_suffix >] -> ()
and remove_suffix = parser
[< 'Map _; _=path >] -> ()
| [< 'Set _; _=path >] -> ()
and instruction_1 = parser
[< _=arguments >] -> ()
| [< 'ASS _; _=expr >] -> ()
| [< _ = brackets expr; 'ASS _; _=expr >] -> ()
| [< _=selections;
_ = opt (brackets expr); 'ASS _; _=expr >] -> ()
and path = parser
[< 'Ident _; _ = opt selections >] -> ()
and selections = parser
[< 'DOT _; _ = nsepseq selection dot >] -> ()
and injection kind element = parser
[< _=kind; _ = inj_suffix element >] -> ()
and inj_suffix element = parser
[< _ = series element semi end_ >] -> ()
| [< 'End _ >] -> ()
| [< 'LBRACKET _; _ = bracketed element >] -> ()
and bracketed element = parser
[< _ = series element semi rbracket >] -> ()
| [< 'RBRACKET _ >] -> ()
and binding = parser
[< _=expr; 'ARROW _; _=expr >] -> ()
and if_clause = parser
[< _=instruction >] -> ()
| [< 'LBRACE _; _ = series statement comma rbrace >] -> ()
and case rhs = parser
[< 'Case _; _=expr; 'Of _; _ = case_suffix rhs >] -> ()
and case_suffix rhs = parser
[< _ = cases rhs; 'End _ >] -> ()
| [< 'LBRACKET _; _ = cases rhs; 'RBRACKET _ >] -> ()
and cases rhs = parser
[< _ = nsepseq (case_clause rhs) vbar >] -> ()
| [< 'VBAR _; _ = nsepseq (case_clause rhs) vbar >] -> ()
and case_clause rhs = parser
[< _=pattern; 'ARROW _; _=rhs >] -> ()
and loop = parser
[< 'While _; _=expr; _=block >] -> ()
| [< 'For _; 'Ident _; _=for_suffix >] -> ()
and for_suffix = parser
[< 'ASS _; _=expr; _ = opt down;
'To _; _=expr; _ = opt step_clause; _=block >] -> ()
| [< 'In _; _=expr; _=block >] -> ()
| [< 'ARROW _; 'Ident _; 'In _; _=expr; _=block >] -> ()
and step_clause = parser
[< 'Step _; _=expr >] -> ()
(* Expressions *)
and interactive = parser
[< _=expr; 'EOF _ >] -> ()
and expr = parser
[< _ = case expr >] -> ()
| [< _=disj_expr >] -> ()
and disj_expr strm = left_assoc conj_expr or_ strm
and conj_expr strm = left_assoc set_membership and_ strm
and set_membership = parser
[< _ = comp_expr; _ = opt contains_clause >] -> ()
and contains_clause = parser
[< 'Contains _; _=set_membership >] -> ()
and comp_expr strm = left_assoc cat_expr op_comp strm
and op_comp = parser
[< 'LT _ >] -> fun _ _ -> ()
| [< 'LEQ _ >] -> fun _ _ -> ()
| [< 'GT _ >] -> fun _ _ -> ()
| [< 'GEQ _ >] -> fun _ _ -> ()
| [< 'EQUAL _ >] -> fun _ _ -> ()
| [< 'NEQ _ >] -> fun _ _ -> ()
and cat_expr strm = right_assoc cons_expr cat strm
and cons_expr strm = left_assoc add_expr cons' strm
and add_expr strm = left_assoc mult_expr add_op strm
and add_op = parser
[< 'PLUS _ >] -> fun _ _ -> ()
| [< 'MINUS _ >] -> fun _ _ -> ()
and mult_expr strm = left_assoc unary_expr mult_op strm
and mult_op = parser
[< 'TIMES _ >] -> fun _ _ -> ()
| [< 'SLASH _ >] -> fun _ _ -> ()
| [< 'Mod _ >] -> fun _ _ -> ()
and unary_expr = parser
[< 'MINUS _; _=core_expr >] -> ()
| [< 'Not _; _=core_expr >] -> ()
| [< _=core_expr >] -> ()
and core_expr = parser
[< 'Int _ >] -> ()
| [< 'Nat _ >] -> ()
| [< 'Mtz _ >] -> ()
| [< 'Ident _; _ = opt core_suffix >] -> ()
| [< 'String _ >] -> ()
| [< 'Bytes _ >] -> ()
| [< 'C_False _ >] -> ()
| [< 'C_True _ >] -> ()
| [< 'C_Unit _ >] -> ()
| [< 'C_None _ >] -> ()
| [< 'C_Some _; _=arguments >] -> ()
| [< 'Constr _; _ = opt arguments >] -> ()
| [< _ = par paren_expr >] -> ()
| [< _ = injection list expr >] -> ()
| [< 'Nil _ >] -> ()
| [< _=structure >] -> ()
and core_suffix = parser
[< _ = brackets expr >] -> ()
| [< 'DOT _; _ = nsepseq selection dot;
_ = opt (brackets expr) >] -> ()
| [< _=arguments >] -> ()
and paren_expr = parser
[< _=disj_expr; _ = opt paren_expr_1 >] -> ()
| [< _ = case expr; _ = opt paren_expr_2 >] -> ()
and paren_expr_1 = parser
[< 'COLON _; _=type_expr >] -> ()
| [< 'COMMA _; _ = nsepseq expr comma >] -> ()
and paren_expr_2 = parser
[< 'COMMA _; _ = nsepseq expr comma >] -> ()
and structure = parser
[< _ = injection map binding >] -> ()
| [< _ = injection set expr >] -> ()
| [< _=record_expr >] -> ()
and selection = parser
[< 'Ident _ >] -> ()
| [< 'Int _ >] -> ()
and record_expr = parser
[< 'Record _; _=record_expr_suffix >] -> ()
and record_expr_suffix = parser
[< _ = series field_assignment semi end_ >] -> ()
| [< 'LBRACKET _;
_ = series field_assignment semi rbracket >] -> ()
and field_assignment = parser
[< 'Ident _; 'EQUAL _; _=expr >] -> ()
and arguments = parser
[< _ = par (nsepseq expr comma) >] -> ()
(* Patterns *)
and pattern = parser
[< _ = nsepseq core_pattern cons >] -> ()
and core_pattern = parser
[< 'Ident _ >] -> ()
| [< 'WILD _ >] -> ()
| [< 'Int _ >] -> ()
| [< 'String _ >] -> ()
| [< 'C_Unit _ >] -> ()
| [< 'C_False _ >] -> ()
| [< 'C_True _ >] -> ()
| [< 'C_None _ >] -> ()
| [< 'C_Some _; _ = par core_pattern >] -> ()
| [< 'Constr _; _ = opt tuple_pattern >] -> ()
| [< _ = injection list core_pattern >] -> ()
| [< 'Nil _ >] -> ()
| [< _ = par (opt paren_pattern) >] -> ()
and paren_pattern = parser
[< 'CONS _; _=pattern >] -> ()
| [< 'COMMA _; _ = nsepseq core_pattern comma >] -> ()
and tuple_pattern = parser
[< _ = par (nsepseq core_pattern comma) >] -> ()

View File

@ -0,0 +1,124 @@
(* Driver for the parser of PascaLIGO *)
open SParser (* TEMPORARY *)
(* Error printing and exception tracing *)
let () = Printexc.record_backtrace true
(* Reading the command-line options *)
let options = EvalOpt.read ()
open EvalOpt
(* Auxiliary functions *)
let sprintf = Printf.sprintf
(* Extracting the input file *)
let file =
match options.input with
None | Some "-" -> false
| Some _ -> true
(* Error printing and exception tracing *)
let () = Printexc.record_backtrace true
let external_ text =
Utils.highlight (Printf.sprintf "External error: %s" text); exit 1;;
type Error.t += ParseError
let error_to_string = function
ParseError -> "Syntax error.\n"
| _ -> assert false
let print_error ?(offsets=true) mode Region.{region; value} ~file =
let msg = error_to_string value in
let reg = region#to_string ~file ~offsets mode in
Utils.highlight (sprintf "Parse error %s:\n%s%!" reg msg)
(* Path for CPP inclusions (#include) *)
let lib_path =
match options.libs with
[] -> ""
| libs -> let mk_I dir path = Printf.sprintf " -I %s%s" dir path
in List.fold_right mk_I libs ""
(* Preprocessing the input source and opening the input channels *)
let prefix =
match options.input with
None | Some "-" -> "temp"
| Some file -> Filename.(file |> basename |> remove_extension)
let suffix = ".pp.ligo"
let pp_input =
if Utils.String.Set.mem "cpp" options.verbose
then prefix ^ suffix
else let pp_input, pp_out = Filename.open_temp_file prefix suffix
in close_out pp_out; pp_input
let cpp_cmd =
match options.input with
None | Some "-" ->
Printf.sprintf "cpp -traditional-cpp%s - > %s"
lib_path pp_input
| Some file ->
Printf.sprintf "cpp -traditional-cpp%s %s > %s"
lib_path file pp_input
let () =
if Utils.String.Set.mem "cpp" options.verbose
then Printf.eprintf "%s\n%!" cpp_cmd;
if Sys.command cpp_cmd <> 0 then
external_ (Printf.sprintf "the command \"%s\" failed." cpp_cmd)
(* Instanciating the lexer *)
module Lexer = Lexer.Make (LexToken)
module Log = LexerLog.Make (Lexer)
let Lexer.{read; buffer; get_pos; get_last; close} =
Lexer.open_token_stream (Some pp_input)
and cout = stdout
let log = Log.output_token ~offsets:options.offsets
options.mode options.cmd cout
and close_all () = close (); close_out cout
(* Tokeniser *)
let tokeniser = read ~log
(* Main *)
let () =
try
let ast = Parser.contract tokeniser buffer in
if Utils.String.Set.mem "ast" options.verbose
then begin
ParserLog.offsets := options.offsets;
ParserLog.mode := options.mode;
ParserLog.print_tokens ast
end
with
Lexer.Error err ->
close_all ();
Lexer.print_error ~offsets:options.offsets
options.mode err ~file
| Parser.Error ->
let region = get_last () in
let error = Region.{region; value=ParseError} in
let () = close_all () in
print_error ~offsets:options.offsets
options.mode error ~file
| Sys_error msg -> Utils.highlight msg

View File

@ -1,64 +1,55 @@
type store is
record [
goal : nat;
goal : mutez;
deadline : timestamp;
backers : map (address, nat);
funded : bool;
]
entrypoint contribute (storage store : store;
const sender : address;
const amount : mutez)
: store * list (operation) is
var operations : list (operation) := nil
// const s : list (int) = list [1; 2; 3]
//const t : set (int) = set []
function back (var store : store) : list (operation) * store is
var operations : list (operation) := list []
begin
if now (Unit) > store.deadline then
fail "Deadline passed";
if now > store.deadline then
failwith ("Deadline passed");
else
case store.backers[sender] of [
None -> store.backers[sender] := Some (amount);
// None -> patch store.backers with map sender -> amount end
None -> store.backers[sender] := amount
// or: None -> patch store.backers with map sender -> amount end
| _ -> skip
]
end with (store, operations)
end with (operations, store)
entrypoint withdraw (storage store : store; const sender : address)
: store * list (operation) is
var operations : list (operation) := list end
begin
// if set ["a"; "b"] contains x then skip else skip;
if sender = owner then
if now (Unit) >= store.deadline then
if balance >= store.goal then {
store.funded := True;
// patch store with record funded = True end;
operations := list [Transfer (owner, balance)];
};
else fail "Below target"
else block { fail "Too soon"; }
else skip
end with (store, operations)
entrypoint claim (storage store : store; const sender : address)
: store * list (operation) is
var operations : list (operation) := list []
var amount : mutez := 0
function claim (var store : store) : list (operation) * store is
var operations : list (operation) := nil
begin
if now <= store.deadline then
fail "Too soon"
failwith ("Too soon.")
else
case store.backers[sender] of
None ->
fail "Not a backer"
failwith ("Not a backer.")
| Some (amount) ->
if balance >= store.goal or store.funded then
fail "Cannot refund"
failwith ("Goal reached: no refund.")
else
begin
operations := list [Transfer (sender, amount)];
operations := list [transaction (unit, sender, amount)];
remove sender from map store.backers
end
end
end with (store, operations)
end with (operations, store)
function withdraw (var store : store) : list (operation) * store is
var operations : list (operation) := list end
begin
if sender = owner then
if now >= store.deadline then
if balance >= store.goal then {
store.funded := True;
// or: patch store with record funded = True end;
operations := list [Transfer (owner, balance)];
};
else failwith ("Below target.")
else fail "Too soon.";
else skip
end with (operations, store)

View File

@ -28,11 +28,11 @@
source regions, so useful error messages can be printed, therefore
they are part of the signature [TOKEN] that parameterises the
functor generated here. For instance, if, in a future release of
LIGO, new tokens may be added, and the recognition of their lexemes
may entail new errors, the signature [TOKEN] will have to be
augmented and the lexer specification changed. However, in
practice, it is more likely that instructions or types are added,
instead of new kinds of tokens.
LIGO, new tokens are added, and the recognition of their lexemes
entails new errors, the signature [TOKEN] will have to be augmented
and this lexer specification changed. However, in practice, it is
more likely that instructions or types will be added, instead of
new kinds of tokens.
*)
module Region = Simple_utils.Region

View File

@ -506,7 +506,6 @@ let nl = ['\n' '\r'] | "\r\n"
let blank = ' ' | '\t'
let digit = ['0'-'9']
let natural = digit | digit (digit | '_')* digit
let integer = '-'? natural
let decimal = digit+ '.' digit+
let small = ['a'-'z']
let capital = ['A'-'Z']
@ -552,7 +551,7 @@ and scan state = parse
| natural "mtz" { mk_mtz state lexbuf |> enqueue }
| natural "tz" { mk_tz state lexbuf |> enqueue }
| decimal "tz" { mk_tz_decimal state lexbuf |> enqueue }
| integer { mk_int state lexbuf |> enqueue }
| natural { mk_int state lexbuf |> enqueue }
| symbol { mk_sym state lexbuf |> enqueue }
| eof { mk_eof state lexbuf |> enqueue }
@ -595,7 +594,7 @@ and scan state = parse
processed).
*)
| '#' blank* ("line" blank+)? (integer as line) blank+
| '#' blank* ("line" blank+)? (natural as line) blank+
'"' (string as file) '"' {
let _, _, state = sync state lexbuf in
let flags, state = scan_flags state [] lexbuf in
@ -611,7 +610,7 @@ and scan state = parse
Some special errors are recognised in the semantic actions of the
following regular expressions. The first error is a minus sign
separated from the integer it modifies by some markup (space or
separated from the integer it applies by some markup (space or
tabs). The second is a minus sign immediately followed by
anything else than a natural number (matched above) or markup and
a number (previous error). The third is the strange occurrence of
@ -630,7 +629,7 @@ and scan state = parse
fail region Orphan_minus
| _ -> fail region Unterminated_integer }
| '-' "0x" byte_seq?
| "-0x" byte_seq?
{ let region, _, _ = sync state lexbuf
in fail region Negative_byte_sequence }
@ -642,7 +641,7 @@ and scan state = parse
and scan_flags state acc = parse
blank+ { let _, _, state = sync state lexbuf
in scan_flags state acc lexbuf }
| integer as code { let _, _, state = sync state lexbuf in
| natural as code { let _, _, state = sync state lexbuf in
let acc = int_of_string code :: acc
in scan_flags state acc lexbuf }
| nl { List.rev acc, push_newline state lexbuf }
@ -748,7 +747,7 @@ and scan_utf8 thread state = parse
report special error patterns), we need to keep a hidden reference
to a queue of recognised lexical units (that is, tokens and markup)
that acts as a mutable state between the calls to
[read_token]. When [read_token] is called, that queue is consulted
[read_token]. When [read_token] is called, that queue is examined
first and, if it contains at least one token, that token is
returned; otherwise, the lexing buffer is scanned for at least one
more new token. That is the general principle: we put a high-level
@ -843,19 +842,18 @@ let open_token_stream file_path_opt =
Some ([], next) ->
let pos = (Token.to_region token)#stop in
let region = Region.make ~start:pos ~stop:pos in
if is_bytes token && is_int next then
if is_int next then
fail region Odd_lengthed_bytes
else
if is_ident next || is_string next
|| is_bytes next || is_int next then
if is_ident next || is_string next || is_bytes next then
fail region Missing_break
| _ -> ()
else
if Token.is_ident token || Token.is_string token then
if is_ident token || is_string token then
match next_token buffer with
Some ([], next) ->
if Token.is_ident next || Token.is_string next
|| Token.is_bytes next || Token.is_int next
if is_ident next || is_string next
|| is_bytes next || is_int next
then
let pos = (Token.to_region token)#stop in
let region = Region.make ~start:pos ~stop:pos

View File

@ -46,17 +46,6 @@ module Errors = struct
] in
error ~data title message
let unsupported_entry_decl decl =
let title () = "entry point declarations" in
let message () =
Format.asprintf "entry points within the contract \
are not supported yet" in
let data = [
("declaration",
fun () -> Format.asprintf "%a" Location.pp_lift @@ decl.Region.region)
] in
error ~data title message
let unsupported_proc_decl decl =
let title () = "procedure declarations" in
let message () =
@ -121,17 +110,6 @@ module Errors = struct
] in
error ~data title message
let unsupported_set_expr expr =
let title () = "set expressions" in
let message () =
Format.asprintf "the set type is not supported yet" in
let expr_loc = Raw.expr_to_region expr in
let data = [
("expr_loc",
fun () -> Format.asprintf "%a" Location.pp_lift @@ expr_loc)
] in
error ~data title message
let unsupported_proc_calls call =
let title () = "procedure calls" in
let message () =
@ -762,8 +740,6 @@ and simpl_declaration : Raw.declaration -> declaration Location.wrap result =
)
| LambdaDecl (ProcDecl decl) ->
fail @@ unsupported_proc_decl decl
| LambdaDecl (EntryDecl decl) ->
fail @@ unsupported_entry_decl decl
and simpl_statement : Raw.statement -> (_ -> expression result) result =
fun s ->