Merge branch 'sail2' of github.com:rems-project/sail into sail2

1 files changed, 27 insertions, 4 deletions

diff --git a/src/parser.mly b/src/parser.mly
index 1c7d1580..a1e93388 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -92,6 +92,7 @@ let mk_typ t n m = ATyp_aux (t, loc n m)
 let mk_pat p n m = P_aux (p, loc n m)
 let mk_pexp p n m = Pat_aux (p, loc n m)
 let mk_exp e n m = E_aux (e, loc n m)
+let mk_measure meas n m = Measure_aux (meas, loc n m)
 let mk_lit l n m = L_aux (l, loc n m)
 let mk_lit_exp l n m = mk_exp (E_lit (mk_lit l n m)) n m
 let mk_typschm tq t n m = TypSchm_aux (TypSchm_ts (tq, t), loc n m)
@@ -748,6 +749,13 @@ exp_eof:
   | exp Eof
     { $1 }
 
+/* Internal syntax for loop measures, rejected in normal code by initial_check */
+internal_loop_measure:
+  |
+    { mk_measure Measure_none $startpos $endpos }
+  | TerminationMeasure Lcurly exp Rcurly
+    { mk_measure (Measure_some $3) $startpos $endpos }
+
 exp:
   | exp0
     { $1 }
@@ -802,10 +810,10 @@ exp:
         else ATyp_aux(ATyp_dec,loc $startpos($6) $endpos($6))
       in
       mk_exp (E_for ($3, $5, $7, step, ord, $9)) $startpos $endpos }
-  | Repeat exp Until exp
-    { mk_exp (E_loop (Until, $4, $2)) $startpos $endpos }
-  | While exp Do exp
-    { mk_exp (E_loop (While, $2, $4)) $startpos $endpos }
+  | Repeat internal_loop_measure exp Until exp
+    { mk_exp (E_loop (Until, $2, $5, $3)) $startpos $endpos }
+  | While internal_loop_measure exp Do exp
+    { mk_exp (E_loop (While, $2, $3, $5)) $startpos $endpos }
 
   /* Debugging only, will be rejected in initial_check if debugging isn't on */
   | InternalPLet pat Eq exp In exp
@@ -1056,6 +1064,8 @@ atomic_exp:
     { mk_exp (E_record $3) $startpos $endpos }
   | Lcurly exp With fexp_exp_list Rcurly
     { mk_exp (E_record_update ($2, $4)) $startpos $endpos }
+  | Lsquare Rsquare
+    { mk_exp (E_vector []) $startpos $endpos }
   | Lsquare exp_list Rsquare
     { mk_exp (E_vector $2) $startpos $endpos }
   | Lsquare exp With atomic_exp Eq exp Rsquare
@@ -1401,6 +1411,17 @@ scattered_clause:
   | Function_ Clause funcl
     { mk_sd (SD_funcl $3) $startpos $endpos }
 
+loop_measure:
+  | Until exp
+    { Loop (Until, $2) }
+  | While exp
+    { Loop (While, $2) }
+
+loop_measures:
+  | loop_measure
+    { [$1] }
+  | loop_measure Comma loop_measures
+    { $1::$3 }
 
 def:
   | fun_def
@@ -1439,6 +1460,8 @@ def:
     { DEF_pragma (fst $1, snd $1, loc $startpos $endpos) }
   | TerminationMeasure id pat Eq exp
     { DEF_measure ($2, $3, $5) }
+  | TerminationMeasure id loop_measures
+    { DEF_loop_measures ($2,$3) }
 
 defs_list:
   | def