@@ -59,16 +59,15 @@ struct Nat
59
59
virtual ~Nat () {}
60
60
};
61
61
62
- typedef std::unique_ptr<Nat> NatPtr;
63
-
64
62
struct O : Nat
65
63
{
66
64
};
67
65
68
66
struct S : Nat
69
67
{
70
- S (Nat* n) : e(n) {}
71
- NatPtr e;
68
+ S (const Nat* n) : e(n) {}
69
+ ~S () { if (e) delete e; }
70
+ const Nat* e;
72
71
};
73
72
74
73
// ------------------------------------------------------------------------------
@@ -97,13 +96,38 @@ int evl(const Nat& n)
97
96
98
97
// ------------------------------------------------------------------------------
99
98
99
+ // Add two inductively defined Nat
100
+ const Nat* plus (const Nat* n, const Nat* m)
101
+ {
102
+ var<const Nat*> a;
103
+ var<const Nat*> b;
104
+
105
+ Match (n, m)
106
+ {
107
+
108
+ Case (_, C<O>()) return n; // m + 0 = m
109
+ Case (C<O>(), _) return m; // 0 + m = m
110
+ Case (C<S>(a), C<S>(b)) return new S (new S (plus (a, b))); // S n + S m = S (S (n + m))
111
+ Otherwise () return nullptr ;
112
+ }
113
+ EndMatch
114
+
115
+ XTL_UNREACHABLE; // To avoid warning that control may reach end of a non-void function
116
+ }
117
+
118
+ // ------------------------------------------------------------------------------
119
+
100
120
int main ()
101
121
{
102
- NatPtr a ( new S (new S (new O) ));
103
- NatPtr b ( new S (new O) );
122
+ Nat* a = new S (new S (new O));
123
+ Nat* b = new S (new O);
104
124
105
125
std::cout << evl (*a) << std::endl;
106
126
std::cout << evl (*b) << std::endl;
127
+
128
+ const Nat* c = plus (a,b);
129
+
130
+ std::cout << evl (*c) << std::endl;
107
131
}
108
132
109
133
// ------------------------------------------------------------------------------
0 commit comments