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)