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