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

--  See license.txt for further details

with

    Ada.Assertions,
    Ada.Unchecked_Deallocation;


package body Kompsos.Collector is


    ----------------------
    --  Progress State  --
    ----------------------

    Book_Root   : Book_Node_Access := null;
    Loose_Books : Loose_Book_Vectors.Vector;

    Global_Var : Variable := Relation.Next_Var;

    Next_Index  : Long_Positive := 1;
    Next_State  : State;
    State_Valid : Boolean       := False;
    Exhausted   : Boolean       := False;




    -------------------------
    --  Memory Management  --
    -------------------------

    procedure Free is new Ada.Unchecked_Deallocation (Book_Node, Book_Node_Access);
    procedure Free is new Ada.Unchecked_Deallocation (Cache_Entry, Cache_Entry_Access);
    procedure Free is new Ada.Unchecked_Deallocation (Goal, Goal_Access);
    procedure Free is new Ada.Unchecked_Deallocation (State, State_Access);

    procedure Finalize
           (This : in out Collector_Final_Controller) is
    begin
        Reset (Relation.Graph.Actual, Book_Root);
    end Finalize;




    ------------------------
    --  Internal Helpers  --
    ------------------------

    --  Unification  --

    procedure Walk
           (This : in     State;
            Item : in out Term)
    is
        Bound_Term : Term;
    begin
        while Item.Kind = Var_Term and then Lookup (This, Item.Var, Bound_Term) loop
            Item := Bound_Term;
        end loop;
    end Walk;


    function Do_Unify
           (Potential   : in     State;
            Left, Right : in     Term'Class;
            Extended    :    out State)
        return Boolean
    is
        Real_Left  : Term := Term (Left);
        Real_Right : Term := Term (Right);
    begin
        --  Resolve Variable substitution
        Walk (Potential, Real_Left);
        Walk (Potential, Real_Right);

        --  Unify equal Variable/Atom/Null Terms
        if (Real_Left.Kind = Var_Term and then
            Real_Right.Kind = Var_Term and then
            Real_Left = Real_Right) or else
           (Real_Left.Kind = Atom_Term and then
            Real_Right.Kind = Atom_Term and then
            Real_Left = Real_Right) or else
           (Real_Left.Kind = Null_Term and Real_Right.Kind = Null_Term)
        then
            Extended := Potential;
            return True;
        end if;

        --  Unify Variable and other Terms by introducing a new substitution
        if Real_Left.Kind = Var_Term then
            Extended := (Ctrl => (Ada.Finalization.Controlled with
                Actual => new State_Component'(
                    Counter => 1,
                    Key     => Real_Left.Var,
                    Value   => Real_Right,
                    Next    => Potential)));
            return True;
        end if;
        if Real_Right.Kind = Var_Term then
            Extended := (Ctrl => (Ada.Finalization.Controlled with
                Actual => new State_Component'(
                    Counter => 1,
                    Key     => Real_Right.Var,
                    Value   => Real_Left,
                    Next    => Potential)));
            return True;
        end if;

        --  Unify Pair Terms by unifying each corresponding part
        if Real_Left.Kind = Pair_Term and then Real_Right.Kind = Pair_Term then
            return Do_Unify (Potential, Real_Left.Left, Real_Right.Left, Extended) and then
                Do_Unify (Extended, Real_Left.Right, Real_Right.Right, Extended);
        end if;

        --  Otherwise unification fails
        return False;
    end Do_Unify;



    --  Result Collection --

    function Call_Lazy
           (This : in Goal;
            Data : in Lazy_Holders.Holder)
        return Goal
    is
        Ref : constant Lazy_Holders.Constant_Reference_Type := Data.Constant_Reference;
    begin
        case Ref.Kind is
        when Zero_Arg =>
            return Ref.ZFunc (This);
        when One_Arg  =>
            return Ref.OFunc (This, Ref.OInput);
        when Many_Arg =>
            return Ref.MFunc (This, Term_Array_Holders.Constant_Reference (Ref.MInput));
        end case;
    end Call_Lazy;


    procedure Do_Reset
           (Ptr   : in     Graph_Component_Access;
            Book  : in out Book_Node_Access;
            Extra : in out Book_Node_Vectors.Vector) is
    begin
        if Ptr = null or Book = null then
            return;
        end if;

        if Book.Cache /= null then
            for Item of Book.Cache.Data loop
                Free (Item.Data);
            end loop;
            Free (Book.Cache);
        end if;

        case Book.Data.Kind is
        when Unify_Node =>
            Do_Reset (Ptr.Uni_Goal.Actual, Book.Next1, Extra);
        when Disjunct_Node =>
            Do_Reset (Ptr.Dis_Goal1.Actual, Book.Next1, Extra);
            Do_Reset (Ptr.Dis_Goal2.Actual, Book.Next2, Extra);
        when Conjunct_Node =>
            Do_Reset (Ptr.Con_Goal.Actual, Book.Next1, Extra);
            if Book.Data.Con_Part /= null then
                Reset (Book.Data.Con_Part.Graph.Actual, Book.Next2);
                Free (Book.Data.Con_Part);
            end if;
            Free (Book.Data.Con_Base);
        when Recurse_Node =>
            Do_Reset (Ptr.Rec_Goal.Actual, Book.Next1, Extra);
        end case;

        if Ptr.Counter > 1 then
            if not Extra.Contains (Book) then
                Extra.Append (Book);
            end if;
        else
            Free (Book);
        end if;
    end Do_Reset;


    procedure Reset
           (Ptr  : in     Graph_Component_Access;
            Book : in out Book_Node_Access)
    is
        Extra : Book_Node_Vectors.Vector;
    begin
        Do_Reset (Ptr, Book, Extra);
        for Item of Extra loop
            if Item = Book then
                Free (Book);
            else
                Free (Item);
            end if;
        end loop;
    end Reset;


    function Raw_New_Book
           (Kind : in Node_Kind)
        return Book_Node_Access is
    begin
        case Kind is
        when Unify_Node =>
            return new Book_Node'(Data => (Kind => Unify_Node,    others => <>), others => <>);
        when Disjunct_Node =>
            return new Book_Node'(Data => (Kind => Disjunct_Node, others => <>), others => <>);
        when Conjunct_Node =>
            return new Book_Node'(Data => (Kind => Conjunct_Node, others => <>), others => <>);
        when Recurse_Node =>
            return new Book_Node'(Data => (Kind => Recurse_Node,  others => <>), others => <>);
        end case;
    end Raw_New_Book;


    function New_Book
           (Ptr : in Graph_Component_Access)
        return Book_Node_Access is
    begin
        pragma Assert (Ptr.Counter /= 0);
        if Ptr.Counter = 1 or Ptr = Relation.Graph.Actual then
            return Raw_New_Book (Ptr.Kind);
        else
            return Acc : constant Book_Node_Access := Raw_New_Book (Ptr.Kind) do
                Loose_Books.Append ((1, Ptr, Acc));
            end return;
        end if;
    end New_Book;


    function Connect_Loose
           (Ptr : in Graph_Component_Access)
        return Book_Node_Access is
    begin
        for Index in Loose_Books.First_Index .. Loose_Books.Last_Index loop
            if Loose_Books.Element (Index).Ptr = Ptr then
                return Acc : constant Book_Node_Access := Loose_Books.Element (Index).Book do
                    Loose_Books (Index).Used := Loose_Books (Index).Used + 1;
                    if Loose_Books.Element (Index).Used >= Ptr.Counter then
                        Loose_Books.Delete (Index);
                    end if;
                end return;
            end if;
        end loop;
        return null;
    end Connect_Loose;


    function Do_Get_Next
           (Ptr    : in     Graph_Component_Access;
            Book   : in out Book_Node_Access;
            Base   : in     State;
            Index  : in     Long_Positive;
            Result :    out State)
        return Boolean is
    begin
        case Ptr.Kind is
        when Unify_Node =>
            if Book = null then
                Book := New_Book (Ptr);
            end if;
            while Get_Next
               (Ptr.Uni_Goal'Unchecked_Access,
                Book.Next1, Base,
                Index + Book.Data.Uni_Offset,
                Result)
            loop
                if Do_Unify (Result, Ptr.Uni_Term1, Ptr.Uni_Term2, Result) then
                    return True;
                else
                    Book.Data.Uni_Offset := Book.Data.Uni_Offset + 1;
                end if;
            end loop;
            return False;

        when Disjunct_Node =>
            if Book = null then
                Book := New_Book (Ptr);
            end if;
            if Book.Data.Dis_Gone1 then
                if Book.Data.Dis_Gone2 then
                    return False;
                elsif Get_Next
                   (Ptr.Dis_Goal2'Unchecked_Access,
                    Book.Next2, Base,
                    Book.Data.Dis_Next2,
                    Result)
                then
                    Book.Data.Dis_Next2 := Book.Data.Dis_Next2 + 1;
                    return True;
                else
                    Book.Data.Dis_Gone2 := True;
                    return False;
                end if;
            elsif Book.Data.Dis_Gone2 then
                if Get_Next
                   (Ptr.Dis_Goal1'Unchecked_Access,
                    Book.Next1, Base,
                    Book.Data.Dis_Next1,
                    Result)
                then
                    Book.Data.Dis_Next1 := Book.Data.Dis_Next1 + 1;
                    return True;
                else
                    Book.Data.Dis_Gone1 := True;
                    return False;
                end if;
            elsif Book.Data.Dis_Flag then
                if Get_Next
                   (Ptr.Dis_Goal1'Unchecked_Access,
                    Book.Next1, Base,
                    Book.Data.Dis_Next1,
                    Result)
                then
                    Book.Data.Dis_Next1 := Book.Data.Dis_Next1 + 1;
                    Book.Data.Dis_Flag := not Book.Data.Dis_Flag;
                    return True;
                else
                    Book.Data.Dis_Gone1 := True;
                    if Get_Next
                       (Ptr.Dis_Goal2'Unchecked_Access,
                        Book.Next2, Base,
                        Book.Data.Dis_Next2,
                        Result)
                    then
                        Book.Data.Dis_Next2 := Book.Data.Dis_Next2 + 1;
                        return True;
                    else
                        Book.Data.Dis_Gone2 := True;
                        return False;
                    end if;
                end if;
            else
                if Get_Next
                   (Ptr.Dis_Goal2'Unchecked_Access,
                    Book.Next2, Base,
                    Book.Data.Dis_Next2,
                    Result)
                then
                    Book.Data.Dis_Next2 := Book.Data.Dis_Next2 + 1;
                    Book.Data.Dis_Flag := not Book.Data.Dis_Flag;
                    return True;
                else
                    Book.Data.Dis_Gone2 := True;
                    if Get_Next
                       (Ptr.Dis_Goal1'Unchecked_Access,
                        Book.Next1, Base,
                        Book.Data.Dis_Next1,
                        Result)
                    then
                        Book.Data.Dis_Next1 := Book.Data.Dis_Next1 + 1;
                        return True;
                    else
                        Book.Data.Dis_Gone1 := True;
                        return False;
                    end if;
                end if;
            end if;

        when Conjunct_Node =>
            if Book = null then
                Book := New_Book (Ptr);
                if not Get_Next (Ptr.Con_Goal'Unchecked_Access, Book.Next1, Base, 1, Result) then
                    Book.Data.Con_Gone := True;
                else
                    Book.Data.Con_Base := new State'(Result);
                    Book.Data.Con_Part := new Goal'(
                        Call_Lazy
                           ((Graph    => (Ada.Finalization.Controlled with Actual => null),
                             Next_Var => Global_Var),
                            Ptr.Con_Data));
                    Global_Var := Book.Data.Con_Part.Next_Var;
                end if;
            end if;
            if Book.Data.Con_Gone then
                return False;
            end if;
            while not Get_Next
               (Constant_Graph_Access'(Book.Data.Con_Part.Graph'Access),
                Book.Next2, Book.Data.Con_Base.all,
                Book.Data.Con_Next,
                Result)
            loop
                Reset (Book.Data.Con_Part.Graph.Actual, Book.Next2);
                Book.Data.Con_From := Book.Data.Con_From + 1;
                if Get_Next
                   (Ptr.Con_Goal'Unchecked_Access,
                    Book.Next1, Base,
                    Book.Data.Con_From,
                    Result)
                then
                    Book.Data.Con_Base.all := Result;
                    Book.Data.Con_Next := 1;
                else
                    Book.Data.Con_Gone := True;
                    Free (Book.Data.Con_Part);
                    Free (Book.Data.Con_Base);
                    return False;
                end if;
            end loop;
            Book.Data.Con_Next := Book.Data.Con_Next + 1;
            return True;

        when Recurse_Node =>
            if Book = null then
                Book := New_Book (Ptr);
            end if;
            if Ptr.Rec_Goal.Actual = null then
                Book.Data.Rec_Cache := False;
            elsif Book.Next1 = null then
                Book.Next1 := Connect_Loose (Ptr.Rec_Goal.Actual);
            end if;
            if Book.Data.Rec_Cache then
                if Book.Next1 = null then
                    Book.Next1 := New_Book (Ptr.Rec_Goal.Actual);
                    Book.Next1.Cache := new Cache_Entry'(True, State_Vectors.Empty_Vector);
                elsif Book.Next1.Cache = null then
                    Book.Next1.Cache := new Cache_Entry'(True, State_Vectors.Empty_Vector);
                else
                    Book.Next1.Cache.Keep := True;
                end if;
            end if;
            if Book.Data.Rec_Gone then
                return False;
            end if;
            while not Get_Next
               (Ptr.Rec_Goal'Unchecked_Access,
                Book.Next1, Base,
                Book.Data.Rec_Next,
                Result)
            loop
                if Book.Data.Rec_Next = 1 then
                    Book.Data.Rec_Gone := True;
                    return False;
                else
                    Book.Data.Rec_Next := 1;
                    Book.Data.Rec_Cache := False;
                end if;
            end loop;
            if Book.Data.Rec_Cache and Ptr.Rec_Goal.Actual.Counter = 1 then
                Book.Next1.Cache.Data.Append ((1, new State'(Result)));
            end if;
            Book.Data.Rec_Next := Book.Data.Rec_Next + 1;
            return True;
        end case;
    end Do_Get_Next;


    function Get_Next
           (Ptr    : in     Constant_Graph_Access;
            Book   : in out Book_Node_Access;
            Base   : in     State;
            Index  : in     Long_Positive;
            Result :    out State)
        return Boolean is
    begin
        if Ptr = null then
            return False;
        elsif Ptr.Actual = null then
            if Index = 1 then
                Result := Base;
                return True;
            else
                return False;
            end if;
        elsif Book = null then
            Book := Connect_Loose (Ptr.Actual);
        end if;
        if Book /= null and then Book.Cache /= null and then
            Index <= Book.Cache.Data.Last_Index
        then
            Result := Book.Cache.Data (Index).Data.all;
            Book.Cache.Data (Index).Used := Book.Cache.Data (Index).Used + 1;
            if not Book.Cache.Keep and then Book.Cache.Data (Index).Used >= Ptr.Actual.Counter then
                Free (Book.Cache.Data (Index).Data);
            end if;
            return True;
        else
            return Found : constant Boolean :=
                Do_Get_Next (Ptr.Actual, Book, Base, Index, Result)
            do
                if Found and Ptr.Actual.Counter > 1 and Ptr.Actual /= Relation.Graph.Actual then
                    if Book.Cache = null then
                        Book.Cache := new Cache_Entry'(False, State_Vectors.Empty_Vector);
                    end if;
                    pragma Assert (Index = Book.Cache.Data.Last_Index + 1);
                    Book.Cache.Data.Append ((1, new State'(Result)));
                end if;
            end return;
        end if;
    end Get_Next;




    -----------------------
    --  API Subprograms  --
    -----------------------

    function Has_Next
        return Boolean
    is
        Ptr : constant Constant_Graph_Access := Relation.Graph'Access;
    begin
        if State_Valid then
            return True;
        elsif Exhausted then
            return False;
        else
            State_Valid := Get_Next (Ptr, Book_Root, Within, Next_Index, Next_State);
            if not State_Valid then
                Exhausted := True;
            else
                Next_Index := Next_Index + 1;
            end if;
            return State_Valid;
        end if;
    end Has_Next;


    function Next
        return State is
    begin
        if Has_Next then
            State_Valid := False;
            return Next_State;
        else
            raise State_Not_Found_Error;
        end if;
    end Next;


    function Next
           (Default : in State)
        return State is
    begin
        if Has_Next then
            State_Valid := False;
            return Next_State;
        else
            return Default;
        end if;
    end Next;


    procedure Reset is
    begin
        Reset (Relation.Graph.Actual, Book_Root);
        Next_Index  := 1;
        State_Valid := False;
        Exhausted   := False;
    end Reset;


end Kompsos.Collector;