Reorganisation and additional numeric comparison subprograms

2 files changed, 421 insertions, 267 deletions

diff --git a/src/kompsos-math.adb b/src/kompsos-math.adb
index b64d393..7ea6310 100644
--- a/src/kompsos-math.adb
+++ b/src/kompsos-math.adb
@@ -18,6 +18,16 @@ package body Kompsos.Math is
 
     --  Can't apply 'Unchecked_Access to a subprogram either, so we're doing this.
 
+    LT_Length_Access : constant access function
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal := LT_Length'Access;
+
+    EQ_Length_Access : constant access function
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal := EQ_Length'Access;
+
     Adder_Access : constant access function
            (This   : in Goal;
             Inputs : in Term_Array)
@@ -43,16 +53,6 @@ package body Kompsos.Math is
             Inputs : in Term_Array)
         return Goal := Bounded_Multiply'Access;
 
-    EQ_Length_Access : constant access function
-           (This   : in Goal;
-            Inputs : in Term_Array)
-        return Goal := EQ_Length'Access;
-
-    LT_Length_Access : constant access function
-           (This   : in Goal;
-            Inputs : in Term_Array)
-        return Goal := LT_Length'Access;
-
 
 
 
@@ -110,7 +110,294 @@ package body Kompsos.Math is
 
 
     ------------------
-    --  Operations  --
+    --  Comparison  --
+    ------------------
+
+    --  poso  --
+
+    function GT_Zero
+           (This     : in Goal;
+            Num_Term : in Term'Class)
+        return Goal is
+    begin
+        return This.Pair (Num_Term);
+    end GT_Zero;
+
+
+    procedure GT_Zero
+           (This     : in out Goal;
+            Num_Term : in     Term'Class) is
+    begin
+        This := GT_Zero (This, Num_Term);
+    end GT_Zero;
+
+
+
+    --  >1o  --
+
+    function GT_One
+           (This     : in Goal;
+            Num_Term : in Term'Class)
+        return Goal
+    is
+        Result : Goal := This;
+        Ref_Term : constant Term := Result.Fresh;
+    begin
+        Result.Tail (Num_Term & Ref_Term);
+        Result.Pair (Ref_Term);
+        return Result;
+    end GT_One;
+
+
+    procedure GT_One
+           (This     : in out Goal;
+            Num_Term : in     Term'Class) is
+    begin
+        This := GT_One (This, Num_Term);
+    end GT_One;
+
+
+
+    --  <lo  --
+
+    function LT_Length
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal
+    is
+        N_Term : Term renames Inputs (1);
+        M_Term : Term renames Inputs (2);
+
+        One, Two, Three : Goal := This;
+
+        X_Var : constant Term := Three.Fresh;
+        Y_Var : constant Term := Three.Fresh;
+    begin
+        One.Unify (N_Term, Zero_Term);
+        GT_Zero (One, M_Term);
+
+        Two.Unify (N_Term, One_Term);
+        GT_One (Two, M_Term);
+
+        Three.Unify (N_Term, T (Three.Fresh, X_Var));
+        GT_Zero (Three, X_Var);
+        Three.Unify (M_Term, T (Three.Fresh, Y_Var));
+        GT_Zero (Three, Y_Var);
+        Three.Conjunct (LT_Length_Access, X_Var & Y_Var);
+
+        return Disjunct (One & Two & Three);
+    end LT_Length;
+
+
+    procedure LT_Length
+           (This   : in out Goal;
+            Inputs : in     Term_Array) is
+    begin
+        This := LT_Length (This, Inputs);
+    end LT_Length;
+
+
+
+    --  <=lo  --
+
+    function LTE_Length
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal is
+    begin
+        return Disjunct
+           (EQ_Length (This, Inputs),
+            LT_Length (This, Inputs));
+    end LTE_Length;
+
+
+    procedure LTE_Length
+           (This   : in out Goal;
+            Inputs : in     Term_Array) is
+    begin
+        This := LTE_Length (This, Inputs);
+    end LTE_Length;
+
+
+
+    --  =lo  --
+
+    function EQ_Length
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal
+    is
+        N_Term : Term renames Inputs (1);
+        M_Term : Term renames Inputs (2);
+
+        One, Two, Three : Goal := This;
+
+        X_Var : constant Term := Three.Fresh;
+        Y_Var : constant Term := Three.Fresh;
+    begin
+        One.Unify (N_Term, Zero_Term);
+        One.Unify (M_Term, Zero_Term);
+
+        Two.Unify (N_Term, One_Term);
+        Two.Unify (M_Term, One_Term);
+
+        Three.Unify (N_Term, T (Three.Fresh, X_Var));
+        GT_Zero (Three, X_Var);
+        Three.Unify (M_Term, T (Three.Fresh, Y_Var));
+        GT_Zero (Three, Y_Var);
+        Three.Conjunct (EQ_Length_Access, X_Var & Y_Var);
+
+        return Disjunct (One & Two & Three);
+    end EQ_Length;
+
+
+    procedure EQ_Length
+           (This   : in out Goal;
+            Inputs : in     Term_Array) is
+    begin
+        This := EQ_Length (This, Inputs);
+    end EQ_Length;
+
+
+
+    --  (extra function)  --
+
+    function GTE_Length
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal is
+    begin
+        return LTE_Length (This, Inputs (2) & Inputs (1));
+    end GTE_Length;
+
+
+    procedure GTE_Length
+           (This   : in out Goal;
+            Inputs : in     Term_Array) is
+    begin
+        This := GTE_Length (This, Inputs);
+    end GTE_Length;
+
+
+
+    --  (extra function)  --
+
+    function GT_Length
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal is
+    begin
+        return LT_Length (This, Inputs (2) & Inputs (1));
+    end GT_Length;
+
+
+    procedure GT_Length
+           (This   : in out Goal;
+            Inputs : in     Term_Array) is
+    begin
+        This := GT_Length (This, Inputs);
+    end GT_Length;
+
+
+
+    --  <o  --
+
+    function LT
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal
+    is
+        N_Term : Term renames Inputs (1);
+        M_Term : Term renames Inputs (2);
+
+        One, Two : Goal := This;
+
+        X_Var : constant Term := Two.Fresh;
+    begin
+        LT_Length (One, Inputs);
+
+        EQ_Length (Two, Inputs);
+        GT_Zero (Two, X_Var);
+        Add (Two, N_Term & X_Var & M_Term);
+
+        return Disjunct (One, Two);
+    end LT;
+
+
+    procedure LT
+           (This   : in out Goal;
+            Inputs : in     Term_Array) is
+    begin
+        This := LT (This, Inputs);
+    end LT;
+
+
+
+    --  <=o  --
+
+    function LTE
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal is
+    begin
+        return Disjunct
+           (This.Unify (Inputs (1), Inputs (2)),
+            LT (This, Inputs));
+    end LTE;
+
+
+    procedure LTE
+           (This   : in out Goal;
+            Inputs : in     Term_Array) is
+    begin
+        This := LTE (This, Inputs);
+    end LTE;
+
+
+
+    --  (extra function)  --
+
+    function GTE
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal is
+    begin
+        return LTE (This, Inputs (2) & Inputs (1));
+    end GTE;
+
+
+    procedure GTE
+           (This   : in out Goal;
+            Inputs : in     Term_Array) is
+    begin
+        This := GTE (This, Inputs);
+    end GTE;
+
+
+
+    --  (extra function)  --
+
+    function GT
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal is
+    begin
+        return LT (This, Inputs (2) & Inputs (1));
+    end GT;
+
+
+    procedure GT
+           (This   : in out Goal;
+            Inputs : in     Term_Array) is
+    begin
+        This := GT (This, Inputs);
+    end GT;
+
+
+
+
+    ------------------
+    --  Arithmetic  --
     ------------------
 
     --  full-addero  --
@@ -165,51 +452,6 @@ package body Kompsos.Math is
 
 
 
-    --  poso  --
-
-    function GT_Zero
-           (This     : in Goal;
-            Num_Term : in Term'Class)
-        return Goal is
-    begin
-        return This.Pair (Num_Term);
-    end GT_Zero;
-
-
-    procedure GT_Zero
-           (This     : in out Goal;
-            Num_Term : in     Term'Class) is
-    begin
-        This := GT_Zero (This, Num_Term);
-    end GT_Zero;
-
-
-
-    --  >1o  --
-
-    function GT_One
-           (This     : in Goal;
-            Num_Term : in Term'Class)
-        return Goal
-    is
-        Result : Goal := This;
-        Ref_Term : constant Term := Result.Fresh;
-    begin
-        Result.Tail (Num_Term & Ref_Term);
-        Result.Pair (Ref_Term);
-        return Result;
-    end GT_One;
-
-
-    procedure GT_One
-           (This     : in out Goal;
-            Num_Term : in     Term'Class) is
-    begin
-        This := GT_One (This, Num_Term);
-    end GT_One;
-
-
-
     --  addero  --
 
     function Adder
@@ -517,163 +759,6 @@ package body Kompsos.Math is
     end Bounded_Multiply;
 
 
-
-    --  =lo  --
-
-    function EQ_Length
-           (This   : in Goal;
-            Inputs : in Term_Array)
-        return Goal
-    is
-        N_Term : Term renames Inputs (1);
-        M_Term : Term renames Inputs (2);
-
-        One, Two, Three : Goal := This;
-
-        X_Var : constant Term := Three.Fresh;
-        Y_Var : constant Term := Three.Fresh;
-    begin
-        One.Unify (N_Term, Zero_Term);
-        One.Unify (M_Term, Zero_Term);
-
-        Two.Unify (N_Term, One_Term);
-        Two.Unify (M_Term, One_Term);
-
-        Three.Unify (N_Term, T (Three.Fresh, X_Var));
-        GT_Zero (Three, X_Var);
-        Three.Unify (M_Term, T (Three.Fresh, Y_Var));
-        GT_Zero (Three, Y_Var);
-        Three.Conjunct (EQ_Length_Access, X_Var & Y_Var);
-
-        return Disjunct (One & Two & Three);
-    end EQ_Length;
-
-
-    procedure EQ_Length
-           (This   : in out Goal;
-            Inputs : in     Term_Array) is
-    begin
-        This := EQ_Length (This, Inputs);
-    end EQ_Length;
-
-
-
-    --  <lo  --
-
-    function LT_Length
-           (This   : in Goal;
-            Inputs : in Term_Array)
-        return Goal
-    is
-        N_Term : Term renames Inputs (1);
-        M_Term : Term renames Inputs (2);
-
-        One, Two, Three : Goal := This;
-
-        X_Var : constant Term := Three.Fresh;
-        Y_Var : constant Term := Three.Fresh;
-    begin
-        One.Unify (N_Term, Zero_Term);
-        GT_Zero (One, M_Term);
-
-        Two.Unify (N_Term, One_Term);
-        GT_One (Two, M_Term);
-
-        Three.Unify (N_Term, T (Three.Fresh, X_Var));
-        GT_Zero (Three, X_Var);
-        Three.Unify (M_Term, T (Three.Fresh, Y_Var));
-        GT_Zero (Three, Y_Var);
-        Three.Conjunct (LT_Length_Access, X_Var & Y_Var);
-
-        return Disjunct (One & Two & Three);
-    end LT_Length;
-
-
-    procedure LT_Length
-           (This   : in out Goal;
-            Inputs : in     Term_Array) is
-    begin
-        This := LT_Length (This, Inputs);
-    end LT_Length;
-
-
-
-    --  <=lo  --
-
-    function LTE_Length
-           (This   : in Goal;
-            Inputs : in Term_Array)
-        return Goal is
-    begin
-        return Disjunct
-           (EQ_Length (This, Inputs),
-            LT_Length (This, Inputs));
-    end LTE_Length;
-
-
-    procedure LTE_Length
-           (This   : in out Goal;
-            Inputs : in     Term_Array) is
-    begin
-        This := LTE_Length (This, Inputs);
-    end LTE_Length;
-
-
-
-    --  <o  --
-
-    function LT
-           (This   : in Goal;
-            Inputs : in Term_Array)
-        return Goal
-    is
-        N_Term : Term renames Inputs (1);
-        M_Term : Term renames Inputs (2);
-
-        One, Two : Goal := This;
-
-        X_Var : constant Term := Two.Fresh;
-    begin
-        LT_Length (One, Inputs);
-
-        EQ_Length (Two, Inputs);
-        GT_Zero (Two, X_Var);
-        Add (Two, N_Term & X_Var & M_Term);
-
-        return Disjunct (One, Two);
-    end LT;
-
-
-    procedure LT
-           (This   : in out Goal;
-            Inputs : in     Term_Array) is
-    begin
-        This := LT (This, Inputs);
-    end LT;
-
-
-
-    --  <=o  --
-
-    function LTE
-           (This   : in Goal;
-            Inputs : in Term_Array)
-        return Goal is
-    begin
-        return Disjunct
-           (This.Unify (Inputs (1), Inputs (2)),
-            LT (This, Inputs));
-    end LTE;
-
-
-    procedure LTE
-           (This   : in out Goal;
-            Inputs : in     Term_Array) is
-    begin
-        This := LTE (This, Inputs);
-    end LTE;
-
-
 end Kompsos.Math;
 
 
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