diff options
Diffstat (limited to 'src/kompsos-math.adb')
| -rw-r--r-- | src/kompsos-math.adb | 46 |
1 files changed, 46 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; |
