From 44bfd9d245f6ba53151b9a149e5ac0c7784ec141 Mon Sep 17 00:00:00 2001 From: Jedidiah Barber Date: Thu, 25 Dec 2025 21:09:53 +1300 Subject: Arithmetic -> Math package rename --- src/kompsos-arithmetic.adb | 679 --------------------------------------------- src/kompsos-arithmetic.ads | 298 -------------------- src/kompsos-math.adb | 679 +++++++++++++++++++++++++++++++++++++++++++++ src/kompsos-math.ads | 298 ++++++++++++++++++++ 4 files changed, 977 insertions(+), 977 deletions(-) delete mode 100644 src/kompsos-arithmetic.adb delete mode 100644 src/kompsos-arithmetic.ads create mode 100644 src/kompsos-math.adb create mode 100644 src/kompsos-math.ads 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; - - - - -- () - -- 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; - - -- Will only return True for number literals, not for variables. - -- If you want to check a variable Term then you must reify it first. - 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 & Sum_Term - function Add - (This : in Goal; - Inputs : in Term_Array) - return Goal - with Pre => Inputs'Length = 3; - - -- Inputs = N_Term & M_Term & Sum_Term - procedure Add - (This : in out Goal; - Inputs : in Term_Array) - with Pre => Inputs'Length = 3; - - - -- -o -- - -- Inputs = N_Term & M_Term & Difference_Term - function Subtract - (This : in Goal; - Inputs : in Term_Array) - return Goal - with Pre => Inputs'Length = 3; - - -- Inputs = N_Term & M_Term & Difference_Term - procedure Subtract - (This : in out Goal; - Inputs : in Term_Array) - with Pre => Inputs'Length = 3; - - - -- *o -- - -- Inputs = N_Term & M_Term & Product_Term - function Multiply - (This : in Goal; - Inputs : in Term_Array) - return Goal - with Pre => Inputs'Length = 3; - - -- Inputs = N_Term & M_Term & Product_Term - procedure Multiply - (This : in out Goal; - Inputs : in Term_Array) - with Pre => Inputs'Length = 3; - - - -- =lo -- - -- Inputs = N_Term & M_Term - function EQ_Length - (This : in Goal; - Inputs : in Term_Array) - return Goal - with Pre => Inputs'Length = 2; - - -- Inputs = N_Term & M_Term - procedure EQ_Length - (This : in out Goal; - Inputs : in Term_Array) - with Pre => Inputs'Length = 2; - - - -- Inputs'Length = 2; - - -- Inputs = N_Term & M_Term - procedure LT_Length - (This : in out Goal; - Inputs : in Term_Array) - with Pre => Inputs'Length = 2; - - - -- <=lo -- - -- Inputs = N_Term & M_Term - function LTE_Length - (This : in Goal; - Inputs : in Term_Array) - return Goal - with Pre => Inputs'Length = 2; - - -- Inputs = N_Term & M_Term - procedure LTE_Length - (This : in out Goal; - Inputs : in Term_Array) - with Pre => Inputs'Length = 2; - - - -- Inputs'Length = 2; - - -- Inputs = N_Term & M_Term - procedure LT - (This : in out Goal; - Inputs : in Term_Array) - with Pre => Inputs'Length = 2; - - - -- <=o -- - -- Inputs = N_Term & M_Term - function LTE - (This : in Goal; - Inputs : in Term_Array) - return Goal - with Pre => Inputs'Length = 2; - - -- Inputs = N_Term & M_Term - procedure LTE - (This : in out Goal; - Inputs : in Term_Array) - with Pre => Inputs'Length = 2; - - -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 & Sum_Term - function Adder - (This : in Goal; - Inputs : in Term_Array) - return Goal - with Pre => Inputs'Length = 4; - - -- Inputs = Cin_Term & N_Term & M_Term & Sum_Term - procedure Adder - (This : in out Goal; - Inputs : in Term_Array) - with Pre => Inputs'Length = 4; - - - -- gen-addero -- - -- The carry-in input is a raw Zero_Element or One_Element. - - -- Inputs = Cin_Term & N_Term & M_Term & Sum_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 & Sum_Term - procedure General_Adder - (This : in out Goal; - Inputs : in Term_Array) - with Pre => Inputs'Length = 4; - - - - -- odd-*o -- - -- (What is the X_Term...?) - -- Inputs = X_Term & N_Term & M_Term & Product_Term - function Odd_Multiply - (This : in Goal; - Inputs : in Term_Array) - return Goal - with Pre => Inputs'Length = 4; - - -- Inputs = X_Term & N_Term & M_Term & Product_Term - procedure Odd_Multiply - (This : in out Goal; - Inputs : in Term_Array) - with Pre => Inputs'Length = 4; - - - -- bound-*o -- - -- (What is the Q_Term...?) - -- Inputs = Q_Term & Product_Term & N_Term & M_Term - function Bounded_Multiply - (This : in Goal; - Inputs : in Term_Array) - return Goal - with Pre => Inputs'Length = 4; - - -- Inputs = Q_Term & Product_Term & N_Term & M_Term - procedure Bounded_Multiply - (This : in out Goal; - Inputs : in Term_Array) - with Pre => Inputs'Length = 4; - - -end Kompsos.Arithmetic; - - diff --git a/src/kompsos-math.adb b/src/kompsos-math.adb new file mode 100644 index 0000000..b64d393 --- /dev/null +++ b/src/kompsos-math.adb @@ -0,0 +1,679 @@ + + +-- 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. + + 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; + + + + -- () + -- 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; + + -- Will only return True for number literals, not for variables. + -- If you want to check a variable Term then you must reify it first. + 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 & Sum_Term + function Add + (This : in Goal; + Inputs : in Term_Array) + return Goal + with Pre => Inputs'Length = 3; + + -- Inputs = N_Term & M_Term & Sum_Term + procedure Add + (This : in out Goal; + Inputs : in Term_Array) + with Pre => Inputs'Length = 3; + + + -- -o -- + -- Inputs = N_Term & M_Term & Difference_Term + function Subtract + (This : in Goal; + Inputs : in Term_Array) + return Goal + with Pre => Inputs'Length = 3; + + -- Inputs = N_Term & M_Term & Difference_Term + procedure Subtract + (This : in out Goal; + Inputs : in Term_Array) + with Pre => Inputs'Length = 3; + + + -- *o -- + -- Inputs = N_Term & M_Term & Product_Term + function Multiply + (This : in Goal; + Inputs : in Term_Array) + return Goal + with Pre => Inputs'Length = 3; + + -- Inputs = N_Term & M_Term & Product_Term + procedure Multiply + (This : in out Goal; + Inputs : in Term_Array) + with Pre => Inputs'Length = 3; + + + -- =lo -- + -- Inputs = N_Term & M_Term + function EQ_Length + (This : in Goal; + Inputs : in Term_Array) + return Goal + with Pre => Inputs'Length = 2; + + -- Inputs = N_Term & M_Term + procedure EQ_Length + (This : in out Goal; + Inputs : in Term_Array) + with Pre => Inputs'Length = 2; + + + -- Inputs'Length = 2; + + -- Inputs = N_Term & M_Term + procedure LT_Length + (This : in out Goal; + Inputs : in Term_Array) + with Pre => Inputs'Length = 2; + + + -- <=lo -- + -- Inputs = N_Term & M_Term + function LTE_Length + (This : in Goal; + Inputs : in Term_Array) + return Goal + with Pre => Inputs'Length = 2; + + -- Inputs = N_Term & M_Term + procedure LTE_Length + (This : in out Goal; + Inputs : in Term_Array) + with Pre => Inputs'Length = 2; + + + -- Inputs'Length = 2; + + -- Inputs = N_Term & M_Term + procedure LT + (This : in out Goal; + Inputs : in Term_Array) + with Pre => Inputs'Length = 2; + + + -- <=o -- + -- Inputs = N_Term & M_Term + function LTE + (This : in Goal; + Inputs : in Term_Array) + return Goal + with Pre => Inputs'Length = 2; + + -- Inputs = N_Term & M_Term + procedure LTE + (This : in out Goal; + Inputs : in Term_Array) + with Pre => Inputs'Length = 2; + + +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 & Sum_Term + function Adder + (This : in Goal; + Inputs : in Term_Array) + return Goal + with Pre => Inputs'Length = 4; + + -- Inputs = Cin_Term & N_Term & M_Term & Sum_Term + procedure Adder + (This : in out Goal; + Inputs : in Term_Array) + with Pre => Inputs'Length = 4; + + + -- gen-addero -- + -- The carry-in input is a raw Zero_Element or One_Element. + + -- Inputs = Cin_Term & N_Term & M_Term & Sum_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 & Sum_Term + procedure General_Adder + (This : in out Goal; + Inputs : in Term_Array) + with Pre => Inputs'Length = 4; + + + + -- odd-*o -- + -- (What is the X_Term...?) + -- Inputs = X_Term & N_Term & M_Term & Product_Term + function Odd_Multiply + (This : in Goal; + Inputs : in Term_Array) + return Goal + with Pre => Inputs'Length = 4; + + -- Inputs = X_Term & N_Term & M_Term & Product_Term + procedure Odd_Multiply + (This : in out Goal; + Inputs : in Term_Array) + with Pre => Inputs'Length = 4; + + + -- bound-*o -- + -- (What is the Q_Term...?) + -- Inputs = Q_Term & Product_Term & N_Term & M_Term + function Bounded_Multiply + (This : in Goal; + Inputs : in Term_Array) + return Goal + with Pre => Inputs'Length = 4; + + -- Inputs = Q_Term & Product_Term & N_Term & M_Term + procedure Bounded_Multiply + (This : in out Goal; + Inputs : in Term_Array) + with Pre => Inputs'Length = 4; + + +end Kompsos.Math; + + -- cgit