diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/kompsos-advanced_reify.adb | 44 | ||||
| -rw-r--r-- | src/kompsos-advanced_reify.ads | 10 | ||||
| -rw-r--r-- | src/kompsos-collector.adb | 18 | ||||
| -rw-r--r-- | src/kompsos-pretty_print.adb | 50 | ||||
| -rw-r--r-- | src/kompsos-pretty_print.ads | 4 | ||||
| -rw-r--r-- | src/kompsos.adb | 113 | ||||
| -rw-r--r-- | src/kompsos.ads | 91 |
7 files changed, 56 insertions, 274 deletions
diff --git a/src/kompsos-advanced_reify.adb b/src/kompsos-advanced_reify.adb index 42df1e7..c2d1670 100644 --- a/src/kompsos-advanced_reify.adb +++ b/src/kompsos-advanced_reify.adb @@ -96,49 +96,7 @@ package body Kompsos.Advanced_Reify is (Subst : in State) return Element_Trees.Tree is begin - if Subst.LVars.Is_Empty then - return Element_Trees.Empty_Tree; - end if; - for Iter in Subst.Ident.Iterate loop - if ID_Number_Maps.Element (Iter) = Subst.LVars.First_Index then - return Treeify (Term (T (Variable'( - Ident => ID_Number_Maps.Key (Iter), - Name => Subst.LVars.Element (ID_Number_Maps.Element (Iter))))), - Subst); - end if; - end loop; - return Element_Trees.Empty_Tree; - end Treeify_First; - - - function Treeify_First - (Subst : in State; - Name : in String) - return Element_Trees.Tree is - begin - return Treeify_First (Subst, +Name); - end Treeify_First; - - - function Treeify_First - (Subst : in State; - Name : in Nametag) - return Element_Trees.Tree - is - Name_Index : constant Name_Vectors.Extended_Index := Subst.LVars.Find_Index (Name); - begin - if Name_Index = Name_Vectors.No_Index then - return Element_Trees.Empty_Tree; - end if; - for Iter in Subst.Ident.Iterate loop - if ID_Number_Maps.Element (Iter) = Name_Index then - return Treeify (Term (T (Variable'( - Ident => ID_Number_Maps.Key (Iter), - Name => Subst.LVars.Element (ID_Number_Maps.Element (Iter))))), - Subst); - end if; - end loop; - return Element_Trees.Empty_Tree; + return To_Tree (Resolve_First (Subst)); end Treeify_First; diff --git a/src/kompsos-advanced_reify.ads b/src/kompsos-advanced_reify.ads index ecda1c9..db51558 100644 --- a/src/kompsos-advanced_reify.ads +++ b/src/kompsos-advanced_reify.ads @@ -53,16 +53,6 @@ package Kompsos.Advanced_Reify is (Subst : in State) return Element_Trees.Tree; - function Treeify_First - (Subst : in State; - Name : in String) - return Element_Trees.Tree; - - function Treeify_First - (Subst : in State; - Name : in Nametag) - return Element_Trees.Tree; - end Kompsos.Advanced_Reify; diff --git a/src/kompsos-collector.adb b/src/kompsos-collector.adb index b076679..792c2b2 100644 --- a/src/kompsos-collector.adb +++ b/src/kompsos-collector.adb @@ -67,7 +67,7 @@ package body Kompsos.Collector is when Null_Term | Atom_Term => return True; when Var_Term => - return This.Ident.Contains (Item.Var.Ident); + return This.LVars.Contains (Item.Var); when Pair_Term => return Fully_Contains (This, Item.Left) and then Fully_Contains (This, Item.Right); end case; @@ -79,10 +79,8 @@ package body Kompsos.Collector is Item : in Term'Class) return Term'Class is begin - if Item.Kind = Var_Term and then - This.Subst.Contains (This.Ident.Element (Item.Var.Ident)) - then - return Walk (This, This.Subst.Constant_Reference (This.Ident.Element (Item.Var.Ident))); + if Item.Kind = Var_Term and then This.Subst.Contains (Item.Var) then + return Walk (This, This.Subst.Element (Item.Var)); else return Item; end if; @@ -126,12 +124,12 @@ package body Kompsos.Collector is -- Unify Variable and other Terms by introducing a new substitution if Real_Left.Kind = Var_Term then Extended := Potential; - Extended.Subst.Insert (Extended.Ident.Element (Real_Left.Var.Ident), Term (Real_Right)); + Extended.Subst.Insert (Real_Left.Var, Term (Real_Right)); return True; end if; if Real_Right.Kind = Var_Term then Extended := Potential; - Extended.Subst.Insert (Extended.Ident.Element (Real_Right.Var.Ident), Term (Real_Left)); + Extended.Subst.Insert (Real_Right.Var, Term (Real_Left)); return True; end if; @@ -233,8 +231,7 @@ package body Kompsos.Collector is when Fresh_Node => if Get_Next (Ptr.Frs_Goal'Unchecked_Access, Base, Index, Result) then - Result.LVars.Append (Ptr.Frs_Var.Name); - Result.Ident.Insert (Ptr.Frs_Var.Ident, Result.LVars.Last_Index); + Result.LVars.Append (Ptr.Frs_Var); return True; else return False; @@ -510,8 +507,7 @@ package body Kompsos.Collector is end Next; - procedure Reset - is + procedure Reset is Ptr : constant Constant_Goal_Access := Relation'Access; begin Reset (Ptr); diff --git a/src/kompsos-pretty_print.adb b/src/kompsos-pretty_print.adb index 250c6a6..c888e13 100644 --- a/src/kompsos-pretty_print.adb +++ b/src/kompsos-pretty_print.adb @@ -10,6 +10,7 @@ with Ada.Characters.Latin_1, Ada.Strings.Fixed, + Ada.Strings.Unbounded, Kompsos.Collector; @@ -18,41 +19,41 @@ package body Kompsos.Pretty_Print is package Latin renames Ada.Characters.Latin_1; package Str renames Ada.Strings; + package SU renames Ada.Strings.Unbounded; function Image - (Item : in Integer) + (Item : in Long_Natural) return String is begin - return Str.Fixed.Trim (Integer'Image (Item), Str.Left); + return Str.Fixed.Trim (Long_Natural'Image (Item), Str.Left); end Image; function Image - (Item : in Long_Natural) + (Item : in Variable) return String is begin - return Str.Fixed.Trim (Long_Natural'Image (Item), Str.Left); + return "Var#" & Image (Long_Natural (Item)); end Image; + ----------------------------------- + -- Datatype->String Conversion -- + ----------------------------------- + function Image - (Item : in Variable) + (Item : in Integer) return String is begin - return "Vargen#" & Image (Long_Natural (Item.Ident)) & - (if SU.Length (Item.Name) /= 0 - then "/" & SU.To_String (Item.Name) - else ""); + return Str.Fixed.Trim (Integer'Image (Item), Str.Left); end Image; - - function Image (Item : in Term) return String @@ -93,28 +94,13 @@ package body Kompsos.Pretty_Print is is Result : SU.Unbounded_String; begin - SU.Append (Result, Latin.HT & "Generation:"); - if Item.Ident.Is_Empty then - SU.Append (Result, " N/A" & Latin.LF); - else - SU.Append (Result, Latin.LF); - for Iter in Item.Ident.Iterate loop - SU.Append (Result, Latin.HT & Latin.HT & "Vargen#" & - Image (Long_Natural (ID_Number_Maps.Key (Iter))) & " => " & - Image (Long_Natural (ID_Number_Maps.Element (Iter))) & Latin.LF); - end loop; - end if; SU.Append (Result, Latin.HT & "Variables:"); if Item.LVars.Is_Empty then SU.Append (Result, " N/A" & Latin.LF); else SU.Append (Result, Latin.LF); - for Index in Item.LVars.First_Index .. Item.LVars.Last_Index loop - SU.Append (Result, Latin.HT & Latin.HT & - "Var#" & Image (Long_Natural (Index)) & - (if SU.Length (Item.LVars (Index)) /= 0 - then "/" & SU.To_String (Item.LVars (Index)) - else "") & Latin.LF); + for LVar of Item.LVars loop + SU.Append (Result, Latin.HT & Latin.HT & Image (LVar) & Latin.LF); end loop; end if; SU.Append (Result, Latin.HT & "Substitution:"); @@ -124,11 +110,11 @@ package body Kompsos.Pretty_Print is SU.Append (Result, Latin.LF); for Iter in Item.Subst.Iterate loop SU.Append (Result, Latin.HT & Latin.HT & - Image (Long_Natural (Binding_Maps.Key (Iter))) & " => " & + Image (Binding_Maps.Key (Iter)) & " => " & Image (Binding_Maps.Element (Iter)) & Latin.LF); end loop; end if; - return -Result; + return SU.To_String (Result); end Image; @@ -173,6 +159,10 @@ package body Kompsos.Pretty_Print is + -------------------------------- + -- Graphviz DAG Of Tomorrow -- + -------------------------------- + procedure Do_Structure_DOT (This : in Goal; Nodes : in out DOT_Node_Maps.Map; diff --git a/src/kompsos-pretty_print.ads b/src/kompsos-pretty_print.ads index 653858b..23c525e 100644 --- a/src/kompsos-pretty_print.ads +++ b/src/kompsos-pretty_print.ads @@ -18,6 +18,8 @@ generic package Kompsos.Pretty_Print is + -- Datatype->String Conversion -- + function Image (Item : in Integer) return String; @@ -39,7 +41,7 @@ package Kompsos.Pretty_Print is return String; - + -- Graphviz DAG Of Tomorrow -- function Structure_DOT (This : in Goal; diff --git a/src/kompsos.adb b/src/kompsos.adb index 56c22cd..7054714 100644 --- a/src/kompsos.adb +++ b/src/kompsos.adb @@ -112,6 +112,8 @@ package body Kompsos is return Left.Actual.Left = Right.Actual.Left and Left.Actual.Right = Right.Actual.Right; when Null_Term => + -- Should never actually get here because Null_Terms + -- are covered by checking Left.Actual = Right.Actual return True; end case; else @@ -190,14 +192,6 @@ package body Kompsos is end Var; - function Name - (This : in Term) - return Nametag is - begin - return This.Var.Name; - end Name; - - function Left (This : in Term) return Term is @@ -237,15 +231,15 @@ package body Kompsos is -- Internal Helpers -- ------------------------ - -- Variable IDs -- + -- Variables -- - Next_Generator_ID : Generator_ID_Number := Generator_ID_Number'First; + Next_Variable : Variable := Variable'First; function Next_Gen - return Generator_ID_Number is + return Variable is begin - return Result : constant Generator_ID_Number := Next_Generator_ID do - Next_Generator_ID := Next_Generator_ID + 1; + return Result : constant Variable := Next_Variable do + Next_Variable := Next_Variable + 1; end return; end Next_Gen; @@ -260,28 +254,9 @@ package body Kompsos is function Fresh (This : in out Goal'Class) - return Term is - begin - return This.Fresh (+""); - end Fresh; - - - function Fresh - (This : in out Goal'Class; - Name : in String) - return Term is - begin - return This.Fresh (+Name); - end Fresh; - - - function Fresh - (This : in out Goal'Class; - Name : in Nametag) return Term is - My_ID : constant Generator_ID_Number := Next_Gen; - My_Var : constant Variable := (Ident => My_ID, Name => Name); + My_Var : constant Variable := Next_Gen; begin return My_Term : constant Term := Term (T (My_Var)) do This.Actual := new Goal_Component'( @@ -296,22 +271,11 @@ package body Kompsos is function Fresh (This : in out Goal'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 Goal'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)); + return My_Terms : Term_Array (1 .. Count) do + for Item of My_Terms loop + Item := This.Fresh; end loop; end return; end Fresh; @@ -587,21 +551,14 @@ package body Kompsos is function Resolve (This : in Term; Subst : in State) - return Term - is - use type SU.Unbounded_String; + return Term is begin case This.Kind is when Null_Term | Atom_Term => return This; when Var_Term => - if Subst.Ident.Contains (This.Var.Ident) and then - Subst.Ident.Element (This.Var.Ident) in - Subst.LVars.First_Index .. Subst.LVars.Last_Index and then - Subst.LVars.Element (Subst.Ident.Element (This.Var.Ident)) = This.Name and then - Subst.Subst.Contains (Subst.Ident.Element (This.Var.Ident)) - then - return Subst.Subst.Element (Subst.Ident.Element (This.Var.Ident)).Resolve (Subst); + if Subst.LVars.Contains (This.Var) and then Subst.Subst.Contains (This.Var) then + return Subst.Subst.Element (This.Var).Resolve (Subst); else return This; end if; @@ -617,47 +574,9 @@ package body Kompsos is begin if Subst.LVars.Is_Empty then return Empty_Term; + else + return Resolve (Term (T (Subst.LVars.First_Element)), Subst); end if; - for Iter in Subst.Ident.Iterate loop - if ID_Number_Maps.Element (Iter) = Subst.LVars.First_Index then - return Resolve (Term (T (Variable'( - Ident => ID_Number_Maps.Key (Iter), - Name => Subst.LVars.Element (ID_Number_Maps.Element (Iter))))), - Subst); - end if; - end loop; - return Empty_Term; - end Resolve_First; - - - function Resolve_First - (Subst : in State; - Name : in String) - return Term is - begin - return Resolve_First (Subst, +Name); - end Resolve_First; - - - function Resolve_First - (Subst : in State; - Name : in Nametag) - return Term - is - Name_Index : constant Name_Vectors.Extended_Index := Subst.LVars.Find_Index (Name); - begin - if Name_Index = Name_Vectors.No_Index then - return Empty_Term; - end if; - for Iter in Subst.Ident.Iterate loop - if ID_Number_Maps.Element (Iter) = Name_Index then - return Resolve (Term (T (Variable'( - Ident => ID_Number_Maps.Key (Iter), - Name => Subst.LVars.Element (ID_Number_Maps.Element (Iter))))), - Subst); - end if; - end loop; - return Empty_Term; end Resolve_First; diff --git a/src/kompsos.ads b/src/kompsos.ads index 862b345..19cfeb8 100644 --- a/src/kompsos.ads +++ b/src/kompsos.ads @@ -6,10 +6,6 @@ -- See license.txt for further details -with - - Ada.Strings.Unbounded; - private with Ada.Containers.Indefinite_Holders, @@ -27,12 +23,6 @@ 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); @@ -67,11 +57,6 @@ package Kompsos is return Element_Type with Pre => This.Kind = Atom_Term; - function Name - (This : in Term) - return Nametag - with Pre => This.Kind = Var_Term; - function Left (This : in Term) return Term @@ -130,18 +115,6 @@ package Kompsos is with Post => Fresh'Result.Kind = Var_Term; function Fresh - (This : in out Goal'Class; - Name : in String) - return Term - with Post => Fresh'Result.Kind = Var_Term; - - function Fresh - (This : in out Goal'Class; - Name : in Nametag) - return Term - with Post => Fresh'Result.Kind = Var_Term; - - function Fresh (This : in out Goal'Class; Count : in Positive) return Term_Array @@ -149,14 +122,6 @@ package Kompsos is Fresh'Result'Length = Count and (for all Item of Fresh'Result => Item.Kind = Var_Term); - function Fresh - (This : in out Goal'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); - generic Verse : in out Goal; function Make_Fresh @@ -286,16 +251,6 @@ package Kompsos is (Subst : in State) return Term; - function Resolve_First - (Subst : in State; - Name : in String) - return Term; - - function Resolve_First - (Subst : in State; - Name : in Nametag) - return Term; - @@ -452,33 +407,11 @@ package Kompsos is private - package SU renames Ada.Strings.Unbounded; - - - function "+" - (Item : in String) - return SU.Unbounded_String - renames SU.To_Unbounded_String; - - function "-" - (Item : in SU.Unbounded_String) - return String - renames SU.To_String; - - - - -- around 2^31 possible Variables should be enough for anybody, right? subtype Long_Natural is Long_Integer range 0 .. Long_Integer'Last; subtype Long_Positive is Long_Integer range 1 .. Long_Integer'Last; - type Generator_ID_Number is new Long_Natural; - type Variable_ID_Number is new Long_Natural; - - type Variable is record - Ident : Generator_ID_Number; - Name : Nametag; - end record; + type Variable is new Long_Natural; @@ -517,7 +450,8 @@ private function T (Item : in Variable) - return Term'Class; + return Term'Class + with Post => T'Result.Kind = Var_Term; function Var (This : in Term'Class) @@ -531,22 +465,16 @@ private - package ID_Number_Maps is new Ada.Containers.Ordered_Maps - (Key_Type => Generator_ID_Number, - Element_Type => Variable_ID_Number); - - package Name_Vectors is new Ada.Containers.Vectors - (Index_Type => Variable_ID_Number, - Element_Type => Nametag, - "=" => SU."="); + package Variable_Vectors is new Ada.Containers.Vectors + (Index_Type => Long_Positive, + Element_Type => Variable); package Binding_Maps is new Ada.Containers.Ordered_Maps - (Key_Type => Variable_ID_Number, + (Key_Type => Variable, Element_Type => Term); type State is record - Ident : ID_Number_Maps.Map; - LVars : Name_Vectors.Vector; + LVars : Variable_Vectors.Vector; Subst : Binding_Maps.Map; end record; @@ -555,8 +483,7 @@ private Element_Type => State); Empty_State : constant State := - (Ident => ID_Number_Maps.Empty_Map, - LVars => Name_Vectors.Empty_Vector, + (LVars => Variable_Vectors.Empty_Vector, Subst => Binding_Maps.Empty_Map); |