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


    ------------------------------
    --  Controlled Subprograms  --
    ------------------------------

    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;




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




    ---------------------
    --  Unify Helpers  --
    ---------------------

    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;




    -------------
    --  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.Next_Ident := This.Next_Ident + 1;
            for Potential of This.Possibles loop
                Potential.LVars.Insert (My_Var.Ident, My_Var.Name);
            end loop;
        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
        Result : World;
        Extended : State;
    begin
        Result.Next_Ident := This.Next_Ident;
        for Potential of This.Possibles loop
            if Do_Unify (Potential, Left, Right, Extended) then
                Result.Possibles.Append (Extended);
            end if;
        end loop;
        return Result;
    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 My_World : constant World :=
           (Possibles  => Left.Possibles & Right.Possibles,
            Next_Ident => ID_Number'Max (Left.Next_Ident, Right.Next_Ident));
    end Disjunct;


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


end Kompsos;