From 8508d8b77106a2586b425df687ddb401cbcf779f Mon Sep 17 00:00:00 2001 From: Jedidiah Barber Date: Sat, 17 Jan 2026 15:25:17 +1300 Subject: Removed free logic Variable tracking in States, removed Fresh_Node and Static_Node from Goal graphs --- src/kompsos-collector.adb | 92 ++++++++++++-------------------------------- src/kompsos-collector.ads | 8 +++- src/kompsos-pretty_print.adb | 31 ++------------- src/kompsos.adb | 20 +++------- src/kompsos.ads | 32 ++------------- 5 files changed, 45 insertions(+), 138 deletions(-) (limited to 'src') diff --git a/src/kompsos-collector.adb b/src/kompsos-collector.adb index e8314ff..7ccdb57 100644 --- a/src/kompsos-collector.adb +++ b/src/kompsos-collector.adb @@ -58,32 +58,13 @@ package body Kompsos.Collector is -- Unification -- - function Fully_Contains - (This : in State; - Item : in Term'Class) - return Boolean is + procedure Walk + (This : in State; + Item : in out Term) is begin - case Item.Kind is - when Null_Term | Atom_Term => - return True; - when Var_Term => - return This.LVars.Contains (Item.Var); - 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 (Item.Var) then - return Walk (This, This.Subst.Element (Item.Var)); - else - return Item; - end if; + while Item.Kind = Var_Term and then This.Actual.Contains (Item.Var) loop + Item := This.Actual.Element (Item.Var); + end loop; end Walk; @@ -93,20 +74,12 @@ package body Kompsos.Collector is Extended : out State) return Boolean is - Real_Left : Term'Class := Left; - Real_Right : Term'Class := Right; + Real_Left : Term := Term (Left); + Real_Right : Term := Term (Right); begin - -- Check for Variable validity with respect to State - pragma Assert (Fully_Contains (Potential, Real_Left)); - pragma Assert (Fully_Contains (Potential, Real_Right)); - -- 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; + Walk (Potential, Real_Left); + Walk (Potential, Real_Right); -- Unify equal Variable/Atom/Null Terms if (Real_Left.Kind = Var_Term and then @@ -124,12 +97,12 @@ package body Kompsos.Collector is -- Unify Variable and other Terms by introducing a new substitution if Real_Left.Kind = Var_Term then Extended := Potential; - Extended.Subst.Insert (Real_Left.Var, Term (Real_Right)); + Extended.Actual.Insert (Real_Left.Var, Real_Right); return True; end if; if Real_Right.Kind = Var_Term then Extended := Potential; - Extended.Subst.Insert (Real_Right.Var, Term (Real_Left)); + Extended.Actual.Insert (Real_Right.Var, Real_Left); return True; end if; @@ -139,11 +112,7 @@ package body Kompsos.Collector is Do_Unify (Extended, Real_Left.Right, Real_Right.Right, Extended); end if; - -- Not sure how things get here, but if all else fails - return False; - - exception - when Ada.Assertions.Assertion_Error => + -- Otherwise unification fails return False; end Do_Unify; @@ -179,10 +148,6 @@ package body Kompsos.Collector is Cache_Memo.Exclude (Ptr.Actual); case Ptr.Actual.Kind is - when Static_Node => - return; - when Fresh_Node => - Reset (Ptr.Actual.Frs_Goal'Unchecked_Access); when Unify_Node => Book.Exclude (Ptr.Actual); Reset (Ptr.Actual.Uni_Goal'Unchecked_Access); @@ -221,22 +186,6 @@ package body Kompsos.Collector is return Boolean is begin case Ptr.Kind is - when Static_Node => - if Index = 1 then - Result := Base; - return True; - else - return False; - end if; - - when Fresh_Node => - if Get_Next (Ptr.Frs_Goal'Unchecked_Access, Base, Index, Result) then - Result.LVars.Append (Ptr.Frs_Var); - return True; - else - return False; - end if; - when Unify_Node => if not Book.Contains (Ptr) then Book.Insert (Ptr, (Kind => Unify_Data, others => <>)); @@ -359,6 +308,7 @@ package body Kompsos.Collector is Result) loop Reset (Constant_Goal_Access (Book.Element (Ptr).Con_Part)); + Book (Ptr).Con_From := Book.Element (Ptr).Con_From + 1; if Get_Next (Ptr.Con_Goal'Unchecked_Access, Base, @@ -367,7 +317,6 @@ package body Kompsos.Collector is then Book (Ptr).Con_Base.all := Result; Book (Ptr).Con_Next := 1; - Book (Ptr).Con_From := Book.Element (Ptr).Con_From + 1; else Book (Ptr).Con_Gone := True; Free (Book (Ptr).Con_Part); @@ -382,7 +331,7 @@ package body Kompsos.Collector is if not Book.Contains (Ptr) then Book.Insert (Ptr, (Kind => Recurse_Data, others => <>)); if Ptr.Rec_Goal.Actual = null then - Book (Ptr).Rec_Gone := True; + Book (Ptr).Rec_Cache := False; elsif not Cache_Memo.Contains (Ptr.Rec_Goal.Actual) then Cache_Memo.Insert (Ptr.Rec_Goal.Actual, State_Vectors.Empty_Vector); end if; @@ -420,8 +369,15 @@ package body Kompsos.Collector is Result : out State) return Boolean is begin - if Ptr = null or else Ptr.Actual = null then + if Ptr = null then return False; + elsif Ptr.Actual = null then + if Index = 1 then + Result := Base; + return True; + else + return False; + end if; elsif Cache_Memo.Contains (Ptr.Actual) and then Index <= Cache_Memo (Ptr.Actual).Last_Index then @@ -429,7 +385,7 @@ package body Kompsos.Collector is return True; else return Found : constant Boolean := Do_Get_Next (Ptr.Actual, Base, Index, Result) do - if Found and Ptr.Actual.Counter > 1 and Ptr.Actual.Kind /= Static_Node then + if Found and Ptr.Actual.Counter > 1 then if not Cache_Memo.Contains (Ptr.Actual) then Cache_Memo.Insert (Ptr.Actual, State_Vectors.Empty_Vector); end if; diff --git a/src/kompsos-collector.ads b/src/kompsos-collector.ads index cbe8dd7..4ee9402 100644 --- a/src/kompsos-collector.ads +++ b/src/kompsos-collector.ads @@ -61,7 +61,7 @@ private Dis_Gone1 : Boolean := False; Dis_Gone2 : Boolean := False; when Conjunct_Data => - Con_From : Long_Positive := 2; -- Number one will be obtained by Get_Next already + Con_From : Long_Positive := 1; Con_Base : State_Access := null; Con_Part : Goal_Access := null; Con_Next : Long_Positive := 1; @@ -84,6 +84,12 @@ private overriding procedure Finalize (This : in out Managed_Map); + + + package State_Vectors is new Ada.Containers.Vectors + (Index_Type => Long_Positive, + Element_Type => State); + package Cache_Maps is new Ada.Containers.Ordered_Maps (Key_Type => Goal_Component_Access, Element_Type => State_Vectors.Vector, diff --git a/src/kompsos-pretty_print.adb b/src/kompsos-pretty_print.adb index c888e13..3171164 100644 --- a/src/kompsos-pretty_print.adb +++ b/src/kompsos-pretty_print.adb @@ -94,22 +94,11 @@ package body Kompsos.Pretty_Print is is Result : SU.Unbounded_String; begin - SU.Append (Result, Latin.HT & "Variables:"); - if Item.LVars.Is_Empty then - SU.Append (Result, " N/A" & Latin.LF); + if Item.Actual.Is_Empty then + SU.Append (Result, Latin.HT & "N/A" & Latin.LF); else - SU.Append (Result, Latin.LF); - for LVar of Item.LVars loop - SU.Append (Result, Latin.HT & Latin.HT & Image (LVar) & Latin.LF); - end loop; - end if; - SU.Append (Result, Latin.HT & "Substitution:"); - if Item.Subst.Is_Empty then - SU.Append (Result, " N/A" & Latin.LF); - else - SU.Append (Result, Latin.LF); - for Iter in Item.Subst.Iterate loop - SU.Append (Result, Latin.HT & Latin.HT & + for Iter in Item.Actual.Iterate loop + SU.Append (Result, Latin.HT & Image (Binding_Maps.Key (Iter)) & " => " & Image (Binding_Maps.Element (Iter)) & Latin.LF); end loop; @@ -175,18 +164,6 @@ package body Kompsos.Pretty_Print is Nodes.Insert (This.Actual, Next); Next := Next + 1; case This.Actual.Kind is - when Static_Node => - SU.Append (Result, Latin.HT & - "n" & Image (Nodes.Element (This.Actual)) & " [label=""static""];" & Latin.LF); - when Fresh_Node => - SU.Append (Result, Latin.HT & - "n" & Image (Nodes.Element (This.Actual)) & " [label=""fresh""];" & Latin.LF); - Do_Structure_DOT (This.Actual.Frs_Goal, Nodes, Next, Result); - if Nodes.Contains (This.Actual.Frs_Goal.Actual) then - SU.Append (Result, Latin.HT & - "n" & Image (Nodes.Element (This.Actual)) & " -> " & - "n" & Image (Nodes.Element (This.Actual.Frs_Goal.Actual)) & ";" & Latin.LF); - end if; when Unify_Node => SU.Append (Result, Latin.HT & "n" & Image (Nodes.Element (This.Actual)) & " [label=""unify""];" & Latin.LF); diff --git a/src/kompsos.adb b/src/kompsos.adb index 7054714..080683b 100644 --- a/src/kompsos.adb +++ b/src/kompsos.adb @@ -254,17 +254,9 @@ package body Kompsos is function Fresh (This : in out Goal'Class) - return Term - is - My_Var : constant Variable := Next_Gen; + return Term is begin - return My_Term : constant Term := Term (T (My_Var)) do - This.Actual := new Goal_Component'( - (Kind => Fresh_Node, - Counter => 1, - Frs_Goal => Goal (This), - Frs_Var => My_Var)); - end return; + return Term (T (Next_Gen)); end Fresh; @@ -557,8 +549,8 @@ package body Kompsos is when Null_Term | Atom_Term => return This; when Var_Term => - if Subst.LVars.Contains (This.Var) and then Subst.Subst.Contains (This.Var) then - return Subst.Subst.Element (This.Var).Resolve (Subst); + if Subst.Actual.Contains (This.Var) then + return Subst.Actual.Element (This.Var).Resolve (Subst); else return This; end if; @@ -572,10 +564,10 @@ package body Kompsos is (Subst : in State) return Term is begin - if Subst.LVars.Is_Empty then + if Subst.Actual.Is_Empty then return Empty_Term; else - return Resolve (Term (T (Subst.LVars.First_Element)), Subst); + return Subst.Actual.First_Element.Resolve (Subst); end if; end Resolve_First; diff --git a/src/kompsos.ads b/src/kompsos.ads index 19cfeb8..32cfc24 100644 --- a/src/kompsos.ads +++ b/src/kompsos.ads @@ -415,7 +415,6 @@ private - type Term_Component; type Term_Component_Access is access Term_Component; @@ -464,28 +463,15 @@ private - - package Variable_Vectors is new Ada.Containers.Vectors - (Index_Type => Long_Positive, - Element_Type => Variable); - package Binding_Maps is new Ada.Containers.Ordered_Maps (Key_Type => Variable, Element_Type => Term); type State is record - LVars : Variable_Vectors.Vector; - Subst : Binding_Maps.Map; + Actual : Binding_Maps.Map; end record; - package State_Vectors is new Ada.Containers.Vectors - (Index_Type => Long_Positive, - Element_Type => State); - - Empty_State : constant State := - (LVars => Variable_Vectors.Empty_Vector, - Subst => Binding_Maps.Empty_Map); - + Empty_State : constant State := (Actual => Binding_Maps.Empty_Map); @@ -515,9 +501,7 @@ private package Lazy_Holders is new Ada.Containers.Indefinite_Holders (Lazy_Data); type Node_Kind is - (Static_Node, - Fresh_Node, - Unify_Node, + (Unify_Node, Disjunct_Node, Conjunct_Node, Recurse_Node); @@ -525,11 +509,6 @@ private type Goal_Component (Kind : Node_Kind) is limited record Counter : Natural; case Kind is - when Static_Node => - null; - when Fresh_Node => - Frs_Goal : aliased Goal; - Frs_Var : Variable; when Unify_Node => Uni_Goal : aliased Goal; Uni_Term1 : Term; @@ -558,10 +537,7 @@ private overriding procedure Finalize (This : in out Goal); - Empty_Goal : constant Goal := (Ada.Finalization.Controlled with - Actual => new Goal_Component'( - (Kind => Static_Node, - Counter => 1))); + Empty_Goal : constant Goal := (Ada.Finalization.Controlled with Actual => null); end Kompsos; -- cgit