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

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

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 !