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

--  See license.txt for further details


package body Kompsos.Math is


    ----------------
    --  Accesses  --
    ----------------

    --  These are needed for some really dumb reason about not allowing 'Access
    --  in a generic body when the access type is declared outside the generic.

    --  Can't apply 'Unchecked_Access to a subprogram either, so we're doing this.

    LT_Length_Access : constant access function
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal := LT_Length'Access;

    EQ_Length_Access : constant access function
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal := EQ_Length'Access;

    Adder_Access : constant access function
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal := Adder'Access;

    General_Adder_Access : constant access function
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal := General_Adder'Access;

    Multiply_Access : constant access function
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal := Multiply'Access;

    Odd_Multiply_Access : constant access function
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal := Odd_Multiply'Access;

    Bounded_Multiply_Access : constant access function
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal := Bounded_Multiply'Access;

    Divide_Access : constant access function
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal := Divide'Access;

    Split_Access : constant access function
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal := Split'Access;

    Exp_Two_Access : constant access function
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal := Exp_Two'Access;

    Repeated_Multiply_Access : constant access function
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal := Repeated_Multiply'Access;




    ---------------
    --  Numbers  --
    ---------------

    function Is_Number
           (Item : in Term)
        return Boolean is
    begin
        if Item.Kind = Null_Term then
            return True;
        elsif Item.Kind = Pair_Term and then Item.Left.Kind = Atom_Term then
            if Item.Right.Kind = Null_Term then
                return Item.Left.Atom = One_Element;
            else
                return (Item.Left.Atom = Zero_Element or else Item.Left.Atom = One_Element) and then
                    Is_Number (Item.Right);
            end if;
        else
            return False;
        end if;
    end Is_Number;


    function Build
           (Value : in Natural)
        return Term is
    begin
        if Value = 0 then
            return Empty_Term;
        elsif Value mod 2 = 0 then
            return T (T (Zero_Element), Build (Value / 2));
        else
            return T (T (One_Element), Build ((Value - 1) / 2));
        end if;
    end Build;


    function Value
           (Item : in Term)
        return Natural is
    begin
        if Item.Kind = Null_Term then
            return 0;
        elsif Item.Left.Atom = Zero_Element then
            return 2 * Value (Item.Right);
        else
            return 1 + 2 * Value (Item.Right);
        end if;
    end Value;




    ------------------
    --  Comparison  --
    ------------------

    --  poso  --

    function GT_Zero
           (This     : in Goal;
            Num_Term : in Term'Class)
        return Goal is
    begin
        return This.Pair (Num_Term);
    end GT_Zero;


    procedure GT_Zero
           (This     : in out Goal;
            Num_Term : in     Term'Class) is
    begin
        This := GT_Zero (This, Num_Term);
    end GT_Zero;



    --  >1o  --

    function GT_One
           (This     : in Goal;
            Num_Term : in Term'Class)
        return Goal
    is
        Result : Goal := This;
        Ref_Term : constant Term := Result.Fresh;
    begin
        Result.Tail (Term (Num_Term) & Ref_Term);
        Result.Pair (Ref_Term);
        return Result;
    end GT_One;


    procedure GT_One
           (This     : in out Goal;
            Num_Term : in     Term'Class) is
    begin
        This := GT_One (This, Num_Term);
    end GT_One;



    --  <lo  --

    function LT_Length
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    is
        N_Term : Term renames Inputs (1);
        M_Term : Term renames Inputs (2);

        One, Two, Three : Goal := This;

        X_Var : constant Term := Three.Fresh;
        Y_Var : constant Term := Three.Fresh;
    begin
        One.Unify (N_Term, Zero_Term);
        GT_Zero (One, M_Term);

        Two.Unify (N_Term, One_Term);
        GT_One (Two, M_Term);

        Three.Unify (N_Term, T (Three.Fresh, X_Var));
        GT_Zero (Three, X_Var);
        Three.Unify (M_Term, T (Three.Fresh, Y_Var));
        GT_Zero (Three, Y_Var);
        Three.Conjunct (LT_Length_Access, X_Var & Y_Var);

        return Disjunct (One & Two & Three);
    end LT_Length;


    procedure LT_Length
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := LT_Length (This, Inputs);
    end LT_Length;



    --  <=lo  --

    function LTE_Length
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal is
    begin
        return Disjunct
           (EQ_Length (This, Inputs),
            LT_Length (This, Inputs));
    end LTE_Length;


    procedure LTE_Length
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := LTE_Length (This, Inputs);
    end LTE_Length;



    --  =lo  --

    function EQ_Length
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    is
        N_Term : Term renames Inputs (1);
        M_Term : Term renames Inputs (2);

        One, Two, Three : Goal := This;

        X_Var : constant Term := Three.Fresh;
        Y_Var : constant Term := Three.Fresh;
    begin
        One.Unify (N_Term, Zero_Term);
        One.Unify (M_Term, Zero_Term);

        Two.Unify (N_Term, One_Term);
        Two.Unify (M_Term, One_Term);

        Three.Unify (N_Term, T (Three.Fresh, X_Var));
        GT_Zero (Three, X_Var);
        Three.Unify (M_Term, T (Three.Fresh, Y_Var));
        GT_Zero (Three, Y_Var);
        Three.Conjunct (EQ_Length_Access, X_Var & Y_Var);

        return Disjunct (One & Two & Three);
    end EQ_Length;


    procedure EQ_Length
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := EQ_Length (This, Inputs);
    end EQ_Length;



    --  (extra function)  --

    function GTE_Length
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal is
    begin
        return LTE_Length (This, Inputs (2) & Inputs (1));
    end GTE_Length;


    procedure GTE_Length
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := GTE_Length (This, Inputs);
    end GTE_Length;



    --  (extra function)  --

    function GT_Length
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal is
    begin
        return LT_Length (This, Inputs (2) & Inputs (1));
    end GT_Length;


    procedure GT_Length
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := GT_Length (This, Inputs);
    end GT_Length;



    --  <o  --

    function LT
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    is
        N_Term : Term renames Inputs (1);
        M_Term : Term renames Inputs (2);

        One, Two : Goal := This;

        X_Var : constant Term := Two.Fresh;
    begin
        LT_Length (One, Inputs);

        EQ_Length (Two, Inputs);
        GT_Zero (Two, X_Var);
        Add (Two, N_Term & X_Var & M_Term);

        return Disjunct (One, Two);
    end LT;


    procedure LT
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := LT (This, Inputs);
    end LT;



    --  <=o  --

    function LTE
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal is
    begin
        return Disjunct
           (This.Unify (Inputs (1), Inputs (2)),
            LT (This, Inputs));
    end LTE;


    procedure LTE
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := LTE (This, Inputs);
    end LTE;



    --  (extra function)  --

    function GTE
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal is
    begin
        return LTE (This, Inputs (2) & Inputs (1));
    end GTE;


    procedure GTE
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := GTE (This, Inputs);
    end GTE;



    --  (extra function)  --

    function GT
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal is
    begin
        return LT (This, Inputs (2) & Inputs (1));
    end GT;


    procedure GT
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := GT (This, Inputs);
    end GT;




    ------------------
    --  Arithmetic  --
    ------------------

    --  full-addero  --

    function Full_Adder
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    is
        Cin_Term  : Term renames Inputs (1);
        A_Term    : Term renames Inputs (2);
        B_Term    : Term renames Inputs (3);
        Sum_Term  : Term renames Inputs (4);
        Cout_Term : Term renames Inputs (5);

        Outputs : Goal_Array := (1 .. 8 => This);
    begin
        Outputs (1).Unify (Cin_Term,  Zero_Element);    Outputs (2).Unify (Cin_Term,   One_Element);
        Outputs (1).Unify (A_Term,    Zero_Element);    Outputs (2).Unify (A_Term,    Zero_Element);
        Outputs (1).Unify (B_Term,    Zero_Element);    Outputs (2).Unify (B_Term,    Zero_Element);
        Outputs (1).Unify (Sum_Term,  Zero_Element);    Outputs (2).Unify (Sum_Term,   One_Element);
        Outputs (1).Unify (Cout_Term, Zero_Element);    Outputs (2).Unify (Cout_Term, Zero_Element);

        Outputs (3).Unify (Cin_Term,  Zero_Element);    Outputs (4).Unify (Cin_Term,   One_Element);
        Outputs (3).Unify (A_Term,     One_Element);    Outputs (4).Unify (A_Term,     One_Element);
        Outputs (3).Unify (B_Term,    Zero_Element);    Outputs (4).Unify (B_Term,    Zero_Element);
        Outputs (3).Unify (Sum_Term,   One_Element);    Outputs (4).Unify (Sum_Term,  Zero_Element);
        Outputs (3).Unify (Cout_Term, Zero_Element);    Outputs (4).Unify (Cout_Term,  One_Element);

        Outputs (5).Unify (Cin_Term,  Zero_Element);    Outputs (6).Unify (Cin_Term,   One_Element);
        Outputs (5).Unify (A_Term,    Zero_Element);    Outputs (6).Unify (A_Term,    Zero_Element);
        Outputs (5).Unify (B_Term,     One_Element);    Outputs (6).Unify (B_Term,     One_Element);
        Outputs (5).Unify (Sum_Term,   One_Element);    Outputs (6).Unify (Sum_Term,  Zero_Element);
        Outputs (5).Unify (Cout_Term, Zero_Element);    Outputs (6).Unify (Cout_Term,  One_Element);

        Outputs (7).Unify (Cin_Term,  Zero_Element);    Outputs (8).Unify (Cin_Term,   One_Element);
        Outputs (7).Unify (A_Term,     One_Element);    Outputs (8).Unify (A_Term,     One_Element);
        Outputs (7).Unify (B_Term,     One_Element);    Outputs (8).Unify (B_Term,     One_Element);
        Outputs (7).Unify (Sum_Term,  Zero_Element);    Outputs (8).Unify (Sum_Term,   One_Element);
        Outputs (7).Unify (Cout_Term,  One_Element);    Outputs (8).Unify (Cout_Term,  One_Element);

        return Disjunct (Outputs);
    end Full_Adder;


    procedure Full_Adder
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := Full_Adder (This, Inputs);
    end Full_Adder;



    --  addero  --

    function Adder
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    is
        Cin_Term : Term renames Inputs (1);
        N_Term   : Term renames Inputs (2);
        M_Term   : Term renames Inputs (3);
        Sum_Term : Term renames Inputs (4);

        Outputs : Goal_Array := (1 .. 8 => This);
    begin
        Outputs (1).Unify (Cin_Term, Zero_Element);
        Outputs (1).Unify (M_Term, Zero_Term);
        Outputs (1).Unify (N_Term, Sum_Term);

        Outputs (2).Unify (Cin_Term, Zero_Element);
        Outputs (2).Unify (N_Term, Zero_Term);
        Outputs (2).Unify (M_Term, Sum_Term);
        GT_Zero (Outputs (2), M_Term);

        Outputs (3).Unify (Cin_Term, One_Element);
        Outputs (3).Unify (M_Term, Zero_Term);
        Outputs (3).Conjunct (Adder_Access, T (Zero_Element) & N_Term & One_Term & Sum_Term);

        Outputs (4).Unify (Cin_Term, One_Element);
        Outputs (4).Unify (N_Term, Zero_Term);
        GT_Zero (Outputs (4), M_Term);
        Outputs (4).Conjunct (Adder_Access, T (Zero_Element) & One_Term & M_Term & Sum_Term);

        Outputs (5).Unify (N_Term, One_Term);
        Outputs (5).Unify (M_Term, One_Term);
        declare
            A_Var : constant Term := Outputs (5).Fresh;
            C_Var : constant Term := Outputs (5).Fresh;
        begin
            Outputs (5).Unify (T (A_Var, C_Var), Sum_Term);
            Full_Adder (Outputs (5), Cin_Term & T (One_Element) & T (One_Element) & A_Var & C_Var);
        end;

        Outputs (6).Unify (N_Term, One_Term);
        GT_One (Outputs (6), M_Term);
        Outputs (6).Conjunct (General_Adder_Access, Inputs);

        Outputs (7).Unify (M_Term, One_Term);
        GT_One (Outputs (7), N_Term);
        GT_One (Outputs (7), Sum_Term);
        Outputs (7).Conjunct (Adder_Access, Cin_Term & One_Term & N_Term & Sum_Term);

        GT_One (Outputs (8), N_Term);
        GT_One (Outputs (8), M_Term);
        Outputs (8).Conjunct (General_Adder_Access, Inputs);

        return Disjunct (Outputs);
    end Adder;


    procedure Adder
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := Adder (This, Inputs);
    end Adder;



    --  gen-addero  --

    function General_Adder
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    is
        Cin_Term : Term renames Inputs (1);
        N_Term   : Term renames Inputs (2);
        M_Term   : Term renames Inputs (3);
        Sum_Term : Term renames Inputs (4);

        Result : Goal := This;

        A_Var : constant Term := Result.Fresh;
        B_Var : constant Term := Result.Fresh;
        C_Var : constant Term := Result.Fresh;
        D_Var : constant Term := Result.Fresh;
        X_Var : constant Term := Result.Fresh;
        Y_Var : constant Term := Result.Fresh;
        Z_Var : constant Term := Result.Fresh;
    begin
        Result.Unify (T (A_Var, X_Var), N_Term);
        Result.Unify (T (B_Var, Y_Var), M_Term);
        GT_Zero (Result, Y_Var);
        Result.Unify (T (C_Var, Z_Var), Sum_Term);
        GT_Zero (Result, Z_Var);
        Full_Adder (Result, Cin_Term & A_Var & B_Var & C_Var & D_Var);
        Result.Conjunct (Adder_Access, D_Var & X_Var & Y_Var & Z_Var);
        return Result;
    end General_Adder;


    procedure General_Adder
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := General_Adder (This, Inputs);
    end General_Adder;



    --  +o  --

    function Add
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal is
    begin
        return Adder (This, T (Zero_Element) & Inputs);
    end Add;


    procedure Add
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := Add (This, Inputs);
    end Add;



    --  -o  --

    function Subtract
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    is
        N_Term          : Term renames Inputs (1);
        M_Term          : Term renames Inputs (2);
        Difference_Term : Term renames Inputs (3);
    begin
        return Add (This, M_Term & Difference_Term & N_Term);
    end Subtract;


    procedure Subtract
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := Subtract (This, Inputs);
    end Subtract;



    --  *o  --

    function Multiply
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    is
        N_Term       : Term renames Inputs (1);
        M_Term       : Term renames Inputs (2);
        Product_Term : Term renames Inputs (3);

        Outputs : Goal_Array := (1 .. 7 => This);
    begin
        Outputs (1).Unify (N_Term, Zero_Term);
        Outputs (1).Unify (Product_Term, Zero_Term);

        GT_Zero (Outputs (2), N_Term);
        Outputs (2).Unify (M_Term, Zero_Term);
        Outputs (2).Unify (Product_Term, Zero_Term);

        Outputs (3).Unify (N_Term, One_Term);
        GT_Zero (Outputs (3), M_Term);
        Outputs (3).Unify (M_Term, Product_Term);

        GT_One (Outputs (4), N_Term);
        Outputs (4).Unify (M_Term, One_Term);
        Outputs (4).Unify (N_Term, Product_Term);

        declare
            X_Var : constant Term := Outputs (5).Fresh;
            Z_Var : constant Term := Outputs (5).Fresh;
        begin
            Outputs (5).Unify (T (T (Zero_Element), X_Var), N_Term);
            GT_Zero (Outputs (5), X_Var);
            Outputs (5).Unify (T (T (Zero_Element), Z_Var), Product_Term);
            GT_Zero (Outputs (5), Z_Var);
            GT_One (Outputs (5), M_Term);
            Outputs (5).Conjunct (Multiply_Access, X_Var & M_Term & Z_Var);
        end;

        declare
            X_Var : constant Term := Outputs (6).Fresh;
            Y_Var : constant Term := Outputs (6).Fresh;
        begin
            Outputs (6).Unify (T (T (One_Element), X_Var), N_Term);
            GT_Zero (Outputs (6), X_Var);
            Outputs (6).Unify (T (T (Zero_Element), Y_Var), M_Term);
            GT_Zero (Outputs (6), Y_Var);
            Outputs (6).Conjunct (Multiply_Access, M_Term & N_Term & Product_Term);
        end;

        declare
            X_Var : constant Term := Outputs (7).Fresh;
            Y_Var : constant Term := Outputs (7).Fresh;
        begin
            Outputs (7).Unify (T (T (One_Element), X_Var), N_Term);
            GT_Zero (Outputs (7), X_Var);
            Outputs (7).Unify (T (T (One_Element), Y_Var), M_Term);
            GT_Zero (Outputs (7), Y_Var);
            Outputs (7).Conjunct (Odd_Multiply_Access, X_Var & N_Term & M_Term & Product_Term);
        end;

        return Disjunct (Outputs);
    end Multiply;


    procedure Multiply
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := Multiply (This, Inputs);
    end Multiply;



    --  odd-*o  --

    function Odd_Multiply
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    is
        X_Term       : Term renames Inputs (1);
        N_Term       : Term renames Inputs (2);
        M_Term       : Term renames Inputs (3);
        Product_Term : Term renames Inputs (4);

        Result : Goal := This;

        Q_Var : constant Term := Result.Fresh;
    begin
        Bounded_Multiply (Result, Q_Var & Product_Term & N_Term & M_Term);
        Multiply (Result, X_Term & M_Term & Q_Var);
        Add (Result, T (T (Zero_Element), Q_Var) & M_Term & Product_Term);
        return Result;
    end Odd_Multiply;


    procedure Odd_Multiply
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := Odd_Multiply (This, Inputs);
    end Odd_Multiply;



    --  bound-*o  --

    function Bounded_Multiply
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    is
        Q_Term       : Term renames Inputs (1);
        Product_Term : Term renames Inputs (2);
        N_Term       : Term renames Inputs (3);
        M_Term       : Term renames Inputs (4);

        One, Two : Goal := This;

        X_Var : constant Term := Two.Fresh;
        Y_Var : constant Term := Two.Fresh;
        Z_Var : constant Term := Two.Fresh;
    begin
        One.Nil (Q_Term);
        One.Pair (Product_Term);

        Two.Tail (Q_Term & X_Var);
        Two.Tail (Product_Term & Y_Var);
        declare
            Two_A, Two_B : Goal := Two;
        begin
            Two_A.Nil (N_Term);
            Two_A.Tail (M_Term & Z_Var);
            Two_A.Conjunct (Bounded_Multiply_Access, X_Var & Y_Var & Z_Var & Zero_Term);

            Two_B.Tail (N_Term & Z_Var);
            Two_B.Conjunct (Bounded_Multiply_Access, X_Var & Y_Var & Z_Var & M_Term);

            return Disjunct (One & Two_A & Two_B);
        end;
    end Bounded_Multiply;


    procedure Bounded_Multiply
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := Bounded_Multiply (This, Inputs);
    end Bounded_Multiply;



    --  /o  --

    function Divide
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    is
        N_Term         : Term renames Inputs (1);
        M_Term         : Term renames Inputs (2);
        Quotient_Term  : Term renames Inputs (3);
        Remainder_Term : Term renames Inputs (4);

        One, Two, Three : Goal := This;

        N_Low             : constant Term := Three.Fresh;
        N_High            : constant Term := Three.Fresh;
        Quot_Low          : constant Term := Three.Fresh;
        Quot_High         : constant Term := Three.Fresh;
        Quot_Low_M        : constant Term := Three.Fresh;
        Quot_Low_M_Remain : constant Term := Three.Fresh;
        Remain_Remain     : constant Term := Three.Fresh;
        Remain_High       : constant Term := Three.Fresh;
    begin
        One.Unify (N_Term, Remainder_Term);
        One.Unify (Quotient_Term, Zero_Term);
        LT (One, N_Term & M_Term);

        Two.Unify (Quotient_Term, One_Term);
        EQ_Length (Two, N_Term & M_Term);
        Add (Two, Remainder_Term & M_Term & N_Term);
        LT (Two, Remainder_Term & M_Term);

        LT_Length (Three, M_Term & N_Term);
        LT (Three, Remainder_Term & M_Term);
        GT_Zero (Three, Quotient_Term);
        Three.Conjunct (Split_Access, N_Term & Remainder_Term & N_Low & N_High);
        Three.Conjunct (Split_Access, Quotient_Term & Remainder_Term & Quot_Low & Quot_High);
        declare
            Three_A, Three_B : Goal := Three;
        begin
            Three_A.Unify (N_High, Zero_Term);
            Three_A.Unify (Quot_High, Zero_Term);
            Subtract (Three_A, N_Low & Remainder_Term & Quot_Low_M);
            Multiply (Three_A, Quot_Low & M_Term & Quot_Low_M);

            GT_Zero (Three_B, N_High);
            Multiply (Three_B, Quot_Low & M_Term & Quot_Low_M);
            Add (Three_B, Quot_Low_M & Remainder_Term & Quot_Low_M_Remain);
            Subtract (Three_B, Quot_Low_M_Remain & N_Low & Remain_Remain);
            Three_B.Conjunct (Split_Access,
                Remain_Remain & Remainder_Term & Zero_Term & Remain_High);
            Three_B.Conjunct (Divide_Access, N_High & M_Term & Quot_High & Remain_High);

            return Disjunct (One & Two & Three_A & Three_B);
        end;
    end Divide;


    procedure Divide
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := Divide (This, Inputs);
    end Divide;



    --  splito  --

    function Split
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    is
        N_Term         : Term renames Inputs (1);
        Remainder_Term : Term renames Inputs (2);
        Low_Term       : Term renames Inputs (3);
        High_Term      : Term renames Inputs (4);

        Outputs : Goal_Array := (1 .. 6 => This);
    begin
        Outputs (1).Unify (N_Term, Zero_Term);
        Outputs (1).Unify (High_Term, Zero_Term);
        Outputs (1).Unify (Low_Term, Zero_Term);

        declare
            B_Var : constant Term := Outputs (2).Fresh;
            N_Hat : constant Term := Outputs (2).Fresh;
        begin
            Outputs (2).Unify (N_Term, T (T (Zero_Element), T (B_Var, N_Hat)));
            Outputs (2).Unify (Remainder_Term, Zero_Term);
            Outputs (2).Unify (High_Term, T (B_Var, N_Hat));
            Outputs (2).Unify (Low_Term, Zero_Term);
        end;

        declare
            N_Hat : constant Term := Outputs (3).Fresh;
        begin
            Outputs (3).Unify (N_Term, T (T (One_Element), N_Hat));
            Outputs (3).Unify (Remainder_Term, Zero_Term);
            Outputs (3).Unify (High_Term, N_Hat);
            Outputs (3).Unify (Low_Term, One_Term);
        end;

        declare
            B_Var : constant Term := Outputs (4).Fresh;
            N_Hat : constant Term := Outputs (4).Fresh;
            A_Var : constant Term := Outputs (4).Fresh;
            R_Hat : constant Term := Outputs (4).Fresh;
        begin
            Outputs (4).Unify (N_Term, T (T (Zero_Element), T (B_Var, N_Hat)));
            Outputs (4).Unify (Remainder_Term, T (A_Var, R_Hat));
            Outputs (4).Unify (Low_Term, Zero_Term);
            Outputs (4).Conjunct (Split_Access, T (B_Var, N_Hat) & R_Hat & Zero_Term & High_Term);
        end;

        declare
            N_Hat : constant Term := Outputs (5).Fresh;
            A_Var : constant Term := Outputs (5).Fresh;
            R_Hat : constant Term := Outputs (5).Fresh;
        begin
            Outputs (5).Unify (N_Term, T (T (One_Element), N_Hat));
            Outputs (5).Unify (Remainder_Term, T (A_Var, R_Hat));
            Outputs (5).Unify (Low_Term, One_Term);
            Outputs (5).Conjunct (Split_Access, N_Hat & R_Hat & Zero_Term & High_Term);
        end;

        declare
            B_Var : constant Term := Outputs (6).Fresh;
            N_Hat : constant Term := Outputs (6).Fresh;
            A_Var : constant Term := Outputs (6).Fresh;
            R_Hat : constant Term := Outputs (6).Fresh;
            L_Hat : constant Term := Outputs (6).Fresh;
        begin
            Outputs (6).Unify (N_Term, T (B_Var, N_Hat));
            Outputs (6).Unify (Remainder_Term, T (A_Var, R_Hat));
            Outputs (6).Unify (Low_Term, T (B_Var, L_Hat));
            GT_Zero (Outputs (6), L_Hat);
            Outputs (6).Conjunct (Split_Access, N_Hat & R_Hat & L_Hat & High_Term);
        end;

        return Disjunct (Outputs);
    end Split;


    procedure Split
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := Split (This, Inputs);
    end Split;



    --  logo  --

    function Logarithm
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    is
        Power_Term     : Term renames Inputs (1);
        Base_Term      : Term renames Inputs (2);
        Exponent_Term  : Term renames Inputs (3);
        Remainder_Term : Term renames Inputs (4);

        Outputs : Goal_Array := (1 .. 7 => This);
    begin
        Outputs (1).Unify (Power_Term, One_Term);
        GT_Zero (Outputs (1), Base_Term);
        Outputs (1).Unify (Exponent_Term, Zero_Term);
        Outputs (1).Unify (Remainder_Term, Zero_Term);

        Outputs (2).Unify (Exponent_Term, Zero_Term);
        LT (Outputs (2), Power_Term & Base_Term);
        Add (Outputs (2), Remainder_Term & One_Term & Power_Term);

        Outputs (3).Unify (Exponent_Term, One_Term);
        GT_One (Outputs (3), Base_Term);
        EQ_Length (Outputs (3), Power_Term & Base_Term);
        Add (Outputs (3), Remainder_Term & Base_Term & Power_Term);

        Outputs (4).Unify (Base_Term, One_Term);
        GT_Zero (Outputs (4), Exponent_Term);
        Add (Outputs (4), Remainder_Term & One_Term & Power_Term);

        Outputs (5).Unify (Base_Term, Zero_Term);
        GT_Zero (Outputs (5), Exponent_Term);
        Outputs (5).Unify (Remainder_Term, Power_Term);

        Outputs (6).Unify (Base_Term, Build (2));
        declare
            DD_Var : constant Term := Outputs (6).Fresh;
        begin
            GT_Zero (Outputs (6), DD_Var);
            Outputs (6).Unify (Power_Term, T (Outputs (6).Fresh, T (Outputs (6).Fresh, DD_Var)));
            Outputs (6).Conjunct (Exp_Two_Access, Power_Term & Zero_Term & Exponent_Term);
            Outputs (6).Conjunct (Split_Access,
                Power_Term & DD_Var & Remainder_Term & Outputs (6).Fresh);
        end;

        --  I know what you're thinking. Clear as mud, right?
        --  Well unfortunately the original miniKanren Scheme isn't really any better.
        --  Needs a refactor or something at some point.
        declare
            function N is new Make_Fresh (Outputs (7));
        begin
            Outputs (7) := Disjunct
               (Outputs (7).Unify (Base_Term, Build (3)),
                Outputs (7).Unify (Base_Term, T (N, T (N, T (N, N)))));
        end;
        LT_Length (Outputs (7), Base_Term & Power_Term);
        declare
            BaseW1_Var   : constant Term := Outputs (7).Fresh;
            BaseW_Var    : constant Term := Outputs (7).Fresh;
            PowerW_Var   : constant Term := Outputs (7).Fresh;
            PowerW1_Var  : constant Term := Outputs (7).Fresh;
            Exp_Low1_Var : constant Term := Outputs (7).Fresh;
            Exp_Low_Var  : constant Term := Outputs (7).Fresh;
            S_Var        : constant Term := Outputs (7).Fresh;

            Exp1_Var       : constant Term := Outputs (7).Fresh;
            BaseW_Exp1_Var : constant Term := Outputs (7).Fresh;

            Base_Exp_Low_Var : constant Term := Outputs (7).Fresh;
            Exp_High_Var     : constant Term := Outputs (7).Fresh;
            S2_Var           : constant Term := Outputs (7).Fresh;
            ExpD_High_Var    : constant Term := Outputs (7).Fresh;
            ExpD_Var         : constant Term := Outputs (7).Fresh;

            Base_ExpD_Var : constant Term := Outputs (7).Fresh;
            Base_Exp1_Var : constant Term := Outputs (7).Fresh;
            Base_Exp_Var  : constant Term := Outputs (7).Fresh;
        begin
            Outputs (7).Conjunct (Exp_Two_Access, Base_Term & Zero_Term & BaseW1_Var);
            Add (Outputs (7), BaseW1_Var & One_Term & BaseW_Var);
            LT_Length (Outputs (7), Exponent_Term & Power_Term);

            Add (Outputs (7), Exponent_Term & One_Term & Exp1_Var);
            Multiply (Outputs (7), BaseW_Var & Exp1_Var & BaseW_Exp1_Var);
            LT (Outputs (7), PowerW1_Var & BaseW_Exp1_Var);

            Outputs (7).Conjunct (Exp_Two_Access, Power_Term & Zero_Term & PowerW1_Var);
            Add (Outputs (7), PowerW1_Var & One_Term & PowerW_Var);
            Divide (Outputs (7), PowerW_Var & BaseW_Var & Exp_Low1_Var & S_Var);
            Add (Outputs (7), Exp_Low_Var & One_Term & Exp_Low1_Var);
            Outputs (7) := Disjunct
               (Outputs (7).Unify (Exponent_Term, Exp_Low_Var),
                LT_Length (Outputs (7), Exp_Low_Var & Exponent_Term));

            Outputs (7).Conjunct (Repeated_Multiply_Access,
                Base_Term & Exp_Low_Var & Base_Exp_Low_Var);
            Divide (Outputs (7), PowerW_Var & BaseW1_Var & Exp_High_Var & S2_Var);
            Add (Outputs (7), Exp_Low_Var & ExpD_High_Var & Exp_High_Var);
            Add (Outputs (7), Exp_Low_Var & ExpD_Var & Exponent_Term);
            Outputs (7) := Disjunct
               (Outputs (7).Unify (ExpD_Var, ExpD_High_Var),
                LT (Outputs (7), ExpD_Var & ExpD_High_Var));

            Outputs (7).Conjunct (Repeated_Multiply_Access,
                Base_Term & ExpD_Var & Base_ExpD_Var);
            Multiply (Outputs (7), Base_Exp_Low_Var & Base_ExpD_Var & Base_Exp_Var);
            Multiply (Outputs (7), Base_Term & Base_Exp_Var & Base_Exp1_Var);
            Add (Outputs (7), Base_Exp_Var & Remainder_Term & Power_Term);
            LT (Outputs (7), Power_Term & Base_Exp1_Var);
        end;
        return Disjunct (Outputs);
    end Logarithm;


    procedure Logarithm
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := Logarithm (This, Inputs);
    end Logarithm;



    --  exp2  --

    function Exp_Two
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    is
        Power_Term    : Term renames Inputs (1);
        Base_Term     : Term renames Inputs (2);
        Exponent_Term : Term renames Inputs (3);

        One, Two, Three, Four : Goal := This;
    begin
        One.Unify (Power_Term, One_Term);
        One.Unify (Exponent_Term, Zero_Term);

        GT_One (Two, Power_Term);
        Two.Unify (Exponent_Term, One_Term);
        Two.Conjunct (Split_Access, Power_Term & Base_Term & Two.Fresh & One_Term);

        declare
            Exp1_Var  : constant Term := Three.Fresh;
            Base2_Var : constant Term := Three.Fresh;
        begin
            Three.Unify (Exponent_Term, T (T (Zero_Element), Exp1_Var));
            GT_Zero (Three, Exp1_Var);
            LT_Length (Three, Base_Term & Power_Term);
            Three.Append (Base_Term & T (T (One_Element), Base_Term) & Base2_Var);
            Three.Conjunct (Exp_Two_Access, Power_Term & Base2_Var & Exp1_Var);
        end;

        declare
            Exp1_Var       : constant Term := Four.Fresh;
            Power_High_Var : constant Term := Four.Fresh;
            Base2_Var      : constant Term := Four.Fresh;
            S_Var          : constant Term := Four.Fresh;
        begin
            Four.Unify (Exponent_Term, T (T (One_Element), Exp1_Var));
            GT_Zero (Four, Exp1_Var);
            GT_Zero (Four, Power_High_Var);
            Four.Conjunct (Split_Access, Power_Term & Base_Term & S_Var & Power_High_Var);
            Four.Append (Base_Term & T (T (One_Element), Base_Term) & Base2_Var);
            Four.Conjunct (Exp_Two_Access, Power_High_Var & Base2_Var & Exp1_Var);
        end;

        return Disjunct (One & Two & Three & Four);
    end Exp_Two;


    procedure Exp_Two
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := Exp_Two (This, Inputs);
    end Exp_Two;



    --  expo  --

    function Exponential
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    is
    begin
        return Logarithm (This, Inputs (3) & Inputs (1) & Inputs (2) & Zero_Term);
    end Exponential;


    procedure Exponential
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := Exponential (This, Inputs);
    end Exponential;



    --  repeated-mul  --

    function Repeated_Multiply
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    is
        Base_Term     : Term renames Inputs (1);
        Exponent_Term : Term renames Inputs (2);
        Power_Term    : Term renames Inputs (3);

        One, Two, Three : Goal := This;

        New_Exponent    : constant Term := Three.Fresh;
        Partial_Product : constant Term := Three.Fresh;
    begin
        GT_Zero (One, Base_Term);
        One.Unify (Exponent_Term, Zero_Term);
        One.Unify (Power_Term, One_Term);

        Two.Unify (Exponent_Term, One_Term);
        Two.Unify (Base_Term, Power_Term);

        GT_One (Three, Exponent_Term);
        Subtract (Three, Exponent_Term & One_Term & New_Exponent);
        Three.Conjunct (Repeated_Multiply_Access, Base_Term & New_Exponent & Partial_Product);
        Multiply (Three, Partial_Product & Base_Term & Power_Term);

        return Disjunct (One & Two & Three);
    end Repeated_Multiply;


    procedure Repeated_Multiply
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := Repeated_Multiply (This, Inputs);
    end Repeated_Multiply;


end Kompsos.Math;