summaryrefslogtreecommitdiff
path: root/src/lem_interp/interp.lem
diff options
context:
space:
mode:
Diffstat (limited to 'src/lem_interp/interp.lem')
-rw-r--r--src/lem_interp/interp.lem11
1 files changed, 4 insertions, 7 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 0abc6220..92fa4ec0 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -583,7 +583,6 @@ let access_vector v n =
| V_lit (L_aux L_zero _) -> v
| V_lit (L_aux L_one _ ) -> v
| V_vector m dir vs ->
- (*let _ = debug_print ("access_vector given " ^ string_of_value v ^ " where dir was " ^ (if is_inc(dir) then "increasing" else "decreaseing") ^ " and start is " ^ show m ^ " and index is " ^ show n ^ "\n") in*)
list_nth vs (if is_inc(dir) then (n - m) else (m - n))
| V_vector_sparse _ _ _ vs d ->
match (List.lookup n vs) with
@@ -702,7 +701,7 @@ val fupdate_vector_slice : value -> value -> nat -> nat -> value
let fupdate_vector_slice vec replace start stop =
let fupdate_vec_help vec replace =
(match (vec,replace) with
- | (V_vector m dir vals,V_vector _ dir' reps) ->
+ | (V_vector m dir vals,V_vector r_m dir' reps) ->
V_vector m dir
(replace_is vals
(if dir=dir' then reps else (List.reverse reps))
@@ -761,7 +760,7 @@ let update_vector_slice track vector value start stop mem =
^ " and " ^ string_of_value value)
end
-let update_vector_start default_dir new_start expected_size v =
+let update_vector_start default_dir new_start expected_size v =
retaint v
(match detaint v with
| V_lit (L_aux L_zero _) -> V_vector new_start default_dir [v]
@@ -1908,13 +1907,11 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
(interp_main mode t_level l_env lm e2)
(fun v2 lm le ->
let append v1 v2 = (match (v1,v2) with
- | (V_vector m dir vals1, V_vector _ _ vals2) ->
+ | (V_vector _ dir vals1, V_vector _ _ vals2) ->
let vals = vals1++vals2 in
let len = List.length vals in
if is_inc(dir)
- then V_vector m dir vals
- else if m > len
- then V_vector m dir vals
+ then V_vector 0 dir vals
else V_vector (len-1) dir vals
| (V_vector m dir vals1, V_vector_sparse _ len _ vals2 d) ->
let original_len = List.length vals1 in