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(choicepoints)).   77:- use_module(library(assertions)).   78:- use_module(library(intercept)).   79:- use_module(library(metaprops)).   80:- use_module(library(typeprops)).   81:- use_module(library(send_check)).

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:

*/

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