make interpreter work better with unknowns, make interp_inter_imp do better on coercions

2 files changed, 16 insertions, 3 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 17a9644d..cf8c325c 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -844,6 +844,7 @@ let rec match_pattern (P_aux p _) value_whole =
     else
     match value with
     | V_lit(litv) -> (lit = litv, false,eenv)
+    | V_vector _ _ [V_lit(litv)] -> (lit = litv,false,eenv)
     | V_unknown -> (true,true,eenv)
     | _ -> (false,false,eenv)
     end
@@ -2236,7 +2237,11 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 		  ((Value (V_lit (L_aux L_unit Unknown)), update_vector_slice v value n1 n2 lm, l_env), Nothing)
                 | (V_vector m inc vs,false) ->
                   ((Value (slice_vector v n1 n2),lm,l_env), Just (next_builder lexp_builder))
-		| (V_unknown,_) -> ((Value v,lm,l_env),Nothing)
+		| (V_unknown,_) -> 
+		  let inc =  n1 < n2 in
+		  let start = if inc then n1 else (n2-1) in
+		  let size = natFromInteger ((abs (n1-n2)) + 1) in      
+		  ((Value (V_vector start inc (List.replicate size V_unknown)),lm,l_env),Nothing)
                 | _ -> ((Error l "Vector required",lm,le),Nothing) end)
               | ((Action (Write_reg regf Nothing value) s, lm,le), Just lexp_builder) ->
                 ((Action 
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index fdb55f5b..3aef9d3b 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -47,16 +47,24 @@ end
 let bits_to_ibits l = List.map bit_to_ibit l
 let bitls_to_ibits l = List.map bitl_to_ibit l
 let bitls_from_ibits l = List.map 
-  (fun b -> match b with
+  (fun b -> 
+    let b = (match b with | Interp.V_track v _ -> v | _ -> b end) in
+    match b with
     | Interp.V_lit (L_aux L_zero _) -> Bitl_zero
+    | Interp.V_vector _ _ [Interp.V_lit (L_aux L_zero _)] -> Bitl_zero
     | Interp.V_lit (L_aux L_one _)  -> Bitl_one
+    | Interp.V_vector _ _ [Interp.V_lit (L_aux L_one _)] -> Bitl_one
     | Interp.V_lit (L_aux L_undef _) -> Bitl_undef
     | Interp.V_unknown -> Bitl_unknown end) l
 
 let bits_from_ibits l = List.map 
-  (fun b -> match b with
+  (fun b -> 
+    let b = (match b with | Interp.V_track v _ -> v | _ -> b end) in
+    match b with
     | Interp.V_lit (L_aux L_zero _) -> Bitc_zero
+    | Interp.V_vector _ _ [Interp.V_lit (L_aux L_zero _)] -> Bitc_zero
     | Interp.V_lit (L_aux L_one _)  -> Bitc_one
+    | Interp.V_vector _ _ [Interp.V_lit (L_aux L_one _)] -> Bitc_one
    end) l
 
 let rec to_bytes l = match l with