Improvements to Fresh and Take

5 files changed, 121 insertions, 42 deletions

diff --git a/src/kompsos-pretty_print.adb b/src/kompsos-pretty_print.adb
index 772c0cd..73cee40 100644
--- a/src/kompsos-pretty_print.adb
+++ b/src/kompsos-pretty_print.adb
@@ -29,8 +29,6 @@ package body Kompsos.Pretty_Print is
     end Image;
 
 
-
-
     function Image
            (Item : in ID_Number)
         return String is
@@ -135,6 +133,23 @@ package body Kompsos.Pretty_Print is
     end Image;
 
 
+    function Image
+           (Items : in State_Array)
+        return String
+    is
+        Result : SU.Unbounded_String;
+    begin
+        if Items'Length = 0 then
+            return "States: N/A" & Latin.LF;
+        end if;
+        for Index in Items'Range loop
+            SU.Append (Result, "State#" & Image (Index) & ":" & Latin.LF);
+            SU.Append (Result, Image (Items (Index)));
+        end loop;
+        return SU.Slice (Result, 1, SU.Length (Result) - 1);
+    end Image;
+
+
 
 
     function Image
diff --git a/src/kompsos-pretty_print.ads b/src/kompsos-pretty_print.ads
index bcaf86e..3d5963e 100644
--- a/src/kompsos-pretty_print.ads
+++ b/src/kompsos-pretty_print.ads
@@ -23,6 +23,16 @@ package Kompsos.Pretty_Print is
         return String;
 
 
+    function Image
+           (Item : in State)
+        return String;
+
+
+    function Image
+           (Items : in State_Array)
+        return String;
+
+
     function Image_Constant
            (Item : in World)
         return String;
@@ -46,11 +56,6 @@ private
         return String;
 
 
-    function Image
-           (Item : in State)
-        return String;
-
-
 end Kompsos.Pretty_Print;
 
 
diff --git a/src/kompsos.adb b/src/kompsos.adb
index b3816fa..f338e7e 100644
--- a/src/kompsos.adb
+++ b/src/kompsos.adb
@@ -84,7 +84,7 @@ package body Kompsos is
 
     function Name
            (This : in Term)
-        return SU.Unbounded_String is
+        return Nametag is
     begin
         return This.Var.Name;
     end Name;
@@ -464,7 +464,7 @@ package body Kompsos is
 
     function Fresh
            (This : in out World'Class;
-            Name : in     Ada.Strings.Unbounded.Unbounded_String)
+            Name : in     Nametag)
         return Term
     is
         My_ID : constant Generator_ID_Number := Next_Gen;
@@ -480,6 +480,30 @@ package body Kompsos is
     end Fresh;
 
 
+    function Fresh
+           (This  : in out World'Class;
+            Count : in     Positive)
+        return Term_Array
+    is
+        Names : constant Nametag_Array (1 .. Count) := (others => +"");
+    begin
+        return This.Fresh (Names);
+    end Fresh;
+
+
+    function Fresh
+           (This  : in out World'Class;
+            Names : in     Nametag_Array)
+        return Term_Array is
+    begin
+        return Terms : Term_Array (1 .. Names'Length) do
+            for Index in Terms'Range loop
+                Terms (Index) := This.Fresh (Names (Names'First + Index - 1));
+            end loop;
+        end return;
+    end Fresh;
+
+
 
     --  Unification  --
 
@@ -685,31 +709,30 @@ package body Kompsos is
     --  Forced Evaluation  --
 
     function Take
-           (This  : in World;
-            Count : in Natural)
-        return World is
-    begin
-        if Count = 0 then
-            return
-               (Possibles => State_Vectors.Empty_Vector,
-                Engine    => (Kind => No_Gen));
-        end if;
-        return Result : World := This do
-            Result.Roll_Until (Count);
-            if Result.Possibles.Last_Index > Count then
-                Result.Possibles.Set_Length (Ada.Containers.Count_Type (Count));
-            end if;
-            Result.Engine := (Kind => No_Gen);
+           (This  : in out World;
+            Count : in     Positive)
+        return State_Array is
+    begin
+        This.Force (Count);
+        return Result : State_Array (1 .. Integer'Min (Count, This.Possibles.Last_Index)) do
+            for Index in Result'Range loop
+                Result (Index) := This.Possibles.Element (Index);
+            end loop;
         end return;
     end Take;
 
 
-    procedure Take
-           (This  : in out World;
-            Count : in     Natural) is
+    function Take_First
+           (This : in out World)
+        return State is
     begin
-        This := This.Take (Count);
-    end Take;
+        This.Force (1);
+        if This.Possibles.Is_Empty then
+            return Empty_State;
+        else
+            return This.Possibles.First_Element;
+        end if;
+    end Take_First;
 
 
     procedure Force
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;
diff --git a/test/fivesix.adb b/test/fivesix.adb
index 3eabf6a..a17cbb1 100644
--- a/test/fivesix.adb
+++ b/test/fivesix.adb
@@ -39,9 +39,9 @@ begin
     Sixes.Unify (Sixes.Fresh, 6);
     Sixes.Recurse;
 
-    Result := Disjunct (Fives, Sixes).Take (5);
+    Result := Disjunct (Fives, Sixes);
 
-    TIO.Put_Line (Image (Result));
+    TIO.Put_Line (Image (Result.Take (5)));
 
 end FiveSix;