Merge branch 'master' of bitbucket.org:Peter_Sewell/l2

1 files changed, 7 insertions, 7 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 1a97f5db..7cdc5149 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -168,13 +168,6 @@ let reg_size reg =
       end 
 end 
 
-let vector_length v = match v with
-  | V_vector n inc vals -> List.length vals
-  | V_vector_sparse n m inc vals def -> m
-  | V_lit _ -> 1
-  | _ -> 0
-end
-
 (*Constant unit value, for use in interpreter *)
 let unitv = V_lit (L_aux L_unit Unknown)
 
@@ -458,6 +451,13 @@ let rec binary_taint thunk vall valr =
    | (vl,vr) -> thunk vl vr
 end 
 
+let vector_length v = match (detaint v) with
+  | V_vector n inc vals -> List.length vals
+  | V_vector_sparse n m inc vals def -> m
+  | V_lit _ -> 1
+  | _ -> 0
+end
+
 val access_vector : value -> nat -> value
 let access_vector v n =
   retaint v (match (detaint v) with