diff options
Diffstat (limited to 'src/rewriter.ml')
| -rw-r--r-- | src/rewriter.ml | 20 |
1 files changed, 10 insertions, 10 deletions
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'); |