1/* Part of Assertion Reader for SWI-Prolog 2 3 Author: Edison Mera 4 E-mail: efmera@gmail.com 5 WWW: https://github.com/edisonm/assertions 6 Copyright (C): 2017, Process Design Center, Breda, The Netherlands. 7 All rights reserved. 8 9 Redistribution and use in source and binary forms, with or without 10 modification, are permitted provided that the following conditions 11 are met: 12 13 1. Redistributions of source code must retain the above copyright 14 notice, this list of conditions and the following disclaimer. 15 16 2. Redistributions in binary form must reproduce the above copyright 17 notice, this list of conditions and the following disclaimer in 18 the documentation and/or other materials provided with the 19 distribution. 20 21 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS 22 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT 23 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS 24 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE 25 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, 26 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, 27 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; 28 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER 29 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT 30 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN 31 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE 32 POSSIBILITY OF SUCH DAMAGE. 33*/ 34 35:- module(globprops, 36 [(deprecated)/1, 37 database/1, 38 det/1, 39 dupclauses/1, 40 equiv/2, 41 eval/1, 42 has_exception/1, 43 has_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 mve/2, 54 no_choicepoints/1, 55 no_exception/1, 56 no_exception/2, 57 no_meta_modes/1, 58 no_signal/1, 59 no_signal/2, 60 non_det/1, 61 nondet/1, 62 not_fails/1, 63 nsh/2, 64 num_solutions/2, 65 num_solutions_eq/2, 66 semidet/1, 67 signal/1, 68 signal/2, 69 signals/2, 70 solutions/2, 71 throws_ex/2, 72 throws_exs/2, 73 unknown/1, 74 user_output/2 75 ]). 76 77:- use_module(library(lists)). 78:- use_module(library(memfile)). 79:- use_module(library(choicepoints)). 80:- use_module(library(assertions)). 81:- use_module(library(intercept)). 82:- use_module(library(metaprops)). 83:- use_module(library(typeprops)). 84:- use_module(library(send_check)). 85:- init_expansors.

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:

For any Goal, call(Goal) must be equivalent to:
```
intercept(Prop(Goal), RTCheck, true).
```
Should remove the choicepoints if the goal does not introduce new ones.
Should try to throw the run-time check exception as soon as the property being validated has been violated.
All the checks must be compatible among them.
Should be conmutative.
Should be side-effects free

116:- meta_predicate equiv(0, 0). 117:- global equiv/2. 118 119equiv(_, Goal) :- call(Goal). 120 121%! unknown(:Goal) 122% 123% Does nothing, just provided as a stub for the meta/2 predicate 124 125:- global unknown/1. 126 127unknown(Goal) :- Goal.

133:- meta_predicate det(0). 134:- global det(X) + equiv(not_fails(is_det(X))). 135 136det(Goal) :- 137 Solved = solved(no), 138 ( true 139 ; arg(1, Solved, no) 140 ->send_comp_rtcheck(Goal, det, fails), 141 fail 142 ), 143 prolog_current_choice(C1), 144 Goal, 145 prolog_current_choice(C2), 146 ( arg(1, Solved, no) 147 ->true 148 ; send_comp_rtcheck(Goal, det, non_det) 149 ), 150 ( C1 == C2 151 ->! 152 ; nb_setarg(1, Solved, yes) 153 ). 154 155%! semidet(:Goal) 156% 157% Goal has zero or one solution 158 159:- global semidet/1. 160 161semidet(Goal) :- semidet(Goal, semidet). 162 163%! nondet(:Goal) 164% 165% Goal is non-deterministic. 166 167:- global nondet/1. 168 169nondet(Goal) :- Goal. 170 171%! multi(:Goal) 172% 173% Goal could have multiple solutions. 174 175:- global multi/1. 176 177multi(Goal) :- multi(Goal, multi). 178 179multi(Goal, Prop) :- 180 Solved = solved(no), 181 ( true 182 ; arg(1, Solved, no) 183 ->send_comp_rtcheck(Goal, Prop, failure), 184 fail 185 ), 186 prolog_current_choice(C1), 187 test_throws_2(Goal, Prop, _, true), 188 prolog_current_choice(C2), 189 ( C1 == C2 190 ->! 191 ; nb_setarg(1, Solved, yes) 192 ). 193 194%! not_fails(:Goal) 195% 196% Goal does not fail 197 198:- global not_fails(X) + equiv(multi(X)). 199 200not_fails(Goal) :- multi(Goal, not_fails). 201 202%! failure(:Goal) 203% 204% Goal always fail 205 206:- global failure/1. 207 208failure(Goal) :- failure(Goal, failure). 209 210%! fails(:Goal) 211% 212% Equivalent to failure/1 213 214:- global fails(X) + equiv(failure(X)). 215 216fails(Goal) :- failure(Goal, fails). 217 218failure(Goal, Prop) :- 219 Solved = solved(no), 220 test_throws_2(Goal, Prop, _, true), 221 ( arg(1, Solved, no) 222 ->send_comp_rtcheck(Goal, Prop, not_fails), 223 nb_setarg(1, Solved, yes) 224 ; true 225 ). 226 227 228%! is_det(:Goal) 229% 230% Goal is deterministic. Equivalent to semidet. 231 232:- global is_det(X) + equiv(semidet(X)). 233 234is_det(Goal) :- semidet(Goal, is_det). 235 236semidet(Goal, Prop) :- 237 Solved = solved(no), 238 Goal, 239 ( arg(1, Solved, no) 240 ->true 241 ; send_comp_rtcheck(Goal, Prop, non_det) 242 ), 243 nb_setarg(1, Solved, yes). 244 245%! non_det(:Goal) 246% 247% Goal is non-deterministic 248 249:- global non_det/1. 250 251non_det(Goal) :- 252 Solved = solved(no), 253 ( true 254 ; arg(1, Solved, one) 255 ->send_comp_rtcheck(Goal, non_det, is_det), 256 fail 257 ), 258 prolog_current_choice(C1), 259 Goal, 260 prolog_current_choice(C2), 261 ( arg(1, Solved, no) 262 ->( C2 == C1 263 ->!, 264 send_comp_rtcheck(Goal, non_det, no_choicepoints) 265 ; nb_setarg(1, Solved, one) 266 ) 267 ; nb_setarg(1, Solved, yes) 268 ). 269 270%! no_choicepoints(:Goal) 271% 272% Goal does not leave choicepoints on exit 273 274:- global no_choicepoints/1. 275 276no_choicepoints(Goal) :- 277 no_choicepoints(Goal, send_comp_rtcheck(Goal, no_choicepoints, has_choicepoints)). 278 279%! has_choicepoints(:Goal) 280% 281% Goal leave choicepoints on exit 282 283:- global has_choicepoints/1. 284 285has_choicepoints(Goal) :- 286 has_choicepoints(Goal, send_comp_rtcheck(Goal, has_choicepoints, no_choicepoints)). 287 288%! num_solutions_eq(Num:int, :Goal) 289% 290% Goal have Num solutions 291 292:- global num_solutions_eq/2. 293 294num_solutions_eq(N, Goal) :- 295 Sols = solutions(0), 296 ( true 297 ; arg(1, Sols, A), 298 ( ( A == done 299 ; A == N 300 ) 301 ->fail 302 ; send_comp_rtcheck(Goal, num_solutions_eq(N), Sols), 303 fail 304 ) 305 ), 306 prolog_current_choice(C1), 307 call(Goal), 308 prolog_current_choice(C2), 309 arg(1, Sols, A), 310 ( A == done 311 ->true 312 ; N1 is A+1, 313 ( C2 == C1 314 ->!, 315 ( N1 == N 316 ->true 317 ; send_comp_rtcheck(Goal, num_solutions_eq(N), num_solutions_eq(N1)) 318 ) 319 ; N1 > N 320 ->send_comp_rtcheck(Goal, num_solutions_eq(N), num_solutions(>(N))), 321 nb_setarg(1, Sols, done) 322 ; nb_setarg(1, Sols, N1) 323 ) 324 ).

330:- meta_predicate num_solutions(1, 0). 331:- global num_solutions/2 + meta_modes. 332 333num_solutions(Check, Goal) :- 334 Sols = num_solutions(0), 335 ( true 336 ; arg(1, Sols, N1), 337 ( call(Check, N1) 338 ->fail 339 ; send_comp_rtcheck(Goal, num_solutions(Check), num_solutions(N1)), 340 fail 341 ) 342 ), 343 prolog_current_choice(C1), 344 call(Goal), 345 prolog_current_choice(C2), 346 arg(1, Sols, N1), 347 N2 is N1+1, 348 ( C2 == C1 349 ->!, 350 ( call(Check, N2) 351 ->true 352 ; send_comp_rtcheck(Goal, num_solutions(Check), num_solutions(N1)) 353 ) 354 ; nb_setarg(1, Sols, N2) 355 ).

361:- meta_predicate solutions(+, 0). 362:- global solutions(+list, 0). 363 364solutions(Sols, Goal) :- 365 Goal = _:Sol, 366 Remaining = solutions(Sols), 367 ( true 368 ; arg(1, Remaining, Sols1), 369 ( ( Sols == done 370 ; Sols1 == [] 371 ) 372 ->fail 373 ; append(Sols3, Sols1, Sols), 374 send_comp_rtcheck(Goal, solutions(Sols), solutions(Sols3)), 375 fail 376 ) 377 ), 378 prolog_current_choice(C1), 379 call(Goal), 380 prolog_current_choice(C2), 381 arg(1, Remaining, Sols1), 382 ( Sols1 == done 383 ->true 384 ; [Elem|Sols2] = Sols1, 385 ( C2 == C1 386 ->!, 387 ( Elem \= Sol 388 ->append(Curr, Sols1, Sols), 389 append(Curr, [Sol], Sols3), 390 send_comp_rtcheck(Goal, solutions(Sols), solutions(Sols3)) 391 ; true 392 ) 393 ; Elem \= Sol 394 ->append(Curr, Sols1, Sols), 395 append(Curr, [Sol|_], Sols3), 396 send_comp_rtcheck(Goal, solutions(Sols), solutions(Sols3)), 397 nb_setarg(1, Remaining, done) 398 ; nb_setarg(1, Remaining, Sols2) 399 ) 400 ). 401 402%! database(:Goal) 403% 404% Goal will change the prolog database. 405 406:- global database/1. 407 408database(Goal) :- call(Goal). 409 410%! eval(:Goal) 411% 412% Goal is evaluable at compile-time. 413 414:- global eval/1. 415 416eval(Goal) :- call(Goal). 417 418%! dupclauses(:Goal) 419% 420% Goal is a predicate with duplicated clauses. 421 422:- global dupclauses/1 + (eval, database). 423 424dupclauses(M:Goal) :- 425 ( functor(Goal, F, A), 426 functor(Head1, F, A), 427 functor(Head2, F, A), 428 clause(M:Head1, Body1, Ref1), 429 clause(M:Head2, Body2, Ref2), 430 Ref1 \= Ref2, 431 (M:Head1 :- Body1) =@= (M:Head2 :- Body2) 432 ->true 433 ; send_comp_rtcheck(Goal, dupclauses, not(dupclauses)) 434 ), 435 call(Goal). 436 437:- thread_local signal_db/3. 438 439asserta_signal_check(Choice, _, E, _) :- asserta(signal_db(Choice, no, E)). 440asserta_signal_check(Choice, G, _, Thrown) :- 441 end_signal_check(Choice, G, Thrown), 442 fail. 443 444retract_signal_check(Choice, G, _, Thrown) :- end_signal_check(Choice, G, Thrown). 445retract_signal_check(Choice, _, E, _) :- asserta(signal_db(Choice, no, E)), fail. 446 447signal_prop(yes, E, signal(E, yes), signal(E, no )). 448signal_prop(no, E, signal(E, no ), signal(E, yes)). 449 450end_signal_check(Choice, Goal, CheckThrown) :- 451 retract(signal_db(Choice, Thrown, E)), 452 signal_prop(CheckThrown, E, EP, EV), 453 ( Thrown = CheckThrown 454 ->true 455 ; send_comp_rtcheck(Goal, EP, EV) 456 ). 457 458emit_signal(Choice, E) :- 459 retract(signal_db(Choice, _, _)), 460 assertz(signal_db(Choice, yes, E)). 461 462%! signal(:Goal) 463% 464% Goal sends a signal 465 466:- global signal/1. 467 468signal(Goal) :- signal(_, Goal). 469 470%! signal(:Goal, Signal) 471% 472% Goal sends a signal that unifies with Signal 473 474:- global signal/2. 475 476signal(Signal, Goal) :- 477 prolog_current_choice(Choice), 478 asserta_signal_check(Choice, Goal, Signal, yes), 479 prolog_current_choice(C1), 480 intercept(Goal, Signal, 481 ( emit_signal(Choice, Signal), 482 send_signal(Signal) 483 )), 484 prolog_current_choice(C2), 485 retract_signal_check(Choice, Goal, Signal, yes), 486 ( C1 == C2 487 ->! 488 ; true 489 ). 490 491%! no_signal(:Goal) 492% 493% Goal don't send any signal. 494 495:- global no_signal/1. 496 497no_signal(Goal) :- no_signal(_, Goal). 498 499%! no_signal(:Goal, Signal) 500% 501% Goal don't send signals that unifies with Signal 502 503:- global no_signal/2. 504 505no_signal(Signal, Goal) :- 506 prolog_current_choice(Choice), 507 asserta_signal_check(Choice, Goal, Signal, no), 508 prolog_current_choice(C1), 509 intercept(Goal, Signal, 510 ( emit_signal(Choice, Signal), 511 throw(Signal) 512 )), 513 prolog_current_choice(C2), 514 retract_signal_check(Choice, Goal, Signal, no), 515 ( C1 == C2 516 ->! 517 ; true 518 ). 519 520%! has_exception(:Goal) 521% 522% Goal throws an exception. 523 524:- global has_exception/1. 525 526has_exception(Goal) :- Goal, send_comp_rtcheck(Goal, has_exception, no_exception). 527 528%! throws_ex(Exception, :Goal) 529% 530% Goal can throw an exception that unifies with Exception 531 532:- global throws_ex/2. 533throws_ex(E, Goal) :- test_throws_2(Goal, throw(E), F, F \= E). 534 535:- meta_predicate test_throws_2(0, ?, ?, 0). 536test_throws_2(Goal, Prop, F, Test) :- 537 catch(Goal, F, 538 ( ( F \= assrchk(_), 539 Test 540 ->send_comp_rtcheck(Goal, Prop, has_exception(F)) 541 ; true 542 ), 543 throw(F) 544 )). 545 546%! has_exception(Exception, :Goal) 547% 548% Goal throws an exception that unifies with Exception 549 550:- global has_exception(E, Goal) + equiv(has_exception(throws_ex(E, Goal))). 551 552has_exception(E, Goal) :- 553 test_throws_2(Goal, has_exception(E), F, F \= E), 554 send_comp_rtcheck(Goal, has_exception(E), no_exception). 555 556%! no_exception(:Goal) 557% 558% Goal doesn't throw any exception. 559 560:- global no_exception/1. 561 562no_exception(Goal) :- test_throws_2(Goal, no_exception, _, true). 563 564%! no_exception(Exception, :Goal) 565% 566% Goal doesn't throw an exception that unifies with Exception 567 568:- global no_exception/2. 569 570no_exception(E, Goal) :- test_throws_2(Goal, no_exception(E), F, \+F \= E). 571 572%! throws_exs(Exceptions:List, :Goal) 573% 574% Goal can only throw the exceptions that unify with the elements of 575% Exceptions 576 577:- global throws_exs/2. 578 579throws_exs(EL, Goal) :- test_throws_2(Goal, throws_exs(EL), F, \+memberchk(F, EL)). 580 581%! signals(Signals:List, :Goal) 582% 583% Goal can generate only the signals that unify with the elements of 584% Signals 585% 586% @tbd proper implementation 587 588:- global signals/2. 589 590signals(_, Goal) :- call(Goal). 591 592%! meta_modes(:Goal) 593% 594% The modes for Goal are specified in the meta_predicate declaration. 595 596:- global meta_modes/1. 597 598meta_modes(Goal) :- call(Goal). 599 600%! no_meta_modes(:Goal) 601% 602% The modes for ~w are not specified in the meta_predicate declaration. 603 604:- global no_meta_modes/1. 605 606no_meta_modes(Goal) :- call(Goal). 607 608%! deprecated(:Goal) 609% 610% Specifies that the predicate marked with this global property has been 611% deprecated, i.e., its use is not recommended any more since it will be 612% deleted at a future date. Typically this is done because its functionality 613% has been superseded by another predicate. 614 615:- global declaration (deprecated)/1. 616 617deprecated(Goal) :- 618 send_comp_rtcheck(Goal, deprecated, called), 619 call(Goal). 620 621%! iso(:Goal) 622% 623% Complies with the ISO-Prolog standard. 624 625:- global iso/1. 626 627iso(Goal) :- call(Goal). 628 629%! nfi(Term, :Goal) 630% 631% On success of Goal, Term is not further instantiated. 632 633:- global nfi/2. 634 635nfi(V, Goal) :- 636 copy_term(V, X), 637 call(Goal), 638 ( subsumes_term(V, X) 639 ->true 640 ; send_comp_rtcheck(Goal, nfi(V), fi(X)) 641 ). 642 643:- global mve/2. 644 645mve(_, Goal) :- call(Goal). 646 647%! fi(Term, :Goal) 648% 649% On success of Goal, Term is further instantiated. 650 651:- global fi/2. 652 653fi(V, Goal) :- 654 copy_term(V, X), 655 call(Goal), 656 ( subsumes_term(V, X) 657 ->send_comp_rtcheck(Goal, fi(V), nfi(X)) 658 ; true 659 ). 660 661%! nsh(Term, :Goal) 662% 663% On call of Goal, Goal and Term don't share variables 664 665:- global nsh/2. 666nsh(Arg, Goal) :- check_nsh(Arg, Goal), call(Goal). 667 668check_nsh(Arg, _:Goal) :- 669 ( term_variables(Arg, Vars), 670 Vars \= [] 671 ->Goal =.. [_|Args], 672 ( select(Arg1, Args, Left), 673 Arg1 == Arg 674 ->term_variables(Left, GVars), 675 intersection(Vars, GVars, Shared), 676 ( Shared \= [] 677 ->send_comp_rtcheck(Goal, nsh, shared(Shared)) 678 ; true 679 ) 680 ; true 681 ) 682 ; true 683 ). 684 685%! user_output(+String, :Goal) 686% 687% Goal produces String as standard output 688 689:- global user_output/2. 690 691user_output(S, Goal) :- 692 setup_call_cleanup(new_memory_file(File), 693 use_output_mf(File, S, Goal), 694 free_memory_file(File)). 695 696use_output_mf(File, S, Goal) :- 697 asserta_user_output_check(File, S, Goal), 698 prolog_current_choice(C1), 699 catch(Goal, E, 700 ( end_output_check(File, S, Goal), 701 throw(E) 702 )), 703 prolog_current_choice(C2), 704 retract_user_output_check(File, S, Goal), 705 ( C1 == C2 706 ->!, 707 output_check(File, S, Goal) 708 ; true 709 ). 710 711asserta_user_output_check(File, _, _) :- 712 open_memory_file(File, write, Stream), 713 tell(Stream). 714asserta_user_output_check(File, S, Goal) :- 715 told, 716 output_check(File, S, Goal), 717 fail. 718 719retract_user_output_check(_, _, _) :- 720 told. 721retract_user_output_check(File, _, _) :- 722 open_memory_file(File, append, Stream), 723 append(Stream), 724 fail. 725 726end_output_check(File, S, Goal) :- told, output_check(File, S, Goal). 727 728output_check(File, S, Goal) :- 729 memory_file_to_string(File, S1), 730 format("~s", [S1]), 731 ( S \== S1 732 ->send_comp_rtcheck(Goal, user_output(S), user_output(S1)) 733 ; true 734 ), 735 !