Added alternate syntax for record types, with brackets.

New syntax: record [...]
This commit is contained in:
Christian Rinderknecht 2019-04-01 14:51:07 +02:00
parent b1502106e9
commit 0d98252fa0
No known key found for this signature in database
GPG Key ID: 9446816CFD267040
4 changed files with 20 additions and 32 deletions

View File

@ -191,7 +191,7 @@ and type_decl = {
and type_expr =
TProd of cartesian
| TSum of (variant reg, vbar) nsepseq reg
| TRecord of record_type reg
| TRecord of record_type
| TApp of (type_name * type_tuple) reg
| TPar of type_expr par reg
| TAlias of variable
@ -204,14 +204,7 @@ and variant = {
product : cartesian
}
and record_type = {
opening : kwd_record;
field_decls : field_decls;
terminator : semi option;
closing : kwd_end
}
and field_decls = (field_decl reg, semi) nsepseq
and record_type = field_decl reg injection reg
and field_decl = {
field_name : field_name;
@ -932,12 +925,8 @@ and print_variant {value; _} =
and print_sum_type {value; _} =
print_nsepseq "|" print_variant value
and print_record_type {value; _} =
let {opening; field_decls; terminator; closing} = value in
print_token opening "record";
print_field_decls field_decls;
print_terminator terminator;
print_token closing "end"
and print_record_type record_type =
print_injection "record" print_field_decl record_type
and print_type_app {value; _} =
let type_name, type_tuple = value in
@ -950,9 +939,6 @@ and print_par_type {value; _} =
print_type_expr inside;
print_token rpar ")"
and print_field_decls sequence =
print_nsepseq ";" print_field_decl sequence
and print_field_decl {value; _} =
let {field_name; colon; field_type} = value in
print_var field_name;

View File

@ -175,7 +175,7 @@ and type_decl = {
and type_expr =
TProd of cartesian
| TSum of (variant reg, vbar) nsepseq reg
| TRecord of record_type reg
| TRecord of record_type
| TApp of (type_name * type_tuple) reg
| TPar of type_expr par reg
| TAlias of variable
@ -188,14 +188,7 @@ and variant = {
product : cartesian
}
and record_type = {
opening : kwd_record;
field_decls : field_decls;
terminator : semi option;
closing : kwd_end
}
and field_decls = (field_decl reg, semi) nsepseq
and record_type = field_decl reg injection reg
and field_decl = {
field_name : field_name;

View File

@ -205,10 +205,19 @@ record_type:
let first, (others, terminator, closing) = $2 in
let region = cover $1 closing
and value = {
opening = $1;
field_decls = first, others;
opening = Kwd $1;
elements = Some (first, others);
terminator;
closing}
closing = End closing}
in {region; value}}
| Record LBRACKET series(field_decl,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}}
field_decl:

View File

@ -1,10 +1,10 @@
type store is
record
record [
goal : nat;
deadline : timestamp;
backers : map (address, nat);
funded : bool;
end
]
entrypoint contribute (storage store : store;
const sender : address;