Initial commit

1 files changed, 424 insertions, 0 deletions

diff --git a/src/kompsos.adb b/src/kompsos.adb
new file mode 100644
index 0000000..5997ddf
--- /dev/null
+++ b/src/kompsos.adb
@@ -0,0 +1,424 @@
+
+
+--  Programmed by Jedidiah Barber
+--  Licensed under the Sunset License v1.0
+
+--  See license.txt for further details
+
+
+with
+
+    Ada.Unchecked_Deallocation;
+
+
+package body Kompsos is
+
+
+    ------------------------------
+    --  Controlled Subprograms  --
+    ------------------------------
+
+    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;
+
+
+
+
+    -------------
+    --  Terms  --
+    -------------
+
+    function "="
+           (Left, Right : in Term)
+        return Boolean 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 "=";
+
+
+    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;
+    end T;
+
+
+    function T
+           (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;
+    end T;
+
+
+    function T
+           (Items : in Term_Array)
+        return Term is
+    begin
+        if Items'Length = 0 then
+            return My_Term : Term;
+        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;
+
+
+
+
+    ---------------------
+    --  Unify Helpers  --
+    ---------------------
+
+    function Has_Var
+           (This : in State;
+            Var  : in Variable)
+        return Boolean
+    is
+        use type SU.Unbounded_String;
+    begin
+        return This.LVars.Contains (Var.Ident) and then
+            This.LVars.Constant_Reference (Var.Ident) = Var.Name;
+    end Has_Var;
+
+
+    function Fully_Contains
+           (This : in State;
+            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 =>
+            return True;
+        when Var_Term =>
+            return Has_Var (This, Item.Actual.Refer);
+        when Pair_Term =>
+            return Fully_Contains (This, Item.Actual.Left) and then
+                Fully_Contains (This, Item.Actual.Right);
+        end case;
+    end Fully_Contains;
+
+
+    function Walk
+           (This : in State;
+            Item : in Term'Class)
+        return Term'Class is
+    begin
+        if This.Subst.Contains (Item.Actual.Refer.Ident) then
+            return Walk (This, This.Subst.Constant_Reference (Item.Actual.Refer.Ident));
+        else
+            return Item;
+        end if;
+    end Walk;
+
+
+    function Do_Unify
+           (Potential   : in     State;
+            Left, Right : in     Term'Class;
+            Extended    :    out State)
+        return Boolean
+    is
+        Real_Left  : Term'Class := Left;
+        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
+                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
+                Real_Right := Walk (Potential, Right);
+            else
+                return False;
+            end if;
+        end if;
+
+        --  Check for null Terms
+        if Real_Left.Actual = null and Real_Right.Actual = null then
+            Extended := Potential;
+            return True;
+        end if;
+        if Real_Left.Actual = null or Real_Right.Actual = null then
+            return False;
+        end if;
+
+        --  Unify equal Variable Terms
+        if  Real_Left.Actual.Kind = Var_Term and then
+            Real_Right.Actual.Kind = Var_Term and then
+            Real_Left = Real_Right
+        then
+            Extended := Potential;
+            return True;
+        end if;
+
+        --  Unify equal Atom Terms
+        if  Real_Left.Actual.Kind = Atom_Term and then
+            Real_Right.Actual.Kind = Atom_Term and then
+            Real_Left = Real_Right
+        then
+            Extended := Potential;
+            return True;
+        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
+            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);
+            end;
+        end if;
+
+        --  Unify Variable and other Terms by introducing a new substitution
+        if Real_Left.Actual.Kind = Var_Term then
+            if  Real_Right.Actual.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));
+            return True;
+        end if;
+        if Real_Right.Actual.Kind = Var_Term then
+            if  Real_Left.Actual.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));
+            return True;
+        end if;
+
+        --  Not sure how things get here, but if all else fails
+        return False;
+    end Do_Unify;
+
+
+
+
+    -------------
+    --  Fresh  --
+    -------------
+
+    function Fresh
+           (This : in out World)
+        return Variable is
+    begin
+        return This.Fresh (+"");
+    end Fresh;
+
+
+    function Fresh
+           (This : in out World;
+            Name : in     String)
+        return Variable is
+    begin
+        return This.Fresh (+Name);
+    end Fresh;
+
+
+    function Fresh
+           (This : in out World;
+            Name : in     Ada.Strings.Unbounded.Unbounded_String)
+        return Variable is
+    begin
+        return My_Var : constant Variable := (Ident => This.Next_Ident, Name => Name) do
+            This.Next_Ident := This.Next_Ident + 1;
+            for Potential of This.Possibles loop
+                Potential.LVars.Insert (My_Var.Ident, My_Var.Name);
+            end loop;
+        end return;
+    end Fresh;
+
+
+
+
+    -------------
+    --  Unify  --
+    -------------
+
+    function Unify
+           (This  : in World;
+            Left  : in Variable;
+            Right : in Element_Type)
+        return World is
+    begin
+        return This.Unify (T (Left), T (Right));
+    end Unify;
+
+
+    procedure Unify
+           (This  : in out World;
+            Left  : in     Variable;
+            Right : in     Element_Type) is
+    begin
+        This := This.Unify (T (Left), T (Right));
+    end Unify;
+
+
+    function Unify
+           (This        : in World;
+            Left, Right : in Variable)
+        return World is
+    begin
+        return This.Unify (T (Left), T (Right));
+    end Unify;
+
+
+    procedure Unify
+           (This        : in out World;
+            Left, Right : in     Variable) is
+    begin
+        This := This.Unify (T (Left), T (Right));
+    end Unify;
+
+
+    function Unify
+           (This  : in World;
+            Left  : in Variable;
+            Right : in Term'Class)
+        return World is
+    begin
+        return This.Unify (T (Left), Right);
+    end Unify;
+
+
+    procedure Unify
+           (This  : in out World;
+            Left  : in     Variable;
+            Right : in     Term'Class) is
+    begin
+        This := This.Unify (T (Left), Right);
+    end Unify;
+
+
+    function Unify
+           (This        : in World;
+            Left, Right : in Term'Class)
+        return World
+    is
+        Result : World;
+        Extended : State;
+    begin
+        Result.Next_Ident := This.Next_Ident;
+        for Potential of This.Possibles loop
+            if Do_Unify (Potential, Left, Right, Extended) then
+                Result.Possibles.Append (Extended);
+            end if;
+        end loop;
+        return Result;
+    end Unify;
+
+
+    procedure Unify
+           (This        : in out World;
+            Left, Right : in     Term'Class) is
+    begin
+        This := This.Unify (Left, Right);
+    end Unify;
+
+
+
+
+    ----------------
+    --  Disjunct  --
+    ----------------
+
+    function Disjunct
+           (Left, Right : in World)
+        return World is
+    begin
+        return My_World : constant World :=
+           (Possibles  => Left.Possibles & Right.Possibles,
+            Next_Ident => ID_Number'Max (Left.Next_Ident, Right.Next_Ident));
+    end Disjunct;
+
+
+    procedure Disjunct
+           (This  : in out World;
+            Right : in     World) is
+    begin
+        This := Disjunct (This, Right);
+    end Disjunct;
+
+
+end Kompsos;
+
+