Idris-dev/iif/testvm.iif

data O 0
data S 1

fun plus(x, y) = case x of {
                     O => y
                   | S(k) => S (plus(k, y))
                 }

fun fact(x) = factAux(x, 1)

fun factAux(x, acc) = case (x == 1) of {
                           0 => factAux(x-1, acc * x)
                         | 1 => acc
                       }

fun natToInt(x) = case x of {
                     O => 0
                   | S(k) => let y = natToInt(k) in y + 1
                  }

fun intToNat(x) = case x of {
                     0 => O
                   | _ => S (intToNat (x - 1))
                  }

fun sin(x) = foreign C Float "sin" (Float x)

fun main() = let val = natToInt(plus(intToNat(fact(6)), S(S(O)))) in
             let sval = sin(1.0) in
                 %WriteString("Answer: " ++ %IntString(val)
                                         ++ " " ++ %FloatString(sval))