Arithmetic -> Math package rename

1 files changed, 0 insertions, 679 deletions

diff --git a/src/kompsos-arithmetic.adb b/src/kompsos-arithmetic.adb
deleted file mode 100644
index 9d02a5a..0000000
--- a/src/kompsos-arithmetic.adb
+++ /dev/null
@@ -1,679 +0,0 @@
-
-
---  Programmed by Jedidiah Barber
---  Licensed under the Sunset License v1.0
-
---  See license.txt for further details
-
-
-package body Kompsos.Arithmetic is
-
-
-    ----------------
-    --  Accesses  --
-    ----------------
-
-    --  These are needed for some really dumb reason about not allowing 'Access
-    --  in a generic body when the access type is declared outside the generic.
-
-    --  Can't apply 'Unchecked_Access to a subprogram either, so we're doing this.
-
-    Adder_Access : constant access function
-           (This   : in Goal;
-            Inputs : in Term_Array)
-        return Goal := Adder'Access;
-
-    General_Adder_Access : constant access function
-           (This   : in Goal;
-            Inputs : in Term_Array)
-        return Goal := General_Adder'Access;
-
-    Multiply_Access : constant access function
-           (This   : in Goal;
-            Inputs : in Term_Array)
-        return Goal := Multiply'Access;
-
-    Odd_Multiply_Access : constant access function
-           (This   : in Goal;
-            Inputs : in Term_Array)
-        return Goal := Odd_Multiply'Access;
-
-    Bounded_Multiply_Access : constant access function
-           (This   : in Goal;
-            Inputs : in Term_Array)
-        return Goal := Bounded_Multiply'Access;
-
-    EQ_Length_Access : constant access function
-           (This   : in Goal;
-            Inputs : in Term_Array)
-        return Goal := EQ_Length'Access;
-
-    LT_Length_Access : constant access function
-           (This   : in Goal;
-            Inputs : in Term_Array)
-        return Goal := LT_Length'Access;
-
-
-
-
-    ---------------
-    --  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);
-        Sum_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, Sum_Term);
-
-        Outputs (2).Unify (Cin_Term, Zero_Element);
-        Outputs (2).Unify (N_Term, Zero_Term);
-        Outputs (2).Unify (M_Term, Sum_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 & Sum_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 & Sum_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), Sum_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), Sum_Term);
-        Outputs (7).Conjunct (Adder_Access, Cin_Term & One_Term & N_Term & Sum_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);
-        Sum_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), Sum_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);
-        Difference_Term : Term renames Inputs (3);
-    begin
-        return Add (This, M_Term & Difference_Term & N_Term);
-    end Subtract;
-
-
-    procedure Subtract
-           (This   : in out Goal;
-            Inputs : in     Term_Array) is
-    begin
-        This := Subtract (This, Inputs);
-    end Subtract;
-
-
-
-    --  *o  --
-
-    function Multiply
-           (This   : in Goal;
-            Inputs : in Term_Array)
-        return Goal
-    is
-        N_Term       : Term renames Inputs (1);
-        M_Term       : Term renames Inputs (2);
-        Product_Term : Term renames Inputs (3);
-
-        Outputs : Goal_Array := (1 .. 7 => This);
-    begin
-        Outputs (1).Unify (N_Term, Zero_Term);
-        Outputs (1).Unify (Product_Term, Zero_Term);
-
-        GT_Zero (Outputs (2), N_Term);
-        Outputs (2).Unify (M_Term, Zero_Term);
-        Outputs (2).Unify (Product_Term, Zero_Term);
-
-        Outputs (3).Unify (N_Term, One_Term);
-        GT_Zero (Outputs (3), M_Term);
-        Outputs (3).Unify (M_Term, Product_Term);
-
-        GT_One (Outputs (4), N_Term);
-        Outputs (4).Unify (M_Term, One_Term);
-        Outputs (4).Unify (N_Term, Product_Term);
-
-        declare
-            X_Var : constant Term := Outputs (5).Fresh;
-            Z_Var : constant Term := Outputs (5).Fresh;
-        begin
-            Outputs (5).Unify (T (T (Zero_Element), X_Var), N_Term);
-            GT_Zero (Outputs (5), X_Var);
-            Outputs (5).Unify (T (T (Zero_Element), Z_Var), Product_Term);
-            GT_Zero (Outputs (5), Z_Var);
-            GT_One (Outputs (5), M_Term);
-            Outputs (5).Conjunct (Multiply_Access, X_Var & M_Term & Z_Var);
-        end;
-
-        declare
-            X_Var : constant Term := Outputs (6).Fresh;
-            Y_Var : constant Term := Outputs (6).Fresh;
-        begin
-            Outputs (6).Unify (T (T (One_Element), X_Var), N_Term);
-            GT_Zero (Outputs (6), X_Var);
-            Outputs (6).Unify (T (T (Zero_Element), Y_Var), M_Term);
-            GT_Zero (Outputs (6), Y_Var);
-            Outputs (6).Conjunct (Multiply_Access, M_Term & N_Term & Product_Term);
-        end;
-
-        declare
-            X_Var : constant Term := Outputs (7).Fresh;
-            Y_Var : constant Term := Outputs (7).Fresh;
-        begin
-            Outputs (7).Unify (T (T (One_Element), X_Var), N_Term);
-            GT_Zero (Outputs (7), X_Var);
-            Outputs (7).Unify (T (T (One_Element), Y_Var), M_Term);
-            GT_Zero (Outputs (7), Y_Var);
-            Outputs (7).Conjunct (Odd_Multiply_Access, X_Var & N_Term & M_Term & Product_Term);
-        end;
-
-        return Disjunct (Outputs);
-    end Multiply;
-
-
-    procedure Multiply
-           (This   : in out Goal;
-            Inputs : in     Term_Array) is
-    begin
-        This := Multiply (This, Inputs);
-    end Multiply;
-
-
-
-    --  odd-*o  --
-
-    function Odd_Multiply
-           (This   : in Goal;
-            Inputs : in Term_Array)
-        return Goal
-    is
-        X_Term       : Term renames Inputs (1);
-        N_Term       : Term renames Inputs (2);
-        M_Term       : Term renames Inputs (3);
-        Product_Term : Term renames Inputs (4);
-
-        Result : Goal := This;
-
-        Q_Var : constant Term := Result.Fresh;
-    begin
-        Bounded_Multiply (Result, Q_Var & Product_Term & N_Term & M_Term);
-        Multiply (Result, X_Term & M_Term & Q_Var);
-        Add (Result, T (T (Zero_Element), Q_Var) & M_Term & Product_Term);
-        return Result;
-    end Odd_Multiply;
-
-
-    procedure Odd_Multiply
-           (This   : in out Goal;
-            Inputs : in     Term_Array) is
-    begin
-        This := Odd_Multiply (This, Inputs);
-    end Odd_Multiply;
-
-
-
-    --  bound-*o  --
-
-    function Bounded_Multiply
-           (This   : in Goal;
-            Inputs : in Term_Array)
-        return Goal
-    is
-        Q_Term       : Term renames Inputs (1);
-        Product_Term : Term renames Inputs (2);
-        N_Term       : Term renames Inputs (3);
-        M_Term       : Term renames Inputs (4);
-
-        One, Two : Goal := This;
-
-        X_Var : constant Term := Two.Fresh;
-        Y_Var : constant Term := Two.Fresh;
-        Z_Var : constant Term := Two.Fresh;
-    begin
-        One.Nil (Q_Term);
-        One.Pair (Product_Term);
-
-        Two.Tail (Q_Term & X_Var);
-        Two.Tail (Product_Term & Y_Var);
-        declare
-            Two_A, Two_B : Goal := Two;
-        begin
-            Two_A.Nil (N_Term);
-            Two_A.Tail (M_Term & Z_Var);
-            Two_A.Conjunct (Bounded_Multiply_Access, X_Var & Y_Var & Z_Var & Zero_Term);
-
-            Two_B.Tail (N_Term & Z_Var);
-            Two_B.Conjunct (Bounded_Multiply_Access, X_Var & Y_Var & Z_Var & M_Term);
-
-            return Disjunct (One & Two_A & Two_B);
-        end;
-    end Bounded_Multiply;
-
-
-    procedure Bounded_Multiply
-           (This   : in out Goal;
-            Inputs : in     Term_Array) is
-    begin
-        This := Bounded_Multiply (This, Inputs);
-    end Bounded_Multiply;
-
-
-
-    --  =lo  --
-
-    function EQ_Length
-           (This   : in Goal;
-            Inputs : in Term_Array)
-        return Goal
-    is
-        N_Term : Term renames Inputs (1);
-        M_Term : Term renames Inputs (2);
-
-        One, Two, Three : Goal := This;
-
-        X_Var : constant Term := Three.Fresh;
-        Y_Var : constant Term := Three.Fresh;
-    begin
-        One.Unify (N_Term, Zero_Term);
-        One.Unify (M_Term, Zero_Term);
-
-        Two.Unify (N_Term, One_Term);
-        Two.Unify (M_Term, One_Term);
-
-        Three.Unify (N_Term, T (Three.Fresh, X_Var));
-        GT_Zero (Three, X_Var);
-        Three.Unify (M_Term, T (Three.Fresh, Y_Var));
-        GT_Zero (Three, Y_Var);
-        Three.Conjunct (EQ_Length_Access, X_Var & Y_Var);
-
-        return Disjunct (One & Two & Three);
-    end EQ_Length;
-
-
-    procedure EQ_Length
-           (This   : in out Goal;
-            Inputs : in     Term_Array) is
-    begin
-        This := EQ_Length (This, Inputs);
-    end EQ_Length;
-
-
-
-    --  <lo  --
-
-    function LT_Length
-           (This   : in Goal;
-            Inputs : in Term_Array)
-        return Goal
-    is
-        N_Term : Term renames Inputs (1);
-        M_Term : Term renames Inputs (2);
-
-        One, Two, Three : Goal := This;
-
-        X_Var : constant Term := Three.Fresh;
-        Y_Var : constant Term := Three.Fresh;
-    begin
-        One.Unify (N_Term, Zero_Term);
-        GT_Zero (One, M_Term);
-
-        Two.Unify (N_Term, One_Term);
-        GT_One (Two, M_Term);
-
-        Three.Unify (N_Term, T (Three.Fresh, X_Var));
-        GT_Zero (Three, X_Var);
-        Three.Unify (M_Term, T (Three.Fresh, Y_Var));
-        GT_Zero (Three, Y_Var);
-        Three.Conjunct (LT_Length_Access, X_Var & Y_Var);
-
-        return Disjunct (One & Two & Three);
-    end LT_Length;
-
-
-    procedure LT_Length
-           (This   : in out Goal;
-            Inputs : in     Term_Array) is
-    begin
-        This := LT_Length (This, Inputs);
-    end LT_Length;
-
-
-
-    --  <=lo  --
-
-    function LTE_Length
-           (This   : in Goal;
-            Inputs : in Term_Array)
-        return Goal is
-    begin
-        return Disjunct
-           (EQ_Length (This, Inputs),
-            LT_Length (This, Inputs));
-    end LTE_Length;
-
-
-    procedure LTE_Length
-           (This   : in out Goal;
-            Inputs : in     Term_Array) is
-    begin
-        This := LTE_Length (This, Inputs);
-    end LTE_Length;
-
-
-
-    --  <o  --
-
-    function LT
-           (This   : in Goal;
-            Inputs : in Term_Array)
-        return Goal
-    is
-        N_Term : Term renames Inputs (1);
-        M_Term : Term renames Inputs (2);
-
-        One, Two : Goal := This;
-
-        X_Var : constant Term := Two.Fresh;
-    begin
-        LT_Length (One, Inputs);
-
-        EQ_Length (Two, Inputs);
-        GT_Zero (Two, X_Var);
-        Add (Two, N_Term & X_Var & M_Term);
-
-        return Disjunct (One, Two);
-    end LT;
-
-
-    procedure LT
-           (This   : in out Goal;
-            Inputs : in     Term_Array) is
-    begin
-        This := LT (This, Inputs);
-    end LT;
-
-
-
-    --  <=o  --
-
-    function LTE
-           (This   : in Goal;
-            Inputs : in Term_Array)
-        return Goal is
-    begin
-        return Disjunct
-           (This.Unify (Inputs (1), Inputs (2)),
-            LT (This, Inputs));
-    end LTE;
-
-
-    procedure LTE
-           (This   : in out Goal;
-            Inputs : in     Term_Array) is
-    begin
-        This := LTE (This, Inputs);
-    end LTE;
-
-
-end Kompsos.Arithmetic;
-
-