git.iko.soy/Idris-dev
on 496cf41 help sign in
Idris-dev/iif/testvm.iif
32 lines 872 B history raw
1data O 0
2data S 1
4fun plus(x, y) = case x of {
5 O => y
6 | S(k) => S (plus(k, y))
7 }
9fun fact(x) = factAux(x, 1)
11fun factAux(x, acc) = case (x == 1) of {
12 0 => factAux(x-1, acc * x)
13 | 1 => acc
14 }
16fun natToInt(x) = case x of {
17 O => 0
18 | S(k) => let y = natToInt(k) in y + 1
19 }
21fun intToNat(x) = case x of {
22 0 => O
23 | _ => S (intToNat (x - 1))
24 }
26fun sin(x) = foreign C Float "sin" (Float x)
28fun main() = let val = natToInt(plus(intToNat(fact(6)), S(S(O)))) in
29 let sval = sin(1.0) in
30 %WriteString("Answer: " ++ %IntString(val)
31 ++ " " ++ %FloatString(sval))