blob: 4044e23cbe60c605f867448882a672e30226d55c (
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
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
open import Pervasives_extra
type bit = O | I | Undef
type vector 'a = V of list 'a * integer * bool
let rec nth xs (n : integer) =
match xs with
| x :: xs -> if n = 0 then x else nth xs (n - 1)
| _ -> failwith "nth applied to empty list"
end
let to_bool = function
| O -> false
| I -> true
| Undef -> failwith "to_bool applied to Undef"
end
let get_start (V _ s _) = s
let length (V bs _ _) = length bs
let rec replace bs ((n : integer),b') = match bs with
| [] -> []
| b :: bs ->
if n = 0 then
b' :: bs
else
b :: replace bs (n - 1,b')
end
let vector_concat (V bs start is_inc) (V bs' _ _) =
V (bs ++ bs') start is_inc
let (^^) = vector_concat
val slice : vector bit -> integer -> integer -> vector bit
let slice (V bs start is_inc) n m =
let n = natFromInteger n in
let m = natFromInteger m in
let start = natFromInteger start in
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
let n = integerFromNat n in
V subvector n is_inc
let update (V bs start is_inc) n m (V bs' _ _) =
let n = natFromInteger n in
let m = natFromInteger m in
let start = natFromInteger start in
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
let start = integerFromNat start in
V (prefix ++ (List.take length bs') ++ suffix) start is_inc
val access : forall 'a. vector 'a -> (*nat*) integer -> 'a
let access (V bs start is_inc) n =
if is_inc then nth bs (n - start) else nth bs (start - n)
val update_pos : forall 'a. vector 'a -> (*nat*) integer -> 'a -> vector 'a
let update_pos v n b =
update v n n (V [b] 0 true)
|
