blob: fe70c9c0d677819c82a245d15563ff1f9902c6e4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
open import Pervasives
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
let (subvector,_) = List.splitAt length suffix in
Vector subvector n
let write_vector_subrange is_inc (Vector bs start) n m (Vector bs' _) =
let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
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
|
