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

--  See license.txt for further details


--   1. There are five houses in a row, each of a different color
--       and inhabited by men of different nationalities,
--       with different pets, drinks, and cigarettes.
--   2. The Englishman lives in the red house.
--   3. The Spaniard owns a dog.
--   4. Coffee is drunk in the green house.
--   5. The Ukrainian drinks tea.
--   6. The green house is directly to the right of the ivory house.
--   7. The Old Gold smoker owns snails.
--   8. Kools are being smoked in the yellow house.
--   9. Milk is drunk in the middle house.
--  10. The Norwegian lives in the first house on the left.
--  11. The Chesterfield smoker lives next to the fox owner.
--  12. Kools are smoked in the house next to the house where the horse is kept.
--  13. The Lucky Strike smoker drinks orange juice.
--  14. The Japanese smokes Parliaments.
--  15. The Norwegian lives next to the blue house.


with

    Ada.Strings.Unbounded,
    Ada.Text_IO,
    Kompsos.Pretty_Print;


procedure Zebra is

    package SU  renames Ada.Strings.Unbounded;
    package TIO renames Ada.Text_IO;

    function "+"
           (Item : in String)
        return SU.Unbounded_String
    renames SU.To_Unbounded_String;


    package SKomp is new Kompsos (SU.Unbounded_String);
    use SKomp;

    package Printer is new SKomp.Pretty_Print (SU.To_String);


    function On_Right
           (This   : in World;
            Inputs : in Term_Array)
        return World;

    function On_Right
           (This   : in World;
            Inputs : in Term_Array)
        return World
    is
        Left_Term  : Term renames Inputs (1);
        Right_Term : Term renames Inputs (2);
        List_Term  : Term renames Inputs (3);

        One, Two : World := This;
        One_Ref  : constant Term := One.Fresh;
        Two_Ref  : constant Term := Two.Fresh;
    begin
        One.Head (List_Term & Left_Term);
        One.Tail (List_Term & One_Ref);
        One.Head (One_Ref & Right_Term);

        Two.Tail (List_Term & Two_Ref);
        Two.Conjunct (On_Right'Access, Left_Term & Right_Term & Two_Ref);

        return Disjunct (One, Two);
    end On_Right;


    function Next_To
           (This   : in World;
            Inputs : in Term_Array)
        return World
    is
        Left_Term  : Term renames Inputs (1);
        Right_Term : Term renames Inputs (2);
        List_Term  : Term renames Inputs (3);
    begin
        return Disjunct
           (On_Right (This, Left_Term  & Right_Term & List_Term),
            On_Right (This, Right_Term & Left_Term  & List_Term));
    end Next_To;


    Verse : World := Empty_World;

    function N is new Make_Fresh (Verse);

    Houses      : constant Term_Array := N & N & N & N & N;
    Houses_Term : constant Term       := T (Houses);

    Result : State;

begin

    Verse.Unify (Houses (1), T (T (+"norwegian") & N & N & N & N));
    Verse.Unify (Houses (3), T (N & N & T (+"milk") & N & N));

    Verse.Member (T (T (+"englishman") & N & N & N & T (+"red")) & Houses_Term);
    Verse.Member (T (N & T (+"kools") & N & N & T (+"yellow")) & Houses_Term);
    Verse.Member (T (T (+"spaniard") & N & N & T (+"dog") & N) & Houses_Term);
    Verse.Member (T (N & N & T (+"coffee") & N & T (+"green")) & Houses_Term);
    Verse.Member (T (T (+"ukrainian") & N & T (+"tea") & N & N) & Houses_Term);
    Verse.Member (T (N & T (+"luckystrikes") & T (+"oj") & N & N) & Houses_Term);
    Verse.Member (T (T (+"japanese") & T (+"parliaments") & N & N & N) & Houses_Term);
    Verse.Member (T (N & T (+"oldgolds") & N & T (+"snails") & N) & Houses_Term);
    Verse.Member (T (N & N & T (+"water") & N & N) & Houses_Term);
    Verse.Member (T (N & N & N & T (+"zebra") & N) & Houses_Term);

    Verse := On_Right (Verse,
        T (N & N & N & N & T (+"ivory")) &
        T (N & N & N & N & T (+"green")) & Houses_Term);

    Verse := Next_To (Verse,
        T (T (+"norwegian") & N & N & N & N) &
        T (N & N & N & N & T (+"blue")) & Houses_Term);
    Verse := Next_To (Verse,
        T (N & N & N & T (+"horse") & N) &
        T (N & T (+"kools") & N & N & N) & Houses_Term);
    Verse := Next_To (Verse,
        T (N & N & N & T (+"fox") & N) &
        T (N & T (+"chesterfields") & N & N & N) & Houses_Term);

    Result := Verse.Take_First;

    for House of Houses loop
        TIO.Put_Line (Printer.Image (House.Resolve (Result)));
    end loop;

end Zebra;