--  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 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
           (Item1, Item2 : in Term'Class)
        return Term;

    function T
           (Items : in Term_Array)
        return Term;

    --  Might include subprograms to retrieve Term contents later?


    type Mu_World is tagged private;
    type Mu_World_Array is array (Positive range <>) of Mu_World;

    Empty_Mu_World : constant Mu_World;




    function Fresh
           (This : in out Mu_World'Class)
        return Term;

    function Fresh
           (This : in out Mu_World'Class;
            Name : in     String)
        return Term;

    function Fresh
           (This : in out Mu_World'Class;
            Name : in     Ada.Strings.Unbounded.Unbounded_String)
        return Term;




    function Unify
           (This  : in Mu_World;
            Left  : in Term'Class;
            Right : in Element_Type)
        return Mu_World;

    procedure Unify
           (This  : in out Mu_World;
            Left  : in     Term'Class;
            Right : in     Element_Type);

    function Unify
           (This        : in Mu_World;
            Left, Right : in Term'Class)
        return Mu_World;

    procedure Unify
           (This        : in out Mu_World;
            Left, Right : in     Term'Class);




    function Disjunct
           (Left, Right : in Mu_World)
        return Mu_World;

    procedure Disjunct
           (This  : in out Mu_World;
            Right : in     Mu_World);

    function Disjunct
           (Inputs : in Mu_World_Array)
        return Mu_World;

    procedure Disjunct
           (This   : in out Mu_World;
            Inputs : in     Mu_World_Array);




    function Recurse
           (This : in Mu_World)
        return Mu_World;

    procedure Recurse
           (This : in out Mu_World);




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

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

    procedure Force
           (This  : in out Mu_World;
            Count : in     Positive);

    procedure Force_All
           (This : in out Mu_World);

    function Failed
           (This : in out Mu_World)
        return Boolean;


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 Mu_World'Class;

    type World_Holder is new Ada.Finalization.Controlled with record
        Ptr : World_Access;
    end record;

    overriding procedure Initialize
           (This : in out World_Holder);

    overriding procedure Adjust
           (This : in out World_Holder);

    overriding procedure Finalize
           (This : in out World_Holder);

    function Hold
           (This : in Mu_World'Class)
        return World_Holder;

    procedure Swap
           (Left, Right : in out World_Holder);

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

    type Generator (Kind : Generator_Kind := No_Gen) is record
        case Kind is
        when No_Gen =>
            null;
        when Fresh_Gen =>
            Frs_World  : World_Holder;
            Frs_Name   : SU.Unbounded_String;
        when Unify_Gen =>
            Uni_World  : World_Holder;
            Uni_Term1  : Term;
            Uni_Term2  : Term;
        when Buffer_Gen =>
            Buff_World : World_Holder;
        when Disjunct_Gen =>
            Dis_World1 : World_Holder;
            Dis_World2 : World_Holder;
        when Recurse_Gen =>
            Rec_World  : World_Holder;
            Rec_Index  : Positive;
        end case;
    end record;

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

    type Mu_World is tagged record
        Possibles  : State_Vectors.Vector;
        Next_Ident : ID_Number;
        Engine     : Generator;
    end record;

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

    procedure Rollover
           (This : in out Mu_World);

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

    use type State_Vectors.Vector;

    Empty_Mu_World : constant Mu_World :=
       (Possibles  => State_Vectors.Empty_Vector & Empty_State,
        Next_Ident => 0,
        Engine     => (Kind => No_Gen));


end Kompsos;