1 files changed, 0 insertions, 59 deletions
diff --git a/src/gen_lib/vector.lem b/src/gen_lib/vector.lem
deleted file mode 100644
index 07238180..00000000
--- a/src/gen_lib/vector.lem
+++ /dev/null
@@ -1,59 +0,0 @@
-open import Pervasives_extra
-
-(* element list * start * has increasing direction *)
-type vector 'a = Vector 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 get_dir (Vector _ _ ord) = ord
-let get_start (Vector _ s _) = s
-let length (Vector bs _ _) = integerFromNat (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 (Vector bs start is_inc) (Vector bs' _ _) =
-  Vector (bs ++ bs') start is_inc
-
-let (^^) = vector_concat
-
-val slice : forall 'a. vector 'a -> integer -> integer -> vector 'a
-let slice (Vector 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
-  Vector subvector n is_inc
-
-val update : forall 'a. vector 'a -> integer -> integer -> vector 'a -> vector 'a
-let update (Vector bs start is_inc) n m (Vector 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
-  Vector (prefix ++ (List.take length bs') ++ suffix) start is_inc
-
-val access : forall 'a. vector 'a -> integer -> 'a
-let access (Vector 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 -> integer -> 'a -> vector 'a
-let update_pos v n b =
-  update v n n (Vector [b] 0 true)