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