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

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

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