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

1 files changed, 104 insertions, 106 deletions

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;