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

    --  Variable Names  --

    subtype Nametag is Ada.Strings.Unbounded.Unbounded_String;
    type Nametag_Array is array (Positive range <>) of Nametag;


    --  Terms  --

    type Term_Kind is (Null_Term, Atom_Term, Var_Term, Pair_Term);

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

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

    function Kind
           (This : in Term)
        return Term_Kind;

    function Atom
           (This : in Term)
        return Element_Type
    with Pre => This.Kind = Atom_Term;

    function Name
           (This : in Term)
        return Nametag
    with Pre => This.Kind = Var_Term;

    function Left
           (This : in Term)
        return Term
    with Pre => This.Kind = Pair_Term;

    function Right
           (This : in Term)
        return Term
    with Pre => This.Kind = Pair_Term;


    --  States  --

    type State is private;
    type State_Array is array (Positive range <>) of State;

    Empty_State : constant State;


    --  Goals  --

    type Goal is tagged private;
    type Goal_Array is array (Positive range <>) of Goal;

    Empty_Goal : constant Goal;


    --  Junction Functions  --

    type Junction_Zero_Func is access function
           (This : in Goal)
        return Goal;

    type Junction_One_Func is access function
           (This  : in Goal;
            Input : in Term'Class)
        return Goal;

    type Junction_Many_Func is access function
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal;




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

    --  Variable Introduction  --

    function Fresh
           (This : in out Goal'Class)
        return Term
    with Post => Fresh'Result.Kind = Var_Term;

    function Fresh
           (This : in out Goal'Class;
            Name : in     String)
        return Term
    with Post => Fresh'Result.Kind = Var_Term;

    function Fresh
           (This : in out Goal'Class;
            Name : in     Nametag)
        return Term
    with Post => Fresh'Result.Kind = Var_Term;

    function Fresh
           (This  : in out Goal'Class;
            Count : in     Positive)
        return Term_Array
    with Post =>
        Fresh'Result'Length = Count and
        (for all Item of Fresh'Result => Item.Kind = Var_Term);

    function Fresh
           (This  : in out Goal'Class;
            Names : in     Nametag_Array)
        return Term_Array
    with Post =>
        Fresh'Result'Length = Names'Length and
        (for all Item of Fresh'Result => Item.Kind = Var_Term);

    generic
        Verse : in out Goal;
    function Make_Fresh
        return Term
    with Post => Make_Fresh'Result.Kind = Var_Term;


    --  Unification  --

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

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

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

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


    --  Combining / Disjunction  --

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

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

    function Disjunct
           (Inputs : in Goal_Array)
        return Goal;

    procedure Disjunct
           (This   : in out Goal;
            Inputs : in     Goal_Array);


    --  Lazy Sequencing / Conjunction  --

    function Conjunct
           (This : in Goal;
            Func : in Junction_Zero_Func)
        return Goal;

    procedure Conjunct
           (This : in out Goal;
            Func : in     Junction_Zero_Func);

    function Conjunct
           (This  : in Goal;
            Func  : in Junction_One_Func;
            Input : in Term'Class)
        return Goal;

    procedure Conjunct
           (This  : in out Goal;
            Func  : in     Junction_One_Func;
            Input : in     Term'Class);

    function Conjunct
           (This   : in Goal;
            Func   : in Junction_Many_Func;
            Inputs : in Term_Array)
        return Goal;

    procedure Conjunct
           (This   : in out Goal;
            Func   : in     Junction_Many_Func;
            Inputs : in     Term_Array);




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

    --  Infinite State Loops  --

    function Recurse
           (This : in Goal)
        return Goal;

    procedure Recurse
           (This : in out Goal);


    --  Evaluation  --

    function Run
           (This  : in Goal;
            Count : in Positive;
            Base  : in State := Empty_State)
        return State_Array;

    function Run
           (This : in Goal;
            Base : in State := Empty_State)
        return State;

    function Run_All
           (This : in Goal;
            Base : in State := Empty_State)
        return State_Array;


    --  Reification  --

    function Resolve
           (This  : in Term;
            Subst : in State)
        return Term;

    function Resolve_First
           (Subst : in State)
        return Term;

    function Resolve_First
           (Subst : in State;
            Name  : in String)
        return Term;

    function Resolve_First
           (Subst : in State;
            Name  : in Nametag)
        return Term;




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

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

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


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

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


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

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


    --  nullo  --

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

    procedure Nil
           (This     : in out Goal;
            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 Goal;
            Pair_Term : in Term'Class)
        return Goal;

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


    --  listo  --

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

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


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

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


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

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


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

    --  Inputs = List_Term & Item_Term & Out_Term
    procedure Append
           (This   : in out Goal;
            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 Goal


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




    --  around 2^31 possible Variables should be enough for anybody, right?
    subtype Long_Natural  is Long_Integer range 0 .. Long_Integer'Last;
    subtype Long_Positive is Long_Integer range 1 .. Long_Integer'Last;

    type Generator_ID_Number is new Long_Natural;
    type Variable_ID_Number  is new Long_Natural;

    type Variable is record
        Ident : Generator_ID_Number;
        Name  : Nametag;
    end record;




    type Term_Component;

    type Term_Component_Access is access Term_Component;

    subtype Not_Null_Term_Kind is Term_Kind range Atom_Term .. Pair_Term;

    type Term_Component (Kind : Not_Null_Term_Kind) is limited record
        Counter : Natural;
        case Kind is
        when Atom_Term =>
            Value : Element_Type;
        when Var_Term =>
            Refer : Variable;
        when Pair_Term =>
            Left  : Term;
            Right : Term;
        end case;
    end record;

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

    overriding procedure Initialize
           (This : in out Term);

    overriding procedure Adjust
           (This : in out Term);

    overriding procedure Finalize
           (This : in out Term);

    function T
           (Item : in Variable)
        return Term'Class;

    function Var
           (This : in Term'Class)
        return Variable
    with Pre => This.Kind = Var_Term;

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

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




    package ID_Number_Maps is new Ada.Containers.Ordered_Maps
       (Key_Type     => Generator_ID_Number,
        Element_Type => Variable_ID_Number);

    package Name_Vectors is new Ada.Containers.Vectors
       (Index_Type   => Variable_ID_Number,
        Element_Type => Nametag,
        "="          => SU."=");

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

    type State is record
        Ident : ID_Number_Maps.Map;
        LVars : Name_Vectors.Vector;
        Subst : Binding_Maps.Map;
    end record;

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

    Empty_State : constant State :=
       (Ident => ID_Number_Maps.Empty_Map,
        LVars => Name_Vectors.Empty_Vector,
        Subst => Binding_Maps.Empty_Map);




    type Goal_Component;

    type Goal_Component_Access is access Goal_Component;

    function "<"
           (Left, Right : in Goal_Component_Access)
        return Boolean;

    type Lazy_Kind is (Zero_Arg, One_Arg, Many_Arg);

    type Lazy_Data (Kind : Lazy_Kind) is record
        case Kind is
        when Zero_Arg =>
            ZFunc  : Junction_Zero_Func;
        when One_Arg =>
            OFunc  : Junction_One_Func;
            OInput : Term;
        when Many_Arg =>
            MFunc  : Junction_Many_Func;
            MInput : Term_Array_Holders.Holder;
        end case;
    end record;

    package Lazy_Holders is new Ada.Containers.Indefinite_Holders (Lazy_Data);

    type Node_Kind is
       (Static_Node,
        Fresh_Node,
        Unify_Node,
        Disjunct_Node,
        Conjunct_Node,
        Recurse_Node);

    type Goal_Component (Kind : Node_Kind) is limited record
        Counter : Natural;
        case Kind is
        when Static_Node =>
            null;
        when Fresh_Node =>
            Frs_Goal  : aliased Goal;
            Frs_Var   : Variable;
        when Unify_Node =>
            Uni_Goal  : aliased Goal;
            Uni_Term1 : Term;
            Uni_Term2 : Term;
        when Disjunct_Node =>
            Dis_Goal1 : aliased Goal;
            Dis_Goal2 : aliased Goal;
        when Conjunct_Node =>
            Con_Goal  : aliased Goal;
            Con_Data  : Lazy_Holders.Holder;
        when Recurse_Node =>
            Rec_Goal  : aliased Goal;
        end case;
    end record;

    type Goal is new Ada.Finalization.Controlled with record
        Actual : Goal_Component_Access := null;
    end record;

    overriding procedure Initialize
           (This : in out Goal);

    overriding procedure Adjust
           (This : in out Goal);

    overriding procedure Finalize
           (This : in out Goal);

    Empty_Goal : constant Goal := (Ada.Finalization.Controlled with
        Actual => new Goal_Component'(
           (Kind    => Static_Node,
            Counter => 1)));


end Kompsos;