--  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


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

    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 Managed_Map) is
    begin
        for Datum of This.Actual loop
            if Datum.Kind = Conjunct_Data then
                Free (Datum.Con_Base);
                Free (Datum.Con_Part);
            end if;
        end loop;
    end Finalize;




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

    Cache_Memo : Cache_Maps.Map := Cache_Maps.Empty_Map;
    Bookkeep   : Managed_Map    := (Ada.Finalization.Controlled with Actual => Eval_Maps.Empty_Map);

    Book : Eval_Maps.Map renames Bookkeep.Actual;

    Global_Var : Variable := Relation.Next_Var;

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




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

    --  Unification  --

    procedure Walk
           (This : in     State;
            Item : in out Term) is
    begin
        while Item.Kind = Var_Term and then This.Actual.Contains (Item.Var) loop
            Item := This.Actual.Element (Item.Var);
        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 := Potential;
            Extended.Actual.Insert (Real_Left.Var, Real_Right);
            return True;
        end if;
        if Real_Right.Kind = Var_Term then
            Extended := Potential;
            Extended.Actual.Insert (Real_Right.Var, Real_Left);
            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 Reset
           (Ptr : in Constant_Goal_Access);


    procedure Do_Reset
           (Ptr : in Constant_Graph_Access) is
    begin
        if Ptr = null or else Ptr.Actual = null then
            return;
        end if;

        Cache_Memo.Exclude (Ptr.Actual);

        case Ptr.Actual.Kind is
        when Unify_Node =>
            Book.Exclude (Ptr.Actual);
            Do_Reset (Ptr.Actual.Uni_Goal'Unchecked_Access);
        when Disjunct_Node =>
            Book.Exclude (Ptr.Actual);
            Do_Reset (Ptr.Actual.Dis_Goal1'Unchecked_Access);
            Do_Reset (Ptr.Actual.Dis_Goal2'Unchecked_Access);
        when Conjunct_Node =>
            if Book.Contains (Ptr.Actual) then
                Reset (Constant_Goal_Access (Book.Element (Ptr.Actual).Con_Part));
                Free (Book (Ptr.Actual).Con_Part);
                Free (Book (Ptr.Actual).Con_Base);
                Book.Delete (Ptr.Actual);
            end if;
            Do_Reset (Ptr.Actual.Con_Goal'Unchecked_Access);
        when Recurse_Node =>
            Book.Exclude (Ptr.Actual);
            Do_Reset (Ptr.Actual.Rec_Goal'Unchecked_Access);
        end case;
    end Do_Reset;


    procedure Reset
           (Ptr : in Constant_Goal_Access) is
    begin
        if Ptr = null then
            return;
        else
            Do_Reset (Ptr.Graph'Access);
        end if;
    end Reset;


    function Get_Next
           (Ptr    : in     Constant_Graph_Access;
            Base   : in     State;
            Index  : in     Long_Positive;
            Result :    out State)
        return Boolean;


    function Do_Get_Next
           (Ptr    : in     Graph_Component_Access;
            Base   : in     State;
            Index  : in     Long_Positive;
            Result :    out State)
        return Boolean is
    begin
        case Ptr.Kind is
        when Unify_Node =>
            if not Book.Contains (Ptr) then
                Book.Insert (Ptr, (Kind => Unify_Data, others => <>));
            end if;
            while Get_Next
               (Ptr.Uni_Goal'Unchecked_Access,
                Base,
                Index + Book.Element (Ptr).Uni_Offset,
                Result)
            loop
                if Do_Unify (Result, Ptr.Uni_Term1, Ptr.Uni_Term2, Result) then
                    return True;
                else
                    Book (Ptr).Uni_Offset := Book.Element (Ptr).Uni_Offset + 1;
                end if;
            end loop;
            return False;

        when Disjunct_Node =>
            if not Book.Contains (Ptr) then
                Book.Insert (Ptr, (Kind => Disjunct_Data, others => <>));
            end if;
            if Book.Element (Ptr).Dis_Gone1 then
                if Book.Element (Ptr).Dis_Gone2 then
                    return False;
                elsif Get_Next
                   (Ptr.Dis_Goal2'Unchecked_Access,
                    Base,
                    Book.Element (Ptr).Dis_Next2,
                    Result)
                then
                    Book (Ptr).Dis_Next2 := Book.Element (Ptr).Dis_Next2 + 1;
                    return True;
                else
                    Book (Ptr).Dis_Gone2 := True;
                    return False;
                end if;
            elsif Book.Element (Ptr).Dis_Gone2 then
                if Get_Next
                   (Ptr.Dis_Goal1'Unchecked_Access,
                    Base,
                    Book.Element (Ptr).Dis_Next1,
                    Result)
                then
                    Book (Ptr).Dis_Next1 := Book.Element (Ptr).Dis_Next1 + 1;
                    return True;
                else
                    Book (Ptr).Dis_Gone1 := True;
                    return False;
                end if;
            elsif Book.Element (Ptr).Dis_Flag then
                if Get_Next
                   (Ptr.Dis_Goal1'Unchecked_Access,
                    Base,
                    Book.Element (Ptr).Dis_Next1,
                    Result)
                then
                    Book (Ptr).Dis_Next1 := Book.Element (Ptr).Dis_Next1 + 1;
                    Book (Ptr).Dis_Flag := not Book.Element (Ptr).Dis_Flag;
                    return True;
                else
                    Book (Ptr).Dis_Gone1 := True;
                    if Get_Next
                       (Ptr.Dis_Goal2'Unchecked_Access,
                        Base,
                        Book.Element (Ptr).Dis_Next2,
                        Result)
                    then
                        Book (Ptr).Dis_Next2 := Book.Element (Ptr).Dis_Next2 + 1;
                        return True;
                    else
                        Book (Ptr).Dis_Gone2 := True;
                        return False;
                    end if;
                end if;
            else
                if Get_Next
                   (Ptr.Dis_Goal2'Unchecked_Access,
                    Base,
                    Book.Element (Ptr).Dis_Next2,
                    Result)
                then
                    Book (Ptr).Dis_Next2 := Book.Element (Ptr).Dis_Next2 + 1;
                    Book (Ptr).Dis_Flag := not Book.Element (Ptr).Dis_Flag;
                    return True;
                else
                    Book (Ptr).Dis_Gone2 := True;
                    if Get_Next
                       (Ptr.Dis_Goal1'Unchecked_Access,
                        Base,
                        Book.Element (Ptr).Dis_Next1,
                        Result)
                    then
                        Book (Ptr).Dis_Next1 := Book.Element (Ptr).Dis_Next1 + 1;
                        return True;
                    else
                        Book (Ptr).Dis_Gone1 := True;
                        return False;
                    end if;
                end if;
            end if;

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

        when Recurse_Node =>
            if not Book.Contains (Ptr) then
                Book.Insert (Ptr, (Kind => Recurse_Data, others => <>));
                if Ptr.Rec_Goal.Actual = null then
                    Book (Ptr).Rec_Cache := False;
                elsif not Cache_Memo.Contains (Ptr.Rec_Goal.Actual) then
                    Cache_Memo.Insert (Ptr.Rec_Goal.Actual, State_Vectors.Empty_Vector);
                end if;
            end if;
            if Book (Ptr).Rec_Gone then
                return False;
            end if;
            while not Get_Next
               (Ptr.Rec_Goal'Unchecked_Access,
                Base,
                Book.Element (Ptr).Rec_Next,
                Result)
            loop
                if Book.Element (Ptr).Rec_Next = 1 then
                    Book (Ptr).Rec_Gone := True;
                    return False;
                else
                    Book (Ptr).Rec_Next := 1;
                    Book (Ptr).Rec_Cache := False;
                end if;
            end loop;
            if Book (Ptr).Rec_Cache and Ptr.Rec_Goal.Actual.Counter = 1 then
                Cache_Memo (Ptr.Rec_Goal.Actual).Append (Result);
            end if;
            Book (Ptr).Rec_Next := Book.Element (Ptr).Rec_Next + 1;
            return True;
        end case;
    end Do_Get_Next;


    function Get_Next
           (Ptr    : in     Constant_Graph_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 Cache_Memo.Contains (Ptr.Actual) and then
            Index <= Cache_Memo (Ptr.Actual).Last_Index
        then
            Result := Cache_Memo (Ptr.Actual) (Index);
            return True;
        else
            return Found : constant Boolean := Do_Get_Next (Ptr.Actual, Base, Index, Result) do
                if Found and Ptr.Actual.Counter > 1 then
                    if not Cache_Memo.Contains (Ptr.Actual) then
                        Cache_Memo.Insert (Ptr.Actual, State_Vectors.Empty_Vector);
                    end if;
                    pragma Assert (Index = Cache_Memo (Ptr.Actual).Last_Index + 1);
                    Cache_Memo (Ptr.Actual).Append (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, 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
        Ptr : constant Constant_Goal_Access := Relation'Access;
    begin
        Reset (Ptr);
        Next_Index  := 1;
        State_Valid := False;
        Exhausted   := False;
    end Reset;


end Kompsos.Collector;