Division, logarithm, exponentiation

1 files changed, 377 insertions, 4 deletions

diff --git a/src/kompsos-math.adb b/src/kompsos-math.adb
index 8de7c9f..2c2ddf8 100644
--- a/src/kompsos-math.adb
+++ b/src/kompsos-math.adb
@@ -53,6 +53,21 @@ package body Kompsos.Math is
             Inputs : in Term_Array)
         return Goal := Bounded_Multiply'Access;
 
+    Divide_Access : constant access function
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal := Divide'Access;
+
+    Split_Access : constant access function
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal := Split'Access;
+
+    Exp_Two_Access : constant access function
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal := Exp_Two'Access;
+
     Repeated_Multiply_Access : constant access function
            (This   : in Goal;
             Inputs : in Term_Array)
@@ -765,6 +780,364 @@ package body Kompsos.Math is
 
 
 
+    --  /o  --
+
+    function Divide
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal
+    is
+        N_Term         : Term renames Inputs (1);
+        M_Term         : Term renames Inputs (2);
+        Quotient_Term  : Term renames Inputs (3);
+        Remainder_Term : Term renames Inputs (4);
+
+        One, Two, Three : Goal := This;
+
+        N_Low             : constant Term := Three.Fresh;
+        N_High            : constant Term := Three.Fresh;
+        Quot_Low          : constant Term := Three.Fresh;
+        Quot_High         : constant Term := Three.Fresh;
+        Quot_Low_M        : constant Term := Three.Fresh;
+        Quot_Low_M_Remain : constant Term := Three.Fresh;
+        Remain_Remain     : constant Term := Three.Fresh;
+        Remain_High       : constant Term := Three.Fresh;
+    begin
+        One.Unify (N_Term, Remainder_Term);
+        One.Unify (Quotient_Term, Zero_Term);
+        LT (One, N_Term & M_Term);
+
+        Two.Unify (Quotient_Term, One_Term);
+        EQ_Length (Two, N_Term & M_Term);
+        Add (Two, Remainder_Term & M_Term & N_Term);
+        LT (Two, Remainder_Term & M_Term);
+
+        LT_Length (Three, M_Term & N_Term);
+        LT (Three, Remainder_Term & M_Term);
+        GT_Zero (Three, Quotient_Term);
+        Three.Conjunct (Split_Access, N_Term & Remainder_Term & N_Low & N_High);
+        Three.Conjunct (Split_Access, Quotient_Term & Remainder_Term & Quot_Low & Quot_High);
+        declare
+            Three_A, Three_B : Goal := Three;
+        begin
+            Three_A.Unify (N_High, Zero_Term);
+            Three_A.Unify (Quot_High, Zero_Term);
+            Subtract (Three_A, N_Low & Remainder_Term & Quot_Low_M);
+            Multiply (Three_A, Quot_Low & M_Term & Quot_Low_M);
+
+            GT_Zero (Three_B, N_High);
+            Multiply (Three_B, Quot_Low & M_Term & Quot_Low_M);
+            Add (Three_B, Quot_Low_M & Remainder_Term & Quot_Low_M_Remain);
+            Subtract (Three_B, Quot_Low_M_Remain & N_Low & Remain_Remain);
+            Three_B.Conjunct (Split_Access,
+                Remain_Remain & Remainder_Term & Zero_Term & Remain_High);
+            Three_B.Conjunct (Divide_Access, N_High & M_Term & Quot_High & Remain_High);
+
+            return Disjunct (One & Two & Three_A & Three_B);
+        end;
+    end Divide;
+
+
+    procedure Divide
+           (This   : in out Goal;
+            Inputs : in     Term_Array) is
+    begin
+        This := Divide (This, Inputs);
+    end Divide;
+
+
+
+    --  splito  --
+
+    function Split
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal
+    is
+        N_Term         : Term renames Inputs (1);
+        Remainder_Term : Term renames Inputs (2);
+        Low_Term       : Term renames Inputs (3);
+        High_Term      : Term renames Inputs (4);
+
+        Outputs : Goal_Array := (1 .. 6 => This);
+    begin
+        Outputs (1).Unify (N_Term, Zero_Term);
+        Outputs (1).Unify (High_Term, Zero_Term);
+        Outputs (1).Unify (Low_Term, Zero_Term);
+
+        declare
+            B_Var : constant Term := Outputs (2).Fresh;
+            N_Hat : constant Term := Outputs (2).Fresh;
+        begin
+            Outputs (2).Unify (N_Term, T (T (Zero_Element), T (B_Var, N_Hat)));
+            Outputs (2).Unify (Remainder_Term, Zero_Term);
+            Outputs (2).Unify (High_Term, T (B_Var, N_Hat));
+            Outputs (2).Unify (Low_Term, Zero_Term);
+        end;
+
+        declare
+            N_Hat : constant Term := Outputs (3).Fresh;
+        begin
+            Outputs (3).Unify (N_Term, T (T (One_Element), N_Hat));
+            Outputs (3).Unify (Remainder_Term, Zero_Term);
+            Outputs (3).Unify (High_Term, N_Hat);
+            Outputs (3).Unify (Low_Term, One_Term);
+        end;
+
+        declare
+            B_Var : constant Term := Outputs (4).Fresh;
+            N_Hat : constant Term := Outputs (4).Fresh;
+            A_Var : constant Term := Outputs (4).Fresh;
+            R_Hat : constant Term := Outputs (4).Fresh;
+        begin
+            Outputs (4).Unify (N_Term, T (T (Zero_Element), T (B_Var, N_Hat)));
+            Outputs (4).Unify (Remainder_Term, T (A_Var, R_Hat));
+            Outputs (4).Unify (Low_Term, Zero_Term);
+            Outputs (4).Conjunct (Split_Access, T (B_Var, N_Hat) & R_Hat & Zero_Term & High_Term);
+        end;
+
+        declare
+            N_Hat : constant Term := Outputs (5).Fresh;
+            A_Var : constant Term := Outputs (5).Fresh;
+            R_Hat : constant Term := Outputs (5).Fresh;
+        begin
+            Outputs (5).Unify (N_Term, T (T (One_Element), N_Hat));
+            Outputs (5).Unify (Remainder_Term, T (A_Var, R_Hat));
+            Outputs (5).Unify (Low_Term, One_Term);
+            Outputs (5).Conjunct (Split_Access, N_Hat & R_Hat & Zero_Term & High_Term);
+        end;
+
+        declare
+            B_Var : constant Term := Outputs (6).Fresh;
+            N_Hat : constant Term := Outputs (6).Fresh;
+            A_Var : constant Term := Outputs (6).Fresh;
+            R_Hat : constant Term := Outputs (6).Fresh;
+            L_Hat : constant Term := Outputs (6).Fresh;
+        begin
+            Outputs (6).Unify (N_Term, T (B_Var, N_Hat));
+            Outputs (6).Unify (Remainder_Term, T (A_Var, R_Hat));
+            Outputs (6).Unify (Low_Term, T (B_Var, L_Hat));
+            GT_Zero (Outputs (6), L_Hat);
+            Outputs (6).Conjunct (Split_Access, N_Hat & R_Hat & L_Hat & High_Term);
+        end;
+
+        return Disjunct (Outputs);
+    end Split;
+
+
+    procedure Split
+           (This   : in out Goal;
+            Inputs : in     Term_Array) is
+    begin
+        This := Split (This, Inputs);
+    end Split;
+
+
+
+    --  logo  --
+
+    function Logarithm
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal
+    is
+        Power_Term     : Term renames Inputs (1);
+        Base_Term      : Term renames Inputs (2);
+        Exponent_Term  : Term renames Inputs (3);
+        Remainder_Term : Term renames Inputs (4);
+
+        Outputs : Goal_Array := (1 .. 7 => This);
+    begin
+        Outputs (1).Unify (Power_Term, One_Term);
+        GT_Zero (Outputs (1), Base_Term);
+        Outputs (1).Unify (Exponent_Term, Zero_Term);
+        Outputs (1).Unify (Remainder_Term, Zero_Term);
+
+        Outputs (2).Unify (Exponent_Term, Zero_Term);
+        LT (Outputs (2), Power_Term & Base_Term);
+        Add (Outputs (2), Remainder_Term & One_Term & Power_Term);
+
+        Outputs (3).Unify (Exponent_Term, One_Term);
+        GT_One (Outputs (3), Base_Term);
+        EQ_Length (Outputs (3), Power_Term & Base_Term);
+        Add (Outputs (3), Remainder_Term & Base_Term & Power_Term);
+
+        Outputs (4).Unify (Base_Term, One_Term);
+        GT_Zero (Outputs (4), Exponent_Term);
+        Add (Outputs (4), Remainder_Term & One_Term & Power_Term);
+
+        Outputs (5).Unify (Base_Term, Zero_Term);
+        GT_Zero (Outputs (5), Exponent_Term);
+        Outputs (5).Unify (Remainder_Term, Power_Term);
+
+        Outputs (6).Unify (Base_Term, Build (2));
+        declare
+            DD_Var : constant Term := Outputs (6).Fresh;
+        begin
+            GT_Zero (Outputs (6), DD_Var);
+            Outputs (6).Unify (Power_Term, T (Outputs (6).Fresh, T (Outputs (6).Fresh, DD_Var)));
+            Outputs (6).Conjunct (Exp_Two_Access, Power_Term & Zero_Term & Exponent_Term);
+            Outputs (6).Conjunct (Split_Access,
+                Power_Term & DD_Var & Remainder_Term & Outputs (6).Fresh);
+        end;
+
+        --  I know what you're thinking. Clear as mud, right?
+        --  Well unfortunately the original miniKanren Scheme isn't really any better.
+        --  Needs a refactor or something at some point.
+        declare
+            function N is new Make_Fresh (Outputs (7));
+        begin
+            Outputs (7) := Disjunct
+               (Outputs (7).Unify (Base_Term, Build (3)),
+                Outputs (7).Unify (Base_Term, T (N, T (N, T (N, N)))));
+        end;
+        LT_Length (Outputs (7), Base_Term & Power_Term);
+        declare
+            BaseW1_Var   : constant Term := Outputs (7).Fresh;
+            BaseW_Var    : constant Term := Outputs (7).Fresh;
+            PowerW_Var   : constant Term := Outputs (7).Fresh;
+            PowerW1_Var  : constant Term := Outputs (7).Fresh;
+            Exp_Low1_Var : constant Term := Outputs (7).Fresh;
+            Exp_Low_Var  : constant Term := Outputs (7).Fresh;
+            S_Var        : constant Term := Outputs (7).Fresh;
+
+            Exp1_Var       : constant Term := Outputs (7).Fresh;
+            BaseW_Exp1_Var : constant Term := Outputs (7).Fresh;
+
+            Base_Exp_Low_Var : constant Term := Outputs (7).Fresh;
+            Exp_High_Var     : constant Term := Outputs (7).Fresh;
+            S2_Var           : constant Term := Outputs (7).Fresh;
+            ExpD_High_Var    : constant Term := Outputs (7).Fresh;
+            ExpD_Var         : constant Term := Outputs (7).Fresh;
+
+            Base_ExpD_Var : constant Term := Outputs (7).Fresh;
+            Base_Exp1_Var : constant Term := Outputs (7).Fresh;
+            Base_Exp_Var  : constant Term := Outputs (7).Fresh;
+        begin
+            Outputs (7).Conjunct (Exp_Two_Access, Base_Term & Zero_Term & BaseW1_Var);
+            Add (Outputs (7), BaseW1_Var & One_Term & BaseW_Var);
+            LT_Length (Outputs (7), Exponent_Term & Power_Term);
+
+            Add (Outputs (7), Exponent_Term & One_Term & Exp1_Var);
+            Multiply (Outputs (7), BaseW_Var & Exp1_Var & BaseW_Exp1_Var);
+            LT (Outputs (7), PowerW1_Var & BaseW_Exp1_Var);
+
+            Outputs (7).Conjunct (Exp_Two_Access, Power_Term & Zero_Term & PowerW1_Var);
+            Add (Outputs (7), PowerW1_Var & One_Term & PowerW_Var);
+            Divide (Outputs (7), PowerW_Var & BaseW_Var & Exp_Low1_Var & S_Var);
+            Add (Outputs (7), Exp_Low_Var & One_Term & Exp_Low1_Var);
+            Outputs (7) := Disjunct
+               (Outputs (7).Unify (Exponent_Term, Exp_Low_Var),
+                LT_Length (Outputs (7), Exp_Low_Var & Exponent_Term));
+
+            Outputs (7).Conjunct (Repeated_Multiply_Access,
+                Base_Term & Exp_Low_Var & Base_Exp_Low_Var);
+            Divide (Outputs (7), PowerW_Var & BaseW1_Var & Exp_High_Var & S2_Var);
+            Add (Outputs (7), Exp_Low_Var & ExpD_High_Var & Exp_High_Var);
+            Add (Outputs (7), Exp_Low_Var & ExpD_Var & Exponent_Term);
+            Outputs (7) := Disjunct
+               (Outputs (7).Unify (ExpD_Var, ExpD_High_Var),
+                LT (Outputs (7), ExpD_Var & ExpD_High_Var));
+
+            Outputs (7).Conjunct (Repeated_Multiply_Access,
+                Base_Term & ExpD_Var & Base_ExpD_Var);
+            Multiply (Outputs (7), Base_Exp_Low_Var & Base_ExpD_Var & Base_Exp_Var);
+            Multiply (Outputs (7), Base_Term & Base_Exp_Var & Base_Exp1_Var);
+            Add (Outputs (7), Base_Exp_Var & Remainder_Term & Power_Term);
+            LT (Outputs (7), Power_Term & Base_Exp1_Var);
+        end;
+        return Disjunct (Outputs);
+    end Logarithm;
+
+
+    procedure Logarithm
+           (This   : in out Goal;
+            Inputs : in     Term_Array) is
+    begin
+        This := Logarithm (This, Inputs);
+    end Logarithm;
+
+
+
+    --  exp2  --
+
+    function Exp_Two
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal
+    is
+        Power_Term    : Term renames Inputs (1);
+        Base_Term     : Term renames Inputs (2);
+        Exponent_Term : Term renames Inputs (3);
+
+        One, Two, Three, Four : Goal := This;
+    begin
+        One.Unify (Power_Term, One_Term);
+        One.Unify (Exponent_Term, Zero_Term);
+
+        GT_One (Two, Power_Term);
+        Two.Unify (Exponent_Term, One_Term);
+        Two.Conjunct (Split_Access, Power_Term & Base_Term & Two.Fresh & One_Term);
+
+        declare
+            Exp1_Var  : constant Term := Three.Fresh;
+            Base2_Var : constant Term := Three.Fresh;
+        begin
+            Three.Unify (Exponent_Term, T (T (Zero_Element), Exp1_Var));
+            GT_Zero (Three, Exp1_Var);
+            LT_Length (Three, Base_Term & Power_Term);
+            Three.Append (Base_Term & T (T (One_Element), Base_Term) & Base2_Var);
+            Three.Conjunct (Exp_Two_Access, Power_Term & Base2_Var & Exp1_Var);
+        end;
+
+        declare
+            Exp1_Var       : constant Term := Four.Fresh;
+            Power_High_Var : constant Term := Four.Fresh;
+            Base2_Var      : constant Term := Four.Fresh;
+            S_Var          : constant Term := Four.Fresh;
+        begin
+            Four.Unify (Exponent_Term, T (T (One_Element), Exp1_Var));
+            GT_Zero (Four, Exp1_Var);
+            GT_Zero (Four, Power_High_Var);
+            Four.Conjunct (Split_Access, Power_Term & Base_Term & S_Var & Power_High_Var);
+            Four.Append (Base_Term & T (T (One_Element), Base_Term) & Base2_Var);
+            Four.Conjunct (Exp_Two_Access, Power_High_Var & Base2_Var & Exp1_Var);
+        end;
+
+        return Disjunct (One & Two & Three & Four);
+    end Exp_Two;
+
+
+    procedure Exp_Two
+           (This   : in out Goal;
+            Inputs : in     Term_Array) is
+    begin
+        This := Exp_Two (This, Inputs);
+    end Exp_Two;
+
+
+
+    --  expo  --
+
+    function Exponential
+           (This   : in Goal;
+            Inputs : in Term_Array)
+        return Goal
+    is
+    begin
+        return Logarithm (This, Inputs (3) & Inputs (1) & Inputs (2) & Zero_Term);
+    end Exponential;
+
+
+    procedure Exponential
+           (This   : in out Goal;
+            Inputs : in     Term_Array) is
+    begin
+        This := Exponential (This, Inputs);
+    end Exponential;
+
+
+
     --  repeated-mul  --
 
     function Repeated_Multiply
@@ -774,7 +1147,7 @@ package body Kompsos.Math is
     is
         Base_Term     : Term renames Inputs (1);
         Exponent_Term : Term renames Inputs (2);
-        Product_Term  : Term renames Inputs (3);
+        Power_Term    : Term renames Inputs (3);
 
         One, Two, Three : Goal := This;
 
@@ -783,15 +1156,15 @@ package body Kompsos.Math is
     begin
         GT_Zero (One, Base_Term);
         One.Unify (Exponent_Term, Zero_Term);
-        One.Unify (Product_Term, One_Term);
+        One.Unify (Power_Term, One_Term);
 
         Two.Unify (Exponent_Term, One_Term);
-        Two.Unify (Base_Term, Product_Term);
+        Two.Unify (Base_Term, Power_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);
+        Multiply (Three, Partial_Product & Base_Term & Power_Term);
 
         return Disjunct (One & Two & Three);
     end Repeated_Multiply;