Initial commit

4 files changed, 842 insertions, 0 deletions

diff --git a/src/kompsos-pretty_print.adb b/src/kompsos-pretty_print.adb
new file mode 100644
index 0000000..d1d89b8
--- /dev/null
+++ b/src/kompsos-pretty_print.adb
@@ -0,0 +1,142 @@
+
+
+--  Programmed by Jedidiah Barber
+--  Licensed under the Sunset License v1.0
+
+--  See license.txt for further details
+
+
+with
+
+    Ada.Characters.Latin_1,
+    Ada.Strings.Fixed;
+
+
+package body Kompsos.Pretty_Print is
+
+
+    package Latin renames Ada.Characters.Latin_1;
+    package Str   renames Ada.Strings;
+
+
+
+
+    function Image
+           (Item : in Integer)
+        return String is
+    begin
+        return Str.Fixed.Trim (Integer'Image (Item), Str.Left);
+    end Image;
+
+
+    function Image
+           (Item : in ID_Number)
+        return String is
+    begin
+        return Str.Fixed.Trim (ID_Number'Image (Item), Str.Left);
+    end Image;
+
+
+
+
+    function Image
+           (Item : in Variable)
+        return String is
+    begin
+        return "Var#" & Image (Item.Ident) &
+           (if SU.Length (Item.Name) /= 0
+            then "/" & SU.To_String (Item.Name)
+            else "");
+    end Image;
+
+
+
+
+    function Image
+           (Item : in Term)
+        return String
+    is
+        function Bare
+               (Item : in Term)
+            return String is
+        begin
+            case Item.Actual.Kind is
+            when Atom_Term =>
+                return Element_Image (Item.Actual.Value);
+            when Var_Term =>
+                return Image (Item.Actual.Refer);
+            when Pair_Term =>
+                if Item.Actual.Right.Actual = null then
+                    return Image (Item.Actual.Left);
+                else
+                    return Image (Item.Actual.Left) & " " & Bare (Item.Actual.Right);
+                end if;
+            end case;
+        end Bare;
+    begin
+        if Item.Actual = null then
+            return "()";
+        elsif Item.Actual.Kind = Pair_Term then
+            return "(" & Bare (Item) & ")";
+        else
+            return Bare (Item);
+        end if;
+    end Image;
+
+
+
+
+    function Image
+           (Item : in State)
+        return String
+    is
+        Result : SU.Unbounded_String;
+        My_Var : Variable;
+    begin
+        SU.Append (Result, Latin.HT & "Variables:");
+        if Item.LVars.Is_Empty then
+            SU.Append (Result, " N/A" & Latin.LF);
+        else
+            SU.Append (Result, Latin.LF);
+            for Iter in Item.LVars.Iterate loop
+                My_Var := (Ident => Name_Maps.Key (Iter), Name => Name_Maps.Element (Iter));
+                SU.Append (Result, Latin.HT & Latin.HT & Image (My_Var) & Latin.LF);
+            end loop;
+        end if;
+        SU.Append (Result, Latin.HT & "Substitution:");
+        if Item.Subst.Is_Empty then
+            SU.Append (Result, " N/A" & Latin.LF);
+        else
+            SU.Append (Result, Latin.LF);
+            for Iter in Item.Subst.Iterate loop
+                SU.Append (Result, Latin.HT & Latin.HT &
+                    Image (Binding_Maps.Key (Iter)) & " => " &
+                    Image (Binding_Maps.Element (Iter)) & Latin.LF);
+            end loop;
+        end if;
+        return -Result;
+    end Image;
+
+
+
+
+    function Image
+           (Item : in World)
+        return String
+    is
+        Result : SU.Unbounded_String;
+    begin
+        if Item.Possibles.Is_Empty then
+            return "States: N/A" & Latin.LF;
+        end if;
+        for Index in Integer range Item.Possibles.First_Index .. Item.Possibles.Last_Index loop
+            SU.Append (Result, "State#" & Image (Index) & ":" & Latin.LF);
+            SU.Append (Result, Image (Item.Possibles.Constant_Reference (Index)));
+        end loop;
+        return SU.Slice (Result, 1, SU.Length (Result) - 1);
+    end Image;
+
+
+end Kompsos.Pretty_Print;
+
+
diff --git a/src/kompsos-pretty_print.ads b/src/kompsos-pretty_print.ads
new file mode 100644
index 0000000..3ef7ac7
--- /dev/null
+++ b/src/kompsos-pretty_print.ads
@@ -0,0 +1,33 @@
+
+
+--  Programmed by Jedidiah Barber
+--  Licensed under the Sunset License v1.0
+
+--  See license.txt for further details
+
+
+generic
+    with function Element_Image
+           (Item : in Element_Type)
+        return String;
+package Kompsos.Pretty_Print is
+
+
+    function Image
+           (Item : in Variable)
+        return String;
+
+
+    function Image
+           (Item : in Term)
+        return String;
+
+
+    function Image
+           (Item : in World)
+        return String;
+
+
+end Kompsos.Pretty_Print;
+
+
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;
+
+
diff --git a/src/kompsos.ads b/src/kompsos.ads
new file mode 100644
index 0000000..c25cf52
--- /dev/null
+++ b/src/kompsos.ads
@@ -0,0 +1,243 @@
+
+
+--  Programmed by Jedidiah Barber
+--  Licensed under the Sunset License v1.0
+
+--  See license.txt for further details
+
+
+with
+
+    Ada.Strings.Unbounded;
+
+private with
+
+    Ada.Containers.Ordered_Maps,
+    Ada.Containers.Vectors,
+    Ada.Finalization;
+
+
+generic
+    type Element_Type is private;
+package Kompsos is
+
+
+    type Variable is private;
+    type Variable_Array is array (Positive range <>) of Variable;
+
+
+
+
+    type Term is tagged private;
+    type Term_Array is array (Positive range <>) of Term;
+
+    --  Can also be constructed by supplying an empty array to T
+    --  or just declaring a Term without initial value.
+    Null_Term : constant Term;
+
+    function "="
+           (Left, Right : in Term)
+        return Boolean;
+
+    function T
+           (Item : in Element_Type)
+        return Term;
+
+    function T
+           (Item : in Variable)
+        return Term;
+
+    function T
+           (Items : in Term_Array)
+        return Term;
+
+    --  Might include subprograms to retrieve Term contents later?
+
+
+
+
+    type World is tagged private;
+
+    Empty_World : constant World;
+
+
+
+
+    function Fresh
+           (This : in out World)
+        return Variable;
+
+    function Fresh
+           (This : in out World;
+            Name : in     String)
+        return Variable;
+
+    function Fresh
+           (This : in out World;
+            Name : in     Ada.Strings.Unbounded.Unbounded_String)
+        return Variable;
+
+
+
+
+    function Unify
+           (This  : in World;
+            Left  : in Variable;
+            Right : in Element_Type)
+        return World;
+
+    procedure Unify
+           (This  : in out World;
+            Left  : in     Variable;
+            Right : in     Element_Type);
+
+    function Unify
+           (This        : in World;
+            Left, Right : in Variable)
+        return World;
+
+    procedure Unify
+           (This        : in out World;
+            Left, Right : in     Variable);
+
+    function Unify
+           (This  : in World;
+            Left  : in Variable;
+            Right : in Term'Class)
+        return World;
+
+    procedure Unify
+           (This  : in out World;
+            Left  : in     Variable;
+            Right : in     Term'Class);
+
+    function Unify
+           (This        : in World;
+            Left, Right : in Term'Class)
+        return World;
+
+    procedure Unify
+           (This        : in out World;
+            Left, Right : in     Term'Class);
+
+
+
+
+    function Disjunct
+           (Left, Right : in World)
+        return World;
+
+    procedure Disjunct
+           (This  : in out World;
+            Right : in     World);
+
+
+private
+
+
+    package SU renames Ada.Strings.Unbounded;
+
+
+    function "+"
+           (Item : in String)
+        return SU.Unbounded_String
+    renames SU.To_Unbounded_String;
+
+    function "-"
+           (Item : in SU.Unbounded_String)
+        return String
+    renames SU.To_String;
+
+
+
+
+    --  2^32 possible variables per World is enough for anybody, right?
+    type ID_Number is mod 2 ** 32;
+
+    type Variable is record
+        Ident : ID_Number;
+        Name  : SU.Unbounded_String;
+    end record;
+
+
+
+
+    type Term_Kind is (Atom_Term, Var_Term, Pair_Term);
+
+    type Term_Component (Kind : Term_Kind) is record
+        Count : Long_Integer;
+        case Kind is
+        when Atom_Term =>
+            Value : Element_Type;
+        when Var_Term =>
+            Refer : Variable;
+        when Pair_Term =>
+            Left, Right : Term;
+        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;
+    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);
+
+
+
+
+    package Name_Maps is new Ada.Containers.Ordered_Maps
+       (Key_Type     => ID_Number,
+        Element_Type => SU.Unbounded_String,
+        "="          => SU."=");
+
+    package Binding_Maps is new Ada.Containers.Ordered_Maps
+       (Key_Type     => ID_Number,
+        Element_Type => Term);
+
+    type State is record
+        LVars : Name_Maps.Map;
+        Subst : Binding_Maps.Map;
+    end record;
+
+    Empty_State : constant State :=
+       (LVars => Name_Maps.Empty_Map,
+        Subst => Binding_Maps.Empty_Map);
+
+
+
+
+    --  obviously this World definition will need revision for delays and generators
+
+    --  going to have to turn worlds into a similar sort of reference counted recursive
+    --  controlled type along the lines of what terms are, in order to make them into generators
+
+    package State_Vectors is new Ada.Containers.Vectors
+       (Index_Type   => Positive,
+        Element_Type => State);
+
+    use type State_Vectors.Vector;
+
+    type World is tagged record
+        Possibles  : State_Vectors.Vector;
+        Next_Ident : ID_Number;
+    end record;
+
+    Empty_World : constant World :=
+       (Possibles  => State_Vectors.Empty_Vector & Empty_State,
+        Next_Ident => 0);
+
+
+end Kompsos;
+
+