diff options
Diffstat (limited to 'src/kompsos.adb')
| -rw-r--r-- | src/kompsos.adb | 299 |
1 files changed, 269 insertions, 30 deletions
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; |