diff options
| -rw-r--r-- | src/kompsos-pretty_print.adb | 19 | ||||
| -rw-r--r-- | src/kompsos-pretty_print.ads | 15 | ||||
| -rw-r--r-- | src/kompsos.adb | 67 | ||||
| -rw-r--r-- | src/kompsos.ads | 58 | ||||
| -rw-r--r-- | test/fivesix.adb | 4 |
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; |