summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/lem_interp/interp_lib.lem2
-rw-r--r--src/lem_interp/run_interp.ml5
2 files changed, 6 insertions, 1 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 8a0083a7..b5e94a42 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -51,7 +51,7 @@ let rec add (V_tuple args) = match args with
(* XXX how shall I decide this? max? max+1? *)
let len = max (List.length l) (List.length l') in
(* XXX assume d = d' *)
- (if d then to_vec_inc else to_vec_dec) len (V_lit (L_aux (L_num (x+y)) lx))
+ 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)] ->
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 8ae6d1ee..8e495df4 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -196,6 +196,11 @@ 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