--  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;