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