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). |