diff options
Diffstat (limited to 'src/kompsos-collector.adb')
| -rw-r--r-- | src/kompsos-collector.adb | 92 |
1 files changed, 24 insertions, 68 deletions
diff --git a/src/kompsos-collector.adb b/src/kompsos-collector.adb index e8314ff..7ccdb57 100644 --- a/src/kompsos-collector.adb +++ b/src/kompsos-collector.adb @@ -58,32 +58,13 @@ package body Kompsos.Collector is -- Unification -- - function Fully_Contains - (This : in State; - Item : in Term'Class) - return Boolean is + procedure Walk + (This : in State; + Item : in out Term) is begin - case Item.Kind is - when Null_Term | Atom_Term => - return True; - when Var_Term => - return This.LVars.Contains (Item.Var); - when Pair_Term => - return Fully_Contains (This, Item.Left) and then Fully_Contains (This, Item.Right); - end case; - end Fully_Contains; - - - function Walk - (This : in State; - Item : in Term'Class) - return Term'Class is - begin - 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; + while Item.Kind = Var_Term and then This.Actual.Contains (Item.Var) loop + Item := This.Actual.Element (Item.Var); + end loop; end Walk; @@ -93,20 +74,12 @@ package body Kompsos.Collector is Extended : out State) return Boolean is - Real_Left : Term'Class := Left; - Real_Right : Term'Class := Right; + Real_Left : Term := Term (Left); + Real_Right : Term := Term (Right); begin - -- Check for Variable validity with respect to State - pragma Assert (Fully_Contains (Potential, Real_Left)); - pragma Assert (Fully_Contains (Potential, Real_Right)); - -- Resolve Variable substitution - if Left.Kind = Var_Term then - Real_Left := Walk (Potential, Real_Left); - end if; - if Right.Kind = Var_Term then - Real_Right := Walk (Potential, Real_Right); - end if; + Walk (Potential, Real_Left); + Walk (Potential, Real_Right); -- Unify equal Variable/Atom/Null Terms if (Real_Left.Kind = Var_Term and then @@ -124,12 +97,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 (Real_Left.Var, Term (Real_Right)); + Extended.Actual.Insert (Real_Left.Var, Real_Right); return True; end if; if Real_Right.Kind = Var_Term then Extended := Potential; - Extended.Subst.Insert (Real_Right.Var, Term (Real_Left)); + Extended.Actual.Insert (Real_Right.Var, Real_Left); return True; end if; @@ -139,11 +112,7 @@ package body Kompsos.Collector is Do_Unify (Extended, Real_Left.Right, Real_Right.Right, Extended); end if; - -- Not sure how things get here, but if all else fails - return False; - - exception - when Ada.Assertions.Assertion_Error => + -- Otherwise unification fails return False; end Do_Unify; @@ -179,10 +148,6 @@ package body Kompsos.Collector is Cache_Memo.Exclude (Ptr.Actual); case Ptr.Actual.Kind is - when Static_Node => - return; - when Fresh_Node => - Reset (Ptr.Actual.Frs_Goal'Unchecked_Access); when Unify_Node => Book.Exclude (Ptr.Actual); Reset (Ptr.Actual.Uni_Goal'Unchecked_Access); @@ -221,22 +186,6 @@ package body Kompsos.Collector is return Boolean is begin case Ptr.Kind is - when Static_Node => - if Index = 1 then - Result := Base; - return True; - else - return False; - end if; - - when Fresh_Node => - if Get_Next (Ptr.Frs_Goal'Unchecked_Access, Base, Index, Result) then - Result.LVars.Append (Ptr.Frs_Var); - return True; - else - return False; - end if; - when Unify_Node => if not Book.Contains (Ptr) then Book.Insert (Ptr, (Kind => Unify_Data, others => <>)); @@ -359,6 +308,7 @@ package body Kompsos.Collector is Result) loop Reset (Constant_Goal_Access (Book.Element (Ptr).Con_Part)); + Book (Ptr).Con_From := Book.Element (Ptr).Con_From + 1; if Get_Next (Ptr.Con_Goal'Unchecked_Access, Base, @@ -367,7 +317,6 @@ package body Kompsos.Collector is then Book (Ptr).Con_Base.all := Result; Book (Ptr).Con_Next := 1; - Book (Ptr).Con_From := Book.Element (Ptr).Con_From + 1; else Book (Ptr).Con_Gone := True; Free (Book (Ptr).Con_Part); @@ -382,7 +331,7 @@ package body Kompsos.Collector is if not Book.Contains (Ptr) then Book.Insert (Ptr, (Kind => Recurse_Data, others => <>)); if Ptr.Rec_Goal.Actual = null then - Book (Ptr).Rec_Gone := True; + Book (Ptr).Rec_Cache := False; elsif not Cache_Memo.Contains (Ptr.Rec_Goal.Actual) then Cache_Memo.Insert (Ptr.Rec_Goal.Actual, State_Vectors.Empty_Vector); end if; @@ -420,8 +369,15 @@ package body Kompsos.Collector is Result : out State) return Boolean is begin - if Ptr = null or else Ptr.Actual = null then + if Ptr = null then return False; + elsif Ptr.Actual = null then + if Index = 1 then + Result := Base; + return True; + else + return False; + end if; elsif Cache_Memo.Contains (Ptr.Actual) and then Index <= Cache_Memo (Ptr.Actual).Last_Index then @@ -429,7 +385,7 @@ package body Kompsos.Collector is return True; else return Found : constant Boolean := Do_Get_Next (Ptr.Actual, Base, Index, Result) do - if Found and Ptr.Actual.Counter > 1 and Ptr.Actual.Kind /= Static_Node then + if Found and Ptr.Actual.Counter > 1 then if not Cache_Memo.Contains (Ptr.Actual) then Cache_Memo.Insert (Ptr.Actual, State_Vectors.Empty_Vector); end if; |