Initial commit

1 files changed, 243 insertions, 0 deletions

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;
+
+