(* The example from the 'Dependent types' subsection of \cite[p. 66]{KennedyThesis}.

Inconsequentially modified because Stardust doesn't do numeric patterns.  Also, the
dependent universal quantifier in Kennedy's proposed type corresponds to an -all- plus an
arrow. *)
;

(*[ val power : -all d : dim- -all n : int- int(n) -> real(d) -> real(d^n) ]*)
fun power n x =
    if n = 0 then
        1.0
    else if n < 0 then
        1.0 / power (~n) x
    else
        x * power (n-1) x

(* Some buggy versions follow (and shadow the correct version!) *)

(*[ val power :! -all d : dim- -all n : int- int(n) -> real(d) -> real(d^n) ]*)
fun power n x =
    if n = 0 then
        1.0
    else if n < 0 then
        1.0 / power (~n) x
    else
        x * x * power (n-1) x  (* BUG *)

(*[ val power :! -all d : dim- -all n : int- int(n) -> real(d) -> real(d^n) ]*)
fun power n x =
    if n = 0 then
        1.0
    else if n < 0 then
        1.0 / power (n-1) x   (* BUG *)
    else
        x * power (n-1) x

(*[ val power :! -all d : dim- -all n : int- int(n) -> real(d) -> real(d^n) ]*)
fun power n x =
    if n = 0 then
        1.0
    else if n < 0 then
        1.0 / power (~n) x
    else
        power (n-1) x  (* BUG *)

(*[ val power : -all d : dim- -all n : int- int(n) -> real(d) -> real(d^n) ]*)
fun power n x =
    if n = 0 then
        1.0
    else if n < 0 then
        0.0 / power (~n + 3) x      (* Two bugs, but well typed since zero has any dimension *)
    else
        x * power (n-1) x