Reorganisation and additional numeric comparison subprograms

1 files changed, 123 insertions, 54 deletions

diff --git a/src/kompsos-math.ads b/src/kompsos-math.ads
index d082f09..a223fcb 100644
--- a/src/kompsos-math.ads
+++ b/src/kompsos-math.ads
@@ -53,27 +53,9 @@ package Kompsos.Math is
 
 
     ------------------
-    --  Operations  --
+    --  Comparison  --
     ------------------
 
-    --  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
@@ -98,49 +80,34 @@ package Kompsos.Math is
             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
+    --  <lo  --
+    --  Inputs = N_Term & M_Term
+    function LT_Length
            (This   : in Goal;
             Inputs : in Term_Array)
         return Goal
-    with Pre => Inputs'Length = 3;
+    with Pre => Inputs'Length = 2;
 
-    --  Inputs = N_Term & M_Term & Difference_Term
-    procedure Subtract
+    --  Inputs = N_Term & M_Term
+    procedure LT_Length
            (This   : in out Goal;
             Inputs : in     Term_Array)
-    with Pre => Inputs'Length = 3;
+    with Pre => Inputs'Length = 2;
 
 
-    --  *o  --
-    --  Inputs = N_Term & M_Term & Product_Term
-    function Multiply
+    --  <=lo  --
+    --  Inputs = N_Term & M_Term
+    function LTE_Length
            (This   : in Goal;
             Inputs : in Term_Array)
         return Goal
-    with Pre => Inputs'Length = 3;
+    with Pre => Inputs'Length = 2;
 
-    --  Inputs = N_Term & M_Term & Product_Term
-    procedure Multiply
+    --  Inputs = N_Term & M_Term
+    procedure LTE_Length
            (This   : in out Goal;
             Inputs : in     Term_Array)
-    with Pre => Inputs'Length = 3;
+    with Pre => Inputs'Length = 2;
 
 
     --  =lo  --
@@ -158,31 +125,31 @@ package Kompsos.Math is
     with Pre => Inputs'Length = 2;
 
 
-    --  <lo  --
+    --  (extra function)  --
     --  Inputs = N_Term & M_Term
-    function LT_Length
+    function GTE_Length
            (This   : in Goal;
             Inputs : in Term_Array)
         return Goal
     with Pre => Inputs'Length = 2;
 
     --  Inputs = N_Term & M_Term
-    procedure LT_Length
+    procedure GTE_Length
            (This   : in out Goal;
             Inputs : in     Term_Array)
     with Pre => Inputs'Length = 2;
 
 
-    --  <=lo  --
+    --  (extra function)  --
     --  Inputs = N_Term & M_Term
-    function LTE_Length
+    function GT_Length
            (This   : in Goal;
             Inputs : in Term_Array)
         return Goal
     with Pre => Inputs'Length = 2;
 
     --  Inputs = N_Term & M_Term
-    procedure LTE_Length
+    procedure GT_Length
            (This   : in out Goal;
             Inputs : in     Term_Array)
     with Pre => Inputs'Length = 2;
@@ -218,6 +185,108 @@ package Kompsos.Math is
     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;
+
+
 private