34
35:- module(ctrtchecks,
36 ['$with_asr'/2,
37 '$with_gloc'/2,
38 '$with_ploc'/2,
39 assrt_op/4,
40 check_call/3,
41 check_goal/5,
42 check_asrs_pre/5,
43 collect_assertions/4,
44 current_assertion/4,
45 is_prop_check/5,
46 is_valid_status_type/2,
47 part_time/2,
48 rtcheck_assr_status/1]). 49
50:- use_module(library(apply)). 51:- use_module(library(intercept)). 52:- use_module(library(lists)). 53:- use_module(library(pairs)). 54:- use_module(library(assertions)). 55:- use_module(library(send_check)). 56:- use_module(library(extend_args)). 57:- use_module(library(clambda)). 58:- use_module(library(context_values)). 59:- use_module(library(rtcprops)). 60:- use_module(library(metaprops)). 61:- init_expansors. 62
63:- meta_predicate checkif_modl(?, ?, 0, ?, 0). 64checkif_modl(M, M, _, _, Goal) :- !, call(Goal).
65checkif_modl(_, _, GMod, Goal, Goal) :- call(GMod).
66
67is_prop_check(Step, Level, T, Part, Asr) :-
68 part_time(Part, T),
69 asr_aprop(Asr, type, Type, _),
70 asr_aprop(Asr, stat, Status, _),
71 assrt_op(Part, Step, Level, Type),
72 is_valid_status_type(Status, Type), !.
73
74part_time(call, _).
75part_time(succ, _).
76part_time(glob, rt).
80assrt_op(call, step1, exports, calls).
81assrt_op(call, step1, exports, pred).
82assrt_op(call, step1, exports, prop).
83assrt_op(call, step2, inner, calls).
84assrt_op(call, step2, inner, pred).
85assrt_op(call, step2, inner, prop).
86assrt_op(succ, step1, exports, success).
87assrt_op(succ, step1, exports, pred).
88assrt_op(succ, step1, exports, prop).
89assrt_op(succ, step2, inner, success).
90assrt_op(succ, step2, inner, pred).
91assrt_op(succ, step2, inner, prop).
92assrt_op(glob, step1, exports, comp).
93assrt_op(glob, step1, exports, pred).
94assrt_op(glob, step1, exports, prop).
95assrt_op(glob, step2, inner, comp).
96assrt_op(glob, step2, inner, pred).
97assrt_op(glob, step2, inner, prop).
98
99is_valid_status_type(Status, Type) :-
100 rtcheck_assr_type(Type),
101 rtcheck_assr_status(Status).
102
103rtcheck_assr_status(Status) :-
104 current_prolog_flag(rtchecks_status, StatusL),
105 member(Status, StatusL).
106
107rtcheck_assr_type(calls).
108rtcheck_assr_type(pred).
109rtcheck_assr_type(prop).
110rtcheck_assr_type(comp).
111rtcheck_assr_type(success).
112
127
128black_list_pred(_=_).
129
130assertion_is_valid(T, Status, Type, Asr) :-
131 ( \+ prop_asr(glob, acheck(_), _, Asr),
132 \+ prop_asr(glob, acheck(T, _), _, Asr)
133 ->is_valid_status_type(Status, Type),
134 \+ prop_asr(glob, no_acheck(_), _, Asr),
135 \+ prop_asr(glob, no_acheck(T, _), _, Asr)
136 ; true 137 ).
138
139no_acheck_predicate(T, Pred, M) :-
140 prop_asr(Pred, M, true, comp, _, _, Asr),
141 \+ prop_asr(call, _, _, Asr),
142 ( prop_asr(glob, no_acheck(_), _, Asr)
143 ; prop_asr(glob, no_acheck(T, _), _, Asr)
144 ).
145
146current_assertion(T, Pred, M, Asr) :-
147 prop_asr(Pred, M, Status, Type, _, _, Asr),
148 \+ ( T = rt,
149 prop_asr(Pred, M, _, prop, _, _, _)
150 ),
151 \+ no_acheck_predicate(T, Pred, M),
152 assertion_is_valid(T, Status, Type, Asr),
153 ( current_prolog_flag(rtchecks_level, inner)
154 ->true
155 ; current_prolog_flag(rtchecks_level, exports),
156 predicate_property(M:Pred, exported)
157 ->true
158 ),
159 \+ black_list_pred(Pred).
160
161collect_assertions(T, Pred, M, AsrL) :-
162 copy_term_nat(Pred, Head), % copy to avoid duplication of atributes
163 findall(Head-Asr, current_assertion(T, Head, M, Asr), Pairs),
164 maplist([Pred] +\ (Pred-T)^T^true, Pairs, AsrL).
165
166:- meta_predicate check_goal(+, 0, +, +, +). 167
168check_goal(T, Call, M, CM, AsrL) :-
169 current_prolog_flag(rtchecks_level, Level),
170 checkif_modl(M, CM,
171 check_asrs(T, is_prop_check(step1, Level), AsrL, G2), G2,
172 check_asrs(T, is_prop_check(step2, Level), AsrL, Call)).
173
174:- meta_predicate
175 check_asrs(+, 3, +, +),
176 check_asrs_pre(+, 3, +, -, -). 177
178check_asrs(T, IsPropCheck, AsrL, Goal) :-
179 check_asrs_pre(T, IsPropCheck, AsrL, AsrGlobL, AsrSuccL),
180 checkif_asrs_comp(AsrGlobL, T, Goal),
181 checkif_asrs_props(T, success, AsrSuccL).
182
183check_asrs_pre(T, IsPropCheck, AsrL, AsrGlobL, AsrSuccL) :-
184 prop_rtchecks(T, AsrL, IsPropCheck, call, AsrCallL),
185 prop_rtchecks(T, AsrL, IsPropCheck, succ, AsrSuccL),
186 subtract(AsrSuccL, AsrCallL, DAsrSuccL),
187 prop_rtchecks(T, AsrL, IsPropCheck, glob, AsrGlobL),
188 subtract(AsrGlobL, AsrCallL, DAsrGlobL),
189 check_asrs_props_calls(T, AsrCallL),
190 check_asrs_props(T, success, DAsrSuccL),
191 check_asrs_props(T, comp, DAsrGlobL).
192
193prop_rtchecks(T, AsrL1, IsPropCheck, Part, AsrPVL) :-
194 include(call(IsPropCheck, T, Part), AsrL1, AsrL),
195 pairs_keys_values(AsrPVL, AsrL, _PValuesL).
196
197:- meta_predicate checkif_asrs_comp(+, +, 0). 198checkif_asrs_comp([], _, Goal) :-
199 call(Goal).
200checkif_asrs_comp([Asr-PVL|AsrL], T, Goal1) :-
201 checkif_asr_comp(T, PVL, Asr, Goal1, Goal),
202 checkif_asrs_comp(AsrL, T, Goal).
203
204checkif_asr_comp(T, PropValues, Asr, M:Goal1, M:Goal) :-
205 ( memberchk(PropValues, [[], [[]]]),
206 copy_term_nat(Asr, NAsr),
207 findall(g(NAsr, Glob, Loc),
208 ( asr_aprop(NAsr, glob, Glob, Loc),
209 valid_prop(T, Glob)
210 ), GlobL),
211 GlobL \= []
212 ->comps_to_goal(GlobL, comp_pos_to_goal(Asr), Goal2, M:Goal1),
213 Goal = '$with_asr'(Goal2, Asr)
214 ; Goal = Goal1
215 ).
216
217comp_pos_to_goal(Asr, g(Asr, M:Glob, Loc), '$with_gloc'(M:Glob, Loc), Goal) :-
218 functor(Glob, _, N),
219 arg(N, Glob, Goal).
220
221:- meta_predicate '$with_asr'(0, ?). 222'$with_asr'(Comp, Asr) :-
223 with_value(Comp, '$with_asr', Asr).
224
225:- meta_predicate '$with_gloc'(0, ?). 226'$with_gloc'(Comp, GLoc) :-
227 with_value(Comp, '$with_gloc', GLoc).
228
229:- meta_predicate '$with_ploc'(0, ?). 230'$with_ploc'(Comp, GLoc) :-
231 with_value(Comp, '$with_ploc', GLoc).
243:- meta_predicate comps_to_goal(?, 3, ?, ?). 244comps_to_goal([], _) --> [].
245comps_to_goal([Check|Checks], Goal) -->
246 comps_to_goal2(Checks, Check, Goal).
247
248:- meta_predicate comps_to_goal2(?, ?, 3, ?, ?). 249comps_to_goal2([], Check, Goal) -->
250 call(Goal, Check).
251comps_to_goal2([Check|Checks], Check1, Goal) -->
252 call(Goal, Check1),
253 comps_to_goal2(Checks, Check, Goal).
254
255:- meta_predicate check_call(+, +, 0). 256check_call(T, AsrL, Goal) :-
257 predicate_property(Goal, implementation_module(M)),
258 check_call(T, Goal, M, AsrL).
259
261check_call(ct, CM:_, M, AsrL) :- check_goal(ct, CM:true, M, CM, AsrL).
262check_call(rt, CM:Call, M, AsrL) :- check_goal(rt, CM:Call, M, CM, AsrL).
263
264check_asrs_props_calls(T, AsrPVL) :-
265 check_asrs_props_all(T, calls, AsrPVL).
266
267check_asrs_props_all(T, PType, AsrPVL) :-
268 check_asrs_props(T, PType, AsrPVL),
269 ( \+ memberchk(_-[], AsrPVL)
270 ->maplist(send_check_asr(PType), AsrPVL)
271 ; true
272 ).
273
274check_asrs_props(T, PType, AsrPVL) :-
275 maplist(check_asr_props(T, PType), AsrPVL).
276
277checkif_asrs_props(T, PType, AsrPVL) :-
278 maplist(checkif_asr_props(T, PType), AsrPVL).
279
280checkif_asr_props(T, PType, Asr-CondValues) :-
281 checkif_asr_props(T, CondValues, Asr, PType).
282
283check_asr_props(T, PType, Asr-PropValues) :-
284 check_asr_props(T, Asr, inco, PType, PropValues).
285
286send_check_asr(PType, Asr-PropValues) :-
287 ( PropValues = [[]] 288 ->true
289 ; once(asr_aprop(Asr, head, Pred, ALoc)),
290 send_check(PropValues, PType, Pred, ALoc)
291 ).
292
293checkif_asr_props(T, CondValues, Asr, PType) :-
294 ( memberchk(CondValues, [[], [[]]])
295 ->check_asr_props(T, Asr, cond, PType, PropValues),
296 send_check_asr(PType, Asr-PropValues)
297 ; true
298 ).
299
300check_asr_props(T, Asr, Cond, PType, PropValues) :-
301 copy_term_nat(Asr, NAsr),
302 once(asr_aprop(NAsr, head, _:Pred, _)),
303 term_variables(Pred, VU),
304 sort(VU, VS),
305 findall(NAsr-PropValue,
306 current_asr_prop_value(VS, T, Cond, PType, NAsr, PropValue),
307 AsrPropValues),
308 maplist([Asr] +\ (Asr-PV)^PV^true, AsrPropValues, PropValues).
309
310current_asr_prop_value(VS, T, Cond, PType, NAsr, PropValue) :-
311 ( type_cond_part_check_mult(Cond, PType, Part, Check, Mult),
312 asr_aprop(NAsr, Part, Prop, From)
313 *->
314 make_valid_prop(T, Prop, VProp), 315 \+ catch(check_prop(Check, VS, VProp),
316 Error,
317 send_signal(at_location(From, Error))),
318 last_prop_failure(L),
319 (Mult = once -> ! ; true),
320 CheckProp =.. [Check, Prop],
321 PropValue = (From/CheckProp-L)
322 ; PropValue = [] 323 ).
324
325check_prop(compat, VS, Prop) :- compat(Prop, VS).
326check_prop(instan, VS, Prop) :- instan(Prop, VS).
327
328make_valid_prop(T, M:Prop, M:Valid) :-
329 make_valid_prop(Prop, M, T, Valid).
330
331disj_prop(true, A, A).
332disj_prop(A, true, A).
333disj_prop(A, B, (A;B)).
334
335conj_prop(true, _, true).
336conj_prop(_, true, true).
337conj_prop(A, B, (A,B)).
338
339make_valid_prop(A;B, M, T, V) :-
340 !,
341 make_valid_prop(A, M, T, VA),
342 make_valid_prop(B, M, T, VB),
343 once(disj_prop(VA, VB, V)).
344make_valid_prop((A,B), M, T, V) :-
345 !,
346 make_valid_prop(A, M, T, VA),
347 make_valid_prop(B, M, T, VB),
348 once(conj_prop(VA, VB, V)).
349make_valid_prop(list(Type, X), M, T, V) :-
350 351 !,
352 ( extend_args(Type, [_], Type1),
353 valid_prop(T, M, Type1)
354 ->V = list(Type, X)
355 ; V = list(X)
356 ).
357make_valid_prop(A, M, T, V) :-
358 ( valid_prop(T, M, A)
359 ->V = A
360 ; V = true
361 ).
362
363:- meta_predicate valid_prop(+, 0 ). 364
365valid_prop(T, M:Prop) :- valid_prop(T, M, Prop).
366
367valid_prop(T, M, Prop) :-
368 functor(Prop, F, A),
369 tabled_valid_prop(T, M, F, A).
370
371:- table tabled_valid_prop/4. 372
373tabled_valid_prop(T, M, F, A) :-
374 functor(H, F, A),
375 \+ (( prop_asr(head, M:H, _, Asr),
376 ( prop_asr(glob, no_acheck( _), _, Asr)
377 ; prop_asr(glob, no_acheck(T, _), _, Asr)
378 )
379 )).
380
381type_cond_part_check_mult(inco, PType, Part, Check, Mult) :-
382 type_inco_part_check_mult(PType, Part, Check, Mult).
383type_cond_part_check_mult(cond, PType, Part, Check, Mult) :-
384 type_cond_part_check_mult(PType, Part, Check, Mult).
385
386type_inco_part_check_mult(calls, call, instan, call).
387type_inco_part_check_mult(calls, comp, compat, call).
388type_inco_part_check_mult(success, call, instan, once).
389type_inco_part_check_mult(success, comp, compat, once).
390type_inco_part_check_mult(comp, call, instan, once).
391
392type_cond_part_check_mult(success, comp, compat, call).
393type_cond_part_check_mult(success, succ, instan, call)