diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/kompsos-collector.adb | 101 | ||||
| -rw-r--r-- | src/kompsos-collector.ads | 17 | ||||
| -rw-r--r-- | src/kompsos-pretty_print.adb | 44 | ||||
| -rw-r--r-- | src/kompsos-pretty_print.ads | 6 | ||||
| -rw-r--r-- | src/kompsos.adb | 307 | ||||
| -rw-r--r-- | src/kompsos.ads | 210 |
6 files changed, 340 insertions, 345 deletions
diff --git a/src/kompsos-collector.adb b/src/kompsos-collector.adb index d7c40eb..e2ee677 100644 --- a/src/kompsos-collector.adb +++ b/src/kompsos-collector.adb @@ -17,14 +17,15 @@ package body Kompsos.Collector is -- Memory Management -- ------------------------- - procedure Free is new Ada.Unchecked_Deallocation (World, World_Access); - + procedure Free is new Ada.Unchecked_Deallocation (Goal, Goal_Access); + procedure Free is new Ada.Unchecked_Deallocation (State, State_Access); procedure Finalize (This : in out Managed_Map) is begin for Datum of This.Actual loop if Datum.Kind = Conjunct_Data then + Free (Datum.Con_Base); Free (Datum.Con_Part); end if; end loop; @@ -138,12 +139,8 @@ package body Kompsos.Collector is -- Unify Pair Terms by unifying each corresponding part if Real_Left.Kind = Pair_Term and then Real_Right.Kind = Pair_Term then - declare - Middle : State; - begin - return Do_Unify (Potential, Real_Left.Left, Real_Right.Left, Middle) and then - Do_Unify (Middle, Real_Left.Right, Real_Right.Right, Extended); - end; + return Do_Unify (Potential, Real_Left.Left, Real_Right.Left, Extended) and then + Do_Unify (Extended, Real_Left.Right, Real_Right.Right, Extended); end if; -- Not sure how things get here, but if all else fails @@ -155,9 +152,9 @@ package body Kompsos.Collector is -- Result Collection -- function Call_Lazy - (This : in World; + (This : in Goal; Data : in Lazy_Holders.Holder) - return World + return Goal is Ref : constant Lazy_Holders.Constant_Reference_Type := Data.Constant_Reference; begin @@ -173,7 +170,7 @@ package body Kompsos.Collector is procedure Reset - (Ptr : in Constant_World_Access) is + (Ptr : in Constant_Goal_Access) is begin if Ptr = null or else Ptr.Actual = null then return; @@ -185,53 +182,55 @@ package body Kompsos.Collector is when Static_Node => return; when Fresh_Node => - Reset (Ptr.Actual.Frs_World'Unchecked_Access); + Reset (Ptr.Actual.Frs_Goal'Unchecked_Access); when Unify_Node => Book.Exclude (Ptr.Actual); - Reset (Ptr.Actual.Uni_World'Unchecked_Access); + Reset (Ptr.Actual.Uni_Goal'Unchecked_Access); when Disjunct_Node => Book.Exclude (Ptr.Actual); - Reset (Ptr.Actual.Dis_World1'Unchecked_Access); - Reset (Ptr.Actual.Dis_World2'Unchecked_Access); + Reset (Ptr.Actual.Dis_Goal1'Unchecked_Access); + Reset (Ptr.Actual.Dis_Goal2'Unchecked_Access); when Conjunct_Node => if Book.Contains (Ptr.Actual) then - Reset (Constant_World_Access (Book.Element (Ptr.Actual).Con_Part)); + Reset (Constant_Goal_Access (Book.Element (Ptr.Actual).Con_Part)); Free (Book (Ptr.Actual).Con_Part); Free (Book (Ptr.Actual).Con_Base); Book.Delete (Ptr.Actual); end if; - Reset (Ptr.Actual.Con_World'Unchecked_Access); + Reset (Ptr.Actual.Con_Goal'Unchecked_Access); when Recurse_Node => Book.Exclude (Ptr.Actual); - Reset (Ptr.Actual.Rec_World'Unchecked_Access); + Reset (Ptr.Actual.Rec_Goal'Unchecked_Access); end case; end Reset; function Get_Next - (Ptr : in Constant_World_Access; + (Ptr : in Constant_Goal_Access; + Base : in State; Index : in Long_Positive; Result : out State) return Boolean; function Do_Get_Next - (Ptr : in World_Component_Access; + (Ptr : in Goal_Component_Access; + Base : in State; Index : in Long_Positive; Result : out State) return Boolean is begin case Ptr.Kind is when Static_Node => - if Index <= Ptr.Stc_States.Last_Index then - Result := Ptr.Stc_States (Index); + if Index = 1 then + Result := Base; return True; else return False; end if; when Fresh_Node => - if Get_Next (Ptr.Frs_World'Unchecked_Access, Index, Result) then + if Get_Next (Ptr.Frs_Goal'Unchecked_Access, Base, Index, Result) then Result.LVars.Append (Ptr.Frs_Var.Name); Result.Ident.Insert (Ptr.Frs_Var.Ident, Result.LVars.Last_Index); return True; @@ -244,7 +243,8 @@ package body Kompsos.Collector is Book.Insert (Ptr, (Kind => Unify_Data, others => <>)); end if; while Get_Next - (Ptr.Uni_World'Unchecked_Access, + (Ptr.Uni_Goal'Unchecked_Access, + Base, Index + Book.Element (Ptr).Uni_Offset, Result) loop @@ -264,7 +264,8 @@ package body Kompsos.Collector is if Book.Element (Ptr).Dis_Gone2 then return False; elsif Get_Next - (Ptr.Dis_World2'Unchecked_Access, + (Ptr.Dis_Goal2'Unchecked_Access, + Base, Book.Element (Ptr).Dis_Next2, Result) then @@ -276,7 +277,8 @@ package body Kompsos.Collector is end if; elsif Book.Element (Ptr).Dis_Gone2 then if Get_Next - (Ptr.Dis_World1'Unchecked_Access, + (Ptr.Dis_Goal1'Unchecked_Access, + Base, Book.Element (Ptr).Dis_Next1, Result) then @@ -288,7 +290,8 @@ package body Kompsos.Collector is end if; elsif Book.Element (Ptr).Dis_Flag then if Get_Next - (Ptr.Dis_World1'Unchecked_Access, + (Ptr.Dis_Goal1'Unchecked_Access, + Base, Book.Element (Ptr).Dis_Next1, Result) then @@ -298,7 +301,8 @@ package body Kompsos.Collector is else Book (Ptr).Dis_Gone1 := True; if Get_Next - (Ptr.Dis_World2'Unchecked_Access, + (Ptr.Dis_Goal2'Unchecked_Access, + Base, Book.Element (Ptr).Dis_Next2, Result) then @@ -311,7 +315,8 @@ package body Kompsos.Collector is end if; else if Get_Next - (Ptr.Dis_World2'Unchecked_Access, + (Ptr.Dis_Goal2'Unchecked_Access, + Base, Book.Element (Ptr).Dis_Next2, Result) then @@ -321,7 +326,8 @@ package body Kompsos.Collector is else Book (Ptr).Dis_Gone2 := True; if Get_Next - (Ptr.Dis_World1'Unchecked_Access, + (Ptr.Dis_Goal1'Unchecked_Access, + Base, Book.Element (Ptr).Dis_Next1, Result) then @@ -337,29 +343,30 @@ package body Kompsos.Collector is when Conjunct_Node => if not Book.Contains (Ptr) then Book.Insert (Ptr, (Kind => Conjunct_Data, others => <>)); - if not Get_Next (Ptr.Con_World'Unchecked_Access, 1, Result) then + if not Get_Next (Ptr.Con_Goal'Unchecked_Access, Base, 1, Result) then Book (Ptr).Con_Gone := True; else - Book (Ptr).Con_Base := new World'(World (Static (Result))); - Book (Ptr).Con_Part := new World'(Call_Lazy - (Book.Element (Ptr).Con_Base.all, Ptr.Con_Data)); + Book (Ptr).Con_Base := new State'(Result); + Book (Ptr).Con_Part := new Goal'(Call_Lazy (Empty_Goal, Ptr.Con_Data)); end if; end if; if Book (Ptr).Con_Gone then return False; end if; while not Get_Next - (Constant_World_Access (Book.Element (Ptr).Con_Part), + (Constant_Goal_Access (Book.Element (Ptr).Con_Part), + Book.Element (Ptr).Con_Base.all, Book.Element (Ptr).Con_Next, Result) loop - Reset (Constant_World_Access (Book.Element (Ptr).Con_Part)); + Reset (Constant_Goal_Access (Book.Element (Ptr).Con_Part)); if Get_Next - (Ptr.Con_World'Unchecked_Access, + (Ptr.Con_Goal'Unchecked_Access, + Base, Book.Element (Ptr).Con_From, Result) then - Book (Ptr).Con_Base.Actual.Stc_States (1) := Result; + Book (Ptr).Con_Base.all := Result; Book (Ptr).Con_Next := 1; Book (Ptr).Con_From := Book.Element (Ptr).Con_From + 1; else @@ -380,7 +387,8 @@ package body Kompsos.Collector is return False; end if; while not Get_Next - (Ptr.Rec_World'Unchecked_Access, + (Ptr.Rec_Goal'Unchecked_Access, + Base, Book.Element (Ptr).Rec_Next, Result) loop @@ -398,7 +406,7 @@ package body Kompsos.Collector is function Cached - (Ptr : in World_Component_Access; + (Ptr : in Goal_Component_Access; Index : in Long_Positive; Result : out State) return Boolean is @@ -413,7 +421,7 @@ package body Kompsos.Collector is procedure Cache_This - (Ptr : in World_Component_Access; + (Ptr : in Goal_Component_Access; Index : in Long_Positive; Result : in State) is begin @@ -428,7 +436,8 @@ package body Kompsos.Collector is function Get_Next - (Ptr : in Constant_World_Access; + (Ptr : in Constant_Goal_Access; + Base : in State; Index : in Long_Positive; Result : out State) return Boolean is @@ -438,7 +447,7 @@ package body Kompsos.Collector is elsif Cached (Ptr.Actual, Index, Result) then return True; else - return Found : constant Boolean := Do_Get_Next (Ptr.Actual, Index, Result) do + return Found : constant Boolean := Do_Get_Next (Ptr.Actual, Base, Index, Result) do if Found then Cache_This (Ptr.Actual, Index, Result); end if; @@ -456,14 +465,14 @@ package body Kompsos.Collector is function Has_Next return Boolean is - Ptr : constant Constant_World_Access := Source'Access; + Ptr : constant Constant_Goal_Access := Relation'Access; begin if State_Valid then return True; elsif Exhausted then return False; else - State_Valid := Get_Next (Ptr, Next_Index, Next_State); + State_Valid := Get_Next (Ptr, Within, Next_Index, Next_State); if not State_Valid then Exhausted := True; else @@ -501,7 +510,7 @@ package body Kompsos.Collector is procedure Reset is - Ptr : constant Constant_World_Access := Source'Access; + Ptr : constant Constant_Goal_Access := Relation'Access; begin Reset (Ptr); Next_Index := 1; diff --git a/src/kompsos-collector.ads b/src/kompsos-collector.ads index d3e22a1..2b175a1 100644 --- a/src/kompsos-collector.ads +++ b/src/kompsos-collector.ads @@ -14,7 +14,8 @@ private with generic - Source : in World; + Relation : in Goal; + Within : in State; package Kompsos.Collector is @@ -37,9 +38,11 @@ package Kompsos.Collector is private - type World_Access is access all World; + type Goal_Access is access all Goal; - type Constant_World_Access is access constant World; + type Constant_Goal_Access is access constant Goal; + + type State_Access is access State; type Eval_Kind is (Unify_Data, @@ -59,8 +62,8 @@ private Dis_Gone2 : Boolean := False; when Conjunct_Data => Con_From : Long_Positive := 2; -- Number one will be obtained by Get_Next already - Con_Base : World_Access := null; - Con_Part : World_Access := null; + Con_Base : State_Access := null; + Con_Part : Goal_Access := null; Con_Next : Long_Positive := 1; Con_Gone : Boolean := False; when Recurse_Data => @@ -70,7 +73,7 @@ private end record; package Eval_Maps is new Ada.Containers.Ordered_Maps - (Key_Type => World_Component_Access, + (Key_Type => Goal_Component_Access, Element_Type => Eval_Data); type Managed_Map is new Ada.Finalization.Controlled with record @@ -81,7 +84,7 @@ private (This : in out Managed_Map); package Cache_Maps is new Ada.Containers.Ordered_Maps - (Key_Type => World_Component_Access, + (Key_Type => Goal_Component_Access, Element_Type => State_Vectors.Vector, "=" => State_Vectors."="); diff --git a/src/kompsos-pretty_print.adb b/src/kompsos-pretty_print.adb index 8d11f81..250c6a6 100644 --- a/src/kompsos-pretty_print.adb +++ b/src/kompsos-pretty_print.adb @@ -150,13 +150,13 @@ package body Kompsos.Pretty_Print is function Image - (Item : in World) + (Item : in Goal) return String is Result : SU.Unbounded_String; Counter : Positive := 1; - package Collect is new Collector (Item); + package Collect is new Collector (Item, Empty_State); begin if not Collect.Has_Next then return "States: N/A" & Latin.LF; @@ -174,7 +174,7 @@ package body Kompsos.Pretty_Print is procedure Do_Structure_DOT - (This : in World; + (This : in Goal; Nodes : in out DOT_Node_Maps.Map; Next : in out Long_Natural; Result : in out SU.Unbounded_String) is @@ -191,62 +191,62 @@ package body Kompsos.Pretty_Print is when Fresh_Node => SU.Append (Result, Latin.HT & "n" & Image (Nodes.Element (This.Actual)) & " [label=""fresh""];" & Latin.LF); - Do_Structure_DOT (This.Actual.Frs_World, Nodes, Next, Result); - if Nodes.Contains (This.Actual.Frs_World.Actual) then + Do_Structure_DOT (This.Actual.Frs_Goal, Nodes, Next, Result); + if Nodes.Contains (This.Actual.Frs_Goal.Actual) then SU.Append (Result, Latin.HT & "n" & Image (Nodes.Element (This.Actual)) & " -> " & - "n" & Image (Nodes.Element (This.Actual.Frs_World.Actual)) & ";" & Latin.LF); + "n" & Image (Nodes.Element (This.Actual.Frs_Goal.Actual)) & ";" & Latin.LF); end if; when Unify_Node => SU.Append (Result, Latin.HT & "n" & Image (Nodes.Element (This.Actual)) & " [label=""unify""];" & Latin.LF); - Do_Structure_DOT (This.Actual.Uni_World, Nodes, Next, Result); - if Nodes.Contains (This.Actual.Uni_World.Actual) then + Do_Structure_DOT (This.Actual.Uni_Goal, Nodes, Next, Result); + if Nodes.Contains (This.Actual.Uni_Goal.Actual) then SU.Append (Result, Latin.HT & "n" & Image (Nodes.Element (This.Actual)) & " -> " & - "n" & Image (Nodes.Element (This.Actual.Uni_World.Actual)) & ";" & Latin.LF); + "n" & Image (Nodes.Element (This.Actual.Uni_Goal.Actual)) & ";" & Latin.LF); end if; when Disjunct_Node => SU.Append (Result, Latin.HT & "n" & Image (Nodes.Element (This.Actual)) & " [label=""disjunct""];" & Latin.LF); - Do_Structure_DOT (This.Actual.Dis_World1, Nodes, Next, Result); - Do_Structure_DOT (This.Actual.Dis_World2, Nodes, Next, Result); - if Nodes.Contains (This.Actual.Dis_World1.Actual) then + Do_Structure_DOT (This.Actual.Dis_Goal1, Nodes, Next, Result); + Do_Structure_DOT (This.Actual.Dis_Goal2, Nodes, Next, Result); + if Nodes.Contains (This.Actual.Dis_Goal1.Actual) then SU.Append (Result, Latin.HT & "n" & Image (Nodes.Element (This.Actual)) & " -> " & - "n" & Image (Nodes.Element (This.Actual.Dis_World1.Actual)) & + "n" & Image (Nodes.Element (This.Actual.Dis_Goal1.Actual)) & " [label=""1""];" & Latin.LF); end if; - if Nodes.Contains (This.Actual.Dis_World2.Actual) then + if Nodes.Contains (This.Actual.Dis_Goal2.Actual) then SU.Append (Result, Latin.HT & "n" & Image (Nodes.Element (This.Actual)) & " -> " & - "n" & Image (Nodes.Element (This.Actual.Dis_World2.Actual)) & + "n" & Image (Nodes.Element (This.Actual.Dis_Goal2.Actual)) & " [label=""2""];" & Latin.LF); end if; when Conjunct_Node => SU.Append (Result, Latin.HT & "n" & Image (Nodes.Element (This.Actual)) & " [label=""conjunct""];" & Latin.LF); - Do_Structure_DOT (This.Actual.Con_World, Nodes, Next, Result); - if Nodes.Contains (This.Actual.Con_World.Actual) then + Do_Structure_DOT (This.Actual.Con_Goal, Nodes, Next, Result); + if Nodes.Contains (This.Actual.Con_Goal.Actual) then SU.Append (Result, Latin.HT & "n" & Image (Nodes.Element (This.Actual)) & " -> " & - "n" & Image (Nodes.Element (This.Actual.Con_World.Actual)) & ";" & Latin.LF); + "n" & Image (Nodes.Element (This.Actual.Con_Goal.Actual)) & ";" & Latin.LF); end if; when Recurse_Node => SU.Append (Result, Latin.HT & "n" & Image (Nodes.Element (This.Actual)) & " [label=""recurse""];" & Latin.LF); - Do_Structure_DOT (This.Actual.Rec_World, Nodes, Next, Result); - if Nodes.Contains (This.Actual.Rec_World.Actual) then + Do_Structure_DOT (This.Actual.Rec_Goal, Nodes, Next, Result); + if Nodes.Contains (This.Actual.Rec_Goal.Actual) then SU.Append (Result, Latin.HT & "n" & Image (Nodes.Element (This.Actual)) & " -> " & - "n" & Image (Nodes.Element (This.Actual.Rec_World.Actual)) & ";" & Latin.LF); + "n" & Image (Nodes.Element (This.Actual.Rec_Goal.Actual)) & ";" & Latin.LF); end if; end case; end Do_Structure_DOT; function Structure_DOT - (This : in World; + (This : in Goal; Name : in String := "") return String is diff --git a/src/kompsos-pretty_print.ads b/src/kompsos-pretty_print.ads index 19da0af..653858b 100644 --- a/src/kompsos-pretty_print.ads +++ b/src/kompsos-pretty_print.ads @@ -35,14 +35,14 @@ package Kompsos.Pretty_Print is return String; function Image - (Item : in World) + (Item : in Goal) return String; function Structure_DOT - (This : in World; + (This : in Goal; Name : in String := "") return String; @@ -60,7 +60,7 @@ private package DOT_Node_Maps is new Ada.Containers.Ordered_Maps - (Key_Type => World_Component_Access, + (Key_Type => Goal_Component_Access, Element_Type => Long_Natural); diff --git a/src/kompsos.adb b/src/kompsos.adb index 476eb86..56c22cd 100644 --- a/src/kompsos.adb +++ b/src/kompsos.adb @@ -55,20 +55,20 @@ package body Kompsos is - -- Worlds -- + -- Goals -- - procedure Free is new Ada.Unchecked_Deallocation (World_Component, World_Component_Access); + procedure Free is new Ada.Unchecked_Deallocation (Goal_Component, Goal_Component_Access); procedure Initialize - (This : in out World) is + (This : in out Goal) is begin This.Actual := null; end Initialize; procedure Adjust - (This : in out World) is + (This : in out Goal) 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 World) is + (This : in out Goal) is begin if This.Actual /= null then This.Actual.Counter := This.Actual.Counter - 1; @@ -215,36 +215,22 @@ package body Kompsos is - -- Worlds -- + -- Goals -- - package World_Convert is new System.Address_To_Access_Conversions (World_Component); + package Goal_Convert is new System.Address_To_Access_Conversions (Goal_Component); function "<" - (Left, Right : in World_Component_Access) + (Left, Right : in Goal_Component_Access) return Boolean is use System.Storage_Elements; begin return - To_Integer (World_Convert.To_Address (World_Convert.Object_Pointer (Left))) < - To_Integer (World_Convert.To_Address (World_Convert.Object_Pointer (Right))); + To_Integer (Goal_Convert.To_Address (Goal_Convert.Object_Pointer (Left))) < + To_Integer (Goal_Convert.To_Address (Goal_Convert.Object_Pointer (Right))); end "<"; - function Static - (Item : in State) - return World'Class - is - use type State_Vectors.Vector; - begin - return Result : constant World := (Ada.Finalization.Controlled with - Actual => new World_Component'( - (Kind => Static_Node, - Counter => 1, - Stc_States => State_Vectors.Empty_Vector & Item))); - end Static; - - ------------------------ @@ -273,7 +259,7 @@ package body Kompsos is -- Variable Introduction -- function Fresh - (This : in out World'Class) + (This : in out Goal'Class) return Term is begin return This.Fresh (+""); @@ -281,7 +267,7 @@ package body Kompsos is function Fresh - (This : in out World'Class; + (This : in out Goal'Class; Name : in String) return Term is begin @@ -290,7 +276,7 @@ package body Kompsos is function Fresh - (This : in out World'Class; + (This : in out Goal'Class; Name : in Nametag) return Term is @@ -298,17 +284,17 @@ package body Kompsos is My_Var : constant Variable := (Ident => My_ID, Name => Name); begin return My_Term : constant Term := Term (T (My_Var)) do - This.Actual := new World_Component'( - (Kind => Fresh_Node, - Counter => 1, - Frs_World => World (This), - Frs_Var => My_Var)); + This.Actual := new Goal_Component'( + (Kind => Fresh_Node, + Counter => 1, + Frs_Goal => Goal (This), + Frs_Var => My_Var)); end return; end Fresh; function Fresh - (This : in out World'Class; + (This : in out Goal'Class; Count : in Positive) return Term_Array is @@ -319,7 +305,7 @@ package body Kompsos is function Fresh - (This : in out World'Class; + (This : in out Goal'Class; Names : in Nametag_Array) return Term_Array is begin @@ -342,17 +328,17 @@ package body Kompsos is -- Unification -- function Unify - (This : in World; + (This : in Goal; Left : in Term'Class; Right : in Element_Type) - return World is + return Goal is begin return This.Unify (Left, T (Right)); end Unify; procedure Unify - (This : in out World; + (This : in out Goal; Left : in Term'Class; Right : in Element_Type) is begin @@ -361,22 +347,22 @@ package body Kompsos is function Unify - (This : in World; + (This : in Goal; Left, Right : in Term'Class) - return World is + return Goal is begin - return Result : constant World := (Ada.Finalization.Controlled with - Actual => new World_Component'( + return Result : constant Goal := (Ada.Finalization.Controlled with + Actual => new Goal_Component'( (Kind => Unify_Node, Counter => 1, - Uni_World => This, + Uni_Goal => This, Uni_Term1 => Term (Left), Uni_Term2 => Term (Right)))); end Unify; procedure Unify - (This : in out World; + (This : in out Goal; Left, Right : in Term'Class) is begin This := This.Unify (Left, Right); @@ -387,52 +373,48 @@ package body Kompsos is -- Combining / Disjunction -- function Disjunct - (Left, Right : in World) - return World is - begin - return Result : constant World := (Ada.Finalization.Controlled with - Actual => new World_Component'( - (Kind => Disjunct_Node, - Counter => 1, - Dis_World1 => Left, - Dis_World2 => Right))); + (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))); end Disjunct; procedure Disjunct - (This : in out World; - Right : in World) is + (This : in out Goal; + Right : in Goal) is begin This := Disjunct (This, Right); end Disjunct; function Disjunct - (Inputs : in World_Array) - return World is + (Inputs : in Goal_Array) + return Goal is begin if Inputs'Length = 0 then - return Result : constant World := (Ada.Finalization.Controlled with - Actual => new World_Component'( - (Kind => Static_Node, - Counter => 1, - Stc_States => State_Vectors.Empty_Vector))); + return (Ada.Finalization.Controlled with Actual => null); elsif Inputs'Length = 1 then return Inputs (Inputs'First); else - return Result : constant World := (Ada.Finalization.Controlled with - Actual => new World_Component'( - (Kind => Disjunct_Node, - Counter => 1, - Dis_World1 => Inputs (Inputs'First), - Dis_World2 => Disjunct (Inputs (Inputs'First + 1 .. Inputs'Last))))); + 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))))); end if; end Disjunct; procedure Disjunct - (This : in out World; - Inputs : in World_Array) is + (This : in out Goal; + Inputs : in Goal_Array) is begin This := Disjunct (This & Inputs); end Disjunct; @@ -442,21 +424,21 @@ package body Kompsos is -- Lazy Sequencing / Conjunction -- function Conjunct - (This : in World; + (This : in Goal; Func : in Junction_Zero_Func) - return World is - begin - return Result : constant World := (Ada.Finalization.Controlled with - Actual => new World_Component'( - (Kind => Conjunct_Node, - Counter => 1, - Con_World => This, - Con_Data => Lazy_Holders.To_Holder ((Kind => Zero_Arg, ZFunc => 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))))); end Conjunct; procedure Conjunct - (This : in out World; + (This : in out Goal; Func : in Junction_Zero_Func) is begin This := This.Conjunct (Func); @@ -464,17 +446,17 @@ package body Kompsos is function Conjunct - (This : in World; + (This : in Goal; Func : in Junction_One_Func; Input : in Term'Class) - return World is - begin - return Result : constant World := (Ada.Finalization.Controlled with - Actual => new World_Component'( - (Kind => Conjunct_Node, - Counter => 1, - Con_World => This, - Con_Data => Lazy_Holders.To_Holder + 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)))))); @@ -482,7 +464,7 @@ package body Kompsos is procedure Conjunct - (This : in out World; + (This : in out Goal; Func : in Junction_One_Func; Input : in Term'Class) is begin @@ -491,17 +473,17 @@ package body Kompsos is function Conjunct - (This : in World; + (This : in Goal; Func : in Junction_Many_Func; Inputs : in Term_Array) - return World is - begin - return Result : constant World := (Ada.Finalization.Controlled with - Actual => new World_Component'( - (Kind => Conjunct_Node, - Counter => 1, - Con_World => This, - Con_Data => Lazy_Holders.To_Holder + 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)))))); @@ -509,7 +491,7 @@ package body Kompsos is procedure Conjunct - (This : in out World; + (This : in out Goal; Func : in Junction_Many_Func; Inputs : in Term_Array) is begin @@ -526,19 +508,19 @@ package body Kompsos is -- Infinite State Loops -- function Recurse - (This : in World) - return World is - begin - return Result : constant World := (Ada.Finalization.Controlled with - Actual => new World_Component'( - (Kind => Recurse_Node, - Counter => 1, - Rec_World => This))); + (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))); end Recurse; procedure Recurse - (This : in out World) is + (This : in out Goal) is begin This := This.Recurse; end Recurse; @@ -547,15 +529,16 @@ package body Kompsos is -- Evaluation -- - function Take - (This : in World; - Count : in Positive) + function Run + (This : in Goal; + Count : in Positive; + Base : in State := Empty_State) return State_Array is Result : State_Array (1 .. Count); Valid : Natural := 0; - package Collect is new Collector (This); + package Collect is new Collector (This, Base); begin for Item of Result loop exit when not Collect.Has_Next; @@ -563,37 +546,39 @@ package body Kompsos is Valid := Valid + 1; end loop; return Result (1 .. Valid); - end Take; + end Run; - function Take_First - (This : in World) + function Run + (This : in Goal; + Base : in State := Empty_State) return State is - package Collect is new Collector (This); + package Collect is new Collector (This, Base); begin return Collect.Next (Empty_State); - end Take_First; + end Run; - function Take_All - (This : in World) + function Run_All + (This : in Goal; + Base : in State := Empty_State) return State_Array is - package Collect is new Collector (This); + package Collect is new Collector (This, Base); - function Do_Take + function Do_Run return State_Array is begin if Collect.Has_Next then - return Collect.Next & Do_Take; + return Collect.Next & Do_Run; else return Result : State_Array (1 .. 0); end if; - end Do_Take; + end Do_Run; begin - return Do_Take; - end Take_All; + return Do_Run; + end Run_All; @@ -685,21 +670,21 @@ package body Kompsos is -- caro -- function Head - (This : in World; + (This : in Goal; Inputs : in Term_Array) - return World + return Goal is List_Term : Term renames Inputs (1); Head_Term : Term renames Inputs (2); begin - return Result : World := This do + return Result : Goal := This do Result.Unify (T (Head_Term, Result.Fresh), List_Term); end return; end Head; procedure Head - (This : in out World; + (This : in out Goal; Inputs : in Term_Array) is begin This := This.Head (Inputs); @@ -710,21 +695,21 @@ package body Kompsos is -- cdro -- function Tail - (This : in World; + (This : in Goal; Inputs : in Term_Array) - return World + return Goal is List_Term : Term renames Inputs (1); Tail_Term : Term renames Inputs (2); begin - return Result : World := This do + return Result : Goal := This do Result.Unify (T (Result.Fresh, Tail_Term), List_Term); end return; end Tail; procedure Tail - (This : in out World; + (This : in out Goal; Inputs : in Term_Array) is begin This := This.Tail (Inputs); @@ -735,22 +720,22 @@ package body Kompsos is -- conso -- function Cons - (This : in World; + (This : in Goal; Inputs : in Term_Array) - return World + return Goal is Head_Term : Term renames Inputs (1); Tail_Term : Term renames Inputs (2); List_Term : Term renames Inputs (3); begin - return Result : World := This do + return Result : Goal := This do Result.Unify (T (Head_Term, Tail_Term), List_Term); end return; end Cons; procedure Cons - (This : in out World; + (This : in out Goal; Inputs : in Term_Array) is begin This := This.Cons (Inputs); @@ -761,18 +746,18 @@ package body Kompsos is -- nullo -- function Nil - (This : in World; + (This : in Goal; Nil_Term : in Term'Class) - return World is + return Goal is begin - return Result : World := This do + return Result : Goal := This do Result.Unify (Empty_Term, Nil_Term); end return; end Nil; procedure Nil - (This : in out World; + (This : in out Goal; Nil_Term : in Term'Class) is begin This := This.Nil (Nil_Term); @@ -783,18 +768,18 @@ package body Kompsos is -- pairo -- function Pair - (This : in World; + (This : in Goal; Pair_Term : in Term'Class) - return World is + return Goal is begin - return Result : World := This do + return Result : Goal := This do Result.Cons (Result.Fresh & Result.Fresh & Term (Pair_Term)); end return; end Pair; procedure Pair - (This : in out World; + (This : in out Goal; Pair_Term : in Term'Class) is begin This := This.Pair (Pair_Term); @@ -805,11 +790,11 @@ package body Kompsos is -- listo -- function Linked_List - (This : in World; + (This : in Goal; List_Term : in Term'Class) - return World + return Goal is - One, Two : World := This; + One, Two : Goal := This; Ref_Term : constant Term := Two.Fresh; begin One.Nil (List_Term); @@ -823,7 +808,7 @@ package body Kompsos is procedure Linked_List - (This : in out World; + (This : in out Goal; List_Term : in Term'Class) is begin This := This.Linked_List (List_Term); @@ -834,14 +819,14 @@ package body Kompsos is -- membero -- function Member - (This : in World; + (This : in Goal; Inputs : in Term_Array) - return World + return Goal is Item_Term : Term renames Inputs (1); List_Term : Term renames Inputs (2); - One, Two : World := This; + One, Two : Goal := This; Ref_Term : constant Term := Two.Fresh; begin One.Head (List_Term & Item_Term); @@ -854,7 +839,7 @@ package body Kompsos is procedure Member - (This : in out World; + (This : in out Goal; Inputs : in Term_Array) is begin This := This.Member (Inputs); @@ -865,15 +850,15 @@ package body Kompsos is -- rembero -- function Remove - (This : in World; + (This : in Goal; Inputs : in Term_Array) - return World + return Goal is Item_Term : Term renames Inputs (1); List_Term : Term renames Inputs (2); Out_Term : Term renames Inputs (3); - One, Two : World := This; + One, Two : Goal := This; Left : constant Term := Two.Fresh; Right : constant Term := Two.Fresh; Rest : constant Term := Two.Fresh; @@ -890,7 +875,7 @@ package body Kompsos is procedure Remove - (This : in out World; + (This : in out Goal; Inputs : in Term_Array) is begin This := This.Remove (Inputs); @@ -901,15 +886,15 @@ package body Kompsos is -- appendo -- function Append - (This : in World; + (This : in Goal; Inputs : in Term_Array) - return World + return Goal is List_Term : Term renames Inputs (1); Item_Term : Term renames Inputs (2); Out_Term : Term renames Inputs (3); - One, Two : World := This; + One, Two : Goal := This; Left : constant Term := Two.Fresh; Right : constant Term := Two.Fresh; Rest : constant Term := Two.Fresh; @@ -926,7 +911,7 @@ package body Kompsos is procedure Append - (This : in out World; + (This : in out Goal; Inputs : in Term_Array) is begin This := This.Append (Inputs); diff --git a/src/kompsos.ads b/src/kompsos.ads index 22e5a8b..862b345 100644 --- a/src/kompsos.ads +++ b/src/kompsos.ads @@ -91,29 +91,29 @@ package Kompsos is Empty_State : constant State; - -- Worlds -- + -- Goals -- - type World is tagged private; - type World_Array is array (Positive range <>) of World; + type Goal is tagged private; + type Goal_Array is array (Positive range <>) of Goal; - Empty_World : constant World; + Empty_Goal : constant Goal; -- Junction Functions -- type Junction_Zero_Func is access function - (This : in World) - return World; + (This : in Goal) + return Goal; type Junction_One_Func is access function - (This : in World; + (This : in Goal; Input : in Term'Class) - return World; + return Goal; type Junction_Many_Func is access function - (This : in World; + (This : in Goal; Inputs : in Term_Array) - return World; + return Goal; @@ -125,24 +125,24 @@ package Kompsos is -- Variable Introduction -- function Fresh - (This : in out World'Class) + (This : in out Goal'Class) return Term with Post => Fresh'Result.Kind = Var_Term; function Fresh - (This : in out World'Class; + (This : in out Goal'Class; Name : in String) return Term with Post => Fresh'Result.Kind = Var_Term; function Fresh - (This : in out World'Class; + (This : in out Goal'Class; Name : in Nametag) return Term with Post => Fresh'Result.Kind = Var_Term; function Fresh - (This : in out World'Class; + (This : in out Goal'Class; Count : in Positive) return Term_Array with Post => @@ -150,7 +150,7 @@ package Kompsos is (for all Item of Fresh'Result => Item.Kind = Var_Term); function Fresh - (This : in out World'Class; + (This : in out Goal'Class; Names : in Nametag_Array) return Term_Array with Post => @@ -158,7 +158,7 @@ package Kompsos is (for all Item of Fresh'Result => Item.Kind = Var_Term); generic - Verse : in out World; + Verse : in out Goal; function Make_Fresh return Term with Post => Make_Fresh'Result.Kind = Var_Term; @@ -167,75 +167,75 @@ package Kompsos is -- Unification -- function Unify - (This : in World; + (This : in Goal; Left : in Term'Class; Right : in Element_Type) - return World; + return Goal; procedure Unify - (This : in out World; + (This : in out Goal; Left : in Term'Class; Right : in Element_Type); function Unify - (This : in World; + (This : in Goal; Left, Right : in Term'Class) - return World; + return Goal; procedure Unify - (This : in out World; + (This : in out Goal; Left, Right : in Term'Class); -- Combining / Disjunction -- function Disjunct - (Left, Right : in World) - return World; + (Left, Right : in Goal) + return Goal; procedure Disjunct - (This : in out World; - Right : in World); + (This : in out Goal; + Right : in Goal); function Disjunct - (Inputs : in World_Array) - return World; + (Inputs : in Goal_Array) + return Goal; procedure Disjunct - (This : in out World; - Inputs : in World_Array); + (This : in out Goal; + Inputs : in Goal_Array); -- Lazy Sequencing / Conjunction -- function Conjunct - (This : in World; + (This : in Goal; Func : in Junction_Zero_Func) - return World; + return Goal; procedure Conjunct - (This : in out World; + (This : in out Goal; Func : in Junction_Zero_Func); function Conjunct - (This : in World; + (This : in Goal; Func : in Junction_One_Func; Input : in Term'Class) - return World; + return Goal; procedure Conjunct - (This : in out World; + (This : in out Goal; Func : in Junction_One_Func; Input : in Term'Class); function Conjunct - (This : in World; + (This : in Goal; Func : in Junction_Many_Func; Inputs : in Term_Array) - return World; + return Goal; procedure Conjunct - (This : in out World; + (This : in out Goal; Func : in Junction_Many_Func; Inputs : in Term_Array); @@ -249,26 +249,29 @@ package Kompsos is -- Infinite State Loops -- function Recurse - (This : in World) - return World; + (This : in Goal) + return Goal; procedure Recurse - (This : in out World); + (This : in out Goal); -- Evaluation -- - function Take - (This : in World; - Count : in Positive) + function Run + (This : in Goal; + Count : in Positive; + Base : in State := Empty_State) return State_Array; - function Take_First - (This : in World) + function Run + (This : in Goal; + Base : in State := Empty_State) return State; - function Take_All - (This : in World) + function Run_All + (This : in Goal; + Base : in State := Empty_State) return State_Array; @@ -303,14 +306,14 @@ package Kompsos is -- caro -- -- Inputs = List_Term & Head_Term function Head - (This : in World; + (This : in Goal; Inputs : in Term_Array) - return World + return Goal with Pre => Inputs'Length = 2; -- Inputs = List_Term & Head_Term procedure Head - (This : in out World; + (This : in out Goal; Inputs : in Term_Array) with Pre => Inputs'Length = 2; @@ -318,14 +321,14 @@ package Kompsos is -- cdro -- -- Inputs = List_Term & Tail_Term function Tail - (This : in World; + (This : in Goal; Inputs : in Term_Array) - return World + return Goal with Pre => Inputs'Length = 2; -- Inputs = List_Term & Tail_Term procedure Tail - (This : in out World; + (This : in out Goal; Inputs : in Term_Array) with Pre => Inputs'Length = 2; @@ -333,14 +336,14 @@ package Kompsos is -- conso -- -- Inputs = Head_Term & Tail_Term & List_Term function Cons - (This : in World; + (This : in Goal; Inputs : in Term_Array) - return World + return Goal with Pre => Inputs'Length = 3; -- Inputs = Head_Term & Tail_Term & List_Term procedure Cons - (This : in out World; + (This : in out Goal; Inputs : in Term_Array) with Pre => Inputs'Length = 3; @@ -348,12 +351,12 @@ package Kompsos is -- nullo -- function Nil - (This : in World; + (This : in Goal; Nil_Term : in Term'Class) - return World; + return Goal; procedure Nil - (This : in out World; + (This : in out Goal; Nil_Term : in Term'Class); @@ -368,38 +371,38 @@ package Kompsos is -- pairo -- function Pair - (This : in World; + (This : in Goal; Pair_Term : in Term'Class) - return World; + return Goal; procedure Pair - (This : in out World; + (This : in out Goal; Pair_Term : in Term'Class); -- listo -- function Linked_List - (This : in World; + (This : in Goal; List_Term : in Term'Class) - return World; + return Goal; procedure Linked_List - (This : in out World; + (This : in out Goal; List_Term : in Term'Class); -- membero -- -- Inputs = Item_Term & List_Term function Member - (This : in World; + (This : in Goal; Inputs : in Term_Array) - return World + return Goal with Pre => Inputs'Length = 2; -- Inputs = Item_Term & List_Term procedure Member - (This : in out World; + (This : in out Goal; Inputs : in Term_Array) with Pre => Inputs'Length = 2; @@ -407,14 +410,14 @@ package Kompsos is -- rembero -- -- Inputs = Item_Term & List_Term & Out_Term function Remove - (This : in World; + (This : in Goal; Inputs : in Term_Array) - return World + return Goal with Pre => Inputs'Length = 3; -- Inputs = Item_Term & List_Term & Out_Term procedure Remove - (This : in out World; + (This : in out Goal; Inputs : in Term_Array) with Pre => Inputs'Length = 3; @@ -422,14 +425,14 @@ package Kompsos is -- appendo -- -- Inputs = List_Term & Item_Term & Out_Term function Append - (This : in World; + (This : in Goal; Inputs : in Term_Array) - return World + return Goal with Pre => Inputs'Length = 3; -- Inputs = List_Term & Item_Term & Out_Term procedure Append - (This : in out World; + (This : in out Goal; Inputs : in Term_Array) with Pre => Inputs'Length = 3; @@ -439,7 +442,7 @@ package Kompsos is -- nevero -- - -- Skipped since it just creates a failed World + -- Skipped since it just creates a failed Goal -- alwayso -- @@ -559,12 +562,12 @@ private - type World_Component; + type Goal_Component; - type World_Component_Access is access World_Component; + type Goal_Component_Access is access Goal_Component; function "<" - (Left, Right : in World_Component_Access) + (Left, Right : in Goal_Component_Access) return Boolean; type Lazy_Kind is (Zero_Arg, One_Arg, Many_Arg); @@ -592,51 +595,46 @@ private Conjunct_Node, Recurse_Node); - type World_Component (Kind : Node_Kind) is limited record + type Goal_Component (Kind : Node_Kind) is limited record Counter : Natural; case Kind is when Static_Node => - Stc_States : State_Vectors.Vector; + null; when Fresh_Node => - Frs_World : aliased World; - Frs_Var : Variable; + Frs_Goal : aliased Goal; + Frs_Var : Variable; when Unify_Node => - Uni_World : aliased World; - Uni_Term1 : Term; - Uni_Term2 : Term; + Uni_Goal : aliased Goal; + Uni_Term1 : Term; + Uni_Term2 : Term; when Disjunct_Node => - Dis_World1 : aliased World; - Dis_World2 : aliased World; + Dis_Goal1 : aliased Goal; + Dis_Goal2 : aliased Goal; when Conjunct_Node => - Con_World : aliased World; - Con_Data : Lazy_Holders.Holder; + Con_Goal : aliased Goal; + Con_Data : Lazy_Holders.Holder; when Recurse_Node => - Rec_World : aliased World; + Rec_Goal : aliased Goal; end case; end record; - type World is new Ada.Finalization.Controlled with record - Actual : World_Component_Access := null; + type Goal is new Ada.Finalization.Controlled with record + Actual : Goal_Component_Access := null; end record; overriding procedure Initialize - (This : in out World); + (This : in out Goal); overriding procedure Adjust - (This : in out World); + (This : in out Goal); overriding procedure Finalize - (This : in out World); + (This : in out Goal); - function Static - (Item : in State) - return World'Class; - - 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)))); + Empty_Goal : constant Goal := (Ada.Finalization.Controlled with + Actual => new Goal_Component'( + (Kind => Static_Node, + Counter => 1))); end Kompsos; |