Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into experiments

1 files changed, 40 insertions, 10 deletions

diff --git a/src/rewriter.ml b/src/rewriter.ml
index e257e19c..c2b8e618 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -130,6 +130,7 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with
       union_effects (fun_app_effects f env) (union_eff_exps [e1;e2])
     | E_if (e1,e2,e3) -> union_eff_exps [e1;e2;e3]
     | E_for (_,e1,e2,e3,_,e4) -> union_eff_exps [e1;e2;e3;e4]
+    | E_loop (_,e1,e2) -> union_eff_exps [e1;e2]
     | E_vector es -> union_eff_exps es
     | E_vector_indexed (ies,opt_default) ->
        let (_,es) = List.split ies in
@@ -388,6 +389,8 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot))) =
   | E_if (c,t,e) -> rewrap (E_if (rewrite c,rewrite t, rewrite e))
   | E_for (id, e1, e2, e3, o, body) ->
     rewrap (E_for (id, rewrite e1, rewrite e2, rewrite e3, o, rewrite body))
+  | E_loop (loop, e1, e2) ->
+    rewrap (E_loop (loop, rewrite e1, rewrite e2))
   | E_vector exps -> rewrap (E_vector (List.map rewrite exps))
   | E_vector_indexed (exps,(Def_val_aux(default,dannot))) ->
     let def = match default with
@@ -1449,10 +1452,10 @@ let remove_vector_concat_pat pat =
       let index_j = simple_num l j in
 
       (* FIXME *)
-      (* let subv = fix_eff_exp (E_aux (E_vector_subrange (root, index_i, index_j), cannot)) in *)
-      let (_, _, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of root) (typ_of root)) in
+      let subv = fix_eff_exp (E_aux (E_vector_subrange (root, index_i, index_j), cannot)) in
+      (* let (_, _, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of root) (typ_of root)) in
       let subrange_id = if is_order_inc ord then "bitvector_subrange_inc" else "bitvector_subrange_dec" in
-      let subv = fix_eff_exp (E_aux (E_app (mk_id subrange_id, [root; index_i; index_j]), cannot)) in
+      let subv = fix_eff_exp (E_aux (E_app (mk_id subrange_id, [root; index_i; index_j]), cannot)) in *)
 
       let id_pat =
         match typ_opt with
@@ -1917,12 +1920,12 @@ let remove_bitvector_pat pat =
   let access_bit_exp (rootid,rannot) l idx =
     let root : tannot exp = E_aux (E_id rootid,rannot) in
     (* FIXME *)
-    (* E_aux (E_vector_access (root,simple_num l idx), simple_annot l bit_typ) in *)
-    let env = env_of_annot rannot in
+    E_aux (E_vector_access (root,simple_num l idx), simple_annot l bit_typ) in
+    (*let env = env_of_annot rannot in
     let t = Env.base_typ_of env (typ_of_annot rannot) in
     let (_, _, ord, _) = vector_typ_args_of t in
     let access_id = if is_order_inc ord then "bitvector_access_inc" else "bitvector_access_dec" in
-    E_aux (E_app (mk_id access_id, [root; simple_num l idx]), simple_annot l bit_typ) in
+    E_aux (E_app (mk_id access_id, [root; simple_num l idx]), simple_annot l bit_typ) in*)
 
   let test_bit_exp rootid l t idx exp =
     let rannot = simple_annot l t in
@@ -1948,12 +1951,12 @@ let remove_bitvector_pat pat =
       (*if vec_start t = i && vec_length t = List.length lits
       then E_id rootid
       else*)
-          (* E_vector_subrange (
+          E_vector_subrange (
              E_aux (E_id rootid, simple_annot l typ),
              simple_num l i,
-             simple_num l j) in *)
-          let subrange_id = if is_order_inc ord then "bitvector_subrange_inc" else "bitvector_subrange_dec" in
-          E_app (mk_id subrange_id, [E_aux (E_id rootid, simple_annot l typ); simple_num l i; simple_num l j]) in
+             simple_num l j) in
+          (* let subrange_id = if is_order_inc ord then "bitvector_subrange_inc" else "bitvector_subrange_dec" in
+          E_app (mk_id subrange_id, [E_aux (E_id rootid, simple_annot l typ); simple_num l i; simple_num l j]) in *)
     E_aux (E_app(
       Id_aux (Id "eq_vec", Parse_ast.Generated l),
       [E_aux (subvec_exp, simple_annot l typ');
@@ -2847,6 +2850,10 @@ let rewrite_defs_letbind_effects  =
        n_exp_name by (fun by ->
        let body = n_exp_term (effectful body) body in
        k (rewrap (E_for (id,start,stop,by,dir,body))))))
+    | E_loop (loop, cond, body) ->
+       let cond = n_exp_term (effectful cond) cond in
+       let body = n_exp_term (effectful body) body in
+       k (rewrap (E_loop (loop,cond,body)))
     | E_vector exps ->
        n_exp_nameL exps (fun exps ->
        k (rewrap (E_vector exps)))
@@ -3171,6 +3178,29 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
          else P_aux (P_tup [pat; mktup_pat pl vars],
                      simple_annot pl (typ_of v)) in
        Added_vars (v,pat)
+     | E_loop(loop,cond,body) ->
+        let vars = List.map (fun (var,(l,t)) -> E_aux (E_id var,(l,t))) (find_updated_vars body) in
+        let vartuple = mktup el vars in
+        (* let cond = rewrite_var_updates (add_vars false cond vartuple) in *)
+        let body = rewrite_var_updates (add_vars overwrite body vartuple) in
+        let (E_aux (_,(_,bannot))) = body in
+        let fname = match effectful cond, effectful body with
+          | false, false -> "while_PP"
+          | false, true  -> "while_PM"
+          | true,  false -> "while_MP"
+          | true,  true  -> "while_MM" in
+        let funcl = Id_aux (Id fname,Parse_ast.Generated el) in
+        let is_while =
+          match loop with
+          | While -> E_aux (E_lit (mk_lit L_true), simple_annot el bool_typ)
+          | Until -> E_aux (E_lit (mk_lit L_false), simple_annot el bool_typ) in
+        let v = E_aux (E_app (funcl,[is_while;cond;body;vartuple]),
+                       (Parse_ast.Generated el, bannot)) in
+        let pat =
+          if overwrite then mktup_pat el vars
+          else P_aux (P_tup [pat; mktup_pat pl vars],
+                      simple_annot pl (typ_of v)) in
+        Added_vars (v,pat)
     | E_if (c,e1,e2) ->
        let vars = List.map (fun (var,(l,t)) -> E_aux (E_id var,(l,t)))
                            (dedup eqidtyp (find_updated_vars e1 @ find_updated_vars e2)) in