diff options
Diffstat (limited to 'src/kompsos.adb')
| -rw-r--r-- | src/kompsos.adb | 157 |
1 files changed, 67 insertions, 90 deletions
diff --git a/src/kompsos.adb b/src/kompsos.adb index 4513706..b12e1fb 100644 --- a/src/kompsos.adb +++ b/src/kompsos.adb @@ -53,43 +53,11 @@ 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); + procedure Free is new Ada.Unchecked_Deallocation (Term_Array, Term_Array_Access); + procedure Free is new Ada.Unchecked_Deallocation (Lazy_Data, Lazy_Data_Access); procedure Initialize @@ -114,6 +82,14 @@ package body Kompsos is if This.Actual /= null then This.Actual.Counter := This.Actual.Counter - 1; if This.Actual.Counter = 0 then + if This.Actual.Kind = Conjunct_Node then + if This.Actual.Con_Data /= null and then + This.Actual.Con_Data.Kind = Many_Arg + then + Free (This.Actual.Con_Data.MInput); + end if; + Free (This.Actual.Con_Data); + end if; Free (This.Actual); end if; end if; @@ -243,27 +219,54 @@ package body Kompsos is -- States -- + function Variable_Index_Hash + (Key : in Variable) + return Ada.Containers.Hash_Type is + begin + return Ada.Containers.Hash_Type (Key mod Ada.Containers.Hash_Type'Modulus); + end Variable_Index_Hash; + + + procedure Insert + (This : in out State; + Key : in Variable; + Value : in Term'Class) is + begin + This.Binds.Append ((Key, Term (Value))); + This.Refs.Insert (Key, This.Binds.Last_Index); + end Insert; + + function Lookup (This : in State; Key : in Variable; Value : out Term'Class) return Boolean is - Ptr : State_Component_Access := This.Ctrl.Actual; + use type Variable_Index_Maps.Cursor; + Result : constant Variable_Index_Maps.Cursor := This.Refs.Find (Key); begin - while Ptr /= null loop - for Index in Valid_Count range Valid_Count'First .. Ptr.Valid loop - if Ptr.Data (Index).Key = Key then - Value := Term'Class (Ptr.Data (Index).Value); - return True; - end if; - end loop; - Ptr := Ptr.Next.Ctrl.Actual; - end loop; + if Result /= Variable_Index_Maps.No_Element then + Value := This.Binds (Variable_Index_Maps.Element (Result)).Value; + return True; + end if; return False; end Lookup; + procedure Truncate + (This : in out State; + Length : in Long_Natural) is + begin + if This.Binds.Last_Index > Length then + for Index in Long_Positive range Length + 1 .. This.Binds.Last_Index loop + This.Refs.Exclude (This.Binds (Index).Key); + end loop; + This.Binds.Set_Length (Ada.Containers.Count_Type (Length)); + end if; + end Truncate; + + ------------------- @@ -413,7 +416,7 @@ package body Kompsos is (Kind => Conjunct_Node, Counter => 1, Con_Goal => This.Graph, - Con_Data => Lazy_Holders.To_Holder ((Kind => Zero_Arg, ZFunc => Func))))), + Con_Data => new Lazy_Data'((Kind => Zero_Arg, ZFunc => Func))))), Next_Var => This.Next_Var); end Conjunct; @@ -438,10 +441,10 @@ package body Kompsos is (Kind => Conjunct_Node, Counter => 1, Con_Goal => This.Graph, - Con_Data => Lazy_Holders.To_Holder - ((Kind => One_Arg, - OFunc => Func, - OInput => Term (Input)))))), + Con_Data => new Lazy_Data'( + (Kind => One_Arg, + OFunc => Func, + OInput => Term (Input)))))), Next_Var => This.Next_Var); end Conjunct; @@ -467,10 +470,10 @@ package body Kompsos is (Kind => Conjunct_Node, Counter => 1, Con_Goal => This.Graph, - Con_Data => Lazy_Holders.To_Holder - ((Kind => Many_Arg, - MFunc => Func, - MInput => Term_Array_Holders.To_Holder (Inputs)))))), + Con_Data => new Lazy_Data'( + (Kind => Many_Arg, + MFunc => Func, + MInput => new Term_Array'(Inputs)))))), Next_Var => This.Next_Var); end Conjunct; @@ -490,30 +493,6 @@ package body Kompsos is -- Auxiliary Helpers -- ------------------------- - -- Infinite State Loops -- - - function Recurse - (This : in Goal) - return Goal is - begin - return Result : constant Goal := - (Graph => (Ada.Finalization.Controlled with - Actual => new Graph_Component'( - (Kind => Recurse_Node, - Counter => 1, - Rec_Goal => This.Graph))), - Next_Var => This.Next_Var); - end Recurse; - - - procedure Recurse - (This : in out Goal) is - begin - This := This.Recurse; - end Recurse; - - - -- Evaluation -- function Run @@ -599,24 +578,22 @@ package body Kompsos is (Subst : in State) return Term is begin - if Subst.Ctrl.Actual = null then + if Subst.Binds.Is_Empty then return Empty_Term; end if; declare - Min_Pos : State_Component_Access := Subst.Ctrl.Actual; - Min_Ind : Valid_Count := Valid_Count'First; - Marker : State_Component_Access := Min_Pos; + Min_Index : Long_Positive := 1; + Min_Var : Variable := Subst.Binds.First_Element.Key; begin - while Marker /= null loop - for Index in Valid_Count range Valid_Count'First .. Marker.Valid loop - if Marker.Data (Index).Key < Min_Pos.Data (Min_Ind).Key then - Min_Pos := Marker; - Min_Ind := Index; - end if; - end loop; - Marker := Marker.Next.Ctrl.Actual; + for Index in Long_Positive range + Subst.Binds.First_Index + 1 .. Subst.Binds.Last_Index + loop + if Subst.Binds (Index).Key < Min_Var then + Min_Index := Index; + Min_Var := Subst.Binds (Index).Key; + end if; end loop; - return Min_Pos.Data (Min_Ind).Value.Resolve (Subst); + return Subst.Binds (Min_Index).Value.Resolve (Subst); end; end Resolve_First; |