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