diff options
Diffstat (limited to 'src/kompsos-math.adb')
| -rw-r--r-- | src/kompsos-math.adb | 511 |
1 files changed, 298 insertions, 213 deletions
diff --git a/src/kompsos-math.adb b/src/kompsos-math.adb index b64d393..7ea6310 100644 --- a/src/kompsos-math.adb +++ b/src/kompsos-math.adb @@ -18,6 +18,16 @@ package body Kompsos.Math is -- 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) @@ -43,16 +53,6 @@ package body Kompsos.Math is 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; - @@ -110,7 +110,294 @@ package body Kompsos.Math is ------------------ - -- Operations -- + -- 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 -- @@ -165,51 +452,6 @@ package body Kompsos.Math is - -- 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 @@ -517,163 +759,6 @@ package body Kompsos.Math is 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.Math; |