From 17ead46c29ff1f852d4a05326e0286bb018c291a Mon Sep 17 00:00:00 2001 From: Jedidiah Barber Date: Sun, 21 Dec 2025 21:08:34 +1300 Subject: Addition and subtraction arithmetic --- src/kompsos-arithmetic.adb | 321 +++++++++++++++++++++++++++++++++++++++++++++ src/kompsos-arithmetic.ads | 185 ++++++++++++++++++++++++++ 2 files changed, 506 insertions(+) create mode 100644 src/kompsos-arithmetic.adb create mode 100644 src/kompsos-arithmetic.ads diff --git a/src/kompsos-arithmetic.adb b/src/kompsos-arithmetic.adb new file mode 100644 index 0000000..a9e2c14 --- /dev/null +++ b/src/kompsos-arithmetic.adb @@ -0,0 +1,321 @@ + + +-- Programmed by Jedidiah Barber +-- Licensed under the Sunset License v1.0 + +-- See license.txt for further details + + +package body Kompsos.Arithmetic is + + + --------------- + -- Numbers -- + --------------- + + function Is_Number + (Item : in Term) + return Boolean is + begin + if Item.Kind = Null_Term then + return True; + elsif Item.Kind = Pair_Term and then Item.Left.Kind = Atom_Term then + if Item.Right.Kind = Null_Term then + return Item.Left.Atom = One_Element; + else + return (Item.Left.Atom = Zero_Element or else Item.Left.Atom = One_Element) and then + Is_Number (Item.Right); + end if; + else + return False; + end if; + end Is_Number; + + + function Build + (Value : in Natural) + return Term is + begin + if Value = 0 then + return Empty_Term; + elsif Value mod 2 = 0 then + return T (T (Zero_Element), Build (Value / 2)); + else + return T (T (One_Element), Build ((Value - 1) / 2)); + end if; + end Build; + + + function Value + (Item : in Term) + return Natural is + begin + if Item.Kind = Null_Term then + return 0; + elsif Item.Left.Atom = Zero_Element then + return 2 * Value (Item.Right); + else + return 1 + 2 * Value (Item.Right); + end if; + end Value; + + + + + ------------------ + -- Operations -- + ------------------ + + -- full-addero -- + + function Full_Adder + (This : in Goal; + Inputs : in Term_Array) + return Goal + is + Cin_Term : Term renames Inputs (1); + A_Term : Term renames Inputs (2); + B_Term : Term renames Inputs (3); + Sum_Term : Term renames Inputs (4); + Cout_Term : Term renames Inputs (5); + + Outputs : Goal_Array := (1 .. 8 => This); + begin + Outputs (1).Unify (Cin_Term, Zero_Element); Outputs (2).Unify (Cin_Term, One_Element); + Outputs (1).Unify (A_Term, Zero_Element); Outputs (2).Unify (A_Term, Zero_Element); + Outputs (1).Unify (B_Term, Zero_Element); Outputs (2).Unify (B_Term, Zero_Element); + Outputs (1).Unify (Sum_Term, Zero_Element); Outputs (2).Unify (Sum_Term, One_Element); + Outputs (1).Unify (Cout_Term, Zero_Element); Outputs (2).Unify (Cout_Term, Zero_Element); + + Outputs (3).Unify (Cin_Term, Zero_Element); Outputs (4).Unify (Cin_Term, One_Element); + Outputs (3).Unify (A_Term, One_Element); Outputs (4).Unify (A_Term, One_Element); + Outputs (3).Unify (B_Term, Zero_Element); Outputs (4).Unify (B_Term, Zero_Element); + Outputs (3).Unify (Sum_Term, One_Element); Outputs (4).Unify (Sum_Term, Zero_Element); + Outputs (3).Unify (Cout_Term, Zero_Element); Outputs (4).Unify (Cout_Term, One_Element); + + Outputs (5).Unify (Cin_Term, Zero_Element); Outputs (6).Unify (Cin_Term, One_Element); + Outputs (5).Unify (A_Term, Zero_Element); Outputs (6).Unify (A_Term, Zero_Element); + Outputs (5).Unify (B_Term, One_Element); Outputs (6).Unify (B_Term, One_Element); + Outputs (5).Unify (Sum_Term, One_Element); Outputs (6).Unify (Sum_Term, Zero_Element); + Outputs (5).Unify (Cout_Term, Zero_Element); Outputs (6).Unify (Cout_Term, One_Element); + + Outputs (7).Unify (Cin_Term, Zero_Element); Outputs (8).Unify (Cin_Term, One_Element); + Outputs (7).Unify (A_Term, One_Element); Outputs (8).Unify (A_Term, One_Element); + Outputs (7).Unify (B_Term, One_Element); Outputs (8).Unify (B_Term, One_Element); + Outputs (7).Unify (Sum_Term, Zero_Element); Outputs (8).Unify (Sum_Term, One_Element); + Outputs (7).Unify (Cout_Term, One_Element); Outputs (8).Unify (Cout_Term, One_Element); + + return Disjunct (Outputs); + end Full_Adder; + + + procedure Full_Adder + (This : in out Goal; + Inputs : in Term_Array) is + begin + This := Full_Adder (This, Inputs); + end Full_Adder; + + + + -- poso -- + + function GT_Zero + (This : in Goal; + Num_Term : in Term'Class) + return Goal is + begin + return This.Pair (Num_Term); + end GT_Zero; + + + procedure GT_Zero + (This : in out Goal; + Num_Term : in Term'Class) is + begin + This := GT_Zero (This, Num_Term); + end GT_Zero; + + + + -- >1o -- + + function GT_One + (This : in Goal; + Num_Term : in Term'Class) + return Goal + is + Result : Goal := This; + Ref_Term : constant Term := Result.Fresh; + begin + Result.Tail (Num_Term & Ref_Term); + Result.Pair (Ref_Term); + return Result; + end GT_One; + + + procedure GT_One + (This : in out Goal; + Num_Term : in Term'Class) is + begin + This := GT_One (This, Num_Term); + end GT_One; + + + + -- addero -- + + function Adder + (This : in Goal; + 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); + + 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 (2).Unify (Cin_Term, Zero_Element); + Outputs (2).Unify (N_Term, Zero_Term); + Outputs (2).Unify (M_Term, Result_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 (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 (5).Unify (N_Term, One_Term); + Outputs (5).Unify (M_Term, One_Term); + declare + 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); + Full_Adder (Outputs (5), Cin_Term & T (One_Element) & T (One_Element) & A_Var & C_Var); + end; + + Outputs (6).Unify (N_Term, One_Term); + GT_One (Outputs (6), M_Term); + Outputs (6).Conjunct (General_Adder_Access, Inputs); + + 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 (8), N_Term); + GT_One (Outputs (8), M_Term); + Outputs (8).Conjunct (General_Adder_Access, Inputs); + + return Disjunct (Outputs); + end Adder; + + + procedure Adder + (This : in out Goal; + Inputs : in Term_Array) is + begin + This := Adder (This, Inputs); + end Adder; + + + + -- gen-addero -- + + function General_Adder + (This : in Goal; + 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); + + Result : Goal := This; + + A_Var : constant Term := Result.Fresh; + B_Var : constant Term := Result.Fresh; + C_Var : constant Term := Result.Fresh; + D_Var : constant Term := Result.Fresh; + X_Var : constant Term := Result.Fresh; + Y_Var : constant Term := Result.Fresh; + Z_Var : constant Term := Result.Fresh; + begin + 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); + 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); + return Result; + end General_Adder; + + + procedure General_Adder + (This : in out Goal; + Inputs : in Term_Array) is + begin + This := General_Adder (This, Inputs); + end General_Adder; + + + + -- +o -- + + function Add + (This : in Goal; + Inputs : in Term_Array) + return Goal is + begin + return Adder (This, T (Zero_Element) & Inputs); + end Add; + + + procedure Add + (This : in out Goal; + Inputs : in Term_Array) is + begin + This := Add (This, Inputs); + end Add; + + + + -- -o -- + + function Subtract + (This : in Goal; + 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); + begin + return Add (This, M_Term & Result_Term & N_Term); + end Subtract; + + + procedure Subtract + (This : in out Goal; + Inputs : in Term_Array) is + begin + This := Subtract (This, Inputs); + end Subtract; + + +end Kompsos.Arithmetic; + + diff --git a/src/kompsos-arithmetic.ads b/src/kompsos-arithmetic.ads new file mode 100644 index 0000000..85071cc --- /dev/null +++ b/src/kompsos-arithmetic.ads @@ -0,0 +1,185 @@ + + +-- 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; + + 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 & Result_Term + function Add + (This : in Goal; + Inputs : in Term_Array) + return Goal + with Pre => Inputs'Length = 3; + + -- Inputs = N_Term & M_Term & Result_Term + procedure Add + (This : in out Goal; + Inputs : in Term_Array) + with Pre => Inputs'Length = 3; + + + -- -o -- + -- Inputs = N_Term & M_Term & Result_Term + function Subtract + (This : in Goal; + Inputs : in Term_Array) + return Goal + with Pre => Inputs'Length = 3; + + -- Inputs = N_Term & M_Term & Result_Term + procedure Subtract + (This : in out Goal; + Inputs : in Term_Array) + with Pre => Inputs'Length = 3; + + +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 & Result_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 + 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 + 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 + 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 + (This : in Goal; + Inputs : in Term_Array) + return Goal := General_Adder'Access; + + +end Kompsos.Arithmetic; + + -- cgit