diff options
| -rw-r--r-- | src/kompsos.adb | 201 | ||||
| -rw-r--r-- | src/kompsos.ads | 59 |
2 files changed, 181 insertions, 79 deletions
diff --git a/src/kompsos.adb b/src/kompsos.adb index 7cfd581..d018c27 100644 --- a/src/kompsos.adb +++ b/src/kompsos.adb @@ -71,9 +71,11 @@ package body Kompsos is 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 Disjunct1_Gen => + This.Engine.Dis1G_World := new World'(This.Engine.Dis1G_World.all); + when Disjunct2_Gen => + This.Engine.Dis2G_World1 := new World'(This.Engine.Dis2G_World1.all); + This.Engine.Dis2G_World2 := new World'(This.Engine.Dis2G_World2.all); when Recurse_Gen => This.Engine.RecG_World := new World'(This.Engine.RecG_World.all); end case; @@ -90,9 +92,11 @@ package body Kompsos is 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 Disjunct1_Gen => + Free (This.Engine.Dis1G_World); + when Disjunct2_Gen => + Free (This.Engine.Dis2G_World1); + Free (This.Engine.Dis2G_World2); when Recurse_Gen => Free (This.Engine.RecG_World); end case; @@ -351,8 +355,11 @@ package body Kompsos is 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); + This.Engine.FrG_World.Rollover; + if This.Engine.FrG_World.Possibles.Last_Index < This.Engine.FrG_Index then + if This.Engine.FrG_World.Engine.Kind = No_Gen then + This.Engine := (Kind => No_Gen); + end if; return; end if; This.Possibles.Append (This.Engine.FrG_World.Possibles.Element (This.Engine.FrG_Index)); @@ -368,73 +375,102 @@ package body Kompsos is is Extended : State; begin - loop - if not This.Engine.UniG_World.Has_State (This.Engine.UniG_Index) then + This.Engine.UniG_World.Rollover; + if This.Engine.UniG_World.Possibles.Last_Index < This.Engine.UniG_Index then + if This.Engine.UniG_World.Engine.Kind = No_Gen then This.Engine := (Kind => No_Gen); - return; end if; - exit when Do_Unify + return; + end if; + if not Do_Unify (This.Engine.UniG_World.Possibles (This.Engine.UniG_Index), This.Engine.UniG_Term1, This.Engine.UniG_Term2, - Extended); + Extended) + then This.Engine.UniG_Index := This.Engine.UniG_Index + 1; - end loop; + return; + end if; This.Possibles.Append (Extended); This.Engine.UniG_Index := This.Engine.UniG_Index + 1; end Roll_Unify_Gen; - procedure Roll_Disjunct_Gen + procedure Roll_Disjunct1_Gen + (This : in out World) is + begin + This.Engine.Dis1G_World.Rollover; + if This.Engine.Dis1G_World.Possibles.Last_Index < This.Engine.Dis1G_Index then + if This.Engine.Dis1G_World.Engine.Kind = No_Gen then + This.Engine := (Kind => No_Gen); + end if; + return; + end if; + This.Possibles.Append (This.Engine.Dis1G_World.Possibles (This.Engine.Dis1G_Index)); + This.Engine.Dis1G_Index := This.Engine.Dis1G_Index + 1; + end Roll_Disjunct1_Gen; + + + procedure Roll_Disjunct2_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); + This.Engine.Dis2G_World1.Rollover; + if This.Engine.Dis2G_World1.Possibles.Last_Index < This.Engine.Dis2G_Index1 then + if This.Engine.Dis2G_World1.Engine.Kind = No_Gen then + This.Engine := + (Kind => Disjunct1_Gen, + Dis1G_World => This.Engine.Dis2G_World2, + Dis1G_Index => This.Engine.Dis2G_Index2); 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; + This.Possibles.Append (This.Engine.Dis2G_World1.Possibles (This.Engine.Dis2G_Index1)); + This.Engine.Dis2G_Index1 := This.Engine.Dis2G_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; + Temp_World := This.Engine.Dis2G_World1; + Temp_Index := This.Engine.Dis2G_Index1; + This.Engine.Dis2G_World1 := This.Engine.Dis2G_World2; + This.Engine.Dis2G_Index1 := This.Engine.Dis2G_Index2; + This.Engine.Dis2G_World2 := Temp_World; + This.Engine.Dis2G_Index2 := Temp_Index; + end Roll_Disjunct2_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; + This.Engine.RecG_World.Rollover; + if This.Engine.RecG_World.Possibles.Last_Index < This.Engine.RecG_Index then + if This.Engine.RecG_World.Engine.Kind = No_Gen then + if This.Engine.RecG_Index = 1 then + This.Engine := (Kind => No_Gen); + return; + end if; + This.Engine.RecG_Index := 1; end if; - This.Engine.RecG_Index := 1; + return; 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; + -- Note that more than one call to Rollover may be needed to generate the next State. + -- This is intentional to get better behaviour with infinite Worlds. + 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; + when No_Gen => null; + when Fresh_Gen => This.Roll_Fresh_Gen; + when Unify_Gen => This.Roll_Unify_Gen; + when Disjunct1_Gen => This.Roll_Disjunct1_Gen; + when Disjunct2_Gen => This.Roll_Disjunct2_Gen; + when Recurse_Gen => This.Roll_Recurse_Gen; end case; end Rollover; @@ -488,7 +524,6 @@ package body Kompsos is FrG_World => new World'(This), FrG_Index => 1, FrG_Name => Name)); - This.Rollover; end return; end Fresh; @@ -557,7 +592,7 @@ package body Kompsos is Left, Right : in Term'Class) return World is begin - return Result : World := (Ada.Finalization.Controlled with + return Result : constant World := (Ada.Finalization.Controlled with Possibles => State_Vectors.Empty_Vector, Next_Ident => This.Next_Ident, Engine => @@ -565,10 +600,7 @@ package body Kompsos is UniG_World => new World'(This), UniG_Index => 1, UniG_Term1 => Term (Left), - UniG_Term2 => Term (Right))) - do - Result.Rollover; - end return; + UniG_Term2 => Term (Right))); end Unify; @@ -588,18 +620,15 @@ package body Kompsos is (Left, Right : in World) return World is begin - return Result : World := (Ada.Finalization.Controlled with + return Result : constant 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; + (Kind => Disjunct2_Gen, + Dis2G_World1 => new World'(Left), + Dis2G_Index1 => 1, + Dis2G_World2 => new World'(Right), + Dis2G_Index2 => 1)); end Disjunct; @@ -611,6 +640,44 @@ package body Kompsos is end Disjunct; + function Disjunct + (Inputs : in World_Array) + return World is + begin + if Inputs'Length = 0 then + return Failed : constant World := (Ada.Finalization.Controlled with + Possibles => State_Vectors.Empty_Vector, + Next_Ident => 0, + Engine => (Kind => No_Gen)); + elsif Inputs'Length = 1 then + return Inputs (Inputs'First); + else + return Result : World := (Ada.Finalization.Controlled with + Possibles => State_Vectors.Empty_Vector, + Next_Ident => 0, -- dummy + Engine => + (Kind => Disjunct2_Gen, + Dis2G_World1 => new World'(Inputs (Inputs'First)), + Dis2G_Index1 => 1, + Dis2G_World2 => new World'(Disjunct (Inputs (Inputs'First + 1 .. Inputs'Last))), + Dis2G_Index2 => 1)) + do + Result.Next_Ident := ID_Number'Max + (Result.Engine.Dis2G_World1.Next_Ident, + Result.Engine.Dis2G_World2.Next_Ident); + end return; + end if; + end Disjunct; + + + procedure Disjunct + (This : in out World; + Inputs : in World_Array) is + begin + This := Disjunct (This & Inputs); + end Disjunct; + + -- Recurse -- @@ -619,16 +686,13 @@ package body Kompsos is (This : in World) return World is begin - return Result : World := (Ada.Finalization.Controlled with + return Result : constant 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; + RecG_Index => 1)); end Recurse; @@ -641,7 +705,7 @@ package body Kompsos is - -- Take -- + -- Forced Evaluation -- function Take (This : in World; @@ -672,6 +736,23 @@ package body Kompsos is end Take; + procedure Force + (This : in out World; + Count : in Positive) is + begin + This.Roll_Until (Count); + end Force; + + + procedure Force_All + (This : in out World) is + begin + while This.Engine.Kind /= No_Gen loop + This.Rollover; + end loop; + end Force_All; + + end Kompsos; diff --git a/src/kompsos.ads b/src/kompsos.ads index a2e210e..d229eb3 100644 --- a/src/kompsos.ads +++ b/src/kompsos.ads @@ -26,8 +26,6 @@ package Kompsos is type Variable_Array is array (Positive range <>) of Variable; - - type Term is tagged private; type Term_Array is array (Positive range <>) of Term; @@ -58,9 +56,8 @@ package Kompsos is -- Might include subprograms to retrieve Term contents later? - - type World is tagged private; + type World_Array is array (Positive range <>) of World; Empty_World : constant World; @@ -135,6 +132,14 @@ package Kompsos is (This : in out World; Right : in World); + function Disjunct + (Inputs : in World_Array) + return World; + + procedure Disjunct + (This : in out World; + Inputs : in World_Array); + @@ -157,6 +162,13 @@ package Kompsos is (This : in out World; Count : in Natural); + procedure Force + (This : in out World; + Count : in Positive); + + procedure Force_All + (This : in out World); + private @@ -245,29 +257,38 @@ private type World_Access is access World; - type Generator_Kind is (No_Gen, Fresh_Gen, Unify_Gen, Disjunct_Gen, Recurse_Gen); + type Generator_Kind is + (No_Gen, + Fresh_Gen, + Unify_Gen, + Disjunct1_Gen, + Disjunct2_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; + 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; + UniG_World : World_Access; + UniG_Index : Positive; + UniG_Term1 : Term; + UniG_Term2 : Term; + when Disjunct1_Gen => + Dis1G_World : World_Access; + Dis1G_Index : Positive; + when Disjunct2_Gen => + Dis2G_World1 : World_Access; + Dis2G_Index1 : Positive; + Dis2G_World2 : World_Access; + Dis2G_Index2 : Positive; when Recurse_Gen => - RecG_World : World_Access; - RecG_Index : Positive; + RecG_World : World_Access; + RecG_Index : Positive; end case; end record; |