From 203222f4ffbdaf23a30ab390a7ad765cfef0c008 Mon Sep 17 00:00:00 2001 From: Jedidiah Barber Date: Sun, 16 Nov 2025 20:09:18 +1300 Subject: Variable counting handled properly on a per-State basis --- src/kompsos-pretty_print.adb | 44 ++++++++--- src/kompsos-pretty_print.ads | 11 ++- src/kompsos.adb | 169 ++++++++++++++++++------------------------- src/kompsos.ads | 60 +++++++++------ 4 files changed, 149 insertions(+), 135 deletions(-) (limited to 'src') diff --git a/src/kompsos-pretty_print.adb b/src/kompsos-pretty_print.adb index 8739af8..772c0cd 100644 --- a/src/kompsos-pretty_print.adb +++ b/src/kompsos-pretty_print.adb @@ -45,7 +45,7 @@ package body Kompsos.Pretty_Print is (Item : in Variable) return String is begin - return "Var#" & Image (Item.Ident) & + return "Vargen#" & Image (ID_Number (Item.Ident)) & (if SU.Length (Item.Name) /= 0 then "/" & SU.To_String (Item.Name) else ""); @@ -95,16 +95,29 @@ package body Kompsos.Pretty_Print is return String is Result : SU.Unbounded_String; - My_Var : Variable; begin + SU.Append (Result, Latin.HT & "Generation:"); + if Item.Ident.Is_Empty then + SU.Append (Result, " N/A" & Latin.LF); + else + SU.Append (Result, Latin.LF); + for Iter in Item.Ident.Iterate loop + SU.Append (Result, Latin.HT & Latin.HT & "Vargen#" & + Image (ID_Number (ID_Number_Maps.Key (Iter))) & " => " & + Image (ID_Number (ID_Number_Maps.Element (Iter))) & Latin.LF); + end loop; + end if; SU.Append (Result, Latin.HT & "Variables:"); if Item.LVars.Is_Empty then SU.Append (Result, " N/A" & Latin.LF); else SU.Append (Result, Latin.LF); - for Iter in Item.LVars.Iterate loop - My_Var := (Ident => Name_Maps.Key (Iter), Name => Name_Maps.Element (Iter)); - SU.Append (Result, Latin.HT & Latin.HT & Image (My_Var) & Latin.LF); + for Index in Item.LVars.First_Index .. Item.LVars.Last_Index loop + SU.Append (Result, Latin.HT & Latin.HT & + "Var#" & Image (ID_Number (Index)) & + (if SU.Length (Item.LVars (Index)) /= 0 + then "/" & SU.To_String (Item.LVars (Index)) + else "") & Latin.LF); end loop; end if; SU.Append (Result, Latin.HT & "Substitution:"); @@ -114,7 +127,7 @@ package body Kompsos.Pretty_Print is SU.Append (Result, Latin.LF); for Iter in Item.Subst.Iterate loop SU.Append (Result, Latin.HT & Latin.HT & - Image (Binding_Maps.Key (Iter)) & " => " & + Image (ID_Number (Binding_Maps.Key (Iter))) & " => " & Image (Binding_Maps.Element (Iter)) & Latin.LF); end loop; end if; @@ -125,26 +138,35 @@ package body Kompsos.Pretty_Print is function Image - (Item : in World) + (Item : in out World) return String is Result : SU.Unbounded_String; - Scratch : World := Item; Counter : Positive := 1; begin - if not Scratch.Has_State (Counter) then + if not Item.Has_State (Counter) then return "States: N/A" & Latin.LF; end if; loop SU.Append (Result, "State#" & Image (Counter) & ":" & Latin.LF); - SU.Append (Result, Image (Scratch.Possibles.Constant_Reference (Counter))); + SU.Append (Result, Image (Item.Possibles.Constant_Reference (Counter))); Counter := Counter + 1; - exit when not Scratch.Has_State (Counter); + exit when not Item.Has_State (Counter); end loop; return SU.Slice (Result, 1, SU.Length (Result) - 1); end Image; + function Image_Constant + (Item : in World) + return String + is + Scratch : World := Item; + begin + return Image (Scratch); + end Image_Constant; + + end Kompsos.Pretty_Print; diff --git a/src/kompsos-pretty_print.ads b/src/kompsos-pretty_print.ads index bf0b9d7..bcaf86e 100644 --- a/src/kompsos-pretty_print.ads +++ b/src/kompsos-pretty_print.ads @@ -14,16 +14,16 @@ package Kompsos.Pretty_Print is function Image - (Item : in Variable) + (Item : in Term) return String; function Image - (Item : in Term) + (Item : in out World) return String; - function Image + function Image_Constant (Item : in World) return String; @@ -41,6 +41,11 @@ private return String; + function Image + (Item : in Variable) + return String; + + function Image (Item : in State) return String; diff --git a/src/kompsos.adb b/src/kompsos.adb index 9d45f66..b3816fa 100644 --- a/src/kompsos.adb +++ b/src/kompsos.adb @@ -75,13 +75,21 @@ package body Kompsos is function Var - (This : in Term) + (This : in Term'Class) return Variable is begin return Term_Component (This.Actual.Constant_Reference.Element.all).Refer; end Var; + function Name + (This : in Term) + return SU.Unbounded_String is + begin + return This.Var.Name; + end Name; + + function Left (This : in Term) return Term is @@ -134,20 +142,22 @@ package body Kompsos is -- Internal Helpers -- ------------------------ - -- Unification -- + -- Variable IDs -- - function Has_Var - (This : in State; - Var : in Variable) - return Boolean - is - use type SU.Unbounded_String; + Next_Generator_ID : Generator_ID_Number := Generator_ID_Number'First; + + function Next_Gen + return Generator_ID_Number is begin - return This.LVars.Contains (Var.Ident) and then - This.LVars.Constant_Reference (Var.Ident) = Var.Name; - end Has_Var; + return Result : constant Generator_ID_Number := Next_Generator_ID do + Next_Generator_ID := Next_Generator_ID + 1; + end return; + end Next_Gen; + + -- Unification -- + function Fully_Contains (This : in State; Item : in Term'Class) @@ -157,7 +167,7 @@ package body Kompsos is when Null_Term | Atom_Term => return True; when Var_Term => - return Has_Var (This, Item.Var); + 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; @@ -169,8 +179,10 @@ package body Kompsos is Item : in Term'Class) return Term'Class is begin - if Item.Kind = Var_Term and then This.Subst.Contains (Item.Var.Ident) then - return Walk (This, This.Subst.Constant_Reference (Item.Var.Ident)); + 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; @@ -186,32 +198,29 @@ package body Kompsos 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 - if Has_Var (Potential, Left.Var) then - Real_Left := Walk (Potential, Left); - else - return False; - end if; + Real_Left := Walk (Potential, Real_Left); end if; if Right.Kind = Var_Term then - if Has_Var (Potential, Right.Var) then - Real_Right := Walk (Potential, Right); - else - return False; - end if; + Real_Right := Walk (Potential, Real_Right); end if; - -- Check for equal Null Terms - if Real_Left.Kind = Null_Term and Real_Right.Kind = Null_Term then - Extended := Potential; - return True; - end if; - - -- Unify equal Variable Terms - if Real_Left.Kind = Var_Term and then + -- 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 + 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; @@ -219,41 +228,18 @@ package body Kompsos is -- Unify Variable and other Terms by introducing a new substitution if Real_Left.Kind = Var_Term then - if Real_Right.Kind = Pair_Term and then - not Fully_Contains (Potential, Real_Right) - then - return False; - end if; Extended := Potential; - Extended.Subst.Insert (Real_Left.Var.Ident, Term (Real_Right)); + Extended.Subst.Insert (Extended.Ident.Element (Real_Left.Var.Ident), Term (Real_Right)); return True; end if; if Real_Right.Kind = Var_Term then - if Real_Left.Kind = Pair_Term and then - not Fully_Contains (Potential, Real_Left) - then - return False; - end if; - Extended := Potential; - Extended.Subst.Insert (Real_Right.Var.Ident, Term (Real_Left)); - return True; - end if; - - -- Unify equal Atom Terms - if Real_Left.Kind = Atom_Term and then - Real_Right.Kind = Atom_Term and then - Real_Left = Real_Right - 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 and then - Fully_Contains (Potential, Real_Left) and then - Fully_Contains (Potential, Real_Right) - then + if Real_Left.Kind = Pair_Term and then Real_Right.Kind = Pair_Term then declare Middle : State; begin @@ -285,7 +271,8 @@ package body Kompsos is begin Ptr (This.Engine.Frs_World).Rollover; for Potential of Ptr (This.Engine.Frs_World).Possibles loop - Potential.LVars.Insert (Ptr (This.Engine.Frs_World).Next_Ident, This.Engine.Frs_Name); + Potential.LVars.Append (This.Engine.Frs_Name); + Potential.Ident.Insert (This.Engine.Frs_Ident, Potential.LVars.Last_Index); This.Possibles.Append (Potential); end loop; if Ptr (This.Engine.Frs_World).Engine.Kind = No_Gen then @@ -478,14 +465,16 @@ package body Kompsos is function Fresh (This : in out World'Class; Name : in Ada.Strings.Unbounded.Unbounded_String) - return Term is + return Term + is + My_ID : constant Generator_ID_Number := Next_Gen; begin - return My_Term : constant Term := T (Variable'(Ident => This.Next_Ident, Name => Name)) do + return My_Term : constant Term := T (Variable'(Ident => My_ID, Name => Name)) do This.Engine := (Kind => Fresh_Gen, + Frs_Ident => My_ID, Frs_World => Hold (This), Frs_Name => Name); - This.Next_Ident := This.Next_Ident + 1; This.Possibles := State_Vectors.Empty_Vector; end return; end Fresh; @@ -519,9 +508,8 @@ package body Kompsos is return World is begin return Result : constant World := - (Possibles => State_Vectors.Empty_Vector, - Next_Ident => This.Next_Ident, - Engine => + (Possibles => State_Vectors.Empty_Vector, + Engine => (Kind => Unify_Gen, Uni_World => Hold (This), Uni_Term1 => Term (Left), @@ -545,9 +533,8 @@ package body Kompsos is return World is begin return Result : constant World := - (Possibles => State_Vectors.Empty_Vector, - Next_Ident => ID_Number'Max (Left.Next_Ident, Right.Next_Ident), - Engine => + (Possibles => State_Vectors.Empty_Vector, + Engine => (Kind => Disjunct_Gen, Dis_World1 => Hold (Left), Dis_World2 => Hold (Right))); @@ -568,24 +555,17 @@ package body Kompsos is begin if Inputs'Length = 0 then return Failed : constant World := - (Possibles => State_Vectors.Empty_Vector, - Next_Ident => 0, - Engine => (Kind => No_Gen)); + (Possibles => State_Vectors.Empty_Vector, + Engine => (Kind => No_Gen)); elsif Inputs'Length = 1 then return Inputs (Inputs'First); else - return Result : World := - (Possibles => State_Vectors.Empty_Vector, - Next_Ident => 0, -- dummy - Engine => + return Result : constant World := + (Possibles => State_Vectors.Empty_Vector, + Engine => (Kind => Disjunct_Gen, Dis_World1 => Hold (Inputs (Inputs'First)), - Dis_World2 => Hold (Disjunct (Inputs (Inputs'First + 1 .. Inputs'Last))))) - do - Result.Next_Ident := ID_Number'Max - (Ptr (Result.Engine.Dis_World1).Next_Ident, - Ptr (Result.Engine.Dis_World2).Next_Ident); - end return; + Dis_World2 => Hold (Disjunct (Inputs (Inputs'First + 1 .. Inputs'Last))))); end if; end Disjunct; @@ -607,9 +587,8 @@ package body Kompsos is return World is begin return Result : constant World := - (Possibles => State_Vectors.Empty_Vector, - Next_Ident => 0, -- dummy - Engine => + (Possibles => State_Vectors.Empty_Vector, + Engine => (Kind => Conjunct_Zero_Gen, ConZ_World => Hold (This), ConZ_Func => Func)); @@ -631,9 +610,8 @@ package body Kompsos is return World is begin return Result : constant World := - (Possibles => State_Vectors.Empty_Vector, - Next_Ident => 0, -- dummy - Engine => + (Possibles => State_Vectors.Empty_Vector, + Engine => (Kind => Conjunct_One_Gen, ConO_World => Hold (This), ConO_Func => Func, @@ -657,9 +635,8 @@ package body Kompsos is return World is begin return Result : constant World := - (Possibles => State_Vectors.Empty_Vector, - Next_Ident => 0, -- dummy - Engine => + (Possibles => State_Vectors.Empty_Vector, + Engine => (Kind => Conjunct_Many_Gen, ConM_World => Hold (This), ConM_Func => Func, @@ -689,9 +666,8 @@ package body Kompsos is return World is begin return Result : constant World := - (Possibles => State_Vectors.Empty_Vector, - Next_Ident => This.Next_Ident, - Engine => + (Possibles => State_Vectors.Empty_Vector, + Engine => (Kind => Recurse_Gen, Rec_World => Hold (This), Rec_Index => 1)); @@ -715,9 +691,8 @@ package body Kompsos is begin if Count = 0 then return - (Possibles => State_Vectors.Empty_Vector, - Next_Ident => ID_Number'First, - Engine => (Kind => No_Gen)); + (Possibles => State_Vectors.Empty_Vector, + Engine => (Kind => No_Gen)); end if; return Result : World := This do Result.Roll_Until (Count); diff --git a/src/kompsos.ads b/src/kompsos.ads index cf4ba31..c336a41 100644 --- a/src/kompsos.ads +++ b/src/kompsos.ads @@ -14,8 +14,7 @@ private with Ada.Containers.Indefinite_Holders, Ada.Containers.Ordered_Maps, - Ada.Containers.Vectors, - Ada.Finalization; + Ada.Containers.Vectors; generic @@ -27,9 +26,6 @@ package Kompsos is -- Datatypes -- ----------------- - type Variable is private; - - type Term_Kind is (Null_Term, Atom_Term, Var_Term, Pair_Term); type Term is tagged private; @@ -58,9 +54,9 @@ package Kompsos is return Element_Type with Pre => This.Kind = Atom_Term; - function Var + function Name (This : in Term) - return Variable + return Ada.Strings.Unbounded.Unbounded_String with Pre => This.Kind = Var_Term; function Left @@ -105,17 +101,20 @@ package Kompsos is function Fresh (This : in out World'Class) - return Term; + return Term + with Post => Fresh'Result.Kind = Var_Term; function Fresh (This : in out World'Class; Name : in String) - return Term; + return Term + with Post => Fresh'Result.Kind = Var_Term; function Fresh (This : in out World'Class; Name : in Ada.Strings.Unbounded.Unbounded_String) - return Term; + return Term + with Post => Fresh'Result.Kind = Var_Term; -- Unification -- @@ -404,11 +403,14 @@ private - -- 2^32 possible Variables per World is enough for anybody, right? - type ID_Number is mod 2 ** 32; + -- around 2^31 possible Variables should be enough for anybody, right? + type ID_Number is new Long_Integer range 0 .. Long_Integer'Last; + + type Generator_ID_Number is new ID_Number; + type Variable_ID_Number is new ID_Number; type Variable is record - Ident : ID_Number; + Ident : Generator_ID_Number; Name : SU.Unbounded_String; end record; @@ -436,6 +438,11 @@ private Actual : Term_Holders.Holder; end record; + function Var + (This : in Term'Class) + return Variable + with Pre => This.Kind = Var_Term; + Empty_Term : constant Term := (Actual => Term_Holders.To_Holder (Term_Component'(Kind => Null_Term))); @@ -444,22 +451,28 @@ private - package Name_Maps is new Ada.Containers.Ordered_Maps - (Key_Type => ID_Number, + package ID_Number_Maps is new Ada.Containers.Ordered_Maps + (Key_Type => Generator_ID_Number, + Element_Type => Variable_ID_Number); + + package Name_Vectors is new Ada.Containers.Vectors + (Index_Type => Variable_ID_Number, Element_Type => SU.Unbounded_String, "=" => SU."="); package Binding_Maps is new Ada.Containers.Ordered_Maps - (Key_Type => ID_Number, + (Key_Type => Variable_ID_Number, Element_Type => Term); type State is record - LVars : Name_Maps.Map; + Ident : ID_Number_Maps.Map; + LVars : Name_Vectors.Vector; Subst : Binding_Maps.Map; end record; Empty_State : constant State := - (LVars => Name_Maps.Empty_Map, + (Ident => ID_Number_Maps.Empty_Map, + LVars => Name_Vectors.Empty_Vector, Subst => Binding_Maps.Empty_Map); @@ -501,6 +514,7 @@ private when No_Gen => null; when Fresh_Gen => + Frs_Ident : Generator_ID_Number; Frs_World : World_Holders.Holder; Frs_Name : SU.Unbounded_String; when Unify_Gen => @@ -534,9 +548,8 @@ private Element_Type => State); type World is new World_Root with record - Possibles : State_Vectors.Vector; - Next_Ident : ID_Number; - Engine : Generator; + Possibles : State_Vectors.Vector; + Engine : Generator; end record; function Has_State @@ -554,9 +567,8 @@ private use type State_Vectors.Vector; Empty_World : constant World := - (Possibles => State_Vectors.Empty_Vector & Empty_State, - Next_Ident => 0, - Engine => (Kind => No_Gen)); + (Possibles => State_Vectors.Empty_Vector & Empty_State, + Engine => (Kind => No_Gen)); end Kompsos; -- cgit