diff options
| author | Christopher Pulte | 2015-11-10 22:59:56 +0000 |
|---|---|---|
| committer | Christopher Pulte | 2015-11-10 22:59:56 +0000 |
| commit | 3945afb351cda3ed4eacb494ff426d108fd38612 (patch) | |
| tree | 085834c127bd733013c341af587c89cab43a5df4 /src/gen_lib/vector.lem | |
| parent | afb10f429248912984a7915bf05c58de85ea5cbb (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.lem | 20 |
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 |
