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 :- module(kernel_records,[is_a_record_wf/3, not_is_a_record_wf/3,
6 construct_record_wf/3,
7 access_record_wf/4,
8 normalise_record_type/2, normalise_record_types/4,
9 record_has_multiple_field_names/2,
10 check_field_name_compatibility/3,
11 overwrite_record_wf/5
12 ]).
13
14
15 :- use_module(self_check).
16 :- use_module(debug).
17 :- use_module(tools).
18 :- use_module(typechecker).
19 :- use_module(error_manager).
20 :- use_module(library(samsort),[samsort/2]).
21
22 :- use_module(module_information,[module_info/2]).
23 :- module_info(group,kernel).
24 :- module_info(description,'This module contains predicates that operate on the record type.').
25
26 :- assert_must_succeed(( kernel_records:normalise_record_type(
27 record([field(name,global('ID')),field(balance,integer)]),X),
28 X == record([field(balance,integer),field(name,global('ID'))]) )).
29 :- assert_must_succeed(( kernel_records:normalise_record_type(
30 record([field(balance,integer),field(name,global('ID'))]),X),
31 X == record([field(balance,integer),field(name,global('ID'))]) )).
32 :- assert_must_succeed(( kernel_records:normalise_record_type(
33 record([field(b,d),field(a,c)]),X),
34 X == record([field(a,c),field(b,d)]) )).
35
36 % just normalise a top-level record type
37 normalise_record_type(record(Fields),record(SortedFields)) :-
38 check_known_field_names(Fields),
39 samsort(Fields,SortedFields). % Note: this will not remove duplicates with same type !
40
41
42 :- assert_must_succeed(( kernel_records:normalise_record_types(
43 record([field(name,global('ID')),field(balance,integer)]),[],X,HR), HR==true,
44 X == record([field(balance,integer),field(name,global('ID'))]) )).
45 :- assert_must_succeed(( kernel_records:normalise_record_types(
46 set(record([field(name,global('ID')),field(balance,integer)])),[],X, HR), HR==true,
47 X == set(record([field(balance,integer),field(name,global('ID'))])) )).
48
49 :- use_module(probsrc(tools),[exact_member/2]).
50
51 % normalise all record types within a type and instantiate HasRecords if a record is encountered
52 % allows variables
53 normalise_record_types(Var,NonGroundExceptions,R,_) :- var(Var), !,
54 (NonGroundExceptions=do_not_ground_types -> true % TODO: check if Var in NonGroundExceptions
55 ; exact_member(Var,NonGroundExceptions) -> true
56 ; add_internal_error('Variable type:',normalise_record_types(Var,NonGroundExceptions,R,_))),
57 R=Var.
58 normalise_record_types(couple(TA,TB),NonGroundExceptions,couple(NTA,NTB),HasRecords) :- !,
59 normalise_record_types(TA,NonGroundExceptions,NTA,HasRecords),
60 normalise_record_types(TB,NonGroundExceptions,NTB,HasRecords).
61 normalise_record_types(seq(T),NonGroundExceptions,seq(NT),HasRecords) :- !,
62 normalise_record_types(T,NonGroundExceptions,NT,HasRecords).
63 normalise_record_types(set(T),NonGroundExceptions,set(NT),HasRecords) :- !,
64 normalise_record_types(T,NonGroundExceptions,NT,HasRecords).
65 normalise_record_types(record(Fields),NonGroundExceptions,record(SortedFields),HasRecords) :- !,
66 HasRecords=true,
67 normalise_fields(Fields,NonGroundExceptions,NFields,HasVar),
68 (HasVar==true
69 ->
70 debug_format(9,'Record type with partially known fields: ~w~n',[Fields]),
71 SortedFields=NFields
72 % grounding_open_ended_record
73 ; samsort(NFields,SortedFields)). % Note: this will not remove duplicates with same type !
74 normalise_record_types(AtomicType,_,AtomicType,_).
75
76 normalise_fields(Var,NonGroundExceptions,Res,HasVar) :- var(Var), !,
77 (NonGroundExceptions=do_not_ground_types -> true
78 ; add_internal_error('Variable fields:',normalise_fields(Var,NonGroundExceptions,Res,HasVar))),
79 HasVar=true, Res=Var.
80 normalise_fields([],_,[],_).
81 normalise_fields([field(Name,FieldType)|T],NonGroundExceptions,[field(Name,NFieldType)|NT],HasVar) :-
82 (var(Name)
83 -> add_internal_error('Illegal var fields: ',normalise_fields([field(Name,_)|T])),
84 HasVar=true
85 ; true),
86 normalise_record_types(FieldType,NonGroundExceptions,NFieldType,_HasRecords),
87 normalise_fields(T,NonGroundExceptions,NT,HasVar).
88
89 :- use_module(kernel_waitflags).
90 :- assert_must_succeed(( kernel_waitflags:init_wait_flags(WF),
91 kernel_records:is_a_record_wf(rec([field(balance,int(1)),field(name,fd(2,'Name'))]),
92 rec([field(balance,global_set('NAT')),field(name,global_set('Name'))]),WF),
93 kernel_waitflags:ground_wait_flags(WF))).
94 :- assert_must_fail(( kernel_waitflags:init_wait_flags(WF),
95 kernel_records:is_a_record_wf(rec([field(a,int(0)),field(b,fd(2,'Name'))]),
96 rec([field(a,global_set('NAT1')),field(b,global_set('Name'))]),WF),
97 kernel_waitflags:ground_wait_flags(WF))).
98 :- assert_must_fail(( kernel_waitflags:init_wait_flags(WF),
99 kernel_records:is_a_record_wf(rec([field(a,int(1)),field(b,fd(2,'Name')),field(c,int(0))]),
100 rec([field(a,global_set('NAT1')),field(b,global_set('Name')),field(c,global_set('NAT1'))]),WF),
101 kernel_waitflags:ground_wait_flags(WF))).
102
103
104 is_a_record_wf(rec(Fields),rec(FieldSets),WF) :-
105 check_field_values(Fields,FieldSets,WF).
106
107
108 :-use_module(kernel_objects,[check_element_of_wf/3, membership_test_wf/4]).
109
110 :- block check_field_values(-,-,?).
111 check_field_values([],[],_WF).
112 check_field_values([field(Name1,V)|ValueRest],[field(Name2,VT)|TypeRest],WF) :-
113 check_field_name_compatibility(Name1,Name2,check_field_values),
114 check_element_of_wf(V,VT,WF),
115 check_field_values(ValueRest,TypeRest,WF).
116
117
118 :- assert_must_succeed(( kernel_waitflags:init_wait_flags(WF),
119 kernel_records:not_is_a_record_wf(rec([field(balance,int(0)),field(name,fd(2,'Name'))]),
120 rec([field(balance,global_set('NAT1')),field(name,global_set('Name'))]),WF),
121 kernel_waitflags:ground_wait_flags(WF))).
122 :- assert_must_succeed(( kernel_waitflags:init_wait_flags(WF),
123 kernel_records:not_is_a_record_wf(rec([field(a,int(1)),field(b,fd(2,'Name')),field(c,int(0))]),
124 rec([field(a,global_set('NAT1')),field(b,global_set('Name')),field(c,global_set('NAT1'))]),WF),
125 kernel_waitflags:ground_wait_flags(WF))).
126 :- assert_must_fail(( kernel_waitflags:init_wait_flags(WF),
127 kernel_records:not_is_a_record_wf(rec([field(a,int(1)),field(b,fd(2,'Name')),field(c,int(1))]),
128 rec([field(a,global_set('NAT1')),field(b,global_set('Name')),field(c,global_set('NAT1'))]),WF),
129 kernel_waitflags:ground_wait_flags(WF))).
130
131 not_is_a_record_wf(rec(Fields),rec(FieldSets),WF) :-
132 not_check_field_values(Fields,FieldSets,WF).
133
134
135 :- block not_check_field_values(-,-,?).
136 not_check_field_values([field(Name1,V)|ValueRest],[field(Name2,VT)|TypeRest],WF) :-
137 check_field_name_compatibility(Name1,Name2,not_check_field_values),
138 membership_test_wf(VT,V,MemRes,WF),
139 not_check_field_values2(MemRes,ValueRest,TypeRest,WF).
140
141 :- block not_check_field_values2(-,?,?,?).
142 not_check_field_values2(pred_false,_,_,_).
143 not_check_field_values2(pred_true,ValueRest,TypeRest,WF) :-
144 not_check_field_values(ValueRest,TypeRest,WF).
145
146
147
148
149
150 :- assert_must_fail(( X = [field(b,int(33)),field(a,int(2))], X2 = [field(a,int(33)),field(b,int(2))], kernel_records:construct_record_wf(X,rec(X2),_WF) )).
151 :- assert_must_succeed(( kernel_records:construct_record_wf(X,rec([field(a,int(2)),field(b,int(3))]),_WF),
152 X = [field(b,int(3)),field(a,int(2))] )).
153 :- assert_must_succeed(( kernel_records:construct_record_wf(X,rec([field(a,int(2)),field(b,int(3))]),_WF),
154 X = [field(a,int(2)),field(b,int(3))] )).
155 :- assert_must_succeed(( kernel_records:construct_record_wf(X,Y,_WF),
156 X = [field(b,int(4)),field(a,int(2))], Y = rec([field(a,int(2)),field(b,int(4))]) )).
157 :- assert_must_succeed(( kernel_records:construct_record_wf(X,rec([field(a,[int(2),int(3)]),field(b,int(3))]),_WF), X = [field(a,[int(3),int(2)]),field(b,int(3))] )).
158
159 :- block construct_record_wf(-,?,?).
160 construct_record_wf(Fields,Res,WF) :-
161 check_known_field_names(Fields),
162 sort(Fields,SortedFields),
163 kernel_objects:equal_object_wf(Res,rec(SortedFields),WF).
164
165 check_known_field_names(Var) :- var(Var), !,
166 add_internal_error('Illegal var fields: ',check_known_field_names(Var)).
167 check_known_field_names([]).
168 check_known_field_names([field(Name,_)|T]) :-
169 (var(Name) -> add_internal_error('Illegal var fields: ',check_known_field_names([field(Name,_)|T]))
170 ; true),
171 check_known_field_names(T).
172
173
174
175 %instantiate output argument when all field names known + indicate whether sorted or not
176 %:- block known_field_names(-,?).
177 %known_field_names([],sorted).
178 %known_field_names([field(Name,_)|T],Known) :- known_field_names4(T,Name,sorted,Known).
179 %
180 %:- block known_field_names4(-,?,?,?),known_field_names4(?,-,?,?).
181 %known_field_names4([],_,K,K).
182 %known_field_names4([field(Name,_)|T],PrevName,SortedSoFar,Known) :-
183 % (PrevName @< Name -> S2=SortedSoFar ; S2=not_sorted),
184 % known_field_names4(T,Name,S2,Known).
185
186
187
188 % check if a sorted records has multiple field names
189 record_has_multiple_field_names([field(N,_)|T],Res) :- multiple_fields_aux(T,N,Res).
190 multiple_fields_aux([field(N,_)|T],N1,Res) :-
191 (N1=N -> Res=N ; multiple_fields_aux(T,N,Res)).
192
193 :- use_module(library(lists)).
194
195 %%:- assert_must_fail(( kernel_records:access_record(rec([]),a,_) )). %% actually: must generate error; not just fail
196 :- assert_must_fail(( kernel_records:access_record(rec([field(a,int(2))]),a,int(3)) )).
197 :- assert_must_succeed(( kernel_records:access_record(rec(X),a,int(2)), X=[field(b,_),field(a,int(2))|_] )).
198 :- assert_must_succeed(( kernel_records:access_record(rec(X),b,int(2)), X=[field(b,_),field(a,int(3))|_] )).
199
200 access_record(Rec,Field,V) :- access_record_wf(Rec,Field,V,no_wf_available).
201
202 %access_record(X,Y,Z) :- print_message(access_record(X,Y,Z)),fail.
203 :- block access_record_wf(?,-,?,?). % when we add access_record_wf(-,?,?,?) we do not instantiate to rec(_), but PROB-356 runs slower.
204 access_record_wf(rec(Fields),FieldName,Value,WF) :-
205 % access_record2(Fields,FieldName,Value).
206 %:- block access_record2(?,-,?).
207 %access_record2(Fields,FieldName,Value) :-
208 get_field(Fields,FieldName,Value,Fields,WF).
209
210 :- block get_field(-,?,?,?,?). % note: FieldName is already known
211 get_field([],FieldName,_Value,OrigFields,_WF) :-
212 add_internal_error('Could not get field: ', FieldName:OrigFields),fail.
213 get_field([field(SFieldName,SValue)|T], FieldName,Value,OrigFields,WF) :-
214 get_field2(SFieldName,SValue,T, FieldName,Value,OrigFields,WF).
215
216 :- block get_field2(-,?,?, ?,?,?,?).
217 get_field2(SFieldName,SValue,T, FieldName,Value,OrigFields,WF) :-
218 (SFieldName=FieldName
219 -> kernel_objects:equal_object_wf(Value,SValue,get_field2,WF)
220 ; get_field(T,FieldName,Value,OrigFields,WF)
221 ).
222
223
224
225 % try and unify field names and throw error if unification fails
226 % indicates an incorrectly sorted field
227 :- assert_must_succeed(( kernel_records:check_field_name_compatibility(a,a,test))).
228 check_field_name_compatibility(Name1,Name2,Origin) :-
229 nonvar(Name1), nonvar(Name2), Name1 \= Name2, !,
230 add_internal_error('Incompatible fields: ',check_field_name_compatibility(Name1,Name2,Origin)),
231 fail.
232 check_field_name_compatibility(Name,Name,_).
233
234
235 :- assert_must_succeed(( kernel_records:overwrite_record_wf(rec(X),c,int(22),Y,no_wf_available),
236 X=[field(b,int(33)),field(c,int(4))],
237 Y==rec([field(b,int(33)),field(c,int(22))]) )).
238
239 % overwrite one field of a record, used for assignment x'field := RHS
240 :- block overwrite_record_wf(?,-,?,?,?).
241 overwrite_record_wf(rec(Fields),FieldToChange,ChangedVal,rec(NewFields),WF) :-
242 overwrite_field(Fields,FieldToChange,ChangedVal,NewFields,WF).
243
244 :- block overwrite_field(-,?,?,?,?).
245 overwrite_field([],FieldToChange,ChangedVal,T,WF) :-
246 add_internal_error('Could not find field to overwrite:',overwrite_field([],FieldToChange,ChangedVal,T,WF)),
247 T=[].
248 overwrite_field([field(FN,V)|T],FieldToChange,ChangedVal,[field(FN,NewVal)|TN],WF) :-
249 overwrite_field_aux(FN,V,T,FieldToChange,ChangedVal,NewVal,TN,WF).
250
251 :- block overwrite_field_aux(-,?,?,?,?,?,?,?).
252 overwrite_field_aux(FN,OldVal,T,FieldToChange,ChangedVal,NewVal,TN,WF) :-
253 (FN=FieldToChange
254 -> kernel_objects:equal_object_wf(NewVal,ChangedVal,overwrite_field_aux,WF),
255 kernel_objects:equal_object_wf(rec(T),rec(TN),overwrite_field_aux,WF)
256 ; kernel_objects:equal_object_wf(NewVal,OldVal,overwrite_field_aux,WF),
257 overwrite_field(T,FieldToChange,ChangedVal,TN,WF)
258 ).