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

--  See license.txt for further details


package body Kompsos.Prelude is


    function Head
           (This                 : in World;
            Full_List, Head_Term : in Term'Class)
        return World is
    begin
        return Result : World := This do
            Result.Unify (T (Head_Term, Result.Fresh), Full_List);
        end return;
    end Head;


    procedure Head
           (This                 : in out World;
            Full_List, Head_Term : in     Term'Class) is
    begin
        This := This.Head (Full_List, Head_Term);
    end Head;




    function Tail
           (This                 : in World;
            Full_List, Tail_Term : in Term'Class)
        return World is
    begin
        return Result : World := This do
            Result.Unify (T (Result.Fresh, Tail_Term), Full_List);
        end return;
    end Tail;


    procedure Tail
           (This                 : in out World;
            Full_List, Tail_Term : in     Term'Class) is
    begin
        This := This.Tail (Full_List, Tail_Term);
    end Tail;




    function Cons
           (This                            : in World;
            Head_Term, Tail_Term, Full_List : in Term'Class)
        return World is
    begin
        return Result : World := This do
            Result.Unify (T (Head_Term, Tail_Term), Full_List);
        end return;
    end Cons;


    procedure Cons
           (This                            : in out World;
            Head_Term, Tail_Term, Full_List : in     Term'Class) is
    begin
        This := This.Cons (Head_Term, Tail_Term, Full_List);
    end Cons;




    function Nil
           (This     : in World;
            Nil_Term : in Term'Class)
        return World is
    begin
        return Result : World := This do
            Result.Unify (Null_Term, Nil_Term);
        end return;
    end Nil;


    procedure Nil
           (This     : in out World;
            Nil_Term : in     Term'Class) is
    begin
        This := This.Nil (Nil_Term);
    end Nil;




    function Pair
           (This      : in World;
            Pair_Term : in Term'Class)
        return World is
    begin
        return Result : World := This do
            Result.Cons (Result.Fresh, Result.Fresh, Pair_Term);
        end return;
    end Pair;


    procedure Pair
           (This      : in out World;
            Pair_Term : in     Term'Class) is
    begin
        This := This.Pair (Pair_Term);
    end Pair;




    function Linked_List
           (This      : in World;
            List_Term : in Term'Class)
        return World
    is
        One, Two : World := This;
        Ref_Term : constant Term := Two.Fresh;
    begin
        One.Nil (List_Term);

        Two.Pair (List_Term);
        Two.Tail (List_Term, Ref_Term);
        if not Two.Failed then
            Two.Linked_List (Ref_Term);
        end if;

        return Disjunct (One, Two);
    end Linked_List;


    procedure Linked_List
           (This      : in out World;
            List_Term : in     Term'Class) is
    begin
        This := This.Linked_List (List_Term);
    end Linked_List;




    function Member
           (This                 : in World;
            Item_Term, List_Term : in Term'Class)
        return World
    is
        One, Two : World := This;
        Ref_Term : constant Term := Two.Fresh;
    begin
        One.Head (List_Term, Item_Term);

        Two.Tail (List_Term, Ref_Term);
        if not Two.Failed then
            Two.Member (Item_Term, Ref_Term);
        end if;

        return Disjunct (One, Two);
    end Member;


    procedure Member
           (This                 : in out World;
            Item_Term, List_Term : in     Term'Class) is
    begin
        This := This.Member (Item_Term, List_Term);
    end Member;




    function Remove
           (This                           : in World;
            Item_Term, List_Term, Out_Term : in Term'Class)
        return World
    is
        One, Two : World := This;
        Left  : constant Term := Two.Fresh;
        Right : constant Term := Two.Fresh;
        Rest  : constant Term := Two.Fresh;
    begin
        One.Head (List_Term, Item_Term);
        One.Tail (List_Term, Out_Term);

        --  infinite loops if run in reverse with vars for item and list
        --  probably needs lazy conjunction to work properly
        Two.Cons (Left, Right, List_Term);
        if not Two.Failed then
            Two.Remove (Item_Term, Right, Rest);
            Two.Cons (Left, Rest, Out_Term);
        end if;

        return Disjunct (One, Two);
    end Remove;


    procedure Remove
           (This                           : in out World;
            Item_Term, List_Term, Out_Term : in     Term'Class) is
    begin
        This := This.Remove (Item_Term, List_Term, Out_Term);
    end Remove;




    function Append
           (This                            : in World;
            List_Term, Item_Term, Out_Term : in Term'Class)
        return World
    is
        One, Two : World := This;
        Left  : constant Term := Two.Fresh;
        Right : constant Term := Two.Fresh;
        Rest  : constant Term := Two.Fresh;
    begin
        One.Nil (List_Term);
        One.Unify (Item_Term, Out_Term);

        Two.Cons (Left, Right, List_Term);
        Two.Cons (Left, Rest, Out_Term);
        if not Two.Failed then
            Two.Append (Right, Item_Term, Rest);
        end if;

        return Disjunct (One, Two);
    end Append;


    procedure Append
           (This                            : in out World;
            List_Term, Item_Term, Out_Term : in     Term'Class) is
    begin
        This := This.Append (List_Term, Item_Term, Out_Term);
    end Append;


end Kompsos.Prelude;