Commit | Line | Data |
---|---|---|
7f918cf1 CE |
1 | datatype 'a t = R of 'a | L of 'a t t |
2 | ||
3 | val rec build: int -> int t = | |
4 | fn 0 => R 17 | |
5 | | n => L (R (build (n - 1))) | |
6 | ||
7 | val rec depth: int t -> int = | |
8 | fn R _ => 0 | |
9 | | L (R z) => 1 + depth z | |
10 | | _ => raise Match | |
11 | ||
12 | val n = depth (build 13) | |
13 | val _ = | |
14 | if n = 13 | |
15 | then () | |
16 | else raise Fail "bug" | |
17 | ||
18 | (* | |
19 | val _ = R 13 | |
20 | val _ = L (R (R 13)) | |
21 | ||
22 | val rec build: int -> int t = | |
23 | fn 0 => R 13 | |
24 | | n => L (R (build (n - 1))) | |
25 | ||
26 | val _ = f 13 | |
27 | *) | |
28 | (* | |
29 | ||
30 | val rec f = | |
31 | fn R _ => 0 | |
32 | | L (R z) => 1 + f z | |
33 | ||
34 | val v0: int t = R 13 | |
35 | val v2: int t t = R v0 | |
36 | val v1: int t = L (v2: int t t) | |
37 | val _ = L (L (R (R (R 13)))) | |
38 | val _ = L (R (L (R (R 13)))) | |
39 | val _ = L (L (R (R (R (R (R 13)))))) | |
40 | ||
41 | *) | |
42 | ||
43 | (* | |
44 | datatype 'a t = A of 'a | B of ('a t * 'a t) t | |
45 | val v1 = A 13 | |
46 | val v2 = A (v1, v1) | |
47 | val v3 = A (v2, v2) | |
48 | val v4 = B v3 | |
49 | val v5 = B v4 | |
50 | ||
51 | val x = A 1 : int t | |
52 | ||
53 | val y = B (A (x, x)) | |
54 | ||
55 | val z = B (A (y, y)) | |
56 | ||
57 | val a = B (A (z, z)) | |
58 | ||
59 | fun d ((A _) : 'a t) : int = 0 | |
60 | | d ((B (A (x, _))) : 'a t) : int = 1 + d x | |
61 | ||
62 | val n = d a | |
63 | *) | |
64 | ||
65 | ||
66 | (* | |
67 | ||
68 | Here's (the relevant part of) what the monomorphiser in smlc returns | |
69 | for your program. | |
70 | ||
71 | datatype t_0 = B_0 of t_1 | A_0 of int | |
72 | and t_1 = A_1 of (t_0 * t_0) | |
73 | ||
74 | It figures out exactly your observation that every use of B must be | |
75 | followed by A. | |
76 | ||
77 | [z0 = int t] | |
78 | datatype z0 = A of int | B of z1 | |
79 | ||
80 | [z1 = (z0 * z0) t] | |
81 | datatype z1 = A of z0 * z0 | B of z2 | |
82 | ||
83 | [z2 = (z1 * z1) t] | |
84 | datatype z2 = A of z1 * z1 | B of z3 | |
85 | ||
86 | [z3 = (z2 * z2) t] | |
87 | ||
88 | ||
89 | ||
90 | ||
91 | B z1 | |
92 | B (B z2) | |
93 | B (B (A (z1, z1))) | |
94 | B (B (A (A (z0,z0), A (z0,z0)))) | |
95 | ||
96 | B (B (A (A (v1, v1), A (v1, v1)))) | |
97 | ||
98 | B (B (A (A (v1, v1), A (v1, v1)))) | |
99 | ||
100 | ||
101 | ||
102 | datatype z = A of int | B of (z * z) t | |
103 | datatype w = A of z * z | B of (w * w) t | |
104 | ||
105 | *) |