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