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

--  See license.txt for further details


with

    Ada.Unchecked_Deallocation,
    Kompsos.Collector,
    System.Address_To_Access_Conversions,
    System.Storage_Elements;


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
        This.Actual := null;
    end Initialize;


    procedure Adjust
           (This : in out Term) is
    begin
        if This.Kind /= Null_Term then
            This.Actual.Counter := This.Actual.Counter + 1;
        end if;
    end Adjust;


    procedure Finalize
           (This : in out Term) is
    begin
        if This.Kind /= Null_Term then
            This.Actual.Counter := This.Actual.Counter - 1;
            if This.Actual.Counter = 0 then
                Free (This.Actual);
            end if;
        end if;
    end Finalize;



    --  Goal Graphs  --

    procedure Free is new Ada.Unchecked_Deallocation (Graph_Component, Graph_Component_Access);


    procedure Initialize
           (This : in out Goal_Graph) is
    begin
        This.Actual := null;
    end Initialize;


    procedure Adjust
           (This : in out Goal_Graph) is
    begin
        if This.Actual /= null then
            This.Actual.Counter := This.Actual.Counter + 1;
        end if;
    end Adjust;


    procedure Finalize
           (This : in out Goal_Graph) is
    begin
        if This.Actual /= null then
            This.Actual.Counter := This.Actual.Counter - 1;
            if This.Actual.Counter = 0 then
                Free (This.Actual);
            end if;
        end if;
    end Finalize;




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

    --  Terms  --

    function "="
           (Left, Right : in Term)
        return Boolean is
    begin
        if Left.Actual = Right.Actual then
            return True;
        elsif Left.Kind = Right.Kind then
            case Left.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;
            when Null_Term =>
                --  Should never actually get here because Null_Terms
                --  are covered by checking Left.Actual = Right.Actual
                return True;
            end case;
        else
            return False;
        end if;
    end "=";


    function Kind
           (This : in Term)
        return Term_Kind is
    begin
        return (if This.Actual = null then Null_Term else This.Actual.Kind);
    end Kind;


    function T
           (Item : in Element_Type)
        return Term is
    begin
        return (Ada.Finalization.Controlled with Actual => new Term_Component'(
            Kind    => Atom_Term,
            Counter => 1,
            Value   => Item));
    end T;


    function T
           (Item : in Variable)
        return Term'Class is
    begin
        return Term'(Ada.Finalization.Controlled with Actual => new Term_Component'(
            Kind    => Var_Term,
            Counter => 1,
            Refer   => Item));
    end T;


    function T
           (Item1, Item2 : in Term'Class)
        return Term is
    begin
        return (Ada.Finalization.Controlled with Actual => new Term_Component'(
            Kind    => Pair_Term,
            Counter => 1,
            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 This.Actual.Value;
    end Atom;


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


    function Left
           (This : in Term)
        return Term is
    begin
        return This.Actual.Left;
    end Left;


    function Right
           (This : in Term)
        return Term is
    begin
        return This.Actual.Right;
    end Right;



    --  States  --

    function Lookup
           (This  : in     State;
            Key   : in     Variable;
            Value :    out Term'Class)
        return Boolean is
    begin
        for Bind of This.Actual loop
            if Bind.Key = Key then
                Value := Term'Class (Bind.Elem);
                return True;
            end if;
        end loop;
        return False;
    end Lookup;



    --  Goal Graphs  --

    package Graph_Convert is new System.Address_To_Access_Conversions (Graph_Component);

    function "<"
           (Left, Right : in Graph_Component_Access)
        return Boolean
    is
        use System.Storage_Elements;
    begin
        return
            To_Integer (Graph_Convert.To_Address (Graph_Convert.Object_Pointer (Left))) <
            To_Integer (Graph_Convert.To_Address (Graph_Convert.Object_Pointer (Right)));
    end "<";




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

    --  Variable Introduction  --

    function Fresh
           (This : in out Goal'Class)
        return Term is
    begin
        return Result : constant Term := Term (T (This.Next_Var)) do
            This.Next_Var := This.Next_Var + 1;
        end return;
    end Fresh;


    function Fresh
           (This  : in out Goal'Class;
            Count : in     Positive)
        return Term_Array is
    begin
        return My_Terms : Term_Array (1 .. Count) do
            for Item of My_Terms loop
                Item := This.Fresh;
            end loop;
        end return;
    end Fresh;


    function Make_Fresh
        return Term is
    begin
        return Verse.Fresh;
    end Make_Fresh;



    --  Unification  --

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


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


    function Unify
           (This        : in Goal;
            Left, Right : in Term'Class)
        return Goal is
    begin
        return Result : constant Goal :=
           (Graph    => (Ada.Finalization.Controlled with
                Actual => new Graph_Component'(
                   (Kind      => Unify_Node,
                    Counter   => 1,
                    Uni_Goal  => This.Graph,
                    Uni_Term1 => Term (Left),
                    Uni_Term2 => Term (Right)))),
            Next_Var => This.Next_Var);
    end Unify;


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



    --  Combining / Disjunction  --

    function Disjunct
           (Left, Right : in Goal)
        return Goal is
    begin
        return Result : constant Goal :=
           (Graph    => (Ada.Finalization.Controlled with
                Actual => new Graph_Component'(
                   (Kind      => Disjunct_Node,
                    Counter   => 1,
                    Dis_Goal1 => Left.Graph,
                    Dis_Goal2 => Right.Graph))),
            Next_Var => Variable'Max (Left.Next_Var, Right.Next_Var));
    end Disjunct;


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


    function Disjunct
           (Inputs : in Goal_Array)
        return Goal is
    begin
        if Inputs'Length = 0 then
            return Empty_Goal;
        elsif Inputs'Length = 1 then
            return Inputs (Inputs'First);
        else
            declare
                Rest : constant Goal := Disjunct (Inputs (Inputs'First + 1 .. Inputs'Last));
            begin
                return Result : constant Goal :=
                   (Graph    => (Ada.Finalization.Controlled with
                        Actual => new Graph_Component'(
                           (Kind      => Disjunct_Node,
                            Counter   => 1,
                            Dis_Goal1 => Inputs (Inputs'First).Graph,
                            Dis_Goal2 => Rest.Graph))),
                    Next_Var => Variable'Max (Inputs (Inputs'First).Next_Var, Rest.Next_Var));
            end;
        end if;
    end Disjunct;


    procedure Disjunct
           (This   : in out Goal;
            Inputs : in     Goal_Array) is
    begin
        This := Disjunct (This & Inputs);
    end Disjunct;



    --  Lazy Sequencing / Conjunction  --

    function Conjunct
           (This : in Goal;
            Func : in Junction_Zero_Func)
        return Goal is
    begin
        return Result : constant Goal :=
           (Graph    => (Ada.Finalization.Controlled with
                Actual => new Graph_Component'(
                   (Kind     => Conjunct_Node,
                    Counter  => 1,
                    Con_Goal => This.Graph,
                    Con_Data => Lazy_Holders.To_Holder ((Kind => Zero_Arg, ZFunc => Func))))),
            Next_Var => This.Next_Var);
    end Conjunct;


    procedure Conjunct
           (This : in out Goal;
            Func : in     Junction_Zero_Func) is
    begin
        This := This.Conjunct (Func);
    end Conjunct;


    function Conjunct
           (This  : in Goal;
            Func  : in Junction_One_Func;
            Input : in Term'Class)
        return Goal is
    begin
        return Result : constant Goal :=
           (Graph    => (Ada.Finalization.Controlled with
                Actual => new Graph_Component'(
                   (Kind     => Conjunct_Node,
                    Counter  => 1,
                    Con_Goal => This.Graph,
                    Con_Data => Lazy_Holders.To_Holder
                       ((Kind   => One_Arg,
                         OFunc  => Func,
                         OInput => Term (Input)))))),
            Next_Var => This.Next_Var);
    end Conjunct;


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


    function Conjunct
           (This   : in Goal;
            Func   : in Junction_Many_Func;
            Inputs : in Term_Array)
        return Goal is
    begin
        return Result : constant Goal :=
           (Graph    => (Ada.Finalization.Controlled with
                Actual => new Graph_Component'(
                   (Kind     => Conjunct_Node,
                    Counter  => 1,
                    Con_Goal => This.Graph,
                    Con_Data => Lazy_Holders.To_Holder
                       ((Kind   => Many_Arg,
                         MFunc  => Func,
                         MInput => Term_Array_Holders.To_Holder (Inputs)))))),
            Next_Var => This.Next_Var);
    end Conjunct;


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




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

    --  Infinite State Loops  --

    function Recurse
           (This : in Goal)
        return Goal is
    begin
        return Result : constant Goal :=
           (Graph    => (Ada.Finalization.Controlled with
                Actual => new Graph_Component'(
                   (Kind     => Recurse_Node,
                    Counter  => 1,
                    Rec_Goal => This.Graph))),
            Next_Var => This.Next_Var);
    end Recurse;


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



    --  Evaluation  --

    function Run
           (This  : in Goal;
            Count : in Positive;
            Base  : in State := Empty_State)
        return State_Array
    is
        Result : State_Array (1 .. Count);
        Valid  : Natural := 0;

        package Collect is new Collector (This, Base);
    begin
        for Item of Result loop
            exit when not Collect.Has_Next;
            Item := Collect.Next;
            Valid := Valid + 1;
        end loop;
        return Result (1 .. Valid);
    end Run;


    function Run
           (This : in Goal;
            Base : in State := Empty_State)
        return State
    is
        package Collect is new Collector (This, Base);
    begin
        return Collect.Next (Empty_State);
    end Run;


    function Run_All
           (This : in Goal;
            Base : in State := Empty_State)
        return State_Array
    is
        package Collect is new Collector (This, Base);

        function Do_Run
            return State_Array is
        begin
            if Collect.Has_Next then
                return Collect.Next & Do_Run;
            else
                return Result : State_Array (1 .. 0);
            end if;
        end Do_Run;
    begin
        return Do_Run;
    end Run_All;



    --  Reification  --

    function Resolve
           (This  : in Term;
            Subst : in State)
        return Term is
    begin
        case This.Kind is
        when Null_Term | Atom_Term =>
            return This;
        when Var_Term =>
            declare
                Bound_Term : Term;
            begin
                if Lookup (Subst, This.Var, Bound_Term) then
                    return Bound_Term.Resolve (Subst);
                else
                    return This;
                end if;
            end;
        when Pair_Term =>
            return T (This.Left.Resolve (Subst), This.Right.Resolve (Subst));
        end case;
    end Resolve;


    function Resolve_First
           (Subst : in State)
        return Term is
    begin
        if Subst.Actual.Is_Empty then
            return Empty_Term;
        else
            declare
                Min_Pos : Long_Positive := Subst.Actual.First_Index;
                Min_Var : Variable      := Subst.Actual.First_Element.Key;
            begin
                for Index in Subst.Actual.First_Index + 1 .. Subst.Actual.Last_Index loop
                    if Subst.Actual (Index).Key < Min_Var then
                        Min_Pos := Index;
                        Min_Var := Subst.Actual (Index).Key;
                    end if;
                end loop;
                return Subst.Actual (Min_Pos).Elem.Resolve (Subst);
            end;
        end if;
    end Resolve_First;




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

    --  caro  --

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


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



    --  cdro  --

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


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



    --  conso  --

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


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



    --  nullo  --

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


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



    --  pairo  --

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


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



    --  listo  --

    function Linked_List
           (This      : in Goal;
            List_Term : in Term'Class)
        return Goal
    is
        One, Two : Goal := 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 Goal;
            List_Term : in     Term'Class) is
    begin
        This := This.Linked_List (List_Term);
    end Linked_List;



    --  membero  --

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

        One, Two : Goal := 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 Goal;
            Inputs : in     Term_Array) is
    begin
        This := This.Member (Inputs);
    end Member;



    --  rembero  --

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

        One, Two : Goal := 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 Goal;
            Inputs : in     Term_Array) is
    begin
        This := This.Remove (Inputs);
    end Remove;



    --  appendo  --

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

        One, Two : Goal := 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 Goal;
            Inputs : in     Term_Array) is
    begin
        This := This.Append (Inputs);
    end Append;


end Kompsos;