Addition and subtraction arithmeticHEADmaster

2 files changed, 506 insertions, 0 deletions

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;
+
+