Multiply and arithmetic comparison operators

1 files changed, 130 insertions, 17 deletions

diff --git a/src/kompsos-arithmetic.ads b/src/kompsos-arithmetic.ads
index 85071cc..661dadf 100644
--- a/src/kompsos-arithmetic.ads
+++ b/src/kompsos-arithmetic.ads
@@ -34,6 +34,8 @@ package Kompsos.Arithmetic is
 
     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;
@@ -97,14 +99,14 @@ package Kompsos.Arithmetic is
 
 
     --  +o  --
-    --  Inputs = N_Term & M_Term & Result_Term
+    --  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 & Result_Term
+    --  Inputs = N_Term & M_Term & Sum_Term
     procedure Add
            (This   : in out Goal;
             Inputs : in     Term_Array)
@@ -112,20 +114,110 @@ package Kompsos.Arithmetic is
 
 
     --  -o  --
-    --  Inputs = N_Term & M_Term & Result_Term
+    --  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 & Result_Term
+    --  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
 
 
@@ -137,47 +229,68 @@ private
     --  addero  --
     --  The carry-in input is a raw Zero_Element or One_Element.
 
-    --  Inputs = Cin_Term & N_Term & M_Term & Result_Term
+    --  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 & Result_Term
+    --  Inputs = Cin_Term & N_Term & M_Term & Sum_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
+    --  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 & Result_Term
+    --  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;
 
-    --  This is needed for dumb reasons.
-    General_Adder_Access : constant access function
+
+
+    --  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 := General_Adder'Access;
+        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.Arithmetic;