From 17ead46c29ff1f852d4a05326e0286bb018c291a Mon Sep 17 00:00:00 2001
From: Jedidiah Barber <contact@jedbarber.id.au>
Date: Sun, 21 Dec 2025 21:08:34 +1300
Subject: Addition and subtraction arithmetic

---
 src/kompsos-arithmetic.ads | 185 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 185 insertions(+)
 create mode 100644 src/kompsos-arithmetic.ads

(limited to 'src/kompsos-arithmetic.ads')

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