diff options
Diffstat (limited to 'src/kompsos-arithmetic.ads')
| -rw-r--r-- | src/kompsos-arithmetic.ads | 147 |
1 files changed, 130 insertions, 17 deletions
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; |