1
2 % (c) 2015-2023 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
3 % Heinrich Heine Universitaet Duesseldorf
4 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
5
6 :- module(kernel_ordering,[ordered_value/2, leq_ordered_value/3]).
7
8 :- use_module(self_check).
9
10 :- use_module(debug).
11 :- use_module(tools).
12
13 :- use_module(module_information,[module_info/2]).
14 :- module_info(group,kernel).
15 :- module_info(description,'This module provides term ordering utilities.').
16
17 :- use_module(b_global_sets,[b_get_fd_type_bounds/3]).
18 :- use_module(kernel_objects,[less_than_direct/2, less_than_equal_direct/2]).
19
20 % check that values are strictly ordered:
21 :- block ordered_value(-,?).
22 ordered_value(pred_false,Y) :- !, Y=pred_true.
23 ordered_value(pred_true,_Y) :- !, fail.
24 ordered_value(fd(X,Type),FDY) :- nonvar(Type),
25 b_get_fd_type_bounds(Type,LowBnd,UpBnd),
26 !,
27 LB1 is LowBnd+1,
28 (LB1 = UpBnd -> X=LowBnd, FDY=fd(UpBnd,Type)
29 ; (UpBnd=inf -> true ; less_than_direct(X,UpBnd)),
30 FDY = fd(Y,Type),
31 less_than_direct(X,Y)).
32 ordered_value(X,Y) :- % nl,nl,print(order2(X,Y)),nl,nl,
33 ordered_value2(X,Y).
34
35 %:- use_module(library(avl),[avl_to_list/2]).
36 :- block ordered_value2(?,-).
37 ordered_value2(int(X),int(Y)) :- !, less_than_direct(X,Y).
38 ordered_value2(fd(X,T),fd(Y,T)) :- !, less_than_direct(X,Y).
39 ordered_value2(string(X),string(Y)) :- !, prolog_order_less(X,Y).
40 ordered_value2([],avl_set(_)) :- !.
41 ordered_value2([],[_|_]) :- !.
42 ordered_value2([],[]) :- !,fail.
43 ordered_value2(avl_set(_),[]) :- !,fail.
44 ordered_value2([_|_],[]) :- !,fail.
45 %ordered_value2(avl_set(A),avl_set(B)) :- !,
46 % avl_to_list(A,AL),avl_to_list(B,BL), AL @<BL. % we need to normalize ! we could check avl_size ?
47 ordered_value2((X1,X2),(Y1,Y2)) :- !,
48 leq_ordered_value(X1,Y1,EqPred), opt_ordered_value(EqPred,X2,Y2).
49 ordered_value2(rec(XFields),rec(YFields)) :- !, ordered_fields(XFields,YFields).
50 %ordered_value2(A,B) :- print(uncovered_ordered_value(A,B)),nl,fail.
51 ordered_value2(_,_). % TO DO : treat more: sets, reals,...
52 % TO DO: use something like lex_chain([[X,X],[Y,Z]],[op(#<)]) for pairs/records of FD values
53
54 % check ordered_value only if first arg = pred_true
55 :- block opt_ordered_value(-,?,?).
56 opt_ordered_value(pred_true,X2,Y2) :- !, ordered_value(X2,Y2).
57 opt_ordered_value(_,_,_).
58
59 :- block prolog_order_less(-,?), prolog_order_less(?,-).
60 prolog_order_less(Atom1,Atom2) :- Atom1 @< Atom2.
61 :- block prolog_order_less_equal(-,?), prolog_order_less_equal(?,-).
62 prolog_order_less_equal(Atom1,Atom2) :- Atom1 @=< Atom2.
63
64 :- use_module(bool_pred,[negate/2]).
65 % check that values are ordered (<=) and return pred_true if equal, pred_false if strictly <, and unknown if it cannot be determined:
66 :- block leq_ordered_value(-,?,?).
67 leq_ordered_value(pred_true,Y,PredRes) :- !, (Y,PredRes)=(pred_true,pred_true).
68 leq_ordered_value(pred_false,Y,PredRes) :- !, negate(Y,PredRes).
69 leq_ordered_value(X,Y,PredRes) :- leq_ordered_value2(X,Y,PredRes).
70
71 :- block leq_ordered_value2(?,-,?).
72 leq_ordered_value2(int(X),int(Y),PredRes) :- !,
73 less_than_equal_direct(X,Y), atomic_eq_check(X,Y,PredRes).
74 leq_ordered_value2(fd(X,T),fd(Y,T),PredRes) :- !,
75 less_than_equal_direct(X,Y), atomic_eq_check(X,Y,PredRes).
76 leq_ordered_value2(string(X),string(Y),PredRes) :- !,
77 prolog_order_less_equal(X,Y), atomic_eq_check(X,Y,PredRes).
78 leq_ordered_value2((X1,X2),(Y1,Y2),PredRes) :- !,
79 leq_ordered_value(X1,Y1,EqPred), opt_leq_ordered_value(EqPred,X2,Y2,PredRes).
80 leq_ordered_value2(rec(FX),rec(FY),PredRes) :- !, leq_ordered_fields(FX,FY,PredRes).
81 %leq_ordered_value2(A,B,R) :- nl,print_term_summary(leq_ordered_value2(A,B,R)),nl,fail.
82 leq_ordered_value2(_,_,pred_unknown). % TO DO : treat more
83
84 atomic_eq_check(X,Y,EqRes) :- when(?=(X,Y),(X=Y -> EqRes=pred_true ; EqRes=pred_false)).
85
86 % check ordered_value only if first arg = pred_true
87 :- block opt_leq_ordered_value(-,?,?,?).
88 opt_leq_ordered_value(pred_true,X2,Y2,PredRes) :- !, % if component 1 equal: check component 2 leq
89 leq_ordered_value(X2,Y2,PredRes).
90 opt_leq_ordered_value(Res,_,_,Res). % component 1 less or unknown: return result unmodified
91
92 % ordering for records:
93
94
95 :- block ordered_fields(-,-).
96 ordered_fields([],[]).
97 ordered_fields([FX|TX],[FY|TY]) :-
98 ordered_fields_aux(FX,TX,FY,TY).
99
100 :- use_module(kernel_records,[check_field_name_compatibility/3]).
101 :- block ordered_fields_aux(-,?,-,?).
102 ordered_fields_aux(field(Name1,FX),TX,field(Name2,FY),TY) :-
103 check_field_name_compatibility(Name1,Name2,ordered_fields),
104 (TX==[] -> ordered_value(FX,FY),TY=[] % no other field remaining
105 ; leq_ordered_value(FX,FY,EqPred),
106 opt_ordered_fields(EqPred,TX,TY)).
107
108 % check ordered_value only if first arg = pred_true
109 :- block opt_ordered_fields(-,?,?).
110 opt_ordered_fields(pred_true,X2,Y2) :- !, ordered_fields(X2,Y2).
111 opt_ordered_fields(_,_,_).
112
113
114 :- block leq_ordered_fields(-,-,?).
115 leq_ordered_fields([],[],pred_true). % are equal
116 leq_ordered_fields([FX|TX],[FY|TY],PredRes) :-
117 leq_ordered_fields_aux(FX,TX,FY,TY,PredRes).
118
119 :- block leq_ordered_fields_aux(-,?,-,?,?).
120 leq_ordered_fields_aux(field(Name1,FX),TX,field(Name2,FY),TY,PredRes) :-
121 check_field_name_compatibility(Name1,Name2,leq_ordered_fields),
122 (TX==[] -> leq_ordered_value(FX,FY,PredRes),TY=[] % no other field remaining
123 ; leq_ordered_value(FX,FY,EqPred),
124 opt_leq_ordered_fields(EqPred,TX,TY,PredRes)).
125
126 % check leq_ordered_fields only if first arg = pred_true
127 :- block opt_leq_ordered_fields(-,?,?,?).
128 opt_leq_ordered_fields(pred_true,X2,Y2,EqPred) :- !, leq_ordered_fields(X2,Y2,EqPred).
129 opt_leq_ordered_fields(P,_,_,P).