Improvements to enable parsing and checking intermediate rewriting

steps

Parser now has syntax for mutual recusion blocks

mutual {
  ... fundefs ...
}

which is used for parsing and pretty printing
DEF_internal_mutrec. It's stripped away by the initial_check, so the
typechecker never sees DEF_internal_mutrec. Maybe this could change,
as forcing mutual recursion to be explicit would probably be a good
thing.

Added record syntax to the new parser

New option -dmagic_hash is similar to GHC's -XMagicHash in that it
allows for identifiers to contain the special hash character, which is
used to introduce new autogenerated variables in a way that doesn't
clash with existing names.

Option -sil compiles sail down to the intermediate language defined in
sil.ott (not complete yet).

1 files changed, 26 insertions, 2 deletions

diff --git a/src/parser2.mly b/src/parser2.mly
index a752e5c1..1444f6cd 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -142,13 +142,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 +957,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] }
@@ -1042,6 +1058,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 +1137,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