path: root/src/kompsos-math.adb

--  Programmed by Jedidiah Barber
--  Licensed under the Sunset License v1.0

--  See license.txt for further details


package body Kompsos.Math 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.

    LT_Length_Access : constant access function
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal := LT_Length'Access;

    EQ_Length_Access : constant access function
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal := EQ_Length'Access;

    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;

    Repeated_Multiply_Access : constant access function
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal := Repeated_Multiply'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;




    ------------------
    --  Comparison  --
    ------------------

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



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



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



    --  (extra function)  --

    function GTE_Length
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal is
    begin
        return LTE_Length (This, Inputs (2) & Inputs (1));
    end GTE_Length;


    procedure GTE_Length
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := GTE_Length (This, Inputs);
    end GTE_Length;



    --  (extra function)  --

    function GT_Length
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal is
    begin
        return LT_Length (This, Inputs (2) & Inputs (1));
    end GT_Length;


    procedure GT_Length
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := GT_Length (This, Inputs);
    end GT_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;



    --  (extra function)  --

    function GTE
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal is
    begin
        return LTE (This, Inputs (2) & Inputs (1));
    end GTE;


    procedure GTE
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := GTE (This, Inputs);
    end GTE;



    --  (extra function)  --

    function GT
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal is
    begin
        return LT (This, Inputs (2) & Inputs (1));
    end GT;


    procedure GT
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := GT (This, Inputs);
    end GT;




    ------------------
    --  Arithmetic  --
    ------------------

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



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



    --  repeated-mul  --

    function Repeated_Multiply
           (This   : in Goal;
            Inputs : in Term_Array)
        return Goal
    is
        Base_Term     : Term renames Inputs (1);
        Exponent_Term : Term renames Inputs (2);
        Product_Term  : Term renames Inputs (3);

        One, Two, Three : Goal := This;

        New_Exponent    : constant Term := Three.Fresh;
        Partial_Product : constant Term := Three.Fresh;
    begin
        GT_Zero (One, Base_Term);
        One.Unify (Exponent_Term, Zero_Term);
        One.Unify (Product_Term, One_Term);

        Two.Unify (Exponent_Term, One_Term);
        Two.Unify (Base_Term, Product_Term);

        GT_One (Three, Exponent_Term);
        Subtract (Three, Exponent_Term & One_Term & New_Exponent);
        Three.Conjunct (Repeated_Multiply_Access, Base_Term & New_Exponent & Partial_Product);
        Multiply (Three, Partial_Product & Base_Term & Product_Term);

        return Disjunct (One & Two & Three);
    end Repeated_Multiply;


    procedure Repeated_Multiply
           (This   : in out Goal;
            Inputs : in     Term_Array) is
    begin
        This := Repeated_Multiply (This, Inputs);
    end Repeated_Multiply;


end Kompsos.Math;