diff options
| -rw-r--r-- | src/kompsos-collector.adb | 46 | ||||
| -rw-r--r-- | src/kompsos-collector.ads | 8 | ||||
| -rw-r--r-- | src/kompsos-pretty_print.adb | 4 | ||||
| -rw-r--r-- | src/kompsos-pretty_print.ads | 2 | ||||
| -rw-r--r-- | src/kompsos.adb | 159 | ||||
| -rw-r--r-- | src/kompsos.ads | 49 |
6 files changed, 150 insertions, 118 deletions
diff --git a/src/kompsos-collector.adb b/src/kompsos-collector.adb index 7ccdb57..592979f 100644 --- a/src/kompsos-collector.adb +++ b/src/kompsos-collector.adb @@ -44,6 +44,8 @@ package body Kompsos.Collector is Book : Eval_Maps.Map renames Bookkeep.Actual; + Global_Var : Variable := Relation.Next_Var; + Next_Index : Long_Positive := 1; Next_State : State; State_Valid : Boolean := False; @@ -139,7 +141,11 @@ package body Kompsos.Collector is procedure Reset - (Ptr : in Constant_Goal_Access) is + (Ptr : in Constant_Goal_Access); + + + procedure Do_Reset + (Ptr : in Constant_Graph_Access) is begin if Ptr = null or else Ptr.Actual = null then return; @@ -150,11 +156,11 @@ package body Kompsos.Collector is case Ptr.Actual.Kind is when Unify_Node => Book.Exclude (Ptr.Actual); - Reset (Ptr.Actual.Uni_Goal'Unchecked_Access); + Do_Reset (Ptr.Actual.Uni_Goal'Unchecked_Access); when Disjunct_Node => Book.Exclude (Ptr.Actual); - Reset (Ptr.Actual.Dis_Goal1'Unchecked_Access); - Reset (Ptr.Actual.Dis_Goal2'Unchecked_Access); + Do_Reset (Ptr.Actual.Dis_Goal1'Unchecked_Access); + Do_Reset (Ptr.Actual.Dis_Goal2'Unchecked_Access); when Conjunct_Node => if Book.Contains (Ptr.Actual) then Reset (Constant_Goal_Access (Book.Element (Ptr.Actual).Con_Part)); @@ -162,16 +168,27 @@ package body Kompsos.Collector is Free (Book (Ptr.Actual).Con_Base); Book.Delete (Ptr.Actual); end if; - Reset (Ptr.Actual.Con_Goal'Unchecked_Access); + Do_Reset (Ptr.Actual.Con_Goal'Unchecked_Access); when Recurse_Node => Book.Exclude (Ptr.Actual); - Reset (Ptr.Actual.Rec_Goal'Unchecked_Access); + Do_Reset (Ptr.Actual.Rec_Goal'Unchecked_Access); end case; + end Do_Reset; + + + procedure Reset + (Ptr : in Constant_Goal_Access) is + begin + if Ptr = null then + return; + else + Do_Reset (Ptr.Graph'Access); + end if; end Reset; function Get_Next - (Ptr : in Constant_Goal_Access; + (Ptr : in Constant_Graph_Access; Base : in State; Index : in Long_Positive; Result : out State) @@ -179,7 +196,7 @@ package body Kompsos.Collector is function Do_Get_Next - (Ptr : in Goal_Component_Access; + (Ptr : in Graph_Component_Access; Base : in State; Index : in Long_Positive; Result : out State) @@ -295,14 +312,19 @@ package body Kompsos.Collector is Book (Ptr).Con_Gone := True; else Book (Ptr).Con_Base := new State'(Result); - Book (Ptr).Con_Part := new Goal'(Call_Lazy (Empty_Goal, Ptr.Con_Data)); + Book (Ptr).Con_Part := new Goal'( + Call_Lazy + ((Graph => (Ada.Finalization.Controlled with Actual => null), + Next_Var => Global_Var), + Ptr.Con_Data)); + Global_Var := Book (Ptr).Con_Part.Next_Var; end if; end if; if Book (Ptr).Con_Gone then return False; end if; while not Get_Next - (Constant_Goal_Access (Book.Element (Ptr).Con_Part), + (Constant_Graph_Access'(Book.Element (Ptr).Con_Part.Graph'Access), Book.Element (Ptr).Con_Base.all, Book.Element (Ptr).Con_Next, Result) @@ -363,7 +385,7 @@ package body Kompsos.Collector is function Get_Next - (Ptr : in Constant_Goal_Access; + (Ptr : in Constant_Graph_Access; Base : in State; Index : in Long_Positive; Result : out State) @@ -406,7 +428,7 @@ package body Kompsos.Collector is function Has_Next return Boolean is - Ptr : constant Constant_Goal_Access := Relation'Access; + Ptr : constant Constant_Graph_Access := Relation.Graph'Access; begin if State_Valid then return True; diff --git a/src/kompsos-collector.ads b/src/kompsos-collector.ads index 4ee9402..b58721a 100644 --- a/src/kompsos-collector.ads +++ b/src/kompsos-collector.ads @@ -39,9 +39,11 @@ private type Goal_Access is access all Goal; - type Constant_Goal_Access is access constant Goal; + type Graph_Access is access all Goal_Graph; + type Constant_Graph_Access is access constant Goal_Graph; + type State_Access is access State; type Eval_Kind is @@ -74,7 +76,7 @@ private end record; package Eval_Maps is new Ada.Containers.Ordered_Maps - (Key_Type => Goal_Component_Access, + (Key_Type => Graph_Component_Access, Element_Type => Eval_Data); type Managed_Map is new Ada.Finalization.Controlled with record @@ -91,7 +93,7 @@ private Element_Type => State); package Cache_Maps is new Ada.Containers.Ordered_Maps - (Key_Type => Goal_Component_Access, + (Key_Type => Graph_Component_Access, Element_Type => State_Vectors.Vector, "=" => State_Vectors."="); diff --git a/src/kompsos-pretty_print.adb b/src/kompsos-pretty_print.adb index 3171164..3a65fb9 100644 --- a/src/kompsos-pretty_print.adb +++ b/src/kompsos-pretty_print.adb @@ -153,7 +153,7 @@ package body Kompsos.Pretty_Print is -------------------------------- procedure Do_Structure_DOT - (This : in Goal; + (This : in Goal_Graph; Nodes : in out DOT_Node_Maps.Map; Next : in out Long_Natural; Result : in out SU.Unbounded_String) is @@ -226,7 +226,7 @@ package body Kompsos.Pretty_Print is SU.Append (Result, Name & " "); end if; SU.Append (Result, "{" & Latin.LF); - Do_Structure_DOT (This, Nodes, Next_ID, Result); + Do_Structure_DOT (This.Graph, Nodes, Next_ID, Result); SU.Append (Result, "}"); return SU.To_String (Result); end Structure_DOT; diff --git a/src/kompsos-pretty_print.ads b/src/kompsos-pretty_print.ads index 23c525e..2e32fb8 100644 --- a/src/kompsos-pretty_print.ads +++ b/src/kompsos-pretty_print.ads @@ -62,7 +62,7 @@ private package DOT_Node_Maps is new Ada.Containers.Ordered_Maps - (Key_Type => Goal_Component_Access, + (Key_Type => Graph_Component_Access, Element_Type => Long_Natural); diff --git a/src/kompsos.adb b/src/kompsos.adb index 080683b..4a34b1b 100644 --- a/src/kompsos.adb +++ b/src/kompsos.adb @@ -55,20 +55,20 @@ package body Kompsos is - -- Goals -- + -- Goal Graphs -- - procedure Free is new Ada.Unchecked_Deallocation (Goal_Component, Goal_Component_Access); + procedure Free is new Ada.Unchecked_Deallocation (Graph_Component, Graph_Component_Access); procedure Initialize - (This : in out Goal) is + (This : in out Goal_Graph) is begin This.Actual := null; end Initialize; procedure Adjust - (This : in out Goal) is + (This : in out Goal_Graph) is begin if This.Actual /= null then This.Actual.Counter := This.Actual.Counter + 1; @@ -77,7 +77,7 @@ package body Kompsos is procedure Finalize - (This : in out Goal) is + (This : in out Goal_Graph) is begin if This.Actual /= null then This.Actual.Counter := This.Actual.Counter - 1; @@ -209,43 +209,24 @@ package body Kompsos is - -- Goals -- + -- Goal Graphs -- - package Goal_Convert is new System.Address_To_Access_Conversions (Goal_Component); + package Graph_Convert is new System.Address_To_Access_Conversions (Graph_Component); function "<" - (Left, Right : in Goal_Component_Access) + (Left, Right : in Graph_Component_Access) return Boolean is use System.Storage_Elements; begin return - To_Integer (Goal_Convert.To_Address (Goal_Convert.Object_Pointer (Left))) < - To_Integer (Goal_Convert.To_Address (Goal_Convert.Object_Pointer (Right))); + To_Integer (Graph_Convert.To_Address (Graph_Convert.Object_Pointer (Left))) < + To_Integer (Graph_Convert.To_Address (Graph_Convert.Object_Pointer (Right))); end "<"; - ------------------------ - -- Internal Helpers -- - ------------------------ - - -- Variables -- - - Next_Variable : Variable := Variable'First; - - function Next_Gen - return Variable is - begin - return Result : constant Variable := Next_Variable do - Next_Variable := Next_Variable + 1; - end return; - end Next_Gen; - - - - ------------------- -- microKanren -- ------------------- @@ -256,7 +237,9 @@ package body Kompsos is (This : in out Goal'Class) return Term is begin - return Term (T (Next_Gen)); + return Result : constant Term := Term (T (This.Next_Var)) do + This.Next_Var := This.Next_Var + 1; + end return; end Fresh; @@ -307,13 +290,15 @@ package body Kompsos is Left, Right : in Term'Class) return Goal is begin - return Result : constant Goal := (Ada.Finalization.Controlled with - Actual => new Goal_Component'( - (Kind => Unify_Node, - Counter => 1, - Uni_Goal => This, - Uni_Term1 => Term (Left), - Uni_Term2 => Term (Right)))); + return Result : constant Goal := + (Graph => (Ada.Finalization.Controlled with + Actual => new Graph_Component'( + (Kind => Unify_Node, + Counter => 1, + Uni_Goal => This.Graph, + Uni_Term1 => Term (Left), + Uni_Term2 => Term (Right)))), + Next_Var => This.Next_Var); end Unify; @@ -332,12 +317,14 @@ package body Kompsos is (Left, Right : in Goal) return Goal is begin - return Result : constant Goal := (Ada.Finalization.Controlled with - Actual => new Goal_Component'( - (Kind => Disjunct_Node, - Counter => 1, - Dis_Goal1 => Left, - Dis_Goal2 => Right))); + return Result : constant Goal := + (Graph => (Ada.Finalization.Controlled with + Actual => new Graph_Component'( + (Kind => Disjunct_Node, + Counter => 1, + Dis_Goal1 => Left.Graph, + Dis_Goal2 => Right.Graph))), + Next_Var => Variable'Max (Left.Next_Var, Right.Next_Var)); end Disjunct; @@ -354,16 +341,22 @@ package body Kompsos is return Goal is begin if Inputs'Length = 0 then - return (Ada.Finalization.Controlled with Actual => null); + return Empty_Goal; elsif Inputs'Length = 1 then return Inputs (Inputs'First); else - return Result : constant Goal := (Ada.Finalization.Controlled with - Actual => new Goal_Component'( - (Kind => Disjunct_Node, - Counter => 1, - Dis_Goal1 => Inputs (Inputs'First), - Dis_Goal2 => Disjunct (Inputs (Inputs'First + 1 .. Inputs'Last))))); + declare + Rest : constant Goal := Disjunct (Inputs (Inputs'First + 1 .. Inputs'Last)); + begin + return Result : constant Goal := + (Graph => (Ada.Finalization.Controlled with + Actual => new Graph_Component'( + (Kind => Disjunct_Node, + Counter => 1, + Dis_Goal1 => Inputs (Inputs'First).Graph, + Dis_Goal2 => Rest.Graph))), + Next_Var => Variable'Max (Inputs (Inputs'First).Next_Var, Rest.Next_Var)); + end; end if; end Disjunct; @@ -384,12 +377,14 @@ package body Kompsos is Func : in Junction_Zero_Func) return Goal is begin - return Result : constant Goal := (Ada.Finalization.Controlled with - Actual => new Goal_Component'( - (Kind => Conjunct_Node, - Counter => 1, - Con_Goal => This, - Con_Data => Lazy_Holders.To_Holder ((Kind => Zero_Arg, ZFunc => Func))))); + return Result : constant Goal := + (Graph => (Ada.Finalization.Controlled with + Actual => new Graph_Component'( + (Kind => Conjunct_Node, + Counter => 1, + Con_Goal => This.Graph, + Con_Data => Lazy_Holders.To_Holder ((Kind => Zero_Arg, ZFunc => Func))))), + Next_Var => This.Next_Var); end Conjunct; @@ -407,15 +402,17 @@ package body Kompsos is Input : in Term'Class) return Goal is begin - return Result : constant Goal := (Ada.Finalization.Controlled with - Actual => new Goal_Component'( - (Kind => Conjunct_Node, - Counter => 1, - Con_Goal => This, - Con_Data => Lazy_Holders.To_Holder - ((Kind => One_Arg, - OFunc => Func, - OInput => Term (Input)))))); + return Result : constant Goal := + (Graph => (Ada.Finalization.Controlled with + Actual => new Graph_Component'( + (Kind => Conjunct_Node, + Counter => 1, + Con_Goal => This.Graph, + Con_Data => Lazy_Holders.To_Holder + ((Kind => One_Arg, + OFunc => Func, + OInput => Term (Input)))))), + Next_Var => This.Next_Var); end Conjunct; @@ -434,15 +431,17 @@ package body Kompsos is Inputs : in Term_Array) return Goal is begin - return Result : constant Goal := (Ada.Finalization.Controlled with - Actual => new Goal_Component'( - (Kind => Conjunct_Node, - Counter => 1, - Con_Goal => This, - Con_Data => Lazy_Holders.To_Holder - ((Kind => Many_Arg, - MFunc => Func, - MInput => Term_Array_Holders.To_Holder (Inputs)))))); + return Result : constant Goal := + (Graph => (Ada.Finalization.Controlled with + Actual => new Graph_Component'( + (Kind => Conjunct_Node, + Counter => 1, + Con_Goal => This.Graph, + Con_Data => Lazy_Holders.To_Holder + ((Kind => Many_Arg, + MFunc => Func, + MInput => Term_Array_Holders.To_Holder (Inputs)))))), + Next_Var => This.Next_Var); end Conjunct; @@ -467,11 +466,13 @@ package body Kompsos is (This : in Goal) return Goal is begin - return Result : constant Goal := (Ada.Finalization.Controlled with - Actual => new Goal_Component'( - (Kind => Recurse_Node, - Counter => 1, - Rec_Goal => This))); + return Result : constant Goal := + (Graph => (Ada.Finalization.Controlled with + Actual => new Graph_Component'( + (Kind => Recurse_Node, + Counter => 1, + Rec_Goal => This.Graph))), + Next_Var => This.Next_Var); end Recurse; diff --git a/src/kompsos.ads b/src/kompsos.ads index 32cfc24..9ab7994 100644 --- a/src/kompsos.ads +++ b/src/kompsos.ads @@ -475,14 +475,27 @@ private - type Goal_Component; + type Graph_Component; - type Goal_Component_Access is access Goal_Component; + type Graph_Component_Access is access Graph_Component; function "<" - (Left, Right : in Goal_Component_Access) + (Left, Right : in Graph_Component_Access) return Boolean; + type Goal_Graph is new Ada.Finalization.Controlled with record + Actual : Graph_Component_Access := null; + end record; + + overriding procedure Initialize + (This : in out Goal_Graph); + + overriding procedure Adjust + (This : in out Goal_Graph); + + overriding procedure Finalize + (This : in out Goal_Graph); + type Lazy_Kind is (Zero_Arg, One_Arg, Many_Arg); type Lazy_Data (Kind : Lazy_Kind) is record @@ -506,38 +519,32 @@ private Conjunct_Node, Recurse_Node); - type Goal_Component (Kind : Node_Kind) is limited record + type Graph_Component (Kind : Node_Kind) is limited record Counter : Natural; case Kind is when Unify_Node => - Uni_Goal : aliased Goal; + Uni_Goal : aliased Goal_Graph; Uni_Term1 : Term; Uni_Term2 : Term; when Disjunct_Node => - Dis_Goal1 : aliased Goal; - Dis_Goal2 : aliased Goal; + Dis_Goal1 : aliased Goal_Graph; + Dis_Goal2 : aliased Goal_Graph; when Conjunct_Node => - Con_Goal : aliased Goal; + Con_Goal : aliased Goal_Graph; Con_Data : Lazy_Holders.Holder; when Recurse_Node => - Rec_Goal : aliased Goal; + Rec_Goal : aliased Goal_Graph; end case; end record; - type Goal is new Ada.Finalization.Controlled with record - Actual : Goal_Component_Access := null; + type Goal is tagged record + Graph : aliased Goal_Graph := (Ada.Finalization.Controlled with Actual => null); + Next_Var : Variable := Variable'First; end record; - overriding procedure Initialize - (This : in out Goal); - - overriding procedure Adjust - (This : in out Goal); - - overriding procedure Finalize - (This : in out Goal); - - Empty_Goal : constant Goal := (Ada.Finalization.Controlled with Actual => null); + Empty_Goal : constant Goal := + (Graph => (Ada.Finalization.Controlled with Actual => null), + Next_Var => Variable'First); end Kompsos; |