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