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

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




    ------------------
    --  Operations  --
    ------------------

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


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


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

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


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

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


private


    Zero_Term : constant Term := Build (0);
    One_Term  : constant Term := Build (1);



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

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

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

    --  This is needed for dumb reasons.
    Adder_Access : constant access function
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal := Adder'Access;


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

    --  Inputs = Cin_Term & N_Term & M_Term & Result_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 & Result_Term
    procedure General_Adder
           (This   : in out Goal;
            Inputs : in     Term_Array)
    with Pre => Inputs'Length = 4;

    --  This is needed for dumb reasons.
    General_Adder_Access : constant access function
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal := General_Adder'Access;


end Kompsos.Arithmetic;