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




    function Recurse
           (This : in World)
        return World;

    procedure Recurse
           (This : in out World);




    function Take
           (This  : in World;
            Count : in Natural)
        return World;

    procedure Take
           (This  : in out World;
            Count : in     Natural);


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




    type World_Access is access World;

    type Generator_Kind is (No_Gen, Fresh_Gen, Unify_Gen, Disjunct_Gen, Recurse_Gen);

    type Generator (Kind : Generator_Kind := No_Gen) is record
        case Kind is
        when No_Gen =>
            null;
        when Fresh_Gen =>
            FrG_World   : World_Access;
            FrG_Index   : Positive;
            FrG_Name    : SU.Unbounded_String;
        when Unify_Gen =>
            UniG_World  : World_Access;
            UniG_Index  : Positive;
            UniG_Term1  : Term;
            UniG_Term2  : Term;
        when Disjunct_Gen =>
            DisG_World1 : World_Access;
            DisG_Index1 : Positive;
            DisG_World2 : World_Access;
            DisG_Index2 : Positive;
        when Recurse_Gen =>
            RecG_World  : World_Access;
            RecG_Index  : Positive;
        end case;
    end record;

    package State_Vectors is new Ada.Containers.Vectors
       (Index_Type   => Positive,
        Element_Type => State);

    type World is new Ada.Finalization.Controlled with record
        Possibles  : State_Vectors.Vector;
        Next_Ident : ID_Number;
        Engine     : Generator;
    end record;

    overriding procedure Adjust
           (This : in out World);

    overriding procedure Finalize
           (This : in out World);

    function Has_State
           (This  : in out World;
            Index : in     Positive)
        return Boolean;

    procedure Rollover
           (This : in out World);

    procedure Roll_Until
           (This  : in out World;
            Index : in     Positive);

    use type State_Vectors.Vector;

    Empty_World : constant World := (Ada.Finalization.Controlled with
        Possibles  => State_Vectors.Empty_Vector & Empty_State,
        Next_Ident => 0,
        Engine     => (Kind => No_Gen));


end Kompsos;