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(metaprops,
   36          [(declaration)/1,
   37           (declaration)/2,
   38           (global)/1,
   39           (global)/2,
   40           (type)/1,
   41           (type)/2,
   42           checkprop_goal/1,
   43           compat/1,
   44           compat/2,
   45           with_cv_module/2,
   46           cv_module/1,
   47           instan/1,
   48           instan/2,
   49           last_prop_failure/1
   50          ]).   51
   52:- use_module(library(assertions)).   53:- use_module(library(resolve_calln)).   54:- use_module(library(context_values)).   55:- use_module(library(extend_args)).   56:- use_module(library(qualify_meta_goal)).   57
   58:- true prop (type)/1 + (declaration(check), global(prop)) # "Defines a type.".
   59
   60type(Goal) :- call(Goal).
   61
   62:- true prop (global)/1 + (global(prop), declaration)
   63# "A property that is global, i.e., can appear after the + in the assertion.
   64and as meta predicates, meta_predicate F(0)".
   65
   66global(Goal) :- call(Goal).
   67
   68:- type assrt_type/1, assrt_status/1.
   69
   70:- global global(Prop, Goal) : (assrt_type(Prop), callable(Goal))
   71# "Like global/1, but allows to specify the default assertion type".
   72
   73global(_, Goal) :- call(Goal).
   74
   75:- true prop (declaration)/1 + (global(prop), declaration)
   76# "A property that is a declaration, i.e., an operator is added as op(1125, fx, F). Implies global/1".
   77
   78declaration(Goal) :- call(Goal).
   79
   80:- true prop declaration(Status, Goal) : (assrt_status(Status), callable(Goal)) + global(prop)
   81# "Like declaration/1, but allows to specify the default assertion status".
   82
   83declaration(_, Goal) :- call(Goal).
   84
   85:- true prop cv_module/1.
   86
   87cv_module(CM) :-
   88    current_context_value(current_module, CM),
   89    !.
   90cv_module(user).
   91
   92:- true prop type(T, A)
   93# "~w is internally of type ~w, a predicate of arity 1 defined as a type/1."-[A, T].
   94
   95:- meta_predicate
   96        type(1, ?),
   97        type(1, ?, -).   98
   99type(M:T, A) :-
  100    type(M:T, A, H),
  101    M:H.
  102
  103type(M:T, A, H) :-
  104    extend_args(T, [Arg], H),
  105    ( cv_module(C),
  106      predicate_property(M:H, meta_predicate(Spec)),
  107      functor(H, _, N),
  108      arg(N, Spec, Meta),
  109      '$expand':meta_arg(Meta)
  110    ->Arg = C:A
  111    ; Arg = A
  112    ).
  113
  114:- multifile
  115    unfold_calls:unfold_call_hook/4.  116
  117unfold_calls:unfold_call_hook(type(T, A), metaprops, M, M:call(T, A)).
  118
  119:- true prop compat(Prop)
  120# "Uses ~w as a compatibility property."-[Prop].
  121
  122:- meta_predicate compat(0 ).  123
  124compat(M:Goal) :-
  125    term_variables(Goal, VS),
  126    compat(M:Goal, VS).
  127
  128:- use_module(library(gcb)).  129:- use_module(library(list_sequence)).  130:- use_module(library(substitute)).  131:- use_module(library(clambda)).  132:- use_module(library(terms_share)).  133
  134:- thread_local
  135        '$last_prop_failure'/2.  136
  137generalize_term(STerm, Term, _) :-
  138    \+ terms_share(STerm, Term).
  139
  140neg(nonvar(A), var(A)).
  141neg(A==B,  A \== B).
  142neg(A =B,  A  \= B).
  143neg(A=:=B, A =\= B).
  144neg(A,     \+A).
  145
  146current_prop_failure((SG :- Body)) :-
  147    '$last_prop_failure'(Term, SubU),
  148    sort(SubU, Sub),
  149    greatest_common_binding(Term, Sub, ST, SSub, [[]], Unifier, []),
  150    substitute(generalize_term(SSub), ST, SG),
  151    maplist(\ A^NA^once(neg(A, NA)), SSub, NSub),
  152    foldl(simplify_unifier(SG-SSub), Unifier, LitL, NSub),
  153    LitL \= [],
  154    list_sequence(LitL, Body).
  155
  156simplify_unifier(Term, A=B) -->
  157    ( {occurrences_of_var(A, Term, 0 )}
  158    ->{A=B}
  159    ; [A=B]
  160    ).
  161
  162last_prop_failure(L) :-
  163    findall(E, once(current_prop_failure(E)), L),
  164    retractall('$last_prop_failure'(_, _)).
  165
  166asserta_prop_failure(T, S) :-
  167    once(( retract('$last_prop_failure'(T, L))
  168         ; L = []
  169         )),
  170    asserta('$last_prop_failure'(T, [S|L])).
  171
  172cleanup_prop_failure(T, S) :-
  173    retractall('$last_prop_failure'(_, _)),
  174    asserta('$last_prop_failure'(T, S)).
  175
  176:- meta_predicate with_cv_module(0, +).  177with_cv_module(Goal, CM) :-
  178    with_context_value(Goal, current_module, CM).
  179
  180:- meta_predicate checkprop_goal(0 ).  181checkprop_goal(Goal) :-
  182    ( current_context_value(checkprop, CheckProp)
  183    ->CheckProp = compat
  184    ; Goal
  185    ).
  186
  187:- meta_predicate compat(0, +).  188
  189compat(M:Goal, VarL) :-
  190    copy_term_nat(Goal-VarL, Term-VarTL), % get rid of corroutining while checking compatibility
  191    sort(VarTL, VS),
  192    cleanup_prop_failure(Term, []),
  193    prolog_current_choice(CP),
  194    with_context_value(
  195        compat(Term, data(VS, Term, CP), M), checkprop, compat).
  196
  197% this small interpreter will reduce the possibility of loops if the goal being
  198% checked is not linear, i.e., if it contains linked variables:
  199compat(Var, _, _) :- var(Var), !.
  200compat(M:Goal, D, _) :-
  201    !,
  202    compat(Goal, D, M).
  203compat(A, D, M) :-
  204    do_resolve_calln(A, B),
  205    !,
  206    compat(B, D, M).
  207compat((A, B), D, M) :-
  208    !,
  209    compat(A, D, M),
  210    compat(B, D, M).
  211compat(type(T, A), D, M) :-
  212    !,
  213    strip_module(M:T, C, H),
  214    type(C:H, A, G),
  215    compat(G, D, C).
  216compat(compat(A), D, M) :-
  217    !,
  218    compat(A, D, M).
  219compat((A->B; C), D, M) :-
  220    !,
  221    ( call(M:A)
  222    ->compat(B, D, M)
  223    ; compat(C, D, M)
  224    ),
  225    !.
  226compat(\+ G, _, M) :-
  227    !,
  228    \+ M:G.
  229compat((A->B), D, M) :-
  230    !,
  231    ( call(M:A)
  232    ->compat(B, D, M)
  233    ).
  234compat(!, data(_, _, CP), _) :-
  235    !,
  236    cut_from(CP).
  237compat(checkprop_goal(_), _, _) :- !.
  238compat(with_cv_module(A, C), D, M) :-
  239    !,
  240    with_cv_module(compat(A, D, M), C).
  241compat(var(V), _, _) :-
  242    nonvar(V),
  243    !,
  244    fail.
  245compat(A, data(VarL, _, _), M) :-
  246    % This clause allows usage of simple test predicates as compatibility check
  247    compound(A),
  248    A \= (_;_),
  249    compatc(A, VarL, M),
  250    !.
  251compat(Term, D, M) :-
  252    D = data(_, T, _),
  253    asserta_prop_failure(T, Term),
  254    compat_1(Term, D, M),
  255    cleanup_prop_failure(T, []).
  256
  257% NOTE: The cut in compat_1 assume that is safe to do it.  That happens when the
  258% arguments of the Goal do not share with other parts of the check that could
  259% eventually lead the execution to a failure and backtrack.
  260
  261compat_1((A; B), D, M) :-
  262    ( compat(A, D, M)
  263    ; compat(B, D, M)
  264    ),
  265    !.
  266compat_1(@(A, C), D, M) :-
  267    !,
  268    compat_1(A, @(M:A, C), D, C, M).
  269compat_1(A, D, M) :-
  270    compat_1(A, M:A, D, M, M).
  271
  272compat_1(A, G, D, C, M) :-
  273    ( is_type(A, M)
  274    ->catch(compat_body(A, C, M, D),
  275            _,
  276            do_compat(G, D))
  277    ; \+ ( \+ compat_safe(A, M),
  278           \+ ground(A),
  279           \+ aux_pred(A),
  280           \+ is_prop(A, M),
  281           print_message(warning, format("While checking compat, direct execution of predicate could cause infinite loops: ~q", [G-D])),
  282           fail
  283         ),
  284      do_compat(G, D)
  285    ),
  286    !.
  287
  288aux_pred(P) :-
  289    functor(P, F, _),
  290    atom_concat('__aux_', _, F).
  291
  292compat_safe(_ =.. _, _).
  293compat_safe(_ is _, _).
  294compat_safe(call_cm(_, _, _), _).
  295compat_safe(context_module(_), _).
  296compat_safe(curr_arithmetic_function(_), _).
  297compat_safe(current_predicate(_), _).
  298compat_safe(functor(_, _, _), _).
  299compat_safe(goal_2(_, _), _).
  300compat_safe(prop_asr(_, _, _, _), _).
  301compat_safe(static_strip_module(_, _, _, _), _).
  302
  303do_compat(Goal, data(VarL, _, _)) :-
  304    term_variables(VarL, VS),
  305    prolog_current_choice(CP),
  306    maplist(freeze_cut(CP), VS),
  307    Goal,
  308    maplist(del_freeze, VS).
  309
  310del_freeze(Var) :-
  311    ( attvar(Var)
  312    ->del_attr(Var, freeze)
  313    ; true
  314    ).
  315
  316is_prop(Head, M) :-
  317    prop_asr(Head, M, Stat, prop, _, _, _),
  318    memberchk(Stat, [check, true]).
  319
  320is_type(Head, M) :-
  321    once(( prop_asr(Head, M, Stat, prop, _, _, Asr),
  322           memberchk(Stat, [check, true]),
  323           once(prop_asr(glob, type(_), _, Asr))
  324         )).
  325
  326:- meta_predicate compat_body(0,+,+,+,+).  327
  328compat_body(MG, C, V, T, CP) :-
  329    clause(MG, Body, Ref),
  330    clause_property(Ref, module(S)), % Source module
  331    ( predicate_property(MG, transparent),
  332      \+ ( predicate_property(MG, meta_predicate(Meta)),
  333           arg(_, Meta, Spec),
  334           '$expand':meta_arg(Spec)
  335         )
  336    ->CM = C
  337    ; CM = S
  338    ),
  339    compat(Body, data(V, T, CP), CM).
  340
  341compat_body(G1, C, M, data(V, T, _)) :-
  342    qualify_meta_goal(G1, M, C, G),
  343    prolog_current_choice(CP),
  344    compat_body(M:G, C, V, T, CP).
  345
  346:- use_module(library(safe_prolog_cut_to)).  347
  348cut_from(CP) :- catch(safe_prolog_cut_to(CP), _, true).
  349
  350freeze_cut(CP, V) :-
  351    freeze(V, catch(prolog_cut_to(CP), _, true)).
  352
  353compatc(H, VarL, M) :-
  354    functor(H, _, N),
  355    arg(N, H, A),
  356    ( var(A),
  357      ord_intersect(VarL, [A], [A])
  358    ; predicate_property(M:H, meta_predicate(Spec)),
  359      arg(N, Spec, Meta),
  360      '$expand':meta_arg(Meta),
  361      A = X:Y,
  362      ( ( var(X)
  363        ; current_module(X)
  364        )
  365      ->var(Y),
  366        ord_intersect(VarL, [Y], [Y])
  367      )
  368    ),
  369    !.
  370compatc(H, VarL, _) :-
  371    compatc_arg(H, A),
  372    ( var(A)
  373    ->ord_intersect(VarL, [A], [A])
  374    ; true
  375    ).

 compatc_arg(+Call, Arg) is semidet

True if Call is a call that is always true when the last argument is any term, or if Call is var(Arg).

  382compatc_arg(var(      A), A).
  383compatc_arg(nonvar(   A), A).
  384compatc_arg(term(     A), A).
  385compatc_arg(gnd(      A), A).
  386compatc_arg(ground(   A), A).
  387compatc_arg(nonground(A), A).
  388
  389freeze_fail(CP, Term, V, N) :-
  390    freeze(V, ( prolog_cut_to(CP),
  391                cleanup_prop_failure(Term, [nonvar(N), N==V]),
  392                fail
  393              )).
  394
  395:- global instan(Prop)
  396# "Uses Prop as an instantiation property. Verifies that execution of
  397   ~w does not produce bindings for the argument variables."-[Prop].
  398
  399:- meta_predicate instan(0).  400
  401instan(Goal) :-
  402    term_variables(Goal, VS),
  403    instan(Goal, VS).
  404
  405:- meta_predicate instan(0, +).  406
  407instan(Goal, VS) :-
  408    prolog_current_choice(CP),
  409    \+ \+ ( copy_term_nat(Goal-VS, Term-VN),
  410            maplist(freeze_fail(CP, Term), VS, VN),
  411            with_context_value(Goal, checkprop, instan)
  412          )