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

1 files changed, 18 insertions, 2 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 28446db2..790a6624 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -367,8 +367,8 @@ and to_ast_exp ctx (P.E_aux(exp,l) : P.exp) =
     | P.E_for(id,e1,e2,e3,atyp,e4) ->
       E_for(to_ast_id id,to_ast_exp ctx e1, to_ast_exp ctx e2,
             to_ast_exp ctx e3,to_ast_order ctx atyp, to_ast_exp ctx e4)
-    | P.E_loop (P.While, e1, e2) -> E_loop (While, to_ast_exp ctx e1, to_ast_exp ctx e2)
-    | P.E_loop (P.Until, e1, e2) -> E_loop (Until, to_ast_exp ctx e1, to_ast_exp ctx e2)
+    | P.E_loop (P.While, m, e1, e2) -> E_loop (While, to_ast_measure ctx m, to_ast_exp ctx e1, to_ast_exp ctx e2)
+    | P.E_loop (P.Until, m, e1, e2) -> E_loop (Until, to_ast_measure ctx m, to_ast_exp ctx e1, to_ast_exp ctx e2)
     | P.E_vector(exps) -> E_vector(List.map (to_ast_exp ctx) exps)
     | P.E_vector_access(vexp,exp) -> E_vector_access(to_ast_exp ctx vexp, to_ast_exp ctx exp)
     | P.E_vector_subrange(vex,exp1,exp2) ->
@@ -414,6 +414,16 @@ and to_ast_exp ctx (P.E_aux(exp,l) : P.exp) =
     | _ -> raise (Reporting.err_unreachable l __POS__ "Unparsable construct in to_ast_exp")
     ), (l,()))
 
+and to_ast_measure ctx (P.Measure_aux(m,l)) : unit internal_loop_measure =
+  let m = match m with
+    | P.Measure_none -> Measure_none
+    | P.Measure_some exp ->
+       if !opt_magic_hash then
+         Measure_some (to_ast_exp ctx exp)
+       else
+         raise (Reporting.err_general l "Internal loop termination measure found without -dmagic_hash")
+  in Measure_aux (m,l)
+
 and to_ast_lexp ctx (P.E_aux(exp,l) : P.exp) : unit lexp =
   let lexp = match exp with
     | P.E_id id -> LEXP_id (to_ast_id id)
@@ -762,6 +772,10 @@ let to_ast_prec = function
   | P.InfixL -> InfixL
   | P.InfixR -> InfixR
 
+let to_ast_loop_measure ctx = function
+  | P.Loop (P.While, exp) -> Loop (While, to_ast_exp ctx exp)
+  | P.Loop (P.Until, exp) -> Loop (Until, to_ast_exp ctx exp)
+
 let to_ast_def ctx def : unit def list ctx_out =
   match def with
   | P.DEF_overload (id, ids) ->
@@ -800,6 +814,8 @@ let to_ast_def ctx def : unit def list ctx_out =
      [DEF_scattered sdef], ctx
   | P.DEF_measure (id, pat, exp) ->
      [DEF_measure (to_ast_id id, to_ast_pat ctx pat, to_ast_exp ctx exp)], ctx
+  | P.DEF_loop_measures (id, measures) ->
+     [DEF_loop_measures (to_ast_id id, List.map (to_ast_loop_measure ctx) measures)], ctx
 
 let rec remove_mutrec = function
   | [] -> []