diff options
| -rw-r--r-- | src/kompsos-pretty_print.adb | 22 | ||||
| -rw-r--r-- | src/kompsos-pretty_print.ads | 10 | ||||
| -rw-r--r-- | src/kompsos.adb | 203 | ||||
| -rw-r--r-- | src/kompsos.ads | 62 |
4 files changed, 132 insertions, 165 deletions
diff --git a/src/kompsos-pretty_print.adb b/src/kompsos-pretty_print.adb index 7ecbb75..8739af8 100644 --- a/src/kompsos-pretty_print.adb +++ b/src/kompsos-pretty_print.adb @@ -62,25 +62,25 @@ package body Kompsos.Pretty_Print is (Item : in Term) return String is begin - case Item.Actual.Kind is + case Item.Kind is + when Null_Term => + return "()"; when Atom_Term => - return Element_Image (Item.Actual.Value); + return Element_Image (Item.Atom); when Var_Term => - return Image (Item.Actual.Refer); + return Image (Item.Var); when Pair_Term => - if Item.Actual.Right.Actual = null then - return Image (Item.Actual.Left); - elsif Item.Actual.Right.Actual.Kind /= Pair_Term then - return Image (Item.Actual.Left) & " . " & Bare (Item.Actual.Right); + if Item.Right.Kind = Null_Term then + return Image (Item.Left); + elsif Item.Right.Kind /= Pair_Term then + return Image (Item.Left) & " . " & Bare (Item.Right); else - return Image (Item.Actual.Left) & " " & Bare (Item.Actual.Right); + return Image (Item.Left) & " " & Bare (Item.Right); end if; end case; end Bare; begin - if Item.Actual = null then - return "()"; - elsif Item.Actual.Kind = Pair_Term then + if Item.Kind = Pair_Term then return "(" & Bare (Item) & ")"; else return Bare (Item); diff --git a/src/kompsos-pretty_print.ads b/src/kompsos-pretty_print.ads index ed9509a..bf0b9d7 100644 --- a/src/kompsos-pretty_print.ads +++ b/src/kompsos-pretty_print.ads @@ -14,6 +14,11 @@ package Kompsos.Pretty_Print is function Image + (Item : in Variable) + return String; + + + function Image (Item : in Term) return String; @@ -37,11 +42,6 @@ private function Image - (Item : in Variable) - return String; - - - function Image (Item : in State) return String; diff --git a/src/kompsos.adb b/src/kompsos.adb index c1d63da..22f0eb9 100644 --- a/src/kompsos.adb +++ b/src/kompsos.adb @@ -18,43 +18,6 @@ package body Kompsos is -- Memory Management -- ------------------------- - -- Terms -- - - procedure Free is new Ada.Unchecked_Deallocation (Term_Component, Term_Component_Access); - - - procedure Initialize - (This : in out Term) is - begin - -- For some reason, under some circumstances this is needed to ensure - -- the access value is actually null. Not sure why. - -- Seems to occur when constructing arrays with the & operator? - This.Actual := null; - end Initialize; - - - procedure Adjust - (This : in out Term) is - begin - if This.Actual /= null then - This.Actual.Count := This.Actual.Count + 1; - end if; - end Adjust; - - - procedure Finalize - (This : in out Term) is - begin - if This.Actual /= null then - This.Actual.Count := This.Actual.Count - 1; - if This.Actual.Count = 0 then - Free (This.Actual); - end if; - end if; - end Finalize; - - - -- World_Holders -- procedure Free is new Ada.Unchecked_Deallocation (World'Class, World_Access); @@ -107,40 +70,21 @@ package body Kompsos is -- Terms -- - function "=" - (Left, Right : in Term) - return Boolean is + function Kind + (This : in Term) + return Term_Kind is begin - if Left.Actual = null and Right.Actual = null then - return True; - end if; - if Left.Actual = null or Right.Actual = null then - return False; - end if; - if Left.Actual.Kind /= Right.Actual.Kind then - return False; - end if; - case Left.Actual.Kind is - when Atom_Term => - return Left.Actual.Value = Right.Actual.Value; - when Var_Term => - return Left.Actual.Refer = Right.Actual.Refer; - when Pair_Term => - return Left.Actual.Left = Right.Actual.Left and Left.Actual.Right = Right.Actual.Right; - end case; - end "="; + return Term_Component (This.Actual.Constant_Reference.Element.all).Kind; + end Kind; function T (Item : in Element_Type) return Term is begin - return My_Term : Term do - My_Term.Actual := new Term_Component'( - Kind => Atom_Term, - Count => 1, - Value => Item); - end return; + return (Actual => Term_Holders.To_Holder (Term_Component'( + Kind => Atom_Term, + Value => Item))); end T; @@ -148,12 +92,9 @@ package body Kompsos is (Item : in Variable) return Term is begin - return My_Term : Term do - My_Term.Actual := new Term_Component'( - Kind => Var_Term, - Count => 1, - Refer => Item); - end return; + return (Actual => Term_Holders.To_Holder (Term_Component'( + Kind => Var_Term, + Refer => Item))); end T; @@ -161,13 +102,10 @@ package body Kompsos is (Item1, Item2 : in Term'Class) return Term is begin - return My_Term : Term do - My_Term.Actual := new Term_Component'( - Kind => Pair_Term, - Count => 1, - Left => Term (Item1), - Right => Term (Item2)); - end return; + return (Actual => Term_Holders.To_Holder (Term_Component'( + Kind => Pair_Term, + Left => Term (Item1), + Right => Term (Item2)))); end T; @@ -176,18 +114,45 @@ package body Kompsos is return Term is begin if Items'Length = 0 then - return My_Term : Term; + return Empty_Term; + else + return T (Items (Items'First), T (Items (Items'First + 1 .. Items'Last))); end if; - return My_Term : Term do - My_Term.Actual := new Term_Component'( - Kind => Pair_Term, - Count => 1, - Left => Items (Items'First), - Right => T (Items (Items'First + 1 .. Items'Last))); - end return; end T; + function Atom + (This : in Term) + return Element_Type is + begin + return Term_Component (This.Actual.Constant_Reference.Element.all).Value; + end Atom; + + + function Var + (This : in Term) + return Variable is + begin + return Term_Component (This.Actual.Constant_Reference.Element.all).Refer; + end Var; + + + function Left + (This : in Term) + return Term is + begin + return Term_Component (This.Actual.Constant_Reference.Element.all).Left; + end Left; + + + function Right + (This : in Term) + return Term is + begin + return Term_Component (This.Actual.Constant_Reference.Element.all).Right; + end Right; + + ------------------------ @@ -213,17 +178,13 @@ package body Kompsos is Item : in Term'Class) return Boolean is begin - if Item.Actual = null then - return True; - end if; - case Item.Actual.Kind is - when Atom_Term => + case Item.Kind is + when Null_Term | Atom_Term => return True; when Var_Term => - return Has_Var (This, Item.Actual.Refer); + return Has_Var (This, Item.Var); when Pair_Term => - return Fully_Contains (This, Item.Actual.Left) and then - Fully_Contains (This, Item.Actual.Right); + return Fully_Contains (This, Item.Left) and then Fully_Contains (This, Item.Right); end case; end Fully_Contains; @@ -233,11 +194,8 @@ package body Kompsos is Item : in Term'Class) return Term'Class is begin - if Item.Actual /= null and then - Item.Actual.Kind = Var_Term and then - This.Subst.Contains (Item.Actual.Refer.Ident) - then - return Walk (This, This.Subst.Constant_Reference (Item.Actual.Refer.Ident)); + if Item.Kind = Var_Term and then This.Subst.Contains (Item.Var.Ident) then + return Walk (This, This.Subst.Constant_Reference (Item.Var.Ident)); else return Item; end if; @@ -254,30 +212,30 @@ package body Kompsos is Real_Right : Term'Class := Right; begin -- Resolve Variable substitution - if Left.Actual /= null and then Left.Actual.Kind = Var_Term then - if Has_Var (Potential, Left.Actual.Refer) then + if Left.Kind = Var_Term then + if Has_Var (Potential, Left.Var) then Real_Left := Walk (Potential, Left); else return False; end if; end if; - if Right.Actual /= null and then Right.Actual.Kind = Var_Term then - if Has_Var (Potential, Right.Actual.Refer) then + if Right.Kind = Var_Term then + if Has_Var (Potential, Right.Var) then Real_Right := Walk (Potential, Right); else return False; end if; end if; - -- Check for equal null Terms - if Real_Left.Actual = null and Real_Right.Actual = null then + -- 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.Actual /= null and then Real_Left.Actual.Kind = Var_Term and then - Real_Right.Actual /= null and then Real_Right.Actual.Kind = Var_Term and then + if Real_Left.Kind = Var_Term and then + Real_Right.Kind = Var_Term and then Real_Left = Real_Right then Extended := Potential; @@ -285,35 +243,30 @@ package body Kompsos is end if; -- Unify Variable and other Terms by introducing a new substitution - if Real_Left.Actual /= null and then Real_Left.Actual.Kind = Var_Term then - if Real_Right.Actual /= null and then Real_Right.Actual.Kind = Pair_Term and then + 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.Actual.Refer.Ident, Term (Real_Right)); + Extended.Subst.Insert (Real_Left.Var.Ident, Term (Real_Right)); return True; end if; - if Real_Right.Actual /= null and then Real_Right.Actual.Kind = Var_Term then - if Real_Left.Actual /= null and then Real_Left.Actual.Kind = Pair_Term and then + 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.Actual.Refer.Ident, Term (Real_Left)); + Extended.Subst.Insert (Real_Right.Var.Ident, Term (Real_Left)); return True; end if; - -- Don't want any null terms beyond here - if Real_Left.Actual = null or Real_Right.Actual = null then - return False; - end if; - -- Unify equal Atom Terms - if Real_Left.Actual.Kind = Atom_Term and then - Real_Right.Actual.Kind = Atom_Term and then + if Real_Left.Kind = Atom_Term and then + Real_Right.Kind = Atom_Term and then Real_Left = Real_Right then Extended := Potential; @@ -321,18 +274,16 @@ package body Kompsos is end if; -- Unify Pair Terms by unifying each corresponding part - if Real_Left.Actual.Kind = Pair_Term and then - Real_Right.Actual.Kind = Pair_Term and then + 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 declare Middle : State; begin - return - Do_Unify (Potential, Real_Left.Actual.Left, Real_Right.Actual.Left, Middle) - and then - Do_Unify (Middle, Real_Left.Actual.Right, Real_Right.Actual.Right, Extended); + return Do_Unify (Potential, Real_Left.Left, Real_Right.Left, Middle) and then + Do_Unify (Middle, Real_Left.Right, Real_Right.Right, Extended); end; end if; @@ -927,7 +878,7 @@ package body Kompsos is return World is begin return Result : World := This do - Result.Unify (Null_Term, Nil_Term); + Result.Unify (Empty_Term, Nil_Term); end return; end Nil; diff --git a/src/kompsos.ads b/src/kompsos.ads index 0463f6f..37533be 100644 --- a/src/kompsos.ads +++ b/src/kompsos.ads @@ -27,14 +27,15 @@ package Kompsos is -- Datatypes -- ----------------- + type Variable is private; + + + type Term_Kind is (Null_Term, Atom_Term, Var_Term, Pair_Term); + type Term is tagged private; type Term_Array is array (Positive range <>) of Term; - Null_Term : constant Term; - - function "=" - (Left, Right : in Term) - return Boolean; + Empty_Term : constant Term; function T (Item : in Element_Type) @@ -48,7 +49,29 @@ package Kompsos is (Items : in Term_Array) return Term; - -- Might include subprograms to retrieve Term contents later? + function Kind + (This : in Term) + return Term_Kind; + + function Atom + (This : in Term) + return Element_Type + with Pre => This.Kind = Atom_Term; + + function Var + (This : in Term) + return Variable + with Pre => This.Kind = Var_Term; + + function Left + (This : in Term) + return Term + with Pre => This.Kind = Pair_Term; + + function Right + (This : in Term) + return Term + with Pre => This.Kind = Pair_Term; type World is tagged private; @@ -392,11 +415,14 @@ private - type Term_Kind is (Atom_Term, Var_Term, Pair_Term); + type Term_Root is abstract tagged null record; - type Term_Component (Kind : Term_Kind) is record - Count : Long_Integer; + package Term_Holders is new Ada.Containers.Indefinite_Holders (Term_Root'Class); + + type Term_Component (Kind : Term_Kind) is new Term_Root with record case Kind is + when Null_Term => + null; when Atom_Term => Value : Element_Type; when Var_Term => @@ -406,22 +432,12 @@ private end case; end record; - type Term_Component_Access is access Term_Component; - - type Term is new Ada.Finalization.Controlled with record - Actual : Term_Component_Access; + type Term is tagged record + Actual : Term_Holders.Holder := Term_Holders.To_Holder (Term_Component'(Kind => Null_Term)); end record; - overriding procedure Initialize - (This : in out Term); - - overriding procedure Adjust - (This : in out Term); - - overriding procedure Finalize - (This : in out Term); - - Null_Term : constant Term := (Ada.Finalization.Controlled with Actual => null); + Empty_Term : constant Term := + (Actual => Term_Holders.To_Holder (Term_Component'(Kind => Null_Term))); package Term_Array_Holders is new Ada.Containers.Indefinite_Holders (Term_Array); |