Merge branch 'rinderknecht-dev' into 'dev'

Getting current front-ends closer

See merge request ligolang/ligo!56
This commit is contained in:
Gabriel Alfour 2019-07-30 17:10:14 +00:00
commit 80fd970ba4
32 changed files with 6493 additions and 441 deletions

View File

@ -0,0 +1,296 @@
type region
type 'a reg
type lexeme = string reg
(* Tokens *)
type integer = [`Integer of lexeme reg]
type natural = [`Natural of lexeme reg]
type ident = [`Ident of lexeme reg]
type uident = [`Uident of lexeme reg]
type chr = [`Chr of lexeme reg]
type str = [`Str of lexeme reg]
type bool_or = [`bool_or of lexeme reg]
type bool_and = [`bool_and of lexeme reg]
type lt = [`lt of lexeme reg]
type le = [`le of lexeme reg]
type gt = [`gt of lexeme reg]
type ge = [`ge of lexeme reg]
type eq = [`eq of lexeme reg]
type ne = [`ne of lexeme reg]
type cat = [`cat of lexeme reg]
type cons = [`cons of lexeme reg]
type plus = [`plus of lexeme reg]
type minus = [`minus of lexeme reg]
type times = [`times of lexeme reg]
type slash = [`slash of lexeme reg]
type div = [`div of lexeme reg]
type kwd_mod = [`kwd_mod of lexeme reg]
type uminus = [`uminus of lexeme reg]
type kwd_not = [`kwd_not of lexeme reg]
type lpar = [`lpar of lexeme reg]
type rpar = [`rpar of lexeme reg]
type lbracket = [`lbracket of lexeme reg]
type rbracket = [`rbracket of lexeme reg]
type lbrace = [`lbrace of lexeme reg]
type rbrace = [`rbrace of lexeme reg]
type semi = [`semi of lexeme reg]
type comma = [`comma of lexeme reg]
type colon = [`colon of lexeme reg]
type vbar = [`vbar of lexeme reg]
type arrow = [`arrow of lexeme reg]
type wild = [`wild of lexeme reg]
type kwd_and = [`kwd_and of lexeme reg]
type kwd_begin = [`kwd_begin of lexeme reg]
type kwd_else = [`kwd_else of lexeme reg]
type kwd_end = [`kwd_end of lexeme reg]
type kwd_false = [`kwd_false of lexeme reg]
type kwd_fun = [`kwd_fun of lexeme reg]
type kwd_if = [`kwd_if of lexeme reg]
type kwd_in = [`kwd_in of lexeme reg]
type kwd_let = [`kwd_let of lexeme reg]
type kwd_list = [`kwd_list of lexeme reg]
type kwd_map = [`kwd_map of lexeme reg]
type kwd_match = [`kwd_match of lexeme reg]
type kwd_of = [`kwd_of of lexeme reg]
type kwd_set = [`kwd_set of lexeme reg]
type kwd_then = [`kwd_then of lexeme reg]
type kwd_true = [`kwd_true of lexeme reg]
type kwd_type = [`kwd_type of lexeme reg]
type kwd_with = [`kwd_with of lexeme reg]
type token =
Integer of integer
| Natural of natural
| Ident of ident
| Uident of uident
| Chr of chr
| Str of str
| Bool_or of bool_or
| Bool_and of bool_and
| Lt of lt
| Le of le
| Gt of gt
| Ge of ge
| Eq of eq
| Ne of ne
| Cat of cat
| Cons of cons
| Plus of plus
| Minus of minus
| Times of times
| Slash of slash
| Div of div
| Kwd_mod of kwd_mod
| Uminus of uminus
| Kwd_not of kwd_not
| Lpar of lpar
| Rpar of rpar
| Lbracket of lbracket
| Rbracket of rbracket
| Lbrace of lbrace
| Rbrace of rbrace
| Semi of semi
| Comma of comma
| Colon of colon
| Vbar of vbar
| Arrow of arrow
| Wild of wild
| Kwd_and of kwd_and
| Kwd_begin of kwd_begin
| Kwd_else of kwd_else
| Kwd_end of kwd_end
| Kwd_false of kwd_false
| Kwd_fun of kwd_fun
| Kwd_if of kwd_if
| Kwd_in of kwd_in
| Kwd_let of kwd_let
| Kwd_list of kwd_list
| Kwd_map of kwd_map
| Kwd_match of kwd_match
| Kwd_of of kwd_of
| Kwd_set of kwd_set
| Kwd_then of kwd_then
| Kwd_true of kwd_true
| Kwd_type of kwd_type
| Kwd_with of kwd_with
(* The following are meant to be part of a library *)
type 'item seq = 'item list
type 'item nseq = 'item * 'item seq
type ('item,'sep) nsepseq = 'item * ('sep * 'item) list
type ('item,'sep) sepseq = ('item,'sep) nsepseq option
type ('item,'sep) sep_or_term_list =
('item,'sep) nsepseq * 'sep option
(* The following are specific to the present grammar *)
type 'item list_of__rec_0 = {
lbracket__1 : lbracket;
list_of__rec_0__2 : ('item, semi) nsepseq;
rbracket__3 : rbracket
}
type 'item list_of = [`List of 'item list_of__rec_0]
type 'item tuple__rec_0 = {
item__1 : 'item;
comma__2 : comma;
tuple__rec_0__3 : ('item, comma) nsepseq
}
type 'item tuple = [`Tuple of 'item tuple__rec_0]
type 'item par__rec_0 = {
lpar__1 : lpar;
item__2 : 'item;
rpar__3 : rpar
}
type 'item par = [`Par of 'item par__rec_0]
(* Non-recursive value declarations *)
type sub_irrefutable = [
`P_Var of string
| `P_Wild
| `P_Unit
| closed_irrefutable par
]
and closed_irrefutable = [
sub_irrefutable tuple
| `P_SubI of sub_irrefutable (* `P_SubI necessary *)
]
type irrefutable = [
sub_irrefutable tuple
| sub_irrefutable
]
type let_binding__rec_1 = {
variable__1 : variable;
sub_irrefutable__nseq__2 : sub_irrefutable nseq;
eq__3 : eq;
expr__4 : expr
}
type let_binding__rec_2 = {
irrefutable__1 : irrefutable;
eq__2 : eq;
expr__3 : expr
}
type let_binding = [
`LetFun of let_binding__rec_1
| `LetNonFun of let_binding__rec_2 (* `LetNonFun necessary *)
]
type let_bindings = (let_binding, kwd_and) nsepseq
type let_declarations = {
kwd_let : kwd_let;
let_bindings : let_bindings
}
(*
type pattern = [
`P_Cons of {sub_pattern: sub_pattern; cons: cons; tail: tail}
| `P_Tuple
*)
(* Type declarations *)
type type_name = ident
type field_name = ident
type constr = uident
type type_constr = [
`T_Constr of ident
| kwd_set
| kwd_map
| kwd_list
]
type record_type = {
lbrace : lbrace;
record_type__2 : (field_decl, semi) sep_or_term_list;
rbrace : rbrace
}
and field_decl = {
field_name : field_name;
colon : colon;
type_expr : type_expr
}
and variant = {
constr : constr;
kwd_of : kwd_of;
cartesian : cartesian
}
and sum_type = {
vbar_opt : vbar option;
sum_type__2 : (variant, vbar) nsepseq
}
and type_param__rec_1 = {
core_type : core_type;
type_constr : type_constr
}
and type_param = [
(type_expr, comma) nsepseq par
| `T_App of type_param__rec_1
]
and core_type__rec_1 = {
type_param : type_param;
type_constr : type_constr
}
and core_type = [
`T_Alias of type_name
| `T_App of core_type__rec_1
| cartesian par
]
and fun_type__rec_0 = {
core_type : core_type;
arrow : arrow;
fun_type : fun_type
}
and fun_type = [
`T_Fun of fun_type__rec_0
| `T_Core of core_type (* `T_Core necessary *)
]
and cartesian = (fun_type, times) nsepseq
and type_expr = [
`T_Prod of cartesian
| `T_Sum of sum_type
| `T_Record of record_type
]
type type_declaration = {
kwd_type__1 : kwd_type;
type_name__2 : type_name;
eq__3 : eq;
type_expr__4 : type_expr
}
(* Entry *)
type statement = [
`Let of let_declarations
| `TypeDecl of type_declaration
]
type program = statement list

View File

@ -0,0 +1,270 @@
(* Extended Backus-Naur Form (EBNF) for Mini-ML *)
(* LEXIS *)
let nl = ['\n' '\r']
let blank = [' ' '\t']
let digit = ['0'-'9']
let natural = digit | digit (digit | '_')* digit
let integer = '-'? natural
let small = ['a'-'z']
let capital = ['A'-'Z']
let letter = small | capital
let ichar = letter | digit | ['_' '\'']
let ident = small ichar* | '_' ichar+
let uident = capital ichar*
let hexa = digit | ['A'-'F']
let byte = hexa hexa
let esc = "\\n" | "\\\\" | "\\b" | "\\r" | "\\t"
let string
let char_set = [^'\'' '\\'] # nl
| "\\'" | esc | "\\x" byte | "\\0" digit digit
let char = "'" char_set "'"
(* SYNTAX *)
(* Helpers *)
(* The following are meant to be part of a library *)
sep_or_term_list<item,sep> ::=
item sep ...
| (item sep)+
seq<item> ::= nseq<item>?
nseq<item> ::= item seq<item>
nsepseq<item,sep> ::=
item
| item sep nsepseq<item,sep>
sepseq<item,sep> ::= nsepseq<item,sep>?
(* The following are specific to the present grammar *)
list_of<item> ::= "[" item ";" ... "]"
csv<item> ::= item "," item "," ...
(* Entry *)
program ::= statement* EOF
statement ::=
let_declarations
| type_declaration
(* Type declarations *)
type_declaration ::= "type" type_name "=" type_expr
type_name == ident
type_expr ::=
cartesian
| sum_type
| record_type
cartesian ::= fun_type "*" ...
fun_type ::=
core_type "->" fun_type
| core_type
core_type ::=
type_name
| type_param type_constr
| "(" cartesian ")"
type_param ==
core_type type_constr
| type_tuple type_constr
type_constr == type_name
type_tuple ::= "(" type_expr "," ... ")"
sum_type ::= variant "|" ...
variant ::= constr "of" cartesian
constr == uident
record_type ::=
"{" sep_or_term_list<field_decl, ";"> "}"
field_decl ::= field_name ":" type_expr
field_name == ident
(* Non-recursive value declarations *)
let_declarations ::= "let" let_bindings
let_bindings := let_binding "and" ...
let_binding ::=
value_name pattern+ "=" expr
| let_lhs "=" expr
value_name == ident
(* Patterns *)
let_lhs ::=
pattern "::" cons_pat
| pattern "," pattern "," ...
| core_pattern
core_pattern ::=
variable
| "_"
| "(" ")"
| number
| "true"
| "false"
| string
| list_of<cons_pat>
| "(" ptuple ")"
| constr core_pattern
variable == ident
number == int
ptuple ::= csv<cons_pat>
unit ::= "(" ")"
cons_pat ::=
pattern "::" cons_pat
| pattern
pattern ::=
"(" cons_pat ")"
| core_pattern
(* Expressions *)
expr ::=
base_cond__open<expr>
| match_expr<base_cond>
base_cond__open<x> ::=
base_expr<x>
| conditional<x>
base_cond ::= base_cond__open<base_cond>
base_expr<right_expr> ::=
let_expr<right_expr>
| fun_expr<right_expr>
| csv<op_expr>
| op_expr
conditional<right_expr> ::=
if_then_else<right_expr>
| if_then<right_expr>
if_then<right_expr> ::= "if" expr "then" right_expr
if_then_else<right_expr> ::=
"if" expr "then" closed_if "else" right_expr
base_if_then_else__open<x> ::=
base_expr<x>
| if_then_else<x>
base_if_then_else ::=
base_if_then_else__open<base_if_then_else>
closed_if ::=
base_if_then_else__open<closed_if>
| match_expr<base_if_then_else>
match_expr<right_expr> ::=
"match" expr "with" cases<right_expr>
cases<right_expr> ::=
case<right_expr>
| cases<base_cond> "|" case<right_expr>
case<right_expr> ::= let_lhs "->" right_expr
let_in<right_expr> ::= "let" par_let "in" right_expr
fun_expr<right_expr> ::= "fun" pattern+ "->" right_expr
op_expr ::=
op_expr "||" conj_expr
| conj_expr
conj_expr ::=
conj_expr "&&" comp_expr
| comp_expr
comp_expr ::=
comp_expr "<" cat_expr
| comp_expr "<=" cat_expr
| comp_expr ">" cat_expr
| comp_expr ">=" cat_expr
| comp_expr "=" cat_expr
| comp_expr "<>" cat_expr
| cat_expr
cat_expr ::=
cons_expr "^" cat_expr
| cons_expr
cons_expr ::=
add_expr "::" cons_expr
| add_expr
add_expr ::=
add_expr "+" mult_expr
| add_expr "-" mult_expr
| mult_expr
mult_expr ::=
mult_expr "*" unary_expr
| mult_expr "div" unary_expr
| mult_expr "mod" unary_expr
| unary_expr
unary_expr ::=
"-" core_expr
| "not" core_expr
| call_expr
call_expr ::=
call_expr core_expr
| core_expr
core_expr ::=
number
| module_name "." variable
| string
| char
| "()"
| "false"
| "true"
| list_of<expr>
| "(" expr ")"
| constr
| sequence
| record_expr
module_name == uident
record_expr ::=
"{" sep_or_term_list(field_assignment,";") "}"
field_assignment ::= field_name "=" expr
sequence ::= "begin" (expr ";" ...)? "end"

View File

@ -0,0 +1,270 @@
(* Extended Backus-Naur Form (EBNF) for Mini-ML *)
(* LEXIS *)
let nl = ['\n' '\r']
let blank = [' ' '\t']
let digit = ['0'-'9']
let natural = digit | digit (digit | '_')* digit
token int = '-'? natural
let small = ['a'-'z']
let capital = ['A'-'Z']
let letter = small | capital
let ichar = letter | digit | ['_' '\'']
token ident = small ichar* | '_' ichar+
token uident = capital ichar*
let esc = "\\n" | "\\\\" | "\\b" | "\\r" | "\\t"
token string
let hexa = digit | ['A'-'F']
let byte = hexa hexa
let char_set = [^'\'' '\\'] # nl
| "\\'" | esc | "\\x" byte | "\\0" digit digit
token char = "'" char_set "'"
(* SYNTAX *)
(* Helpers *)
(* The following are meant to be part of a library *)
sep_or_term_list<item,sep> ::=
item sep ...
| (item sep)+
seq<item> ::= nseq<item>?
nseq<item> ::= item seq<item>
nsepseq<item,sep> ::=
item
| item sep nsepseq<item,sep>
sepseq<item,sep> ::= nsepseq<item,sep>?
(* The following are specific to the present grammar *)
list_of<item> ::= "[" item ";" ... "]"
csv<item> ::= item "," item "," ...
(* Entry *)
program ::= statement* EOF
statement ::=
let_declarations
| type_declaration
(* Type declarations *)
type_declaration ::= "type" type_name "=" type_expr
type_name == ident
type_expr ::=
cartesian
| sum_type
| record_type
cartesian ::= fun_type "*" ...
fun_type ::=
core_type "->" fun_type
| core_type
core_type ::=
type_name
| type_param type_constr
| "(" cartesian ")"
type_param ==
core_type type_constr
| type_tuple type_constr
type_constr == type_name
type_tuple ::= "(" type_expr "," ... ")"
sum_type ::= variant "|" ...
variant ::= constr "of" cartesian
constr == uident
record_type ::=
"{" sep_or_term_list<field_decl,";"> "}"
field_decl ::= field_name ":" type_expr
field_name == ident
(* Non-recursive value declarations *)
let_declarations ::= "let" let_bindings
let_bindings := let_binding "and" ...
let_binding ::=
value_name pattern+ "=" expr
| let_lhs "=" expr
value_name == ident
(* Patterns *)
let_lhs ::=
pattern "::" cons_pat
| pattern "," pattern "," ...
| core_pattern
core_pattern ::=
variable
| "_"
| "(" ")"
| number
| "true"
| "false"
| string
| list_of<cons_pat>
| "(" ptuple ")"
| constr core_pattern
variable == ident
number == int
ptuple ::= csv<cons_pat>
unit ::= "(" ")"
cons_pat ::=
pattern "::" cons_pat
| pattern
pattern ::=
"(" cons_pat ")"
| core_pattern
(* Expressions *)
expr ::=
base_cond__open<expr>
| match_expr<base_cond>
base_cond__open<x> ::=
base_expr<x>
| conditional<x>
base_cond ::= base_cond__open<base_cond>
base_expr<right_expr> ::=
let_expr<right_expr>
| fun_expr<right_expr>
| csv<op_expr>
| op_expr
conditional<right_expr> ::=
if_then_else<right_expr>
| if_then<right_expr>
if_then<right_expr> ::= "if" expr "then" right_expr
if_then_else<right_expr> ::=
"if" expr "then" closed_if "else" right_expr
base_if_then_else__open<x> ::=
base_expr<x>
| if_then_else<x>
base_if_then_else ::=
base_if_then_else__open<base_if_then_else>
closed_if ::=
base_if_then_else__open<closed_if>
| match_expr<base_if_then_else>
match_expr<right_expr> ::=
"match" expr "with" cases<right_expr>
cases<right_expr> ::=
case<right_expr>
| cases<base_cond> "|" case<right_expr>
case<right_expr> ::= let_lhs "->" right_expr
let_in<right_expr> ::= "let" par_let "in" right_expr
fun_expr<right_expr> ::= "fun" pattern+ "->" right_expr
op_expr ::=
op_expr "||" conj_expr
| conj_expr
conj_expr ::=
conj_expr "&&" comp_expr
| comp_expr
comp_expr ::=
comp_expr "<" cat_expr
| comp_expr "<=" cat_expr
| comp_expr ">" cat_expr
| comp_expr ">=" cat_expr
| comp_expr "=" cat_expr
| comp_expr "<>" cat_expr
| cat_expr
cat_expr ::=
cons_expr "^" cat_expr
| cons_expr
cons_expr ::=
add_expr "::" cons_expr
| add_expr
add_expr ::=
add_expr "+" mult_expr
| add_expr "-" mult_expr
| mult_expr
mult_expr ::=
mult_expr "*" unary_expr
| mult_expr "div" unary_expr
| mult_expr "mod" unary_expr
| unary_expr
unary_expr ::=
"-" core_expr
| "not" core_expr
| call_expr
call_expr ::=
call_expr core_expr
| core_expr
core_expr ::=
number
| module_name "." variable
| string
| char
| "()"
| "false"
| "true"
| list_of<expr>
| "(" expr ")"
| constr
| sequence
| record_expr
module_name == uident
record_expr ::=
"{" sep_or_term_list<field_assignment,";"> "}"
field_assignment ::= field_name "=" expr
sequence ::= "begin" (expr ";" ...)? "end"

View File

@ -0,0 +1,249 @@
(* Extended Backus-Naur Form (EBNF) for Mini-ML *)
(* LEXIS *)
let nl = ['\n' '\r']
let blank = [' ' '\t']
let digit = ['0'-'9']
let natural = digit | digit (digit | '_')* digit
token int = '-'? natural
let small = ['a'-'z']
let capital = ['A'-'Z']
let letter = small | capital
let ichar = letter | digit | ['_' '\'']
token ident = small ichar* | '_' ichar+
token uident = capital ichar*
let esc = "\\n" | "\\\\" | "\\b" | "\\r" | "\\t"
let hexa = digit | ['A'-'F']
let byte = hexa hexa
let char_set = [^'\'' '\\'] # nl
| "\\'" | esc | "\\x" byte | "\\0" digit digit
token char = "'" char_set "'"
token string
(* SYNTAX *)
(* Helpers *)
(* The following are meant to be part of a library *)
sep_or_term_list<item,sep> ::=
item sep etc.
| (item sep)+
seq<item> ::= nseq<item>?
nseq<item> ::= item seq<item>
nsepseq<item,sep> ::=
item
| item sep nsepseq<item,sep>
sepseq<item,sep> ::= nsepseq<item,sep>?
(* The following are specific to the present grammar *)
list_of<item> ::= "[" item ";" etc. "]"
csv<item> ::= item "," item "," etc.
(* Entry *)
program ::= statement*
statement ::=
let_declarations
| type_declaration
(* Type declarations *)
type_declaration ::= "type" type_name "=" type_expr
type_name == ident
type_expr ::=
cartesian
| sum_type
| record_type
cartesian ::= fun_type "*" etc.
fun_type ::=
core_type "->" fun_type
| core_type
core_type ::=
type_name
| type_param type_constr
| "(" cartesian ")"
type_param ==
core_type type_constr
| type_tuple type_constr
type_constr == type_name
type_tuple ::= "(" type_expr "," etc. ")"
sum_type ::= "|"? variant "|" etc.
variant ::= constr "of" cartesian
constr == uident
record_type ::=
"{" sep_or_term_list<field_decl,";"> "}"
field_decl ::= field_name ":" type_expr
field_name == ident
(* Non-recursive value declarations *)
let_declarations ::= "let" let_bindings
let_bindings := let_binding "and" etc.
let_binding ::=
value_name pattern+ "=" expr
| let_lhs "=" expr
value_name == ident
(* Patterns *)
let_lhs ::=
pattern "::" cons_pat
| pattern "," pattern "," etc.
| core_pattern
core_pattern ::=
variable
| "_"
| "(" ")"
| number
| "true"
| "false"
| string
| list_of<cons_pat>
| "(" ptuple ")"
| constr core_pattern
variable == ident
number == int
ptuple ::= csv<cons_pat>
unit ::= "(" ")"
cons_pat ::=
pattern "::" cons_pat
| pattern
pattern ::=
"(" cons_pat ")"
| core_pattern
(* Expressions *)
expr ::=
base_cond__<expr>
| match_expr<base_cond>
base_cond__<x> ::=
base_expr<x>
| conditional<x>
base_cond ::= base_cond__<base_cond>
base_expr<right_expr> ::=
let_expr<right_expr>
| fun_expr<right_expr>
| csv<op_expr>
| op_expr
conditional<right_expr> ::=
if_then_else<right_expr>
| if_then<right_expr>
if_then<right_expr> ::= "if" expr "then" right_expr
if_then_else<right_expr> ::=
"if" expr "then" closed_if "else" right_expr
base_if_then_else__<x> ::=
base_expr<x>
| if_then_else<x>
base_if_then_else ::=
base_if_then_else__<base_if_then_else>
closed_if ::=
base_if_then_else__<closed_if>
| match_expr<base_if_then_else>
match_expr<right_expr> ::=
"match" expr "with" cases<right_expr>
cases<right_expr> ::=
case<right_expr>
| cases<base_cond> "|" case<right_expr>
case<right_expr> ::= let_lhs "->" right_expr
let_in<right_expr> ::= "let" par_let "in" right_expr
fun_expr<right_expr> ::= "fun" pattern+ "->" right_expr
op_expr ::=
op_expr "||" %left %prec1 op_expr
| op_expr "&&" %left %prec2 op_expr
| op_expr "<" %left %prec3 op_expr
| op_expr "<=" %left %prec3 op_expr
| op_expr ">" %left %prec3 op_expr
| op_expr ">=" %left %prec3 op_expr
| op_expr "=" %left %prec3 op_expr
| op_expr "<>" %left %prec3 op_expr
| op_expr "^" %right %prec4 op_expr
| op_expr "::" %right %prec5 op_expr
| op_expr "+" %left %prec6 op_expr
| op_expr "-" %left %prec6 op_expr
| op_expr "*" %left %prec7 op_expr
| op_expr "div" %left %prec7 op_expr
| op_expr "mod" %left %prec7 op_expr
| "-" %prec8 op_expr
| "not" %prec8 op_expr
| call_expr
call_expr ::=
call_expr core_expr
| core_expr
core_expr ::=
number
| module_name "." variable
| string
| char
| "()"
| "false"
| "true"
| list_of<expr>
| "(" expr ")"
| constr
| sequence
| record_expr
module_name == uident
record_expr ::=
"{" sep_or_term_list<field_assignment,";"> "}"
field_assignment ::= field_name "=" expr
sequence ::= "begin" sep_or_term_list<expr,";">? "end"

View File

@ -0,0 +1,336 @@
(* Extended Backus-Naur Form (EBNF) for Mini-ML *)
(* LEXIS *)
let digit = ['0'-'9']
let natural = digit | digit (digit | '_')* digit
%token integer = '-'? natural
%token natural = natural 'n'
let small = ['a'-'z']
let capital = ['A'-'Z']
let letter = small | capital
let ichar = letter | digit | ['_' '\'']
%token ident = small ichar* | '_' ichar+
%token uident = capital ichar*
let esc = "\\n" | "\\\\" | "\\b" | "\\r" | "\\t"
let hexa = digit | ['A'-'F']
let byte = hexa hexa
let char_set = [^'\'' '\\'] # nl
| "\\'" | esc | "\\x" byte | "\\0" digit digit
%token chr = "'" char_set "'"
%token str
%token bool_or = "||" %left %prec1
%token bool_and = "&&" %left %prec2
%token lt = "<" %left %prec3
%token le = "<=" %left %prec3
%token gt = ">" %left %prec3
%token ge = ">=" %left %prec3
%token eq = "=" %left %prec3
%token ne = "<>" %left %prec3
%token cat = "^" %right %prec4
%token cons = "::" %right %prec5
%token plus = "+" %left %prec6
%token minus = "-" %left %prec6
%token times = "*" %left %prec7
%token slash = "/" %left %prec7
%token kwd_div = "div" %left %prec7
%token kwd_mod = "mod" %left %prec7
%token uminus = "-" %prec8
%token kwd_not = "not" %prec8
%token lpar = "("
%token rpar = ")"
%token lbracket = "["
%token rbracket = "]"
%token lbrace = "{"
%token rbrace = "}"
%token semi = ";"
%token comma = ","
%token colon = ":"
%token vbar = "|"
%token arrow = "->"
%token wild = "_"
(* SYNTAX *)
(* Helpers *)
(* The following are meant to be part of a library *)
%ocaml "Utils"
type 'item seq = 'item list
type 'item nseq = 'item * 'item seq
type ('item,'sep) nsepseq = 'item * ('sep * 'item) list
type ('item,'sep) sepseq = ('item,'sep) nsepseq option
type ('item,'sep) sep_or_term_list =
('item,'sep) nsepseq * 'sep option
%end
%menhir_decl "Parser"
%start program interactive_expr
%type <AST.t> program
%type <AST.expr> interactive_expr
%type <('item,'sep) sep_or_term_list> sep_or_term_list
%end
%menhir_rule "Parser"
seq(item):
(**) { [] }
| X seq(item) { $1::$2 }
nseq(item):
item seq(item) { $1,$2 }
nsepseq(item,sep):
item { $1, [] }
| item sep nsepseq(item,sep) { let h,t = $3 in $1, ($2,h)::t }
sepseq(item,sep):
(**) { None }
| nsepseq(item,sep) { Some $1 }
sep_or_term_list(item,sep):
nsepseq(item,sep) {
$1, None
}
| nseq(item sep {$1,$2}) {
let (first,sep), tail = $1 in
let rec trans (seq, prev_sep as acc) = function
[] -> acc
| (item,next_sep)::others ->
trans ((prev_sep,item)::seq, next_sep) others in
let list, term = trans ([],sep) tail
in (first, List.rev list), Some term }
%end
(* The following are specific to the present grammar *)
list<item> ::= "[" item ";" etc. "]"
tuple<item> ::= item "," item "," etc.
par<item> ::= "(" item ")"
(* Entry *)
program == statement*
statement ::=
let_declarations { `Let }
| type_declaration { `TypeDecl }
(* Type declarations *)
type_declaration == "type" type_name "=" type_expr
type_name == ident
type_expr ::=
cartesian { `T_Prod }
| sum_type { `T_Sum }
| record_type { `T_Record }
cartesian == fun_type "*" etc.
fun_type ::=
core_type "->" fun_type { `T_Fun }
| core_type { `T_Core }
core_type ::=
type_name { `T_Alias }
| type_param type_constr { `T_App }
| par<cartesian>
type_param ::=
par<type_expr "," etc.>
| core_type type_constr { `T_App }
type_constr ::=
ident { `T_Constr }
| "set"
| "map"
| "list"
sum_type == "|"? variant "|" etc.
variant == constr "of" cartesian
constr == uident
record_type ==
"{" sep_or_term_list<field_decl,";"> "}"
field_decl == field_name ":" type_expr
field_name == ident
(* Non-recursive value declarations *)
let_declarations == "let" let_bindings
let_bindings == let_binding "and" etc.
let_binding ::=
variable sub_irrefutable+ "=" expr { `LetFun }
| irrefutable "=" expr { `LetNonFun }
(* Patterns *)
irrefutable ::=
tuple<sub_irrefutable> { `P_Tuple }
| sub_irrefutable
sub_irrefutable ::=
variable { `P_Var }
| "_" { `P_Wild }
| unit { `P_Unit }
| par<closed_irrefutable>
closed_irrefutable ::=
tuple<sub_irrefutable>
| sub_irrefutable { `P_SubI }
pattern ::=
sub_pattern "::" tail { `P_Cons }
| tuple<sub_pattern> { `P_Tuple }
| core_pattern { `P_Core }
sub_pattern ::=
par<tail>
| core_pattern { `P_Core }
core_pattern ::=
variable { `P_Var }
| "_" { `P_Wild }
| unit { `P_Unit }
| integer { `P_Int }
| natural { `P_Nat }
| "true" { `P_True }
| "false" { `P_False }
| str { `P_Str }
| chr { `P_Chr }
| list<tail> { `P_List }
| constr sub_pattern { `P_Constr }
| record_pattern { `P_Record }
| par<tuple<tail>>
variable == ident
record_pattern ::=
"{" sep_or_term_list<field_pattern,";"> "}"
field_pattern ::= field_name "=" sub_pattern
unit ::= "(" ")"
tail ::=
sub_pattern "::" tail
| sub_pattern
(* Expressions *)
expr ::=
base_cond__<expr>
| match_expr<base_cond>
base_cond__<x> ::=
base_expr<x>
| conditional<x>
base_cond == base_cond__<base_cond>
base_expr<right_expr> ::=
let_expr<right_expr>
| fun_expr<right_expr>
| csv<op_expr>
conditional<right_expr> ::=
if_then_else<right_expr>
| if_then<right_expr>
if_then<right_expr> ::=
"if" expr "then" right_expr { `IfThen }
if_then_else<right_expr> ::=
"if" expr "then" closed_if "else" right_expr { `IfThenElse }
base_if_then_else__<x> ::=
base_expr<x>
| if_then_else<x>
base_if_then_else ::=
base_if_then_else__<base_if_then_else>
closed_if ::=
base_if_then_else__<closed_if>
| match_expr<base_if_then_else>
match_expr<right_expr> ::=
"match" expr "with" cases<right_expr>
cases<right_expr> ::=
case<right_expr>
| cases<base_cond> "|" case<right_expr>
case<right_expr> ::= pattern "->" right_expr
let_in<right_expr> ::= "let" par_let "in" right_expr
fun_expr<right_expr> ::= "fun" sub_pattern+ "->" right_expr
op_expr ::=
op_expr "||" op_expr
| op_expr "&&" op_expr
| op_expr "<" op_expr
| op_expr "<=" op_expr
| op_expr ">" op_expr
| op_expr ">=" op_expr
| op_expr "=" op_expr
| op_expr "<>" op_expr
| op_expr "^" op_expr
| op_expr "::" op_expr
| op_expr "+" op_expr
| op_expr "-" op_expr
| op_expr "*" op_expr
| op_expr "/" op_expr
| op_expr "div" op_expr
| op_expr "mod" op_expr
| "-" op_expr
| "not" op_expr
| call_expr
call_expr ::=
call_expr core_expr
| core_expr
core_expr ::=
variable
| module_name "." path
| unit
| integer
| natural
| "false"
| "true"
| str
| chr
| constr
| sequence
| record_expr
| list<expr>
| par<expr>
module_name == uident
path == ident "." etc.
record_expr ::=
"{" sep_or_term_list<field_assignment,";"> "}"
field_assignment ::= field_name "=" expr
sequence ::= "begin" sep_or_term_list<expr,";">? "end"

View File

@ -1,12 +1,9 @@
(* Parsing the command-line option for the Mini-ML compiler/interpreter *)
(* Parsing the command-line option for CameLIGO *)
type options = {
input : string option;
eval : bool;
compile : string option;
libs : string list;
verbose : Utils.String.Set.t;
raw_edits : bool
verbose : Utils.String.Set.t
}
let abort msg =
@ -14,22 +11,19 @@ let abort msg =
let printf = Printf.printf
let sprintf = Printf.sprintf
let print = print_endline
(* Help *)
let help () =
let file = Filename.basename Sys.argv.(0) in
printf "Usage: %s [<option> ...] [<input>.ml | \"-\"]\n" file;
print_endline "where <input>.mml is the Mini-ML source file (default: stdin),";
print_endline "and each <option> (if any) is one of the following:";
print_endline " -I <paths> Library paths (colon-separated)";
print_endline " -c [<file>.ml] Translate to OCaml in <file>.ml";
print_endline " (default: <input>.ml)";
print_endline " -e, --eval Interpret <input>.mml or stdin";
print_endline " --raw-edits Do not optimise translation edits";
print_endline " --verbose=<phases> Colon-separated phases: cmdline, lexer, parser";
print_endline " --version Short commit hash on stdout";
print_endline " -h, --help This help";
printf "Usage: %s [<option> ...] [<input>.mligo | \"-\"]\n" file;
print "where <input>.mligo is the CameLIGO source file (default: stdin),";
print "and each <option> (if any) is one of the following:";
print " -I <paths> Library paths (colon-separated)";
print " --verbose=<phases> Colon-separated phases: cmdline, lexer, parser";
print " --version Send short commit hash to stdout";
print " -h, --help This help";
exit 0
(* Version *)
@ -39,16 +33,9 @@ let version () = printf "%s\n" Version.version; exit 0
(* Specifying the command-line options a la GNU *)
let input = ref None
and eval = ref false
and compile = ref None
and verbose = ref Utils.String.Set.empty
and libs = ref []
and raw_edits = ref false
let verb_str = ref ""
let set_opt var err =
Some (fun x -> if !var = None then var := Some x else raise (Getopt.Error err))
and verb_str = ref ""
let split_at_colon = Str.(split (regexp ":"))
@ -62,10 +49,6 @@ let add_verbose d =
let specs =
let open! Getopt in [
'I', nolong, None, Some add_path;
'c', nolong, set compile (Some ""),
set_opt compile "Multiple OCaml outputs";
'e', "eval", set eval true, None;
noshort, "raw-edits", set raw_edits true, None;
noshort, "verbose", None, Some add_verbose;
'h', "help", Some help, None;
noshort, "version", Some version, None
@ -94,9 +77,6 @@ let quote s = Printf.sprintf "\"%s\"" s
let print_opt () =
printf "COMMAND LINE\n";
printf "input = %s\n" (string_of quote !input);
printf "compile = %s\n" (string_of quote !compile);
printf "eval = %B\n" !eval;
printf "raw_edits = %b\n" !raw_edits;
printf "verbose = %s\n" !verb_str;
printf "libs = %s\n" (string_of_path !libs)
@ -106,50 +86,29 @@ let check () =
let input =
match !input with
None | Some "-" ->
if !compile <> None then
abort "An input file is missing (for compilation)."
else !input
None | Some "-" -> !input
| Some file_path ->
if Filename.check_suffix file_path ".mml"
if Filename.check_suffix file_path ".mligo"
then if Sys.file_exists file_path
then Some file_path
else abort "Source file not found."
else abort "Source file lacks the extension .mml." in
let compile =
match !compile with
Some _ when !eval -> abort "Options -e and -c are mutually exclusive."
| None | Some "-" -> !compile
| Some "" ->
(match input with
None | Some "-" -> abort "The target OCaml filename is missing."
| Some file -> Some (Filename.remove_extension file ^ ".ml"))
| Some compile' ->
if Filename.check_suffix compile' ".ml"
then !compile
else abort "The extension of the target OCaml file is not .ml" in
else abort "Source file lacks the extension .mligo." in
(* Exporting remaining options as non-mutable values *)
let eval = !eval
and verbose = !verbose
and libs = !libs
and raw_edits = !raw_edits in
let verbose = !verbose
and libs = !libs in
let () =
if Utils.String.Set.mem "cmdline" verbose then
begin
printf "\nEXPORTED COMMAND LINE\n";
printf "input = %s\n" (string_of quote input);
printf "compile = %s\n" (string_of quote compile);
printf "eval = %B\n" eval;
printf "raw_edits = %B\n" raw_edits;
printf "verbose = %s\n" !verb_str;
printf "I = %s\n" (string_of_path libs)
printf "libs = %s\n" (string_of_path libs)
end
in {input; eval; compile; libs; verbose; raw_edits}
in {input; libs; verbose}
(* Parsing the command-line options *)

View File

@ -1,24 +1,23 @@
(* Command-line options for the Mini-ML compiler/interpreter *)
(* Command-line options for CameLIGO *)
(* If the value of [input] is [Some src], the name of the Mini-ML
source file, with the extension ".mml", is [src]. If [input] is
[Some "-"] or [None], the source file is read from standard
input. *)
(* The type [options] gathers the command-line options.
(* The Mini-ML source file can be processed in two mutually exclusive
manners: if the value [eval] is set to [true], the source is
interpreted; if the value [compile] is not [None], the source is
compiled to OCaml; if [eval] is [false] and [compile] is [None],
nothing is done with the source. Note: if [compile] is [Some "-"],
the compiled code is sent to standard output. *)
If the field [input] is [Some src], the name of the CameLIGO
source file, with the extension ".mligo", is [src]. If [input] is
[Some "-"] or [None], the source file is read from standard input.
The field [libs] is made of library paths (colon-separated).
The field [verbose] is a set of stages of the compiler chain,
about which more information may be displayed.
*)
type options = {
input : string option;
eval : bool;
compile : string option;
libs : string list;
verbose : Utils.String.Set.t;
raw_edits : bool
}
(* Parsing the command-line options on stdin *)
val read : unit -> options

View File

@ -1,12 +1,12 @@
(* Driver for the lexer of Mini-ML *)
(* Driver for the lexer of CameLIGO *)
(* Error printing and exception tracing *)
Printexc.record_backtrace true;;
let () = Printexc.record_backtrace true
(* Running the lexer on the source *)
let options = EvalOpt.read ();;
let options = EvalOpt.read ()
open EvalOpt;;

View File

@ -3,47 +3,8 @@
open AST
(* Rewrite "let pattern = e" as "let x = e;; let x1 = ...;; let x2 = ...;;" *)
(*
module VMap = Utils.String.Map
let ghost_of value = Region.{region=ghost; value}
*)
let ghost = Region.ghost
(* let fail_syn_unif type1 type2 : 'a =
let reg = AST.region_of_type_expr type1 in
let reg = reg#compact ~file:false `Byte in
let value =
Printf.sprintf "Unification with %s is not\
implemented." reg in
let region = AST.region_of_type_expr type2 in
let err = Region.{value; region} in
(Lexer.prerr ~kind:"Syntactical" err; exit 1)
let mk_component rank =
let num = string_of_int rank, Z.of_int rank in
let par = {lpar=ghost; inside = ghost_of num; rpar=ghost}
in Component (ghost_of par)
let rec mk_field_path (rank, tail) =
let head = mk_component rank in
match tail with
[] -> head, []
| hd::tl -> mk_field_path (hd,tl) |> Utils.nsepseq_cons head ghost
let mk_projection fresh (path : int Utils.nseq) = {
struct_name = fresh;
selector = ghost;
field_path = Utils.nsepseq_rev (mk_field_path path)
} *)
(* We rewrite "fun p -> e" into "fun x -> match x with p -> e" *)
(* END HEADER *)
%}
@ -178,7 +139,7 @@ tuple(item):
(* Possibly empty semicolon-separated values between brackets *)
list_of(item):
list(item):
lbracket sep_or_term_list(item,semi) rbracket {
let elements, terminator = $2 in {
opening = LBracket $1;
@ -360,7 +321,7 @@ core_pattern:
| kwd(False) { PFalse $1 }
| string { PString $1 }
| par(ptuple) { PPar $1 }
| reg(list_of(tail)) { PList (Sugar $1) }
| reg(list(tail)) { PList (Sugar $1) }
| reg(constr_pattern) { PConstr $1 }
| reg(record_pattern) { PRecord $1 }
@ -608,7 +569,7 @@ core_expr:
| unit { EUnit $1 }
| kwd(False) { ELogic (BoolExpr (False $1)) }
| kwd(True) { ELogic (BoolExpr (True $1)) }
| reg(list_of(expr)) { EList (List $1) }
| reg(list(expr)) { EList (List $1) }
| par(expr) { EPar $1 }
| reg(sequence) { ESeq $1 }
| reg(record_expr) { ERecord $1 }

View File

@ -1,8 +1,8 @@
(* Driver for the parser of Mini-ML *)
(* Driver for the parser of CameLIGO *)
(* Error printing and exception tracing *)
Printexc.record_backtrace true;;
let () = Printexc.record_backtrace true
(* Reading the command-line options *)

View File

@ -0,0 +1,433 @@
option(X) :=
(**)
| X
sep_or_term_list(item,sep) ::=
nsepseq(item,sep)
| nseq(item sep)
(* Compound constructs *)
par(X) ::= LPAR X RPAR
brackets(X) ::= LBRACKET X RBRACKET
(* Sequences *)
(* Possibly empty sequence of items *)
seq(X) ::=
(**)
| X seq(X)
(* Non-empty sequence of items *)
nseq(X) ::= X seq(X)
(* Non-empty separated sequence of items *)
nsepseq(X,Sep) ::=
X
| X Sep nsepseq(X,Sep)
(* Possibly empy separated sequence of items *)
sepseq(X,Sep) ::=
(**)
| nsepseq(X,Sep)
(* Inlines *)
var ::= Ident
type_name ::= Ident
fun_name ::= Ident
field_name ::= Ident
struct_name ::= Ident
(* Main *)
contract ::=
nseq(declaration) EOF
declaration ::=
type_decl
| const_decl
| lambda_decl
(* Type declarations *)
type_decl ::=
Type type_name Is type_expr option(SEMI)
type_expr ::=
cartesian
| sum_type
| record_type
cartesian ::=
nsepseq(function_type,TIMES)
function_type ::=
core_type
| core_type ARROW function_type
core_type ::=
type_name
| type_name type_tuple
| Map type_tuple
| Set par(type_expr)
| List par(type_expr)
| par(type_expr)
type_tuple ::=
par(nsepseq(type_expr,COMMA))
sum_type ::=
option(VBAR) nsepseq(variant,VBAR)
variant ::=
Constr Of cartesian
| Constr
record_type ::=
Record sep_or_term_list(field_decl,SEMI) End
| Record LBRACKET sep_or_term_list(field_decl,SEMI) RBRACKET
field_decl ::=
field_name COLON type_expr
(* Function and procedure declarations *)
lambda_decl ::=
fun_decl
| proc_decl
| entry_decl
fun_decl ::=
Function fun_name parameters COLON type_expr Is
seq(local_decl)
block
With expr option(SEMI)
entry_decl ::=
Entrypoint fun_name entry_params COLON type_expr Is
seq(local_decl)
block
With expr option(SEMI)
entry_params ::=
par(nsepseq(entry_param_decl,SEMI))
proc_decl ::=
Procedure fun_name parameters Is
seq(local_decl)
block option(SEMI)
parameters ::=
par(nsepseq(param_decl,SEMI))
param_decl ::=
Var var COLON param_type
| Const var COLON param_type
entry_param_decl ::=
param_decl
| Storage var COLON param_type
param_type ::=
cartesian
block ::=
Begin sep_or_term_list(statement,SEMI) End
| Block LBRACE sep_or_term_list(statement,SEMI) RBRACE
statement ::=
instruction
| open_data_decl
open_data_decl ::=
open_const_decl
| open_var_decl
open_const_decl ::=
Const unqualified_decl(EQUAL)
open_var_decl ::=
Var unqualified_decl(ASS)
local_decl ::=
fun_decl
| proc_decl
| data_decl
data_decl ::=
const_decl
| var_decl
unqualified_decl(OP) ::=
var COLON type_expr OP expr
const_decl ::=
open_const_decl SEMI
| open_const_decl
var_decl ::=
open_var_decl SEMI
| open_var_decl
instruction ::=
single_instr
| block
single_instr ::=
conditional
| case_instr
| assignment
| loop
| proc_call
| fail_instr
| Skip
| record_patch
| map_patch
| set_patch
| map_remove
| set_remove
set_remove ::=
Remove expr From Set path
map_remove ::=
Remove expr From Map path
set_patch ::=
Patch path With injection(Set,expr)
map_patch ::=
Patch path With injection(Map,binding)
injection(Kind,element) ::=
Kind sep_or_term_list(element,SEMI) End
| Kind End
| Kind LBRACKET sep_or_term_list(element,SEMI) RBRACKET
| Kind LBRACKET RBRACKET
binding ::=
expr ARROW expr
record_patch ::=
Patch path With record_expr
fail_instr ::=
Fail expr
proc_call ::=
fun_call
conditional ::=
If expr Then if_clause option(SEMI) Else if_clause
if_clause ::=
instruction
| LBRACE sep_or_term_list(statement,COMMA) RBRACE
case_instr ::=
case(instruction)
case(rhs) ::=
Case expr Of option(VBAR) cases(rhs) End
| Case expr Of LBRACKET option(VBAR) cases(rhs) RBRACKET
cases(rhs) ::=
nsepseq(case_clause(rhs),VBAR)
case_clause(rhs) ::=
pattern ARROW rhs
assignment ::=
lhs ASS rhs
rhs ::=
expr
lhs ::=
path
| map_lookup
loop ::=
while_loop
| for_loop
while_loop ::=
While expr block
for_loop ::=
For var_assign option(Down) To expr option(step_clause) block
| For var option(arrow_clause) In expr block
var_assign ::=
var ASS expr
step_clause ::=
Step expr
arrow_clause ::=
ARROW var
(* Expressions *)
interactive_expr ::=
expr EOF
expr ::=
case(expr)
| annot_expr
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
| disj_expr
disj_expr ::=
disj_expr Or conj_expr
| conj_expr
conj_expr ::=
conj_expr And set_membership
| set_membership
set_membership ::=
core_expr Contains set_membership
| comp_expr
comp_expr ::=
comp_expr LT cat_expr
| comp_expr LEQ cat_expr
| comp_expr GT cat_expr
| comp_expr GEQ cat_expr
| comp_expr EQUAL cat_expr
| comp_expr NEQ cat_expr
| cat_expr
cat_expr ::=
cons_expr CAT cat_expr
| cons_expr
cons_expr ::=
add_expr CONS cons_expr
| add_expr
add_expr ::=
add_expr PLUS mult_expr
| add_expr MINUS mult_expr
| mult_expr
mult_expr ::=
mult_expr TIMES unary_expr
| mult_expr SLASH unary_expr
| mult_expr Mod unary_expr
| unary_expr
unary_expr ::=
MINUS core_expr
| Not core_expr
| core_expr
core_expr ::=
Int
| Nat
| Mtz
| var
| String
| Bytes
| C_False
| C_True
| C_Unit
| tuple_expr
| list_expr
| C_None
| fun_call
| map_expr
| set_expr
| record_expr
| projection
| Constr arguments
| Constr
| C_Some arguments
set_expr ::=
injection(Set,expr)
map_expr ::=
map_lookup
| injection(Map,binding)
map_lookup ::=
path brackets(expr)
path ::=
var
| projection
projection ::=
struct_name DOT nsepseq(selection,DOT)
selection ::=
field_name
| Int
record_expr ::=
Record sep_or_term_list(field_assignment,SEMI) End
| Record LBRACKET sep_or_term_list(field_assignment,SEMI) RBRACKET
field_assignment ::=
field_name EQUAL expr
fun_call ::=
fun_name arguments
tuple_expr ::=
tuple_inj
tuple_inj ::=
par(nsepseq(expr,COMMA))
arguments ::=
tuple_inj
list_expr ::=
injection(List,expr)
| Nil
(* Patterns *)
pattern ::=
nsepseq(core_pattern,CONS)
core_pattern ::=
var
| WILD
| Int
| String
| C_Unit
| C_False
| C_True
| C_None
| list_pattern
| tuple_pattern
| constr_pattern
| C_Some par(core_pattern)
list_pattern ::=
injection(List,core_pattern)
| Nil
| par(cons_pattern)
cons_pattern ::=
core_pattern CONS pattern
tuple_pattern ::=
par(nsepseq(core_pattern,COMMA))
constr_pattern ::=
Constr tuple_pattern
| Constr

View File

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

View File

@ -0,0 +1,418 @@
option(X) :=
(**)
| X
series(item,sep,term) ::=
item after_item(item,sep,term)
after_item(item,sep,term) ::=
sep item_or_closing(item,sep,term)
| term
item_or_closing(item,sep,term) ::=
term
| series(item,sep,term)
(* Compound constructs *)
par(X) ::= LPAR X RPAR
brackets(X) ::= LBRACKET X RBRACKET
(* Sequences *)
(* Possibly empty sequence of items *)
seq(X) ::=
(**)
| X seq(X)
(* Non-empty sequence of items *)
nseq(X) ::= X seq(X)
(* Non-empty separated sequence of items *)
nsepseq(X,Sep) ::=
X
| X Sep nsepseq(X,Sep)
(* Possibly empy separated sequence of items *)
sepseq(X,Sep) ::=
(**)
| nsepseq(X,Sep)
(* Main *)
contract ::=
nseq(declaration) EOF
declaration ::=
type_decl
| const_decl
| lambda_decl
(* Type declarations *)
type_decl ::=
Type Ident (* type_name *) Is type_expr option(SEMI)
type_expr ::=
cartesian
| sum_type
| record_type
cartesian ::=
nsepseq(function_type,TIMES)
function_type ::=
core_type
| core_type ARROW function_type
core_type ::=
Ident (* type_name *)
| Ident (* type_name *) type_tuple
| Map type_tuple
| Set par(type_expr)
| List par(type_expr)
| par(type_expr)
type_tuple ::=
par(nsepseq(type_expr,COMMA))
sum_type ::=
option(VBAR) nsepseq(variant,VBAR)
variant ::=
Constr Of cartesian
| Constr
record_type ::=
Record series(field_decl,SEMI,End)
| Record LBRACKET series(field_decl,SEMI,RBRACKET)
field_decl ::=
Ident (* field_name *) COLON type_expr
(* Function and procedure declarations *)
lambda_decl ::=
fun_decl
| proc_decl
| entry_decl
fun_decl ::=
Function Ident (* fun_name *) parameters COLON type_expr Is
seq(local_decl)
block
With expr option(SEMI)
entry_decl ::=
Entrypoint Ident (* fun_name *) entry_params COLON type_expr Is
seq(local_decl)
block
With expr option(SEMI)
entry_params ::=
par(nsepseq(entry_param_decl,SEMI))
proc_decl ::=
Procedure Ident (* fun_name *) parameters Is
seq(local_decl)
block option(SEMI)
parameters ::=
par(nsepseq(param_decl,SEMI))
param_decl ::=
Var Ident (* var *) COLON param_type
| Const Ident (* var *) COLON param_type
entry_param_decl ::=
param_decl
| Storage Ident (* var *) COLON param_type
param_type ::=
cartesian
block ::=
Begin series(statement,SEMI,End)
| Block LBRACE series(statement,SEMI,RBRACE)
statement ::=
instruction
| open_data_decl
open_data_decl ::=
open_const_decl
| open_var_decl
open_const_decl ::=
Const unqualified_decl(EQUAL)
open_var_decl ::=
Var unqualified_decl(ASS)
local_decl ::=
fun_decl
| proc_decl
| data_decl
data_decl ::=
const_decl
| var_decl
unqualified_decl(OP) ::=
Ident (* var *) COLON type_expr OP expr
const_decl ::=
open_const_decl SEMI
| open_const_decl
var_decl ::=
open_var_decl option(SEMI)
instruction ::=
single_instr
| block
single_instr ::=
conditional
| case_instr
| assignment
| loop
| proc_call
| fail_instr
| Skip
| record_patch
| Patch path With injection(Map,binding)
| Patch path With injection(Set,expr)
| Remove expr From Map path
| Remove expr From Set path
injection(Kind,element) ::=
Kind series(element,SEMI,End)
| Kind End
| Kind LBRACKET series(element,SEMI,RBRACKET)
| Kind LBRACKET RBRACKET
binding ::=
expr ARROW expr
record_patch ::=
Patch path With record_expr
fail_instr ::=
Fail expr
proc_call ::=
fun_call
conditional ::=
If expr Then if_clause option(SEMI) Else if_clause
if_clause ::=
instruction
| LBRACE series(statement,COMMA,RBRACE)
case_instr ::=
case(instruction)
case(rhs) ::=
Case expr Of option(VBAR) cases(rhs) End
| Case expr Of LBRACKET option(VBAR) cases(rhs) RBRACKET
cases(rhs) ::=
nsepseq(case_clause(rhs),VBAR)
case_clause(rhs) ::=
pattern ARROW rhs
assignment ::=
lhs ASS rhs
rhs ::=
expr
lhs ::=
path
| map_lookup
loop ::=
while_loop
| for_loop
while_loop ::=
While expr block
for_loop ::=
For var_assign option(Down) To expr option(step_clause) block
| For Ident (* var *) option(arrow_clause) In expr block
var_assign ::=
Ident (* var *) ASS expr
step_clause ::=
Step expr
arrow_clause ::=
ARROW Ident (* var *)
(* Expressions *)
interactive_expr ::=
expr EOF
expr ::=
case(expr)
| annot_expr
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
| disj_expr
disj_expr ::=
disj_expr Or conj_expr
| conj_expr
conj_expr ::=
conj_expr And set_membership
| set_membership
set_membership ::=
core_expr Contains set_membership
| comp_expr
comp_expr ::=
comp_expr LT cat_expr
| comp_expr LEQ cat_expr
| comp_expr GT cat_expr
| comp_expr GEQ cat_expr
| comp_expr EQUAL cat_expr
| comp_expr NEQ cat_expr
| cat_expr
cat_expr ::=
cons_expr CAT cat_expr
| cons_expr
cons_expr ::=
add_expr CONS cons_expr
| add_expr
add_expr ::=
add_expr PLUS mult_expr
| add_expr MINUS mult_expr
| mult_expr
mult_expr ::=
mult_expr TIMES unary_expr
| mult_expr SLASH unary_expr
| mult_expr Mod unary_expr
| unary_expr
unary_expr ::=
MINUS core_expr
| Not core_expr
| core_expr
core_expr ::=
Int
| Nat
| Mtz
| Ident (* var *)
| String
| Bytes
| C_False
| C_True
| C_Unit
| tuple_expr
| list_expr
| C_None
| fun_call
| map_expr
| set_expr
| record_expr
| projection
| Constr arguments
| Constr
| C_Some arguments
set_expr ::=
injection(Set,expr)
map_expr ::=
map_lookup
| injection(Map,binding)
map_lookup ::=
path brackets(expr)
path ::=
Ident (* var *)
| projection
projection ::=
Ident (* struct_name *) DOT nsepseq(selection,DOT)
selection ::=
Ident (* field_name *)
| Int
record_expr ::=
Record series(field_assignment,SEMI,End)
| Record LBRACKET series(field_assignment,SEMI,RBRACKET)
field_assignment ::=
Ident (* field_name *) EQUAL expr
fun_call ::=
Ident (* fun_name *) arguments
tuple_expr ::=
tuple_inj
tuple_inj ::=
par(nsepseq(expr,COMMA))
arguments ::=
tuple_inj
list_expr ::=
injection(List,expr)
| Nil
(* Patterns *)
pattern ::=
nsepseq(core_pattern,CONS)
core_pattern ::=
Ident (* var *)
| WILD
| Int
| String
| C_Unit
| C_False
| C_True
| C_None
| list_pattern
| tuple_pattern
| constr_pattern
| C_Some par(core_pattern)
list_pattern ::=
injection(List,core_pattern)
| Nil
| par(cons_pattern)
cons_pattern ::=
core_pattern CONS pattern
tuple_pattern ::=
par(nsepseq(core_pattern,COMMA))
constr_pattern ::=
Constr tuple_pattern
| Constr

View File

@ -0,0 +1,393 @@
option(X) :=
(**)
| X
series(item,sep,term) ::=
item after_item(item,sep,term)
after_item(item,sep,term) ::=
sep item_or_closing(item,sep,term)
| term
item_or_closing(item,sep,term) ::=
term
| series(item,sep,term)
(* Compound constructs *)
par(X) ::= LPAR X RPAR
brackets(X) ::= LBRACKET X RBRACKET
(* Sequences *)
(* Possibly empty sequence of items *)
seq(X) ::=
(**)
| X seq(X)
(* Non-empty sequence of items *)
nseq(X) ::= X seq(X)
(* Non-empty separated sequence of items *)
nsepseq(X,Sep) ::=
X
| X Sep nsepseq(X,Sep)
(* Possibly empy separated sequence of items *)
sepseq(X,Sep) ::=
(**)
| nsepseq(X,Sep)
(* Main *)
contract ::=
nseq(declaration) EOF
declaration ::=
type_decl
| const_decl
| lambda_decl
(* Type declarations *)
type_decl ::=
Type Ident (* type_name *) Is type_expr option(SEMI)
type_expr ::=
cartesian
| sum_type
| record_type
cartesian ::=
nsepseq(function_type,TIMES)
function_type ::=
core_type
| core_type ARROW function_type
core_type ::=
Ident (* type_name *)
| Ident (* type_name *) type_tuple
| Map type_tuple
| Set par(type_expr)
| List par(type_expr)
| par(type_expr)
type_tuple ::=
par(nsepseq(type_expr,COMMA))
sum_type ::=
option(VBAR) nsepseq(variant,VBAR)
variant ::=
Constr Of cartesian
| Constr
record_type ::=
Record series(field_decl,SEMI,End)
| Record LBRACKET series(field_decl,SEMI,RBRACKET)
field_decl ::=
Ident (* field_name *) COLON type_expr
(* Function and procedure declarations *)
lambda_decl ::=
fun_decl
| proc_decl
| entry_decl
fun_decl ::=
Function Ident (* fun_name *) parameters COLON type_expr Is
seq(local_decl)
block
With expr option(SEMI)
entry_decl ::=
Entrypoint Ident (* fun_name *) entry_params COLON type_expr Is
seq(local_decl)
block
With expr option(SEMI)
entry_params ::=
par(nsepseq(entry_param_decl,SEMI))
proc_decl ::=
Procedure Ident (* fun_name *) parameters Is
seq(local_decl)
block option(SEMI)
parameters ::=
par(nsepseq(param_decl,SEMI))
param_decl ::=
Var Ident (* var *) COLON param_type
| Const Ident (* var *) COLON param_type
entry_param_decl ::=
param_decl
| Storage Ident (* var *) COLON param_type
param_type ::=
cartesian
block ::=
Begin series(statement,SEMI,End)
| Block LBRACE series(statement,SEMI,RBRACE)
statement ::=
instruction
| open_data_decl
open_data_decl ::=
open_const_decl
| open_var_decl
open_const_decl ::=
Const unqualified_decl(EQUAL)
open_var_decl ::=
Var unqualified_decl(ASS)
local_decl ::=
fun_decl
| proc_decl
| data_decl
data_decl ::=
const_decl
| var_decl
unqualified_decl(OP) ::=
Ident (* var *) COLON type_expr OP expr
const_decl ::=
open_const_decl option(SEMI)
var_decl ::=
open_var_decl option(SEMI)
instruction ::=
single_instr
| block
single_instr ::=
If expr Then if_clause option(SEMI) Else if_clause
| case(instruction)
| path ASS expr
| path brackets(expr) (* map_lookup *) ASS expr
| loop
| proc_call
| Fail expr
| Skip
| Patch path With record_expr
| Patch path With injection(Map,binding)
| Patch path With injection(Set,expr)
| Remove expr From Map path
| Remove expr From Set path
injection(Kind,element) ::=
Kind series(element,SEMI,End)
| Kind End
| Kind LBRACKET series(element,SEMI,RBRACKET)
| Kind LBRACKET RBRACKET
binding ::=
expr ARROW expr
proc_call ::=
fun_call
if_clause ::=
instruction
| LBRACE series(statement,COMMA,RBRACE)
case(rhs) ::=
Case expr Of option(VBAR) cases(rhs) End
| Case expr Of LBRACKET option(VBAR) cases(rhs) RBRACKET
cases(rhs) ::=
nsepseq(case_clause(rhs),VBAR)
case_clause(rhs) ::=
pattern ARROW rhs
loop ::=
while_loop
| for_loop
while_loop ::=
While expr block
for_loop ::=
For var_assign option(Down) To expr option(step_clause) block
| For Ident (* var *) option(arrow_clause) In expr block
var_assign ::=
Ident (* var *) ASS expr
step_clause ::=
Step expr
arrow_clause ::=
ARROW Ident (* var *)
(* Expressions *)
interactive_expr ::=
expr EOF
expr ::=
case(expr)
| annot_expr
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
| disj_expr
disj_expr ::=
disj_expr Or conj_expr
| conj_expr
conj_expr ::=
conj_expr And set_membership
| set_membership
set_membership ::=
core_expr Contains set_membership
| comp_expr
comp_expr ::=
comp_expr LT cat_expr
| comp_expr LEQ cat_expr
| comp_expr GT cat_expr
| comp_expr GEQ cat_expr
| comp_expr EQUAL cat_expr
| comp_expr NEQ cat_expr
| cat_expr
cat_expr ::=
cons_expr CAT cat_expr
| cons_expr
cons_expr ::=
add_expr CONS cons_expr
| add_expr
add_expr ::=
add_expr PLUS mult_expr
| add_expr MINUS mult_expr
| mult_expr
mult_expr ::=
mult_expr TIMES unary_expr
| mult_expr SLASH unary_expr
| mult_expr Mod unary_expr
| unary_expr
unary_expr ::=
MINUS core_expr
| Not core_expr
| core_expr
core_expr ::=
Int
| Nat
| Mtz
| Ident (* var *)
| String
| Bytes
| C_False
| C_True
| C_Unit
| tuple_expr
| list_expr
| C_None
| fun_call
| map_expr
| set_expr
| record_expr
| Ident (* struct_name *) DOT nsepseq(selection,DOT)
| Constr arguments
| Constr
| C_Some arguments
set_expr ::=
injection(Set,expr)
map_expr ::=
map_lookup
| injection(Map,binding)
map_lookup ::=
path brackets(expr)
path ::=
Ident (* var *)
| Ident (* struct_name *) DOT nsepseq(selection,DOT)
selection ::=
Ident (* field_name *)
| Int
record_expr ::=
Record series(field_assignment,SEMI,End)
| Record LBRACKET series(field_assignment,SEMI,RBRACKET)
field_assignment ::=
Ident (* field_name *) EQUAL expr
fun_call ::=
Ident (* fun_name *) arguments
tuple_expr ::=
tuple_inj
tuple_inj ::=
par(nsepseq(expr,COMMA))
arguments ::=
tuple_inj
list_expr ::=
injection(List,expr)
| Nil
(* Patterns *)
pattern ::=
nsepseq(core_pattern,CONS)
core_pattern ::=
Ident (* var *)
| WILD
| Int
| String
| C_Unit
| C_False
| C_True
| C_None
| list_pattern
| tuple_pattern
| constr_pattern
| C_Some par(core_pattern)
list_pattern ::=
injection(List,core_pattern)
| Nil
| par(cons_pattern)
cons_pattern ::=
core_pattern CONS pattern
tuple_pattern ::=
par(nsepseq(core_pattern,COMMA))
constr_pattern ::=
Constr tuple_pattern
| Constr

View File

@ -0,0 +1,387 @@
option(X) :=
(**)
| X
series(item,sep,term) ::=
item after_item(item,sep,term)
after_item(item,sep,term) ::=
sep item_or_closing(item,sep,term)
| term
item_or_closing(item,sep,term) ::=
term
| series(item,sep,term)
(* Compound constructs *)
par(X) ::= LPAR X RPAR
brackets(X) ::= LBRACKET X RBRACKET
(* Sequences *)
(* Possibly empty sequence of items *)
seq(X) ::=
(**)
| X seq(X)
(* Non-empty sequence of items *)
nseq(X) ::= X seq(X)
(* Non-empty separated sequence of items *)
nsepseq(X,Sep) ::=
X
| X Sep nsepseq(X,Sep)
(* Possibly empy separated sequence of items *)
sepseq(X,Sep) ::=
(**)
| nsepseq(X,Sep)
(* Main *)
contract ::=
nseq(declaration) EOF
declaration ::=
type_decl
| const_decl
| lambda_decl
(* Type declarations *)
type_decl ::=
Type Ident (* type_name *) Is type_expr option(SEMI)
type_expr ::=
cartesian
| sum_type
| record_type
cartesian ::=
nsepseq(function_type,TIMES)
function_type ::=
core_type
| core_type ARROW function_type
core_type ::=
Ident (* type_name *)
| Ident (* type_name *) type_tuple
| Map type_tuple
| Set par(type_expr)
| List par(type_expr)
| par(type_expr)
type_tuple ::=
par(nsepseq(type_expr,COMMA))
sum_type ::=
option(VBAR) nsepseq(variant,VBAR)
variant ::=
Constr Of cartesian
| Constr
record_type ::=
Record series(field_decl,SEMI,End)
| Record LBRACKET series(field_decl,SEMI,RBRACKET)
field_decl ::=
Ident (* field_name *) COLON type_expr
(* Function and procedure declarations *)
lambda_decl ::=
fun_decl
| proc_decl
| entry_decl
fun_decl ::=
Function Ident (* fun_name *) parameters COLON type_expr Is
seq(local_decl)
block
With expr option(SEMI)
entry_decl ::=
Entrypoint Ident (* fun_name *) entry_params COLON type_expr Is
seq(local_decl)
block
With expr option(SEMI)
entry_params ::=
par(nsepseq(entry_param_decl,SEMI))
proc_decl ::=
Procedure Ident (* fun_name *) parameters Is
seq(local_decl)
block option(SEMI)
parameters ::=
par(nsepseq(param_decl,SEMI))
param_decl ::=
Var Ident (* var *) COLON param_type
| Const Ident (* var *) COLON param_type
entry_param_decl ::=
param_decl
| Storage Ident (* var *) COLON param_type
param_type ::=
cartesian
block ::=
Begin series(statement,SEMI,End)
| Block LBRACE series(statement,SEMI,RBRACE)
statement ::=
instruction
| open_data_decl
open_data_decl ::=
open_const_decl
| open_var_decl
open_const_decl ::=
Const unqualified_decl(EQUAL)
open_var_decl ::=
Var unqualified_decl(ASS)
local_decl ::=
fun_decl
| proc_decl
| data_decl
data_decl ::=
const_decl
| var_decl
unqualified_decl(OP) ::=
Ident (* var *) COLON type_expr OP expr
const_decl ::=
open_const_decl option(SEMI)
var_decl ::=
open_var_decl option(SEMI)
instruction ::=
single_instr
| block
single_instr ::=
If expr Then if_clause option(SEMI) Else if_clause
| case(instruction)
| Ident (* proc_name *) arguments
| Ident option(brackets(expr)) ASS expr
| Ident DOT nsepseq(selection,DOT) option(brackets(expr)) ASS expr
| loop
| Fail expr
| Skip
| Patch path With record_expr
| Patch path With injection(Map,binding)
| Patch path With injection(Set,expr)
| Remove expr From Map path
| Remove expr From Set path
injection(Kind,element) ::=
Kind series(element,SEMI,End)
| Kind End
| Kind LBRACKET series(element,SEMI,RBRACKET)
| Kind LBRACKET RBRACKET
binding ::=
expr ARROW expr
if_clause ::=
instruction
| LBRACE series(statement,COMMA,RBRACE)
case(rhs) ::=
Case expr Of option(VBAR) cases(rhs) End
| Case expr Of LBRACKET option(VBAR) cases(rhs) RBRACKET
cases(rhs) ::=
nsepseq(case_clause(rhs),VBAR)
case_clause(rhs) ::=
pattern ARROW rhs
loop ::=
while_loop
| for_loop
while_loop ::=
While expr block
for_loop ::=
For Ident (* var *) ASS expr option(Down) To expr option(step_clause) block
| For Ident (* var *) option(arrow_clause) In expr block
step_clause ::=
Step expr
arrow_clause ::=
ARROW Ident (* var *)
(* Expressions *)
interactive_expr ::=
expr EOF
expr ::=
case(expr)
| annot_expr
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
| disj_expr
disj_expr ::=
disj_expr Or conj_expr
| conj_expr
conj_expr ::=
conj_expr And set_membership
| set_membership
set_membership ::=
core_expr Contains set_membership
| comp_expr
comp_expr ::=
comp_expr LT cat_expr
| comp_expr LEQ cat_expr
| comp_expr GT cat_expr
| comp_expr GEQ cat_expr
| comp_expr EQUAL cat_expr
| comp_expr NEQ cat_expr
| cat_expr
cat_expr ::=
cons_expr CAT cat_expr
| cons_expr
cons_expr ::=
add_expr CONS cons_expr
| add_expr
add_expr ::=
add_expr PLUS mult_expr
| add_expr MINUS mult_expr
| mult_expr
mult_expr ::=
mult_expr TIMES unary_expr
| mult_expr SLASH unary_expr
| mult_expr Mod unary_expr
| unary_expr
unary_expr ::=
MINUS core_expr
| Not core_expr
| core_expr
core_expr ::=
Int
| Nat
| Mtz
| Ident (* var *)
| String
| Bytes
| C_False
| C_True
| C_Unit
| tuple_expr
| list_expr
| C_None
| fun_call
| map_expr
| set_expr
| record_expr
| Ident (* struct_name *) DOT nsepseq(selection,DOT)
| Constr arguments
| Constr
| C_Some arguments
set_expr ::=
injection(Set,expr)
map_expr ::=
map_lookup
| injection(Map,binding)
map_lookup ::=
path brackets(expr)
path ::=
Ident (* var *)
| Ident (* struct_name *) DOT nsepseq(selection,DOT)
selection ::=
Ident (* field_name *)
| Int
record_expr ::=
Record series(field_assignment,SEMI,End)
| Record LBRACKET series(field_assignment,SEMI,RBRACKET)
field_assignment ::=
Ident (* field_name *) EQUAL expr
fun_call ::=
Ident (* fun_name *) arguments
tuple_expr ::=
tuple_inj
tuple_inj ::=
par(nsepseq(expr,COMMA))
arguments ::=
tuple_inj
list_expr ::=
injection(List,expr)
| Nil
(* Patterns *)
pattern ::=
nsepseq(core_pattern,CONS)
core_pattern ::=
Ident (* var *)
| WILD
| Int
| String
| C_Unit
| C_False
| C_True
| C_None
| list_pattern
| tuple_pattern
| constr_pattern
| C_Some par(core_pattern)
list_pattern ::=
injection(List,core_pattern)
| Nil
| par(cons_pattern)
cons_pattern ::=
core_pattern CONS pattern
tuple_pattern ::=
par(nsepseq(core_pattern,COMMA))
constr_pattern ::=
Constr tuple_pattern
| Constr

View File

@ -0,0 +1,390 @@
option(X) :=
(**)
| X
series(item,sep,term) ::=
item after_item(item,sep,term)
after_item(item,sep,term) ::=
sep item_or_closing(item,sep,term)
| term
item_or_closing(item,sep,term) ::=
term
| series(item,sep,term)
(* Compound constructs *)
par(X) ::= LPAR X RPAR
brackets(X) ::= LBRACKET X RBRACKET
(* Sequences *)
(* Possibly empty sequence of items *)
seq(X) ::=
(**)
| X seq(X)
(* Non-empty sequence of items *)
nseq(X) ::= X seq(X)
(* Non-empty separated sequence of items *)
nsepseq(X,Sep) ::=
X
| X Sep nsepseq(X,Sep)
(* Possibly empy separated sequence of items *)
sepseq(X,Sep) ::=
(**)
| nsepseq(X,Sep)
(* Main *)
contract ::=
nseq(declaration) EOF
declaration ::=
type_decl
| const_decl
| lambda_decl
(* Type declarations *)
type_decl ::=
Type Ident (* type_name *) Is type_expr option(SEMI)
type_expr ::=
cartesian
| sum_type
| record_type
cartesian ::=
nsepseq(function_type,TIMES)
function_type ::=
core_type
| core_type ARROW function_type
core_type ::=
Ident (* type_name *)
| Ident (* type_name *) type_tuple
| Map type_tuple
| Set par(type_expr)
| List par(type_expr)
| par(type_expr)
type_tuple ::=
par(nsepseq(type_expr,COMMA))
sum_type ::=
option(VBAR) nsepseq(variant,VBAR)
variant ::=
Constr Of cartesian
| Constr
record_type ::=
Record series(field_decl,SEMI,End)
| Record LBRACKET series(field_decl,SEMI,RBRACKET)
field_decl ::=
Ident (* field_name *) COLON type_expr
(* Function and procedure declarations *)
lambda_decl ::=
fun_decl
| proc_decl
| entry_decl
fun_decl ::=
Function Ident (* fun_name *) parameters COLON type_expr Is
seq(local_decl)
block
With expr option(SEMI)
entry_decl ::=
Entrypoint Ident (* fun_name *) entry_params COLON type_expr Is
seq(local_decl)
block
With expr option(SEMI)
entry_params ::=
par(nsepseq(entry_param_decl,SEMI))
proc_decl ::=
Procedure Ident (* fun_name *) parameters Is
seq(local_decl)
block option(SEMI)
parameters ::=
par(nsepseq(param_decl,SEMI))
param_decl ::=
Var Ident (* var *) COLON param_type
| Const Ident (* var *) COLON param_type
entry_param_decl ::=
param_decl
| Storage Ident (* var *) COLON param_type
param_type ::=
cartesian
block ::=
Begin series(statement,SEMI,End)
| Block LBRACE series(statement,SEMI,RBRACE)
statement ::=
instruction
| open_data_decl
open_data_decl ::=
open_const_decl
| open_var_decl
open_const_decl ::=
Const unqualified_decl(EQUAL)
open_var_decl ::=
Var unqualified_decl(ASS)
local_decl ::=
fun_decl
| proc_decl
| data_decl
data_decl ::=
const_decl
| var_decl
unqualified_decl(op) ::=
Ident (* var *) COLON type_expr op expr
const_decl ::=
open_const_decl option(SEMI)
var_decl ::=
open_var_decl option(SEMI)
instruction ::=
single_instr
| block
single_instr ::=
If expr Then if_clause option(SEMI) Else if_clause
| case(instruction)
| Ident (* proc_name *) arguments
| Ident option(brackets(expr)) ASS expr
| Ident DOT nsepseq(selection,DOT) option(brackets(expr)) ASS expr
| loop
| Fail expr
| Skip
| Patch path With record_expr
| Patch path With injection(Map,binding)
| Patch path With injection(Set,expr)
| Remove expr From Map path
| Remove expr From Set path
injection(Kind,element) ::=
Kind series(element,SEMI,End)
| Kind End
| Kind LBRACKET bracketed
bracketed ::=
series(element,SEMI,RBRACKET)
| RBRACKET
binding ::=
expr ARROW expr
if_clause ::=
instruction
| LBRACE series(statement,COMMA,RBRACE)
case(rhs) ::=
Case expr Of cases(rhs) End
| Case expr Of LBRACKET cases(rhs) RBRACKET
cases(rhs) ::=
option(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 option(arrow_clause) In expr block
step_clause ::=
Step expr
arrow_clause ::=
ARROW Ident (* var *)
(* Expressions *)
interactive_expr ::=
expr EOF
expr ::=
case(expr)
| annot_expr
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
| disj_expr
disj_expr ::=
disj_expr Or conj_expr
| conj_expr
conj_expr ::=
conj_expr And set_membership
| set_membership
set_membership ::=
core_expr Contains set_membership
| comp_expr
comp_expr ::=
comp_expr LT cat_expr
| comp_expr LEQ cat_expr
| comp_expr GT cat_expr
| comp_expr GEQ cat_expr
| comp_expr EQUAL cat_expr
| comp_expr NEQ cat_expr
| cat_expr
cat_expr ::=
cons_expr CAT cat_expr
| cons_expr
cons_expr ::=
add_expr CONS cons_expr
| add_expr
add_expr ::=
add_expr PLUS mult_expr
| add_expr MINUS mult_expr
| mult_expr
mult_expr ::=
mult_expr TIMES unary_expr
| mult_expr SLASH unary_expr
| mult_expr Mod unary_expr
| unary_expr
unary_expr ::=
MINUS core_expr
| Not core_expr
| core_expr
core_expr ::=
Int
| Nat
| Mtz
| Ident (* var *)
| String
| Bytes
| C_False
| C_True
| C_Unit
| tuple_expr
| list_expr
| C_None
| fun_call
| map_expr
| set_expr
| record_expr
| Ident (* struct_name *) DOT nsepseq(selection,DOT)
| Constr arguments
| Constr
| C_Some arguments
set_expr ::=
injection(Set,expr)
map_expr ::=
map_lookup
| injection(Map,binding)
map_lookup ::=
path brackets(expr)
path ::=
Ident (* var *)
| Ident (* struct_name *) DOT nsepseq(selection,DOT)
selection ::=
Ident (* field_name *)
| Int
record_expr ::=
Record series(field_assignment,SEMI,End)
| Record LBRACKET series(field_assignment,SEMI,RBRACKET)
field_assignment ::=
Ident (* field_name *) EQUAL expr
fun_call ::=
Ident (* fun_name *) arguments
tuple_expr ::=
tuple_inj
tuple_inj ::=
par(nsepseq(expr,COMMA))
arguments ::=
tuple_inj
list_expr ::=
injection(List,expr)
| Nil
(* Patterns *)
pattern ::=
nsepseq(core_pattern,CONS)
core_pattern ::=
Ident (* var *)
| WILD
| Int
| String
| C_Unit
| C_False
| C_True
| C_None
| list_pattern
| tuple_pattern
| constr_pattern
| C_Some par(core_pattern)
list_pattern ::=
injection(List,core_pattern)
| Nil
| par(cons_pattern)
cons_pattern ::=
core_pattern CONS pattern
tuple_pattern ::=
par(nsepseq(core_pattern,COMMA))
constr_pattern ::=
Constr tuple_pattern
| Constr

View File

@ -0,0 +1,380 @@
option(X) :=
(**)
| X
series(item,sep,term) ::=
item after_item(item,sep,term)
after_item(item,sep,term) ::=
sep item_or_closing(item,sep,term)
| term
item_or_closing(item,sep,term) ::=
term
| series(item,sep,term)
(* Compound constructs *)
par(X) ::= LPAR X RPAR
brackets(X) ::= LBRACKET X RBRACKET
(* Sequences *)
(* Possibly empty sequence of items *)
seq(X) ::=
(**)
| X seq(X)
(* Non-empty sequence of items *)
nseq(X) ::= X seq(X)
(* Non-empty separated sequence of items *)
nsepseq(X,Sep) ::=
X
| X Sep nsepseq(X,Sep)
(* Possibly empy separated sequence of items *)
sepseq(X,Sep) ::=
(**)
| nsepseq(X,Sep)
(* Main *)
contract ::=
nseq(declaration) EOF
declaration ::=
type_decl option(SEMI)
| const_decl option(SEMI)
| lambda_decl option(SEMI)
(* Type declarations *)
type_decl ::=
Type Ident (* type_name *) Is type_expr
type_expr ::=
cartesian
| sum_type
| record_type
cartesian ::=
nsepseq(function_type,TIMES)
function_type ::=
core_type
| core_type ARROW function_type
core_type ::=
Ident (* type_name *)
| Ident (* type_name *) type_tuple
| Map type_tuple
| Set par(type_expr)
| List par(type_expr)
| par(type_expr)
type_tuple ::=
par(nsepseq(type_expr,COMMA))
sum_type ::=
option(VBAR) nsepseq(variant,VBAR)
variant ::=
Constr Of cartesian
| Constr
record_type ::=
Record series(field_decl,SEMI,End)
| Record LBRACKET series(field_decl,SEMI,RBRACKET)
field_decl ::=
Ident (* field_name *) COLON type_expr
(* Function and procedure declarations *)
lambda_decl ::=
fun_decl
| proc_decl
| entry_decl
fun_decl ::=
Function Ident (* fun_name *) parameters COLON type_expr Is
seq(local_decl)
block
With expr
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 option(brackets(expr)) ASS expr
| Ident DOT nsepseq(selection,DOT) option(brackets(expr)) ASS expr
| loop
| Fail expr
| Skip
| Patch path With record_expr
| Patch path With injection(Map,binding)
| Patch path With injection(Set,expr)
| Remove expr From Map path
| Remove expr From Set path
injection(Kind,element) ::=
Kind series(element,SEMI,End)
| Kind End
| Kind LBRACKET bracketed
bracketed ::=
series(element,SEMI,RBRACKET)
| RBRACKET
binding ::=
expr ARROW expr
if_clause ::=
instruction
| LBRACE series(statement,COMMA,RBRACE)
case(rhs) ::=
Case expr Of cases(rhs) End
| Case expr Of LBRACKET cases(rhs) RBRACKET
cases(rhs) ::=
option(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 option(arrow_clause) In expr block
step_clause ::=
Step expr
arrow_clause ::=
ARROW Ident (* var *)
(* Expressions *)
interactive_expr ::=
expr EOF
expr ::=
case(expr)
| annot_expr
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
| disj_expr
disj_expr ::=
disj_expr Or conj_expr
| conj_expr
conj_expr ::=
conj_expr And set_membership
| set_membership
set_membership ::=
core_expr Contains set_membership
| comp_expr
comp_expr ::=
comp_expr LT cat_expr
| comp_expr LEQ cat_expr
| comp_expr GT cat_expr
| comp_expr GEQ cat_expr
| comp_expr EQUAL cat_expr
| comp_expr NEQ cat_expr
| cat_expr
cat_expr ::=
cons_expr CAT cat_expr
| cons_expr
cons_expr ::=
add_expr CONS cons_expr
| add_expr
add_expr ::=
add_expr PLUS mult_expr
| add_expr MINUS mult_expr
| mult_expr
mult_expr ::=
mult_expr TIMES unary_expr
| mult_expr SLASH unary_expr
| mult_expr Mod unary_expr
| unary_expr
unary_expr ::=
MINUS core_expr
| Not core_expr
| core_expr
core_expr ::=
Int
| Nat
| Mtz
| Ident (* var *)
| String
| Bytes
| C_False
| C_True
| C_Unit
| tuple_expr
| list_expr
| C_None
| fun_call
| map_expr
| set_expr
| record_expr
| Ident (* struct_name *) DOT nsepseq(selection,DOT)
| Constr arguments
| Constr
| C_Some arguments
set_expr ::=
injection(Set,expr)
map_expr ::=
map_lookup
| injection(Map,binding)
map_lookup ::=
path brackets(expr)
path ::=
Ident (* var *)
| Ident (* struct_name *) DOT nsepseq(selection,DOT)
selection ::=
Ident (* field_name *)
| Int
record_expr ::=
Record series(field_assignment,SEMI,End)
| Record LBRACKET series(field_assignment,SEMI,RBRACKET)
field_assignment ::=
Ident (* field_name *) EQUAL expr
fun_call ::=
Ident (* fun_name *) arguments
tuple_expr ::=
tuple_inj
tuple_inj ::=
par(nsepseq(expr,COMMA))
arguments ::=
tuple_inj
list_expr ::=
injection(List,expr)
| Nil
(* Patterns *)
pattern ::=
nsepseq(core_pattern,CONS)
core_pattern ::=
Ident (* var *)
| WILD
| Int
| String
| C_Unit
| C_False
| C_True
| C_None
| list_pattern
| tuple_pattern
| constr_pattern
| C_Some par(core_pattern)
list_pattern ::=
injection(List,core_pattern)
| Nil
| par(cons_pattern)
cons_pattern ::=
core_pattern CONS pattern
tuple_pattern ::=
par(nsepseq(core_pattern,COMMA))
constr_pattern ::=
Constr tuple_pattern
| Constr

View File

@ -0,0 +1,382 @@
option(X) :=
(**)
| X
series(item,sep,term) ::=
item after_item(item,sep,term)
after_item(item,sep,term) ::=
sep item_or_closing(item,sep,term)
| term
item_or_closing(item,sep,term) ::=
term
| series(item,sep,term)
(* Compound constructs *)
par(X) ::= LPAR X RPAR
brackets(X) ::= LBRACKET X RBRACKET
(* Sequences *)
(* Possibly empty sequence of items *)
seq(X) ::=
(**)
| X seq(X)
(* Non-empty sequence of items *)
nseq(X) ::= X seq(X)
(* Non-empty separated sequence of items *)
nsepseq(X,Sep) ::=
X
| X Sep nsepseq(X,Sep)
(* Possibly empy separated sequence of items *)
sepseq(X,Sep) ::=
(**)
| nsepseq(X,Sep)
(* Main *)
contract ::=
nseq(declaration) EOF
declaration ::=
type_decl option(SEMI)
| const_decl option(SEMI)
| lambda_decl option(SEMI)
(* Type declarations *)
type_decl ::=
Type Ident (* type_name *) Is type_expr
type_expr ::=
cartesian
| sum_type
| record_type
cartesian ::=
nsepseq(function_type,TIMES)
function_type ::=
core_type
| core_type ARROW function_type
core_type ::=
Ident (* type_name *)
| Ident (* type_name *) type_tuple
| Map type_tuple
| Set par(type_expr)
| List par(type_expr)
| par(type_expr)
type_tuple ::=
par(nsepseq(type_expr,COMMA))
sum_type ::=
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 record_expr
| Patch path With injection(Map,binding)
| Patch path With injection(Set,expr)
| Remove expr From Map path
| Remove expr From Set path
injection(Kind,element) ::=
Kind series(element,SEMI,End)
| Kind End
| Kind LBRACKET bracketed
bracketed ::=
series(element,SEMI,RBRACKET)
| RBRACKET
binding ::=
expr ARROW expr
if_clause ::=
instruction
| LBRACE series(statement,COMMA,RBRACE)
case(rhs) ::=
Case expr Of cases(rhs) End
| Case expr Of LBRACKET cases(rhs) RBRACKET
cases(rhs) ::=
option(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 option(arrow_clause) In expr block
step_clause ::=
Step expr
arrow_clause ::=
ARROW Ident (* var *)
(* Expressions *)
interactive_expr ::=
expr EOF
expr ::=
case(expr)
| annot_expr
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
| disj_expr
disj_expr ::=
disj_expr Or conj_expr
| conj_expr
conj_expr ::=
conj_expr And set_membership
| set_membership
set_membership ::=
core_expr Contains set_membership
| comp_expr
comp_expr ::=
comp_expr LT cat_expr
| comp_expr LEQ cat_expr
| comp_expr GT cat_expr
| comp_expr GEQ cat_expr
| comp_expr EQUAL cat_expr
| comp_expr NEQ cat_expr
| cat_expr
cat_expr ::=
cons_expr CAT cat_expr
| cons_expr
cons_expr ::=
add_expr CONS cons_expr
| add_expr
add_expr ::=
add_expr PLUS mult_expr
| add_expr MINUS mult_expr
| mult_expr
mult_expr ::=
mult_expr TIMES unary_expr
| mult_expr SLASH unary_expr
| mult_expr Mod unary_expr
| unary_expr
unary_expr ::=
MINUS core_expr
| Not core_expr
| core_expr
core_expr ::=
Int
| Nat
| Mtz
| Ident (* var *)
| String
| Bytes
| C_False
| C_True
| C_Unit
| tuple_expr
| list_expr
| C_None
| fun_call
| map_expr
| set_expr
| record_expr
| Ident (* struct_name *) DOT nsepseq(selection,DOT)
| Constr arguments
| Constr
| C_Some arguments
set_expr ::=
injection(Set,expr)
map_expr ::=
map_lookup
| injection(Map,binding)
map_lookup ::=
path brackets(expr)
path ::=
Ident (* var *)
| Ident (* struct_name *) DOT nsepseq(selection,DOT)
selection ::=
Ident (* field_name *)
| Int
record_expr ::=
Record series(field_assignment,SEMI,End)
| Record LBRACKET series(field_assignment,SEMI,RBRACKET)
field_assignment ::=
Ident (* field_name *) EQUAL expr
fun_call ::=
Ident (* fun_name *) arguments
tuple_expr ::=
tuple_inj
tuple_inj ::=
par(nsepseq(expr,COMMA))
arguments ::=
tuple_inj
list_expr ::=
injection(List,expr)
| Nil
(* Patterns *)
pattern ::=
nsepseq(core_pattern,CONS)
core_pattern ::=
Ident (* var *)
| WILD
| Int
| String
| C_Unit
| C_False
| C_True
| C_None
| list_pattern
| tuple_pattern
| constr_pattern
| C_Some par(core_pattern)
list_pattern ::=
injection(List,core_pattern)
| Nil
| par(cons_pattern)
cons_pattern ::=
core_pattern CONS pattern
tuple_pattern ::=
par(nsepseq(core_pattern,COMMA))
constr_pattern ::=
Constr tuple_pattern
| Constr

View File

@ -0,0 +1,385 @@
left_assoc(item,op)
right_assoc(item,op) ::=
item
| item op right_assoc(item,op)
option(X) :=
(**)
| X
series(item,sep,term) ::=
item after_item(item,sep,term)
after_item(item,sep,term) ::=
sep item_or_closing(item,sep,term)
| term
item_or_closing(item,sep,term) ::=
term
| series(item,sep,term)
(* Compound constructs *)
par(X) ::= LPAR X RPAR
brackets(X) ::= LBRACKET X RBRACKET
(* Sequences *)
(* Possibly empty sequence of items *)
seq(X) ::=
(**)
| X seq(X)
(* Non-empty sequence of items *)
nseq(X) ::= X seq(X)
(* Non-empty separated sequence of items *)
nsepseq(X,Sep) ::=
X
| X Sep nsepseq(X,Sep)
(* Possibly empy separated sequence of items *)
sepseq(X,Sep) ::=
(**)
| nsepseq(X,Sep)
(* Main *)
contract ::=
nseq(declaration) EOF
declaration ::=
type_decl option(SEMI)
| const_decl option(SEMI)
| lambda_decl option(SEMI)
(* Type declarations *)
type_decl ::=
Type Ident (* type_name *) Is type_expr
type_expr ::=
cartesian
| sum_type
| record_type
cartesian ::=
nsepseq(function_type,TIMES)
function_type ::=
right_assoc(core_type,ARROW)
core_type ::=
Ident (* type_name *)
| Ident (* type_name *) type_tuple
| Map type_tuple
| Set par(type_expr)
| List par(type_expr)
| par(type_expr)
type_tuple ::=
par(nsepseq(type_expr,COMMA))
sum_type ::=
nsepseq(variant,VBAR)
| VBAR nsepseq(variant,VBAR)
variant ::=
Constr Of cartesian
| Constr
record_type ::=
Record series(field_decl,SEMI,End)
| Record LBRACKET series(field_decl,SEMI,RBRACKET)
field_decl ::=
Ident (* field_name *) COLON type_expr
(* Function and procedure declarations *)
lambda_decl ::=
fun_decl
| proc_decl
| entry_decl
fun_decl ::=
Function Ident (* fun_name *) parameters COLON type_expr Is
seq(local_decl)
block
With expr
entry_decl ::=
Entrypoint Ident (* fun_name *) entry_params COLON type_expr Is
seq(local_decl)
block
With expr
entry_params ::=
par(nsepseq(entry_param_decl,SEMI))
proc_decl ::=
Procedure Ident (* fun_name *) parameters Is
seq(local_decl)
block
parameters ::=
par(nsepseq(param_decl,SEMI))
param_decl ::=
Var Ident (* var *) COLON param_type
| Const Ident (* var *) COLON param_type
entry_param_decl ::=
param_decl
| Storage Ident (* var *) COLON param_type
param_type ::=
cartesian
block ::=
Begin series(statement,SEMI,End)
| Block LBRACE series(statement,SEMI,RBRACE)
statement ::=
instruction
| data_decl
data_decl ::=
const_decl
| var_decl
const_decl ::=
Const unqualified_decl(EQUAL)
var_decl ::=
Var unqualified_decl(ASS)
local_decl ::=
fun_decl option(SEMI)
| proc_decl option(SEMI)
| data_decl option(SEMI)
unqualified_decl(op) ::=
Ident (* var *) COLON type_expr op expr
instruction ::=
single_instr
| block
single_instr ::=
If expr Then if_clause option(SEMI) Else if_clause
| case(instruction)
| Ident (* proc_name *) arguments
| Ident ASS expr
| Ident brackets(expr) ASS expr
| Ident DOT nsepseq(selection,DOT) option(brackets(expr)) ASS expr
| loop
| Fail expr
| Skip
| Patch path With record_expr
| Patch path With injection(Map,binding)
| Patch path With injection(Set,expr)
| Remove expr From Map path
| Remove expr From Set path
injection(Kind,element) ::=
Kind series(element,SEMI,End)
| Kind End
| Kind LBRACKET bracketed
bracketed ::=
series(element,SEMI,RBRACKET)
| RBRACKET
binding ::=
expr ARROW expr
if_clause ::=
instruction
| LBRACE series(statement,COMMA,RBRACE)
case(rhs) ::=
Case expr Of cases(rhs) End
| Case expr Of LBRACKET cases(rhs) RBRACKET
cases(rhs) ::=
option(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)
| annot_expr
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
| disj_expr
disj_expr ::=
disj_expr Or conj_expr
| conj_expr
conj_expr ::=
conj_expr And set_membership
| set_membership
set_membership ::=
core_expr Contains set_membership
| comp_expr
comp_expr ::=
comp_expr LT cat_expr
| comp_expr LEQ cat_expr
| comp_expr GT cat_expr
| comp_expr GEQ cat_expr
| comp_expr EQUAL cat_expr
| comp_expr NEQ cat_expr
| cat_expr
cat_expr ::=
cons_expr CAT cat_expr
| cons_expr
cons_expr ::=
add_expr CONS cons_expr
| add_expr
add_expr ::=
add_expr PLUS mult_expr
| add_expr MINUS mult_expr
| mult_expr
mult_expr ::=
mult_expr TIMES unary_expr
| mult_expr SLASH unary_expr
| mult_expr Mod unary_expr
| unary_expr
unary_expr ::=
MINUS core_expr
| Not core_expr
| core_expr
core_expr ::=
Int
| Nat
| Mtz
| Ident (* var *)
| String
| Bytes
| C_False
| C_True
| C_Unit
| tuple_expr
| list_expr
| C_None
| fun_call
| map_expr
| set_expr
| record_expr
| Ident (* struct_name *) DOT nsepseq(selection,DOT)
| Constr arguments
| Constr
| C_Some arguments
set_expr ::=
injection(Set,expr)
map_expr ::=
map_lookup
| injection(Map,binding)
map_lookup ::=
path brackets(expr)
path ::=
Ident (* var *)
| Ident (* struct_name *) DOT nsepseq(selection,DOT)
selection ::=
Ident (* field_name *)
| Int
record_expr ::=
Record series(field_assignment,SEMI,End)
| Record LBRACKET series(field_assignment,SEMI,RBRACKET)
field_assignment ::=
Ident (* field_name *) EQUAL expr
fun_call ::=
Ident (* fun_name *) arguments
tuple_expr ::=
tuple_inj
tuple_inj ::=
par(nsepseq(expr,COMMA))
arguments ::=
tuple_inj
list_expr ::=
injection(List,expr)
| Nil
(* Patterns *)
pattern ::=
nsepseq(core_pattern,CONS)
core_pattern ::=
Ident (* var *)
| WILD
| Int
| String
| C_Unit
| C_False
| C_True
| C_None
| list_pattern
| tuple_pattern
| constr_pattern
| C_Some par(core_pattern)
list_pattern ::=
injection(List,core_pattern)
| Nil
| par(cons_pattern)
cons_pattern ::=
core_pattern CONS pattern
tuple_pattern ::=
par(nsepseq(core_pattern,COMMA))
constr_pattern ::=
Constr tuple_pattern
| Constr

View File

@ -0,0 +1,377 @@
left_assoc(item,op)
right_assoc(item,op) ::=
item
| item op right_assoc(item,op)
option(X) :=
(**)
| X
series(item,sep,term) ::=
item after_item(item,sep,term)
after_item(item,sep,term) ::=
sep item_or_closing(item,sep,term)
| term
item_or_closing(item,sep,term) ::=
term
| series(item,sep,term)
(* Compound constructs *)
par(X) ::= LPAR X RPAR
brackets(X) ::= LBRACKET X RBRACKET
(* Sequences *)
(* Possibly empty sequence of items *)
seq(X) ::=
(**)
| X seq(X)
(* Non-empty sequence of items *)
nseq(X) ::= X seq(X)
(* Non-empty separated sequence of items *)
nsepseq(X,Sep) ::=
X
| X Sep nsepseq(X,Sep)
(* Possibly empy separated sequence of items *)
sepseq(X,Sep) ::=
(**)
| nsepseq(X,Sep)
(* Main *)
contract ::=
nseq(declaration) EOF
declaration ::=
type_decl option(SEMI)
| const_decl option(SEMI)
| lambda_decl option(SEMI)
(* Type declarations *)
type_decl ::=
Type Ident (* type_name *) Is type_expr
type_expr ::=
cartesian
| sum_type
| record_type
cartesian ::=
nsepseq(function_type,TIMES)
function_type ::=
right_assoc(core_type,ARROW)
core_type ::=
Ident (* type_name *)
| Ident (* type_name *) type_tuple
| Map type_tuple
| Set par(type_expr)
| List par(type_expr)
| par(type_expr)
type_tuple ::=
par(nsepseq(type_expr,COMMA))
sum_type ::=
nsepseq(variant,VBAR)
| VBAR nsepseq(variant,VBAR)
variant ::=
Constr Of cartesian
| Constr
record_type ::=
Record series(field_decl,SEMI,End)
| Record LBRACKET series(field_decl,SEMI,RBRACKET)
field_decl ::=
Ident (* field_name *) COLON type_expr
(* Function and procedure declarations *)
lambda_decl ::=
fun_decl
| proc_decl
| entry_decl
fun_decl ::=
Function Ident (* fun_name *) parameters COLON type_expr Is
seq(local_decl)
block
With expr
entry_decl ::=
Entrypoint Ident (* fun_name *) entry_params COLON type_expr Is
seq(local_decl)
block
With expr
entry_params ::=
par(nsepseq(entry_param_decl,SEMI))
proc_decl ::=
Procedure Ident (* fun_name *) parameters Is
seq(local_decl)
block
parameters ::=
par(nsepseq(param_decl,SEMI))
param_decl ::=
Var Ident (* var *) COLON param_type
| Const Ident (* var *) COLON param_type
entry_param_decl ::=
param_decl
| Storage Ident (* var *) COLON param_type
param_type ::=
cartesian
block ::=
Begin series(statement,SEMI,End)
| Block LBRACE series(statement,SEMI,RBRACE)
statement ::=
instruction
| data_decl
data_decl ::=
const_decl
| var_decl
const_decl ::=
Const unqualified_decl(EQUAL)
var_decl ::=
Var unqualified_decl(ASS)
local_decl ::=
fun_decl option(SEMI)
| proc_decl option(SEMI)
| data_decl option(SEMI)
unqualified_decl(op) ::=
Ident (* var *) COLON type_expr op expr
instruction ::=
single_instr
| block
single_instr ::=
If expr Then if_clause option(SEMI) Else if_clause
| case(instruction)
| Ident (* proc_name *) arguments
| Ident ASS expr
| Ident brackets(expr) ASS expr
| Ident DOT nsepseq(selection,DOT) option(brackets(expr)) ASS expr
| loop
| Fail expr
| Skip
| Patch path With record_expr
| Patch path With injection(Map,binding)
| Patch path With injection(Set,expr)
| Remove expr From Map path
| Remove expr From Set path
injection(Kind,element) ::=
Kind series(element,SEMI,End)
| Kind End
| Kind LBRACKET bracketed
bracketed ::=
series(element,SEMI,RBRACKET)
| RBRACKET
binding ::=
expr ARROW expr
if_clause ::=
instruction
| LBRACE series(statement,COMMA,RBRACE)
case(rhs) ::=
Case expr Of cases(rhs) End
| Case expr Of LBRACKET cases(rhs) RBRACKET
cases(rhs) ::=
nsepseq(case_clause(rhs),VBAR)
| VBAR nsepseq(case_clause(rhs),VBAR)
case_clause(rhs) ::=
pattern ARROW rhs
loop ::=
while_loop
| for_loop
while_loop ::=
While expr block
for_loop ::=
For Ident ASS expr option(Down) To expr option(step_clause) block
| For Ident In expr block
| For Ident ARROW Ident In expr block
step_clause ::=
Step expr
(* Expressions *)
interactive_expr ::=
expr EOF
expr ::=
case(expr)
| annot_expr
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
| 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 *)
| String
| Bytes
| C_False
| C_True
| C_Unit
| tuple_expr
| list_expr
| C_None
| fun_call
| map_expr
| set_expr
| record_expr
| Ident (* struct_name *) DOT nsepseq(selection,DOT)
| Constr arguments
| Constr
| C_Some arguments
set_expr ::=
injection(Set,expr)
map_expr ::=
path brackets(expr) (* lookup *)
| injection(Map,binding)
path ::=
Ident (* var *)
| Ident (* struct_name *) DOT nsepseq(selection,DOT)
selection ::=
Ident (* field_name *)
| Int
record_expr ::=
Record series(field_assignment,SEMI,End)
| Record LBRACKET series(field_assignment,SEMI,RBRACKET)
field_assignment ::=
Ident (* field_name *) EQUAL expr
fun_call ::=
Ident (* fun_name *) arguments
tuple_expr ::=
tuple_inj
tuple_inj ::=
par(nsepseq(expr,COMMA))
arguments ::=
tuple_inj
list_expr ::=
injection(List,expr)
| Nil
(* Patterns *)
pattern ::=
nsepseq(core_pattern,CONS)
core_pattern ::=
Ident (* var *)
| WILD
| Int
| String
| C_Unit
| C_False
| C_True
| C_None
| list_pattern
| tuple_pattern
| constr_pattern
| C_Some par(core_pattern)
list_pattern ::=
injection(List,core_pattern)
| Nil
| par(cons_pattern)
cons_pattern ::=
core_pattern CONS pattern
tuple_pattern ::=
par(nsepseq(core_pattern,COMMA))
constr_pattern ::=
Constr tuple_pattern
| Constr

View File

@ -0,0 +1,373 @@
left_assoc(item,op)
right_assoc(item,op) ::=
item
| item op right_assoc(item,op)
option(X) :=
(**)
| X
series(item,sep,term) ::=
item after_item(item,sep,term)
after_item(item,sep,term) ::=
sep item_or_closing(item,sep,term)
| term
item_or_closing(item,sep,term) ::=
term
| series(item,sep,term)
(* Compound constructs *)
par(X) ::= LPAR X RPAR
brackets(X) ::= LBRACKET X RBRACKET
(* Sequences *)
(* Possibly empty sequence of items *)
seq(X) ::=
(**)
| X seq(X)
(* Non-empty sequence of items *)
nseq(X) ::= X seq(X)
(* Non-empty separated sequence of items *)
nsepseq(X,Sep) ::=
X
| X Sep nsepseq(X,Sep)
(* Possibly empy separated sequence of items *)
sepseq(X,Sep) ::=
(**)
| nsepseq(X,Sep)
(* Main *)
contract ::=
nseq(declaration) EOF
declaration ::=
type_decl option(SEMI)
| const_decl option(SEMI)
| lambda_decl option(SEMI)
(* Type declarations *)
type_decl ::=
Type Ident (* type_name *) Is type_expr
type_expr ::=
cartesian
| sum_type
| record_type
cartesian ::=
nsepseq(function_type,TIMES)
function_type ::=
right_assoc(core_type,ARROW)
core_type ::=
Ident (* type_name *)
| Ident (* type_name *) type_tuple
| Map type_tuple
| Set par(type_expr)
| List par(type_expr)
| par(type_expr)
type_tuple ::=
par(nsepseq(type_expr,COMMA))
sum_type ::=
nsepseq(variant,VBAR)
| VBAR nsepseq(variant,VBAR)
variant ::=
Constr Of cartesian
| Constr
record_type ::=
Record series(field_decl,SEMI,End)
| Record LBRACKET series(field_decl,SEMI,RBRACKET)
field_decl ::=
Ident (* field_name *) COLON type_expr
(* Function and procedure declarations *)
lambda_decl ::=
fun_decl
| proc_decl
| entry_decl
fun_decl ::=
Function Ident (* fun_name *) parameters COLON type_expr Is
seq(local_decl)
block
With expr
entry_decl ::=
Entrypoint Ident (* fun_name *) entry_params COLON type_expr Is
seq(local_decl)
block
With expr
entry_params ::=
par(nsepseq(entry_param_decl,SEMI))
proc_decl ::=
Procedure Ident (* fun_name *) parameters Is
seq(local_decl)
block
parameters ::=
par(nsepseq(param_decl,SEMI))
param_decl ::=
Var Ident (* var *) COLON param_type
| Const Ident (* var *) COLON param_type
entry_param_decl ::=
param_decl
| Storage Ident (* var *) COLON param_type
param_type ::=
cartesian
block ::=
Begin series(statement,SEMI,End)
| Block LBRACE series(statement,SEMI,RBRACE)
statement ::=
instruction
| data_decl
data_decl ::=
const_decl
| var_decl
const_decl ::=
Const unqualified_decl(EQUAL)
var_decl ::=
Var unqualified_decl(ASS)
local_decl ::=
fun_decl option(SEMI)
| proc_decl option(SEMI)
| data_decl option(SEMI)
unqualified_decl(op) ::=
Ident (* var *) COLON type_expr op expr
instruction ::=
single_instr
| block
single_instr ::=
If expr Then if_clause option(SEMI) Else if_clause
| case(instruction)
| Ident (* proc_name *) arguments
| Ident ASS expr
| Ident brackets(expr) ASS expr
| Ident DOT nsepseq(selection,DOT) option(brackets(expr)) ASS expr
| loop
| Fail expr
| Skip
| Patch path With structure
| Remove expr From Map path
| Remove expr From Set path
injection(Kind,element) ::=
Kind series(element,SEMI,End)
| Kind End
| Kind LBRACKET bracketed
bracketed ::=
series(element,SEMI,RBRACKET)
| RBRACKET
binding ::=
expr ARROW expr
if_clause ::=
instruction
| LBRACE series(statement,COMMA,RBRACE)
case(rhs) ::=
Case expr Of cases(rhs) End
| Case expr Of LBRACKET cases(rhs) RBRACKET
cases(rhs) ::=
nsepseq(case_clause(rhs),VBAR)
| VBAR nsepseq(case_clause(rhs),VBAR)
case_clause(rhs) ::=
pattern ARROW rhs
loop ::=
while_loop
| for_loop
while_loop ::=
While expr block
for_loop ::=
For Ident ASS expr option(Down) To expr option(step_clause) block
| For Ident In expr block
| For Ident ARROW Ident In expr block
step_clause ::=
Step expr
(* Expressions *)
interactive_expr ::=
expr EOF
expr ::=
case(expr)
| annot_expr
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
| 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) brackets(expr) (* lookup *)
| Ident (* struct_name *) DOT nsepseq(selection,DOT)
| String
| Bytes
| C_False
| C_True
| C_Unit
| tuple_expr
| list_expr
| C_None
| fun_call
| structure
| Constr arguments
| Constr
| C_Some arguments
structure ::=
injection(Map,binding)
| injection(Set,expr)
| record_expr
path ::=
Ident (* var *)
| Ident (* struct_name *) DOT nsepseq(selection,DOT)
selection ::=
Ident (* field_name *)
| Int
record_expr ::=
Record series(field_assignment,SEMI,End)
| Record LBRACKET series(field_assignment,SEMI,RBRACKET)
field_assignment ::=
Ident (* field_name *) EQUAL expr
fun_call ::=
Ident (* fun_name *) arguments
tuple_expr ::=
tuple_inj
tuple_inj ::=
par(nsepseq(expr,COMMA))
arguments ::=
tuple_inj
list_expr ::=
injection(List,expr)
| Nil
(* Patterns *)
pattern ::=
nsepseq(core_pattern,CONS)
core_pattern ::=
Ident (* var *)
| WILD
| Int
| String
| C_Unit
| C_False
| C_True
| C_None
| list_pattern
| tuple_pattern
| constr_pattern
| C_Some par(core_pattern)
list_pattern ::=
injection(List,core_pattern)
| Nil
| par(cons_pattern)
cons_pattern ::=
core_pattern CONS pattern
tuple_pattern ::=
par(nsepseq(core_pattern,COMMA))
constr_pattern ::=
Constr tuple_pattern
| Constr

View File

@ -0,0 +1,368 @@
left_assoc(item,op)
right_assoc(item,op) ::=
item
| item op right_assoc(item,op)
option(X) :=
(**)
| X
series(item,sep,term) ::=
item after_item(item,sep,term)
after_item(item,sep,term) ::=
sep item_or_closing(item,sep,term)
| term
item_or_closing(item,sep,term) ::=
term
| series(item,sep,term)
(* Compound constructs *)
par(X) ::= LPAR X RPAR
brackets(X) ::= LBRACKET X RBRACKET
(* Sequences *)
(* Possibly empty sequence of items *)
seq(X) ::=
(**)
| X seq(X)
(* Non-empty sequence of items *)
nseq(X) ::= X seq(X)
(* Non-empty separated sequence of items *)
nsepseq(X,Sep) ::=
X
| X Sep nsepseq(X,Sep)
(* Possibly empy separated sequence of items *)
sepseq(X,Sep) ::=
(**)
| nsepseq(X,Sep)
(* Main *)
contract ::=
nseq(declaration) EOF
declaration ::=
type_decl option(SEMI)
| const_decl option(SEMI)
| lambda_decl option(SEMI)
(* Type declarations *)
type_decl ::=
Type Ident (* type_name *) Is type_expr
type_expr ::=
cartesian
| sum_type
| record_type
cartesian ::=
nsepseq(function_type,TIMES)
function_type ::=
right_assoc(core_type,ARROW)
core_type ::=
Ident (* type_name *)
| Ident (* type_name *) type_tuple
| Map type_tuple
| Set par(type_expr)
| List par(type_expr)
| par(type_expr)
type_tuple ::=
par(nsepseq(type_expr,COMMA))
sum_type ::=
nsepseq(variant,VBAR)
| VBAR nsepseq(variant,VBAR)
variant ::=
Constr Of cartesian
| Constr
record_type ::=
Record series(field_decl,SEMI,End)
| Record LBRACKET series(field_decl,SEMI,RBRACKET)
field_decl ::=
Ident (* field_name *) COLON type_expr
(* Function and procedure declarations *)
lambda_decl ::=
fun_decl
| proc_decl
| entry_decl
fun_decl ::=
Function Ident (* fun_name *) parameters COLON type_expr Is
seq(local_decl)
block
With expr
entry_decl ::=
Entrypoint Ident (* fun_name *) entry_params COLON type_expr Is
seq(local_decl)
block
With expr
entry_params ::=
par(nsepseq(entry_param_decl,SEMI))
proc_decl ::=
Procedure Ident (* fun_name *) parameters Is
seq(local_decl)
block
parameters ::=
par(nsepseq(param_decl,SEMI))
param_decl ::=
Var Ident (* var *) COLON param_type
| Const Ident (* var *) COLON param_type
entry_param_decl ::=
param_decl
| Storage Ident (* var *) COLON param_type
param_type ::=
cartesian
block ::=
Begin series(statement,SEMI,End)
| Block LBRACE series(statement,SEMI,RBRACE)
statement ::=
instruction
| data_decl
data_decl ::=
const_decl
| var_decl
const_decl ::=
Const unqualified_decl(EQUAL)
var_decl ::=
Var unqualified_decl(ASS)
local_decl ::=
fun_decl option(SEMI)
| proc_decl option(SEMI)
| data_decl option(SEMI)
unqualified_decl(op) ::=
Ident (* var *) COLON type_expr op expr
instruction ::=
single_instr
| block
single_instr ::=
If expr Then if_clause option(SEMI) Else if_clause
| case(instruction)
| Ident (* proc_name *) arguments
| Ident ASS expr
| Ident brackets(expr) ASS expr
| Ident DOT nsepseq(selection,DOT) option(brackets(expr)) ASS expr
| loop
| Fail expr
| Skip
| Patch path With structure
| Remove expr From Map path
| Remove expr From Set path
injection(Kind,element) ::=
Kind series(element,SEMI,End)
| Kind End
| Kind LBRACKET bracketed
bracketed ::=
series(element,SEMI,RBRACKET)
| RBRACKET
binding ::=
expr ARROW expr
if_clause ::=
instruction
| LBRACE series(statement,COMMA,RBRACE)
case(rhs) ::=
Case expr Of cases(rhs) End
| Case expr Of LBRACKET cases(rhs) RBRACKET
cases(rhs) ::=
nsepseq(case_clause(rhs),VBAR)
| VBAR nsepseq(case_clause(rhs),VBAR)
case_clause(rhs) ::=
pattern ARROW rhs
loop ::=
while_loop
| for_loop
while_loop ::=
While expr block
for_loop ::=
For Ident ASS expr option(Down) To expr option(step_clause) block
| For Ident In expr block
| For Ident ARROW Ident In expr block
step_clause ::=
Step expr
(* Expressions *)
interactive_expr ::=
expr EOF
expr ::=
case(expr)
| annot_expr
annot_expr ::=
LPAR disj_expr COLON type_expr RPAR
| 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)
| tuple_expr
| list_expr
| structure
structure ::=
injection(Map,binding)
| injection(Set,expr)
| record_expr
path ::=
Ident (* var *)
| Ident (* struct_name *) DOT nsepseq(selection,DOT)
selection ::=
Ident (* field_name *)
| Int
record_expr ::=
Record series(field_assignment,SEMI,End)
| Record LBRACKET series(field_assignment,SEMI,RBRACKET)
field_assignment ::=
Ident (* field_name *) EQUAL expr
tuple_expr ::=
tuple_inj
tuple_inj ::=
par(nsepseq(expr,COMMA))
arguments ::=
tuple_inj
list_expr ::=
injection(List,expr)
| Nil
(* Patterns *)
pattern ::=
nsepseq(core_pattern,CONS)
core_pattern ::=
Ident (* var *)
| WILD
| Int
| String
| C_Unit
| C_False
| C_True
| C_None
| list_pattern
| tuple_pattern
| constr_pattern
| C_Some par(core_pattern)
list_pattern ::=
injection(List,core_pattern)
| Nil
| par(cons_pattern)
cons_pattern ::=
core_pattern CONS pattern
tuple_pattern ::=
par(nsepseq(core_pattern,COMMA))
constr_pattern ::=
Constr tuple_pattern
| Constr

View File

@ -1,8 +1,26 @@
(* Parsing the command-line option for testing the LIGO lexer and
parser *)
(* Parsing the command-line options of PascaLIGO *)
(* The type [command] denotes some possible behaviours of the
compiler. *)
type command = Quiet | Copy | Units | Tokens
(* The type [options] gathers the command-line options. *)
type options = {
input : string option;
libs : string list;
verbose : Utils.String.Set.t;
offsets : bool;
mode : [`Byte | `Point];
cmd : command
}
(* Auxiliary functions *)
let printf = Printf.printf
let sprintf = Printf.sprintf
let print = print_endline
let abort msg =
Utils.highlight (sprintf "Command-line error: %s\n" msg); exit 1
@ -12,18 +30,18 @@ let abort msg =
let help () =
let file = Filename.basename Sys.argv.(0) in
printf "Usage: %s [<option> ...] [<input>.ligo | \"-\"]\n" file;
print_endline "where <input>.ligo is the LIGO source file (default: stdin),";
print_endline "and each <option> (if any) is one of the following:";
print_endline " -I <paths> Library paths (colon-separated)";
print_endline " -c, --copy Print lexemes of tokens and markup (lexer)";
print_endline " -t, --tokens Print tokens (lexer)";
print_endline " -u, --units Print tokens and markup (lexer)";
print_endline " -q, --quiet No output, except errors (default)";
print_endline " --columns Columns for source locations";
print_endline " --bytes Bytes for source locations";
print_endline " --verbose=<stages> cmdline, cpp, ast (colon-separated)";
print_endline " --version Commit hash on stdout";
print_endline " -h, --help This help";
print "where <input>.ligo is the PascaLIGO source file (default: stdin),";
print "and each <option> (if any) is one of the following:";
print " -I <paths> Library paths (colon-separated)";
print " -c, --copy Print lexemes of tokens and markup (lexer)";
print " -t, --tokens Print tokens (lexer)";
print " -u, --units Print tokens and markup (lexer)";
print " -q, --quiet No output, except errors (default)";
print " --columns Columns for source locations";
print " --bytes Bytes for source locations";
print " --verbose=<stages> cmdline, cpp, ast (colon-separated)";
print " --version Commit hash on stdout";
print " -h, --help This help";
exit 0
(* Version *)
@ -41,6 +59,7 @@ and bytes = ref false
and verbose = ref Utils.String.Set.empty
and input = ref None
and libs = ref []
and verb_str = ref ""
let split_at_colon = Str.(split (regexp ":"))
@ -71,28 +90,12 @@ let specs =
let anonymous arg =
match !input with
None -> input := Some arg
| Some _ -> abort (sprintf "Multiple inputs")
;;
(* Parsing the command-line options *)
try Getopt.parse_cmdline specs anonymous with
Getopt.Error msg -> abort msg
| Some s -> Printf.printf "s=%s\n" s;
abort (sprintf "Multiple inputs")
;;
(* Checking options and exporting them as non-mutable values *)
type command = Quiet | Copy | Units | Tokens
let cmd =
match !quiet, !copy, !units, !tokens with
false, false, false, false
| true, false, false, false -> Quiet
| false, true, false, false -> Copy
| false, false, true, false -> Units
| false, false, false, true -> Tokens
| _ -> abort "Choose one of -q, -c, -u, -t."
let string_of convert = function
None -> "None"
| Some s -> sprintf "Some %s" (convert s)
@ -103,11 +106,6 @@ let string_of_path p =
let quote s = sprintf "\"%s\"" s
let verbose_str =
let apply e a =
if a <> "" then sprintf "%s, %s" e a else e
in Utils.String.Set.fold apply !verbose ""
let print_opt () =
printf "COMMAND LINE\n";
printf "copy = %b\n" !copy;
@ -116,12 +114,14 @@ let print_opt () =
printf "quiet = %b\n" !quiet;
printf "columns = %b\n" !columns;
printf "bytes = %b\n" !bytes;
printf "verbose = \"%s\"\n" verbose_str;
printf "verbose = %s\n" !verb_str;
printf "input = %s\n" (string_of quote !input);
printf "libs = %s\n" (string_of_path !libs)
;;
if Utils.String.Set.mem "cmdline" !verbose then print_opt ();;
let check () =
let () =
if Utils.String.Set.mem "cmdline" !verbose then print_opt () in
let input =
match !input with
@ -131,7 +131,7 @@ let input =
then if Sys.file_exists file_path
then Some file_path
else abort "Source file not found."
else abort "Source file lacks the extension .ligo."
else abort "Source file lacks the extension .ligo." in
(* Exporting remaining options as non-mutable values *)
@ -142,9 +142,9 @@ and quiet = !quiet
and offsets = not !columns
and mode = if !bytes then `Byte else `Point
and verbose = !verbose
and libs = !libs
;;
and libs = !libs in
let () =
if Utils.String.Set.mem "cmdline" verbose then
begin
printf "\nEXPORTED COMMAND LINE\n";
@ -154,8 +154,30 @@ if Utils.String.Set.mem "cmdline" verbose then
printf "quiet = %b\n" quiet;
printf "offsets = %b\n" offsets;
printf "mode = %s\n" (if mode = `Byte then "`Byte" else "`Point");
printf "verbose = \"%s\"\n" verbose_str;
printf "verbose = %s\n" !verb_str;
printf "input = %s\n" (string_of quote input);
printf "I = %s\n" (string_of_path libs)
end
;;
printf "libs = %s\n" (string_of_path libs)
end in
let cmd =
match quiet, copy, units, tokens with
false, false, false, false
| true, false, false, false -> Quiet
| false, true, false, false -> Copy
| false, false, true, false -> Units
| false, false, false, true -> Tokens
| _ -> abort "Choose one of -q, -c, -u, -t."
in {input; libs; verbose; offsets; mode; cmd}
(* Parsing the command-line options *)
let read () =
try
Getopt.parse_cmdline specs anonymous;
(verb_str :=
let apply e a =
if a <> "" then Printf.sprintf "%s, %s" e a else e
in Utils.String.Set.fold apply !verbose "");
check ()
with Getopt.Error msg -> abort msg

View File

@ -1,35 +1,8 @@
(* Parsing the command-line option for testing the LIGO lexer and
parser *)
(* Parsing the command-line options of PascaLIGO *)
(* If the value [offsets] is [true], then the user requested that
messages about source positions and regions be expressed in terms
of horizontal offsets. *)
(* The type [command] denotes some possible behaviours of the
compiler. The constructors are
val offsets : bool
(* If the value [mode] is [`Byte], then the unit in which source
positions and regions are expressed in messages is the byte. If
[`Point], the unit is unicode points. *)
val mode : [`Byte | `Point]
(* If the option [verbose] is set to a list of predefined stages of
the compiler chain, then more information may be displayed about
those stages. *)
val verbose : Utils.String.Set.t
(* If the value [input] is [None] or [Some "-"], the input is standard
input. If [Some f], then the input is the file whose name (file
path) is [f]. *)
val input : string option
(* Paths where to find LIGO files for inclusion *)
val libs : string list
(* If the value [cmd] is
* [Quiet], then no output from the lexer and parser should be
expected, safe error messages: this is the default value;
* [Copy], then lexemes of tokens and markup will be printed to
@ -43,4 +16,37 @@ val libs : string list
type command = Quiet | Copy | Units | Tokens
val cmd : command
(* The type [options] gathers the command-line options.
If the field [input] is [Some src], the name of the PascaLIGO
source file, with the extension ".ligo", is [src]. If [input] is
[Some "-"] or [None], the source file is read from standard input.
The field [libs] is the paths where to find PascaLIGO files for
inclusion (#include).
The field [verbose] is a set of stages of the compiler chain,
about which more information may be displayed.
If the field [offsets] is [true], then the user requested that
messages about source positions and regions be expressed in terms
of horizontal offsets.
If the value [mode] is [`Byte], then the unit in which source
positions and regions are expressed in messages is the byte. If
[`Point], the unit is unicode points.
*)
type options = {
input : string option;
libs : string list;
verbose : Utils.String.Set.t;
offsets : bool;
mode : [`Byte | `Point];
cmd : command
}
(* Parsing the command-line options on stdin *)
val read : unit -> options

View File

@ -6,7 +6,7 @@
early reject potentially misleading or poorly written
LIGO contracts;
(2) provide precise error messages with hint as how to fix the
(2) provide precise error messages with hints as how to fix the
issue, which is achieved by consulting the lexical
right-context of lexemes;
@ -15,23 +15,24 @@
specification: this is achieved by using the most general
regular expressions to match the lexing buffer and broadly
distinguish the syntactic categories, and then delegating a
finer, protocol-dependent, second analysis to an external
module making the tokens (hence a functor below);
finer, second analysis to an external module making the
tokens (hence a functor below);
(4) support unit testing (lexing of the whole input with debug
traces);
traces).
The limitation to the protocol independence lies in the errors that
the external module building the tokens (which is
protocol-dependent) may have to report. Indeed these errors have to
be contextualised by the lexer in terms of input source regions, so
useful error messages can be printed, therefore they are part of
the signature [TOKEN] that parameterise 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, it is more likely that
instructions or types are added, instead of new kinds of tokens.
A limitation to the independence with respect to the LIGO version
lies in the errors that the external module building the tokens
(which may be version-dependent) may have to report. Indeed these
errors have to be contextualised by the lexer in terms of input
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.
*)
module Region = Simple_utils.Region
@ -96,7 +97,7 @@ module type TOKEN =
[open_token_stream], which returns
* a function [read] that extracts tokens from a lexing buffer,
* together with a lexing buffer [buffer] to read from,
together with a lexing buffer [buffer] to read from,
* a function [close] that closes that buffer,
* a function [get_pos] that returns the current position, and
* a function [get_last] that returns the region of the last
@ -105,12 +106,11 @@ module type TOKEN =
Note that a module [Token] is exported too, because the signature
of the exported functions depend on it.
The call [read ~log] evaluates in a lexer (a.k.a tokeniser or
scanner) whose type is [Lexing.lexbuf -> token], and suitable for a
parser generated by Menhir.
The argument labelled [log] is a logger. It may print a token and
its left markup to a given channel, at the caller's discretion.
The call [read ~log] evaluates in a lexer (also known as a
tokeniser or scanner) whose type is [Lexing.lexbuf -> token], and
suitable for a parser generated by Menhir. The argument labelled
[log] is a logger, that is, it may print a token and its left
markup to a given channel, at the caller's discretion.
*)
module type S =
@ -135,7 +135,8 @@ module type S =
exception Error of Error.t Region.reg
val print_error : ?offsets:bool -> [`Byte | `Point] ->
val print_error :
?offsets:bool -> [`Byte | `Point] ->
Error.t Region.reg -> file:bool -> unit
end

View File

@ -720,7 +720,7 @@ and scan_utf8 thread state = parse
[lex_start_p] and [lex_curr_p], as these fields are read by parsers
generated by Menhir when querying source positions (regions). This
is the purpose of the function [patch_buffer]. After reading one
ore more tokens and markup by the scanning rule [scan], we have to
or more tokens and markup by the scanning rule [scan], we have to
save in the hidden reference [buf_reg] the region of the source
that was matched by [scan]. This atomic sequence of patching,
scanning and saving is implemented by the _function_ [scan]

View File

@ -1,12 +1,7 @@
(* Standalone lexer for debugging purposes *)
(* Embedding the lexer of PascaLIGO in a debug module *)
let sprintf = Printf.sprintf
let file =
match EvalOpt.input with
None | Some "-" -> false
| Some _ -> true
module type S =
sig
module Lexer : Lexer.S
@ -39,7 +34,8 @@ module Make (Lexer: Lexer.S) : (S with module Lexer = Lexer) =
let output_nl str = output (str ^ "\n") in
match command with
EvalOpt.Quiet -> ()
| EvalOpt.Tokens -> Token.to_string token ~offsets mode |> output_nl
| EvalOpt.Tokens ->
Token.to_string token ~offsets mode |> output_nl
| EvalOpt.Copy ->
let lexeme = Token.to_lexeme token
and apply acc markup = Markup.to_lexeme markup :: acc
@ -67,6 +63,10 @@ module Make (Lexer: Lexer.S) : (S with module Lexer = Lexer) =
if Token.is_eof token then close_all ()
else iter ()
| exception Lexer.Error e ->
let file =
match file_path_opt with
None | Some "-" -> false
| Some _ -> true in
Lexer.print_error ~offsets mode e ~file;
close_all ()
in iter ()

View File

@ -1,18 +1,22 @@
(* Driver for the lexer of LIGO *)
open! EvalOpt (* Reads the command-line options: Effectful! *)
(* Driver for the lexer of PascaLIGO *)
(* Error printing and exception tracing *)
let () = Printexc.record_backtrace true
(* Running the lexer on the source *)
let options = EvalOpt.read ()
open EvalOpt
let external_ text =
Utils.highlight (Printf.sprintf "External error: %s" text); exit 1;;
(* Path for CPP inclusions (#include) *)
let lib_path =
match EvalOpt.libs with
match options.libs with
[] -> ""
| libs -> let mk_I dir path = Printf.sprintf " -I %s%s" dir path
in List.fold_right mk_I libs ""
@ -20,20 +24,20 @@ let lib_path =
(* Preprocessing the input source and opening the input channels *)
let prefix =
match EvalOpt.input with
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" EvalOpt.verbose
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 EvalOpt.input with
match options.input with
None | Some "-" ->
Printf.sprintf "cpp -traditional-cpp%s - > %s"
lib_path pp_input
@ -42,7 +46,7 @@ let cpp_cmd =
lib_path file pp_input
let () =
if Utils.String.Set.mem "cpp" EvalOpt.verbose
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)
@ -53,5 +57,5 @@ module Lexer = Lexer.Make (LexToken)
module Log = LexerLog.Make (Lexer)
let () = Log.trace ~offsets:EvalOpt.offsets
EvalOpt.mode (Some pp_input) EvalOpt.cmd
let () = Log.trace ~offsets:options.offsets
options.mode (Some pp_input) options.cmd

View File

@ -21,33 +21,22 @@ open AST
(* RULES *)
(* 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. *)
(* The rule [sep_or_term(item,sep)] ("separated or terminated list")
parses a non-empty list of items separated by [sep], and optionally
terminated by [sep]. *)
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)
sep_or_term_list(item,sep):
nsepseq(item,sep) {
$1, None
}
| nseq(item sep {$1,$2}) {
let (first,sep), tail = $1 in
let rec trans (seq, prev_sep as acc) = function
[] -> acc
| (item,next_sep)::others ->
trans ((prev_sep,item)::seq, next_sep) others in
let list, term = trans ([],sep) tail
in (first, List.rev list), Some term }
(* Compound constructs *)
@ -109,13 +98,6 @@ sepseq(X,Sep):
(**) { None }
| nsepseq(X,Sep) { Some $1 }
(* TODO *)
(*
sequence(Item,TERM):
nsepseq(Item,TERM) {}
| nseq(Item TERM {$1,$2}) {}
*)
(* Inlines *)
%inline var : Ident { $1 }
@ -220,24 +202,24 @@ variant:
{region=$1.region; value= {constr=$1; args=None}} }
record_type:
Record series(field_decl,End) {
let first, (others, terminator, closing) = $2 in
let region = cover $1 closing
Record sep_or_term_list(field_decl,SEMI) End {
let elements, terminator = $2 in
let region = cover $1 $3
and value = {
opening = Kwd $1;
elements = Some (first, others);
elements = Some elements;
terminator;
closing = End closing}
closing = End $3}
in {region; value}
}
| Record LBRACKET series(field_decl,RBRACKET) {
let first, (others, terminator, closing) = $3 in
let region = cover $1 closing
| Record LBRACKET sep_or_term_list(field_decl,SEMI) RBRACKET {
let elements, terminator = $3 in
let region = cover $1 $4
and value = {
opening = KwdBracket ($1,$2);
elements = Some (first, others);
elements = Some elements;
terminator;
closing = RBracket closing}
closing = RBracket $4}
in {region; value} }
field_decl:
@ -369,24 +351,24 @@ param_type:
cartesian { TProd $1 }
block:
Begin series(statement,End) {
let first, (others, terminator, closing) = $2 in
let region = cover $1 closing
Begin sep_or_term_list(statement,SEMI) End {
let statements, terminator = $2 in
let region = cover $1 $3
and value = {
opening = Begin $1;
statements = first, others;
statements;
terminator;
closing = End closing}
closing = End $3}
in {region; value}
}
| Block LBRACE series(statement,RBRACE) {
let first, (others, terminator, closing) = $3 in
let region = cover $1 closing
| Block LBRACE sep_or_term_list(statement,SEMI) RBRACE {
let statements, terminator = $3 in
let region = cover $1 $4
and value = {
opening = Block ($1,$2);
statements = first, others;
statements;
terminator;
closing = Block closing}
closing = Block $4}
in {region; value}}
statement:
@ -435,15 +417,9 @@ data_decl:
| var_decl { LocalVar $1 }
unqualified_decl(OP):
var COLON type_expr OP extended_expr {
let init, region =
match $5 with
`Expr e -> e, expr_to_region e
| `EList kwd_nil ->
EList (Nil kwd_nil), kwd_nil
| `ENone region ->
EConstr (NoneExpr region), region
in $1, $2, $3, $4, init, region}
var COLON type_expr OP expr {
let region = expr_to_region $5
in $1, $2, $3, $4, $5, region}
const_decl:
open_const_decl SEMI {
@ -459,12 +435,9 @@ var_decl:
}
| open_var_decl { $1 }
extended_expr:
expr { `Expr $1 }
instruction:
single_instr { Single $1 }
| block { Block $1 : instruction }
| block { Block $1 }
single_instr:
conditional { Cond $1 }
@ -513,7 +486,7 @@ set_patch:
in {region; value}}
map_patch:
Patch path With map_injection {
Patch path With injection(Map,binding) {
let region = cover $1 $4.region in
let value = {
kwd_patch = $1;
@ -523,14 +496,14 @@ map_patch:
in {region; value}}
injection(Kind,element):
Kind series(element,End) {
let first, (others, terminator, closing) = $2 in
let region = cover $1 closing
Kind sep_or_term_list(element,SEMI) End {
let elements, terminator = $2 in
let region = cover $1 $3
and value = {
opening = Kwd $1;
elements = Some (first, others);
elements = Some elements;
terminator;
closing = End closing}
closing = End $3}
in {region; value}
}
| Kind End {
@ -542,14 +515,14 @@ injection(Kind,element):
closing = End $2}
in {region; value}
}
| Kind LBRACKET series(element,RBRACKET) {
let first, (others, terminator, closing) = $3 in
let region = cover $1 closing
| Kind LBRACKET sep_or_term_list(element,SEMI) RBRACKET {
let elements, terminator = $3 in
let region = cover $1 $4
and value = {
opening = KwdBracket ($1,$2);
elements = Some (first, others);
elements = Some elements;
terminator;
closing = RBracket closing}
closing = RBracket $4}
in {region; value}
}
| Kind LBRACKET RBRACKET {
@ -561,45 +534,6 @@ injection(Kind,element):
closing = RBracket $3}
in {region; value}}
map_injection:
Map series(binding,End) {
let first, (others, terminator, closing) = $2 in
let region = cover $1 closing
and value = {
opening = Kwd $1;
elements = Some (first, others);
terminator;
closing = End closing}
in {region; value}
}
| Map End {
let region = cover $1 $2
and value = {
opening = Kwd $1;
elements = None;
terminator = None;
closing = End $2}
in {region; value}
}
| Map LBRACKET series(binding,RBRACKET) {
let first, (others, terminator, closing) = $3 in
let region = cover $1 closing
and value = {
opening = KwdBracket ($1,$2);
elements = Some (first, others);
terminator;
closing = RBracket closing}
in {region; value}
}
| Map LBRACKET RBRACKET {
let region = cover $1 $3
and value = {
opening = KwdBracket ($1,$2);
elements = None;
terminator = None;
closing = RBracket $3}
in {region; value}}
binding:
expr ARROW expr {
let start = expr_to_region $1
@ -647,13 +581,12 @@ if_clause:
instruction {
ClauseInstr $1
}
| LBRACE series(statement,RBRACE) {
let first, (others, terminator, closing) = $2 in
let region = cover $1 closing in
| LBRACE sep_or_term_list(statement,SEMI) RBRACE {
let region = cover $1 $3 in
let value = {
lbrace = $1;
inside = (first, others), terminator;
rbrace = closing} in
inside = $2;
rbrace = $3} in
ClauseBlock {value; region} }
case_instr:
@ -770,16 +703,7 @@ interactive_expr:
expr:
case(expr) { ECase ($1 expr_to_region) }
| annot_expr { $1 }
annot_expr:
LPAR disj_expr COLON type_expr RPAR {
let start = expr_to_region $2
and stop = type_expr_to_region $4 in
let region = cover start stop
and value = ($2 , $4) in
(EAnnot {region; value})
}
(*| annot_expr { $1 }*)
| disj_expr { $1 }
disj_expr:
@ -946,6 +870,7 @@ core_expr:
| C_False { ELogic (BoolExpr (False $1)) }
| C_True { ELogic (BoolExpr (True $1)) }
| C_Unit { EUnit $1 }
| annot_expr { EAnnot $1 }
| tuple_expr { ETuple $1 }
| list_expr { EList $1 }
| C_None { EConstr (NoneExpr $1) }
@ -965,12 +890,21 @@ core_expr:
let region = cover $1 $2.region in
EConstr (SomeApp {region; value = $1,$2})}
annot_expr:
LPAR disj_expr COLON type_expr RPAR {
let start = expr_to_region $2
and stop = type_expr_to_region $4 in
let region = cover start stop
and value = ($2 , $4)
in {region; value}
}
set_expr:
injection(Set,expr) { SetInj $1 }
map_expr:
map_lookup { MapLookUp $1 }
| map_injection { MapInj $1 }
| injection(Map,binding) { MapInj $1 }
map_lookup:
path brackets(expr) {
@ -997,24 +931,24 @@ selection:
| Int { Component $1 }
record_expr:
Record series(field_assignment,End) {
let first, (others, terminator, closing) = $2 in
let region = cover $1 closing
Record sep_or_term_list(field_assignment,SEMI) End {
let elements, terminator = $2 in
let region = cover $1 $3
and value = {
opening = Kwd $1;
elements = Some (first, others);
elements = Some elements;
terminator;
closing = End closing}
closing = End $3}
in {region; value}
}
| Record LBRACKET series(field_assignment,RBRACKET) {
let first, (others, terminator, closing) = $3 in
let region = cover $1 closing
| Record LBRACKET sep_or_term_list(field_assignment,SEMI) RBRACKET {
let elements, terminator = $3 in
let region = cover $1 $4
and value = {
opening = KwdBracket ($1,$2);
elements = Some (first, others);
elements = Some elements;
terminator;
closing = RBracket closing}
closing = RBracket $4}
in {region; value} }
field_assignment:

View File

@ -1,11 +1,23 @@
(* Driver for the parser of LIGO *)
(* Driver for the parser of PascaLIGO *)
open! EvalOpt (* Reads the command-line options: Effectful! *)
(* 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 EvalOpt.input with
match options.input with
None | Some "-" -> false
| Some _ -> true
@ -30,7 +42,7 @@ let print_error ?(offsets=true) mode Region.{region; value} ~file =
(* Path for CPP inclusions (#include) *)
let lib_path =
match EvalOpt.libs with
match options.libs with
[] -> ""
| libs -> let mk_I dir path = Printf.sprintf " -I %s%s" dir path
in List.fold_right mk_I libs ""
@ -38,20 +50,20 @@ let lib_path =
(* Preprocessing the input source and opening the input channels *)
let prefix =
match EvalOpt.input with
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" EvalOpt.verbose
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 EvalOpt.input with
match options.input with
None | Some "-" ->
Printf.sprintf "cpp -traditional-cpp%s - > %s"
lib_path pp_input
@ -60,7 +72,7 @@ let cpp_cmd =
lib_path file pp_input
let () =
if Utils.String.Set.mem "cpp" EvalOpt.verbose
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)
@ -76,8 +88,8 @@ let Lexer.{read; buffer; get_pos; get_last; close} =
and cout = stdout
let log = Log.output_token ~offsets:EvalOpt.offsets
EvalOpt.mode EvalOpt.cmd cout
let log = Log.output_token ~offsets:options.offsets
options.mode options.cmd cout
and close_all () = close (); close_out cout
@ -90,19 +102,21 @@ let tokeniser = read ~log
let () =
try
let ast = Parser.contract tokeniser buffer in
if Utils.String.Set.mem "ast" EvalOpt.verbose
if Utils.String.Set.mem "ast" options.verbose
then begin
ParserLog.offsets := EvalOpt.offsets;
ParserLog.mode := EvalOpt.mode;
ParserLog.offsets := options.offsets;
ParserLog.mode := options.mode;
ParserLog.print_tokens ast
end
with
Lexer.Error err ->
close_all ();
Lexer.print_error ~offsets EvalOpt.mode err ~file
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 EvalOpt.mode error ~file
print_error ~offsets:options.offsets
options.mode error ~file
| Sys_error msg -> Utils.highlight msg

View File

@ -913,6 +913,12 @@ and simpl_cases : type a . (Raw.pattern * a) list -> a matching result = fun t -
let%bind var = get_var single_pat in
ok (const.value , var)
)
(*
| PConstr {value = constr, Some tuple; _} ->
let%bind var = get_single (PTuple tuple) >>? get_var in
ok (constr.value, var)
| PConstr {value = constr, None; _} ->
*)
| _ -> fail @@ only_constructors t in
let%bind patterns =
let aux (x , y) =