diff options
Diffstat (limited to 'src/kompsos-collector.adb')
| -rw-r--r-- | src/kompsos-collector.adb | 526 |
1 files changed, 526 insertions, 0 deletions
diff --git a/src/kompsos-collector.adb b/src/kompsos-collector.adb new file mode 100644 index 0000000..16e2b1f --- /dev/null +++ b/src/kompsos-collector.adb @@ -0,0 +1,526 @@ + + +-- 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; + + |