--  Programmed by Jedidiah Barber
--  Licensed under the Sunset License v1.0

--  See license.txt for further details


with

    Ada.Text_IO,
    Kompsos.Pretty_Print;


procedure Complete is

    package TIO renames Ada.Text_IO;


    package InKomp is new Kompsos (Integer);
    use InKomp;

    package Printer is new InKomp.Pretty_Print (Integer'Image);


    function Fives
           (This : in Goal;
            Item : in Term'Class)
        return Goal
    is
        One, Two : Goal := This;
    begin
        One.Unify (Item, 5);
        Two.Conjunct (Fives'Access, Item);
        return Disjunct (One, Two);
    end Fives;

begin

    TIO.Put_Line ("This program will loop forever unless the implementation is using");
    TIO.Put_Line ("a complete search strategy. It is suggested to terminate it manually");
    TIO.Put_Line ("if it doesn't complete quickly.");

    TIO.New_Line;

    declare
        Relation : Goal          := Empty_Goal;
        Value    : constant Term := Relation.Fresh;
        Ignore   : constant Term := Relation.Fresh;
    begin
        Relation := Disjunct (Relation.Unify (Ignore, 6), Relation.Unify (Value, 7));
        Relation := Fives (Relation, Ignore);
        TIO.Put_Line ("Value is " & Printer.Image (Value.Resolve (Relation.Run)) & " on right.");
    end;

    declare
        Relation : Goal          := Empty_Goal;
        Value    : constant Term := Relation.Fresh;
        Ignore   : constant Term := Relation.Fresh;
    begin
        Relation := Disjunct (Relation.Unify (Value, 7), Relation.Unify (Ignore, 6));
        Relation := Fives (Relation, Ignore);
        TIO.Put_Line ("Value is " & Printer.Image (Value.Resolve (Relation.Run)) & " on left.");
    end;

    TIO.New_Line;

    TIO.Put_Line ("Test complete.");

end Complete;