4 files changed, 18 insertions, 15 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 1a97f5db..7cdc5149 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -168,13 +168,6 @@ let reg_size reg =
       end 
 end 
 
-let vector_length v = match v with
-  | V_vector n inc vals -> List.length vals
-  | V_vector_sparse n m inc vals def -> m
-  | V_lit _ -> 1
-  | _ -> 0
-end
-
 (*Constant unit value, for use in interpreter *)
 let unitv = V_lit (L_aux L_unit Unknown)
 
@@ -458,6 +451,13 @@ let rec binary_taint thunk vall valr =
    | (vl,vr) -> thunk vl vr
 end 
 
+let vector_length v = match (detaint v) with
+  | V_vector n inc vals -> List.length vals
+  | V_vector_sparse n m inc vals def -> m
+  | V_lit _ -> 1
+  | _ -> 0
+end
+
 val access_vector : value -> nat -> value
 let access_vector v n =
   retaint v (match (detaint v) with
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index bcacaabc..06aabd46 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -683,6 +683,8 @@ let library_functions direction = [
   ("gt_vec_unsigned", compare_op_vec (>) Unsigned);
   ("lteq_vec_unsigned", compare_op_vec (<=) Unsigned);
   ("gteq_vec_unsigned", compare_op_vec (>=) Unsigned);
+  ("signed", to_num Signed);
+  ("unsigned", to_num Unsigned);
   ("ltu", compare_op_vec_unsigned (<));
   ("gtu", compare_op_vec_unsigned (>));
   ("duplicate", duplicate direction);
diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml
index 76f216ee..76e696f9 100644
--- a/src/lem_interp/pretty_interp.ml
+++ b/src/lem_interp/pretty_interp.ml
@@ -364,13 +364,13 @@ let doc_exp, doc_let =
     let default_print _ = brackets (separate_map comma (exp env add_red) exps) in
     (match exps with
       | [] -> default_print ()
-      | E_aux(e,_)::es ->
-	(match e with
-	  | E_lit (L_aux(L_one, _)) | E_lit (L_aux(L_zero, _)) ->
-	    utf8string
-	      ("0b" ^ 
-	       (List.fold_right (fun (E_aux(E_lit(L_aux(l, _)),_)) rst -> match l with | L_one -> "1"^rst | L_zero -> "0"^rst) exps "")) 
-	  | _ -> default_print ()))
+      | es ->
+	if (List.for_all (fun e -> match e with (E_aux(E_lit(L_aux((L_one | L_zero),_)),_)) -> true | _ -> false) es)
+	then
+	  utf8string
+	    ("0b" ^ 
+		(List.fold_right (fun (E_aux(E_lit(L_aux(l, _)),_)) rst -> match l with | L_one -> "1"^rst | L_zero -> "0"^rst | L_undef -> "u"^rst) exps "")) 
+	else default_print ())
   | E_vector_indexed (iexps, (Def_val_aux(default,_))) ->
     let default_string = 
       (match default with
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index 60e5359b..57326d46 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -54,7 +54,8 @@ let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (fu
   | Interp.V_lit(L_aux(L_one, _)) -> "1"
   | Interp.V_lit(L_aux(L_undef, _)) -> "u"
   | Interp.V_unknown -> "?"
-  | v -> (Printf.printf "bitvec found a non bit %s%!\n" (Interp.string_of_value v));assert false) l))
+  | v -> (Printf.printf "bitvec found a non bit %s%!\n" (Interp.string_of_value v));assert false) 
+								      (List.map Interp.detaint l)))
 ;;
 
 (* pp the bytes of a Bytevector as a hex value *)