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

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

  394compatc_arg(var(      A), A).
  395compatc_arg(nonvar(   A), A).
  396compatc_arg(term(     A), A).
  397compatc_arg(gnd(      A), A).
  398compatc_arg(ground(   A), A).
  399compatc_arg(nonground(A), A).
  400
  401freeze_fail(CP, Term, V, N) :-
  402    freeze(V, ( prolog_cut_to(CP),
  403                cleanup_prop_failure(Term, [nonvar(N), N==V]),
  404                fail
  405              )).
  406
  407:- global instan(Prop)
  408# "Uses Prop as an instantiation property. Verifies that execution of
  409   ~w does not produce bindings for the argument variables."-[Prop].
  410
  411:- meta_predicate instan(0).  412
  413instan(Goal) :-
  414    term_variables(Goal, VS),
  415    instan(Goal, VS).
  416
  417:- meta_predicate instan(0, +).  418
  419instan(Goal, VS) :-
  420    prolog_current_choice(CP),
  421    \+ \+ ( copy_term_nat(Goal-VS, Term-VN),
  422            maplist(freeze_fail(CP, Term), VS, VN),
  423            with_context_value(Goal, checkprop, instan)
  424          )