Remove work-around from interpreter, move it to power.sail

Two bugs are worked-around here:
- missing cast to nat when a vector is wrapped in exts
  (exts is a no-op currently anyway, so we are discarding it)
- missing cast (due to limited type-inference) in one if branch:
  type given explicitly.

2 files changed, 0 insertions, 31 deletions

diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index b5e94a42..9b3ba3b0 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -44,33 +44,7 @@ let to_vec_dec len (V_lit(L_aux (L_num n) ln)) =
   V_vector 0 false (map bool_to_bit l) ;;
 
 let rec add (V_tuple args) = match args with
-  (* vector case *)
-  | [(V_vector _ d l as v); (V_vector _ d' l' as v')] ->
-      let (V_lit (L_aux (L_num x) lx)) = (if d then to_num_inc else to_num_dec) v in
-      let (V_lit (L_aux (L_num y) ly)) = (if d' then to_num_inc else to_num_dec) v' in
-      (* XXX how shall I decide this? max? max+1? *)
-      let len = max (List.length l) (List.length l') in
-      (* XXX assume d = d' *)
-      V_lit (L_aux (L_num (x+y)) lx)
-  (* integer case *)
   | [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> V_lit(L_aux (L_num (x+y)) lx)
-  | [(V_lit(L_aux (L_num _) _) as n); (V_vector _ d l as v)] ->
-      let len = List.length l in
-      add (V_tuple [(if d then to_vec_inc else to_vec_dec) len n; v])
-  | [(V_vector _ d l as v); (V_lit(L_aux (L_num _) _) as n)] ->
-      let len = List.length l in
-      add (V_tuple [v; (if d then to_vec_inc else to_vec_dec) len n])
-  (* assume other literals are L_bin or L_hex, ie. vectors *)
-  | [(V_lit (L_aux L_zero _) as l); x] ->
-      add (V_tuple [V_vector 0 true [l]; x])
-  | [(V_lit (L_aux L_one _) as l); x] ->
-      add (V_tuple [V_vector 0 true [l]; x])
-  | [x; (V_lit (L_aux L_zero _) as l)] ->
-      add (V_tuple [x; V_vector 0 true [l]])
-  | [x; (V_lit (L_aux L_one _) as l)] ->
-      add (V_tuple [x; V_vector 0 true [l]])
-  | [V_lit l; x ] -> add (V_tuple [litV_to_vec l; x])
-  | [ x ; V_lit l ] -> add (V_tuple [x; litV_to_vec l])
   end ;;
 
 let rec vec_concat (V_tuple args) = match args with
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 8e495df4..8ae6d1ee 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -196,11 +196,6 @@ let rec perform_action ((reg, mem) as env) = function
      perform_action env (Write_reg (r, slice, V_vector(zero_big_int, true, [value])))
  | Write_mem (id, (V_lit(L_aux(L_num _,_)) as n), (Some (start, stop) as slice), value) when eq_big_int start stop ->
      perform_action env (Write_mem (id, n, slice, V_vector(zero_big_int, true, [value])))
- (* XXX work-around missing cast *)
- | Write_mem (id, V_tuple (((V_vector (m, true, vs)) as v) :: l), sub, value) ->
-    perform_action env (Write_mem (id, V_tuple ((to_num_inc v) :: l), sub, value))
- | Read_mem (id, V_tuple (((V_vector (m, true, vs)) as v) :: l), sub) ->
-    perform_action env (Read_mem (id, V_tuple ((to_num_inc v) :: l), sub))
  (* extern functions *)
  | Call_extern (name, arg) -> eval_external name arg, env
  | _ -> assert false