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


    -------------------------
    --  Memory Management  --
    -------------------------

    --  Terms  --

    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;




    --  Worlds  --

    procedure Free is new Ada.Unchecked_Deallocation (World, World_Access);


    procedure Adjust
           (This : in out World) is
    begin
        case This.Engine.Kind is
        when No_Gen =>
            null;
        when Fresh_Gen =>
            This.Engine.FrG_World := new World'(This.Engine.FrG_World.all);
        when Unify_Gen =>
            This.Engine.UniG_World := new World'(This.Engine.UniG_World.all);
        when Disjunct_Gen =>
            This.Engine.DisG_World1 := new World'(This.Engine.DisG_World1.all);
            This.Engine.DisG_World2 := new World'(This.Engine.DisG_World2.all);
        when Recurse_Gen =>
            This.Engine.RecG_World := new World'(This.Engine.RecG_World.all);
        end case;
    end Adjust;


    procedure Finalize
           (This : in out World) is
    begin
        case This.Engine.Kind is
        when No_Gen =>
            null;
        when Fresh_Gen =>
            Free (This.Engine.FrG_World);
        when Unify_Gen =>
            Free (This.Engine.UniG_World);
        when Disjunct_Gen =>
            Free (This.Engine.DisG_World1);
            Free (This.Engine.DisG_World2);
        when Recurse_Gen =>
            Free (This.Engine.RecG_World);
        end case;
    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
           (Item1, Item2 : in Term)
        return Term is
    begin
        return My_Term : Term do
            My_Term.Actual := new Term_Component'(
                Kind  => Pair_Term,
                Count => 1,
                Left  => Item1,
                Right => Item2);
        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;




    ------------------------
    --  Internal Helpers  --
    ------------------------

    --  Unification  --

    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;




    --  Lazy World Generation --

    function Has_State
           (This  : in out World;
            Index : in     Positive)
        return Boolean is
    begin
        This.Roll_Until (Index);
        return This.Possibles.Last_Index >= Index;
    end Has_State;


    procedure Roll_Fresh_Gen
           (This : in out World) is
    begin
        if not This.Engine.FrG_World.Has_State (This.Engine.FrG_Index) then
            This.Engine := (Kind => No_Gen);
            return;
        end if;
        This.Possibles.Append (This.Engine.FrG_World.Possibles.Element (This.Engine.FrG_Index));
        This.Possibles.Reference (This.Possibles.Last_Index).LVars.Insert
           (This.Engine.FrG_World.Next_Ident,
            This.Engine.FrG_Name);
        This.Engine.FrG_Index := This.Engine.FrG_Index + 1;
    end Roll_Fresh_Gen;


    procedure Roll_Unify_Gen
           (This : in out World)
    is
        Extended : State;
    begin
        loop
            if not This.Engine.UniG_World.Has_State (This.Engine.UniG_Index) then
                This.Engine := (Kind => No_Gen);
                return;
            end if;
            exit when Do_Unify
               (This.Engine.UniG_World.Possibles (This.Engine.UniG_Index),
                This.Engine.UniG_Term1,
                This.Engine.UniG_Term2,
                Extended);
            This.Engine.UniG_Index := This.Engine.UniG_Index + 1;
        end loop;
        This.Possibles.Append (Extended);
        This.Engine.UniG_Index := This.Engine.UniG_Index + 1;
    end Roll_Unify_Gen;


    procedure Roll_Disjunct_Gen
           (This : in out World)
    is
        Temp_World : World_Access;
        Temp_Index : Positive;
    begin
        if not This.Engine.DisG_World1.Has_State (This.Engine.DisG_Index1) then
            if not This.Engine.DisG_World2.Has_State (This.Engine.DisG_Index2) then
                This.Engine := (Kind => No_Gen);
                return;
            end if;
            This.Possibles.Append (This.Engine.DisG_World2.Possibles (This.Engine.DisG_Index2));
            This.Engine.DisG_Index2 := This.Engine.DisG_Index2 + 1;
        else
            This.Possibles.Append (This.Engine.DisG_World1.Possibles (This.Engine.DisG_Index1));
            This.Engine.DisG_Index1 := This.Engine.DisG_Index1 + 1;
        end if;
        Temp_World := This.Engine.DisG_World1;
        Temp_Index := This.Engine.DisG_Index1;
        This.Engine.DisG_World1 := This.Engine.DisG_World2;
        This.Engine.DisG_Index1 := This.Engine.DisG_Index2;
        This.Engine.DisG_World2 := Temp_World;
        This.Engine.DisG_Index2 := Temp_Index;
    end Roll_Disjunct_Gen;


    procedure Roll_Recurse_Gen
           (This : in out World) is
    begin
        if not This.Engine.RecG_World.Has_State (This.Engine.RecG_Index) then
            if This.Engine.RecG_Index = 1 then
                This.Engine := (Kind => No_Gen);
                return;
            end if;
            This.Engine.RecG_Index := 1;
        end if;
        This.Possibles.Append (This.Engine.RecG_World.Possibles (This.Engine.RecG_Index));
        This.Engine.RecG_Index := This.Engine.RecG_Index + 1;
    end Roll_Recurse_Gen;


    procedure Rollover
           (This : in out World) is
    begin
        case This.Engine.Kind is
        when No_Gen       => null;
        when Fresh_Gen    => This.Roll_Fresh_Gen;
        when Unify_Gen    => This.Roll_Unify_Gen;
        when Disjunct_Gen => This.Roll_Disjunct_Gen;
        when Recurse_Gen  => This.Roll_Recurse_Gen;
        end case;
    end Rollover;


    procedure Roll_Until
           (This  : in out World;
            Index : in     Positive) is
    begin
        while This.Possibles.Last_Index < Index and This.Engine.Kind /= No_Gen loop
            This.Rollover;
        end loop;
    end Roll_Until;




    -----------------------------
    --  Public API Operations  --
    -----------------------------

    --  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 := (Ada.Finalization.Controlled with
                Possibles  => State_Vectors.Empty_Vector,
                Next_Ident => This.Next_Ident + 1,
                Engine     =>
                   (Kind      => Fresh_Gen,
                    FrG_World => new World'(This),
                    FrG_Index => 1,
                    FrG_Name  => Name));
            This.Rollover;
        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
    begin
        return Result : World := (Ada.Finalization.Controlled with
            Possibles  => State_Vectors.Empty_Vector,
            Next_Ident => This.Next_Ident,
            Engine     =>
               (Kind       => Unify_Gen,
                UniG_World => new World'(This),
                UniG_Index => 1,
                UniG_Term1 => Term (Left),
                UniG_Term2 => Term (Right)))
        do
            Result.Rollover;
        end return;
    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 Result : World := (Ada.Finalization.Controlled with
            Possibles  => State_Vectors.Empty_Vector,
            Next_Ident => ID_Number'Max (Left.Next_Ident, Right.Next_Ident),
            Engine     =>
               (Kind        => Disjunct_Gen,
                DisG_World1 => new World'(Left),
                DisG_Index1 => 1,
                DisG_World2 => new World'(Right),
                DisG_Index2 => 1))
        do
            Result.Rollover;
        end return;
    end Disjunct;


    procedure Disjunct
           (This  : in out World;
            Right : in     World) is
    begin
        This := Disjunct (This, Right);
    end Disjunct;




    --  Recurse  --

    function Recurse
           (This : in World)
        return World is
    begin
        return Result : World := (Ada.Finalization.Controlled with
            Possibles  => State_Vectors.Empty_Vector,
            Next_Ident => This.Next_Ident,
            Engine     =>
               (Kind       => Recurse_Gen,
                RecG_World => new World'(This),
                RecG_Index => 1))
        do
            Result.Rollover;
        end return;
    end Recurse;


    procedure Recurse
           (This : in out World) is
    begin
        This := This.Recurse;
    end Recurse;




    --  Take  --

    function Take
           (This  : in World;
            Count : in Natural)
        return World is
    begin
        if Count = 0 then
            return (Ada.Finalization.Controlled with
                Possibles  => State_Vectors.Empty_Vector,
                Next_Ident => ID_Number'First,
                Engine     => (Kind => No_Gen));
        end if;
        return Result : World := This do
            Result.Roll_Until (Count);
            if Result.Possibles.Last_Index > Count then
                Result.Possibles.Set_Length (Ada.Containers.Count_Type (Count));
            end if;
            Result.Engine := (Kind => No_Gen);
        end return;
    end Take;


    procedure Take
           (This  : in out World;
            Count : in     Natural) is
    begin
        This := This.Take (Count);
    end Take;


end Kompsos;