add some missing things in sail_values and make big_int version the default for set_vector_subrange_bit.

2 files changed, 16 insertions, 10 deletions

diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml
index 7e6f0ae7..a0b8e514 100644
--- a/src/gen_lib/sail_values.ml
+++ b/src/gen_lib/sail_values.ml
@@ -7,9 +7,11 @@ let tracef = printf
 (* only expected to be 0, 1, 2; 2 represents undef *)
 type vbit = Vone | Vzero | Vundef
 type number = Big_int_Z.big_int
+
 type _bool = vbit
 type _string = string
 type _nat = number
+type _int = number
 
 let undef_val = ref Vundef
 
@@ -211,7 +213,7 @@ let set_vector_subrange_bit_int v n m new_v =
 
 let set_vector_subrange_bit_big v n m new_v =
   set_vector_subrange_bit_int v (int_of_big_int n) (int_of_big_int m) new_v
-let set_vector_subrange_bit = set_vector_subrange_bit_int
+let set_vector_subrange_bit = set_vector_subrange_bit_big
 
 let set_register_bit_int reg n v = 
   match reg with
@@ -235,7 +237,7 @@ let set_register_field_v reg field new_v =
      | (i,j) ->
        if i = j
        then ()
-       else set_vector_subrange_bit reg i j new_v)
+       else set_vector_subrange_bit_int reg i j new_v)
      end
   | _ -> ()
 
@@ -1186,6 +1188,7 @@ let eq_bit = bitwise_binop_bit (=)
 
 let neq (l,r) = bitwise_not_bit (eq (l,r))
 let neq_vec (l,r) = bitwise_not_bit (eq_vec_vec(l,r))
+let neq_vec_range (l,r) = bitwise_not_bit (eq_vec_range (l,r))
 let neq_bit (l,r) = bitwise_not_bit (eq_bit(l,r))
 let neq_range = neq
 
diff --git a/src/pretty_print_ocaml.ml b/src/pretty_print_ocaml.ml
index 0ce8d782..3772f549 100644
--- a/src/pretty_print_ocaml.ml
+++ b/src/pretty_print_ocaml.ml
@@ -52,10 +52,13 @@ open Pretty_print_common
 
 let star_sp = star ^^ space
 
+let sanitize_name s = 
+  "_" ^ s
+
 let doc_id_ocaml (Id_aux(i,_)) =
   match i with
   | Id("bit") -> string "vbit"
-  | Id i -> string ("_" ^ i)
+  | Id i -> string (sanitize_name i)
   | DeIid x ->
       (* add an extra space through empty to avoid a closing-comment
        * token in case of x ending with star. *)
@@ -64,7 +67,7 @@ let doc_id_ocaml (Id_aux(i,_)) =
 let doc_id_ocaml_type (Id_aux(i,_)) =
   match i with
   | Id("bit") -> string "vbit"
-  | Id i -> string ("_" ^ i)
+  | Id i -> string (sanitize_name i)
   | DeIid x ->
       (* add an extra space through empty to avoid a closing-comment
        * token in case of x ending with star. *)
@@ -308,16 +311,16 @@ let doc_exp_ocaml, doc_let_ocaml =
            let field_f = match t.t with
              | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> string "get_register_field_bit"
              | _ -> string "get_register_field_vec" in
-           parens (separate space [field_f; string (String.uncapitalize reg); string_lit (string field)])
+           parens (separate space [field_f; string (sanitize_name reg); string_lit (string field)])
          | Alias_extract(reg,start,stop) ->
            if start = stop
-           then parens (separate space [string "bit_vector_access";string (String.uncapitalize reg);doc_int start])
+           then parens (separate space [string "bit_vector_access";string (sanitize_name reg);doc_int start])
            else parens
-               (separate space [string "vector_subrange"; string (String.uncapitalize reg); doc_int start; doc_int stop])
+               (separate space [string "vector_subrange"; string (sanitize_name reg); doc_int start; doc_int stop])
          | Alias_pair(reg1,reg2) ->
            parens (separate space [string "vector_concat";
-                                   string (String.uncapitalize reg1);
-                                   string (String.uncapitalize reg2)]))
+                                   string (sanitize_name reg1);
+                                   string (sanitize_name reg2)]))
       | _ -> doc_id_ocaml id)
     | E_lit lit -> doc_lit_ocaml false lit
     | E_cast(typ,e) ->
@@ -509,7 +512,7 @@ let doc_exp_ocaml, doc_let_ocaml =
          (match alias_info with
           | Alias_field(reg,field) ->
             parens ((if is_bit then string "set_register_field_bit" else string "set_register_field_v") ^^ space ^^
-                    string (String.uncapitalize reg) ^^ space ^^string_lit (string field) ^^ space ^^ exp e_new_v)
+                    string (sanitize_name reg) ^^ space ^^string_lit (string field) ^^ space ^^ exp e_new_v)
           | Alias_extract(reg,start,stop) ->
             if start = stop
             then