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

--  See license.txt for further details

with

    Ada.Unchecked_Deallocation,
    System.Address_To_Access_Conversions,
    System.Storage_Elements;


package body Kompsos.Collector is


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

    procedure Free is new Ada.Unchecked_Deallocation (World, World_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_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;

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




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

    --  Map Keys  --

    package World_Convert is new System.Address_To_Access_Conversions (World_Component);

    function "<"
           (Left, Right : in World_Component_Access)
        return Boolean
    is
        use System.Storage_Elements;
    begin
        return
            To_Integer (World_Convert.To_Address (World_Convert.Object_Pointer (Left))) <
            To_Integer (World_Convert.To_Address (World_Convert.Object_Pointer (Right)));
    end "<";



    --  Unification  --

    function Fully_Contains
           (This : in State;
            Item : in Term'Class)
        return Boolean is
    begin
        case Item.Kind is
        when Null_Term | Atom_Term =>
            return True;
        when Var_Term =>
            return This.Ident.Contains (Item.Var.Ident);
        when Pair_Term =>
            return Fully_Contains (This, Item.Left) and then Fully_Contains (This, Item.Right);
        end case;
    end Fully_Contains;


    function Walk
           (This : in State;
            Item : in Term'Class)
        return Term'Class is
    begin
        if  Item.Kind = Var_Term and then
            This.Subst.Contains (This.Ident.Element (Item.Var.Ident))
        then
            return Walk (This, This.Subst.Constant_Reference (This.Ident.Element (Item.Var.Ident)));
        else
            return Item;
        end if;
    end Walk;


    function Do_Unify
           (Potential   : in     State;
            Left, Right : in     Term'Class;
            Extended    :    out State)
        return Boolean
    is
        Real_Left  : Term'Class := Left;
        Real_Right : Term'Class := Right;
    begin
        --  Check for Variable validity with respect to State
        if  not Fully_Contains (Potential, Real_Left) or
            not Fully_Contains (Potential, Real_Right)
        then
            return False;
        end if;

        --  Resolve Variable substitution
        if Left.Kind = Var_Term then
            Real_Left := Walk (Potential, Real_Left);
        end if;
        if Right.Kind = Var_Term then
            Real_Right := Walk (Potential, Real_Right);
        end if;

        --  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.Subst.Insert (Extended.Ident.Element (Real_Left.Var.Ident), Term (Real_Right));
            return True;
        end if;
        if Real_Right.Kind = Var_Term then
            Extended := Potential;
            Extended.Subst.Insert (Extended.Ident.Element (Real_Right.Var.Ident), Term (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
            declare
                Middle : State;
            begin
                return Do_Unify (Potential, Real_Left.Left, Real_Right.Left, Middle) and then
                    Do_Unify (Middle, Real_Left.Right, Real_Right.Right, Extended);
            end;
        end if;

        --  Not sure how things get here, but if all else fails
        return False;
    end Do_Unify;



    --  Result Collection --

    function Call_Lazy
           (This : in World;
            Data : in Lazy_Holders.Holder)
        return World
    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_World_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 Static_Node =>
            return;
        when Fresh_Node =>
            Reset (Ptr.Actual.Frs_World'Unchecked_Access);
        when Unify_Node =>
            Book.Exclude (Ptr.Actual);
            Reset (Ptr.Actual.Uni_World'Unchecked_Access);
        when Disjunct_Node =>
            Book.Exclude (Ptr.Actual);
            Reset (Ptr.Actual.Dis_World1'Unchecked_Access);
            Reset (Ptr.Actual.Dis_World2'Unchecked_Access);
        when Conjunct_Node =>
            if Book.Contains (Ptr.Actual) then
                Reset (Constant_World_Access (Book.Element (Ptr.Actual).Con_Part));
                Free (Book (Ptr.Actual).Con_Part);
                Book.Delete (Ptr.Actual);
            end if;
            Reset (Ptr.Actual.Con_World'Unchecked_Access);
        when Recurse_Node =>
            Book.Exclude (Ptr.Actual);
            Reset (Ptr.Actual.Rec_World'Unchecked_Access);
        end case;
    end Reset;


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


    function Do_Get_Next
           (Ptr    : in     World_Component_Access;
            Index  : in     Long_Positive;
            Result :    out State)
        return Boolean is
    begin
        case Ptr.Kind is
        when Static_Node =>
            if Index <= Ptr.Stc_States.Last_Index then
                Result := Ptr.Stc_States (Index);
                return True;
            else
                return False;
            end if;

        when Fresh_Node =>
            if Get_Next (Ptr.Frs_World'Unchecked_Access, Index, Result) then
                Result.LVars.Append (Ptr.Frs_Var.Name);
                Result.Ident.Insert (Ptr.Frs_Var.Ident, Result.LVars.Last_Index);
                return True;
            else
                return False;
            end if;

        when Unify_Node =>
            if not Book.Contains (Ptr) then
                Book.Insert (Ptr, (Kind => Unify_Data, others => <>));
            end if;
            while Get_Next
               (Ptr.Uni_World'Unchecked_Access,
                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_World2'Unchecked_Access,
                    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_World1'Unchecked_Access,
                    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_World1'Unchecked_Access,
                    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_World2'Unchecked_Access,
                        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_World2'Unchecked_Access,
                    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_World1'Unchecked_Access,
                        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 => <>));
            end if;
            if Book (Ptr).Con_Gone then
                return False;
            end if;
            while not Get_Next
               (Constant_World_Access (Book.Element (Ptr).Con_Part),
                Book.Element (Ptr).Con_Next,
                Result)
            loop
                Reset (Constant_World_Access (Book.Element (Ptr).Con_Part));
                Free (Book (Ptr).Con_Part);
                if Get_Next
                   (Ptr.Con_World'Unchecked_Access,
                    Book.Element (Ptr).Con_From,
                    Result)
                then
                    Book (Ptr).Con_Part :=
                        new World'(Call_Lazy (World (Static (Result)), Ptr.Con_Data));
                    Book (Ptr).Con_Next := 1;
                    Book (Ptr).Con_From := Book.Element (Ptr).Con_From + 1;
                else
                    Book (Ptr).Con_Gone := True;
                    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 => <>));
            end if;
            if Book (Ptr).Rec_Gone then
                return False;
            end if;
            while not Get_Next
               (Ptr.Rec_World'Unchecked_Access,
                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;
                end if;
            end loop;
            Book (Ptr).Rec_Next := Book.Element (Ptr).Rec_Next + 1;
            return True;
        end case;
    end Do_Get_Next;


    function Cached
           (Ptr    : in     World_Component_Access;
            Index  : in     Long_Positive;
            Result :    out State)
        return Boolean is
    begin
        if Cache_Memo.Contains (Ptr) and then Index <= Cache_Memo (Ptr).Last_Index then
            Result := Cache_Memo (Ptr) (Index);
            return True;
        else
            return False;
        end if;
    end Cached;


    procedure Cache_This
           (Ptr    : in World_Component_Access;
            Index  : in Long_Positive;
            Result : in State) is
    begin
        if Ptr.Counter > 1 and Ptr.Kind /= Static_Node then
            if not Cache_Memo.Contains (Ptr) then
                Cache_Memo.Insert (Ptr, State_Vectors.Empty_Vector);
            end if;
            pragma Assert (Index = Cache_Memo (Ptr).Last_Index + 1);
            Cache_Memo (Ptr).Append (Result);
        end if;
    end Cache_This;


    function Get_Next
           (Ptr    : in     Constant_World_Access;
            Index  : in     Long_Positive;
            Result :    out State)
        return Boolean is
    begin
        if Ptr = null or else Ptr.Actual = null then
            return False;
        elsif Cached (Ptr.Actual, Index, Result) then
            return True;
        else
            return Found : constant Boolean := Do_Get_Next (Ptr.Actual, Index, Result) do
                if Found then
                    Cache_This (Ptr.Actual, Index, Result);
                end if;
            end return;
        end if;
    end Get_Next;




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

    function Has_Next
        return Boolean
    is
        Ptr : constant Constant_World_Access := Source'Access;
    begin
        if State_Valid then
            return True;
        elsif Exhausted then
            return False;
        else
            State_Valid := Get_Next (Ptr, 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_World_Access := Source'Access;
    begin
        Reset (Ptr);
        Next_Index  := 1;
        State_Valid := False;
        Exhausted   := False;
    end Reset;


end Kompsos.Collector;