diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/kompsos-collector.adb | 16 | ||||
| -rw-r--r-- | src/kompsos-collector.ads | 2 | ||||
| -rw-r--r-- | src/kompsos-pretty_print.adb | 17 | ||||
| -rw-r--r-- | src/kompsos.adb | 61 | ||||
| -rw-r--r-- | src/kompsos.ads | 32 |
5 files changed, 95 insertions, 33 deletions
diff --git a/src/kompsos-collector.adb b/src/kompsos-collector.adb index c8333cf..4654dc7 100644 --- a/src/kompsos-collector.adb +++ b/src/kompsos-collector.adb @@ -95,13 +95,21 @@ 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.Actual.Append ((Real_Left.Var, Real_Right)); + Extended := (Ctrl => (Ada.Finalization.Controlled with + Actual => new State_Component'( + Counter => 1, + Key => Real_Left.Var, + Value => Real_Right, + Next => Potential))); return True; end if; if Real_Right.Kind = Var_Term then - Extended := Potential; - Extended.Actual.Append ((Real_Right.Var, Real_Left)); + Extended := (Ctrl => (Ada.Finalization.Controlled with + Actual => new State_Component'( + Counter => 1, + Key => Real_Right.Var, + Value => Real_Left, + Next => Potential))); return True; end if; diff --git a/src/kompsos-collector.ads b/src/kompsos-collector.ads index c1ea8bc..f03e1e6 100644 --- a/src/kompsos-collector.ads +++ b/src/kompsos-collector.ads @@ -43,8 +43,6 @@ private type Graph_Access is access all Goal_Graph; type Constant_Graph_Access is access constant Goal_Graph; - type State_Access is access State; - type Eval_Data (Kind : Node_Kind := Unify_Node) is record diff --git a/src/kompsos-pretty_print.adb b/src/kompsos-pretty_print.adb index 729b658..216ceec 100644 --- a/src/kompsos-pretty_print.adb +++ b/src/kompsos-pretty_print.adb @@ -112,14 +112,19 @@ package body Kompsos.Pretty_Print is is Result : SU.Unbounded_String; begin - if Item.Actual.Is_Empty then + if Item.Ctrl.Actual = null then SU.Append (Result, Latin.HT & "N/A" & Latin.LF); else - for Bind of Item.Actual loop - SU.Append (Result, Latin.HT & - Image (Bind.Key) & " => " & - Image (Bind.Elem) & Latin.LF); - end loop; + declare + Marker : State_Component_Access := Item.Ctrl.Actual; + begin + while Marker /= null loop + SU.Append (Result, Latin.HT & + Image (Marker.Key) & " => " & + Image (Marker.Value) & Latin.LF); + Marker := Marker.Next.Ctrl.Actual; + end loop; + end; end if; return SU.To_String (Result); end Image; diff --git a/src/kompsos.adb b/src/kompsos.adb index f7f0ba9..2efa69b 100644 --- a/src/kompsos.adb +++ b/src/kompsos.adb @@ -53,6 +53,40 @@ package body Kompsos is + -- States -- + + procedure Free is new Ada.Unchecked_Deallocation (State_Component, State_Component_Access); + + + procedure Initialize + (This : in out State_Control) is + begin + This.Actual := null; + end Initialize; + + + procedure Adjust + (This : in out State_Control) is + begin + if This.Actual /= null then + This.Actual.Counter := This.Actual.Counter + 1; + end if; + end Adjust; + + + procedure Finalize + (This : in out State_Control) is + begin + if This.Actual /= null then + This.Actual.Counter := This.Actual.Counter - 1; + if This.Actual.Counter = 0 then + Free (This.Actual); + end if; + end if; + end Finalize; + + + -- Goal Graphs -- procedure Free is new Ada.Unchecked_Deallocation (Graph_Component, Graph_Component_Access); @@ -213,13 +247,16 @@ package body Kompsos is (This : in State; Key : in Variable; Value : out Term'Class) - return Boolean is + return Boolean + is + Ptr : State_Component_Access := This.Ctrl.Actual; begin - for Bind of This.Actual loop - if Bind.Key = Key then - Value := Term'Class (Bind.Elem); + while Ptr /= null loop + if Ptr.Key = Key then + Value := Term'Class (Ptr.Value); return True; end if; + Ptr := Ptr.Next.Ctrl.Actual; end loop; return False; end Lookup; @@ -569,20 +606,20 @@ package body Kompsos is (Subst : in State) return Term is begin - if Subst.Actual.Is_Empty then + if Subst.Ctrl.Actual = null then return Empty_Term; else declare - Min_Pos : Long_Positive := Subst.Actual.First_Index; - Min_Var : Variable := Subst.Actual.First_Element.Key; + Min_Pos : State_Component_Access := Subst.Ctrl.Actual; + Marker : State_Component_Access := Min_Pos.Next.Ctrl.Actual; begin - for Index in Subst.Actual.First_Index + 1 .. Subst.Actual.Last_Index loop - if Subst.Actual (Index).Key < Min_Var then - Min_Pos := Index; - Min_Var := Subst.Actual (Index).Key; + while Marker /= null loop + if Marker.Key < Min_Pos.Key then + Min_Pos := Marker; end if; + Marker := Marker.Next.Ctrl.Actual; end loop; - return Subst.Actual (Min_Pos).Elem.Resolve (Subst); + return Min_Pos.Value.Resolve (Subst); end; end if; end Resolve_First; diff --git a/src/kompsos.ads b/src/kompsos.ads index 66ebfd5..d1e19be 100644 --- a/src/kompsos.ads +++ b/src/kompsos.ads @@ -9,7 +9,6 @@ private with Ada.Containers.Indefinite_Holders, - Ada.Containers.Vectors, Ada.Finalization; @@ -460,26 +459,41 @@ private - type Binding is record - Key : Variable; - Elem : Term; + type State_Component is limited record + Counter : Natural; + Key : Variable; + Value : Term; + Next : aliased State; end record; - package Binding_Vectors is new Ada.Containers.Vectors - (Index_Type => Long_Positive, - Element_Type => Binding); + type State_Component_Access is access State_Component; + + type State_Control is new Ada.Finalization.Controlled with record + Actual : State_Component_Access := null; + end record; + + overriding procedure Initialize + (This : in out State_Control); + + overriding procedure Adjust + (This : in out State_Control); + + overriding procedure Finalize + (This : in out State_Control); type State is record - Actual : Binding_Vectors.Vector; + Ctrl : State_Control := (Ada.Finalization.Controlled with Actual => null); end record; + type State_Access is access State; + function Lookup (This : in State; Key : in Variable; Value : out Term'Class) return Boolean; - Empty_State : constant State := (Actual => Binding_Vectors.Empty_Vector); + Empty_State : constant State := (Ctrl => (Ada.Finalization.Controlled with Actual => null)); |