Arithmetic -> Math package rename

1 files changed, 298 insertions, 0 deletions

diff --git a/src/kompsos-math.ads b/src/kompsos-math.ads
new file mode 100644
index 0000000..d082f09
--- /dev/null
+++ b/src/kompsos-math.ads
@@ -0,0 +1,298 @@
+
+
+--  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);
+
+
+
+
+    ------------------
+    --  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 & 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;
+
+
+    --  =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;
+
+
+    --  <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;
+
+
+    --  <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;
+
+
+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 & 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;
+
+
+end Kompsos.Math;
+
+