--  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 (Term (Head_Term), T (Result.Fresh)), Full_List);
        end return;
    end Head;


    procedure Head
           (This                 : in out World;
            Full_List, Head_Term : in     Term'Class) is
    begin
        This := Head (This, 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 (T (Result.Fresh), Term (Tail_Term)), Full_List);
        end return;
    end Tail;


    procedure Tail
           (This                 : in out World;
            Full_List, Tail_Term : in     Term'Class) is
    begin
        This := Tail (This, 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 (Term (Head_Term), 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 := Cons (This, 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 := Nil (This, Nil_Term);
    end Nil;




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


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




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

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

        return Disjunct (Result_Nil, Result_Pair);
    end Linked_List;


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




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

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

        return Disjunct (Result_Head, Result_Rest);
    end Member;


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




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

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

        return Disjunct (Result_Head, Result_Rest);
    end Remove;


    procedure Remove
           (This                           : in out World;
            Item_Term, List_Term, Out_Term : in     Term'Class) is
    begin
        This := Remove (This, 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
        Result_Nil, Result_Rest : World := This;
        Left  : constant Term := T (Result_Rest.Fresh);
        Right : constant Term := T (Result_Rest.Fresh);
        Rest  : constant Term := T (Result_Rest.Fresh);
    begin
        Nil (Result_Nil, List_Term);
        Unify (Result_Nil, Item_Term, Out_Term);

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

        return Disjunct (Result_Nil, Result_Rest);
    end Append;


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


end Kompsos.Prelude;