Merge branch 'sail2' into rmem_interpreter

1 files changed, 26 insertions, 19 deletions

diff --git a/src/parser.mly b/src/parser.mly
index abf533c3..2cd0dbe1 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -134,7 +134,6 @@ let mk_typqn = (TypQ_aux(TypQ_no_forall,Unknown))
 let mk_tannotn = Typ_annot_opt_aux(Typ_annot_opt_none,Unknown)
 let mk_tannot typq typ n m = Typ_annot_opt_aux(Typ_annot_opt_some (typq, typ), loc n m)
 let mk_eannotn = Effect_opt_aux(Effect_opt_pure,Unknown)
-let mk_namesectn = Name_sect_aux(Name_sect_none,Unknown)
 
 let mk_typq kopts nc n m = TypQ_aux (TypQ_tq (List.map qi_id_of_kopt kopts @ nc), loc n m)
 
@@ -178,12 +177,13 @@ let rec desugar_rchain chain s e =
 
 /*Terminals with no content*/
 
-%token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op Where
+%token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op
 %token Enum Else False Forall Foreach Overload Function_ Mapping If_ In Inc Let_ Int Order Bool Cast
 %token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
-%token Undefined Union Newtype With Val Constant Constraint Throw Try Catch Exit Bitfield
+%token Undefined Union Newtype With Val Constraint Throw Try Catch Exit Bitfield
 %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
 %token Repeat Until While Do Mutual Var Ref Configuration TerminationMeasure
+%token InternalPLet InternalReturn
 
 %nonassoc Then
 %nonassoc Else
@@ -807,6 +807,12 @@ exp:
   | While exp Do exp
     { mk_exp (E_loop (While, $2, $4)) $startpos $endpos }
 
+  /* Debugging only, will be rejected in initial_check if debugging isn't on */
+  | InternalPLet pat Eq exp In exp
+    { mk_exp (E_internal_plet ($2,$4,$6)) $startpos $endpos }
+  | InternalReturn exp
+    { mk_exp (E_internal_return($2)) $startpos $endpos }
+
 /* The following implements all nine levels of user-defined precedence for
 operators in expressions, with both left, right and non-associative operators */
 
@@ -1124,9 +1130,9 @@ funcl_typ:
     { mk_tannot mk_typqn $1 $startpos $endpos }
 
 index_range:
-  | Num
+  | typ
     { mk_ir (BF_single $1) $startpos $endpos }
-  | Num DotDot Num
+  | typ DotDot typ
     { mk_ir (BF_range ($1, $3)) $startpos $endpos }
 
 r_id_def:
@@ -1170,21 +1176,21 @@ type_def:
   | Typedef id Colon kind Eq typ
     { mk_td (TD_abbrev ($2, mk_typqn, $4, $6)) $startpos $endpos }
   | Struct id Eq Lcurly struct_fields Rcurly
-    { mk_td (TD_record ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos }
+    { mk_td (TD_record ($2, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos }
   | Struct id typaram Eq Lcurly struct_fields Rcurly
-    { mk_td (TD_record ($2, mk_namesectn, $3, $6, false)) $startpos $endpos }
+    { mk_td (TD_record ($2, $3, $6, false)) $startpos $endpos }
   | Enum id Eq enum_bar
-    { mk_td (TD_enum ($2, mk_namesectn, $4, false)) $startpos $endpos }
+    { mk_td (TD_enum ($2, $4, false)) $startpos $endpos }
   | Enum id Eq Lcurly enum Rcurly
-    { mk_td (TD_enum ($2, mk_namesectn, $5, false)) $startpos $endpos }
+    { mk_td (TD_enum ($2, $5, false)) $startpos $endpos }
   | Newtype id Eq type_union
-    { mk_td (TD_variant ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), [$4], false)) $startpos $endpos }
+    { mk_td (TD_variant ($2, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), [$4], false)) $startpos $endpos }
   | Newtype id typaram Eq type_union
-    { mk_td (TD_variant ($2, mk_namesectn, $3, [$5], false)) $startpos $endpos }
+    { mk_td (TD_variant ($2, $3, [$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 }
+    { mk_td (TD_variant ($2, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos }
   | Union id typaram Eq Lcurly type_unions Rcurly
-    { mk_td (TD_variant ($2, mk_namesectn, $3, $6, false)) $startpos $endpos }
+    { mk_td (TD_variant ($2, $3, $6, false)) $startpos $endpos }
   | Bitfield id Colon typ Eq Lcurly r_def_body Rcurly
     { mk_td (TD_bitfield ($2, $4, $7)) $startpos $endpos }
 
@@ -1363,7 +1369,11 @@ val_spec_def:
 
 register_def:
   | Register id Colon typ
-    { mk_reg_dec (DEC_reg ($4, $2)) $startpos $endpos }
+    { let rreg = mk_typ (ATyp_set [mk_effect BE_rreg $startpos($1) $endpos($1)]) $startpos($1) $endpos($1) in
+      let wreg = mk_typ (ATyp_set [mk_effect BE_wreg $startpos($1) $endpos($1)]) $startpos($1) $endpos($1) in
+      mk_reg_dec (DEC_reg (rreg, wreg, $4, $2)) $startpos $endpos }
+  | Register effect_set effect_set id Colon typ
+    { mk_reg_dec (DEC_reg ($2, $3, $6, $4)) $startpos $endpos }
   | Register Configuration id Colon typ Eq exp
     { mk_reg_dec (DEC_config ($3, $5, $7)) $startpos $endpos }
 
@@ -1375,9 +1385,9 @@ default_def:
 
 scattered_def:
   | Union id typaram
-    { mk_sd (SD_variant($2, mk_namesectn, $3)) $startpos $endpos }
+    { mk_sd (SD_variant($2, $3)) $startpos $endpos }
   | Union id
-    { mk_sd (SD_variant($2, mk_namesectn, mk_typqn)) $startpos $endpos }
+    { mk_sd (SD_variant($2, mk_typqn)) $startpos $endpos }
   | Function_ id
     { mk_sd (SD_function(mk_recn, mk_tannotn, mk_eannotn, $2)) $startpos $endpos }
   | Mapping id
@@ -1423,9 +1433,6 @@ def:
     { DEF_scattered (mk_sd (SD_end $2) $startpos $endpos) }
   | default_def
     { DEF_default $1 }
-  | Constant id Eq typ
-    { DEF_kind (KD_aux (KD_nabbrev (K_aux (K_int, loc $startpos($1) $endpos($1)), $2, mk_namesectn, $4),
-			loc $startpos $endpos)) }
   | Mutual Lcurly fun_def_list Rcurly
     { DEF_internal_mutrec $3 }
   | Pragma