From b539ee5bf314bb4ed5df92ada1e0319fefc647ec Mon Sep 17 00:00:00 2001
From: Jedidiah Barber <contact@jedbarber.id.au>
Date: Thu, 25 Dec 2025 22:00:14 +1300
Subject: Reorganisation and additional numeric comparison subprograms

---
 src/kompsos-math.adb | 511 ++++++++++++++++++++++++++++++---------------------
 1 file changed, 298 insertions(+), 213 deletions(-)

(limited to 'src/kompsos-math.adb')

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