diff options
Diffstat (limited to 'src/kompsos-arithmetic.ads')
| -rw-r--r-- | src/kompsos-arithmetic.ads | 298 |
1 files changed, 0 insertions, 298 deletions
diff --git a/src/kompsos-arithmetic.ads b/src/kompsos-arithmetic.ads deleted file mode 100644 index 661dadf..0000000 --- a/src/kompsos-arithmetic.ads +++ /dev/null @@ -1,298 +0,0 @@ - - --- Programmed by Jedidiah Barber --- Licensed under the Sunset License v1.0 - --- See license.txt for further details - - -generic - Zero_Element, One_Element : in Element_Type; -package Kompsos.Arithmetic is - - - --------------- - -- Numbers -- - --------------- - - -- Valid number Terms are little endian binary lists - -- representing non-negative integers. - - -- The last digit in a non-empty list must always be - -- the One_Element. - - -- 0 -> () - -- 1 -> (1) - -- 2 -> (0 1) - -- 3 -> (1 1) - -- 4 -> (0 0 1) - -- 5 -> (1 0 1) - -- 6 -> (0 1 1) - -- 7 -> (1 1 1) - -- 8 -> (0 0 0 1) - -- ...and so forth. - - 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; - - function Build - (Value : in Natural) - return Term; - - function Value - (Item : in Term) - return Natural - with Pre => Is_Number (Item); - - - - - ------------------ - -- Operations -- - ------------------ - - -- 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 - (This : in Goal; - Num_Term : in Term'Class) - return Goal; - - procedure GT_Zero - (This : in out Goal; - Num_Term : in Term'Class); - - - -- >1o -- - - function GT_One - (This : in Goal; - Num_Term : in Term'Class) - return Goal; - - procedure GT_One - (This : in out Goal; - 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 - (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; - - - -- =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 - - - Zero_Term : constant Term := Build (0); - One_Term : constant Term := Build (1); - - - - -- addero -- - -- The carry-in input is a raw Zero_Element or One_Element. - - -- 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 & Sum_Term - procedure Adder - (This : in out Goal; - Inputs : in Term_Array) - with Pre => Inputs'Length = 4; - - - -- gen-addero -- - -- The carry-in input is a raw Zero_Element or One_Element. - - -- 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 & Sum_Term - procedure General_Adder - (This : in out Goal; - Inputs : in Term_Array) - with Pre => Inputs'Length = 4; - - - - -- 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 - 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; - - |