(*
 * linear_search.whyml
 * WhyML implementation of byteback test `algorithm/LinearSearch`
 *)

module LinearSearch
    use int.Int
    use ref.Ref
    use array.Array

    type t

    val predicate eq (a b : t)
    
    (* nullability preamble *)
    exception NullPointerException
    
    type nullable 't = Null | Some 't

    let predicate is_null (obj: nullable 't) =
        match obj with 
            | Null -> true
            | Some _ -> false
        end

    let dereference (obj: nullable 't) : 't
        raises { NullPointerException -> is_null obj } =
        match obj with
            | Null -> raise NullPointerException
            | Some obj_val -> obj_val
        end
    (* end nullability preamble *)

    type narrt = nullable (array t)
    
    let predicate array_is_not_null (a: narrt) (n: t) (left right: int) = is_null a

    let predicate array_is_null (a: narrt) (n: t) (left right: int) = not (is_null a)

    let predicate bounded_indices (a: narrt) (n: t) (left right: int) =
        match a with
            | Null -> false
            | Some aa -> 0 <= left && left <= right && right <= length aa
        end

    let predicate result_is_index (a: narrt) (n: t) (left right return_val: int) = 
        match a with
            | Null -> false
            | Some aa -> ((not (0 <= return_val)) || (eq aa[return_val] n))
        end

    let search (a: narrt) (n: t) (left right: int) : int
        requires { array_is_not_null a n left right }
        requires { bounded_indices a n left right }
        ensures { result_is_index a n left right result }
        raises { NullPointerException -> false }
    =
        let ref i = left in 
        while i < right do
            invariant { left <= i && i <= right }

            let a_val = dereference a in
            if eq a_val[i] n then
                return i;

            i <- i + 1;
        done;

        -1
end