path: root/src/kompsos-collector.adb

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

--  See license.txt for further details


with

    Ada.Containers,
    Ada.Unchecked_Deallocation;


package body Kompsos.Collector is


    ---------------------
    --  Progress Info  --
    ---------------------

    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;
    Walk_Choices : Choice_Vector;
    Location     : Graph_Component_Access;
    Local_Cursor : Upwards_Maps.Cursor;
    Next_Pick    : Positive;

    Conjunct_Count : Natural := 0;
    Conjunct_Limit : Positive := Initial_Depth_Limit;
    Already_Done   : Choice_Vector_Vectors.Vector;

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

    --  Compares two sparsely encoded binary numbers
    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 "<";




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

    --  Unification  --

    procedure Walk_State
           (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_State;


    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_State (Subst, Real_Left);
        Walk_State (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
        --  Remove the no longer needed edge leading to the Conjunct node
        Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents.Delete (Next_Pick);

        --  Expand out the Conjunct
        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
            --  Declare needed to avoid Tampering issues
            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;

        --  Join the top of the expanded subgraph up to whatever the Conjunct was joined to
        if Up_Map.Contains (Node) then
            Up_Map.Insert (Conjunct_Goals.Last_Element.Graph.Actual, Up_Map.Element (Node));
        end if;
    end Expand_Conjunct;



    --  Upwards Iterative Deepening Depth First Search  --

    procedure Reset_Position is
    begin
        Conjunct_Count := 0;
        Conjunct_Limit := Conjunct_Limit * 2;
        Walk_Trail.Clear;
        Walk_Choices.Clear;
        Location := null;
        Local_Cursor := Up_Map.Find (Location);
        Next_Pick := 1;
        Truncate (Result, Long_Natural (Within.Binds.Length));
    end Reset_Position;


    function Choose_Another_Way
        return Boolean
    is
        Marker : Natural := Walk_Trail.Last_Index;
        Crumb  : Breadcrumb;
        Option : Positive;
    begin
        --  Backtrack until a choice point with unexplored branches is found
        while Marker /= Breadcrumb_Vectors.No_Index loop
            Crumb := Walk_Trail (Marker);
            Option := Walk_Choices (Marker);
            Location := Crumb.Choice_Node;
            Local_Cursor := Up_Map.Find (Location);
            if Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents.Last_Index >= Option + 1 then
                Next_Pick := Option + 1;
                Truncate (Result, Crumb.State_Size);
                Walk_Trail.Set_Length (Ada.Containers.Count_Type (Marker - 1));
                Walk_Choices.Set_Length (Ada.Containers.Count_Type (Marker - 1));
                return True;  --  Backtracking success
            else
                Marker := Marker - 1;
            end if;
        end loop;
        return False;  --  Backtracking failure, nothing further available
    end Choose_Another_Way;


    procedure Walk_Graph is
        use type Upwards_Maps.Cursor;
        Ptr : Graph_Component_Access;
    begin
        loop
            --  Make sure current State passes unification
            if Location = null or else Location.Kind /= Unify_Node or else
                Do_Unify (Result, Location.Uni_Term1, Location.Uni_Term2)
            then

                --  Have we reached the top of the Graph?
                if Local_Cursor = Upwards_Maps.No_Element then
                    if not Already_Done.Contains (Walk_Choices) then
                        Already_Done.Append (Walk_Choices);
                        State_Valid := True;
                        return;
                    elsif not Choose_Another_Way then
                        if Conjunct_Count >= Conjunct_Limit then
                            Reset_Position;
                        else
                            State_Valid := False;
                            Exhausted := True;
                            return;
                        end if;
                    end if;
                end if;

                --  If next node is a Conjunct then expand as necessary until the current limit
                loop
                    Ptr := Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents (Next_Pick).Node;
                    exit when Ptr.Kind /= Conjunct_Node;
                    if Conjunct_Count >= Conjunct_Limit then
                        if not Choose_Another_Way then
                            Reset_Position;
                        end if;
                    else
                        Expand_Conjunct (Ptr);
                        Conjunct_Count := Conjunct_Count + 1;
                    end if;
                end loop;

                --  Keep a trail for backtracking
                if Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents.Last_Index > 1 then
                    Walk_Trail.Append ((Location, Result.Binds.Last_Index));
                    Walk_Choices.Append (Next_Pick);
                end if;

                --  Move up a node
                Location := Up_Vector
                    (Upwards_Maps.Element (Local_Cursor)).Parents (Next_Pick).Node;
                Local_Cursor := Up_Map.Find (Location);
                Next_Pick := 1;
            else

                --  If unification fails then backtrack if possible,
                --  or otherwise reset if the Graph isn't exhausted
                if not Choose_Another_Way then
                    if Conjunct_Count > 0 then
                        Reset_Position;
                    else
                        State_Valid := False;
                        Exhausted := True;
                        return;
                    end if;
                end if;
            end if;
        end loop;
    end Walk_Graph;


    procedure Continue_Walk is
    begin
        if Choose_Another_Way then
            Walk_Graph;
        elsif Conjunct_Count >= Conjunct_Limit then
            Reset_Position;
            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
        --  Declare needed because this parameter must be a variable
        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;