1		% (c) 2009-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html
4
5		% This module contains arithmetic that also supports the symbol inf
6		% The operator infis/2 can be used analogously to the standard Prolog operator is/2.
7		% Currently supported arithmetic operations are +, -, *, min, max
8
9		:- module(inf_arith, [infis/2,infless/2,
10		infgreaterequal/2, infgreater/2, infdec/2, infinc/2, infdec_if_positive/2, infmin/3, infmax/3,
11		block_inf_greater/2, block_inf_greater_equal/2
12		]).
13
14		:- use_module(module_information).
15		:- module_info(group,kernel).
16		:- module_info(description,'This module contains arithmetic that also supports the symbol inf.').
17
18		:- use_module(self_check).
19
20		:- op( 700, xfx, infis).
21
22		Res infis Expr :- infis2(Expr,R), R=Res.
23
24
25		:- assert_must_succeed(( infis(R,22+inf), R==inf )).
26		:- assert_must_succeed(( infis(R,22+21), R==43 )).
27		:- assert_must_succeed(( infis(R,-(22+21)*(-1)), R==43 )).
28		:- assert_must_succeed(( infis(R,(-inf)+21), R==(-inf) )).
29		:- assert_must_succeed(( infis(R,22+(-inf)), R==(-inf) )).
30		:- assert_must_succeed(( infis(R,22-(-inf)), R==inf )).
31		:- assert_must_succeed(( infis(R,22-21), R==1 )).
32		:- assert_must_succeed(( infis(R,(-inf)-21), R==(-inf) )).
33		:- assert_must_succeed(( infis(R,inf-21), R==inf )).
34		:- assert_must_succeed(( infis(R,22*inf), R==inf )).
35		:- assert_must_succeed(( infis(R,inf//22), R==inf )).
36		:- assert_must_succeed(( infis(R,inf//(-22)), R==(-inf) )).
37		:- assert_must_succeed(( infis(R,(-44)//22), R==(-2) )).
38
39
40		infis2(A, A) :- number(A),!.
41		infis2(inf, inf).
42		infis2(-A, Res) :- infis2(A,Ac), infnegate(Ac,Res).
43		infis2(A+B, Res) :- infis2(A,Ac), infis2(B,Bc), infadd(Ac,Bc,Res).
44		infis2(A-B, Res) :- infis2(A,Ac), infis2(-B,Bc), infadd(Ac,Bc,Res).
45		infis2(A*B, Res) :- infis2(A,Ac), infis2(B,Bc), infmult(Ac,Bc,Res).
46		infis2(A//B, Res) :- infis2(A,Ac), infis2(B,Bc), infdiv(Ac,Bc,Res).
47		infis2(min(A,B), Res) :-
48		infis2(A,Ac), infis2(B,Bc), infmin(Ac,Bc,Res).
49		infis2(max(A,B), Res) :-
50		infis2(A,Ac), infis2(B,Bc), infmax(Ac,Bc,Res).
51
52		:- assert_must_succeed(( infisnegative(-2) )).
53		:- assert_must_succeed(( infisnegative(-inf) )).
54		:- assert_must_fail(( infisnegative(inf) )).
55		:- assert_must_fail(( infisnegative(0) )).
56
57		infisnegative(-inf) :- !.
58		infisnegative(inf) :- !,fail.
59		infisnegative(X) :- X<0.
60
61		infnegate(inf,-inf) :- !.
62		infnegate(-inf,inf) :- !.
63		infnegate(A,B) :- B is -A.
64
65		:- assert_must_succeed(( infadd(22,inf,R), R==inf )).
66		:- assert_must_succeed(( infadd(22,21,R), R==43 )).
67		:- assert_must_succeed(( infadd((-inf),21,R), R==(-inf) )).
68		infadd(A,B,R) :-
69		( infisnegative(A) ->
70		infnegate(A,Apos),
71		( infisnegative(B) ->
72		infnegate(B,Bpos),
73		infadd(Apos,Bpos,Rneg),
74		infnegate(Rneg,R)
75		;
76		infsub2(B,Apos,R))
77		;
78		( infisnegative(B) ->
79		infnegate(B,Bpos),
80		infsub2(A,Bpos,R)
81		;
82		infadd2(A,B,R))).
83		infadd2(inf,_,inf) :- !.
84		infadd2(_,inf,inf) :- !.
85		infadd2(A,B,R) :- R is A+B.
86
87		% don't know what is inf - inf
88		infsub2(inf,B,inf) :- !, B \== inf.
89		infsub2(_,inf,-inf) :- !.
90		infsub2(A,B,R) :- R is A-B.
91
92		infmult(A,B,R) :-
93		( infisnegative(A) ->
94		infnegate(A,Aneg),
95		infmult(Aneg,B,Rneg),
96		infnegate(Rneg,R)
97		; infisnegative(B) ->
98		infnegate(B,Bneg),
99		infmult(A,Bneg,Rneg),
100		infnegate(Rneg,R)
101		;
102		infmult2(A,B,R)).
103		infmult2(inf,_,inf) :- !.
104		infmult2(_,inf,inf) :- !.
105		infmult2(A,B,R) :- R is A*B.
106
107		infdiv(A,B,R) :-
108		( infisnegative(A) ->
109		infnegate(A,Aneg),
110		infdiv(Aneg,B,Rneg),
111		infnegate(Rneg,R)
112		; infisnegative(B) ->
113		infnegate(B,Bneg),
114		infdiv(A,Bneg,Rneg),
115		infnegate(Rneg,R)
116		;
117		infdiv2(A,B,R)).
118		infdiv2(inf,B,inf) :- !,B \== inf.
119		infdiv2(_,inf,0) :- !.
120		infdiv2(A,B,R) :- R is A//B.
121
122		:- assert_must_succeed( infgreaterequal(inf,inf)).
123		:- assert_must_succeed( infgreaterequal(inf,100)).
124		:- assert_must_succeed( infgreaterequal(2000,100)).
125		:- assert_must_fail( infgreaterequal(2000,inf)).
126		:- assert_must_fail( infgreaterequal(1999,2000)).
127		infgreaterequal(A,B) :- (A=B -> true ; infgreater(A,B)).
128
129		infgreater(A,B) :- infless(B,A).
130		infless(inf,_) :- !,fail.
131		infless(_,-inf) :- !,fail.
132		infless(-inf,_X) :- !.
133		infless(_X,inf) :- !.
134		infless(A,B) :- A<B.
135
136		:- assert_must_succeed(( infmax(22,inf,R), R==inf )).
137		:- assert_must_succeed(( infmax(22,21,R), R==22 )).
138		:- assert_must_succeed(( infmax((-inf),21,R), R==21 )).
139		:- assert_must_succeed(( infmax((-inf),inf,R), R==inf )).
140
141		infmax(A,B,R) :-
142		(infgreater(A,B) -> A=R ; B=R).
143
144
145		:- assert_must_succeed(( infmin(22,inf,R), R==22 )).
146		:- assert_must_succeed(( infmin(22,21,R), R==21 )).
147		:- assert_must_succeed(( infmin((-inf),21,R), R==(-inf) )).
148		:- assert_must_succeed(( infmin((-inf),inf,R), R==(-inf) )).
149		infmin(A,B,R) :-
150		(infless(A,B) -> A=R ; B=R).
151
152		:- assert_must_succeed(( infdec(inf,R), R==inf )).
153		:- assert_must_succeed(( infdec(3,R), R==2 )).
154		:- assert_must_succeed(( infdec(-inf,R), R==(-inf) )).
155		infdec(inf,R) :- !, R = inf.
156		infdec(-inf,R) :- !, R = -inf.
157		infdec(N,N1) :- N1 is N-1.
158
159		:- assert_must_succeed(( infinc(inf,R), R==inf )).
160		:- assert_must_succeed(( infinc(3,R), R==4 )).
161		:- assert_must_succeed(( infinc(-inf,R), R==(-inf) )).
162		infinc(inf,R) :- !, R = inf.
163		infinc(-inf,R) :- !, R = -inf.
164		infinc(N,N1) :- N1 is N+1.
165
166		:- assert_must_succeed(( infdec_if_positive(inf,R), R==inf )).
167		:- assert_must_succeed(( infdec_if_positive(3,R), R==2 )).
168		:- assert_must_fail(infdec_if_positive((-inf),_)).
169		:- assert_must_fail(infdec_if_positive((-2),(-3))).
170		infdec_if_positive(inf,R) :- !, R = inf.
171		infdec_if_positive(-inf,_) :- !, fail.
172		infdec_if_positive(N,N1) :- N>0, N1 is N-1.
173
174		% ------------------------ blocking versions --------------------
175
176
177		:- block block_inf_greater_equal(-,?), block_inf_greater_equal(?,-).
178		block_inf_greater_equal(X,Y) :- infgreaterequal(X,Y).
179
180
181		:- block block_inf_greater(-,?), block_inf_greater(?,-).
182		block_inf_greater(X,Y) :- infgreater(X,Y).