--  Programmed by Jedidiah Barber
--  Licensed under the Sunset License v1.0

--  See license.txt for further details


package body Kompsos is


    -----------------
    --  Datatypes  --
    -----------------

    --  Terms  --

    function Kind
           (This : in Term)
        return Term_Kind is
    begin
        return Term_Component (This.Actual.Constant_Reference.Element.all).Kind;
    end Kind;


    function T
           (Item : in Element_Type)
        return Term is
    begin
        return (Actual => Term_Holders.To_Holder (Term_Component'(
            Kind  => Atom_Term,
            Value => Item)));
    end T;


    function T
           (Item : in Variable)
        return Term is
    begin
        return (Actual => Term_Holders.To_Holder (Term_Component'(
            Kind  => Var_Term,
            Refer => Item)));
    end T;


    function T
           (Item1, Item2 : in Term'Class)
        return Term is
    begin
        return (Actual => Term_Holders.To_Holder (Term_Component'(
            Kind  => Pair_Term,
            Left  => Term (Item1),
            Right => Term (Item2))));
    end T;


    function T
           (Items : in Term_Array)
        return Term is
    begin
        if Items'Length = 0 then
            return Empty_Term;
        else
            return T (Items (Items'First), T (Items (Items'First + 1 .. Items'Last)));
        end if;
    end T;


    function Atom
           (This : in Term)
        return Element_Type is
    begin
        return Term_Component (This.Actual.Constant_Reference.Element.all).Value;
    end Atom;


    function Var
           (This : in Term'Class)
        return Variable is
    begin
        return Term_Component (This.Actual.Constant_Reference.Element.all).Refer;
    end Var;


    function Name
           (This : in Term)
        return SU.Unbounded_String is
    begin
        return This.Var.Name;
    end Name;


    function Left
           (This : in Term)
        return Term is
    begin
        return Term_Component (This.Actual.Constant_Reference.Element.all).Left;
    end Left;


    function Right
           (This : in Term)
        return Term is
    begin
        return Term_Component (This.Actual.Constant_Reference.Element.all).Right;
    end Right;



    --  Worlds  --

    function Hold
           (This : in World)
        return World_Holders.Holder is
    begin
        return World_Holders.To_Holder (World_Root'Class (This));
    end Hold;


    function Ptr
           (This : in out World_Holders.Holder)
        return World_Access is
    begin
        return World (This.Reference.Element.all)'Unchecked_Access;
    end Ptr;


    procedure Swap
           (Left, Right : in out World_Holders.Holder)
    is
        Temp : World_Holders.Holder;
    begin
        Temp.Move (Left);
        Left.Move (Right);
        Right.Move (Temp);
    end Swap;




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

    --  Variable IDs  --

    Next_Generator_ID : Generator_ID_Number := Generator_ID_Number'First;

    function Next_Gen
        return Generator_ID_Number is
    begin
        return Result : constant Generator_ID_Number := Next_Generator_ID do
            Next_Generator_ID := Next_Generator_ID + 1;
        end return;
    end Next_Gen;



    --  Unification  --

    function Fully_Contains
           (This : in State;
            Item : in Term'Class)
        return Boolean is
    begin
        case Item.Kind is
        when Null_Term | Atom_Term =>
            return True;
        when Var_Term =>
            return This.Ident.Contains (Item.Var.Ident);
        when Pair_Term =>
            return Fully_Contains (This, Item.Left) and then Fully_Contains (This, Item.Right);
        end case;
    end Fully_Contains;


    function Walk
           (This : in State;
            Item : in Term'Class)
        return Term'Class is
    begin
        if  Item.Kind = Var_Term and then
            This.Subst.Contains (This.Ident.Element (Item.Var.Ident))
        then
            return Walk (This, This.Subst.Constant_Reference (This.Ident.Element (Item.Var.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
        --  Check for Variable validity with respect to State
        if  not Fully_Contains (Potential, Real_Left) or
            not Fully_Contains (Potential, Real_Right)
        then
            return False;
        end if;

        --  Resolve Variable substitution
        if Left.Kind = Var_Term then
            Real_Left := Walk (Potential, Real_Left);
        end if;
        if Right.Kind = Var_Term then
            Real_Right := Walk (Potential, Real_Right);
        end if;

        --  Unify equal Variable/Atom/Null Terms
        if (Real_Left.Kind = Var_Term and then
            Real_Right.Kind = Var_Term and then
            Real_Left = Real_Right) or else
           (Real_Left.Kind = Atom_Term and then
            Real_Right.Kind = Atom_Term and then
            Real_Left = Real_Right) or else
           (Real_Left.Kind = Null_Term and Real_Right.Kind = Null_Term)
        then
            Extended := Potential;
            return True;
        end if;

        --  Unify Variable and other Terms by introducing a new substitution
        if Real_Left.Kind = Var_Term then
            Extended := Potential;
            Extended.Subst.Insert (Extended.Ident.Element (Real_Left.Var.Ident), Term (Real_Right));
            return True;
        end if;
        if Real_Right.Kind = Var_Term then
            Extended := Potential;
            Extended.Subst.Insert (Extended.Ident.Element (Real_Right.Var.Ident), Term (Real_Left));
            return True;
        end if;

        --  Unify Pair Terms by unifying each corresponding part
        if Real_Left.Kind = Pair_Term and then Real_Right.Kind = Pair_Term then
            declare
                Middle : State;
            begin
                return Do_Unify (Potential, Real_Left.Left, Real_Right.Left, Middle) and then
                    Do_Unify (Middle, Real_Left.Right, Real_Right.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 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
        Ptr (This.Engine.Frs_World).Rollover;
        for Potential of Ptr (This.Engine.Frs_World).Possibles loop
            Potential.LVars.Append (This.Engine.Frs_Name);
            Potential.Ident.Insert (This.Engine.Frs_Ident, Potential.LVars.Last_Index);
            This.Possibles.Append (Potential);
        end loop;
        if Ptr (This.Engine.Frs_World).Engine.Kind = No_Gen then
            This.Engine := (Kind => No_Gen);
        else
            Ptr (This.Engine.Frs_World).Possibles.Clear;
        end if;
    end Roll_Fresh_Gen;


    procedure Roll_Unify_Gen
           (This : in out World)
    is
        Extended : State;
    begin
        Ptr (This.Engine.Uni_World).Rollover;
        for Potential of Ptr (This.Engine.Uni_World).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 Ptr (This.Engine.Uni_World).Engine.Kind = No_Gen then
            This.Engine := (Kind => No_Gen);
        else
            Ptr (This.Engine.Uni_World).Possibles.Clear;
        end if;
    end Roll_Unify_Gen;


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


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


    procedure Roll_Conjunct_Zero_Gen
           (This : in out World)
    is
        use type Ada.Containers.Count_Type;
    begin
        Ptr (This.Engine.ConZ_World).Rollover;
        if Ptr (This.Engine.ConZ_World).Possibles.Length > 0 then
            declare
                Next : constant World := This.Engine.ConZ_Func (Ptr (This.Engine.ConZ_World).all);
            begin
                This := Next;
            end;
        elsif Ptr (This.Engine.ConZ_World).Engine.Kind = No_Gen then
            This.Engine := (Kind => No_Gen);
        end if;
    end Roll_Conjunct_Zero_Gen;


    procedure Roll_Conjunct_One_Gen
           (This : in out World)
    is
        use type Ada.Containers.Count_Type;
    begin
        Ptr (This.Engine.ConO_World).Rollover;
        if Ptr (This.Engine.ConO_World).Possibles.Length > 0 then
            declare
                Next : constant World := This.Engine.ConO_Func
                   (Ptr (This.Engine.ConO_World).all,
                    This.Engine.ConO_Input);
            begin
                This := Next;
            end;
        elsif Ptr (This.Engine.ConO_World).Engine.Kind = No_Gen then
            This.Engine := (Kind => No_Gen);
        end if;
    end Roll_Conjunct_One_Gen;


    procedure Roll_Conjunct_Many_Gen
           (This : in out World)
    is
        use type Ada.Containers.Count_Type;
    begin
        Ptr (This.Engine.ConM_World).Rollover;
        if Ptr (This.Engine.ConM_World).Possibles.Length > 0 then
            declare
                Next : constant World := This.Engine.ConM_Func
                   (Ptr (This.Engine.ConM_World).all,
                    This.Engine.ConM_Inputs.Constant_Reference);
            begin
                This := Next;
            end;
        elsif Ptr (This.Engine.ConM_World).Engine.Kind = No_Gen then
            This.Engine := (Kind => No_Gen);
        end if;
    end Roll_Conjunct_Many_Gen;


    procedure Roll_Recurse_Gen
           (This : in out World) is
    begin
        Ptr (This.Engine.Rec_World).Rollover;
        if Ptr (This.Engine.Rec_World).Possibles.Last_Index < This.Engine.Rec_Index then
            if Ptr (This.Engine.Rec_World).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 .. Ptr (This.Engine.Rec_World).Possibles.Last_Index
        loop
            This.Possibles.Append (Ptr (This.Engine.Rec_World).Possibles (Index));
        end loop;
        This.Engine.Rec_Index := Ptr (This.Engine.Rec_World).Possibles.Last_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 Buffer_Gen        => This.Roll_Buffer_Gen;
        when Disjunct_Gen      => This.Roll_Disjunct_Gen;
        when Conjunct_Zero_Gen => This.Roll_Conjunct_Zero_Gen;
        when Conjunct_One_Gen  => This.Roll_Conjunct_One_Gen;
        when Conjunct_Many_Gen => This.Roll_Conjunct_Many_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;




    -------------------
    --  microKanren  --
    -------------------

    --  Variable Introduction  --

    function Fresh
           (This : in out World'Class)
        return Term is
    begin
        return This.Fresh (+"");
    end Fresh;


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


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



    --  Unification  --

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


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


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


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



    --  Combining / Disjunction  --

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


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


    function Disjunct
           (Inputs : in World_Array)
        return World is
    begin
        if Inputs'Length = 0 then
            return Failed : constant World :=
               (Possibles => State_Vectors.Empty_Vector,
                Engine    => (Kind => No_Gen));
        elsif Inputs'Length = 1 then
            return Inputs (Inputs'First);
        else
            return Result : constant World :=
               (Possibles => State_Vectors.Empty_Vector,
                Engine    =>
                   (Kind       => Disjunct_Gen,
                    Dis_World1 => Hold (Inputs (Inputs'First)),
                    Dis_World2 => Hold (Disjunct (Inputs (Inputs'First + 1 .. Inputs'Last)))));
        end if;
    end Disjunct;


    procedure Disjunct
           (This   : in out World;
            Inputs : in     World_Array) is
    begin
        This := Disjunct (This & Inputs);
    end Disjunct;



    --  Lazy Sequencing / Conjunction  --

    function Conjunct
           (This : in World;
            Func : in Conjunct_Zero_Func)
        return World is
    begin
        return Result : constant World :=
           (Possibles => State_Vectors.Empty_Vector,
            Engine    =>
               (Kind       => Conjunct_Zero_Gen,
                ConZ_World => Hold (This),
                ConZ_Func  => Func));
    end Conjunct;


    procedure Conjunct
           (This : in out World;
            Func : in     Conjunct_Zero_Func) is
    begin
        This := This.Conjunct (Func);
    end Conjunct;


    function Conjunct
           (This  : in World;
            Func  : in Conjunct_One_Func;
            Input : in Term'Class)
        return World is
    begin
        return Result : constant World :=
           (Possibles => State_Vectors.Empty_Vector,
            Engine    =>
               (Kind       => Conjunct_One_Gen,
                ConO_World => Hold (This),
                ConO_Func  => Func,
                ConO_Input => Term (Input)));
    end Conjunct;


    procedure Conjunct
           (This  : in out World;
            Func  : in     Conjunct_One_Func;
            Input : in     Term'Class) is
    begin
        This := This.Conjunct (Func, Input);
    end Conjunct;


    function Conjunct
           (This   : in World;
            Func   : in Conjunct_Many_Func;
            Inputs : in Term_Array)
        return World is
    begin
        return Result : constant World :=
           (Possibles => State_Vectors.Empty_Vector,
            Engine    =>
               (Kind        => Conjunct_Many_Gen,
                ConM_World  => Hold (This),
                ConM_Func   => Func,
                ConM_Inputs => Term_Array_Holders.To_Holder (Inputs)));
    end Conjunct;


    procedure Conjunct
           (This   : in out World;
            Func   : in     Conjunct_Many_Func;
            Inputs : in     Term_Array) is
    begin
        This := This.Conjunct (Func, Inputs);
    end Conjunct;




    -------------------------
    --  Auxiliary Helpers  --
    -------------------------

    --  Infinite State Loops  --

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


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



    --  Forced Evaluation  --

    function Take
           (This  : in World;
            Count : in Natural)
        return World is
    begin
        if Count = 0 then
            return
               (Possibles => State_Vectors.Empty_Vector,
                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;


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


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


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




    --------------------------
    --  miniKanren Prelude  --
    --------------------------

    --  caro  --

    function Head
           (This   : in World;
            Inputs : in Term_Array)
        return World
    is
        List_Term : Term renames Inputs (1);
        Head_Term : Term renames Inputs (2);
    begin
        return Result : World := This do
            Result.Unify (T (Head_Term, Result.Fresh), List_Term);
        end return;
    end Head;


    procedure Head
           (This   : in out World;
            Inputs : in     Term_Array) is
    begin
        This := This.Head (Inputs);
    end Head;



    --  cdro  --

    function Tail
           (This   : in World;
            Inputs : in Term_Array)
        return World
    is
        List_Term : Term renames Inputs (1);
        Tail_Term : Term renames Inputs (2);
    begin
        return Result : World := This do
            Result.Unify (T (Result.Fresh, Tail_Term), List_Term);
        end return;
    end Tail;


    procedure Tail
           (This   : in out World;
            Inputs : in     Term_Array) is
    begin
        This := This.Tail (Inputs);
    end Tail;



    --  conso  --

    function Cons
           (This   : in World;
            Inputs : in Term_Array)
        return World
    is
        Head_Term : Term renames Inputs (1);
        Tail_Term : Term renames Inputs (2);
        List_Term : Term renames Inputs (3);
    begin
        return Result : World := This do
            Result.Unify (T (Head_Term, Tail_Term), List_Term);
        end return;
    end Cons;


    procedure Cons
           (This   : in out World;
            Inputs : in     Term_Array) is
    begin
        This := This.Cons (Inputs);
    end Cons;



    --  nullo  --

    function Nil
           (This     : in World;
            Nil_Term : in Term'Class)
        return World is
    begin
        return Result : World := This do
            Result.Unify (Empty_Term, Nil_Term);
        end return;
    end Nil;


    procedure Nil
           (This     : in out World;
            Nil_Term : in     Term'Class) is
    begin
        This := This.Nil (Nil_Term);
    end Nil;



    --  pairo  --

    function Pair
           (This      : in World;
            Pair_Term : in Term'Class)
        return World is
    begin
        return Result : World := This do
            Result.Cons (Result.Fresh & Result.Fresh & Term (Pair_Term));
        end return;
    end Pair;


    procedure Pair
           (This      : in out World;
            Pair_Term : in     Term'Class) is
    begin
        This := This.Pair (Pair_Term);
    end Pair;



    --  listo  --

    function Linked_List
           (This      : in World;
            List_Term : in Term'Class)
        return World
    is
        One, Two : World := This;
        Ref_Term : constant Term := Two.Fresh;
    begin
        One.Nil (List_Term);

        Two.Pair (List_Term);
        Two.Tail (Term (List_Term) & Ref_Term);
        Two.Conjunct (Linked_List'Access, Ref_Term);

        return Disjunct (One, Two);
    end Linked_List;


    procedure Linked_List
           (This      : in out World;
            List_Term : in     Term'Class) is
    begin
        This := This.Linked_List (List_Term);
    end Linked_List;



    --  membero  --

    function Member
           (This   : in World;
            Inputs : in Term_Array)
        return World
    is
        Item_Term : Term renames Inputs (1);
        List_Term : Term renames Inputs (2);

        One, Two : World := This;
        Ref_Term : constant Term := Two.Fresh;
    begin
        One.Head (List_Term & Item_Term);

        Two.Tail (List_Term & Ref_Term);
        Two.Conjunct (Member'Access, Item_Term & Ref_Term);

        return Disjunct (One, Two);
    end Member;


    procedure Member
           (This   : in out World;
            Inputs : in     Term_Array) is
    begin
        This := This.Member (Inputs);
    end Member;



    --  rembero  --

    function Remove
           (This   : in World;
            Inputs : in Term_Array)
        return World
    is
        Item_Term : Term renames Inputs (1);
        List_Term : Term renames Inputs (2);
        Out_Term  : Term renames Inputs (3);

        One, Two : World := This;
        Left  : constant Term := Two.Fresh;
        Right : constant Term := Two.Fresh;
        Rest  : constant Term := Two.Fresh;
    begin
        One.Head (List_Term & Item_Term);
        One.Tail (List_Term & Out_Term);

        Two.Cons (Left & Right & List_Term);
        Two.Conjunct (Remove'Access, Item_Term & Right & Rest);
        Two.Cons (Left & Rest & Out_Term);

        return Disjunct (One, Two);
    end Remove;


    procedure Remove
           (This   : in out World;
            Inputs : in     Term_Array) is
    begin
        This := This.Remove (Inputs);
    end Remove;



    --  appendo  --

    function Append
           (This   : in World;
            Inputs : in Term_Array)
        return World
    is
        List_Term : Term renames Inputs (1);
        Item_Term : Term renames Inputs (2);
        Out_Term  : Term renames Inputs (3);

        One, Two : World := This;
        Left  : constant Term := Two.Fresh;
        Right : constant Term := Two.Fresh;
        Rest  : constant Term := Two.Fresh;
    begin
        One.Nil (List_Term);
        One.Unify (Item_Term, Out_Term);

        Two.Cons (Left & Right & List_Term);
        Two.Cons (Left & Rest & Out_Term);
        Two.Conjunct (Append'Access, Right & Item_Term & Rest);

        return Disjunct (One, Two);
    end Append;


    procedure Append
           (This   : in out World;
            Inputs : in     Term_Array) is
    begin
        This := This.Append (Inputs);
    end Append;


end Kompsos;