From 7e1293604ff02c072568e03830d25adfea063087 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 29 Sep 2017 16:22:26 +0100
Subject: Some more refactoring of Sail library

- Remove start indices and indexing order from bitvector types. Instead add
  them as arguments to functions accessing/updating bitvectors. These arguments
are effectively implicit, thanks to wrappers in prelude_wrappers.sail and a
"sizeof" rewriting pass.

- Add a typeclass for bitvectors with a few basic functions (converting to/from
  bitlists, converting to an integer, getting and setting bits). Make both
monads use this interface, so that they work with both the bitlist and the
machine word representation of bitvectors.
---
 src/rewriter.ml | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

(limited to 'src/rewriter.ml')

diff --git a/src/rewriter.ml b/src/rewriter.ml
index fed8408d..6d7b29c7 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -1442,10 +1442,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
@@ -1910,12 +1910,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
@@ -1941,12 +1941,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');
-- 
cgit v1.2.3