From 44bfd9d245f6ba53151b9a149e5ac0c7784ec141 Mon Sep 17 00:00:00 2001 From: Jedidiah Barber Date: Thu, 25 Dec 2025 21:09:53 +1300 Subject: Arithmetic -> Math package rename --- src/kompsos-math.ads | 298 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 298 insertions(+) create mode 100644 src/kompsos-math.ads (limited to 'src/kompsos-math.ads') diff --git a/src/kompsos-math.ads b/src/kompsos-math.ads new file mode 100644 index 0000000..d082f09 --- /dev/null +++ b/src/kompsos-math.ads @@ -0,0 +1,298 @@ + + +-- 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.Math 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; + + + -- 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; + + + -- 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.Math; + + -- cgit