From 7719622ff4f72769f15a771dc5455dabeff295bc Mon Sep 17 00:00:00 2001 From: Jedidiah Barber Date: Mon, 10 Nov 2025 18:57:08 +1300 Subject: Infinite number of States in a World enabled with lazy evaluation --- src/kompsos-pretty_print.adb | 14 +- src/kompsos.adb | 299 ++++++++++++++++++++++++++++++++++++++----- src/kompsos.ads | 85 ++++++++++-- 3 files changed, 353 insertions(+), 45 deletions(-) (limited to 'src') diff --git a/src/kompsos-pretty_print.adb b/src/kompsos-pretty_print.adb index d1d89b8..62f27fa 100644 --- a/src/kompsos-pretty_print.adb +++ b/src/kompsos-pretty_print.adb @@ -124,14 +124,18 @@ package body Kompsos.Pretty_Print is (Item : in World) return String is - Result : SU.Unbounded_String; + Result : SU.Unbounded_String; + Scratch : World := Item; + Counter : Positive := 1; begin - if Item.Possibles.Is_Empty then + if not Scratch.Has_State (Counter) then return "States: N/A" & Latin.LF; end if; - for Index in Integer range Item.Possibles.First_Index .. Item.Possibles.Last_Index loop - SU.Append (Result, "State#" & Image (Index) & ":" & Latin.LF); - SU.Append (Result, Image (Item.Possibles.Constant_Reference (Index))); + loop + SU.Append (Result, "State#" & Image (Counter) & ":" & Latin.LF); + SU.Append (Result, Image (Scratch.Possibles.Constant_Reference (Counter))); + Counter := Counter + 1; + exit when not Scratch.Has_State (Counter); end loop; return SU.Slice (Result, 1, SU.Length (Result) - 1); end Image; diff --git a/src/kompsos.adb b/src/kompsos.adb index 5997ddf..a621b7f 100644 --- a/src/kompsos.adb +++ b/src/kompsos.adb @@ -14,9 +14,11 @@ with package body Kompsos is - ------------------------------ - -- Controlled Subprograms -- - ------------------------------ + ------------------------- + -- Memory Management -- + ------------------------- + + -- Terms -- procedure Free is new Ada.Unchecked_Deallocation (Term_Component, Term_Component_Access); @@ -54,6 +56,51 @@ package body Kompsos is + -- Worlds -- + + procedure Free is new Ada.Unchecked_Deallocation (World, World_Access); + + + procedure Adjust + (This : in out World) is + begin + case This.Engine.Kind is + when No_Gen => + null; + when Fresh_Gen => + This.Engine.FrG_World := new World'(This.Engine.FrG_World.all); + when Unify_Gen => + This.Engine.UniG_World := new World'(This.Engine.UniG_World.all); + when Disjunct_Gen => + This.Engine.DisG_World1 := new World'(This.Engine.DisG_World1.all); + This.Engine.DisG_World2 := new World'(This.Engine.DisG_World2.all); + when Recurse_Gen => + This.Engine.RecG_World := new World'(This.Engine.RecG_World.all); + end case; + end Adjust; + + + procedure Finalize + (This : in out World) is + begin + case This.Engine.Kind is + when No_Gen => + null; + when Fresh_Gen => + Free (This.Engine.FrG_World); + when Unify_Gen => + Free (This.Engine.UniG_World); + when Disjunct_Gen => + Free (This.Engine.DisG_World1); + Free (This.Engine.DisG_World2); + when Recurse_Gen => + Free (This.Engine.RecG_World); + end case; + end Finalize; + + + + ------------- -- Terms -- ------------- @@ -127,9 +174,11 @@ package body Kompsos is - --------------------- - -- Unify Helpers -- - --------------------- + ------------------------ + -- Internal Helpers -- + ------------------------ + + -- Unification -- function Has_Var (This : in State; @@ -273,9 +322,126 @@ package body Kompsos is - ------------- + -- Lazy World Generation -- + + function Has_State + (This : in out World; + Index : in Positive) + return Boolean is + begin + This.Roll_Until (Index); + return This.Possibles.Last_Index >= Index; + end Has_State; + + + procedure Roll_Fresh_Gen + (This : in out World) is + begin + if not This.Engine.FrG_World.Has_State (This.Engine.FrG_Index) then + This.Engine := (Kind => No_Gen); + return; + end if; + This.Possibles.Append (This.Engine.FrG_World.Possibles.Element (This.Engine.FrG_Index)); + This.Possibles.Reference (This.Possibles.Last_Index).LVars.Insert + (This.Engine.FrG_World.Next_Ident, + This.Engine.FrG_Name); + This.Engine.FrG_Index := This.Engine.FrG_Index + 1; + end Roll_Fresh_Gen; + + + procedure Roll_Unify_Gen + (This : in out World) + is + Extended : State; + begin + loop + if not This.Engine.UniG_World.Has_State (This.Engine.UniG_Index) then + This.Engine := (Kind => No_Gen); + return; + end if; + exit when Do_Unify + (This.Engine.UniG_World.Possibles (This.Engine.UniG_Index), + This.Engine.UniG_Term1, + This.Engine.UniG_Term2, + Extended); + This.Engine.UniG_Index := This.Engine.UniG_Index + 1; + end loop; + This.Possibles.Append (Extended); + This.Engine.UniG_Index := This.Engine.UniG_Index + 1; + end Roll_Unify_Gen; + + + procedure Roll_Disjunct_Gen + (This : in out World) + is + Temp_World : World_Access; + Temp_Index : Positive; + begin + if not This.Engine.DisG_World1.Has_State (This.Engine.DisG_Index1) then + if not This.Engine.DisG_World2.Has_State (This.Engine.DisG_Index2) then + This.Engine := (Kind => No_Gen); + return; + end if; + This.Possibles.Append (This.Engine.DisG_World2.Possibles (This.Engine.DisG_Index2)); + This.Engine.DisG_Index2 := This.Engine.DisG_Index2 + 1; + else + This.Possibles.Append (This.Engine.DisG_World1.Possibles (This.Engine.DisG_Index1)); + This.Engine.DisG_Index1 := This.Engine.DisG_Index1 + 1; + end if; + Temp_World := This.Engine.DisG_World1; + Temp_Index := This.Engine.DisG_Index1; + This.Engine.DisG_World1 := This.Engine.DisG_World2; + This.Engine.DisG_Index1 := This.Engine.DisG_Index2; + This.Engine.DisG_World2 := Temp_World; + This.Engine.DisG_Index2 := Temp_Index; + end Roll_Disjunct_Gen; + + + procedure Roll_Recurse_Gen + (This : in out World) is + begin + if not This.Engine.RecG_World.Has_State (This.Engine.RecG_Index) then + if This.Engine.RecG_Index = 1 then + This.Engine := (Kind => No_Gen); + return; + end if; + This.Engine.RecG_Index := 1; + end if; + This.Possibles.Append (This.Engine.RecG_World.Possibles (This.Engine.RecG_Index)); + This.Engine.RecG_Index := This.Engine.RecG_Index + 1; + end Roll_Recurse_Gen; + + + procedure Rollover + (This : in out World) is + begin + case This.Engine.Kind is + when No_Gen => null; + when Fresh_Gen => This.Roll_Fresh_Gen; + when Unify_Gen => This.Roll_Unify_Gen; + when Disjunct_Gen => This.Roll_Disjunct_Gen; + when Recurse_Gen => This.Roll_Recurse_Gen; + end case; + end Rollover; + + + procedure Roll_Until + (This : in out World; + Index : in Positive) is + begin + while This.Possibles.Last_Index < Index and This.Engine.Kind /= No_Gen loop + This.Rollover; + end loop; + end Roll_Until; + + + + + ----------------------------- + -- Public API Operations -- + ----------------------------- + -- Fresh -- - ------------- function Fresh (This : in out World) @@ -300,19 +466,22 @@ package body Kompsos is return Variable is begin return My_Var : constant Variable := (Ident => This.Next_Ident, Name => Name) do - This.Next_Ident := This.Next_Ident + 1; - for Potential of This.Possibles loop - Potential.LVars.Insert (My_Var.Ident, My_Var.Name); - end loop; + This := (Ada.Finalization.Controlled with + Possibles => State_Vectors.Empty_Vector, + Next_Ident => This.Next_Ident + 1, + Engine => + (Kind => Fresh_Gen, + FrG_World => new World'(This), + FrG_Index => 1, + FrG_Name => Name)); + This.Rollover; end return; end Fresh; - ------------- -- Unify -- - ------------- function Unify (This : in World; @@ -372,18 +541,20 @@ package body Kompsos is function Unify (This : in World; Left, Right : in Term'Class) - return World - is - Result : World; - Extended : State; + return World is begin - Result.Next_Ident := This.Next_Ident; - for Potential of This.Possibles loop - if Do_Unify (Potential, Left, Right, Extended) then - Result.Possibles.Append (Extended); - end if; - end loop; - return Result; + return Result : World := (Ada.Finalization.Controlled with + Possibles => State_Vectors.Empty_Vector, + Next_Ident => This.Next_Ident, + Engine => + (Kind => Unify_Gen, + UniG_World => new World'(This), + UniG_Index => 1, + UniG_Term1 => Term (Left), + UniG_Term2 => Term (Right))) + do + Result.Rollover; + end return; end Unify; @@ -397,17 +568,24 @@ package body Kompsos is - ---------------- -- Disjunct -- - ---------------- function Disjunct (Left, Right : in World) return World is begin - return My_World : constant World := - (Possibles => Left.Possibles & Right.Possibles, - Next_Ident => ID_Number'Max (Left.Next_Ident, Right.Next_Ident)); + return Result : World := (Ada.Finalization.Controlled with + Possibles => State_Vectors.Empty_Vector, + Next_Ident => ID_Number'Max (Left.Next_Ident, Right.Next_Ident), + Engine => + (Kind => Disjunct_Gen, + DisG_World1 => new World'(Left), + DisG_Index1 => 1, + DisG_World2 => new World'(Right), + DisG_Index2 => 1)) + do + Result.Rollover; + end return; end Disjunct; @@ -419,6 +597,67 @@ package body Kompsos is end Disjunct; + + + -- Recurse -- + + function Recurse + (This : in World) + return World is + begin + return Result : World := (Ada.Finalization.Controlled with + Possibles => State_Vectors.Empty_Vector, + Next_Ident => This.Next_Ident, + Engine => + (Kind => Recurse_Gen, + RecG_World => new World'(This), + RecG_Index => 1)) + do + Result.Rollover; + end return; + end Recurse; + + + procedure Recurse + (This : in out World) is + begin + This := This.Recurse; + end Recurse; + + + + + -- Take -- + + function Take + (This : in World; + Count : in Natural) + return World is + begin + if Count = 0 then + return (Ada.Finalization.Controlled with + Possibles => State_Vectors.Empty_Vector, + Next_Ident => ID_Number'First, + Engine => (Kind => No_Gen)); + end if; + return Result : World := This do + Result.Roll_Until (Count); + if Result.Possibles.Last_Index > Count then + Result.Possibles.Set_Length (Ada.Containers.Count_Type (Count)); + end if; + Result.Engine := (Kind => No_Gen); + end return; + end Take; + + + procedure Take + (This : in out World; + Count : in Natural) is + begin + This := This.Take (Count); + end Take; + + end Kompsos; diff --git a/src/kompsos.ads b/src/kompsos.ads index c25cf52..bca09b8 100644 --- a/src/kompsos.ads +++ b/src/kompsos.ads @@ -132,6 +132,28 @@ package Kompsos is Right : in World); + + + function Recurse + (This : in World) + return World; + + procedure Recurse + (This : in out World); + + + + + function Take + (This : in World; + Count : in Natural) + return World; + + procedure Take + (This : in out World; + Count : in Natural); + + private @@ -151,7 +173,7 @@ private - -- 2^32 possible variables per World is enough for anybody, right? + -- 2^32 possible Variables per World is enough for anybody, right? type ID_Number is mod 2 ** 32; type Variable is record @@ -217,25 +239,68 @@ private - -- obviously this World definition will need revision for delays and generators + type World_Access is access World; - -- going to have to turn worlds into a similar sort of reference counted recursive - -- controlled type along the lines of what terms are, in order to make them into generators + type Generator_Kind is (No_Gen, Fresh_Gen, Unify_Gen, Disjunct_Gen, Recurse_Gen); + + type Generator (Kind : Generator_Kind := No_Gen) is record + case Kind is + when No_Gen => + null; + when Fresh_Gen => + FrG_World : World_Access; + FrG_Index : Positive; + FrG_Name : SU.Unbounded_String; + when Unify_Gen => + UniG_World : World_Access; + UniG_Index : Positive; + UniG_Term1 : Term; + UniG_Term2 : Term; + when Disjunct_Gen => + DisG_World1 : World_Access; + DisG_Index1 : Positive; + DisG_World2 : World_Access; + DisG_Index2 : Positive; + when Recurse_Gen => + RecG_World : World_Access; + RecG_Index : Positive; + end case; + end record; package State_Vectors is new Ada.Containers.Vectors (Index_Type => Positive, Element_Type => State); - use type State_Vectors.Vector; - - type World is tagged record + type World is new Ada.Finalization.Controlled with record Possibles : State_Vectors.Vector; Next_Ident : ID_Number; + Engine : Generator; end record; - Empty_World : constant World := - (Possibles => State_Vectors.Empty_Vector & Empty_State, - Next_Ident => 0); + overriding procedure Adjust + (This : in out World); + + overriding procedure Finalize + (This : in out World); + + function Has_State + (This : in out World; + Index : in Positive) + return Boolean; + + procedure Rollover + (This : in out World); + + procedure Roll_Until + (This : in out World; + Index : in Positive); + + use type State_Vectors.Vector; + + Empty_World : constant World := (Ada.Finalization.Controlled with + Possibles => State_Vectors.Empty_Vector & Empty_State, + Next_Ident => 0, + Engine => (Kind => No_Gen)); end Kompsos; -- cgit