diff options
Diffstat (limited to 'src/parser2.mly')
| -rw-r--r-- | src/parser2.mly | 38 |
1 files changed, 36 insertions, 2 deletions
diff --git a/src/parser2.mly b/src/parser2.mly index a752e5c1..21959cf5 100644 --- a/src/parser2.mly +++ b/src/parser2.mly @@ -9,6 +9,14 @@ /* Robert Norton-Wright */ /* Christopher Pulte */ /* Peter Sewell */ +/* Alasdair Armstrong */ +/* Brian Campbell */ +/* Thomas Bauereiss */ +/* Anthony Fox */ +/* Jon French */ +/* Dominic Mulligan */ +/* Stephen Kell */ +/* Mark Wassell */ /* */ /* All rights reserved. */ /* */ @@ -142,13 +150,13 @@ let rec desugar_rchain chain s e = %token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef %token Undefined Union With Val Constraint Throw Try Catch Exit %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape -%token Repeat Until While Do +%token Repeat Until While Do Record Mutual %nonassoc Then %nonassoc Else %token Bar Comma Dot Eof Minus Semi Under DotDot -%token Lcurly Rcurly Lparen Rparen Lsquare Rsquare LcurlyBar RcurlyBar +%token Lcurly Rcurly Lparen Rparen Lsquare Rsquare LcurlyBar RcurlyBar LsquareBar RsquareBar %token MinusGt /*Terminals with content*/ @@ -957,17 +965,33 @@ atomic_exp: { mk_exp (E_vector_access ($1, $3)) $startpos $endpos } | atomic_exp Lsquare exp DotDot exp Rsquare { mk_exp (E_vector_subrange ($1, $3, $5)) $startpos $endpos } + | Record Lcurly fexp_exp_list Rcurly + { mk_exp (E_record $3) $startpos $endpos } + | Lcurly exp With fexp_exp_list Rcurly + { mk_exp (E_record_update ($2, $4)) $startpos $endpos } | Lsquare exp_list Rsquare { mk_exp (E_vector $2) $startpos $endpos } | Lsquare exp With atomic_exp Eq exp Rsquare { mk_exp (E_vector_update ($2, $4, $6)) $startpos $endpos } | Lsquare exp With atomic_exp DotDot atomic_exp Eq exp Rsquare { mk_exp (E_vector_update_subrange ($2, $4, $6, $8)) $startpos $endpos } + | LsquareBar exp_list RsquareBar + { mk_exp (E_list $2) $startpos $endpos } | Lparen exp Rparen { $2 } | Lparen exp Comma exp_list Rparen { mk_exp (E_tuple ($2 :: $4)) $startpos $endpos } +fexp_exp: + | atomic_exp Eq exp + { mk_exp (E_app_infix ($1, mk_id (Id "=") $startpos($2) $endpos($2), $3)) $startpos $endpos } + +fexp_exp_list: + | fexp_exp + { [$1] } + | fexp_exp Comma fexp_exp_list + { $1 :: $3 } + exp_list: | exp { [$1] } @@ -997,6 +1021,8 @@ type_def: { mk_td (TD_enum ($2, mk_namesectn, $4, false)) $startpos $endpos } | Enum id Eq Lcurly enum Rcurly { mk_td (TD_enum ($2, mk_namesectn, $5, false)) $startpos $endpos } + | Union id Eq Lcurly type_unions Rcurly + { mk_td (TD_variant ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos } | Union id typquant Eq Lcurly type_unions Rcurly { mk_td (TD_variant ($2, mk_namesectn, $3, $6, false)) $startpos $endpos } @@ -1042,6 +1068,12 @@ fun_def: | Function_ funcls { mk_fun (FD_function (mk_recn, mk_tannotn, mk_eannotn, $2)) $startpos $endpos } +fun_def_list: + | fun_def + { [$1] } + | fun_def fun_def_list + { $1 :: $2 } + let_def: | Let_ letbind { $2 } @@ -1115,6 +1147,8 @@ def: { DEF_scattered (mk_sd (SD_scattered_end $2) $startpos $endpos) } | default_def { DEF_default $1 } + | Mutual Lcurly fun_def_list Rcurly + { DEF_internal_mutrec $3 } defs_list: | def |