Multiply and arithmetic comparison operators

2 files changed, 508 insertions, 37 deletions

diff --git a/src/kompsos-arithmetic.adb b/src/kompsos-arithmetic.adb
index a9e2c14..9d02a5a 100644
--- a/src/kompsos-arithmetic.adb
+++ b/src/kompsos-arithmetic.adb
@@ -9,6 +9,53 @@
 package body Kompsos.Arithmetic is
 
 
+    ----------------
+    --  Accesses  --
+    ----------------
+
+    --  These are needed for some really dumb reason about not allowing 'Access
+    --  in a generic body when the access type is declared outside the generic.
+
+    --  Can't apply 'Unchecked_Access to a subprogram either, so we're doing this.
+
+    Adder_Access : constant access function
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal := Adder'Access;
+
+    General_Adder_Access : constant access function
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal := General_Adder'Access;
+
+    Multiply_Access : constant access function
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal := Multiply'Access;
+
+    Odd_Multiply_Access : constant access function
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal := Odd_Multiply'Access;
+
+    Bounded_Multiply_Access : constant access function
+           (This   : in Goal;
+            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;
+
+
+
+
     ---------------
     --  Numbers  --
     ---------------
@@ -170,30 +217,30 @@ package body Kompsos.Arithmetic is
             Inputs : in Term_Array)
         return Goal
     is
-        Cin_Term    : Term renames Inputs (1);
-        N_Term      : Term renames Inputs (2);
-        M_Term      : Term renames Inputs (3);
-        Result_Term : Term renames Inputs (4);
+        Cin_Term : Term renames Inputs (1);
+        N_Term   : Term renames Inputs (2);
+        M_Term   : Term renames Inputs (3);
+        Sum_Term : Term renames Inputs (4);
 
         Outputs : Goal_Array := (1 .. 8 => This);
     begin
         Outputs (1).Unify (Cin_Term, Zero_Element);
         Outputs (1).Unify (M_Term, Zero_Term);
-        Outputs (1).Unify (N_Term, Result_Term);
+        Outputs (1).Unify (N_Term, Sum_Term);
 
         Outputs (2).Unify (Cin_Term, Zero_Element);
         Outputs (2).Unify (N_Term, Zero_Term);
-        Outputs (2).Unify (M_Term, Result_Term);
+        Outputs (2).Unify (M_Term, Sum_Term);
         GT_Zero (Outputs (2), M_Term);
 
         Outputs (3).Unify (Cin_Term, One_Element);
         Outputs (3).Unify (M_Term, Zero_Term);
-        Outputs (3).Conjunct (Adder_Access, T (Zero_Element) & N_Term & One_Term & Result_Term);
+        Outputs (3).Conjunct (Adder_Access, T (Zero_Element) & N_Term & One_Term & Sum_Term);
 
         Outputs (4).Unify (Cin_Term, One_Element);
         Outputs (4).Unify (N_Term, Zero_Term);
         GT_Zero (Outputs (4), M_Term);
-        Outputs (4).Conjunct (Adder_Access, T (Zero_Element) & One_Term & M_Term & Result_Term);
+        Outputs (4).Conjunct (Adder_Access, T (Zero_Element) & One_Term & M_Term & Sum_Term);
 
         Outputs (5).Unify (N_Term, One_Term);
         Outputs (5).Unify (M_Term, One_Term);
@@ -201,7 +248,7 @@ package body Kompsos.Arithmetic is
             A_Var : constant Term := Outputs (5).Fresh;
             C_Var : constant Term := Outputs (5).Fresh;
         begin
-            Outputs (5).Unify (T (A_Var, C_Var), Result_Term);
+            Outputs (5).Unify (T (A_Var, C_Var), Sum_Term);
             Full_Adder (Outputs (5), Cin_Term & T (One_Element) & T (One_Element) & A_Var & C_Var);
         end;
 
@@ -211,8 +258,8 @@ package body Kompsos.Arithmetic is
 
         Outputs (7).Unify (M_Term, One_Term);
         GT_One (Outputs (7), N_Term);
-        GT_One (Outputs (7), Result_Term);
-        Outputs (7).Conjunct (Adder_Access, Cin_Term & One_Term & N_Term & Result_Term);
+        GT_One (Outputs (7), Sum_Term);
+        Outputs (7).Conjunct (Adder_Access, Cin_Term & One_Term & N_Term & Sum_Term);
 
         GT_One (Outputs (8), N_Term);
         GT_One (Outputs (8), M_Term);
@@ -238,10 +285,10 @@ package body Kompsos.Arithmetic is
             Inputs : in Term_Array)
         return Goal
     is
-        Cin_Term    : Term renames Inputs (1);
-        N_Term      : Term renames Inputs (2);
-        M_Term      : Term renames Inputs (3);
-        Result_Term : Term renames Inputs (4);
+        Cin_Term : Term renames Inputs (1);
+        N_Term   : Term renames Inputs (2);
+        M_Term   : Term renames Inputs (3);
+        Sum_Term : Term renames Inputs (4);
 
         Result : Goal := This;
 
@@ -256,7 +303,7 @@ package body Kompsos.Arithmetic is
         Result.Unify (T (A_Var, X_Var), N_Term);
         Result.Unify (T (B_Var, Y_Var), M_Term);
         GT_Zero (Result, Y_Var);
-        Result.Unify (T (C_Var, Z_Var), Result_Term);
+        Result.Unify (T (C_Var, Z_Var), Sum_Term);
         GT_Zero (Result, Z_Var);
         Full_Adder (Result, Cin_Term & A_Var & B_Var & C_Var & D_Var);
         Result.Conjunct (Adder_Access, D_Var & X_Var & Y_Var & Z_Var);
@@ -300,11 +347,11 @@ package body Kompsos.Arithmetic is
             Inputs : in Term_Array)
         return Goal
     is
-        N_Term      : Term renames Inputs (1);
-        M_Term      : Term renames Inputs (2);
-        Result_Term : Term renames Inputs (3);
+        N_Term          : Term renames Inputs (1);
+        M_Term          : Term renames Inputs (2);
+        Difference_Term : Term renames Inputs (3);
     begin
-        return Add (This, M_Term & Result_Term & N_Term);
+        return Add (This, M_Term & Difference_Term & N_Term);
     end Subtract;
 
 
@@ -316,6 +363,317 @@ package body Kompsos.Arithmetic is
     end Subtract;
 
 
+
+    --  *o  --
+
+    function Multiply
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal
+    is
+        N_Term       : Term renames Inputs (1);
+        M_Term       : Term renames Inputs (2);
+        Product_Term : Term renames Inputs (3);
+
+        Outputs : Goal_Array := (1 .. 7 => This);
+    begin
+        Outputs (1).Unify (N_Term, Zero_Term);
+        Outputs (1).Unify (Product_Term, Zero_Term);
+
+        GT_Zero (Outputs (2), N_Term);
+        Outputs (2).Unify (M_Term, Zero_Term);
+        Outputs (2).Unify (Product_Term, Zero_Term);
+
+        Outputs (3).Unify (N_Term, One_Term);
+        GT_Zero (Outputs (3), M_Term);
+        Outputs (3).Unify (M_Term, Product_Term);
+
+        GT_One (Outputs (4), N_Term);
+        Outputs (4).Unify (M_Term, One_Term);
+        Outputs (4).Unify (N_Term, Product_Term);
+
+        declare
+            X_Var : constant Term := Outputs (5).Fresh;
+            Z_Var : constant Term := Outputs (5).Fresh;
+        begin
+            Outputs (5).Unify (T (T (Zero_Element), X_Var), N_Term);
+            GT_Zero (Outputs (5), X_Var);
+            Outputs (5).Unify (T (T (Zero_Element), Z_Var), Product_Term);
+            GT_Zero (Outputs (5), Z_Var);
+            GT_One (Outputs (5), M_Term);
+            Outputs (5).Conjunct (Multiply_Access, X_Var & M_Term & Z_Var);
+        end;
+
+        declare
+            X_Var : constant Term := Outputs (6).Fresh;
+            Y_Var : constant Term := Outputs (6).Fresh;
+        begin
+            Outputs (6).Unify (T (T (One_Element), X_Var), N_Term);
+            GT_Zero (Outputs (6), X_Var);
+            Outputs (6).Unify (T (T (Zero_Element), Y_Var), M_Term);
+            GT_Zero (Outputs (6), Y_Var);
+            Outputs (6).Conjunct (Multiply_Access, M_Term & N_Term & Product_Term);
+        end;
+
+        declare
+            X_Var : constant Term := Outputs (7).Fresh;
+            Y_Var : constant Term := Outputs (7).Fresh;
+        begin
+            Outputs (7).Unify (T (T (One_Element), X_Var), N_Term);
+            GT_Zero (Outputs (7), X_Var);
+            Outputs (7).Unify (T (T (One_Element), Y_Var), M_Term);
+            GT_Zero (Outputs (7), Y_Var);
+            Outputs (7).Conjunct (Odd_Multiply_Access, X_Var & N_Term & M_Term & Product_Term);
+        end;
+
+        return Disjunct (Outputs);
+    end Multiply;
+
+
+    procedure Multiply
+           (This   : in out Goal;
+            Inputs : in     Term_Array) is
+    begin
+        This := Multiply (This, Inputs);
+    end Multiply;
+
+
+
+    --  odd-*o  --
+
+    function Odd_Multiply
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal
+    is
+        X_Term       : Term renames Inputs (1);
+        N_Term       : Term renames Inputs (2);
+        M_Term       : Term renames Inputs (3);
+        Product_Term : Term renames Inputs (4);
+
+        Result : Goal := This;
+
+        Q_Var : constant Term := Result.Fresh;
+    begin
+        Bounded_Multiply (Result, Q_Var & Product_Term & N_Term & M_Term);
+        Multiply (Result, X_Term & M_Term & Q_Var);
+        Add (Result, T (T (Zero_Element), Q_Var) & M_Term & Product_Term);
+        return Result;
+    end Odd_Multiply;
+
+
+    procedure Odd_Multiply
+           (This   : in out Goal;
+            Inputs : in     Term_Array) is
+    begin
+        This := Odd_Multiply (This, Inputs);
+    end Odd_Multiply;
+
+
+
+    --  bound-*o  --
+
+    function Bounded_Multiply
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal
+    is
+        Q_Term       : Term renames Inputs (1);
+        Product_Term : Term renames Inputs (2);
+        N_Term       : Term renames Inputs (3);
+        M_Term       : Term renames Inputs (4);
+
+        One, Two : Goal := This;
+
+        X_Var : constant Term := Two.Fresh;
+        Y_Var : constant Term := Two.Fresh;
+        Z_Var : constant Term := Two.Fresh;
+    begin
+        One.Nil (Q_Term);
+        One.Pair (Product_Term);
+
+        Two.Tail (Q_Term & X_Var);
+        Two.Tail (Product_Term & Y_Var);
+        declare
+            Two_A, Two_B : Goal := Two;
+        begin
+            Two_A.Nil (N_Term);
+            Two_A.Tail (M_Term & Z_Var);
+            Two_A.Conjunct (Bounded_Multiply_Access, X_Var & Y_Var & Z_Var & Zero_Term);
+
+            Two_B.Tail (N_Term & Z_Var);
+            Two_B.Conjunct (Bounded_Multiply_Access, X_Var & Y_Var & Z_Var & M_Term);
+
+            return Disjunct (One & Two_A & Two_B);
+        end;
+    end Bounded_Multiply;
+
+
+    procedure Bounded_Multiply
+           (This   : in out Goal;
+            Inputs : in     Term_Array) is
+    begin
+        This := Bounded_Multiply (This, Inputs);
+    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.Arithmetic;
 
 
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;