Worlds separated into Goals that run on a State, improvement to unification efficiencyHEADmaster

1 files changed, 146 insertions, 161 deletions

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);