Repeated multiply version of exponentiation

2 files changed, 61 insertions, 0 deletions

diff --git a/src/kompsos-math.adb b/src/kompsos-math.adb
index 7ea6310..8de7c9f 100644
--- a/src/kompsos-math.adb
+++ b/src/kompsos-math.adb
@@ -53,6 +53,11 @@ package body Kompsos.Math is
             Inputs : in Term_Array)
         return Goal := Bounded_Multiply'Access;
 
+    Repeated_Multiply_Access : constant access function
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal := Repeated_Multiply'Access;
+
 
 
 
@@ -759,6 +764,47 @@ package body Kompsos.Math is
     end Bounded_Multiply;
 
 
+
+    --  repeated-mul  --
+
+    function Repeated_Multiply
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal
+    is
+        Base_Term     : Term renames Inputs (1);
+        Exponent_Term : Term renames Inputs (2);
+        Product_Term  : Term renames Inputs (3);
+
+        One, Two, Three : Goal := This;
+
+        New_Exponent    : constant Term := Three.Fresh;
+        Partial_Product : constant Term := Three.Fresh;
+    begin
+        GT_Zero (One, Base_Term);
+        One.Unify (Exponent_Term, Zero_Term);
+        One.Unify (Product_Term, One_Term);
+
+        Two.Unify (Exponent_Term, One_Term);
+        Two.Unify (Base_Term, Product_Term);
+
+        GT_One (Three, Exponent_Term);
+        Subtract (Three, Exponent_Term & One_Term & New_Exponent);
+        Three.Conjunct (Repeated_Multiply_Access, Base_Term & New_Exponent & Partial_Product);
+        Multiply (Three, Partial_Product & Base_Term & Product_Term);
+
+        return Disjunct (One & Two & Three);
+    end Repeated_Multiply;
+
+
+    procedure Repeated_Multiply
+           (This   : in out Goal;
+            Inputs : in     Term_Array) is
+    begin
+        This := Repeated_Multiply (This, Inputs);
+    end Repeated_Multiply;
+
+
 end Kompsos.Math;
 
 
diff --git a/src/kompsos-math.ads b/src/kompsos-math.ads
index a223fcb..093acbf 100644
--- a/src/kompsos-math.ads
+++ b/src/kompsos-math.ads
@@ -287,6 +287,21 @@ package Kompsos.Math is
     with Pre => Inputs'Length = 3;
 
 
+    --  repeated-mul  --
+    --  Inputs = Base_Term & Exponent_Term & Product_Term
+    function Repeated_Multiply
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal
+    with Pre => Inputs'Length = 3;
+
+    --  Inputs = Base_Term & Exponent_Term & Product_Term
+    procedure Repeated_Multiply
+           (This   : in out Goal;
+            Inputs : in     Term_Array)
+    with Pre => Inputs'Length = 3;
+
+
 private