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

--  See license.txt for further details


with

    Ada.Unchecked_Deallocation,
    Kompsos.Collector;


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;



    --  Worlds  --

    procedure Free is new Ada.Unchecked_Deallocation (World_Component, World_Component_Access);


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


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


    procedure Finalize
           (This : in out World) 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 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 Name
           (This : in Term)
        return Nametag is
    begin
        return This.Var.Name;
    end Name;


    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;



    --  Worlds  --

    function Static
           (Item : in State)
        return World'Class
    is
        use type State_Vectors.Vector;
    begin
        return Result : constant World := (Ada.Finalization.Controlled with
            Actual => new World_Component'(
               (Kind       => Static_Node,
                Counter    => 1,
                Stc_States => State_Vectors.Empty_Vector & Item)));
    end Static;




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




    -------------------
    --  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     Nametag)
        return Term
    is
        My_ID  : constant Generator_ID_Number := Next_Gen;
        My_Var : constant Variable := (Ident => My_ID, Name => Name);
    begin
        return My_Term : constant Term := Term (T (My_Var)) do
            This.Actual := new World_Component'(
               (Kind      => Fresh_Node,
                Counter   => 1,
                Frs_World => World (This),
                Frs_Var   => My_Var));
        end return;
    end Fresh;


    function Fresh
           (This  : in out World'Class;
            Count : in     Positive)
        return Term_Array
    is
        Names : constant Nametag_Array (1 .. Count) := (others => +"");
    begin
        return This.Fresh (Names);
    end Fresh;


    function Fresh
           (This  : in out World'Class;
            Names : in     Nametag_Array)
        return Term_Array is
    begin
        return Terms : Term_Array (1 .. Names'Length) do
            for Index in Terms'Range loop
                Terms (Index) := This.Fresh (Names (Names'First + Index - 1));
            end loop;
        end return;
    end Fresh;


    function Make_Fresh
        return Term is
    begin
        return Verse.Fresh;
    end Make_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 := (Ada.Finalization.Controlled with
            Actual => new World_Component'(
               (Kind      => Unify_Node,
                Counter   => 1,
                Uni_World => 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 := (Ada.Finalization.Controlled with
            Actual => new World_Component'(
               (Kind       => Disjunct_Node,
                Counter    => 1,
                Dis_World1 => Left,
                Dis_World2 => 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 Result : constant World := (Ada.Finalization.Controlled with
                Actual => new World_Component'(
                   (Kind       => Static_Node,
                    Counter    => 1,
                    Stc_States => State_Vectors.Empty_Vector)));
        elsif Inputs'Length = 1 then
            return Inputs (Inputs'First);
        else
            return Result : constant World := (Ada.Finalization.Controlled with
                Actual => new World_Component'(
                   (Kind       => Disjunct_Node,
                    Counter    => 1,
                    Dis_World1 => Inputs (Inputs'First),
                    Dis_World2 => 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 Junction_Zero_Func)
        return World is
    begin
        return Result : constant World := (Ada.Finalization.Controlled with
            Actual => new World_Component'(
               (Kind      => Conjunct_Node,
                Counter   => 1,
                Con_World => This,
                Con_Data  => Lazy_Holders.To_Holder ((Kind => Zero_Arg, ZFunc => Func)))));
    end Conjunct;


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


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


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


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


    procedure Conjunct
           (This   : in out World;
            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 World)
        return World is
    begin
        return Result : constant World := (Ada.Finalization.Controlled with
            Actual => new World_Component'(
               (Kind      => Recurse_Node,
                Counter   => 1,
                Rec_World => This)));
    end Recurse;


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



    --  Evaluation  --

    function Take
           (This  : in World;
            Count : in Positive)
        return State_Array
    is
        Result : State_Array (1 .. Count);
        Valid  : Natural := 0;

        package Collect is new Collector (This);
    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 Take;


    function Take_First
           (This : in World)
        return State
    is
        package Collect is new Collector (This);
    begin
        return Collect.Next (Empty_State);
    end Take_First;


    function Take_All
           (This : in World)
        return State_Array
    is
        package Collect is new Collector (This);

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



    --  Reification  --

    function Resolve
           (This  : in Term;
            Subst : in State)
        return Term
    is
        use type SU.Unbounded_String;
    begin
        case This.Kind is
        when Null_Term | Atom_Term =>
            return This;
        when Var_Term =>
            if  Subst.Ident.Contains (This.Var.Ident) and then
                Subst.Ident.Element (This.Var.Ident) in
                    Subst.LVars.First_Index .. Subst.LVars.Last_Index and then
                Subst.LVars.Element (Subst.Ident.Element (This.Var.Ident)) = This.Name and then
                Subst.Subst.Contains (Subst.Ident.Element (This.Var.Ident))
            then
                return Subst.Subst.Element (Subst.Ident.Element (This.Var.Ident)).Resolve (Subst);
            else
                return This;
            end if;
        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.LVars.Is_Empty then
            return Empty_Term;
        end if;
        for Iter in Subst.Ident.Iterate loop
            if ID_Number_Maps.Element (Iter) = Subst.LVars.First_Index then
                return Resolve (Term (T (Variable'(
                    Ident => ID_Number_Maps.Key (Iter),
                    Name  => Subst.LVars.Element (ID_Number_Maps.Element (Iter))))),
                    Subst);
            end if;
        end loop;
        return Empty_Term;
    end Resolve_First;


    function Resolve_First
           (Subst : in State;
            Name  : in String)
        return Term is
    begin
        return Resolve_First (Subst, +Name);
    end Resolve_First;


    function Resolve_First
           (Subst : in State;
            Name  : in Nametag)
        return Term
    is
        Name_Index : constant Name_Vectors.Extended_Index := Subst.LVars.Find_Index (Name);
    begin
        if Name_Index = Name_Vectors.No_Index then
            return Empty_Term;
        end if;
        for Iter in Subst.Ident.Iterate loop
            if ID_Number_Maps.Element (Iter) = Name_Index then
                return Resolve (Term (T (Variable'(
                    Ident => ID_Number_Maps.Key (Iter),
                    Name  => Subst.LVars.Element (ID_Number_Maps.Element (Iter))))),
                    Subst);
            end if;
        end loop;
        return Empty_Term;
    end Resolve_First;




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