test/boolnum.adb


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


--  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 Boolnum is

    package TIO renames Ada.Text_IO;


    package BKomp is new Kompsos (Boolean);
    use BKomp;

    package Math is new BKomp.Math (False, True);

    package Printer is new BKomp.Pretty_Print (Boolean'Image);


    Relation : Goal := Empty_Goal;

    Four : constant Term := Math.Build (4);
    Five : constant Term := Math.Build (5);
    Nine : constant Term := Math.Build (9);

    Sum     : constant Term := Relation.Fresh;
    Product : constant Term := Relation.Fresh;

    Result : State;

begin

    TIO.Put_Line ("Demonstration of arithmetic using boolean zero and one elements.");
    TIO.New_Line;

    Math.Add (Relation, Five & Nine & Sum);
    Math.Multiply (Relation, Four & Five & Product);

    Result := Relation.Run;

    TIO.Put_Line (Printer.Image (Five) & " + " & Printer.Image (Nine) &
        " = " & Printer.Image (Sum.Resolve (Result)));
    TIO.Put_Line (Printer.Image (Four) & " * " & Printer.Image (Five) &
        " = " & Printer.Image (Product.Resolve (Result)));

end Boolnum;