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




    --  World_Holders  --

    procedure Free is new Ada.Unchecked_Deallocation (Mu_World'Class, World_Access);


    procedure Initialize
           (This : in out World_Holder) is
    begin
        This.Ptr := null;
    end Initialize;


    procedure Adjust
           (This : in out World_Holder) is
    begin
        This.Ptr := new Mu_World'Class'(This.Ptr.all);
    end Adjust;


    procedure Finalize
           (This : in out World_Holder) is
    begin
        Free (This.Ptr);
    end Finalize;


    function Hold
           (This : in Mu_World'Class)
        return World_Holder is
    begin
        return (Ada.Finalization.Controlled with Ptr => new Mu_World'Class'(This));
    end Hold;


    procedure Swap
           (Left, Right : in out World_Holder)
    is
        Temp_Ptr : World_Access := Left.Ptr;
    begin
        Left.Ptr := Right.Ptr;
        Right.Ptr := Temp_Ptr;
    end Swap;




    -------------
    --  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'Class)
        return Term is
    begin
        return My_Term : Term do
            My_Term.Actual := new Term_Component'(
                Kind  => Pair_Term,
                Count => 1,
                Left  => Term (Item1),
                Right => Term (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  Item.Actual /= null and then
            Item.Actual.Kind = Var_Term and then
            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 equal null Terms
        if Real_Left.Actual = null and Real_Right.Actual = null then
            Extended := Potential;
            return True;
        end if;

        --  Unify equal Variable Terms
        if  Real_Left.Actual /= null and then Real_Left.Actual.Kind = Var_Term and then
            Real_Right.Actual /= null and then Real_Right.Actual.Kind = Var_Term and then
            Real_Left = Real_Right
        then
            Extended := Potential;
            return True;
        end if;

        --  Unify Variable and other Terms by introducing a new substitution
        if Real_Left.Actual /= null and then Real_Left.Actual.Kind = Var_Term then
            if  Real_Right.Actual /= null and then 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 /= null and then Real_Right.Actual.Kind = Var_Term then
            if  Real_Left.Actual /= null and then 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;

        --  Don't want any null terms beyond here
        if Real_Left.Actual = null or Real_Right.Actual = null then
            return False;
        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;

        --  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 Mu_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 Mu_World) is
    begin
        This.Engine.Frs_World.Ptr.Rollover;
        for Potential of This.Engine.Frs_World.Ptr.Possibles loop
            Potential.LVars.Insert (This.Engine.Frs_World.Ptr.Next_Ident, This.Engine.Frs_Name);
            This.Possibles.Append (Potential);
        end loop;
        if This.Engine.Frs_World.Ptr.Engine.Kind = No_Gen then
            This.Engine := (Kind => No_Gen);
        else
            This.Engine.Frs_World.Ptr.Possibles.Clear;
        end if;
    end Roll_Fresh_Gen;


    procedure Roll_Unify_Gen
           (This : in out Mu_World)
    is
        Extended : State;
    begin
        This.Engine.Uni_World.Ptr.Rollover;
        for Potential of This.Engine.Uni_World.Ptr.Possibles loop
            if Do_Unify (Potential, This.Engine.Uni_Term1, This.Engine.Uni_Term2, Extended) then
                This.Possibles.Append (Extended);
            end if;
        end loop;
        if This.Engine.Uni_World.Ptr.Engine.Kind = No_Gen then
            This.Engine := (Kind => No_Gen);
        else
            This.Engine.Uni_World.Ptr.Possibles.Clear;
        end if;
    end Roll_Unify_Gen;


    procedure Roll_Buffer_Gen
           (This : in out Mu_World) is
    begin
        This.Engine.Buff_World.Ptr.Rollover;
        This.Possibles.Append (This.Engine.Buff_World.Ptr.Possibles);
        if This.Engine.Buff_World.Ptr.Engine.Kind = No_Gen then
            This.Engine := (Kind => No_Gen);
        else
            This.Engine.Buff_World.Ptr.Possibles.Clear;
        end if;
    end Roll_Buffer_Gen;


    procedure Roll_Disjunct_Gen
           (This : in out Mu_World) is
    begin
        This.Engine.Dis_World1.Ptr.Rollover;
        This.Possibles.Append (This.Engine.Dis_World1.Ptr.Possibles);
        if This.Engine.Dis_World1.Ptr.Engine.Kind = No_Gen then
            This.Engine := (Kind => Buffer_Gen, Buff_World => This.Engine.Dis_World2);
        else
            This.Engine.Dis_World1.Ptr.Possibles.Clear;
            Swap (This.Engine.Dis_World1, This.Engine.Dis_World2);
        end if;
    end Roll_Disjunct_Gen;


    procedure Roll_Recurse_Gen
           (This : in out Mu_World) is
    begin
        This.Engine.Rec_World.Ptr.Rollover;
        if This.Engine.Rec_World.Ptr.Possibles.Last_Index < This.Engine.Rec_Index then
            if This.Engine.Rec_World.Ptr.Engine.Kind = No_Gen then
                if This.Engine.Rec_Index = 1 then
                    This.Engine := (Kind => No_Gen);
                else
                    This.Engine.Rec_Index := 1;
                end if;
            end if;
            return;
        end if;
        for Index in Integer range
            This.Engine.Rec_Index .. This.Engine.Rec_World.Ptr.Possibles.Last_Index
        loop
            This.Possibles.Append (This.Engine.Rec_World.Ptr.Possibles (Index));
        end loop;
        This.Engine.Rec_Index := This.Engine.Rec_World.Ptr.Possibles.Last_Index + 1;
    end Roll_Recurse_Gen;


    procedure Rollover
           (This : in out Mu_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 Buffer_Gen   => This.Roll_Buffer_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 Mu_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 Mu_World'Class)
        return Term is
    begin
        return This.Fresh (+"");
    end Fresh;


    function Fresh
           (This : in out Mu_World'Class;
            Name : in     String)
        return Term is
    begin
        return This.Fresh (+Name);
    end Fresh;


    function Fresh
           (This : in out Mu_World'Class;
            Name : in     Ada.Strings.Unbounded.Unbounded_String)
        return Term is
    begin
        return My_Term : constant Term := T (Variable'(Ident => This.Next_Ident, Name => Name)) do
            This.Engine :=
               (Kind      => Fresh_Gen,
                Frs_World => Hold (This),
                Frs_Name  => Name);
            This.Next_Ident := This.Next_Ident + 1;
            This.Possibles := State_Vectors.Empty_Vector;
        end return;
    end Fresh;




    --  Unify  --

    function Unify
           (This  : in Mu_World;
            Left  : in Term'Class;
            Right : in Element_Type)
        return Mu_World is
    begin
        return This.Unify (Left, T (Right));
    end Unify;


    procedure Unify
           (This  : in out Mu_World;
            Left  : in     Term'Class;
            Right : in     Element_Type) is
    begin
        This := This.Unify (Left, T (Right));
    end Unify;


    function Unify
           (This        : in Mu_World;
            Left, Right : in Term'Class)
        return Mu_World is
    begin
        return Result : constant Mu_World :=
           (Possibles  => State_Vectors.Empty_Vector,
            Next_Ident => This.Next_Ident,
            Engine     =>
               (Kind      => Unify_Gen,
                Uni_World => Hold (This),
                Uni_Term1 => Term (Left),
                Uni_Term2 => Term (Right)));
    end Unify;


    procedure Unify
           (This        : in out Mu_World;
            Left, Right : in     Term'Class) is
    begin
        This := This.Unify (Left, Right);
    end Unify;




    --  Disjunct  --

    function Disjunct
           (Left, Right : in Mu_World)
        return Mu_World is
    begin
        return Result : constant Mu_World :=
           (Possibles  => State_Vectors.Empty_Vector,
            Next_Ident => ID_Number'Max (Left.Next_Ident, Right.Next_Ident),
            Engine     =>
               (Kind       => Disjunct_Gen,
                Dis_World1 => Hold (Left),
                Dis_World2 => Hold (Right)));
    end Disjunct;


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


    function Disjunct
           (Inputs : in Mu_World_Array)
        return Mu_World is
    begin
        if Inputs'Length = 0 then
            return Failed : constant Mu_World :=
               (Possibles  => State_Vectors.Empty_Vector,
                Next_Ident => 0,
                Engine     => (Kind => No_Gen));
        elsif Inputs'Length = 1 then
            return Inputs (Inputs'First);
        else
            return Result : Mu_World :=
               (Possibles  => State_Vectors.Empty_Vector,
                Next_Ident => 0,  --  dummy
                Engine     =>
                   (Kind       => Disjunct_Gen,
                    Dis_World1 => Hold (Inputs (Inputs'First)),
                    Dis_World2 => Hold (Disjunct (Inputs (Inputs'First + 1 .. Inputs'Last)))))
            do
                Result.Next_Ident := ID_Number'Max
                   (Result.Engine.Dis_World1.Ptr.Next_Ident,
                    Result.Engine.Dis_World2.Ptr.Next_Ident);
            end return;
        end if;
    end Disjunct;


    procedure Disjunct
           (This   : in out Mu_World;
            Inputs : in     Mu_World_Array) is
    begin
        This := Disjunct (This & Inputs);
    end Disjunct;




    --  Recurse  --

    function Recurse
           (This : in Mu_World)
        return Mu_World is
    begin
        return Result : constant Mu_World :=
           (Possibles  => State_Vectors.Empty_Vector,
            Next_Ident => This.Next_Ident,
            Engine     =>
               (Kind      => Recurse_Gen,
                Rec_World => Hold (This),
                Rec_Index => 1));
    end Recurse;


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




    --  Forced Evaluation  --

    function Take
           (This  : in Mu_World;
            Count : in Natural)
        return Mu_World is
    begin
        if Count = 0 then
            return
               (Possibles  => State_Vectors.Empty_Vector,
                Next_Ident => ID_Number'First,
                Engine     => (Kind => No_Gen));
        end if;
        return Result : Mu_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 Mu_World;
            Count : in     Natural) is
    begin
        This := This.Take (Count);
    end Take;


    procedure Force
           (This  : in out Mu_World;
            Count : in     Positive) is
    begin
        This.Roll_Until (Count);
    end Force;


    procedure Force_All
           (This : in out Mu_World) is
    begin
        while This.Engine.Kind /= No_Gen loop
            This.Rollover;
        end loop;
    end Force_All;


    function Failed
           (This : in out Mu_World)
        return Boolean is
    begin
        return not This.Has_State (1);
    end Failed;


end Kompsos;