diff options
Diffstat (limited to 'src/lem_interp/interp.lem')
| -rw-r--r-- | src/lem_interp/interp.lem | 14 |
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 |
