no more unecessary variables from removing vector-concatenation pattern matches, reset variable name counter for each function clause, fixes

2 files changed, 13 insertions, 11 deletions

diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 4d74976b..33b8444e 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -3,16 +3,18 @@ open import State
 open import Vector
 open import Arch
 
+type i = integer
+
 let length l = integerFromNat (length l)
 
-let has_undef (V bs _ _) = List.any (function U -> true | _ -> false end) bs
+let has_undef (V bs _ _) = List.any (function Undef -> true | _ -> false end) bs
 
 let most_significant (V bs _ _) = let (b :: _) = bs in b
 
 let bitwise_not_bit = function
   | I -> O
   | O -> I
-  | _ -> U
+  | _ -> Undef
   end
 
 let (~) = bitwise_not_bit
@@ -23,8 +25,8 @@ let bitwise_not (V bs start is_inc) =
 let bool_to_bit b = if b then I else O
 
 let bitwise_binop_bit op = function
-  | (U,_) -> U (*Do we want to do this or to respect | of I and & of B0 rules?*)
-  | (_,U) -> U (*Do we want to do this or to respect | of I and & of B0 rules?*)
+  | (Undef,_) -> Undef (*Do we want to do this or to respect | of I and & of B0 rules?*)
+  | (_,Undef) -> Undef (*Do we want to do this or to respect | of I and & of B0 rules?*)
   | (x,y) -> bool_to_bit (op (to_bool x) (to_bool y))
   end
 
@@ -131,7 +133,7 @@ let to_vec_inc = to_vec true
 let to_vec_dec = to_vec false
 
 let to_vec_undef is_inc (len : integer) =
-  V (replicate (natFromInteger len) U) (if is_inc then 0 else len-1) is_inc
+  V (replicate (natFromInteger len) Undef) (if is_inc then 0 else len-1) is_inc
 
 let to_vec_inc_undef = to_vec_undef true
 let to_vec_dec_undef = to_vec_undef false
@@ -289,7 +291,7 @@ let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size (((V _ s
     end in
   if representable 
   then to_vec is_inc (act_size,n')
-  else V (List.replicate (natFromInteger act_size) U) start is_inc
+  else V (List.replicate (natFromInteger act_size) Undef) start is_inc
 
 let mod_vec = arith_op_vec_no0 integerMod false 1
 let quot_vec = arith_op_vec_no0 integerDiv false 1
@@ -313,8 +315,8 @@ let arith_op_overflow_no0_vec op sign size (((V _ start is_inc) as l),r) =
     if representable then
       (to_vec is_inc (act_size,n'),to_vec is_inc (act_size + 1,n_u'))
     else
-      (V (List.replicate (natFromInteger act_size) U) start is_inc,
-       V (List.replicate (natFromInteger (act_size + 1)) U) start is_inc) in
+      (V (List.replicate (natFromInteger act_size) Undef) start is_inc,
+       V (List.replicate (natFromInteger (act_size + 1)) Undef) start is_inc) in
   let overflow = if representable then O else I in
   (correct_size_num,overflow,most_significant one_more)
 
diff --git a/src/gen_lib/vector.lem b/src/gen_lib/vector.lem
index 5e78e010..9efae768 100644
--- a/src/gen_lib/vector.lem
+++ b/src/gen_lib/vector.lem
@@ -1,6 +1,6 @@
 open import Pervasives
 
-type bit = O | I | U
+type bit = O | I | Undef
 type vector 'a = V of list 'a * integer * bool
 
 let rec nth xs (n : integer) = match (n,xs) with
@@ -28,11 +28,11 @@ let make_indexed_vector_reg entries default start length =
   V (List.foldl replace (replicate length v) entries) start
 
 let make_indexed_vector_bit entries default start length =
-  let default = match default with Nothing -> U | Just v -> v end in
+  let default = match default with Nothing -> Undef | Just v -> v end in
   V (List.foldl replace (replicate length default) entries) start
 
 let make_bitvector_undef length =
-  V (replicate length U) 0 true
+  V (replicate length Undef) 0 true
 
 let vector_concat (V bs start is_inc) (V bs' _ _) =
   V (bs ++ bs') start is_inc