diff options
Diffstat (limited to 'src/kompsos-math.ads')
| -rw-r--r-- | src/kompsos-math.ads | 177 |
1 files changed, 123 insertions, 54 deletions
diff --git a/src/kompsos-math.ads b/src/kompsos-math.ads index d082f09..a223fcb 100644 --- a/src/kompsos-math.ads +++ b/src/kompsos-math.ads @@ -53,27 +53,9 @@ package Kompsos.Math is ------------------ - -- Operations -- + -- Comparison -- ------------------ - -- full-addero -- - -- Note the inputs here are all just the raw Zero_Element and One_Element, - -- not the proper numbers constructed by Build. - - -- Inputs = Cin_Term & A_Term & B_Term & Sum_Term & Cout_Term - function Full_Adder - (This : in Goal; - Inputs : in Term_Array) - return Goal - with Pre => Inputs'Length = 5; - - -- Inputs = Cin_Term & A_Term & B_Term & Sum_Term & Cout_Term - procedure Full_Adder - (This : in out Goal; - Inputs : in Term_Array) - with Pre => Inputs'Length = 5; - - -- poso -- function GT_Zero @@ -98,49 +80,34 @@ package Kompsos.Math is Num_Term : in Term'Class); - -- +o -- - -- 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 & Sum_Term - procedure Add - (This : in out Goal; - Inputs : in Term_Array) - with Pre => Inputs'Length = 3; - - - -- -o -- - -- Inputs = N_Term & M_Term & Difference_Term - function Subtract + -- <lo -- + -- Inputs = N_Term & M_Term + function LT_Length (This : in Goal; Inputs : in Term_Array) return Goal - with Pre => Inputs'Length = 3; + with Pre => Inputs'Length = 2; - -- Inputs = N_Term & M_Term & Difference_Term - procedure Subtract + -- Inputs = N_Term & M_Term + procedure LT_Length (This : in out Goal; Inputs : in Term_Array) - with Pre => Inputs'Length = 3; + with Pre => Inputs'Length = 2; - -- *o -- - -- Inputs = N_Term & M_Term & Product_Term - function Multiply + -- <=lo -- + -- Inputs = N_Term & M_Term + function LTE_Length (This : in Goal; Inputs : in Term_Array) return Goal - with Pre => Inputs'Length = 3; + with Pre => Inputs'Length = 2; - -- Inputs = N_Term & M_Term & Product_Term - procedure Multiply + -- Inputs = N_Term & M_Term + procedure LTE_Length (This : in out Goal; Inputs : in Term_Array) - with Pre => Inputs'Length = 3; + with Pre => Inputs'Length = 2; -- =lo -- @@ -158,31 +125,31 @@ package Kompsos.Math is with Pre => Inputs'Length = 2; - -- <lo -- + -- (extra function) -- -- Inputs = N_Term & M_Term - function LT_Length + function GTE_Length (This : in Goal; Inputs : in Term_Array) return Goal with Pre => Inputs'Length = 2; -- Inputs = N_Term & M_Term - procedure LT_Length + procedure GTE_Length (This : in out Goal; Inputs : in Term_Array) with Pre => Inputs'Length = 2; - -- <=lo -- + -- (extra function) -- -- Inputs = N_Term & M_Term - function LTE_Length + function GT_Length (This : in Goal; Inputs : in Term_Array) return Goal with Pre => Inputs'Length = 2; -- Inputs = N_Term & M_Term - procedure LTE_Length + procedure GT_Length (This : in out Goal; Inputs : in Term_Array) with Pre => Inputs'Length = 2; @@ -218,6 +185,108 @@ package Kompsos.Math is with Pre => Inputs'Length = 2; + -- Use Unify to assert two Terms must represent the same value. + + + -- (extra function) -- + -- Inputs = N_Term & M_Term + function GTE + (This : in Goal; + Inputs : in Term_Array) + return Goal + with Pre => Inputs'Length = 2; + + -- Inputs = N_Term & M_Term + procedure GTE + (This : in out Goal; + Inputs : in Term_Array) + with Pre => Inputs'Length = 2; + + + -- (extra function) -- + -- Inputs = N_Term & M_Term + function GT + (This : in Goal; + Inputs : in Term_Array) + return Goal + with Pre => Inputs'Length = 2; + + -- Inputs = N_Term & M_Term + procedure GT + (This : in out Goal; + Inputs : in Term_Array) + with Pre => Inputs'Length = 2; + + + + + ------------------ + -- Arithmetic -- + ------------------ + + -- full-addero -- + -- Note the inputs here are all just the raw Zero_Element and One_Element, + -- not the proper numbers constructed by Build. + + -- Inputs = Cin_Term & A_Term & B_Term & Sum_Term & Cout_Term + function Full_Adder + (This : in Goal; + Inputs : in Term_Array) + return Goal + with Pre => Inputs'Length = 5; + + -- Inputs = Cin_Term & A_Term & B_Term & Sum_Term & Cout_Term + procedure Full_Adder + (This : in out Goal; + Inputs : in Term_Array) + with Pre => Inputs'Length = 5; + + + -- +o -- + -- 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 & Sum_Term + procedure Add + (This : in out Goal; + Inputs : in Term_Array) + with Pre => Inputs'Length = 3; + + + -- -o -- + -- 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 & 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; + + private |