timl/examples/unit-test-basic.timl at master · wangpengmit/timl · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
structure UnitTestBasic = struct

open String

val str_int = int2str
fun println s = print s; print "\n"
fun print_int i return using 1810.0 =
  let
    val StringFromInt s = int2str i
  in
    print s
  end

datatype printable =
         S {len : Nat | len <= 361} of string {len} --> printable
       | I of int --> printable
       | Ln

fun print_printable a return using 1811.0 =
  case a of
      S s => print s
    | I i => print_int i
    | Ln => println ""

fun printls {len : Nat} (ls : list _ {len}) = List.app print_printable ls

val s = ""

val a = 1
val a = ()

val x = 1 + 2
val y = x + 1
val z = x + y + x

val () = print "z=(1+2)+((1+2)+1)+(1+2)="
val () = print_int <| z
val () = println ""

val () = assert (z = 10, "z=(1+2)+((1+2)+1)+(1+2)=10")

val p = (1, ())

val i = 1
val u = ()
val p = (i, u)

val foo = fn arg => arg + 1

val a = foo 1

fun f x = x + 1

val a = f 2

fun f x y = x + y

val a = f 1 2
val () = printls [S "a = f 1 2 = 1+2 = ", I a, Ln]

val () = assert (a = 3, "a = f 1 2 = 1+2 = 3")

fun foo {i : Nat} {j | j > i} () =
    let
      fun bar (a : nat {i}, b : nat {j}) =
          a #+ b
      fun bar2 (a : nat {j}, b : nat {i}) =
          b #+ a
      fun bar3 (a : nat {j}, b : nat {i}) =
          a #+ b
    in
      ()
    end

fun id arg = arg

val f = id

val a = f 1

val a = f ()

fun twice f x = f (f x)

val n = if 1 > 2 then 1 else 2
val () = printls [S "n=(if 1 > 2 then 1 else 2)=", I n, Ln]

val () = assert ((if 1 > 2 then 1 else 0) = 0, "(if 1 > 2 then 1 else 0) = 0")
val () = assert ((ifdec #1 #< #2 then 1 else 0) = 1, "ifdec #1 #< #2 then 1 else 0) = 1")

fun fact_tail {n : Nat} (n : nat {n}, acc) (* return using 3.0 * $n *) =
  ifdec n #< #1 then acc
  else fact_tail (n #- #1, __&nat2int n * acc) using 4.0 * $n

val () = printls [S "fact_tail (4, 1) = ", I <| fact_tail (#4, 1), Ln]

val () = assert (fact_tail (#4, 1) = 24, "fact_tail (#4, 1) = 24")

fun fact {n : Nat} (n : nat {n}) (* return using 3.0 * $n *) =
  ifdec n #< #1 then 1
  else nat2int n * fact (n #- #1) using 4.0 * $n

val () = printls [S "fact 4 = ", I <| fact #4, Ln]

val () = assert (fact #4 = 24, "fact #4 = 24")

end