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

--  See license.txt for further details


with

    Ada.Strings.Unbounded;

private with

    Ada.Containers.Indefinite_Holders,
    Ada.Containers.Ordered_Maps,
    Ada.Containers.Vectors,
    Ada.Finalization;


generic
    type Element_Type is private;
package Kompsos is


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

    type Term is tagged private;
    type Term_Array is array (Positive range <>) of Term;

    Null_Term : constant Term;

    function "="
           (Left, Right : in Term)
        return Boolean;

    function T
           (Item : in Element_Type)
        return Term;

    function T
           (Item1, Item2 : in Term'Class)
        return Term;

    function T
           (Items : in Term_Array)
        return Term;

    --  Might include subprograms to retrieve Term contents later?


    type World is tagged private;
    type World_Array is array (Positive range <>) of World;

    Empty_World : constant World;


    type Conjunct_Zero_Func is access function
           (This : in World)
        return World;

    type Conjunct_One_Func is access function
           (This  : in World;
            Input : in Term'Class)
        return World;

    type Conjunct_Many_Func is access function
           (This   : in World;
            Inputs : in Term_Array)
        return World;




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

    --  Variable Introduction  --

    function Fresh
           (This : in out World'Class)
        return Term;

    function Fresh
           (This : in out World'Class;
            Name : in     String)
        return Term;

    function Fresh
           (This : in out World'Class;
            Name : in     Ada.Strings.Unbounded.Unbounded_String)
        return Term;


    --  Unification  --

    function Unify
           (This  : in World;
            Left  : in Term'Class;
            Right : in Element_Type)
        return World;

    procedure Unify
           (This  : in out World;
            Left  : in     Term'Class;
            Right : in     Element_Type);

    function Unify
           (This        : in World;
            Left, Right : in Term'Class)
        return World;

    procedure Unify
           (This        : in out World;
            Left, Right : in     Term'Class);


    --  Combining / Disjunction  --

    function Disjunct
           (Left, Right : in World)
        return World;

    procedure Disjunct
           (This  : in out World;
            Right : in     World);

    function Disjunct
           (Inputs : in World_Array)
        return World;

    procedure Disjunct
           (This   : in out World;
            Inputs : in     World_Array);


    --  Lazy Sequencing / Conjunction  --

    function Conjunct
           (This : in World;
            Func : in Conjunct_Zero_Func)
        return World;

    procedure Conjunct
           (This : in out World;
            Func : in     Conjunct_Zero_Func);

    function Conjunct
           (This  : in World;
            Func  : in Conjunct_One_Func;
            Input : in Term'Class)
        return World;

    procedure Conjunct
           (This  : in out World;
            Func  : in     Conjunct_One_Func;
            Input : in     Term'Class);

    function Conjunct
           (This   : in World;
            Func   : in Conjunct_Many_Func;
            Inputs : in Term_Array)
        return World;

    procedure Conjunct
           (This   : in out World;
            Func   : in     Conjunct_Many_Func;
            Inputs : in     Term_Array);




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

    --  Infinite State Loops  --

    function Recurse
           (This : in World)
        return World;

    procedure Recurse
           (This : in out World);


    --  Forced Evaluation  --

    function Take
           (This  : in World;
            Count : in Natural)
        return World;

    procedure Take
           (This  : in out World;
            Count : in     Natural);

    procedure Force
           (This  : in out World;
            Count : in     Positive);

    procedure Force_All
           (This : in out World);

    function Failed
           (This : in out World)
        return Boolean;




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

    --  caro  --
    --  Inputs = List_Term & Head_Term
    function Head
           (This   : in World;
            Inputs : in Term_Array)
        return World
    with Pre => Inputs'Length = 2;

    --  Inputs = List_Term & Head_Term
    procedure Head
           (This   : in out World;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 2;


    --  cdro  --
    --  Inputs = List_Term & Tail_Term
    function Tail
           (This   : in World;
            Inputs : in Term_Array)
        return World
    with Pre => Inputs'Length = 2;

    --  Inputs = List_Term & Tail_Term
    procedure Tail
           (This   : in out World;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 2;


    --  conso  --
    --  Inputs = Head_Term & Tail_Term & List_Term
    function Cons
           (This   : in World;
            Inputs : in Term_Array)
        return World
    with Pre => Inputs'Length = 3;

    --  Inputs = Head_Term & Tail_Term & List_Term
    procedure Cons
           (This   : in out World;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 3;


    --  nullo  --

    function Nil
           (This     : in World;
            Nil_Term : in Term'Class)
        return World;

    procedure Nil
           (This     : in out World;
            Nil_Term : in     Term'Class);


    --  eqo  --
    --  Skipped due to being a synonym for Unify


    --  eq-caro  --
    --  Skipped due to being a synonym for Head


    --  pairo  --

    function Pair
           (This      : in World;
            Pair_Term : in Term'Class)
        return World;

    procedure Pair
           (This      : in out World;
            Pair_Term : in     Term'Class);


    --  listo  --

    function Linked_List
           (This      : in World;
            List_Term : in Term'Class)
        return World;

    procedure Linked_List
           (This      : in out World;
            List_Term : in     Term'Class);


    --  membero  --
    --  Inputs = Item_Term & List_Term
    function Member
           (This   : in World;
            Inputs : in Term_Array)
        return World
    with Pre => Inputs'Length = 2;

    --  Inputs = Item_Term & List_Term
    procedure Member
           (This   : in out World;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 2;


    --  rembero  --
    --  Inputs = Item_Term & List_Term & Out_Term
    function Remove
           (This   : in World;
            Inputs : in Term_Array)
        return World
    with Pre => Inputs'Length = 3;

    --  Inputs = Item_Term & List_Term & Out_Term
    procedure Remove
           (This   : in out World;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 3;


    --  appendo  --
    --  Inputs = List_Term & Item_Term & Out_Term
    function Append
           (This   : in World;
            Inputs : in Term_Array)
        return World
    with Pre => Inputs'Length = 3;

    --  Inputs = List_Term & Item_Term & Out_Term
    procedure Append
           (This   : in out World;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 3;


    --  anyo  --
    --  Skipped due to Recurse doing the same thing


    --  nevero  --
    --  Skipped since it just creates a failed World


    --  alwayso  --
    --  Skipped due to Recurse doing the same thing


private


    package SU renames Ada.Strings.Unbounded;


    function "+"
           (Item : in String)
        return SU.Unbounded_String
    renames SU.To_Unbounded_String;

    function "-"
           (Item : in SU.Unbounded_String)
        return String
    renames SU.To_String;




    --  2^32 possible Variables per World is enough for anybody, right?
    type ID_Number is mod 2 ** 32;

    type Variable is record
        Ident : ID_Number;
        Name  : SU.Unbounded_String;
    end record;




    type Term_Kind is (Atom_Term, Var_Term, Pair_Term);

    type Term_Component (Kind : Term_Kind) is record
        Count : Long_Integer;
        case Kind is
        when Atom_Term =>
            Value : Element_Type;
        when Var_Term =>
            Refer : Variable;
        when Pair_Term =>
            Left, Right : Term;
        end case;
    end record;

    type Term_Component_Access is access Term_Component;

    type Term is new Ada.Finalization.Controlled with record
        Actual : Term_Component_Access;
    end record;

    overriding procedure Initialize
           (This : in out Term);

    overriding procedure Adjust
           (This : in out Term);

    overriding procedure Finalize
           (This : in out Term);

    Null_Term : constant Term := (Ada.Finalization.Controlled with Actual => null);

    package Term_Array_Holders is new Ada.Containers.Indefinite_Holders (Term_Array);




    package Name_Maps is new Ada.Containers.Ordered_Maps
       (Key_Type     => ID_Number,
        Element_Type => SU.Unbounded_String,
        "="          => SU."=");

    package Binding_Maps is new Ada.Containers.Ordered_Maps
       (Key_Type     => ID_Number,
        Element_Type => Term);

    type State is record
        LVars : Name_Maps.Map;
        Subst : Binding_Maps.Map;
    end record;

    Empty_State : constant State :=
       (LVars => Name_Maps.Empty_Map,
        Subst => Binding_Maps.Empty_Map);




    type World_Access is access World'Class;

    type World_Holder is new Ada.Finalization.Controlled with record
        Ptr : World_Access;
    end record;

    overriding procedure Initialize
           (This : in out World_Holder);

    overriding procedure Adjust
           (This : in out World_Holder);

    overriding procedure Finalize
           (This : in out World_Holder);

    function Hold
           (This : in World'Class)
        return World_Holder;

    procedure Swap
           (Left, Right : in out World_Holder);

    type Generator_Kind is
       (No_Gen,
        Fresh_Gen,
        Unify_Gen,
        Buffer_Gen,
        Disjunct_Gen,
        Conjunct_Zero_Gen,
        Conjunct_One_Gen,
        Conjunct_Many_Gen,
        Recurse_Gen);

    type Generator (Kind : Generator_Kind := No_Gen) is record
        case Kind is
        when No_Gen =>
            null;
        when Fresh_Gen =>
            Frs_World   : World_Holder;
            Frs_Name    : SU.Unbounded_String;
        when Unify_Gen =>
            Uni_World   : World_Holder;
            Uni_Term1   : Term;
            Uni_Term2   : Term;
        when Buffer_Gen =>
            Buff_World  : World_Holder;
        when Disjunct_Gen =>
            Dis_World1  : World_Holder;
            Dis_World2  : World_Holder;
        when Conjunct_Zero_Gen =>
            ConZ_World  : World_Holder;
            ConZ_Func   : Conjunct_Zero_Func;
        when Conjunct_One_Gen =>
            ConO_World  : World_Holder;
            ConO_Func   : Conjunct_One_Func;
            ConO_Input  : Term;
        when Conjunct_Many_Gen =>
            ConM_World  : World_Holder;
            ConM_Func   : Conjunct_Many_Func;
            ConM_Inputs : Term_Array_Holders.Holder;
        when Recurse_Gen =>
            Rec_World   : World_Holder;
            Rec_Index   : Positive;
        end case;
    end record;

    package State_Vectors is new Ada.Containers.Vectors
       (Index_Type   => Positive,
        Element_Type => State);

    type World is tagged record
        Possibles  : State_Vectors.Vector;
        Next_Ident : ID_Number;
        Engine     : Generator;
    end record;

    function Has_State
           (This  : in out World;
            Index : in     Positive)
        return Boolean;

    procedure Rollover
           (This : in out World);

    procedure Roll_Until
           (This  : in out World;
            Index : in     Positive);

    use type State_Vectors.Vector;

    Empty_World : constant World :=
       (Possibles  => State_Vectors.Empty_Vector & Empty_State,
        Next_Ident => 0,
        Engine     => (Kind => No_Gen));


end Kompsos;