staload _ = "prelude/DATS/array.dats"

fun getitem{n,m:nat}(arr : array(int, n) , length : int(n), index : int m) : int =
    (*  This is an ML-style comment, which is similar to C-style comments
        except that they can be nested arbitrarily (* like this *)
       
        The first thing we do is declare compile-time variables that the
        dependent types refer to, the natural numbers n and m.
        These refer to the size of the list, and the index, respectively.
        {n,m:nat} is the same as {n,m:int | n >= 0 && m >= 0}
        Arguably we should be saying this as
        {n,m:nat | n > m >= 0}, but perhaps that's getting ahead of ourselves.
        Besides, the array type already does that.
       
        a value is of type array(X, Y) if its contents are of type X, and it is 
        of length Y
       
        array(int, nat(n)) says:
            the array has some non-negative length, and only contains integers

        length: nat(n) says:
            length is a natural number value n, which is the same as the length
            of the array
    
        Because the types have been declared this way, the code will fail to
        typecheck (at compile time) if these relations are not true. The
        compiler's job is to verify, everywhere this function is called,
        that the value passed for the length parameter is the same as the
        allocated size of the list.
        
        If the compiler can't prove this, then the program fails to typecheck.
    

        in short, we know at _compile time_ a value "n" which is the length of
        the array and we know, at _run time_, a value "length", which is also
        the length of the array. The compiler guarantees to us that length == n, and moreover it is aware of this fact itself, so that if we check things against length, it knows that it can do the same checks against n.

        This means that we can inspect the value "index" to make sure it will
        not go out of bounds, and when we do that, we also satisfy the compiler
        that we have done so.
    *)
    
    (* The compiler would complain if there was ever a value for which this
       was not true, and we forgot to check it *)
    if index < length then
        arr[index]
    else
        ~1 (* -1, error *)


(* erm ...*)
implement main () = let (* def main(): *)
    val A = array $arrsz{int}(2, 1, ~20, 900, 123, 2, 12) (* A = [2, 1, -20, 900, 123, 2, 12] *)
in (
    printf("%d\n", @(getitem(A, 7, 0))) (* print "%d\n" % (getitem(A, 7, 0),) *)
)
end