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