diff options
Diffstat (limited to 'src/gen_lib/vector.lem')
| -rw-r--r-- | src/gen_lib/vector.lem | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/gen_lib/vector.lem b/src/gen_lib/vector.lem index e7b20aeb..fe70c9c0 100644 --- a/src/gen_lib/vector.lem +++ b/src/gen_lib/vector.lem @@ -1,8 +1,14 @@ open import Pervasives -type bit = Zero | One | Undef +type bit = B0 | B1 | BU type vector = Vector of list bit * nat + +let vector_access (Vector bs start) n = + let (Just b) = if is_inc then List.index bs (n - start) + else List.index bs (start - n) in + b + let read_vector_subrange is_inc (Vector bs start) n m = let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in let (_,suffix) = List.splitAt offset bs in @@ -14,3 +20,5 @@ let write_vector_subrange is_inc (Vector bs start) n m (Vector bs' _) = let (prefix,_) = List.splitAt offset bs in let (_,suffix) = List.splitAt (offset + length) bs in Vector (prefix ++ (List.take length bs') ++ suffix) start + +let hd (x :: xs) = x |