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