small bug fixes

3 files changed, 24 insertions, 22 deletions

diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 06aabd46..c7f42e02 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -86,10 +86,19 @@ let is_unknown v = match v with
   | _ -> false
 end 
 
+let is_undef v = match v with
+  | V_lit (L_aux L_undef _) -> true
+  | _ -> false
+end
+
 let has_unknown v = match detaint v with
   | V_vector _ _ vs -> List.any is_unknown vs
 end
 
+let has_undef v = match detaint v with
+  | V_vector _ _ vs -> List.any is_undef vs
+end 
+
 let rec sparse_walker update ni processed_length length ls df =
   if processed_length = length 
   then []
@@ -189,13 +198,15 @@ let to_num signed v =
     (match detaint v with
       | (V_vector idx inc l) ->
 	if has_unknown v then V_unknown else if l=[] then V_unknown
-	else 
+	  else if has_undef v then V_lit (L_aux L_undef Unknown)
+	  else 
 	  (* Word library in Lem expects bitseq with LSB first *)
-	  let l = reverse l in
+	    let l = reverse l in
 	  (* Make sure the last bit is a zero to force unsigned numbers *)
-	  let l = (match signed with | Signed -> l | Unsigned -> l ++ [V_lit (L_aux L_zero Unknown)] end) in
-	  V_lit(L_aux (L_num(integerFromBitSeq (Maybe_extra.fromJust (bitSeqFromBoolList (map bit_to_bool l))))) Unknown)
+	    let l = (match signed with | Signed -> l | Unsigned -> l ++ [V_lit (L_aux L_zero Unknown)] end) in
+	    V_lit(L_aux (L_num(integerFromBitSeq (Maybe_extra.fromJust (bitSeqFromBoolList (map bit_to_bool l))))) Unknown)
       | V_unknown -> V_unknown
+      | V_lit (L_aux L_undef _) -> v
      end)
 
 let to_vec_inc (V_tuple[v1;v2]) = 
@@ -283,6 +294,8 @@ let arith_op op (V_tuple [vl;vr]) =
       | (V_lit(L_aux (L_num x) lx), V_lit(L_aux (L_num y) ly)) -> V_lit(L_aux (L_num (op x y)) lx)
       | (V_unknown,_) -> V_unknown
       | (_,V_unknown) -> V_unknown
+      | (V_lit (L_aux L_undef lx),_) -> vl
+      | (_, (V_lit (L_aux L_undef ly))) -> vr
   end in 
   binary_taint arith_op_help vl vr
 let rec arith_op_vec op sign size (V_tuple [vl;vr]) =
@@ -651,8 +664,7 @@ let library_functions direction = [
   ("neq", neq);
   ("vec_concat", vec_concat);
   ("is_one", is_one);
-  ("to_num_inc", to_num Unsigned);
-  ("to_num_dec", to_num Unsigned);
+  ("to_num", to_num Unsigned);
   ("EXTS", exts direction);
   ("EXTZ", extz direction);
   ("to_vec_inc", to_vec_inc);
diff --git a/src/type_check.ml b/src/type_check.ml
index 134a2c6c..5b5a0864 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -200,8 +200,8 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
 	  | L_unit  -> unit_t,lit 
 	  | L_zero  -> bit_t,lit
 	  | L_one   -> bit_t,lit
-	  | L_true  -> bool_t,lit
-	  | L_false -> bool_t,lit
+	  | L_true  -> bit_t,L_one
+	  | L_false -> bit_t,L_zero
 	  | L_num i -> 
 	    (match expect_actual.t with
 	      | Tid "bit" -> 
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 9b3eab6d..f46b5409 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -2307,14 +2307,10 @@ let rec type_coerce_internal co d_env enforce is_explicit widen t1 cs1 e t2 cs2
       | _ -> raise (Reporting_basic.err_unreachable l "vector is not properly kinded"))
     | "vector","range",_ -> 
       (match args1,args2 with
-      | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}],
+      | [TA_nexp b1;TA_nexp r1;TA_ord _;TA_typ {t=Tid "bit"}],
         [TA_nexp b2;TA_nexp r2;] -> 
 	let cs = [Eq(co,b2,n_zero);LtEq(co,Guarantee,mk_sub {nexp=N2n(r1,None)} n_one,r2)] in
-	(t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_num_inc",l)),[e]),(l,Base(([],t2),External None,cs,pure_e,nob))))
-      | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}],
-        [TA_nexp b2;TA_nexp r2;] -> 
-	let cs = [Eq(co,b2,n_zero);LtEq(co,Guarantee,mk_sub {nexp=N2n(r1,None)} n_one,r2)] in
-	(t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_num_dec",l)),[e]),(l,Base(([],t2),External None,cs,pure_e,nob))))
+	(t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_num",l)),[e]),(l,Base(([],t2),External None,cs,pure_e,nob))))
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ -> 
 	eq_error l "Cannot convert a vector to an range without an order"
       | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> 
@@ -2322,16 +2318,10 @@ let rec type_coerce_internal co d_env enforce is_explicit widen t1 cs1 e t2 cs2
       | _,_ -> raise (Reporting_basic.err_unreachable l "vector or range is not properly kinded"))
     | "vector","atom",_ -> 
       (match args1,args2 with
-      | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}],
+      | [TA_nexp b1;TA_nexp r1;TA_ord _;TA_typ {t=Tid "bit"}],
         [TA_nexp b2] -> 
 	let cs = [GtEq(co,Guarantee,b2,n_zero);LtEq(co,Guarantee,b2,mk_sub {nexp=N2n(r1,None)} n_one)] in
-	(t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_num_inc",l)),[e]),(l,Base(([],t2),External None,cs,pure_e,nob))))
-      | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}],
-        [TA_nexp b2] -> 
-	let cs = [Eq(co,b2,mk_sub {nexp=N2n(r1,None)} n_one)] in
-	(t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_num_dec",l)),[e]),(l,Base(([],t2),External None,cs,pure_e,nob))))
-      | [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ -> 
-	eq_error l "Cannot convert a vector to an range without an order"
+	(t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_num",l)),[e]),(l,Base(([],t2),External None,cs,pure_e,nob))))
       | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> 
         eq_error l "Cannot convert non-bit vector into an range"
       | _,_ -> raise (Reporting_basic.err_unreachable l "vector or range is not properly kinded"))