Improvements to Fresh and Take

1 files changed, 47 insertions, 11 deletions

diff --git a/src/kompsos.ads b/src/kompsos.ads
index c336a41..ed5c664 100644
--- a/src/kompsos.ads
+++ b/src/kompsos.ads
@@ -26,6 +26,14 @@ package Kompsos is
     --  Datatypes  --
     -----------------
 
+    --  Variable Names  --
+
+    subtype Nametag is Ada.Strings.Unbounded.Unbounded_String;
+    type Nametag_Array is array (Positive range <>) of Nametag;
+
+
+    --  Terms  --
+
     type Term_Kind is (Null_Term, Atom_Term, Var_Term, Pair_Term);
 
     type Term is tagged private;
@@ -56,7 +64,7 @@ package Kompsos is
 
     function Name
            (This : in Term)
-        return Ada.Strings.Unbounded.Unbounded_String
+        return Nametag
     with Pre => This.Kind = Var_Term;
 
     function Left
@@ -70,12 +78,24 @@ package Kompsos is
     with Pre => This.Kind = Pair_Term;
 
 
+    --  States  --
+
+    type State is private;
+    type State_Array is array (Positive range <>) of State;
+
+    Empty_State : constant State;
+
+
+    --  Worlds  --
+
     type World is tagged private;
     type World_Array is array (Positive range <>) of World;
 
     Empty_World : constant World;
 
 
+    --  Junction Functions  --
+
     type Conjunct_Zero_Func is access function
            (This : in World)
         return World;
@@ -112,10 +132,26 @@ package Kompsos is
 
     function Fresh
            (This : in out World'Class;
-            Name : in     Ada.Strings.Unbounded.Unbounded_String)
+            Name : in     Nametag)
         return Term
     with Post => Fresh'Result.Kind = Var_Term;
 
+    function Fresh
+           (This  : in out World'Class;
+            Count : in     Positive)
+        return Term_Array
+    with Post =>
+        Fresh'Result'Length = Count and
+        (for all Item of Fresh'Result => Item.Kind = Var_Term);
+
+    function Fresh
+           (This  : in out World'Class;
+            Names : in     Nametag_Array)
+        return Term_Array
+    with Post =>
+        Fresh'Result'Length = Names'Length and
+        (for all Item of Fresh'Result => Item.Kind = Var_Term);
+
 
     --  Unification  --
 
@@ -212,13 +248,13 @@ package Kompsos is
     --  Forced Evaluation  --
 
     function Take
-           (This  : in World;
-            Count : in Natural)
-        return World;
-
-    procedure Take
            (This  : in out World;
-            Count : in     Natural);
+            Count : in     Positive)
+        return State_Array;
+
+    function Take_First
+           (This : in out World)
+        return State;
 
     procedure Force
            (This  : in out World;
@@ -411,7 +447,7 @@ private
 
     type Variable is record
         Ident : Generator_ID_Number;
-        Name  : SU.Unbounded_String;
+        Name  : Nametag;
     end record;
 
 
@@ -457,7 +493,7 @@ private
 
     package Name_Vectors is new Ada.Containers.Vectors
        (Index_Type   => Variable_ID_Number,
-        Element_Type => SU.Unbounded_String,
+        Element_Type => Nametag,
         "="          => SU."=");
 
     package Binding_Maps is new Ada.Containers.Ordered_Maps
@@ -516,7 +552,7 @@ private
         when Fresh_Gen =>
             Frs_Ident   : Generator_ID_Number;
             Frs_World   : World_Holders.Holder;
-            Frs_Name    : SU.Unbounded_String;
+            Frs_Name    : Nametag;
         when Unify_Gen =>
             Uni_World   : World_Holders.Holder;
             Uni_Term1   : Term;