diff options
Diffstat (limited to 'src/kompsos.adb')
| -rw-r--r-- | src/kompsos.adb | 169 |
1 files changed, 72 insertions, 97 deletions
diff --git a/src/kompsos.adb b/src/kompsos.adb index 9d45f66..b3816fa 100644 --- a/src/kompsos.adb +++ b/src/kompsos.adb @@ -75,13 +75,21 @@ package body Kompsos is function Var - (This : in Term) + (This : in Term'Class) return Variable is begin return Term_Component (This.Actual.Constant_Reference.Element.all).Refer; end Var; + function Name + (This : in Term) + return SU.Unbounded_String is + begin + return This.Var.Name; + end Name; + + function Left (This : in Term) return Term is @@ -134,20 +142,22 @@ package body Kompsos is -- Internal Helpers -- ------------------------ - -- Unification -- + -- Variable IDs -- - function Has_Var - (This : in State; - Var : in Variable) - return Boolean - is - use type SU.Unbounded_String; + Next_Generator_ID : Generator_ID_Number := Generator_ID_Number'First; + + function Next_Gen + return Generator_ID_Number is begin - return This.LVars.Contains (Var.Ident) and then - This.LVars.Constant_Reference (Var.Ident) = Var.Name; - end Has_Var; + return Result : constant Generator_ID_Number := Next_Generator_ID do + Next_Generator_ID := Next_Generator_ID + 1; + end return; + end Next_Gen; + + -- Unification -- + function Fully_Contains (This : in State; Item : in Term'Class) @@ -157,7 +167,7 @@ package body Kompsos is when Null_Term | Atom_Term => return True; when Var_Term => - return Has_Var (This, Item.Var); + return This.Ident.Contains (Item.Var.Ident); when Pair_Term => return Fully_Contains (This, Item.Left) and then Fully_Contains (This, Item.Right); end case; @@ -169,8 +179,10 @@ package body Kompsos is Item : in Term'Class) return Term'Class is begin - if Item.Kind = Var_Term and then This.Subst.Contains (Item.Var.Ident) then - return Walk (This, This.Subst.Constant_Reference (Item.Var.Ident)); + 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))); else return Item; end if; @@ -186,32 +198,29 @@ package body Kompsos is Real_Left : Term'Class := Left; Real_Right : Term'Class := Right; begin + -- Check for Variable validity with respect to State + if not Fully_Contains (Potential, Real_Left) or + not Fully_Contains (Potential, Real_Right) + then + return False; + end if; + -- Resolve Variable substitution if Left.Kind = Var_Term then - if Has_Var (Potential, Left.Var) then - Real_Left := Walk (Potential, Left); - else - return False; - end if; + Real_Left := Walk (Potential, Real_Left); end if; if Right.Kind = Var_Term then - if Has_Var (Potential, Right.Var) then - Real_Right := Walk (Potential, Right); - else - return False; - end if; + Real_Right := Walk (Potential, Real_Right); end if; - -- Check for equal Null Terms - if Real_Left.Kind = Null_Term and Real_Right.Kind = Null_Term then - Extended := Potential; - return True; - end if; - - -- Unify equal Variable Terms - if Real_Left.Kind = Var_Term and then + -- Unify equal Variable/Atom/Null Terms + if (Real_Left.Kind = Var_Term and then Real_Right.Kind = Var_Term and then - Real_Left = Real_Right + Real_Left = Real_Right) or else + (Real_Left.Kind = Atom_Term and then + Real_Right.Kind = Atom_Term and then + Real_Left = Real_Right) or else + (Real_Left.Kind = Null_Term and Real_Right.Kind = Null_Term) then Extended := Potential; return True; @@ -219,41 +228,18 @@ package body Kompsos is -- Unify Variable and other Terms by introducing a new substitution if Real_Left.Kind = Var_Term then - if Real_Right.Kind = Pair_Term and then - not Fully_Contains (Potential, Real_Right) - then - return False; - end if; Extended := Potential; - Extended.Subst.Insert (Real_Left.Var.Ident, Term (Real_Right)); + Extended.Subst.Insert (Extended.Ident.Element (Real_Left.Var.Ident), Term (Real_Right)); return True; end if; if Real_Right.Kind = Var_Term then - if Real_Left.Kind = Pair_Term and then - not Fully_Contains (Potential, Real_Left) - then - return False; - end if; - Extended := Potential; - Extended.Subst.Insert (Real_Right.Var.Ident, Term (Real_Left)); - return True; - end if; - - -- Unify equal Atom Terms - if Real_Left.Kind = Atom_Term and then - Real_Right.Kind = Atom_Term and then - Real_Left = Real_Right - then Extended := Potential; + Extended.Subst.Insert (Extended.Ident.Element (Real_Right.Var.Ident), Term (Real_Left)); return True; end if; -- Unify Pair Terms by unifying each corresponding part - if Real_Left.Kind = Pair_Term and then - Real_Right.Kind = Pair_Term and then - Fully_Contains (Potential, Real_Left) and then - Fully_Contains (Potential, Real_Right) - then + if Real_Left.Kind = Pair_Term and then Real_Right.Kind = Pair_Term then declare Middle : State; begin @@ -285,7 +271,8 @@ package body Kompsos is begin Ptr (This.Engine.Frs_World).Rollover; for Potential of Ptr (This.Engine.Frs_World).Possibles loop - Potential.LVars.Insert (Ptr (This.Engine.Frs_World).Next_Ident, This.Engine.Frs_Name); + Potential.LVars.Append (This.Engine.Frs_Name); + Potential.Ident.Insert (This.Engine.Frs_Ident, Potential.LVars.Last_Index); This.Possibles.Append (Potential); end loop; if Ptr (This.Engine.Frs_World).Engine.Kind = No_Gen then @@ -478,14 +465,16 @@ package body Kompsos is function Fresh (This : in out World'Class; Name : in Ada.Strings.Unbounded.Unbounded_String) - return Term is + return Term + is + My_ID : constant Generator_ID_Number := Next_Gen; begin - return My_Term : constant Term := T (Variable'(Ident => This.Next_Ident, Name => Name)) do + return My_Term : constant Term := T (Variable'(Ident => My_ID, Name => Name)) do This.Engine := (Kind => Fresh_Gen, + Frs_Ident => My_ID, Frs_World => Hold (This), Frs_Name => Name); - This.Next_Ident := This.Next_Ident + 1; This.Possibles := State_Vectors.Empty_Vector; end return; end Fresh; @@ -519,9 +508,8 @@ package body Kompsos is return World is begin return Result : constant World := - (Possibles => State_Vectors.Empty_Vector, - Next_Ident => This.Next_Ident, - Engine => + (Possibles => State_Vectors.Empty_Vector, + Engine => (Kind => Unify_Gen, Uni_World => Hold (This), Uni_Term1 => Term (Left), @@ -545,9 +533,8 @@ package body Kompsos is return World is begin return Result : constant World := - (Possibles => State_Vectors.Empty_Vector, - Next_Ident => ID_Number'Max (Left.Next_Ident, Right.Next_Ident), - Engine => + (Possibles => State_Vectors.Empty_Vector, + Engine => (Kind => Disjunct_Gen, Dis_World1 => Hold (Left), Dis_World2 => Hold (Right))); @@ -568,24 +555,17 @@ package body Kompsos is begin if Inputs'Length = 0 then return Failed : constant World := - (Possibles => State_Vectors.Empty_Vector, - Next_Ident => 0, - Engine => (Kind => No_Gen)); + (Possibles => State_Vectors.Empty_Vector, + Engine => (Kind => No_Gen)); elsif Inputs'Length = 1 then return Inputs (Inputs'First); else - return Result : World := - (Possibles => State_Vectors.Empty_Vector, - Next_Ident => 0, -- dummy - Engine => + return Result : constant World := + (Possibles => State_Vectors.Empty_Vector, + Engine => (Kind => Disjunct_Gen, Dis_World1 => Hold (Inputs (Inputs'First)), - Dis_World2 => Hold (Disjunct (Inputs (Inputs'First + 1 .. Inputs'Last))))) - do - Result.Next_Ident := ID_Number'Max - (Ptr (Result.Engine.Dis_World1).Next_Ident, - Ptr (Result.Engine.Dis_World2).Next_Ident); - end return; + Dis_World2 => Hold (Disjunct (Inputs (Inputs'First + 1 .. Inputs'Last))))); end if; end Disjunct; @@ -607,9 +587,8 @@ package body Kompsos is return World is begin return Result : constant World := - (Possibles => State_Vectors.Empty_Vector, - Next_Ident => 0, -- dummy - Engine => + (Possibles => State_Vectors.Empty_Vector, + Engine => (Kind => Conjunct_Zero_Gen, ConZ_World => Hold (This), ConZ_Func => Func)); @@ -631,9 +610,8 @@ package body Kompsos is return World is begin return Result : constant World := - (Possibles => State_Vectors.Empty_Vector, - Next_Ident => 0, -- dummy - Engine => + (Possibles => State_Vectors.Empty_Vector, + Engine => (Kind => Conjunct_One_Gen, ConO_World => Hold (This), ConO_Func => Func, @@ -657,9 +635,8 @@ package body Kompsos is return World is begin return Result : constant World := - (Possibles => State_Vectors.Empty_Vector, - Next_Ident => 0, -- dummy - Engine => + (Possibles => State_Vectors.Empty_Vector, + Engine => (Kind => Conjunct_Many_Gen, ConM_World => Hold (This), ConM_Func => Func, @@ -689,9 +666,8 @@ package body Kompsos is return World is begin return Result : constant World := - (Possibles => State_Vectors.Empty_Vector, - Next_Ident => This.Next_Ident, - Engine => + (Possibles => State_Vectors.Empty_Vector, + Engine => (Kind => Recurse_Gen, Rec_World => Hold (This), Rec_Index => 1)); @@ -715,9 +691,8 @@ package body Kompsos is begin if Count = 0 then return - (Possibles => State_Vectors.Empty_Vector, - Next_Ident => ID_Number'First, - Engine => (Kind => No_Gen)); + (Possibles => State_Vectors.Empty_Vector, + Engine => (Kind => No_Gen)); end if; return Result : World := This do Result.Roll_Until (Count); |