aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJedidiah Barber <contact@jedbarber.id.au>2026-01-24 01:11:17 +1300
committerJedidiah Barber <contact@jedbarber.id.au>2026-01-24 01:11:17 +1300
commit7b201fc0587e8012189f7b1f245734e117e4975c (patch)
tree8201d7ccea0d6cf4a809614e8e7b4c818f3af79b
parent28d132c2823d7dfa21190bf746f9f39dd59a40d8 (diff)
Unrolled linked lists for StateHEADmaster
-rw-r--r--readme.md13
-rw-r--r--src/kompsos-collector.adb75
-rw-r--r--src/kompsos-collector.ads1
-rw-r--r--src/kompsos-pretty_print.adb8
-rw-r--r--src/kompsos.adb35
-rw-r--r--src/kompsos.ads18
6 files changed, 94 insertions, 56 deletions
diff --git a/readme.md b/readme.md
index 089ffee..9a47632 100644
--- a/readme.md
+++ b/readme.md
@@ -90,12 +90,13 @@ instead.
All the Goal operations beyond the microKanren four take an array of Terms as
input in order to allow for Conjunct to be reasonably implemented.
-The State datatype makes use of custom linked lists, and the bookkeeping data
-in the Collector package uses a custom directed acyclic graph structure that
-reflects the main Goal graph. This is done instead of using Vectors or Maps
-from the standard library both to improve speed and reduce memory requirements.
-The improvement due to tail sharing is considerable, despite the theoretically
-expensive operations involved walking the list to reify a variable.
+The State datatype makes use of custom unrolled linked lists, and the
+bookkeeping data in the Collector package uses a custom directed acyclic graph
+structure that reflects the main Goal graph. This is done instead of using
+Vectors or Maps from the standard library both to improve speed and reduce
+memory requirements. The improvement due to tail sharing is considerable,
+despite the theoretically expensive operations involved in walking the list to
+reify a variable.
diff --git a/src/kompsos-collector.adb b/src/kompsos-collector.adb
index 4654dc7..2c52160 100644
--- a/src/kompsos-collector.adb
+++ b/src/kompsos-collector.adb
@@ -55,6 +55,33 @@ package body Kompsos.Collector is
-- Unification --
+ Use_New_Node : Boolean := False;
+
+ function Append
+ (This : in State;
+ Key : in Variable;
+ Value : in Term)
+ return State is
+ begin
+ if Use_New_Node or else This.Ctrl.Actual = null or else
+ (This.Ctrl.Actual /= null and then This.Ctrl.Actual.Valid = Valid_Count'Last)
+ then
+ Use_New_Node := False;
+ return (Ctrl => (Ada.Finalization.Controlled with
+ Actual => new State_Component'(
+ Counter => 1,
+ Valid => Valid_Count'First,
+ Data => (1 => (Key, Value), others => <>),
+ Next => This)));
+ else
+ return Result : constant State := This do
+ Result.Ctrl.Actual.Valid := Result.Ctrl.Actual.Valid + 1;
+ Result.Ctrl.Actual.Data (Result.Ctrl.Actual.Valid) := (Key, Value);
+ end return;
+ end if;
+ end Append;
+
+
procedure Walk
(This : in State;
Item : in out Term)
@@ -95,21 +122,11 @@ package body Kompsos.Collector is
-- Unify Variable and other Terms by introducing a new substitution
if Real_Left.Kind = Var_Term then
- Extended := (Ctrl => (Ada.Finalization.Controlled with
- Actual => new State_Component'(
- Counter => 1,
- Key => Real_Left.Var,
- Value => Real_Right,
- Next => Potential)));
+ Extended := Append (Potential, Real_Left.Var, Real_Right);
return True;
end if;
if Real_Right.Kind = Var_Term then
- Extended := (Ctrl => (Ada.Finalization.Controlled with
- Actual => new State_Component'(
- Counter => 1,
- Key => Real_Right.Var,
- Value => Real_Left,
- Next => Potential)));
+ Extended := Append (Potential, Real_Right.Var, Real_Left);
return True;
end if;
@@ -205,7 +222,7 @@ package body Kompsos.Collector is
end Reset;
- function Raw_New_Book
+ function New_Book_Factory
(Kind : in Node_Kind)
return Book_Node_Access is
begin
@@ -219,7 +236,7 @@ package body Kompsos.Collector is
when Recurse_Node =>
return new Book_Node'(Data => (Kind => Recurse_Node, others => <>), others => <>);
end case;
- end Raw_New_Book;
+ end New_Book_Factory;
function New_Book
@@ -228,9 +245,9 @@ package body Kompsos.Collector is
begin
pragma Assert (Ptr.Counter /= 0);
if Ptr.Counter = 1 or Ptr = Relation.Graph.Actual then
- return Raw_New_Book (Ptr.Kind);
+ return New_Book_Factory (Ptr.Kind);
else
- return Acc : constant Book_Node_Access := Raw_New_Book (Ptr.Kind) do
+ return Acc : constant Book_Node_Access := New_Book_Factory (Ptr.Kind) do
Loose_Books.Append ((1, Ptr, Acc));
end return;
end if;
@@ -414,12 +431,10 @@ package body Kompsos.Collector is
if Book = null then
Book := New_Book (Ptr);
end if;
- if Ptr.Rec_Goal.Actual = null then
- Book.Data.Rec_Cache := False;
- elsif Book.Next1 = null then
+ if Book.Next1 = null then
Book.Next1 := Connect_Loose (Ptr.Rec_Goal.Actual);
end if;
- if Book.Data.Rec_Cache then
+ if Ptr.Rec_Goal.Actual /= null then
if Book.Next1 = null then
Book.Next1 := New_Book (Ptr.Rec_Goal.Actual);
Book.Next1.Cache := new Cache_Entry'(True, State_Vectors.Empty_Vector);
@@ -443,12 +458,8 @@ package body Kompsos.Collector is
return False;
else
Book.Data.Rec_Next := 1;
- Book.Data.Rec_Cache := False;
end if;
end loop;
- if Book.Data.Rec_Cache and Ptr.Rec_Goal.Actual.Counter = 1 then
- Book.Next1.Cache.Data.Append ((1, new State'(Result)));
- end if;
Book.Data.Rec_Next := Book.Data.Rec_Next + 1;
return True;
end case;
@@ -468,6 +479,7 @@ package body Kompsos.Collector is
elsif Ptr.Actual = null then
if Index = 1 then
Result := Base;
+ Use_New_Node := True;
return True;
else
return False;
@@ -483,17 +495,24 @@ package body Kompsos.Collector is
if not Book.Cache.Keep and then Book.Cache.Data (Index).Used >= Ptr.Actual.Counter then
Free (Book.Cache.Data (Index).Data);
end if;
+ Use_New_Node := True;
return True;
else
return Found : constant Boolean :=
Do_Get_Next (Ptr.Actual, Book, Base, Index, Result)
do
- if Found and Ptr.Actual.Counter > 1 and Ptr.Actual /= Relation.Graph.Actual then
- if Book.Cache = null then
+ if Found then
+ if Ptr.Actual.Counter > 1 and then
+ Ptr.Actual /= Relation.Graph.Actual and then
+ Book.Cache = null
+ then
Book.Cache := new Cache_Entry'(False, State_Vectors.Empty_Vector);
end if;
- pragma Assert (Index = Book.Cache.Data.Last_Index + 1);
- Book.Cache.Data.Append ((1, new State'(Result)));
+ if Book.Cache /= null then
+ pragma Assert (Index = Book.Cache.Data.Last_Index + 1);
+ Book.Cache.Data.Append ((1, new State'(Result)));
+ Use_New_Node := True;
+ end if;
end if;
end return;
end if;
diff --git a/src/kompsos-collector.ads b/src/kompsos-collector.ads
index f03e1e6..93fd6d4 100644
--- a/src/kompsos-collector.ads
+++ b/src/kompsos-collector.ads
@@ -64,7 +64,6 @@ private
when Recurse_Node =>
Rec_Next : Long_Positive := 1;
Rec_Gone : Boolean := False;
- Rec_Cache : Boolean := True;
end case;
end record;
diff --git a/src/kompsos-pretty_print.adb b/src/kompsos-pretty_print.adb
index 216ceec..2befe6d 100644
--- a/src/kompsos-pretty_print.adb
+++ b/src/kompsos-pretty_print.adb
@@ -119,9 +119,11 @@ package body Kompsos.Pretty_Print is
Marker : State_Component_Access := Item.Ctrl.Actual;
begin
while Marker /= null loop
- SU.Append (Result, Latin.HT &
- Image (Marker.Key) & " => " &
- Image (Marker.Value) & Latin.LF);
+ for Index in Valid_Count range Valid_Count'First .. Marker.Valid loop
+ SU.Append (Result, Latin.HT &
+ Image (Marker.Data (Index).Key) & " => " &
+ Image (Marker.Data (Index).Value) & Latin.LF);
+ end loop;
Marker := Marker.Next.Ctrl.Actual;
end loop;
end;
diff --git a/src/kompsos.adb b/src/kompsos.adb
index 2efa69b..97e8ce6 100644
--- a/src/kompsos.adb
+++ b/src/kompsos.adb
@@ -252,10 +252,12 @@ package body Kompsos is
Ptr : State_Component_Access := This.Ctrl.Actual;
begin
while Ptr /= null loop
- if Ptr.Key = Key then
- Value := Term'Class (Ptr.Value);
- return True;
- end if;
+ for Index in Valid_Count range Valid_Count'First .. Ptr.Valid loop
+ if Ptr.Data (Index).Key = Key then
+ Value := Term'Class (Ptr.Data (Index).Value);
+ return True;
+ end if;
+ end loop;
Ptr := Ptr.Next.Ctrl.Actual;
end loop;
return False;
@@ -608,20 +610,23 @@ package body Kompsos is
begin
if Subst.Ctrl.Actual = null then
return Empty_Term;
- else
- declare
- Min_Pos : State_Component_Access := Subst.Ctrl.Actual;
- Marker : State_Component_Access := Min_Pos.Next.Ctrl.Actual;
- begin
- while Marker /= null loop
- if Marker.Key < Min_Pos.Key then
+ end if;
+ declare
+ Min_Pos : State_Component_Access := Subst.Ctrl.Actual;
+ Min_Ind : Valid_Count := Valid_Count'First;
+ Marker : State_Component_Access := Min_Pos;
+ begin
+ while Marker /= null loop
+ for Index in Valid_Count range Valid_Count'First .. Marker.Valid loop
+ if Marker.Data (Index).Key < Min_Pos.Data (Min_Ind).Key then
Min_Pos := Marker;
+ Min_Ind := Index;
end if;
- Marker := Marker.Next.Ctrl.Actual;
end loop;
- return Min_Pos.Value.Resolve (Subst);
- end;
- end if;
+ Marker := Marker.Next.Ctrl.Actual;
+ end loop;
+ return Min_Pos.Data (Min_Ind).Value.Resolve (Subst);
+ end;
end Resolve_First;
diff --git a/src/kompsos.ads b/src/kompsos.ads
index d1e19be..b8629fb 100644
--- a/src/kompsos.ads
+++ b/src/kompsos.ads
@@ -459,11 +459,23 @@ private
+ type Binding is record
+ Key : Variable;
+ Value : Term;
+ end record;
+
+ type Binding_Array is array (Positive range <>) of Binding;
+
+ -- Values of 2, 3, 4 here are honestly fairly similar, but of those, 4 seems to work best
+ Unroll_Max : constant Integer := 4;
+
+ subtype Valid_Count is Integer range 1 .. Unroll_Max;
+
type State_Component is limited record
Counter : Natural;
- Key : Variable;
- Value : Term;
- Next : aliased State;
+ Valid : Valid_Count;
+ Data : Binding_Array (Valid_Count'Range);
+ Next : State;
end record;
type State_Component_Access is access State_Component;