util¶
In [ ]:
//// test
open testing
ski¶
In [ ]:
union rec ski =
| I
| K
| S
| App : ski * ski
inl rec eval ski =
match ski with
| App (App (K, x), y) => x |> eval
| App (App (App (S, x), y), z) => App (App (x, z), App (y, z)) |> eval
| App (I, x) => x |> eval
| App (K, x) => App (K, eval x)
| App (f, x) => App (eval f, x) |> eval
| _ => ski
In [ ]:
//// test
eval I
|> _assert_eq I
App (I, I)
|> eval
|> _assert_eq I
App (I, App (I, I))
|> eval
|> _assert_eq I
App (App (I, I), I)
|> eval
|> _assert_eq I
App (App (App (I, I), I), I)
|> eval
|> _assert_eq I
eval K
|> _assert_eq K
App (K, I)
|> eval
|> _assert_eq (App (K, I))
App (K, K)
|> eval
|> _assert_eq (App (K, K))
App (App (K, I), K)
|> eval
|> _assert_eq I
App (App (K, K), I)
|> eval
|> _assert_eq K
App (App (App (App (K, K), I), S), K)
|> eval
|> _assert_eq S
eval S
|> _assert_eq S
App (App (App (S, I), I), I)
|> eval
|> _assert_eq I
App (App (App (S, K), K), I)
|> eval
|> _assert_eq I
App (App (App (S, K), I), (App (App (K, I), S)))
|> eval
|> _assert_eq I
App (App (K, S), App (I, App (App (App (S, K), S), I)))
|> eval
|> _assert_eq S
App (App (App (S, K), I), K)
|> eval
|> _assert_eq K
__assert_eq / actual: UH0_0 / expected: UH0_0 __assert_eq / actual: UH0_0 / expected: UH0_0 __assert_eq / actual: UH0_0 / expected: UH0_0 __assert_eq / actual: UH0_0 / expected: UH0_0 __assert_eq / actual: UH0_0 / expected: UH0_0 __assert_eq / actual: UH0_1 / expected: UH0_1 __assert_eq / actual: UH0_3 (UH0_1, UH0_0) / expected: UH0_3 (UH0_1, UH0_0) __assert_eq / actual: UH0_3 (UH0_1, UH0_1) / expected: UH0_3 (UH0_1, UH0_1) __assert_eq / actual: UH0_0 / expected: UH0_0 __assert_eq / actual: UH0_1 / expected: UH0_1 __assert_eq / actual: UH0_2 / expected: UH0_2 __assert_eq / actual: UH0_2 / expected: UH0_2 __assert_eq / actual: UH0_0 / expected: UH0_0 __assert_eq / actual: UH0_0 / expected: UH0_0 __assert_eq / actual: UH0_0 / expected: UH0_0 __assert_eq / actual: UH0_2 / expected: UH0_2 __assert_eq / actual: UH0_1 / expected: UH0_1