summaryrefslogtreecommitdiff
path: root/src/gen_lib/vector.lem
diff options
context:
space:
mode:
authorChristopher Pulte2015-11-10 22:59:56 +0000
committerChristopher Pulte2015-11-10 22:59:56 +0000
commit3945afb351cda3ed4eacb494ff426d108fd38612 (patch)
tree085834c127bd733013c341af587c89cab43a5df4 /src/gen_lib/vector.lem
parentafb10f429248912984a7915bf05c58de85ea5cbb (diff)
rewriting fixes, syntactically correct lem syntax, number type errors remaining
Diffstat (limited to 'src/gen_lib/vector.lem')
-rw-r--r--src/gen_lib/vector.lem20
1 files changed, 0 insertions, 20 deletions
diff --git a/src/gen_lib/vector.lem b/src/gen_lib/vector.lem
index d5f47492..5f239e37 100644
--- a/src/gen_lib/vector.lem
+++ b/src/gen_lib/vector.lem
@@ -7,23 +7,3 @@ let rec nth xs (n : nat) = match (n,xs) with
| (0,x :: xs) -> x
| (n + 1,x :: xs) -> nth xs n
end
-
-let vector_access is_inc (Vector bs start) n =
- if is_inc then nth bs (n - start) else nth bs (start - n)
-
-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 write_vector_bit is_inc v n (Vector [b] 0) =
- write_vector_subrange is_inc v n n b
-
-let hd (x :: xs) = x