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
|
-- Programmed by Jedidiah Barber
-- Licensed under the Sunset License v1.0
-- See license.txt for further details
with
Ada.Text_IO,
Kompsos.Math,
Kompsos.Pretty_Print;
procedure Addsubo is
package TIO renames Ada.Text_IO;
package InKomp is new Kompsos (Integer);
use InKomp;
package Math is new InKomp.Math (0, 1);
package Printer is new InKomp.Pretty_Print (Integer'Image);
function B
(Item : in Natural)
return Term
renames Math.Build;
function P
(Item : in Integer)
return String
renames Printer.Image;
function PV
(Item : in Term)
return String is
begin
return P (Math.Value (Item));
exception
when others =>
return Printer.Image (Item);
end PV;
procedure Add_Test
(Addend1, Addend2 : in Natural)
is
Relation : Goal := Empty_Goal;
Sum : constant Term := Relation.Fresh;
Result : State;
begin
Math.Add (Relation, B (Addend1) & B (Addend2) & Sum);
Result := Relation.Run;
TIO.Put_Line (P (Addend1) & " + " & P (Addend2) & " = " & PV (Sum.Resolve (Result)));
end Add_Test;
procedure Sub_Test
(Minuend, Subtrahend : in Natural)
is
Relation : Goal := Empty_Goal;
Diff : constant Term := Relation.Fresh;
Result : State;
begin
Math.Subtract (Relation, B (Minuend) & B (Subtrahend) & Diff);
Result := Relation.Run;
TIO.Put_Line (P (Minuend) & " - " & P (Subtrahend) & " = " & PV (Diff.Resolve (Result)));
end Sub_Test;
begin
TIO.Put_Line ("Addition");
Add_Test (5, 0);
Add_Test (0, 5);
Add_Test (1, 4);
Add_Test (4, 1);
Add_Test (3, 2);
Add_Test (2, 3);
Add_Test (17, 13);
TIO.New_Line;
TIO.Put_Line ("Subtraction");
Sub_Test (25, 17);
Sub_Test (5, 4);
Sub_Test (7, 7);
TIO.New_Line;
TIO.Put_Line ("Expected Failure");
Sub_Test (0, 1); -- Should fail with nothing ending up bound to the variable term
end Addsubo;
|