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

--  See license.txt for further details


with

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


package body Kompsos.Collector is


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

    Conjunct_Goals : Goal_Access_Vectors.Vector;

    Global_Var : Variable := Relation.Next_Var;

    Up_Map    : Upwards_Maps.Map;
    Up_Vector : Upwards_Vectors.Vector;

    Do_Walk      : access procedure;
    Walk_Trail   : Breadcrumb_Vectors.Vector;
    Location     : Graph_Component_Access;
    Local_Cursor : Upwards_Maps.Cursor;
    Next_Pick    : Positive;

    Result      : State   := Within;
    State_Valid : Boolean := False;
    Exhausted   : Boolean := False;




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

    procedure Free is new Ada.Unchecked_Deallocation (Goal, Goal_Access);


    procedure Finalize
           (This : in out Collector_Final_Controller) is
    begin
        for Ptr of Conjunct_Goals loop
            Free (Ptr);
        end loop;
    end Finalize;




    -----------------
    --  Datatypes  --
    -----------------

    function "<"
           (Left, Right : in Disjuncts_Chosen)
        return Boolean is
    begin
        if Left.Is_Empty then
            return not Right.Is_Empty;
        elsif Right.Is_Empty then
            return False;
        end if;
        declare
            Left_Spot  : Natural := Left.Last_Index;
            Right_Spot : Natural := Right.Last_Index;
        begin
            loop
                if Left (Left_Spot) < Right (Right_Spot) then
                    return True;
                elsif Left (Left_Spot) = Right (Right_Spot) then
                    Left_Spot := Left_Spot - 1;
                    Right_Spot := Right_Spot - 1;
                    if Left_Spot = 0 then
                        return Right_Spot /= 0;
                    elsif Right_Spot = 0 then
                        return False;
                    end if;
                else
                    return False;
                end if;
            end loop;
        end;
    end "<";


    function "<"
           (Left, Right : in Parent_Arrow)
        return Boolean is
    begin
        return Left.Order < Right.Order;
    end "<";


    package Graph_Comp_Conv is new System.Address_To_Access_Conversions (Graph_Component);

    function Graph_Component_Access_Hash
           (Key : in Graph_Component_Access)
        return Ada.Containers.Hash_Type
    is
        use Ada.Containers, Graph_Comp_Conv, System.Storage_Elements;
    begin
        return Hash_Type (To_Integer (To_Address (Object_Pointer (Key))) mod Hash_Type'Modulus);
    end Graph_Component_Access_Hash;




    ------------------------
    --  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
           (Subst       : in out State;
            Left, Right : in     Term'Class)
        return Boolean
    is
        Real_Left  : Term := Term (Left);
        Real_Right : Term := Term (Right);
    begin
        --  Resolve Variable substitution
        Walk (Subst, Real_Left);
        Walk (Subst, 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
            return True;
        end if;

        --  Unify Variable and other Terms by introducing a new substitution
        if Real_Left.Kind = Var_Term then
            Insert (Subst, Real_Left.Var, Real_Right);
            return True;
        end if;
        if Real_Right.Kind = Var_Term then
            Insert (Subst, 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 (Subst, Real_Left.Left, Real_Right.Left) and then
                Do_Unify (Subst, Real_Left.Right, Real_Right.Right);
        end if;

        --  Otherwise unification fails
        return False;
    end Do_Unify;



    --  Interleaved Graph Inversion  --

    function Null_Join
           (Left, Right : in Graph_Component_Access)
        return Graph_Component_Access is
    begin
        return (if Left = null then Right else Left);
    end Null_Join;


    procedure Sorted_Insert
           (Quiver : in out Parent_Arrow_Vectors.Vector;
            Arrow  : in     Parent_Arrow)
    is
        Position : Parent_Arrow_Vectors.Extended_Index := Quiver.Last_Index + 1;
    begin
        while Position > 1 and then Arrow < Quiver (Position - 1) loop
            Position := Position - 1;
        end loop;
        Quiver.Insert (Position, Arrow);
    end Sorted_Insert;


    function Connect_Up_Map
           (Parent, Child : in Graph_Component_Access;
            Level         : in Disjuncts_Passed;
            Choices       : in Disjuncts_Chosen)
        return Boolean
    is
        use type Upwards_Maps.Cursor, Parent_Arrow_Vectors.Vector;
        Index_Cursor : constant Upwards_Maps.Cursor := Up_Map.Find (Child);
    begin
        if Index_Cursor = Upwards_Maps.No_Element then
            Up_Vector.Append ((Level, Parent_Arrow_Vectors.Empty_Vector & (Parent, Choices)));
            Up_Map.Insert (Child, Up_Vector.Last_Index);
            return True;
        else
            Sorted_Insert
               (Up_Vector (Upwards_Maps.Element (Index_Cursor)).Parents,
                (Parent, Choices));
            return False;
        end if;
    end Connect_Up_Map;


    procedure Build_Up_Map
           (Top, Bottom : in     Graph_Component_Access;
            Level       : in     Disjuncts_Passed;
            Choices     : in out Disjuncts_Chosen) is
    begin
        if Top = null then
            return;
        end if;
        case Top.Kind is
        when Unify_Node =>
            if Connect_Up_Map (Top, Null_Join (Top.Uni_Goal.Actual, Bottom), Level, Choices) then
                Build_Up_Map (Top.Uni_Goal.Actual, Bottom, Level, Choices);
            end if;
        when Disjunct_Node =>
            if Connect_Up_Map (Top, Null_Join (Top.Dis_Goal1.Actual, Bottom), Level + 1, Choices)
            then
                Build_Up_Map (Top.Dis_Goal1.Actual, Bottom, Level + 1, Choices);
            end if;
            Choices.Append (Level + 1);
            if Connect_Up_Map (Top, Null_Join (Top.Dis_Goal2.Actual, Bottom), Level + 1, Choices)
            then
                Build_Up_Map (Top.Dis_Goal2.Actual, Bottom, Level + 1, Choices);
            end if;
            Choices.Delete_Last;
        when Conjunct_Node =>
            if Connect_Up_Map (Top, Null_Join (Top.Con_Goal.Actual, Bottom), Level, Choices) then
                Build_Up_Map (Top.Con_Goal.Actual, Bottom, Level, Choices);
            end if;
        end case;
    end Build_Up_Map;



    --  Conjunct Expansion  --

    function Call_Lazy
           (This : in Goal;
            Data : in Lazy_Data)
        return Goal is
    begin
        case Data.Kind is
        when Zero_Arg =>
            return Data.ZFunc (This);
        when One_Arg  =>
            return Data.OFunc (This, Data.OInput);
        when Many_Arg =>
            return Data.MFunc (This, Data.MInput.all);
        end case;
    end Call_Lazy;


    procedure Expand_Conjunct
           (Node : in Graph_Component_Access)
    is
        Old_Choices : Disjuncts_Chosen :=
            Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents (Next_Pick).Order;
    begin
        Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents.Delete (Next_Pick);
        Conjunct_Goals.Append (new Goal'(
            Call_Lazy
               ((Graph    => (Ada.Finalization.Controlled with Actual => null),
                 Next_Var => Global_Var),
                Node.Con_Data.all)));
        Global_Var := Conjunct_Goals.Last_Element.Next_Var;
        declare
            Depth : constant Disjuncts_Passed :=
                Up_Vector (Upwards_Maps.Element (Local_Cursor)).Depth;
        begin
            Build_Up_Map (Conjunct_Goals.Last_Element.Graph.Actual, Location, Depth, Old_Choices);
        end;
        Up_Map.Insert (Conjunct_Goals.Last_Element.Graph.Actual, Up_Map.Element (Node));
    end Expand_Conjunct;



    --  Upwards Depth First Search  --

    function Choose_Another_Way
        return Boolean
    is
        Marker : Natural := Walk_Trail.Last_Index;
        Crumb : Breadcrumb;
    begin
        while Marker /= Breadcrumb_Vectors.No_Index loop
            Crumb := Walk_Trail (Marker);
            Location := Crumb.Choice_Node;
            Local_Cursor := Up_Map.Find (Location);
            if Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents.Last_Index >=
                Crumb.Option + 1
            then
                Next_Pick := Crumb.Option + 1;
                Truncate (Result, Crumb.State_Size);
                Walk_Trail.Set_Length (Ada.Containers.Count_Type (Marker - 1));
                return True;
            else
                Marker := Marker - 1;
            end if;
        end loop;
        return False;
    end Choose_Another_Way;


    procedure Walk_Graph is
        use type Upwards_Maps.Cursor;
        Ptr : Graph_Component_Access;
    begin
        loop
            if Location = null or else Location.Kind /= Unify_Node or else
                Do_Unify (Result, Location.Uni_Term1, Location.Uni_Term2)
            then
                if Local_Cursor = Upwards_Maps.No_Element then
                    State_Valid := True;
                    return;
                end if;
                Ptr := Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents (Next_Pick).Node;
                if Ptr.Kind = Conjunct_Node then
                    Expand_Conjunct (Ptr);
                end if;
                if Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents.Last_Index > 1 then
                    Walk_Trail.Append ((Location, Next_Pick, Result.Binds.Last_Index));
                end if;
                Location := Up_Vector
                    (Upwards_Maps.Element (Local_Cursor)).Parents (Next_Pick).Node;
                Local_Cursor := Up_Map.Find (Location);
                Next_Pick := 1;
            else
                if not Choose_Another_Way then
                    State_Valid := False;
                    Exhausted := True;
                    return;
                end if;
            end if;
        end loop;
    end Walk_Graph;


    procedure Continue_Walk is
    begin
        if Choose_Another_Way then
            Walk_Graph;
        else
            State_Valid := False;
            Exhausted := True;
        end if;
    end Continue_Walk;


    procedure Start_Walk is
        use type Upwards_Maps.Cursor;
    begin
        Location := null;
        Local_Cursor := Up_Map.Find (Location);
        if Local_Cursor = Upwards_Maps.No_Element then
            State_Valid := True;
            Exhausted := True;
        else
            Do_Walk := Continue_Walk'Access;
            Next_Pick := 1;
            Walk_Graph;
        end if;
    end Start_Walk;




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

    function Has_Next
        return Boolean is
    begin
        if State_Valid then
            return True;
        elsif Exhausted then
            return False;
        else
            Do_Walk.all;
            return State_Valid;
        end if;
    end Has_Next;


    function Next
        return State is
    begin
        if Has_Next then
            State_Valid := False;
            return Result;
        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 Result;
        else
            return Default;
        end if;
    end Next;




begin

    declare
        Temp : Positive_Vectors.Vector := Positive_Vectors.Empty_Vector;
    begin
        Build_Up_Map (Relation.Graph.Actual, null, 0, Temp);
    end;
    Do_Walk := Start_Walk'Access;

end Kompsos.Collector;