34
35:- module(globprops,
36 [(deprecated)/1,
37 database/1,
38 det/1,
39 dupclauses/1,
40 equiv/2,
41 eval/1,
42 exception/1,
43 exception/2,
44 fails/1,
45 failure/1,
46 fi/2,
47 has_choicepoints/1,
48 is_det/1,
49 iso/1,
50 meta_modes/1,
51 multi/1,
52 nfi/2,
53 no_choicepoints/1,
54 no_exception/1,
55 no_exception/2,
56 no_meta_modes/1,
57 no_signal/1,
58 no_signal/2,
59 non_det/1,
60 nondet/1,
61 not_fails/1,
62 nsh/2,
63 num_solutions/2,
64 num_solutions_eq/2,
65 semidet/1,
66 signal/1,
67 signal/2,
68 signals/2,
69 solutions/2,
70 throw/2,
71 throws/2,
72 unknown/1,
73 user_output/2
74 ]). 75
76:- use_module(library(memfile)). 77:- use_module(library(choicepoints)). 78:- use_module(library(assertions)). 79:- use_module(library(intercept)). 80:- use_module(library(metaprops)). 81:- use_module(library(typeprops)). 82:- use_module(library(send_check)). 83:- init_expansors.
114:- meta_predicate equiv(0, 0). 115:- global equiv/2.
116
117equiv(_, Goal) :- call(Goal).
118
119%! unknown(:Goal)
120%
121% Does nothing, just provided as a stub for the meta/2 predicate
122
123:- global unknown/1.
124
125unknown(Goal) :- Goal.
131:- meta_predicate det(0). 132:- global det(X) + equiv(not_fails(is_det(X))).
133
134det(Goal) :-
135 Solved = solved(no),
136 ( true
137 ; arg(1, Solved, no)
138 ->send_comp_rtcheck(Goal, det, fails),
139 fail
140 ),
141 prolog_current_choice(C1),
142 Goal,
143 prolog_current_choice(C2),
144 ( arg(1, Solved, no)
145 ->true
146 ; send_comp_rtcheck(Goal, det, non_det)
147 ),
148 ( C1 == C2
149 ->!
150 ; nb_setarg(1, Solved, yes)
151 ).
152
153%! semidet(:Goal)
154%
155% Goal has zero or one solution
156
157:- global semidet/1.
158
159semidet(Goal) :- semidet(Goal, semidet).
160
161%! nondet(:Goal)
162%
163% Goal is non-deterministic.
164
165:- global nondet/1.
166
167nondet(Goal) :- Goal.
168
169%! multi(:Goal)
170%
171% Goal could have multiple solutions.
172
173:- global multi/1.
174
175multi(Goal) :- multi(Goal, multi).
176
177multi(Goal, Prop) :-
178 Solved = solved(no),
179 ( true
180 ; arg(1, Solved, no)
181 ->send_comp_rtcheck(Goal, Prop, failure),
182 fail
183 ),
184 prolog_current_choice(C1),
185 test_throw_2(Goal, Prop, _, true),
186 prolog_current_choice(C2),
187 ( C1 == C2
188 ->!
189 ; nb_setarg(1, Solved, yes)
190 ).
191
192%! not_fails(:Goal)
193%
194% Goal does not fail
195
196:- global not_fails(X) + equiv(multi(X)).
197
198not_fails(Goal) :- multi(Goal, not_fails).
199
200%! failure(:Goal)
201%
202% Goal always fail
203
204:- global failure/1.
205
206failure(Goal) :- failure(Goal, failure).
207
208%! fails(:Goal)
209%
210% Equivalent to failure/1
211
212:- global fails(X) + equiv(failure(X)).
213
214fails(Goal) :- failure(Goal, fails).
215
216failure(Goal, Prop) :-
217 Solved = solved(no),
218 test_throw_2(Goal, Prop, _, true),
219 ( arg(1, Solved, no)
220 ->send_comp_rtcheck(Goal, Prop, not_fails),
221 nb_setarg(1, Solved, yes)
222 ; true
223 ).
224
225
226%! is_det(:Goal)
227%
228% Goal is deterministic. Equivalent to semidet.
229
230:- global is_det(X) + equiv(semidet(X)).
231
232is_det(Goal) :- semidet(Goal, is_det).
233
234semidet(Goal, Prop) :-
235 Solved = solved(no),
236 Goal,
237 ( arg(1, Solved, no)
238 ->true
239 ; send_comp_rtcheck(Goal, Prop, non_det)
240 ),
241 nb_setarg(1, Solved, yes).
242
243%! non_det(:Goal)
244%
245% Goal is non-deterministic
246
247:- global non_det/1.
248
249non_det(Goal) :-
250 Solved = solved(no),
251 ( true
252 ; arg(1, Solved, one)
253 ->send_comp_rtcheck(Goal, non_det, is_det),
254 fail
255 ),
256 prolog_current_choice(C1),
257 Goal,
258 prolog_current_choice(C2),
259 ( arg(1, Solved, no)
260 ->( C2 == C1
261 ->!,
262 send_comp_rtcheck(Goal, non_det, no_choicepoints)
263 ; nb_setarg(1, Solved, one)
264 )
265 ; nb_setarg(1, Solved, yes)
266 ).
267
268%! no_choicepoints(:Goal)
269%
270% Goal does not leave choicepoints on exit
271
272:- global no_choicepoints/1.
273
274no_choicepoints(Goal) :-
275 no_choicepoints(Goal, send_comp_rtcheck(Goal, no_choicepoints, has_choicepoints)).
276
277%! has_choicepoints(:Goal)
278%
279% Goal leave choicepoints on exit
280
281:- global has_choicepoints/1.
282
283has_choicepoints(Goal) :-
284 has_choicepoints(Goal, send_comp_rtcheck(Goal, has_choicepoints, no_choicepoints)).
285
286%! num_solutions_eq(Num:int, :Goal)
287%
288% Goal have Num solutions
289
290:- global num_solutions_eq/2.
291
292num_solutions_eq(N, Goal) :-
293 Sols = solutions(0),
294 ( true
295 ; arg(1, Sols, A),
296 ( ( A == done
297 ; A == N
298 )
299 ->fail
300 ; send_comp_rtcheck(Goal, num_solutions_eq(N), Sols),
301 fail
302 )
303 ),
304 prolog_current_choice(C1),
305 call(Goal),
306 prolog_current_choice(C2),
307 arg(1, Sols, A),
308 ( A == done
309 ->true
310 ; N1 is A+1,
311 ( C2 == C1
312 ->!,
313 ( N1 == N
314 ->true
315 ; send_comp_rtcheck(Goal, num_solutions_eq(N), num_solutions_eq(N1))
316 )
317 ; N1 > N
318 ->send_comp_rtcheck(Goal, num_solutions_eq(N), num_solutions(>(N))),
319 nb_setarg(1, Sols, done)
320 ; nb_setarg(1, Sols, N1)
321 )
322 ).
328:- meta_predicate num_solutions(1, 0). 329:- global num_solutions/2 + meta_modes.
330
331num_solutions(Check, Goal) :-
332 Sols = num_solutions(0),
333 ( true
334 ; arg(1, Sols, N1),
335 ( call(Check, N1)
336 ->fail
337 ; send_comp_rtcheck(Goal, num_solutions(Check), num_solutions(N1)),
338 fail
339 )
340 ),
341 prolog_current_choice(C1),
342 call(Goal),
343 prolog_current_choice(C2),
344 arg(1, Sols, N1),
345 N2 is N1+1,
346 ( C2 == C1
347 ->!,
348 ( call(Check, N2)
349 ->true
350 ; send_comp_rtcheck(Goal, num_solutions(Check), num_solutions(N1))
351 )
352 ; nb_setarg(1, Sols, N2)
353 ).
359:- meta_predicate solutions(+, 0). 360:- global solutions(+list, 0).
361
362solutions(Sols, Goal) :-
363 Goal = _:Sol,
364 Remaining = solutions(Sols),
365 ( true
366 ; arg(1, Remaining, Sols1),
367 ( ( Sols == done
368 ; Sols1 == []
369 )
370 ->fail
371 ; append(Sols3, Sols1, Sols),
372 send_comp_rtcheck(Goal, solutions(Sols), solutions(Sols3)),
373 fail
374 )
375 ),
376 prolog_current_choice(C1),
377 call(Goal),
378 prolog_current_choice(C2),
379 arg(1, Remaining, Sols1),
380 ( Sols1 == done
381 ->true
382 ; [Elem|Sols2] = Sols1,
383 ( C2 == C1
384 ->!,
385 ( Elem \= Sol
386 ->append(Curr, Sols1, Sols),
387 append(Curr, [Sol], Sols3),
388 send_comp_rtcheck(Goal, solutions(Sols), solutions(Sols3))
389 ; true
390 )
391 ; Elem \= Sol
392 ->append(Curr, Sols1, Sols),
393 append(Curr, [Sol|_], Sols3),
394 send_comp_rtcheck(Goal, solutions(Sols), solutions(Sols3)),
395 nb_setarg(1, Remaining, done)
396 ; nb_setarg(1, Remaining, Sols2)
397 )
398 ).
399
400%! database(:Goal)
401%
402% Goal will change the prolog database.
403
404:- global database/1.
405
406database(Goal) :- call(Goal).
407
408%! eval(:Goal)
409%
410% Goal is evaluable at compile-time.
411
412:- global eval/1.
413
414eval(Goal) :- call(Goal).
415
416%! dupclauses(:Goal)
417%
418% Goal is a predicate with duplicated clauses.
419
420:- global dupclauses/1 + (eval, database).
421
422dupclauses(M:Goal) :-
423 ( functor(Goal, F, A),
424 functor(Head1, F, A),
425 functor(Head2, F, A),
426 clause(M:Head1, Body1, Ref1),
427 clause(M:Head2, Body2, Ref2),
428 Ref1 \= Ref2,
429 (M:Head1 :- Body1) =@= (M:Head2 :- Body2)
430 ->true
431 ; send_comp_rtcheck(Goal, dupclauses, not(dupclauses))
432 ),
433 call(Goal).
434
435:- thread_local signal_db/3. 436
437asserta_signal_check(Choice, _, E, _) :- asserta(signal_db(Choice, no, E)).
438asserta_signal_check(Choice, G, _, Thrown) :-
439 end_signal_check(Choice, G, Thrown),
440 fail.
441
442retract_signal_check(Choice, G, _, Thrown) :- end_signal_check(Choice, G, Thrown).
443retract_signal_check(Choice, _, E, _) :- asserta(signal_db(Choice, no, E)), fail.
444
445signal_prop(yes, E, signal(E, yes), signal(E, no )).
446signal_prop(no, E, signal(E, no ), signal(E, yes)).
447
448end_signal_check(Choice, Goal, CheckThrown) :-
449 retract(signal_db(Choice, Thrown, E)),
450 signal_prop(CheckThrown, E, EP, EV),
451 ( Thrown = CheckThrown
452 ->true
453 ; send_comp_rtcheck(Goal, EP, EV)
454 ).
455
456emit_signal(Choice, E) :-
457 retract(signal_db(Choice, _, _)),
458 assertz(signal_db(Choice, yes, E)).
459
460%! signal(:Goal)
461%
462% Goal sends a signal
463
464:- global signal/1.
465
466signal(Goal) :- signal(_, Goal).
467
468%! signal(:Goal, Signal)
469%
470% Goal sends a signal that unifies with Signal
471
472:- global signal/2.
473
474signal(Signal, Goal) :-
475 prolog_current_choice(Choice),
476 asserta_signal_check(Choice, Goal, Signal, yes),
477 prolog_current_choice(C1),
478 intercept(Goal, Signal,
479 ( emit_signal(Choice, Signal),
480 send_signal(Signal)
481 )),
482 prolog_current_choice(C2),
483 retract_signal_check(Choice, Goal, Signal, yes),
484 ( C1 == C2
485 ->!
486 ; true
487 ).
488
489%! no_signal(:Goal)
490%
491% Goal don't send any signal.
492
493:- global no_signal/1.
494
495no_signal(Goal) :- no_signal(_, Goal).
496
497%! no_signal(:Goal, Signal)
498%
499% Goal don't send signals that unifies with Signal
500
501:- global no_signal/2.
502
503no_signal(Signal, Goal) :-
504 prolog_current_choice(Choice),
505 asserta_signal_check(Choice, Goal, Signal, no),
506 prolog_current_choice(C1),
507 intercept(Goal, Signal,
508 ( emit_signal(Choice, Signal),
509 throw(Signal)
510 )),
511 prolog_current_choice(C2),
512 retract_signal_check(Choice, Goal, Signal, no),
513 ( C1 == C2
514 ->!
515 ; true
516 ).
517
518%! exception(:Goal)
519%
520% Goal throws an exception.
521
522:- global exception/1.
523
524exception(Goal) :- Goal, send_comp_rtcheck(Goal, exception, no_exception).
525
526%! throw(Exception, :Goal)
527%
528% Goal throws an exception that unifies with Exception
529
530:- global throw/2.
531throw(E, Goal) :- test_throw_2(Goal, throw(E), F, F \= E).
532
533:- meta_predicate test_throw_2(0, ?, ?, 0). 534test_throw_2(Goal, Prop, F, Test) :-
535 catch(Goal, F,
536 ( ( F \= assrchk(_),
537 Test
538 ->send_comp_rtcheck(Goal, Prop, exception(F))
539 ; true
540 ),
541 throw(F)
542 )).
543
544%! exception(Exception, :Goal)
545%
546% Goal throws an exception that unifies with Exception
547
548:- global exception(E, Goal) + equiv(exception(throw(E, Goal))).
549
550exception(E, Goal) :-
551 test_throw_2(Goal, exception(E), F, F \= E),
552 send_comp_rtcheck(Goal, exception(E), no_exception).
553
554%! no_exception(:Goal)
555%
556% Goal doesn't throw any exception.
557
558:- global no_exception/1.
559
560no_exception(Goal) :- test_throw_2(Goal, no_exception, _, true).
561
562%! no_exception(Exception, :Goal)
563%
564% Goal doesn't throw an exception that unifies with Exception
565
566:- global no_exception/2.
567
568no_exception(E, Goal) :- test_throw_2(Goal, no_exception(E), F, \+F \= E).
569
570%! throws(Exceptions:List, :Goal)
571%
572% Goal can only throw the exceptions that unify with the elements of
573% Exceptions
574
575:- global throws/2.
576
577throws(EL, Goal) :- test_throw_2(Goal, throws(EL), F, \+memberchk(F, EL)).
578
579%! signals(Signals:List, :Goal)
580%
581% Goal can generate only the signals that unify with the elements of
582% Signals
583%
584% @tbd proper implementation
585
586:- global signals/2.
587
588signals(_, Goal) :- call(Goal).
589
590%! meta_modes(:Goal)
591%
592% The modes for Goal are specified in the meta_predicate declaration.
593
594:- global meta_modes/1.
595
596meta_modes(Goal) :- call(Goal).
597
598%! no_meta_modes(:Goal)
599%
600% The modes for ~w are not specified in the meta_predicate declaration.
601
602:- global no_meta_modes/1.
603
604no_meta_modes(Goal) :- call(Goal).
605
606%! deprecated(:Goal)
607%
608% Specifies that the predicate marked with this global property has been
609% deprecated, i.e., its use is not recommended any more since it will be
610% deleted at a future date. Typically this is done because its functionality
611% has been superseded by another predicate.
612
613:- global declaration (deprecated)/1.
614
615deprecated(Goal) :-
616 send_comp_rtcheck(Goal, deprecated, called),
617 call(Goal).
618
619%! iso(:Goal)
620%
621% Complies with the ISO-Prolog standard.
622
623:- global iso/1.
624
625iso(Goal) :- call(Goal).
626
627%! nfi(Term, :Goal)
628%
629% On success of Goal, Term is not further instantiated.
630
631:- global nfi/2.
632
633nfi(V, Goal) :-
634 copy_term(V, X),
635 call(Goal),
636 ( subsumes_term(V, X)
637 ->true
638 ; send_comp_rtcheck(Goal, nfi(V), fi(X))
639 ).
640
641%! fi(Term, :Goal)
642%
643% On success of Goal, Term is further instantiated.
644
645:- global fi/2.
646
647fi(V, Goal) :-
648 copy_term(V, X),
649 call(Goal),
650 ( subsumes_term(V, X)
651 ->send_comp_rtcheck(Goal, fi(V), nfi(X))
652 ; true
653 ).
654
655%! nsh(Term, :Goal)
656%
657% On call of Goal, Goal and Term don't share variables
658
659:- global nsh/2.
660nsh(Arg, Goal) :- check_nsh(Arg, Goal), call(Goal).
661
662check_nsh(Arg, _:Goal) :-
663 ( term_variables(Arg, Vars),
664 Vars \= []
665 ->Goal =.. [_|Args],
666 ( select(Arg1, Args, Left),
667 Arg1 == Arg
668 ->term_variables(Left, GVars),
669 intersection(Vars, GVars, Shared),
670 ( Shared \= []
671 ->send_comp_rtcheck(Goal, nsh, shared(Shared))
672 ; true
673 )
674 ; true
675 )
676 ; true
677 ).
678
679%! user_output(+String, :Goal)
680%
681% Goal produces String as standard output
682
683:- global user_output/2.
684
685user_output(S, Goal) :-
686 setup_call_cleanup(new_memory_file(File),
687 use_output_mf(File, S, Goal),
688 free_memory_file(File)).
689
690use_output_mf(File, S, Goal) :-
691 asserta_user_output_check(File, S, Goal),
692 prolog_current_choice(C1),
693 catch(Goal, E,
694 ( end_output_check(File, S, Goal),
695 throw(E)
696 )),
697 prolog_current_choice(C2),
698 retract_user_output_check(File, S, Goal),
699 ( C1 == C2
700 ->!,
701 output_check(File, S, Goal)
702 ; true
703 ).
704
705asserta_user_output_check(File, _, _) :-
706 open_memory_file(File, write, Stream),
707 tell(Stream).
708asserta_user_output_check(File, S, Goal) :-
709 told,
710 output_check(File, S, Goal),
711 fail.
712
713retract_user_output_check(_, _, _) :-
714 told.
715retract_user_output_check(File, _, _) :-
716 open_memory_file(File, append, Stream),
717 append(Stream),
718 fail.
719
720end_output_check(File, S, Goal) :- told, output_check(File, S, Goal).
721
722output_check(File, S, Goal) :-
723 memory_file_to_string(File, S1),
724 format("~s", [S1]),
725 ( S \== S1
726 ->send_comp_rtcheck(Goal, user_output(S), user_output(S1))
727 ; true
728 ),
729 !
Global Properties
These are the properties that can be placed in the global section of an assertion, or in a program-point assertion
Note that the implementations provided for the properties are executed when run-time checking is enabled. Such properties should be implemented following certain rules:
call(Goal)
must be equivalent to:*/