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

--  See license.txt for further details


generic
    Zero_Element, One_Element : in Element_Type;
package Kompsos.Math is


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

    --  Valid number Terms are little endian binary lists
    --  representing non-negative integers.

    --  The last digit in a non-empty list must always be
    --  the One_Element.

    --  0 -> ()
    --  1 -> (1)
    --  2 -> (0 1)
    --  3 -> (1 1)
    --  4 -> (0 0 1)
    --  5 -> (1 0 1)
    --  6 -> (0 1 1)
    --  7 -> (1 1 1)
    --  8 -> (0 0 0 1)
    --  ...and so forth.

    Zero_Term, One_Term : constant Term;

    --  Will only return True for number literals, not for variables.
    --  If you want to check a variable Term then you must reify it first.
    function Is_Number
           (Item : in Term)
        return Boolean;

    function Build
           (Value : in Natural)
        return Term;

    function Value
           (Item : in Term)
        return Natural
    with Pre => Is_Number (Item);




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

    --  poso  --

    function GT_Zero
           (This     : in Goal;
            Num_Term : in Term'Class)
        return Goal;

    procedure GT_Zero
           (This     : in out Goal;
            Num_Term : in     Term'Class);


    --  >1o  --

    function GT_One
           (This     : in Goal;
            Num_Term : in Term'Class)
        return Goal;

    procedure GT_One
           (This     : in out Goal;
            Num_Term : in     Term'Class);


    --  <lo  --
    --  Inputs = N_Term & M_Term
    function LT_Length
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    with Pre => Inputs'Length = 2;

    --  Inputs = N_Term & M_Term
    procedure LT_Length
           (This   : in out Goal;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 2;


    --  <=lo  --
    --  Inputs = N_Term & M_Term
    function LTE_Length
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    with Pre => Inputs'Length = 2;

    --  Inputs = N_Term & M_Term
    procedure LTE_Length
           (This   : in out Goal;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 2;


    --  =lo  --
    --  Inputs = N_Term & M_Term
    function EQ_Length
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    with Pre => Inputs'Length = 2;

    --  Inputs = N_Term & M_Term
    procedure EQ_Length
           (This   : in out Goal;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 2;


    --  (extra function)  --
    --  Inputs = N_Term & M_Term
    function GTE_Length
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    with Pre => Inputs'Length = 2;

    --  Inputs = N_Term & M_Term
    procedure GTE_Length
           (This   : in out Goal;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 2;


    --  (extra function)  --
    --  Inputs = N_Term & M_Term
    function GT_Length
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    with Pre => Inputs'Length = 2;

    --  Inputs = N_Term & M_Term
    procedure GT_Length
           (This   : in out Goal;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 2;


    --  <o  --
    --  Inputs = N_Term & M_Term
    function LT
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    with Pre => Inputs'Length = 2;

    --  Inputs = N_Term & M_Term
    procedure LT
           (This   : in out Goal;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 2;


    --  <=o  --
    --  Inputs = N_Term & M_Term
    function LTE
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    with Pre => Inputs'Length = 2;

    --  Inputs = N_Term & M_Term
    procedure LTE
           (This   : in out Goal;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 2;


    --  Use Unify to assert two Terms must represent the same value.


    --  (extra function)  --
    --  Inputs = N_Term & M_Term
    function GTE
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    with Pre => Inputs'Length = 2;

    --  Inputs = N_Term & M_Term
    procedure GTE
           (This   : in out Goal;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 2;


    --  (extra function)  --
    --  Inputs = N_Term & M_Term
    function GT
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    with Pre => Inputs'Length = 2;

    --  Inputs = N_Term & M_Term
    procedure GT
           (This   : in out Goal;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 2;




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

    --  full-addero  --
    --  Note the inputs here are all just the raw Zero_Element and One_Element,
    --  not the proper numbers constructed by Build.

    --  Inputs = Cin_Term & A_Term & B_Term & Sum_Term & Cout_Term
    function Full_Adder
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    with Pre => Inputs'Length = 5;

    --  Inputs = Cin_Term & A_Term & B_Term & Sum_Term & Cout_Term
    procedure Full_Adder
           (This   : in out Goal;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 5;


    --  +o  --
    --  Inputs = N_Term & M_Term & Sum_Term
    function Add
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    with Pre => Inputs'Length = 3;

    --  Inputs = N_Term & M_Term & Sum_Term
    procedure Add
           (This   : in out Goal;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 3;


    --  -o  --
    --  Inputs = N_Term & M_Term & Difference_Term
    function Subtract
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    with Pre => Inputs'Length = 3;

    --  Inputs = N_Term & M_Term & Difference_Term
    procedure Subtract
           (This   : in out Goal;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 3;


    --  *o  --
    --  Inputs = N_Term & M_Term & Product_Term
    function Multiply
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    with Pre => Inputs'Length = 3;

    --  Inputs = N_Term & M_Term & Product_Term
    procedure Multiply
           (This   : in out Goal;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 3;


    --  /o  --
    --  Inputs = N_Term & M_Term & Quotient_Term & Remainder_Term
    function Divide
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    with Pre => Inputs'Length = 4;

    --  Inputs = N_Term & M_Term & Quotient_Term & Remainder_Term
    procedure Divide
           (This   : in out Goal;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 4;


    --  logo  --
    --  Finds solutions to
    --      Base^Exponent + Remainder = Power
    --  or rather
    --      log_Base (Power - Remainder) = Exponent

    --  Inputs = Power_Term & Base_Term & Exponent_Term & Remainder_Term
    function Logarithm
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    with Pre => Inputs'Length = 4;

    --  Inputs = Power_Term & Base_Term & Exponent_Term & Remainder_Term
    procedure Logarithm
           (This   : in out Goal;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 4;


    --  expo  --
    --  Inputs = Base_Term & Exponent_Term & Power_Term
    function Exponential
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    with Pre => Inputs'Length = 3;

    --  Inputs = Base_Term & Exponent_Term & Power_Term
    procedure Exponential
           (This   : in out Goal;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 3;


    --  repeated-mul  --
    --  Inputs = Base_Term & Exponent_Term & Power_Term
    function Repeated_Multiply
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    with Pre => Inputs'Length = 3;

    --  Inputs = Base_Term & Exponent_Term & Power_Term
    procedure Repeated_Multiply
           (This   : in out Goal;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 3;


private


    Zero_Term : constant Term := Empty_Term;
    One_Term  : constant Term := T (T (One_Element), Empty_Term);



    --  addero  --
    --  The carry-in input is a raw Zero_Element or One_Element.

    --  Inputs = Cin_Term & N_Term & M_Term & Sum_Term
    function Adder
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    with Pre => Inputs'Length = 4;

    --  Inputs = Cin_Term & N_Term & M_Term & Sum_Term
    procedure Adder
           (This   : in out Goal;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 4;


    --  gen-addero  --
    --  The carry-in input is a raw Zero_Element or One_Element.

    --  Inputs = Cin_Term & N_Term & M_Term & Sum_Term
    function General_Adder
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    with Pre => Inputs'Length = 4;

    --  Inputs = Cin_Term & N_Term & M_Term & Sum_Term
    procedure General_Adder
           (This   : in out Goal;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 4;



    --  odd-*o  --
    --  (What is the X_Term...?)
    --  Inputs = X_Term & N_Term & M_Term & Product_Term
    function Odd_Multiply
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    with Pre => Inputs'Length = 4;

    --  Inputs = X_Term & N_Term & M_Term & Product_Term
    procedure Odd_Multiply
           (This   : in out Goal;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 4;


    --  bound-*o  --
    --  (What is the Q_Term...?)
    --  Inputs = Q_Term & Product_Term & N_Term & M_Term
    function Bounded_Multiply
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    with Pre => Inputs'Length = 4;

    --  Inputs = Q_Term & Product_Term & N_Term & M_Term
    procedure Bounded_Multiply
           (This   : in out Goal;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 4;



    --  splito  --
    --  Inputs = N_Term & Remainder_Term & Low_Term & High_Term
    function Split
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    with Pre => Inputs'Length = 4;

    --  Inputs = N_Term & Remainder_Term & Low_Term & High_Term
    procedure Split
           (This   : in out Goal;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 4;



    --  exp2  --
    --  Inputs = Power_Term & Base_Term & Exponent_Term
    function Exp_Two
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    with Pre => Inputs'Length = 3;

    --  Inputs = Power_Term & Base_Term & Exponent_Term
    procedure Exp_Two
           (This   : in out Goal;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 3;


end Kompsos.Math;