From 826b9d2dad1031a3eca29dd2fb8b6643e53e5fc1 Mon Sep 17 00:00:00 2001 From: Jedidiah Barber Date: Sun, 14 Dec 2025 19:53:01 +1300 Subject: Core rewritten with memoisation, but somehow Zebra example is bugged --- src/kompsos.ads | 131 ++++++++++++++++++++++++-------------------------------- 1 file changed, 57 insertions(+), 74 deletions(-) (limited to 'src/kompsos.ads') diff --git a/src/kompsos.ads b/src/kompsos.ads index 0483fa1..e9bbefd 100644 --- a/src/kompsos.ads +++ b/src/kompsos.ads @@ -252,32 +252,21 @@ package Kompsos is (This : in out World); - -- Forced Evaluation -- + -- Evaluation -- function Take - (This : in out World; - Count : in Positive) + (This : in World; + Count : in Positive) return State_Array; function Take_First - (This : in out World) + (This : in World) return State; function Take_All - (This : in out World) + (This : in World) return State_Array; - procedure Force - (This : in out World; - Count : in Positive); - - procedure Force_All - (This : in out World); - - function Failed - (This : in out World) - return Boolean; - -- Reification -- @@ -473,10 +462,11 @@ private -- around 2^31 possible Variables should be enough for anybody, right? - type ID_Number is new Long_Integer range 0 .. Long_Integer'Last; + subtype Long_Natural is Long_Integer range 0 .. Long_Integer'Last; + subtype Long_Positive is Long_Integer range 1 .. Long_Integer'Last; - type Generator_ID_Number is new ID_Number; - type Variable_ID_Number is new ID_Number; + type Generator_ID_Number is new Long_Natural; + type Variable_ID_Number is new Long_Natural; type Variable is record Ident : Generator_ID_Number; @@ -490,9 +480,9 @@ private type Term_Component_Access is access Term_Component; - subtype Non_Null_Term_Kind is Term_Kind range Atom_Term .. Pair_Term; + subtype Not_Null_Term_Kind is Term_Kind range Atom_Term .. Pair_Term; - type Term_Component (Kind : Non_Null_Term_Kind) is limited record + type Term_Component (Kind : Not_Null_Term_Kind) is limited record Counter : Natural; case Kind is when Atom_Term => @@ -500,7 +490,8 @@ private when Var_Term => Refer : Variable; when Pair_Term => - Left, Right : Term; + Left : Term; + Right : Term; end case; end record; @@ -552,6 +543,10 @@ private Subst : Binding_Maps.Map; end record; + package State_Vectors is new Ada.Containers.Vectors + (Index_Type => Long_Positive, + Element_Type => State); + Empty_State : constant State := (Ident => ID_Number_Maps.Empty_Map, LVars => Name_Vectors.Empty_Vector, @@ -560,16 +555,9 @@ private - type World_Root is abstract tagged null record; - - package World_Holders is new Ada.Containers.Indefinite_Holders (World_Root'Class); + type World_Component; - type World_Access is access all World; - - function Hold - (This : in World) - return World_Holders.Holder - with Inline; + type World_Component_Access is access World_Component; type Lazy_Kind is (Zero_Arg, One_Arg, Many_Arg); @@ -588,64 +576,59 @@ private package Lazy_Holders is new Ada.Containers.Indefinite_Holders (Lazy_Data); - type Generator_Kind is - (No_Gen, - Fresh_Gen, - Unify_Gen, - Disjunct_Gen, - Conjunct_Gen, - Recurse_Gen); + type Node_Kind is + (Static_Node, + Fresh_Node, + Unify_Node, + Disjunct_Node, + Conjunct_Node, + Recurse_Node); - type Generator (Kind : Generator_Kind := No_Gen) is record + type World_Component (Kind : Node_Kind) is limited record + Counter : Natural; case Kind is - when No_Gen => - null; - when Fresh_Gen => - Frs_Ident : Generator_ID_Number; - Frs_World : World_Holders.Holder; - Frs_Name : Nametag; - when Unify_Gen => - Uni_World : World_Holders.Holder; + when Static_Node => + Stc_States : State_Vectors.Vector; + when Fresh_Node => + Frs_World : aliased World; + Frs_Var : Variable; + when Unify_Node => + Uni_World : aliased World; Uni_Term1 : Term; Uni_Term2 : Term; - when Disjunct_Gen => - Dis_World1 : World_Holders.Holder; - Dis_World2 : World_Holders.Holder; - when Conjunct_Gen => - Con_World : World_Holders.Holder; + when Disjunct_Node => + Dis_World1 : aliased World; + Dis_World2 : aliased World; + when Conjunct_Node => + Con_World : aliased World; Con_Data : Lazy_Holders.Holder; - when Recurse_Gen => - Rec_World : World_Holders.Holder; - Rec_Index : Positive; + when Recurse_Node => + Rec_World : aliased World; end case; end record; - package State_Vectors is new Ada.Containers.Vectors - (Index_Type => Positive, - Element_Type => State); - - type World is new World_Root with record - Possibles : State_Vectors.Vector; - Engine : Generator; + type World is new Ada.Finalization.Controlled with record + Actual : World_Component_Access := null; end record; - function Has_State - (This : in out World; - Index : in Positive) - return Boolean; + overriding procedure Initialize + (This : in out World); - procedure Rollover + overriding procedure Adjust (This : in out World); - procedure Roll_Until - (This : in out World; - Index : in Positive); + overriding procedure Finalize + (This : in out World); - use type State_Vectors.Vector; + function Static + (Item : in State) + return World'Class; - Empty_World : constant World := - (Possibles => State_Vectors.Empty_Vector & Empty_State, - Engine => (Kind => No_Gen)); + Empty_World : constant World := (Ada.Finalization.Controlled with + Actual => new World_Component'( + (Kind => Static_Node, + Counter => 1, + Stc_States => State_Vectors."&" (State_Vectors.Empty_Vector, Empty_State)))); end Kompsos; -- cgit